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>> ];
}