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