digraph RG {
  T1 [ label="S0(1) R0(1) Richiesta(<Master_00>)
|Master_00|=3 
"];
  T2 [ label="S0(1) R0(1) Richiesta(<Master_01>) Attesa(<Master_00>) Buffer_input(<Master_00>)
|Master_01|=2 |Master_00|=1 
"];
  T1 -> T2 [ label=<T1&gt;>];
  T3 [ label="R0(1) S1_a(&lt;Master_01&gt;) S1_b(&lt;Master_01&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;)
|Master_01|=1 |Master_00|=2 
"];
  T2 -> T3 [ label=<T3&gt;>];
  T4 [ label="S0(1) R_1(&lt;Master_01&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;)
|Master_01|=1 |Master_00|=2 
"];
  T2 -> T4 [ label=<T9&gt;>];
  T5 [ label="S0(1) R0(1) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=2 |Master_01|=1 
"];
  T2 -> T5 [ label=<T1&gt;>];
  T6 [ label="R0(1) S1_b(&lt;Master_01&gt;) S2_a(&lt;Master_01&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;)
|Master_00|=2 |Master_01|=1 
"];
  T3 -> T6 [ label=<T4&gt;>];
  T7 [ label="R0(1) S1_a(&lt;Master_01&gt;) S2_b(&lt;Master_01&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;)
|Master_00|=2 |Master_01|=1 
"];
  T3 -> T7 [ label=<T5&gt;>];
  T8 [ label="R0(1) S1_a(&lt;Master_02&gt;) S1_b(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_02|=1 |Master_00|=1 |Master_01|=1 
"];
  T3 -> T8 [ label=<T1&gt;>];
  T9 [ label="S0(1) R_2(&lt;Master_01&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;)
|Master_00|=2 |Master_01|=1 
"];
  T4 -> T9 [ label=<T8&gt;>];
  T10 [ label="S0(1) R_1(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_02|=1 |Master_00|=1 |Master_01|=1 
"];
  T4 -> T10 [ label=<T1&gt;>];
  T11 [ label="S0(1) R0(1) Attesa(&lt;Master_00&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=3 
"];
  T5 -> T11 [ label=<T1&gt;>];
  T5 -> T10 [ label=<T9&gt;>];
  T5 -> T8 [ label=<T3&gt;>];
  T12 [ label="R0(1) S1_b(&lt;Master_02&gt;) S2_a(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_02|=1 |Master_00|=1 |Master_01|=1 
"];
  T6 -> T12 [ label=<T1&gt;>];
  T13 [ label="R0(1) S2_b(&lt;Master_01&gt;) S2_a(&lt;Master_01&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;)
|Master_00|=2 |Master_01|=1 
"];
  T6 -> T13 [ label=<T5&gt;>];
  T14 [ label="R0(1) S1_a(&lt;Master_02&gt;) S2_b(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_02|=1 |Master_00|=1 |Master_01|=1 
"];
  T7 -> T14 [ label=<T1&gt;>];
  T7 -> T13 [ label=<T4&gt;>];
  T15 [ label="S1_a(&lt;Master_02&gt;) S1_b(&lt;Master_02&gt;) R_1(&lt;Master_01&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;+&lt;Master_02&gt;)
|Master_01|=1 |Master_00|=1 |Master_02|=1 
"];
  T8 -> T15 [ label=<T9&gt;>];
  T16 [ label="R0(1) S1_a(&lt;Master_01&gt;) S1_b(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=2 |Master_01|=1 
"];
  T8 -> T16 [ label=<T1&gt;>];
  T8 -> T14 [ label=<T5&gt;>];
  T8 -> T12 [ label=<T4&gt;>];
  T17 [ label="S0(1) R3(1) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_01|=2 |Master_00|=1 
"];
  T9 -> T17 [ label=<T7&gt;>];
  T18 [ label="S0(1) R_2(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_02|=1 |Master_00|=1 |Master_01|=1 
"];
  T9 -> T18 [ label=<T1&gt;>];
  T10 -> T15 [ label=<T3&gt;>];
  T19 [ label="S0(1) R_1(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=2 |Master_01|=1 
"];
  T10 -> T19 [ label=<T1&gt;>];
  T10 -> T18 [ label=<T8&gt;>];
  T11 -> T16 [ label=<T3&gt;>];
  T11 -> T19 [ label=<T9&gt;>];
  T20 [ label="S1_b(&lt;Master_02&gt;) R_1(&lt;Master_01&gt;) S2_a(&lt;Master_02&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;+&lt;Master_02&gt;)
|Master_01|=1 |Master_00|=1 |Master_02|=1 
"];
  T12 -> T20 [ label=<T9&gt;>];
  T21 [ label="R0(1) S2_b(&lt;Master_02&gt;) S2_a(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T12 -> T21 [ label=<T5&gt;>];
  T22 [ label="R0(1) S1_b(&lt;Master_01&gt;) S2_a(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=2 |Master_01|=1 
"];
  T12 -> T22 [ label=<T1&gt;>];
  T23 [ label="R0(1) S3(1) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_01|=2 |Master_00|=1 
"];
  T13 -> T23 [ label=<T6&gt;>];
  T13 -> T21 [ label=<T1&gt;>];
  T24 [ label="S1_a(&lt;Master_02&gt;) R_1(&lt;Master_01&gt;) S2_b(&lt;Master_02&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;+&lt;Master_02&gt;)
|Master_01|=1 |Master_00|=1 |Master_02|=1 
"];
  T14 -> T24 [ label=<T9&gt;>];
  T14 -> T21 [ label=<T4&gt;>];
  T25 [ label="R0(1) S1_a(&lt;Master_01&gt;) S2_b(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=2 |Master_01|=1 
"];
  T14 -> T25 [ label=<T1&gt;>];
  T26 [ label="S1_a(&lt;Master_02&gt;) S1_b(&lt;Master_02&gt;) R_2(&lt;Master_01&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;+&lt;Master_02&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T15 -> T26 [ label=<T8&gt;>];
  T15 -> T20 [ label=<T4&gt;>];
  T15 -> T24 [ label=<T5&gt;>];
  T27 [ label="S1_a(&lt;Master_02&gt;) S1_b(&lt;Master_02&gt;) R_1(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T15 -> T27 [ label=<T1&gt;>];
  T16 -> T22 [ label=<T4&gt;>];
  T16 -> T25 [ label=<T5&gt;>];
  T16 -> T27 [ label=<T9&gt;>];
  T28 [ label="S0(1) R0(1) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=2 
"];
  T17 -> T28 [ label=<Reset_r>];
  T29 [ label="S0(1) R3(1) Richiesta(&lt;Master_01&gt;) Elabora(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=2 
"];
  T17 -> T29 [ label=<T2&gt;>];
  T30 [ label="S0(1) R3(1) Richiesta(&lt;Master_02&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;) Buffer_input(&lt;Master_01&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_02|=1 |Master_01|=1 
"];
  T17 -> T30 [ label=<T1&gt;>];
  T18 -> T26 [ label=<T3&gt;>];
  T31 [ label="S0(1) R_2(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=2 |Master_01|=1 
"];
  T18 -> T31 [ label=<T1&gt;>];
  T18 -> T30 [ label=<T7&gt;>];
  T19 -> T31 [ label=<T8&gt;>];
  T19 -> T27 [ label=<T3&gt;>];
  T32 [ label="S1_b(&lt;Master_02&gt;) R_2(&lt;Master_01&gt;) S2_a(&lt;Master_02&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;+&lt;Master_02&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T20 -> T32 [ label=<T8&gt;>];
  T33 [ label="S1_b(&lt;Master_02&gt;) R_1(&lt;Master_01&gt;) S2_a(&lt;Master_02&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T20 -> T33 [ label=<T1&gt;>];
  T34 [ label="R_1(&lt;Master_02&gt;) S2_b(&lt;Master_01&gt;) S2_a(&lt;Master_01&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;+&lt;Master_02&gt;)
|Master_00|=1 |Master_02|=1 |Master_01|=1 
"];
  T20 -> T34 [ label=<T5&gt;>];
  T35 [ label="R0(1) S3(1) Richiesta(&lt;Master_02&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;) Buffer_input(&lt;Master_01&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_02|=1 |Master_00|=1 |Master_01|=1 
"];
  T21 -> T35 [ label=<T6&gt;>];
  T36 [ label="R0(1) S2_b(&lt;Master_01&gt;) S2_a(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=2 |Master_01|=1 
"];
  T21 -> T36 [ label=<T1&gt;>];
  T21 -> T34 [ label=<T9&gt;>];
  T22 -> T36 [ label=<T5&gt;>];
  T22 -> T33 [ label=<T9&gt;>];
  T23 -> T28 [ label=<Reset_s>];
  T37 [ label="R0(1) S3(1) Richiesta(&lt;Master_01&gt;) Elabora(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=2 
"];
  T23 -> T37 [ label=<T2&gt;>];
  T23 -> T35 [ label=<T1&gt;>];
  T38 [ label="S1_a(&lt;Master_02&gt;) R_2(&lt;Master_01&gt;) S2_b(&lt;Master_02&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;+&lt;Master_02&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T24 -> T38 [ label=<T8&gt;>];
  T39 [ label="S1_a(&lt;Master_02&gt;) R_1(&lt;Master_01&gt;) S2_b(&lt;Master_02&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T24 -> T39 [ label=<T1&gt;>];
  T24 -> T34 [ label=<T4&gt;>];
  T25 -> T36 [ label=<T4&gt;>];
  T25 -> T39 [ label=<T9&gt;>];
  T40 [ label="S1_a(&lt;Master_02&gt;) S1_b(&lt;Master_02&gt;) R3(1) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_01|=1 |Master_00|=1 |Master_02|=1 
"];
  T26 -> T40 [ label=<T7&gt;>];
  T41 [ label="S1_a(&lt;Master_02&gt;) S1_b(&lt;Master_02&gt;) R_2(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T26 -> T41 [ label=<T1&gt;>];
  T26 -> T38 [ label=<T5&gt;>];
  T26 -> T32 [ label=<T4&gt;>];
  T27 -> T39 [ label=<T5&gt;>];
  T27 -> T33 [ label=<T4&gt;>];
  T27 -> T41 [ label=<T8&gt;>];
  T42 [ label="S0(1) R0(1) Richiesta(&lt;Master_02&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;) Buffer_input(&lt;Master_01&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_02|=1 |Master_01|=1 
"];
  T28 -> T42 [ label=<T1&gt;>];
  T43 [ label="S0(1) R0(1) Richiesta(&lt;Master_01&gt;) Elabora(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=2 
"];
  T28 -> T43 [ label=<T2&gt;>];
  T44 [ label="S0(1) R3(1) Richiesta(&lt;Master_00&gt;)
|Master_00|=3 
"];
  T29 -> T44 [ label=<T0&gt;>];
  T45 [ label="S0(1) R3(1) Richiesta(&lt;Master_02&gt;) Attesa(&lt;Master_01&gt;) Elabora(&lt;Master_00&gt;) Buffer_input(&lt;Master_01&gt;)
|Master_00|=1 |Master_02|=1 |Master_01|=1 
"];
  T29 -> T45 [ label=<T1&gt;>];
  T29 -> T43 [ label=<Reset_r>];
  T30 -> T40 [ label=<T3&gt;>];
  T46 [ label="S0(1) R3(1) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;) Buffer_input(&lt;Master_01&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=2 
"];
  T30 -> T46 [ label=<T1&gt;>];
  T30 -> T45 [ label=<T2&gt;>];
  T30 -> T42 [ label=<Reset_r>];
  T31 -> T46 [ label=<T7&gt;>];
  T31 -> T41 [ label=<T3&gt;>];
  T47 [ label="S1_b(&lt;Master_02&gt;) R3(1) S2_a(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_01|=1 |Master_00|=1 |Master_02|=1 
"];
  T32 -> T47 [ label=<T7&gt;>];
  T48 [ label="R_2(&lt;Master_02&gt;) S2_b(&lt;Master_01&gt;) S2_a(&lt;Master_01&gt;) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;+&lt;Master_02&gt;)
|Master_00|=1 |Master_02|=1 |Master_01|=1 
"];
  T32 -> T48 [ label=<T5&gt;>];
  T49 [ label="S1_b(&lt;Master_02&gt;) R_2(&lt;Master_01&gt;) S2_a(&lt;Master_02&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T32 -> T49 [ label=<T1&gt;>];
  T50 [ label="R_1(&lt;Master_02&gt;) S2_b(&lt;Master_01&gt;) S2_a(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=1 |Master_02|=1 |Master_01|=1 
"];
  T33 -> T50 [ label=<T5&gt;>];
  T33 -> T49 [ label=<T8&gt;>];
  T51 [ label="R_1(&lt;Master_02&gt;) S3(1) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_01|=1 |Master_00|=1 |Master_02|=1 
"];
  T34 -> T51 [ label=<T6&gt;>];
  T34 -> T50 [ label=<T1&gt;>];
  T34 -> T48 [ label=<T8&gt;>];
  T35 -> T42 [ label=<Reset_s>];
  T52 [ label="R0(1) S3(1) Richiesta(&lt;Master_02&gt;) Attesa(&lt;Master_01&gt;) Elabora(&lt;Master_00&gt;) Buffer_input(&lt;Master_01&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T35 -> T52 [ label=<T2&gt;>];
  T35 -> T51 [ label=<T9&gt;>];
  T53 [ label="R0(1) S3(1) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;) Buffer_input(&lt;Master_01&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=2 
"];
  T35 -> T53 [ label=<T1&gt;>];
  T36 -> T50 [ label=<T9&gt;>];
  T36 -> T53 [ label=<T6&gt;>];
  T54 [ label="R0(1) S3(1) Richiesta(&lt;Master_00&gt;)
|Master_00|=3 
"];
  T37 -> T54 [ label=<T0&gt;>];
  T37 -> T52 [ label=<T1&gt;>];
  T37 -> T43 [ label=<Reset_s>];
  T55 [ label="S1_a(&lt;Master_02&gt;) R3(1) S2_b(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_01|=1 |Master_00|=1 |Master_02|=1 
"];
  T38 -> T55 [ label=<T7&gt;>];
  T38 -> T48 [ label=<T4&gt;>];
  T56 [ label="S1_a(&lt;Master_02&gt;) R_2(&lt;Master_01&gt;) S2_b(&lt;Master_02&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T38 -> T56 [ label=<T1&gt;>];
  T39 -> T50 [ label=<T4&gt;>];
  T39 -> T56 [ label=<T8&gt;>];
  T57 [ label="R0(1) S1_a(&lt;Master_02&gt;) S1_b(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T40 -> T57 [ label=<Reset_r>];
  T58 [ label="S1_a(&lt;Master_02&gt;) S1_b(&lt;Master_02&gt;) R3(1) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_02&gt;) Elabora(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T40 -> T58 [ label=<T2&gt;>];
  T40 -> T47 [ label=<T4&gt;>];
  T40 -> T55 [ label=<T5&gt;>];
  T59 [ label="S1_a(&lt;Master_02&gt;) S1_b(&lt;Master_02&gt;) R3(1) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_01&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T40 -> T59 [ label=<T1&gt;>];
  T41 -> T49 [ label=<T4&gt;>];
  T41 -> T56 [ label=<T5&gt;>];
  T41 -> T59 [ label=<T7&gt;>];
  T42 -> T57 [ label=<T3&gt;>];
  T60 [ label="S0(1) R_1(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_02|=1 |Master_01|=1 
"];
  T42 -> T60 [ label=<T9&gt;>];
  T61 [ label="S0(1) R0(1) Richiesta(&lt;Master_02&gt;) Attesa(&lt;Master_01&gt;) Elabora(&lt;Master_00&gt;) Buffer_input(&lt;Master_01&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T42 -> T61 [ label=<T2&gt;>];
  T62 [ label="S0(1) R0(1) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;) Buffer_input(&lt;Master_01&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=2 
"];
  T42 -> T62 [ label=<T1&gt;>];
  T43 -> T1 [ label=<T0&gt;>];
  T43 -> T61 [ label=<T1&gt;>];
  T44 -> T1 [ label=<Reset_r>];
  T63 [ label="S0(1) R3(1) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_01|=2 |Master_00|=1 
"];
  T44 -> T63 [ label=<T1&gt;>];
  T45 -> T58 [ label=<T3&gt;>];
  T45 -> T61 [ label=<Reset_r>];
  T64 [ label="S0(1) R3(1) Attesa(&lt;Master_01&gt;) Elabora(&lt;Master_00&gt;) Buffer_input(&lt;Master_01&gt;)
|Master_00|=1 |Master_01|=2 
"];
  T45 -> T64 [ label=<T1&gt;>];
  T45 -> T63 [ label=<T0&gt;>];
  T46 -> T62 [ label=<Reset_r>];
  T46 -> T64 [ label=<T2&gt;>];
  T46 -> T59 [ label=<T3&gt;>];
  T65 [ label="R0(1) S1_b(&lt;Master_02&gt;) S2_a(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T47 -> T65 [ label=<Reset_r>];
  T66 [ label="S1_b(&lt;Master_02&gt;) R3(1) S2_a(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_02&gt;) Elabora(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T47 -> T66 [ label=<T2&gt;>];
  T67 [ label="S1_b(&lt;Master_02&gt;) R3(1) S2_a(&lt;Master_02&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_01&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T47 -> T67 [ label=<T1&gt;>];
  T68 [ label="R3(1) S2_b(&lt;Master_02&gt;) S2_a(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T47 -> T68 [ label=<T5&gt;>];
  T69 [ label="R_2(&lt;Master_02&gt;) S3(1) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_01|=1 |Master_00|=1 |Master_02|=1 
"];
  T48 -> T69 [ label=<T6&gt;>];
  T70 [ label="R_2(&lt;Master_02&gt;) S2_b(&lt;Master_01&gt;) S2_a(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T48 -> T70 [ label=<T1&gt;>];
  T48 -> T68 [ label=<T7&gt;>];
  T49 -> T70 [ label=<T5&gt;>];
  T49 -> T67 [ label=<T7&gt;>];
  T71 [ label="R_1(&lt;Master_02&gt;) S3(1) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_01&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_01|=1 |Master_00|=1 |Master_02|=1 
"];
  T50 -> T71 [ label=<T6&gt;>];
  T50 -> T70 [ label=<T8&gt;>];
  T51 -> T60 [ label=<Reset_s>];
  T72 [ label="R_1(&lt;Master_02&gt;) S3(1) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_02&gt;) Elabora(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T51 -> T72 [ label=<T2&gt;>];
  T51 -> T69 [ label=<T8&gt;>];
  T51 -> T71 [ label=<T1&gt;>];
  T73 [ label="R0(1) S3(1) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;) Buffer_input(&lt;Master_00&gt;)
|Master_01|=2 |Master_00|=1 
"];
  T52 -> T73 [ label=<T0&gt;>];
  T74 [ label="R0(1) S3(1) Attesa(&lt;Master_01&gt;) Elabora(&lt;Master_00&gt;) Buffer_input(&lt;Master_01&gt;)
|Master_00|=1 |Master_01|=2 
"];
  T52 -> T74 [ label=<T1&gt;>];
  T52 -> T72 [ label=<T9&gt;>];
  T52 -> T61 [ label=<Reset_s>];
  T53 -> T71 [ label=<T9&gt;>];
  T53 -> T74 [ label=<T2&gt;>];
  T53 -> T62 [ label=<Reset_s>];
  T54 -> T1 [ label=<Reset_s>];
  T54 -> T73 [ label=<T1&gt;>];
  T75 [ label="R0(1) S1_a(&lt;Master_02&gt;) S2_b(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_02&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T55 -> T75 [ label=<Reset_r>];
  T76 [ label="S1_a(&lt;Master_02&gt;) R3(1) S2_b(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_02&gt;) Elabora(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T55 -> T76 [ label=<T2&gt;>];
  T77 [ label="S1_a(&lt;Master_02&gt;) R3(1) S2_b(&lt;Master_02&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_01&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T55 -> T77 [ label=<T1&gt;>];
  T55 -> T68 [ label=<T4&gt;>];
  T56 -> T70 [ label=<T4&gt;>];
  T56 -> T77 [ label=<T7&gt;>];
  T78 [ label="R0(1) S1_a(&lt;Master_02&gt;) S1_b(&lt;Master_02&gt;) Attesa(&lt;Master_00&gt;+&lt;Master_01&gt;+&lt;Master_02&gt;) Buffer_input(&lt;Master_01&gt;) Buffer_output(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T57 -> T78 [ label=<T1&gt;>];
  T57 -> T75 [ label=<T5&gt;>];
  T57 -> T65 [ label=<T4&gt;>];
  T79 [ label="R0(1) S1_a(&lt;Master_02&gt;) S1_b(&lt;Master_02&gt;) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_02&gt;) Elabora(&lt;Master_00&gt;)
|Master_00|=1 |Master_01|=1 |Master_02|=1 
"];
  T57 -> T79 [ label=<T2&gt;>];
  T80 [ label="S1_a(&lt;Master_01&gt;) S1_b(&lt;Master_01&gt;) R3(1) Richiesta(&lt;Master_00&gt;) Attesa(&lt;Master_01&gt;)
|Master_01|=1 |Master_00|=2 
"];
  T58 -> T80 [ label=<T0&gt;>];
  T81 [shape=none label="..."];
  T58 -> T81 [ label=<T1&gt;>];
  T58 -> T76 [ label=<T5&gt;>];
  T58 -> T66 [ label=<T4&gt;>];
  T58 -> T79 [ label=<Reset_r>];
  T59 -> T77 [ label=<T5&gt;>];
  T59 -> T67 [ label=<T4&gt;>];
  T81 [shape=none label="..."];
  T59 -> T81 [ label=<T2&gt;>];
  T59 -> T78 [ label=<Reset_r>];
  T82 [shape=none label="..."];
  T60 -> T82 [ label=<T8&gt;>];
  T83 [shape=none label="..."];
  T60 -> T83 [ label=<T1&gt;>];
  T84 [shape=none label="..."];
  T60 -> T84 [ label=<T2&gt;>];
  T61 -> T2 [ label=<T0&gt;>];
  T85 [shape=none label="..."];
  T61 -> T85 [ label=<T1&gt;>];
  T84 [shape=none label="..."];
  T61 -> T84 [ label=<T9&gt;>];
  T61 -> T79 [ label=<T3&gt;>];
  T85 [shape=none label="..."];
  T62 -> T85 [ label=<T2&gt;>];
  T83 [shape=none label="..."];
  T62 -> T83 [ label=<T9&gt;>];
  T62 -> T78 [ label=<T3&gt;>];
  T63 -> T80 [ label=<T3&gt;>];
  T86 [shape=none label="..."];
  T63 -> T86 [ label=<T1&gt;>];
  T63 -> T2 [ label=<Reset_r>];
  T86 [shape=none label="..."];
  T64 -> T86 [ label=<T0&gt;>];
  T85 [shape=none label="..."];
  T64 -> T85 [ label=<Reset_r>];
  T81 [shape=none label="..."];
  T64 -> T81 [ label=<T3&gt;>];
  T87 [shape=none label="..."];
  T65 -> T87 [ label=<T5&gt;>];
  T88 [shape=none label="..."];
  T65 -> T88 [ label=<T1&gt;>];
  T89 [shape=none label="..."];
  T65 -> T89 [ label=<T2&gt;>];
  T90 [shape=none label="..."];
  T66 -> T90 [ label=<T0&gt;>];
  T91 [shape=none label="..."];
  T66 -> T91 [ label=<T5&gt;>];
  T92 [shape=none label="..."];
  T66 -> T92 [ label=<T1&gt;>];
  T89 [shape=none label="..."];
  T66 -> T89 [ label=<Reset_r>];
  T93 [shape=none label="..."];
  T67 -> T93 [ label=<T5&gt;>];
  T92 [shape=none label="..."];
  T67 -> T92 [ label=<T2&gt;>];
  T88 [shape=none label="..."];
  T67 -> T88 [ label=<Reset_r>];
  T94 [shape=none label="..."];
  T68 -> T94 [ label=<T6&gt;>];
  T93 [shape=none label="..."];
  T68 -> T93 [ label=<T1&gt;>];
  T91 [shape=none label="..."];
  T68 -> T91 [ label=<T2&gt;>];
  T87 [shape=none label="..."];
  T68 -> T87 [ label=<Reset_r>];
  T82 [shape=none label="..."];
  T69 -> T82 [ label=<Reset_s>];
  T95 [shape=none label="..."];
  T69 -> T95 [ label=<T2&gt;>];
  T94 [shape=none label="..."];
  T69 -> T94 [ label=<T7&gt;>];
  T96 [shape=none label="..."];
  T69 -> T96 [ label=<T1&gt;>];
  T93 [shape=none label="..."];
  T70 -> T93 [ label=<T7&gt;>];
  T96 [shape=none label="..."];
  T70 -> T96 [ label=<T6&gt;>];
  T83 [shape=none label="..."];
  T71 -> T83 [ label=<Reset_s>];
  T97 [shape=none label="..."];
  T71 -> T97 [ label=<T2&gt;>];
  T96 [shape=none label="..."];
  T71 -> T96 [ label=<T8&gt;>];
  T98 [shape=none label="..."];
  T72 -> T98 [ label=<T0&gt;>];
  T97 [shape=none label="..."];
  T72 -> T97 [ label=<T1&gt;>];
  T95 [shape=none label="..."];
  T72 -> T95 [ label=<T8&gt;>];
  T84 [shape=none label="..."];
  T72 -> T84 [ label=<Reset_s>];
  T73 -> T2 [ label=<Reset_s>];
  T98 [shape=none label="..."];
  T73 -> T98 [ label=<T9&gt;>];
  T99 [shape=none label="..."];
  T73 -> T99 [ label=<T1&gt;>];
  T85 [shape=none label="..."];
  T74 -> T85 [ label=<Reset_s>];
  T97 [shape=none label="..."];
  T74 -> T97 [ label=<T9&gt;>];
  T99 [shape=none label="..."];
  T74 -> T99 [ label=<T0&gt;>];
  T87 [shape=none label="..."];
  T75 -> T87 [ label=<T4&gt;>];
  T100 [shape=none label="..."];
  T75 -> T100 [ label=<T1&gt;>];
  T101 [shape=none label="..."];
  T75 -> T101 [ label=<T2&gt;>];
  T102 [shape=none label="..."];
  T76 -> T102 [ label=<T0&gt;>];
  T91 [shape=none label="..."];
  T76 -> T91 [ label=<T4&gt;>];
  T103 [shape=none label="..."];
  T76 -> T103 [ label=<T1&gt;>];
  T101 [shape=none label="..."];
  T76 -> T101 [ label=<Reset_r>];
  T93 [shape=none label="..."];
  T77 -> T93 [ label=<T4&gt;>];
  T103 [shape=none label="..."];
  T77 -> T103 [ label=<T2&gt;>];
  T100 [shape=none label="..."];
  T77 -> T100 [ label=<Reset_r>];
  T104 [shape=none label="..."];
  T78 -> T104 [ label=<T9&gt;>];
  T105 [shape=none label="..."];
  T78 -> T105 [ label=<T2&gt;>];
  T88 [shape=none label="..."];
  T78 -> T88 [ label=<T4&gt;>];
  T100 [shape=none label="..."];
  T78 -> T100 [ label=<T5&gt;>];
  T79 -> T3 [ label=<T0&gt;>];
  T89 [shape=none label="..."];
  T79 -> T89 [ label=<T4&gt;>];
  T101 [shape=none label="..."];
  T79 -> T101 [ label=<T5&gt;>];
  T105 [shape=none label="..."];
  T79 -> T105 [ label=<T1&gt;>];
  T80 -> T3 [ label=<Reset_r>];
  T90 [shape=none label="..."];
  T80 -> T90 [ label=<T4&gt;>];
  T102 [shape=none label="..."];
  T80 -> T102 [ label=<T5&gt;>];
  T106 [shape=none label="..."];
  T80 -> T106 [ label=<T1&gt;>];
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">Symbolic Reachability Graph</font></td></tr><tr><td align="left" colspan="2"><font color="#7602B9" face="Sans Bold"><b>OPEN GRAPH:</b></font> Showing a subset of markings.</td></tr><tr><td align="left">Total markings:</td><td>80 out of 232</td></tr></table>> ];
}