204 lines
6.6 KiB
Text
204 lines
6.6 KiB
Text
digraph RG {
|
|
T1 [ label="S0(1) M0(2)
|
|
"];
|
|
T2 [ label="S0(1) M0(1) M1(1)
|
|
"];
|
|
T1 -> T2 [ label=<azione_locale_m>];
|
|
T3 [ label="S0(1) Buffer_input(1) M0(1) M2(1)
|
|
"];
|
|
T2 -> T3 [ label=<Richiesta_Servizio>];
|
|
T4 [ label="S0(1) M1(2)
|
|
"];
|
|
T2 -> T4 [ label=<azione_locale_m>];
|
|
T5 [ label="S1_a(1) S1_b(1) M0(1) M2(1)
|
|
"];
|
|
T3 -> T5 [ label=<Inizio_Servizio>];
|
|
T6 [ label="S0(1) Buffer_input(1) M1(1) M2(1)
|
|
"];
|
|
T3 -> T6 [ label=<azione_locale_m>];
|
|
T4 -> T6 [ label=<Richiesta_Servizio>];
|
|
T7 [ label="S1_b(1) S2_a(1) M0(1) M2(1)
|
|
"];
|
|
T5 -> T7 [ label=<azione_locale_sa>];
|
|
T8 [ label="S1_a(1) S2_b(1) M0(1) M2(1)
|
|
"];
|
|
T5 -> T8 [ label=<azione_locale_sb>];
|
|
T9 [ label="S1_a(1) S1_b(1) M1(1) M2(1)
|
|
"];
|
|
T5 -> T9 [ label=<azione_locale_m>];
|
|
T10 [ label="S0(1) Buffer_input(2) M2(2)
|
|
"];
|
|
T6 -> T10 [ label=<Richiesta_Servizio>];
|
|
T6 -> T9 [ label=<Inizio_Servizio>];
|
|
T11 [ label="S1_b(1) S2_a(1) M1(1) M2(1)
|
|
"];
|
|
T7 -> T11 [ label=<azione_locale_m>];
|
|
T12 [ label="S2_a(1) S2_b(1) M0(1) M2(1)
|
|
"];
|
|
T7 -> T12 [ label=<azione_locale_sb>];
|
|
T13 [ label="S1_a(1) S2_b(1) M1(1) M2(1)
|
|
"];
|
|
T8 -> T13 [ label=<azione_locale_m>];
|
|
T8 -> T12 [ label=<azione_locale_sa>];
|
|
T14 [ label="S1_a(1) S1_b(1) Buffer_input(1) M2(2)
|
|
"];
|
|
T9 -> T14 [ label=<Richiesta_Servizio>];
|
|
T9 -> T13 [ label=<azione_locale_sb>];
|
|
T9 -> T11 [ label=<azione_locale_sa>];
|
|
T10 -> T14 [ label=<Inizio_Servizio>];
|
|
T15 [ label="S1_b(1) S2_a(1) Buffer_input(1) M2(2)
|
|
"];
|
|
T11 -> T15 [ label=<Richiesta_Servizio>];
|
|
T16 [ label="S2_a(1) S2_b(1) M1(1) M2(1)
|
|
"];
|
|
T11 -> T16 [ label=<azione_locale_sb>];
|
|
T17 [ label="S3(1) Buffer_output(1) M0(1) M2(1)
|
|
"];
|
|
T12 -> T17 [ label=<Fine_Servizio>];
|
|
T12 -> T16 [ label=<azione_locale_m>];
|
|
T18 [ label="S1_a(1) S2_b(1) Buffer_input(1) M2(2)
|
|
"];
|
|
T13 -> T18 [ label=<Richiesta_Servizio>];
|
|
T13 -> T16 [ label=<azione_locale_sa>];
|
|
T14 -> T15 [ label=<azione_locale_sa>];
|
|
T14 -> T18 [ label=<azione_locale_sb>];
|
|
T19 [ label="S2_a(1) S2_b(1) Buffer_input(1) M2(2)
|
|
"];
|
|
T15 -> T19 [ label=<azione_locale_sb>];
|
|
T20 [ label="S3(1) Buffer_output(1) M1(1) M2(1)
|
|
"];
|
|
T16 -> T20 [ label=<Fine_Servizio>];
|
|
T16 -> T19 [ label=<Richiesta_Servizio>];
|
|
T21 [ label="S0(1) Buffer_output(1) M0(1) M2(1)
|
|
"];
|
|
T17 -> T21 [ label=<Reset>];
|
|
T22 [ label="S3(1) M0(1) M3(1)
|
|
"];
|
|
T17 -> T22 [ label=<Attesa_Elaborazione>];
|
|
T17 -> T20 [ label=<azione_locale_m>];
|
|
T18 -> T19 [ label=<azione_locale_sa>];
|
|
T23 [ label="S3(1) Buffer_output(1) Buffer_input(1) M2(2)
|
|
"];
|
|
T19 -> T23 [ label=<Fine_Servizio>];
|
|
T24 [ label="S0(1) Buffer_output(1) M1(1) M2(1)
|
|
"];
|
|
T20 -> T24 [ label=<Reset>];
|
|
T25 [ label="S3(1) M1(1) M3(1)
|
|
"];
|
|
T20 -> T25 [ label=<Attesa_Elaborazione>];
|
|
T20 -> T23 [ label=<Richiesta_Servizio>];
|
|
T21 -> T24 [ label=<azione_locale_m>];
|
|
T26 [ label="S0(1) M0(1) M3(1)
|
|
"];
|
|
T21 -> T26 [ label=<Attesa_Elaborazione>];
|
|
T27 [ label="S3(1) M0(2)
|
|
"];
|
|
T22 -> T27 [ label=<Reset_M>];
|
|
T22 -> T25 [ label=<azione_locale_m>];
|
|
T22 -> T26 [ label=<Reset>];
|
|
T28 [ label="S0(1) Buffer_output(1) Buffer_input(1) M2(2)
|
|
"];
|
|
T23 -> T28 [ label=<Reset>];
|
|
T29 [ label="S3(1) Buffer_input(1) M2(1) M3(1)
|
|
"];
|
|
T23 -> T29 [ label=<Attesa_Elaborazione>];
|
|
T24 -> T28 [ label=<Richiesta_Servizio>];
|
|
T30 [ label="S0(1) M1(1) M3(1)
|
|
"];
|
|
T24 -> T30 [ label=<Attesa_Elaborazione>];
|
|
T31 [ label="S3(1) M0(1) M1(1)
|
|
"];
|
|
T25 -> T31 [ label=<Reset_M>];
|
|
T25 -> T29 [ label=<Richiesta_Servizio>];
|
|
T25 -> T30 [ label=<Reset>];
|
|
T26 -> T1 [ label=<Reset_M>];
|
|
T26 -> T30 [ label=<azione_locale_m>];
|
|
T27 -> T1 [ label=<Reset>];
|
|
T27 -> T31 [ label=<azione_locale_m>];
|
|
T32 [ label="S1_a(1) S1_b(1) Buffer_output(1) M2(2)
|
|
"];
|
|
T28 -> T32 [ label=<Inizio_Servizio>];
|
|
T33 [ label="S0(1) Buffer_input(1) M2(1) M3(1)
|
|
"];
|
|
T28 -> T33 [ label=<Attesa_Elaborazione>];
|
|
T34 [ label="S3(1) Buffer_input(1) M0(1) M2(1)
|
|
"];
|
|
T29 -> T34 [ label=<Reset_M>];
|
|
T29 -> T33 [ label=<Reset>];
|
|
T30 -> T2 [ label=<Reset_M>];
|
|
T30 -> T33 [ label=<Richiesta_Servizio>];
|
|
T35 [ label="S3(1) M1(2)
|
|
"];
|
|
T31 -> T35 [ label=<azione_locale_m>];
|
|
T31 -> T2 [ label=<Reset>];
|
|
T31 -> T34 [ label=<Richiesta_Servizio>];
|
|
T36 [ label="S1_b(1) S2_a(1) Buffer_output(1) M2(2)
|
|
"];
|
|
T32 -> T36 [ label=<azione_locale_sa>];
|
|
T37 [ label="S1_a(1) S2_b(1) Buffer_output(1) M2(2)
|
|
"];
|
|
T32 -> T37 [ label=<azione_locale_sb>];
|
|
T38 [ label="S1_a(1) S1_b(1) M2(1) M3(1)
|
|
"];
|
|
T32 -> T38 [ label=<Attesa_Elaborazione>];
|
|
T33 -> T3 [ label=<Reset_M>];
|
|
T33 -> T38 [ label=<Inizio_Servizio>];
|
|
T39 [ label="S3(1) Buffer_input(1) M1(1) M2(1)
|
|
"];
|
|
T34 -> T39 [ label=<azione_locale_m>];
|
|
T34 -> T3 [ label=<Reset>];
|
|
T35 -> T39 [ label=<Richiesta_Servizio>];
|
|
T35 -> T4 [ label=<Reset>];
|
|
T40 [ label="S1_b(1) S2_a(1) M2(1) M3(1)
|
|
"];
|
|
T36 -> T40 [ label=<Attesa_Elaborazione>];
|
|
T41 [ label="S2_a(1) S2_b(1) Buffer_output(1) M2(2)
|
|
"];
|
|
T36 -> T41 [ label=<azione_locale_sb>];
|
|
T42 [ label="S1_a(1) S2_b(1) M2(1) M3(1)
|
|
"];
|
|
T37 -> T42 [ label=<Attesa_Elaborazione>];
|
|
T37 -> T41 [ label=<azione_locale_sa>];
|
|
T38 -> T5 [ label=<Reset_M>];
|
|
T38 -> T42 [ label=<azione_locale_sb>];
|
|
T38 -> T40 [ label=<azione_locale_sa>];
|
|
T43 [ label="S3(1) Buffer_input(2) M2(2)
|
|
"];
|
|
T39 -> T43 [ label=<Richiesta_Servizio>];
|
|
T39 -> T6 [ label=<Reset>];
|
|
T40 -> T7 [ label=<Reset_M>];
|
|
T44 [ label="S2_a(1) S2_b(1) M2(1) M3(1)
|
|
"];
|
|
T40 -> T44 [ label=<azione_locale_sb>];
|
|
T45 [ label="S3(1) Buffer_output(2) M2(2)
|
|
"];
|
|
T41 -> T45 [ label=<Fine_Servizio>];
|
|
T41 -> T44 [ label=<Attesa_Elaborazione>];
|
|
T42 -> T8 [ label=<Reset_M>];
|
|
T42 -> T44 [ label=<azione_locale_sa>];
|
|
T43 -> T10 [ label=<Reset>];
|
|
T46 [ label="S3(1) Buffer_output(1) M2(1) M3(1)
|
|
"];
|
|
T44 -> T46 [ label=<Fine_Servizio>];
|
|
T44 -> T12 [ label=<Reset_M>];
|
|
T47 [ label="S0(1) Buffer_output(2) M2(2)
|
|
"];
|
|
T45 -> T47 [ label=<Reset>];
|
|
T45 -> T46 [ label=<Attesa_Elaborazione>];
|
|
T48 [ label="S0(1) Buffer_output(1) M2(1) M3(1)
|
|
"];
|
|
T46 -> T48 [ label=<Reset>];
|
|
T49 [ label="S3(1) M3(2)
|
|
"];
|
|
T46 -> T49 [ label=<Attesa_Elaborazione>];
|
|
T46 -> T17 [ label=<Reset_M>];
|
|
T47 -> T48 [ label=<Attesa_Elaborazione>];
|
|
T48 -> T21 [ label=<Reset_M>];
|
|
T50 [ label="S0(1) M3(2)
|
|
"];
|
|
T48 -> T50 [ label=<Attesa_Elaborazione>];
|
|
T49 -> T22 [ label=<Reset_M>];
|
|
T49 -> T50 [ label=<Reset>];
|
|
T50 -> T26 [ label=<Reset_M>];
|
|
report [ style = "filled, bold" penwidth = 5 fillcolor = "white" shape=box label=<<table border="0" cellborder="0" cellpadding="3" bgcolor="white"><tr><td bgcolor="black" align="center" colspan="2"><font color="white">Reachability Graph</font></td></tr><tr><td align="left" colspan="2">Showing all markings.</td></tr><tr><td align="left">Total markings:</td><td>50</td></tr></table>> ];
|
|
}
|