333 lines
10 KiB
Text
333 lines
10 KiB
Text
|
S0(1)R0(1)Richiesta(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
MARKING T1 (tangible)
|
||
|
|
[T1 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T2 # ordinary markings : 1
|
||
|
|
S0(1)R0(1)Attesa(1<Master_00>)Buffer_input(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T2 (tangible)
|
||
|
|
[T3 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T3 # ordinary markings : 1
|
||
|
|
R0(1)S1_a(1<Master_00>)S1_b(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T2 (tangible)
|
||
|
|
[T9 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T4 # ordinary markings : 1
|
||
|
|
S0(1)R_1(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T3 (tangible)
|
||
|
|
[T4 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T5 # ordinary markings : 1
|
||
|
|
R0(1)S1_b(1<Master_00>)S2_a(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T3 (tangible)
|
||
|
|
[T5 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T6 # ordinary markings : 1
|
||
|
|
R0(1)S1_a(1<Master_00>)S2_b(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T4 (tangible)
|
||
|
|
[T8 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T7 # ordinary markings : 1
|
||
|
|
S0(1)R_2(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T5 (tangible)
|
||
|
|
[T5 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T8 # ordinary markings : 1
|
||
|
|
R0(1)S2_b(1<Master_00>)S2_a(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T6 (tangible)
|
||
|
|
[T4 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T8 # ordinary markings : 1
|
||
|
|
R0(1)S2_b(1<Master_00>)S2_a(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T7 (tangible)
|
||
|
|
[T7 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T9 # ordinary markings : 1
|
||
|
|
S0(1)R3(1)Attesa(1<Master_00>)Buffer_output(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T8 (tangible)
|
||
|
|
[T6 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T10 # ordinary markings : 1
|
||
|
|
R0(1)S3(1)Attesa(1<Master_00>)Buffer_output(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T9 (tangible)
|
||
|
|
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T11 # ordinary markings : 1
|
||
|
|
S0(1)R0(1)Attesa(1<Master_00>)Buffer_output(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T9 (tangible)
|
||
|
|
[T2 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T12 # ordinary markings : 1
|
||
|
|
S0(1)R3(1)Elabora(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T10 (tangible)
|
||
|
|
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T11 # ordinary markings : 1
|
||
|
|
S0(1)R0(1)Attesa(1<Master_00>)Buffer_output(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T10 (tangible)
|
||
|
|
[T2 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T13 # ordinary markings : 1
|
||
|
|
R0(1)S3(1)Elabora(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T11 (tangible)
|
||
|
|
[T2 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T14 # ordinary markings : 1
|
||
|
|
S0(1)R0(1)Elabora(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T12 (tangible)
|
||
|
|
[T0 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T15 # ordinary markings : 1
|
||
|
|
S0(1)R3(1)Richiesta(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T12 (tangible)
|
||
|
|
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T14 # ordinary markings : 1
|
||
|
|
S0(1)R0(1)Elabora(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T13 (tangible)
|
||
|
|
[T0 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T16 # ordinary markings : 1
|
||
|
|
R0(1)S3(1)Richiesta(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T13 (tangible)
|
||
|
|
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T14 # ordinary markings : 1
|
||
|
|
S0(1)R0(1)Elabora(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T14 (tangible)
|
||
|
|
[T0 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T1 # ordinary markings : 1
|
||
|
|
S0(1)R0(1)Richiesta(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T15 (tangible)
|
||
|
|
[T1 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T17 # ordinary markings : 1
|
||
|
|
S0(1)R3(1)Attesa(1<Master_00>)Buffer_input(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T15 (tangible)
|
||
|
|
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T1 # ordinary markings : 1
|
||
|
|
S0(1)R0(1)Richiesta(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T16 (tangible)
|
||
|
|
[T1 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T18 # ordinary markings : 1
|
||
|
|
R0(1)S3(1)Attesa(1<Master_00>)Buffer_input(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T16 (tangible)
|
||
|
|
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T1 # ordinary markings : 1
|
||
|
|
S0(1)R0(1)Richiesta(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T17 (tangible)
|
||
|
|
[T3 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T19 # ordinary markings : 1
|
||
|
|
S1_a(1<Master_00>)S1_b(1<Master_00>)R3(1)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T17 (tangible)
|
||
|
|
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T2 # ordinary markings : 1
|
||
|
|
S0(1)R0(1)Attesa(1<Master_00>)Buffer_input(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T18 (tangible)
|
||
|
|
[T9 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T20 # ordinary markings : 1
|
||
|
|
R_1(1<Master_00>)S3(1)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T18 (tangible)
|
||
|
|
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T2 # ordinary markings : 1
|
||
|
|
S0(1)R0(1)Attesa(1<Master_00>)Buffer_input(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T19 (tangible)
|
||
|
|
[T4 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T21 # ordinary markings : 1
|
||
|
|
S1_b(1<Master_00>)R3(1)S2_a(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T19 (tangible)
|
||
|
|
[T5 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T22 # ordinary markings : 1
|
||
|
|
S1_a(1<Master_00>)R3(1)S2_b(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T19 (tangible)
|
||
|
|
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T3 # ordinary markings : 1
|
||
|
|
R0(1)S1_a(1<Master_00>)S1_b(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T20 (tangible)
|
||
|
|
[T8 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T23 # ordinary markings : 1
|
||
|
|
R_2(1<Master_00>)S3(1)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T20 (tangible)
|
||
|
|
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T4 # ordinary markings : 1
|
||
|
|
S0(1)R_1(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T21 (tangible)
|
||
|
|
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T5 # ordinary markings : 1
|
||
|
|
R0(1)S1_b(1<Master_00>)S2_a(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T21 (tangible)
|
||
|
|
[T5 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T24 # ordinary markings : 1
|
||
|
|
R3(1)S2_b(1<Master_00>)S2_a(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T22 (tangible)
|
||
|
|
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T6 # ordinary markings : 1
|
||
|
|
R0(1)S1_a(1<Master_00>)S2_b(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T22 (tangible)
|
||
|
|
[T4 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T24 # ordinary markings : 1
|
||
|
|
R3(1)S2_b(1<Master_00>)S2_a(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T23 (tangible)
|
||
|
|
[T7 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T25 # ordinary markings : 1
|
||
|
|
R3(1)S3(1)Attesa(1<Master_00>)Buffer_output(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T23 (tangible)
|
||
|
|
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T7 # ordinary markings : 1
|
||
|
|
S0(1)R_2(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T24 (tangible)
|
||
|
|
[T6 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T25 # ordinary markings : 1
|
||
|
|
R3(1)S3(1)Attesa(1<Master_00>)Buffer_output(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T24 (tangible)
|
||
|
|
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T8 # ordinary markings : 1
|
||
|
|
R0(1)S2_b(1<Master_00>)S2_a(1<Master_00>)Attesa(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T25 (tangible)
|
||
|
|
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T10 # ordinary markings : 1
|
||
|
|
R0(1)S3(1)Attesa(1<Master_00>)Buffer_output(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T25 (tangible)
|
||
|
|
[T2 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T26 # ordinary markings : 1
|
||
|
|
R3(1)S3(1)Elabora(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T25 (tangible)
|
||
|
|
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T9 # ordinary markings : 1
|
||
|
|
S0(1)R3(1)Attesa(1<Master_00>)Buffer_output(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T26 (tangible)
|
||
|
|
[T0 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T27 # ordinary markings : 1
|
||
|
|
R3(1)S3(1)Richiesta(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T26 (tangible)
|
||
|
|
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T12 # ordinary markings : 1
|
||
|
|
S0(1)R3(1)Elabora(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T26 (tangible)
|
||
|
|
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T13 # ordinary markings : 1
|
||
|
|
R0(1)S3(1)Elabora(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T27 (tangible)
|
||
|
|
[T1 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
|
||
|
|
MARKING T28 # ordinary markings : 1
|
||
|
|
R3(1)S3(1)Attesa(1<Master_00>)Buffer_input(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T27 (tangible)
|
||
|
|
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T16 # ordinary markings : 1
|
||
|
|
R0(1)S3(1)Richiesta(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T27 (tangible)
|
||
|
|
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T15 # ordinary markings : 1
|
||
|
|
S0(1)R3(1)Richiesta(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T28 (tangible)
|
||
|
|
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T17 # ordinary markings : 1
|
||
|
|
S0(1)R3(1)Attesa(1<Master_00>)Buffer_input(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
MARKING T28 (tangible)
|
||
|
|
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
|
||
|
|
MARKING T18 # ordinary markings : 1
|
||
|
|
R0(1)S3(1)Attesa(1<Master_00>)Buffer_input(1<Master_00>)
|
||
|
|
|Master_00|=1
|
||
|
|
|
||
|
|
|
||
|
|
***** Symbolic Reachability Graph *****
|
||
|
|
|
||
|
|
TANGIBLE MARKINGS : 28
|
||
|
|
VANISHING MARKINGS : 0
|
||
|
|
DEAD MARKINGS : 0
|
||
|
|
|
||
|
|
TOTAL MARKINGS : 28
|
||
|
|
|
||
|
|
***************************************
|
||
|
|
|
||
|
|
Ordinary tangible markings : 28
|
||
|
|
Ordinary vanishing markings : 0
|
||
|
|
Ordinary dead markings : 0
|
||
|
|
The initial marking is a home state
|
||
|
|
Time required ----------> 0
|
||
|
|
|
||
|
|
***************************************
|