diff --git a/anno3/vpc/consegne/2.b/2.b.org b/anno3/vpc/consegne/2.b/2.b.org new file mode 100644 index 0000000..350e47f --- /dev/null +++ b/anno3/vpc/consegne/2.b/2.b.org @@ -0,0 +1,144 @@ +* Rete E + +[[./reteE.jpg]] + +I master sono modellati dai posti Richiesta, Attesa e Elabora. Lo slave +di tipo 1 e` modellato dai posti S0, S1_a, S2_a, S1_a, S1_b e S3. Lo +slave di tipo 2 e` modellato dai posti R0, R1, R2 e R3. +La richiesta agli slave e` modellata attraverso due posti: Buffer_Input, Buffer_output. + +La classe di colori utilizzata e` Master, che permette di distinguere +i tre master /m1, m2, m3/, mentre il color domain e` /m/ e viene +utilizzato in tutte le transizioni dove c'e` necessita` di distinguere +l'origine del marking. + + +** Reachability Graph + +Le seguenti tabelle elencano la dimensione dello spazio degli stati al variare +del numero di master (N) e di slave (Sn e Rn). +| N | Sn, Rn | Marking RG | Marking SRG | +|---+--------+------------+-------------| +| 1 | 1 | 1024 | 232 | +| 1 | 2 | 4080 | 888 | +| 1 | 3 | 9280 | 2032 | +| 1 | 4 | 16480 | 3616 | +|---+--------+------------+-------------| +| 2 | 1 | 28480 | 5240 | +| 2 | 2 | 201708 | 35874 | +| 2 | 3 | 678240 | 119488 | +|---+--------+------------+-------------| +| 3 | 1 | 310400 | 54080 | +| 3 | 2 | 3151680 | 538380 | + +L'utilizzo del Symbolic Reachability Graph permette di ridurre il +numero di marking di un fattore >4 . + +** Reachability Graph al variare delle classi di colore + +| k | Marking RG | Marking SRG | +|----+------------+-------------| +| 3 | 1024 | 232 | +| 4 | 5632 | 460 | +| 5 | 29696 | 804 | +| 6 | 151552 | 1288 | +| 7 | 753664 | 1936 | +| 8 | 3670016 | 2772 | +| 9 | 17563648 | 3820 | +| 10 | 82837504 | 5104 | +La tabella mostra l'aumentare dei marking del Reachability Graph +all'aumentare delle classi di colore. +Benche` la crescita dello spazio degli stati sia lineare in entrambi i +casi, notiamo come lo spazio del SRG sia notevolmente piu` contenuto +dello spazio del RG. +Inoltre, il rapporto marking RG/SRG (dello stato degli spazi) aumenta +proporzionalmente al valore di k. + +A conferma di quanto espresso, notiamo che anche con valori di +marcatura iniziale maggiore per il master e gli slave, notiamo lo +stesso effetto sul rapporto di marking RG/SRG (limitatamente alle +possibilita` di calcolo). +| N, Sn, Rn | k | Marking RG | Marking SRG | +|-----------+---+------------+-------------| +| 2, 2, 2 | 3 | 201708 | 35874 | +| 2, 2, 2 | 4 | 4190624 | 203136 | +| 2, 2, 2 | 5 | 78523200 | 875478 | + +** Considerazioni su Fork/Join +Non puo` avvenire un join fra due processi con diverso padre quando: +- N = 1: sullo stesso spazio non puo` essere presente piu` di un token con lo + stesso colore +- Sn = 1: in questo secondo caso, come nei precedenti esercizi, + avviene un solo fork alla volta. + +Di seguito viene mostrata un'esecuzione in cui e` possibile che +avvenga il join di due processi con lo diverso padre: +- con N > 1 consideriamo che nella rete vi siano al momento iniziale due + token dello stesso colore "m0" +- entrambi i token vengono inseriti nel Buffer_input e in seguito + inviati allo slave di tipo 1. +- quando Sn > 1 uno dei due token puo` eseguire lo scatto attraverso + la transizione T3 prima che l'altro token arrivi alla transizione T6 + (in cui avviene il join). + +* Rete F + +[[./reteF.jpg]] + +I master sono modellati dai posti Richiesta, Attesa e Elabora. Gli slave +di tipo 1 sono modellato dai posti S0, S1_a, S2_a, S1_a, S1_b e S3. +La richiesta agli slave e` modellata attraverso due posti: Buffer_Input, Buffer_output. + +Nella rete sono presenti due classi di colore: +- Master, che permette di distinguere i diversi master /m1, m2, m3/ +- Slave, che permette di distinguere i due slaves /ID1/ e /ID2/ +La classe Slave e` divisa in due sottoclassi, Slave1 e Slave2, +per facilitare in seguito la parametrizzazione degli slaves. +Anche la classe Master e` divisa in due sottoclassi utilizzate +nell'espressione booleane della transizione Fork. +Il /dominio D/ = /Master×Slave/ e` utilizzato per la multiplicity +degli archi fra fork e join, in modo da tener traccia delle richieste effettuate. + + +** TODO Reachability Graph +Le seguenti tabelle elencano la dimensione dello spazio degli stati al variare +del numero di master (N) e di slave (Sn e Rn). +| N | R1, R2 | Marking RG | Marking SRG | +|---+--------+------------+-------------| +| 1 | 1 | 768 | 432 | +| 1 | 2 | 2560 | 1440 | +| 1 | 3 | 5376 | 3024 | +| 1 | 4 | 5184 | 9216 | +|---+--------+------------+-------------| +| 2 | 1 | 18720 | 9720 | +| 2 | 2 | 97696 | 50481 | +| 2 | 3 | 267120 | 137376 | +|---+--------+------------+-------------| +| 3 | 1 | 192000 | 97600 | +| 3 | 2 | 1309440 | 663520 | +Rispetto alla precedente rete, il rapporto stato degli spazi di RG/SRG +e` minore. + +** TODO Reachability Graph al variare delle classi di colore +| \vert{}M1\vert{} | \vert{}M2\vert{} | Marking RG | Marking SRG | +|------------------+------------------+------------+-------------| +| 2 | 1 | 768 | 432 | +| 3 | 1 | 3840 | 960 | +| 2 | 2 | 4096 | 1296 | +| 3 | 2 | 20480 | 2880 | +| 3 | 3 | 102400 | 6400 | +| 4 | 3 | 491520 | 12000 | +| 4 | 4 | 2359296 | 22500 | +| 5 | 4 | 11010048 | 37800 | +| 5 | 5 | 51380224 | 63504 | + + [ ] Cambia diversamente all'aumento di slaves vs masters? +| \vert{}Slave1\vert{} | \vert{}Slave2\vert{} | Marking RG | Marking SRG | +|----------------------+----------------------+------------+-------------| + + +** Considerazioni su Fork/Join +Posso fare le stesse considerazioni che nella rete precedente (rete +E), tenendo in considerazione che avendo due diverse tipologie di +slave, un join fra due processi con padre diverso avverra` solo quando +| (R₁ > 1 ∨ R₂ > 1) ∧ N > 1 diff --git a/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN-RG-0.pdf b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN-RG-0.pdf new file mode 100644 index 0000000..2b071e1 Binary files /dev/null and b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN-RG-0.pdf differ diff --git a/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.cc b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.cc new file mode 100644 index 0000000..9957bb0 --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.cc @@ -0,0 +1,12 @@ +2 2 3 +1 4 +1 4 +2 8 11 +1 6 +1 7 +2 9 11 +1 1 +1 5 +3 1 5 11 +1 12 +1 10 diff --git a/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.def b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.def new file mode 100644 index 0000000..dbb491a --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.def @@ -0,0 +1,12 @@ +|256 +% +| +(Master c 5.885416666666667 1.3333333333333333 (@c +u Master_0 +)) +(Master_0 c 6.552083333333333 1.3333333333333333 (@c +m{1-n} +)) +(m_0 m 10.0 2.0 (@m +N S +)) diff --git a/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.dot b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.dot new file mode 100644 index 0000000..397d552 --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.dot @@ -0,0 +1,564 @@ +digraph RG { + T1 [ label="S0(1) R0(1) Richiesta(<m1>+<m2>+<m3>) +"]; + T2 [ label="S0(1) R0(1) Richiesta(<m2>+<m3>) Attesa(<m1>) Buffer_input(<m1>) +"]; + T1 -> T2 [ label=]; + T3 [ label="S0(1) R0(1) Richiesta(<m1>+<m3>) Attesa(<m2>) Buffer_input(<m2>) +"]; + T1 -> T3 [ label=]; + T4 [ label="S0(1) R0(1) Richiesta(<m1>+<m2>) Attesa(<m3>) Buffer_input(<m3>) +"]; + T1 -> T4 [ label=]; + T5 [ label="R0(1) S1_a(<m1>) S1_b(<m1>) Richiesta(<m2>+<m3>) Attesa(<m1>) +"]; + T2 -> T5 [ label=]; + T6 [ label="S0(1) R_1(<m1>) Richiesta(<m2>+<m3>) Attesa(<m1>) +"]; + T2 -> T6 [ label=]; + T7 [ label="S0(1) R0(1) Richiesta(<m3>) Attesa(<m1>+<m2>) Buffer_input(<m1>+<m2>) +"]; + T2 -> T7 [ label=]; + T8 [ label="S0(1) R0(1) Richiesta(<m2>) Attesa(<m1>+<m3>) Buffer_input(<m1>+<m3>) +"]; + T2 -> T8 [ label=]; + T9 [ label="R0(1) S1_a(<m2>) S1_b(<m2>) Richiesta(<m1>+<m3>) Attesa(<m2>) +"]; + T3 -> T9 [ label=]; + T10 [ label="S0(1) R_1(<m2>) Richiesta(<m1>+<m3>) Attesa(<m2>) +"]; + T3 -> T10 [ label=]; + T3 -> T7 [ label=]; + T11 [ label="S0(1) R0(1) Richiesta(<m1>) Attesa(<m2>+<m3>) Buffer_input(<m2>+<m3>) +"]; + T3 -> T11 [ label=]; + T12 [ label="R0(1) S1_a(<m3>) S1_b(<m3>) Richiesta(<m1>+<m2>) Attesa(<m3>) +"]; + T4 -> T12 [ label=]; + T13 [ label="S0(1) R_1(<m3>) Richiesta(<m1>+<m2>) Attesa(<m3>) +"]; + T4 -> T13 [ label=]; + T4 -> T8 [ label=]; + T4 -> T11 [ label=]; + T14 [ label="R0(1) S1_b(<m1>) S2_a(<m1>) Richiesta(<m2>+<m3>) Attesa(<m1>) +"]; + T5 -> T14 [ label=]; + T15 [ label="R0(1) S1_a(<m1>) S2_b(<m1>) Richiesta(<m2>+<m3>) Attesa(<m1>) +"]; + T5 -> T15 [ label=]; + T16 [ label="R0(1) S1_a(<m1>) S1_b(<m1>) Richiesta(<m2>) Attesa(<m1>+<m3>) Buffer_input(<m3>) +"]; + T5 -> T16 [ label=]; + T17 [ label="R0(1) S1_a(<m1>) S1_b(<m1>) Richiesta(<m3>) Attesa(<m1>+<m2>) Buffer_input(<m2>) +"]; + T5 -> T17 [ label=]; + T18 [ label="S0(1) R_2(<m1>) Richiesta(<m2>+<m3>) Attesa(<m1>) +"]; + T6 -> T18 [ label=]; + T19 [ label="S0(1) R_1(<m1>) Richiesta(<m2>) Attesa(<m1>+<m3>) Buffer_input(<m3>) +"]; + T6 -> T19 [ label=]; + T20 [ label="S0(1) R_1(<m1>) Richiesta(<m3>) Attesa(<m1>+<m2>) Buffer_input(<m2>) +"]; + T6 -> T20 [ label=]; + T21 [ label="S0(1) R0(1) Attesa(<m1>+<m2>+<m3>) Buffer_input(<m1>+<m2>+<m3>) +"]; + T7 -> T21 [ label=]; + T7 -> T20 [ label=]; + T22 [ label="S0(1) R_1(<m2>) Richiesta(<m3>) Attesa(<m1>+<m2>) Buffer_input(<m1>) +"]; + T7 -> T22 [ label=]; + T7 -> T17 [ label=]; + T23 [ label="R0(1) S1_a(<m2>) S1_b(<m2>) Richiesta(<m3>) Attesa(<m1>+<m2>) Buffer_input(<m1>) +"]; + T7 -> T23 [ label=]; + T8 -> T21 [ label=]; + T8 -> T19 [ label=]; + T24 [ label="S0(1) R_1(<m3>) Richiesta(<m2>) Attesa(<m1>+<m3>) Buffer_input(<m1>) +"]; + T8 -> T24 [ label=]; + T8 -> T16 [ label=]; + T25 [ label="R0(1) S1_a(<m3>) S1_b(<m3>) Richiesta(<m2>) Attesa(<m1>+<m3>) Buffer_input(<m1>) +"]; + T8 -> T25 [ label=]; + T26 [ label="R0(1) S1_b(<m2>) S2_a(<m2>) Richiesta(<m1>+<m3>) Attesa(<m2>) +"]; + T9 -> T26 [ label=]; + T27 [ label="R0(1) S1_a(<m2>) S2_b(<m2>) Richiesta(<m1>+<m3>) Attesa(<m2>) +"]; + T9 -> T27 [ label=]; + T28 [ label="R0(1) S1_a(<m2>) S1_b(<m2>) Richiesta(<m1>) Attesa(<m2>+<m3>) Buffer_input(<m3>) +"]; + T9 -> T28 [ label=]; + T9 -> T23 [ label=]; + T29 [ label="S0(1) R_2(<m2>) Richiesta(<m1>+<m3>) Attesa(<m2>) +"]; + T10 -> T29 [ label=]; + T30 [ label="S0(1) R_1(<m2>) Richiesta(<m1>) Attesa(<m2>+<m3>) Buffer_input(<m3>) +"]; + T10 -> T30 [ label=]; + T10 -> T22 [ label=]; + T11 -> T21 [ label=]; + T11 -> T30 [ label=]; + T31 [ label="S0(1) R_1(<m3>) Richiesta(<m1>) Attesa(<m2>+<m3>) Buffer_input(<m2>) +"]; + T11 -> T31 [ label=]; + T11 -> T28 [ label=]; + T32 [ label="R0(1) S1_a(<m3>) S1_b(<m3>) Richiesta(<m1>) Attesa(<m2>+<m3>) Buffer_input(<m2>) +"]; + T11 -> T32 [ label=]; + T33 [ label="R0(1) S1_b(<m3>) S2_a(<m3>) Richiesta(<m1>+<m2>) Attesa(<m3>) +"]; + T12 -> T33 [ label=]; + T34 [ label="R0(1) S1_a(<m3>) S2_b(<m3>) Richiesta(<m1>+<m2>) Attesa(<m3>) +"]; + T12 -> T34 [ label=]; + T12 -> T32 [ label=]; + T12 -> T25 [ label=]; + T35 [ label="S0(1) R_2(<m3>) Richiesta(<m1>+<m2>) Attesa(<m3>) +"]; + T13 -> T35 [ label=]; + T13 -> T31 [ label=]; + T13 -> T24 [ label=]; + T36 [ label="R0(1) S1_b(<m1>) S2_a(<m1>) Richiesta(<m3>) Attesa(<m1>+<m2>) Buffer_input(<m2>) +"]; + T14 -> T36 [ label=]; + T37 [ label="R0(1) S1_b(<m1>) S2_a(<m1>) Richiesta(<m2>) Attesa(<m1>+<m3>) Buffer_input(<m3>) +"]; + T14 -> T37 [ label=]; + T38 [ label="R0(1) S2_b(<m1>) S2_a(<m1>) Richiesta(<m2>+<m3>) Attesa(<m1>) +"]; + T14 -> T38 [ label=]; + T39 [ label="R0(1) S1_a(<m1>) S2_b(<m1>) Richiesta(<m3>) Attesa(<m1>+<m2>) Buffer_input(<m2>) +"]; + T15 -> T39 [ label=]; + T40 [ label="R0(1) S1_a(<m1>) S2_b(<m1>) Richiesta(<m2>) Attesa(<m1>+<m3>) Buffer_input(<m3>) +"]; + T15 -> T40 [ label=]; + T15 -> T38 [ label=]; + T41 [ label="S1_a(<m1>) S1_b(<m1>) R_1(<m3>) Richiesta(<m2>) Attesa(<m1>+<m3>) +"]; + T16 -> T41 [ label=]; + T42 [ label="R0(1) S1_a(<m1>) S1_b(<m1>) Attesa(<m1>+<m2>+<m3>) Buffer_input(<m2>+<m3>) +"]; + T16 -> T42 [ label=]; + T16 -> T40 [ label=]; + T16 -> T37 [ label=]; + T43 [ label="S1_a(<m1>) S1_b(<m1>) R_1(<m2>) Richiesta(<m3>) Attesa(<m1>+<m2>) +"]; + T17 -> T43 [ label=]; + T17 -> T42 [ label=]; + T17 -> T39 [ label=]; + T17 -> T36 [ label=]; + T44 [ label="S0(1) R3(1) Richiesta(<m2>+<m3>) Attesa(<m1>) Buffer_output(<m1>) +"]; + T18 -> T44 [ label=]; + T45 [ label="S0(1) R_2(<m1>) Richiesta(<m3>) Attesa(<m1>+<m2>) Buffer_input(<m2>) +"]; + T18 -> T45 [ label=]; + T46 [ label="S0(1) R_2(<m1>) Richiesta(<m2>) Attesa(<m1>+<m3>) Buffer_input(<m3>) +"]; + T18 -> T46 [ label=]; + T47 [ label="S1_a(<m3>) S1_b(<m3>) R_1(<m1>) Richiesta(<m2>) Attesa(<m1>+<m3>) +"]; + T19 -> T47 [ label=]; + T48 [ label="S0(1) R_1(<m1>) Attesa(<m1>+<m2>+<m3>) Buffer_input(<m2>+<m3>) +"]; + T19 -> T48 [ label=]; + T19 -> T46 [ label=]; + T49 [ label="S1_a(<m2>) S1_b(<m2>) R_1(<m1>) Richiesta(<m3>) Attesa(<m1>+<m2>) +"]; + T20 -> T49 [ label=]; + T20 -> T48 [ label=]; + T20 -> T45 [ label=]; + T21 -> T42 [ label=]; + T50 [ label="R0(1) S1_a(<m2>) S1_b(<m2>) Attesa(<m1>+<m2>+<m3>) Buffer_input(<m1>+<m3>) +"]; + T21 -> T50 [ label=]; + T51 [ label="R0(1) S1_a(<m3>) S1_b(<m3>) Attesa(<m1>+<m2>+<m3>) Buffer_input(<m1>+<m2>) +"]; + T21 -> T51 [ label=]; + T21 -> T48 [ label=]; + T52 [ label="S0(1) R_1(<m2>) Attesa(<m1>+<m2>+<m3>) Buffer_input(<m1>+<m3>) +"]; + T21 -> T52 [ label=]; + T53 [ label="S0(1) R_1(<m3>) Attesa(<m1>+<m2>+<m3>) Buffer_input(<m1>+<m2>) +"]; + T21 -> T53 [ label=]; + T54 [ label="S0(1) R_2(<m2>) Richiesta(<m3>) Attesa(<m1>+<m2>) Buffer_input(<m1>) +"]; + T22 -> T54 [ label=]; + T22 -> T43 [ label=]; + T22 -> T52 [ label=]; + T55 [ label="R0(1) S1_b(<m2>) S2_a(<m2>) Richiesta(<m3>) Attesa(<m1>+<m2>) Buffer_input(<m1>) +"]; + T23 -> T55 [ label=]; + T56 [ label="R0(1) S1_a(<m2>) S2_b(<m2>) Richiesta(<m3>) Attesa(<m1>+<m2>) Buffer_input(<m1>) +"]; + T23 -> T56 [ label=]; + T23 -> T49 [ label=]; + T23 -> T50 [ label=]; + T57 [ label="S0(1) R_2(<m3>) Richiesta(<m2>) Attesa(<m1>+<m3>) Buffer_input(<m1>) +"]; + T24 -> T57 [ label=]; + T24 -> T41 [ label=]; + T24 -> T53 [ label=]; + T58 [ label="R0(1) S1_b(<m3>) S2_a(<m3>) Richiesta(<m2>) Attesa(<m1>+<m3>) Buffer_input(<m1>) +"]; + T25 -> T58 [ label=]; + T59 [ label="R0(1) S1_a(<m3>) S2_b(<m3>) Richiesta(<m2>) Attesa(<m1>+<m3>) Buffer_input(<m1>) +"]; + T25 -> T59 [ label=]; + T25 -> T47 [ label=]; + T25 -> T51 [ label=]; + T26 -> T55 [ label=]; + T60 [ label="R0(1) S1_b(<m2>) S2_a(<m2>) Richiesta(<m1>) Attesa(<m2>+<m3>) Buffer_input(<m3>) +"]; + T26 -> T60 [ label=]; + T61 [ label="R0(1) S2_b(<m2>) S2_a(<m2>) Richiesta(<m1>+<m3>) Attesa(<m2>) +"]; + T26 -> T61 [ label=]; + T27 -> T56 [ label=]; + T62 [ label="R0(1) S1_a(<m2>) S2_b(<m2>) Richiesta(<m1>) Attesa(<m2>+<m3>) Buffer_input(<m3>) +"]; + T27 -> T62 [ label=]; + T27 -> T61 [ label=]; + T63 [ label="S1_a(<m2>) S1_b(<m2>) R_1(<m3>) Richiesta(<m1>) Attesa(<m2>+<m3>) +"]; + T28 -> T63 [ label=]; + T28 -> T50 [ label=]; + T28 -> T62 [ label=]; + T28 -> T60 [ label=]; + T64 [ label="S0(1) R3(1) Richiesta(<m1>+<m3>) Attesa(<m2>) Buffer_output(<m2>) +"]; + T29 -> T64 [ label=]; + T29 -> T54 [ label=]; + T65 [ label="S0(1) R_2(<m2>) Richiesta(<m1>) Attesa(<m2>+<m3>) Buffer_input(<m3>) +"]; + T29 -> T65 [ label=]; + T66 [ label="S1_a(<m3>) S1_b(<m3>) R_1(<m2>) Richiesta(<m1>) Attesa(<m2>+<m3>) +"]; + T30 -> T66 [ label=]; + T30 -> T52 [ label=]; + T30 -> T65 [ label=]; + T67 [ label="S0(1) R_2(<m3>) Richiesta(<m1>) Attesa(<m2>+<m3>) Buffer_input(<m2>) +"]; + T31 -> T67 [ label=]; + T31 -> T63 [ label=]; + T31 -> T53 [ label=]; + T68 [ label="R0(1) S1_b(<m3>) S2_a(<m3>) Richiesta(<m1>) Attesa(<m2>+<m3>) Buffer_input(<m2>) +"]; + T32 -> T68 [ label=]; + T69 [ label="R0(1) S1_a(<m3>) S2_b(<m3>) Richiesta(<m1>) Attesa(<m2>+<m3>) Buffer_input(<m2>) +"]; + T32 -> T69 [ label=]; + T32 -> T66 [ label=]; + T32 -> T51 [ label=]; + T33 -> T58 [ label=]; + T33 -> T68 [ label=]; + T70 [ label="R0(1) S2_b(<m3>) S2_a(<m3>) Richiesta(<m1>+<m2>) Attesa(<m3>) +"]; + T33 -> T70 [ label=]; + T34 -> T59 [ label=]; + T34 -> T69 [ label=]; + T34 -> T70 [ label=]; + T71 [ label="S0(1) R3(1) Richiesta(<m1>+<m2>) Attesa(<m3>) Buffer_output(<m3>) +"]; + T35 -> T71 [ label=]; + T35 -> T57 [ label=]; + T35 -> T67 [ label=]; + T72 [ label="S1_b(<m1>) R_1(<m2>) S2_a(<m1>) Richiesta(<m3>) Attesa(<m1>+<m2>) +"]; + T36 -> T72 [ label=]; + T73 [ label="R0(1) S2_b(<m1>) S2_a(<m1>) Richiesta(<m3>) Attesa(<m1>+<m2>) Buffer_input(<m2>) +"]; + T36 -> T73 [ label=]; + T74 [ label="R0(1) S1_b(<m1>) S2_a(<m1>) Attesa(<m1>+<m2>+<m3>) Buffer_input(<m2>+<m3>) +"]; + T36 -> T74 [ label=]; + T75 [ label="S1_b(<m1>) R_1(<m3>) S2_a(<m1>) Richiesta(<m2>) Attesa(<m1>+<m3>) +"]; + T37 -> T75 [ label=]; + T76 [ label="R0(1) S2_b(<m1>) S2_a(<m1>) Richiesta(<m2>) Attesa(<m1>+<m3>) Buffer_input(<m3>) +"]; + T37 -> T76 [ label=]; + T37 -> T74 [ label=]; + T77 [ label="R0(1) S3(1) Richiesta(<m2>+<m3>) Attesa(<m1>) Buffer_output(<m1>) +"]; + T38 -> T77 [ label=]; + T38 -> T76 [ label=]; + T38 -> T73 [ label=]; + T78 [ label="S1_a(<m1>) R_1(<m2>) S2_b(<m1>) Richiesta(<m3>) Attesa(<m1>+<m2>) +"]; + T39 -> T78 [ label=]; + T39 -> T73 [ label=]; + T79 [ label="R0(1) S1_a(<m1>) S2_b(<m1>) Attesa(<m1>+<m2>+<m3>) Buffer_input(<m2>+<m3>) +"]; + T39 -> T79 [ label=]; + T80 [ label="S1_a(<m1>) R_1(<m3>) S2_b(<m1>) Richiesta(<m2>) Attesa(<m1>+<m3>) +"]; + T40 -> T80 [ label=]; + T40 -> T76 [ label=]; + T40 -> T79 [ label=]; + T81 [shape=none label="..."]; + T41 -> T81 [ label=]; + T41 -> T75 [ label=]; + T41 -> T80 [ label=]; + T82 [shape=none label="..."]; + T41 -> T82 [ label=]; + T42 -> T74 [ label=]; + T42 -> T79 [ label=]; + T83 [shape=none label="..."]; + T42 -> T83 [ label=]; + T82 [shape=none label="..."]; + T42 -> T82 [ label=]; + T84 [shape=none label="..."]; + T43 -> T84 [ label=]; + T43 -> T72 [ label=]; + T43 -> T78 [ label=]; + T83 [shape=none label="..."]; + T43 -> T83 [ label=]; + T85 [shape=none label="..."]; + T44 -> T85 [ label=]; + T86 [shape=none label="..."]; + T44 -> T86 [ label=]; + T87 [shape=none label="..."]; + T44 -> T87 [ label=]; + T88 [shape=none label="..."]; + T44 -> T88 [ label=]; + T89 [shape=none label="..."]; + T45 -> T89 [ label=]; + T90 [shape=none label="..."]; + T45 -> T90 [ label=]; + T88 [shape=none label="..."]; + T45 -> T88 [ label=]; + T91 [shape=none label="..."]; + T46 -> T91 [ label=]; + T90 [shape=none label="..."]; + T46 -> T90 [ label=]; + T87 [shape=none label="..."]; + T46 -> T87 [ label=]; + T92 [shape=none label="..."]; + T47 -> T92 [ label=]; + T93 [shape=none label="..."]; + T47 -> T93 [ label=]; + T91 [shape=none label="..."]; + T47 -> T91 [ label=]; + T94 [shape=none label="..."]; + T47 -> T94 [ label=]; + T90 [shape=none label="..."]; + T48 -> T90 [ label=]; + T95 [shape=none label="..."]; + T48 -> T95 [ label=]; + T94 [shape=none label="..."]; + T48 -> T94 [ label=]; + T96 [shape=none label="..."]; + T49 -> T96 [ label=]; + T97 [shape=none label="..."]; + T49 -> T97 [ label=]; + T89 [shape=none label="..."]; + T49 -> T89 [ label=]; + T95 [shape=none label="..."]; + T49 -> T95 [ label=]; + T98 [shape=none label="..."]; + T50 -> T98 [ label=]; + T99 [shape=none label="..."]; + T50 -> T99 [ label=]; + T95 [shape=none label="..."]; + T50 -> T95 [ label=]; + T100 [shape=none label="..."]; + T50 -> T100 [ label=]; + T101 [shape=none label="..."]; + T51 -> T101 [ label=]; + T102 [shape=none label="..."]; + T51 -> T102 [ label=]; + T94 [shape=none label="..."]; + T51 -> T94 [ label=]; + T103 [shape=none label="..."]; + T51 -> T103 [ label=]; + T104 [shape=none label="..."]; + T52 -> T104 [ label=]; + T83 [shape=none label="..."]; + T52 -> T83 [ label=]; + T103 [shape=none label="..."]; + T52 -> T103 [ label=]; + T105 [shape=none label="..."]; + T53 -> T105 [ label=]; + T82 [shape=none label="..."]; + T53 -> T82 [ label=]; + T100 [shape=none label="..."]; + T53 -> T100 [ label=]; + T106 [shape=none label="..."]; + T54 -> T106 [ label=]; + T104 [shape=none label="..."]; + T54 -> T104 [ label=]; + T84 [shape=none label="..."]; + T54 -> T84 [ label=]; + T98 [shape=none label="..."]; + T55 -> T98 [ label=]; + T96 [shape=none label="..."]; + T55 -> T96 [ label=]; + T107 [shape=none label="..."]; + T55 -> T107 [ label=]; + T99 [shape=none label="..."]; + T56 -> T99 [ label=]; + T97 [shape=none label="..."]; + T56 -> T97 [ label=]; + T107 [shape=none label="..."]; + T56 -> T107 [ label=]; + T108 [shape=none label="..."]; + T57 -> T108 [ label=]; + T105 [shape=none label="..."]; + T57 -> T105 [ label=]; + T81 [shape=none label="..."]; + T57 -> T81 [ label=]; + T101 [shape=none label="..."]; + T58 -> T101 [ label=]; + T92 [shape=none label="..."]; + T58 -> T92 [ label=]; + T109 [shape=none label="..."]; + T58 -> T109 [ label=]; + T102 [shape=none label="..."]; + T59 -> T102 [ label=]; + T93 [shape=none label="..."]; + T59 -> T93 [ label=]; + T109 [shape=none label="..."]; + T59 -> T109 [ label=]; + T110 [shape=none label="..."]; + T60 -> T110 [ label=]; + T111 [shape=none label="..."]; + T60 -> T111 [ label=]; + T98 [shape=none label="..."]; + T60 -> T98 [ label=]; + T112 [shape=none label="..."]; + T61 -> T112 [ label=]; + T111 [shape=none label="..."]; + T61 -> T111 [ label=]; + T107 [shape=none label="..."]; + T61 -> T107 [ label=]; + T113 [shape=none label="..."]; + T62 -> T113 [ label=]; + T111 [shape=none label="..."]; + T62 -> T111 [ label=]; + T99 [shape=none label="..."]; + T62 -> T99 [ label=]; + T114 [shape=none label="..."]; + T63 -> T114 [ label=]; + T110 [shape=none label="..."]; + T63 -> T110 [ label=]; + T113 [shape=none label="..."]; + T63 -> T113 [ label=]; + T100 [shape=none label="..."]; + T63 -> T100 [ label=]; + T115 [shape=none label="..."]; + T64 -> T115 [ label=]; + T116 [shape=none label="..."]; + T64 -> T116 [ label=]; + T117 [shape=none label="..."]; + T64 -> T117 [ label=]; + T106 [shape=none label="..."]; + T64 -> T106 [ label=]; + T118 [shape=none label="..."]; + T65 -> T118 [ label=]; + T104 [shape=none label="..."]; + T65 -> T104 [ label=]; + T117 [shape=none label="..."]; + T65 -> T117 [ label=]; + T119 [shape=none label="..."]; + T66 -> T119 [ label=]; + T120 [shape=none label="..."]; + T66 -> T120 [ label=]; + T118 [shape=none label="..."]; + T66 -> T118 [ label=]; + T103 [shape=none label="..."]; + T66 -> T103 [ label=]; + T121 [shape=none label="..."]; + T67 -> T121 [ label=]; + T105 [shape=none label="..."]; + T67 -> T105 [ label=]; + T114 [shape=none label="..."]; + T67 -> T114 [ label=]; + T101 [shape=none label="..."]; + T68 -> T101 [ label=]; + T119 [shape=none label="..."]; + T68 -> T119 [ label=]; + T122 [shape=none label="..."]; + T68 -> T122 [ label=]; + T102 [shape=none label="..."]; + T69 -> T102 [ label=]; + T120 [shape=none label="..."]; + T69 -> T120 [ label=]; + T122 [shape=none label="..."]; + T69 -> T122 [ label=]; + T123 [shape=none label="..."]; + T70 -> T123 [ label=]; + T122 [shape=none label="..."]; + T70 -> T122 [ label=]; + T109 [shape=none label="..."]; + T70 -> T109 [ label=]; + T124 [shape=none label="..."]; + T71 -> T124 [ label=]; + T125 [shape=none label="..."]; + T71 -> T125 [ label=]; + T121 [shape=none label="..."]; + T71 -> T121 [ label=]; + T108 [shape=none label="..."]; + T71 -> T108 [ label=]; + T126 [shape=none label="..."]; + T72 -> T126 [ label=]; + T127 [shape=none label="..."]; + T72 -> T127 [ label=]; + T128 [shape=none label="..."]; + T72 -> T128 [ label=]; + T129 [shape=none label="..."]; + T73 -> T129 [ label=]; + T130 [shape=none label="..."]; + T73 -> T130 [ label=]; + T128 [shape=none label="..."]; + T73 -> T128 [ label=]; + T130 [shape=none label="..."]; + T74 -> T130 [ label=]; + T127 [shape=none label="..."]; + T74 -> T127 [ label=]; + T131 [shape=none label="..."]; + T74 -> T131 [ label=]; + T132 [shape=none label="..."]; + T75 -> T132 [ label=]; + T131 [shape=none label="..."]; + T75 -> T131 [ label=]; + T133 [shape=none label="..."]; + T75 -> T133 [ label=]; + T134 [shape=none label="..."]; + T76 -> T134 [ label=]; + T130 [shape=none label="..."]; + T76 -> T130 [ label=]; + T133 [shape=none label="..."]; + T76 -> T133 [ label=]; + T85 [shape=none label="..."]; + T77 -> T85 [ label=]; + T135 [shape=none label="..."]; + T77 -> T135 [ label=]; + T129 [shape=none label="..."]; + T77 -> T129 [ label=]; + T134 [shape=none label="..."]; + T77 -> T134 [ label=]; + T136 [shape=none label="..."]; + T78 -> T136 [ label=]; + T137 [shape=none label="..."]; + T78 -> T137 [ label=]; + T128 [shape=none label="..."]; + T78 -> T128 [ label=]; + T130 [shape=none label="..."]; + T79 -> T130 [ label=]; + T137 [shape=none label="..."]; + T79 -> T137 [ label=]; + T138 [shape=none label="..."]; + T79 -> T138 [ label=]; + T139 [shape=none label="..."]; + T80 -> T139 [ label=]; + T138 [shape=none label="..."]; + T80 -> T138 [ label=]; + T133 [shape=none label="..."]; + T80 -> T133 [ label=]; +report [ style = "filled, bold" penwidth = 5 fillcolor = "white" shape=box label=<
Reachability Graph
OPEN GRAPH: Showing a subset of markings.
Total markings:80 out of 1024
> ]; +} diff --git a/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.mark b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.mark new file mode 100644 index 0000000..8001b70 Binary files /dev/null and b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.mark differ diff --git a/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.net b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.net new file mode 100644 index 0000000..d8c2be7 --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.net @@ -0,0 +1,107 @@ +|0| +| +f 4 15 0 12 0 0 0 +N -7134 6.135416666666667 1.0989583333333333 0 +R1 -7134 6.494791666666667 1.0989583333333333 0 +R2 -7134 6.828125 1.0989583333333333 0 +n -7134 7.296875 1.0989583333333333 0 +S0 -2 10.0 2.5 9.96125 2.1122916666666667 0 +R0 -3 13.5 2.5 13.450833333333334 2.1122916666666667 0 +S1_a 0 9.0 3.5 8.205 3.6956249999999997 0 9.200000000000001 3.6666666666666665 Master +S1_b 0 11.0 3.6666666666666665 10.194583333333334 3.8622916666666662 0 11.200000000000001 3.8333333333333335 Master +R_1 0 13.5 4.0 13.257083333333334 3.9456249999999997 0 13.700000000000001 4.166666666666667 Master +R_2 0 13.5 5.333333333333333 13.340416666666668 5.278958333333333 0 13.700000000000001 5.5 Master +R3 0 13.5 6.666666666666667 13.450833333333334 6.862291666666667 0 +S2_b 0 11.0 5.333333333333333 9.444583333333332 5.028958333333333 0 11.200000000000001 5.5 Master +S3 0 10.0 6.5 9.96125 6.695625 0 +S2_a 0 9.0 5.333333333333333 8.955 5.278958333333333 0 9.200000000000001 5.5 Master +Richiesta -10003 5.0 2.3333333333333335 3.809166666666666 2.6122916666666667 0 5.2 2.5 Master +Attesa 0 5.0 4.166666666666667 4.069583333333333 4.445625 0 5.2 4.333333333333333 Master +Elabora 0 5.0 5.833333333333333 3.9758333333333327 6.112291666666667 0 5.2 6.0 Master +Buffer_input 0 6.833333333333333 3.1666666666666665 5.496666666666666 2.778958333333333 0 7.033333333333334 3.3333333333333335 Master +Buffer_output 0 6.833333333333333 6.0 5.402916666666666 6.195625 0 7.033333333333334 6.166666666666667 Master +T3 1.0 0 0 2 0 10.0 3.1666666666666665 9.479166666666666 3.2239583333333335 10.083333333333334 3.234375 0 + 1 1 0 0 + 1 14 0 0 0.000000 0.000000 + 2 + 1 3 0 0 0.000000 0.000000 + 1 4 0 0 0.000000 0.000000 + 0 +T4 1.0 0 0 1 0 9.0 4.5 9.3125 4.557291666666667 9.083333333333334 4.567708333333333 0 + 1 3 0 0 0.000000 0.000000 + 1 + 1 10 0 0 0.000000 0.000000 + 0 +T5 1.0 0 0 1 0 11.0 4.5 10.645833333333334 4.557291666666667 11.083333333333334 4.567708333333333 0 + 1 4 0 0 0.000000 0.000000 + 1 + 1 8 0 0 0.000000 0.000000 + 0 +T6 1.0 0 0 2 0 10.0 6.0 9.979166666666666 5.723958333333333 10.083333333333334 6.067708333333333 0 + 1 10 1 0 0.000000 0.000000 +10.0 5.916666666666667 + 1 8 0 0 0.000000 0.000000 + 2 + 1 9 0 0 + 1 15 3 0 0.000000 0.000000 +8.666666666666666 6.0 +8.666666666666666 6.0 +8.75 6.0 + 0 +T9 1.0 0 0 2 0 13.5 3.1666666666666665 13.8125 3.2239583333333335 13.583333333333334 3.234375 0 + 1 2 0 0 + 1 14 3 0 0.000000 0.000000 +12.5 3.1666666666666665 +12.5 1.8333333333333333 +8.083333333333334 1.8333333333333333 + 1 + 1 5 0 0 0.000000 0.000000 + 0 +T8 1.0 0 0 1 0 13.5 4.666666666666667 13.895833333333334 4.723958333333333 13.583333333333334 4.734375 0 + 1 5 0 0 0.000000 0.000000 + 1 + 1 6 0 0 0.000000 0.000000 + 0 +T7 1.0 0 0 1 0 13.5 6.0 13.8125 6.057291666666667 13.583333333333334 6.067708333333333 0 + 1 6 0 0 0.000000 0.000000 + 2 + 1 7 0 0 + 1 15 3 0 0.000000 0.000000 +12.75 6.0 +12.75 7.166666666666667 +6.833333333333333 7.166666666666667 + 0 +Reset_s 1.0 0 0 1 1 10.833333333333334 2.5 10.640625 2.3072916666666665 10.916666666666666 2.5677083333333335 0 + 1 9 2 0 +11.833333333333334 2.5 +11.833333333333334 6.416666666666667 + 1 + 1 1 0 0 + 0 +Reset_r 1.0 0 0 1 1 14.333333333333334 2.5 14.140625 2.2239583333333335 14.416666666666666 2.5677083333333335 0 + 1 7 2 0 +14.833333333333334 2.5 +14.833333333333334 6.666666666666667 + 1 + 1 2 0 0 + 0 +T1 1.0 0 0 1 0 5.0 3.1666666666666665 5.145833333333333 2.890625 5.083333333333333 3.234375 0 + 1 11 0 0 0.000000 0.000000 + 2 + 1 12 1 0 0.000000 0.000000 +5.0 3.6666666666666665 + 1 14 0 0 0.000000 0.000000 + 0 +T2 1.0 0 0 2 0 5.0 5.0 4.979166666666667 4.807291666666667 5.083333333333333 5.067708333333333 0 + 1 12 0 0 0.000000 0.000000 + 1 15 1 0 0.000000 0.000000 +6.833333333333333 5.0 + 1 + 1 13 0 0 0.000000 0.000000 + 0 +T0 1.0 0 0 1 1 4.0 5.833333333333333 3.9791666666666665 5.640625 4.083333333333333 5.901041666666667 0 + 1 13 0 0 0.000000 0.000000 + 1 + 1 11 1 0 0.000000 0.000000 +4.0 2.3333333333333335 + 0 diff --git a/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.outtype b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.outtype new file mode 100644 index 0000000..c227083 --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.outtype @@ -0,0 +1 @@ +0 \ No newline at end of file diff --git a/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.sc b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.sc new file mode 100644 index 0000000..13f36a6 --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.sc @@ -0,0 +1,12 @@ +1 5 +0 +0 +0 +1 1 +0 +0 +0 +0 +0 +0 +0 diff --git a/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.srgMaster1 b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.srgMaster1 new file mode 100644 index 0000000..25db78f --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.srgMaster1 @@ -0,0 +1,276 @@ +S0(1)R0(1)Richiesta(1<m1>) +MARKING T1 (tangible) +[T1 ( 0 + + *************************************** diff --git a/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.srgMaster3 b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.srgMaster3 new file mode 100644 index 0000000..2c54f1a --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.srgMaster3 @@ -0,0 +1,17856 @@ +S0(1)R0(1)Richiesta(1<m1>1<m2>1<m3>) +MARKING T1 (tangible) +[T1 ( 1 + + *************************************** diff --git a/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.string b/anno3/vpc/consegne/2.b/ReteE-RG of CPN.solution/CPN.string new file mode 100644 index 0000000..e69de29 diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN-RG-0.pdf b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN-RG-0.pdf new file mode 100644 index 0000000..cb0ea06 Binary files /dev/null and b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN-RG-0.pdf differ diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.cap b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.cap new file mode 100644 index 0000000..e69de29 diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.cc b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.cc new file mode 100644 index 0000000..9957bb0 --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.cc @@ -0,0 +1,12 @@ +2 2 3 +1 4 +1 4 +2 8 11 +1 6 +1 7 +2 9 11 +1 1 +1 5 +3 1 5 11 +1 12 +1 10 diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.def b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.def new file mode 100644 index 0000000..dbb491a --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.def @@ -0,0 +1,12 @@ +|256 +% +| +(Master c 5.885416666666667 1.3333333333333333 (@c +u Master_0 +)) +(Master_0 c 6.552083333333333 1.3333333333333333 (@c +m{1-n} +)) +(m_0 m 10.0 2.0 (@m +N S +)) diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.dot b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.dot new file mode 100644 index 0000000..74e6996 --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.dot @@ -0,0 +1,551 @@ +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=]; + T3 [ label="R0(1) S1_a(<Master_01>) S1_b(<Master_01>) Richiesta(<Master_00>) Attesa(<Master_01>) +|Master_01|=1 |Master_00|=2 +"]; + T2 -> T3 [ label=]; + T4 [ label="S0(1) R_1(<Master_01>) Richiesta(<Master_00>) Attesa(<Master_01>) +|Master_01|=1 |Master_00|=2 +"]; + T2 -> T4 [ label=]; + T5 [ label="S0(1) R0(1) Richiesta(<Master_01>) Attesa(<Master_00>) Buffer_input(<Master_00>) +|Master_00|=2 |Master_01|=1 +"]; + T2 -> T5 [ label=]; + T6 [ label="R0(1) S1_b(<Master_01>) S2_a(<Master_01>) Richiesta(<Master_00>) Attesa(<Master_01>) +|Master_00|=2 |Master_01|=1 +"]; + T3 -> T6 [ label=]; + T7 [ label="R0(1) S1_a(<Master_01>) S2_b(<Master_01>) Richiesta(<Master_00>) Attesa(<Master_01>) +|Master_00|=2 |Master_01|=1 +"]; + T3 -> T7 [ label=]; + T8 [ label="R0(1) S1_a(<Master_02>) S1_b(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_input(<Master_00>) +|Master_02|=1 |Master_00|=1 |Master_01|=1 +"]; + T3 -> T8 [ label=]; + T9 [ label="S0(1) R_2(<Master_01>) Richiesta(<Master_00>) Attesa(<Master_01>) +|Master_00|=2 |Master_01|=1 +"]; + T4 -> T9 [ label=]; + T10 [ label="S0(1) R_1(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_input(<Master_00>) +|Master_02|=1 |Master_00|=1 |Master_01|=1 +"]; + T4 -> T10 [ label=]; + T11 [ label="S0(1) R0(1) Attesa(<Master_00>) Buffer_input(<Master_00>) +|Master_00|=3 +"]; + T5 -> T11 [ label=]; + T5 -> T10 [ label=]; + T5 -> T8 [ label=]; + T12 [ label="R0(1) S1_b(<Master_02>) S2_a(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_input(<Master_00>) +|Master_02|=1 |Master_00|=1 |Master_01|=1 +"]; + T6 -> T12 [ label=]; + T13 [ label="R0(1) S2_b(<Master_01>) S2_a(<Master_01>) Richiesta(<Master_00>) Attesa(<Master_01>) +|Master_00|=2 |Master_01|=1 +"]; + T6 -> T13 [ label=]; + T14 [ label="R0(1) S1_a(<Master_02>) S2_b(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_input(<Master_00>) +|Master_02|=1 |Master_00|=1 |Master_01|=1 +"]; + T7 -> T14 [ label=]; + T7 -> T13 [ label=]; + T15 [ label="S1_a(<Master_02>) S1_b(<Master_02>) R_1(<Master_01>) Richiesta(<Master_00>) Attesa(<Master_01>+<Master_02>) +|Master_01|=1 |Master_00|=1 |Master_02|=1 +"]; + T8 -> T15 [ label=]; + T16 [ label="R0(1) S1_a(<Master_01>) S1_b(<Master_01>) Attesa(<Master_00>+<Master_01>) Buffer_input(<Master_00>) +|Master_00|=2 |Master_01|=1 +"]; + T8 -> T16 [ label=]; + T8 -> T14 [ label=]; + T8 -> T12 [ label=]; + T17 [ label="S0(1) R3(1) Richiesta(<Master_01>) Attesa(<Master_00>) Buffer_output(<Master_00>) +|Master_01|=2 |Master_00|=1 +"]; + T9 -> T17 [ label=]; + T18 [ label="S0(1) R_2(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_input(<Master_00>) +|Master_02|=1 |Master_00|=1 |Master_01|=1 +"]; + T9 -> T18 [ label=]; + T10 -> T15 [ label=]; + T19 [ label="S0(1) R_1(<Master_01>) Attesa(<Master_00>+<Master_01>) Buffer_input(<Master_00>) +|Master_00|=2 |Master_01|=1 +"]; + T10 -> T19 [ label=]; + T10 -> T18 [ label=]; + T11 -> T16 [ label=]; + T11 -> T19 [ label=]; + T20 [ label="S1_b(<Master_02>) R_1(<Master_01>) S2_a(<Master_02>) Richiesta(<Master_00>) Attesa(<Master_01>+<Master_02>) +|Master_01|=1 |Master_00|=1 |Master_02|=1 +"]; + T12 -> T20 [ label=]; + T21 [ label="R0(1) S2_b(<Master_02>) S2_a(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_input(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T12 -> T21 [ label=]; + T22 [ label="R0(1) S1_b(<Master_01>) S2_a(<Master_01>) Attesa(<Master_00>+<Master_01>) Buffer_input(<Master_00>) +|Master_00|=2 |Master_01|=1 +"]; + T12 -> T22 [ label=]; + T23 [ label="R0(1) S3(1) Richiesta(<Master_01>) Attesa(<Master_00>) Buffer_output(<Master_00>) +|Master_01|=2 |Master_00|=1 +"]; + T13 -> T23 [ label=]; + T13 -> T21 [ label=]; + T24 [ label="S1_a(<Master_02>) R_1(<Master_01>) S2_b(<Master_02>) Richiesta(<Master_00>) Attesa(<Master_01>+<Master_02>) +|Master_01|=1 |Master_00|=1 |Master_02|=1 +"]; + T14 -> T24 [ label=]; + T14 -> T21 [ label=]; + T25 [ label="R0(1) S1_a(<Master_01>) S2_b(<Master_01>) Attesa(<Master_00>+<Master_01>) Buffer_input(<Master_00>) +|Master_00|=2 |Master_01|=1 +"]; + T14 -> T25 [ label=]; + T26 [ label="S1_a(<Master_02>) S1_b(<Master_02>) R_2(<Master_01>) Richiesta(<Master_00>) Attesa(<Master_01>+<Master_02>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T15 -> T26 [ label=]; + T15 -> T20 [ label=]; + T15 -> T24 [ label=]; + T27 [ label="S1_a(<Master_02>) S1_b(<Master_02>) R_1(<Master_01>) Attesa(<Master_00>+<Master_01>+<Master_02>) Buffer_input(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T15 -> T27 [ label=]; + T16 -> T22 [ label=]; + T16 -> T25 [ label=]; + T16 -> T27 [ label=]; + T28 [ label="S0(1) R0(1) Richiesta(<Master_01>) Attesa(<Master_00>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_01|=2 +"]; + T17 -> T28 [ label=]; + T29 [ label="S0(1) R3(1) Richiesta(<Master_01>) Elabora(<Master_00>) +|Master_00|=1 |Master_01|=2 +"]; + T17 -> T29 [ label=]; + T30 [ label="S0(1) R3(1) Richiesta(<Master_02>) Attesa(<Master_00>+<Master_01>) Buffer_input(<Master_01>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_02|=1 |Master_01|=1 +"]; + T17 -> T30 [ label=]; + T18 -> T26 [ label=]; + T31 [ label="S0(1) R_2(<Master_01>) Attesa(<Master_00>+<Master_01>) Buffer_input(<Master_00>) +|Master_00|=2 |Master_01|=1 +"]; + T18 -> T31 [ label=]; + T18 -> T30 [ label=]; + T19 -> T31 [ label=]; + T19 -> T27 [ label=]; + T32 [ label="S1_b(<Master_02>) R_2(<Master_01>) S2_a(<Master_02>) Richiesta(<Master_00>) Attesa(<Master_01>+<Master_02>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T20 -> T32 [ label=]; + T33 [ label="S1_b(<Master_02>) R_1(<Master_01>) S2_a(<Master_02>) Attesa(<Master_00>+<Master_01>+<Master_02>) Buffer_input(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T20 -> T33 [ label=]; + T34 [ label="R_1(<Master_02>) S2_b(<Master_01>) S2_a(<Master_01>) Richiesta(<Master_00>) Attesa(<Master_01>+<Master_02>) +|Master_00|=1 |Master_02|=1 |Master_01|=1 +"]; + T20 -> T34 [ label=]; + T35 [ label="R0(1) S3(1) Richiesta(<Master_02>) Attesa(<Master_00>+<Master_01>) Buffer_input(<Master_01>) Buffer_output(<Master_00>) +|Master_02|=1 |Master_00|=1 |Master_01|=1 +"]; + T21 -> T35 [ label=]; + T36 [ label="R0(1) S2_b(<Master_01>) S2_a(<Master_01>) Attesa(<Master_00>+<Master_01>) Buffer_input(<Master_00>) +|Master_00|=2 |Master_01|=1 +"]; + T21 -> T36 [ label=]; + T21 -> T34 [ label=]; + T22 -> T36 [ label=]; + T22 -> T33 [ label=]; + T23 -> T28 [ label=]; + T37 [ label="R0(1) S3(1) Richiesta(<Master_01>) Elabora(<Master_00>) +|Master_00|=1 |Master_01|=2 +"]; + T23 -> T37 [ label=]; + T23 -> T35 [ label=]; + T38 [ label="S1_a(<Master_02>) R_2(<Master_01>) S2_b(<Master_02>) Richiesta(<Master_00>) Attesa(<Master_01>+<Master_02>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T24 -> T38 [ label=]; + T39 [ label="S1_a(<Master_02>) R_1(<Master_01>) S2_b(<Master_02>) Attesa(<Master_00>+<Master_01>+<Master_02>) Buffer_input(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T24 -> T39 [ label=]; + T24 -> T34 [ label=]; + T25 -> T36 [ label=]; + T25 -> T39 [ label=]; + T40 [ label="S1_a(<Master_02>) S1_b(<Master_02>) R3(1) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_output(<Master_00>) +|Master_01|=1 |Master_00|=1 |Master_02|=1 +"]; + T26 -> T40 [ label=]; + T41 [ label="S1_a(<Master_02>) S1_b(<Master_02>) R_2(<Master_01>) Attesa(<Master_00>+<Master_01>+<Master_02>) Buffer_input(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T26 -> T41 [ label=]; + T26 -> T38 [ label=]; + T26 -> T32 [ label=]; + T27 -> T39 [ label=]; + T27 -> T33 [ label=]; + T27 -> T41 [ label=]; + T42 [ label="S0(1) R0(1) Richiesta(<Master_02>) Attesa(<Master_00>+<Master_01>) Buffer_input(<Master_01>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_02|=1 |Master_01|=1 +"]; + T28 -> T42 [ label=]; + T43 [ label="S0(1) R0(1) Richiesta(<Master_01>) Elabora(<Master_00>) +|Master_00|=1 |Master_01|=2 +"]; + T28 -> T43 [ label=]; + T44 [ label="S0(1) R3(1) Richiesta(<Master_00>) +|Master_00|=3 +"]; + T29 -> T44 [ label=]; + T45 [ label="S0(1) R3(1) Richiesta(<Master_02>) Attesa(<Master_01>) Elabora(<Master_00>) Buffer_input(<Master_01>) +|Master_00|=1 |Master_02|=1 |Master_01|=1 +"]; + T29 -> T45 [ label=]; + T29 -> T43 [ label=]; + T30 -> T40 [ label=]; + T46 [ label="S0(1) R3(1) Attesa(<Master_00>+<Master_01>) Buffer_input(<Master_01>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_01|=2 +"]; + T30 -> T46 [ label=]; + T30 -> T45 [ label=]; + T30 -> T42 [ label=]; + T31 -> T46 [ label=]; + T31 -> T41 [ label=]; + T47 [ label="S1_b(<Master_02>) R3(1) S2_a(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_output(<Master_00>) +|Master_01|=1 |Master_00|=1 |Master_02|=1 +"]; + T32 -> T47 [ label=]; + T48 [ label="R_2(<Master_02>) S2_b(<Master_01>) S2_a(<Master_01>) Richiesta(<Master_00>) Attesa(<Master_01>+<Master_02>) +|Master_00|=1 |Master_02|=1 |Master_01|=1 +"]; + T32 -> T48 [ label=]; + T49 [ label="S1_b(<Master_02>) R_2(<Master_01>) S2_a(<Master_02>) Attesa(<Master_00>+<Master_01>+<Master_02>) Buffer_input(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T32 -> T49 [ label=]; + T50 [ label="R_1(<Master_02>) S2_b(<Master_01>) S2_a(<Master_01>) Attesa(<Master_00>+<Master_01>+<Master_02>) Buffer_input(<Master_00>) +|Master_00|=1 |Master_02|=1 |Master_01|=1 +"]; + T33 -> T50 [ label=]; + T33 -> T49 [ label=]; + T51 [ label="R_1(<Master_02>) S3(1) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_output(<Master_00>) +|Master_01|=1 |Master_00|=1 |Master_02|=1 +"]; + T34 -> T51 [ label=]; + T34 -> T50 [ label=]; + T34 -> T48 [ label=]; + T35 -> T42 [ label=]; + T52 [ label="R0(1) S3(1) Richiesta(<Master_02>) Attesa(<Master_01>) Elabora(<Master_00>) Buffer_input(<Master_01>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T35 -> T52 [ label=]; + T35 -> T51 [ label=]; + T53 [ label="R0(1) S3(1) Attesa(<Master_00>+<Master_01>) Buffer_input(<Master_01>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_01|=2 +"]; + T35 -> T53 [ label=]; + T36 -> T50 [ label=]; + T36 -> T53 [ label=]; + T54 [ label="R0(1) S3(1) Richiesta(<Master_00>) +|Master_00|=3 +"]; + T37 -> T54 [ label=]; + T37 -> T52 [ label=]; + T37 -> T43 [ label=]; + T55 [ label="S1_a(<Master_02>) R3(1) S2_b(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_output(<Master_00>) +|Master_01|=1 |Master_00|=1 |Master_02|=1 +"]; + T38 -> T55 [ label=]; + T38 -> T48 [ label=]; + T56 [ label="S1_a(<Master_02>) R_2(<Master_01>) S2_b(<Master_02>) Attesa(<Master_00>+<Master_01>+<Master_02>) Buffer_input(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T38 -> T56 [ label=]; + T39 -> T50 [ label=]; + T39 -> T56 [ label=]; + T57 [ label="R0(1) S1_a(<Master_02>) S1_b(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T40 -> T57 [ label=]; + T58 [ label="S1_a(<Master_02>) S1_b(<Master_02>) R3(1) Richiesta(<Master_01>) Attesa(<Master_02>) Elabora(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T40 -> T58 [ label=]; + T40 -> T47 [ label=]; + T40 -> T55 [ label=]; + T59 [ label="S1_a(<Master_02>) S1_b(<Master_02>) R3(1) Attesa(<Master_00>+<Master_01>+<Master_02>) Buffer_input(<Master_01>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T40 -> T59 [ label=]; + T41 -> T49 [ label=]; + T41 -> T56 [ label=]; + T41 -> T59 [ label=]; + T42 -> T57 [ label=]; + T60 [ label="S0(1) R_1(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_02|=1 |Master_01|=1 +"]; + T42 -> T60 [ label=]; + T61 [ label="S0(1) R0(1) Richiesta(<Master_02>) Attesa(<Master_01>) Elabora(<Master_00>) Buffer_input(<Master_01>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T42 -> T61 [ label=]; + T62 [ label="S0(1) R0(1) Attesa(<Master_00>+<Master_01>) Buffer_input(<Master_01>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_01|=2 +"]; + T42 -> T62 [ label=]; + T43 -> T1 [ label=]; + T43 -> T61 [ label=]; + T44 -> T1 [ label=]; + T63 [ label="S0(1) R3(1) Richiesta(<Master_01>) Attesa(<Master_00>) Buffer_input(<Master_00>) +|Master_01|=2 |Master_00|=1 +"]; + T44 -> T63 [ label=]; + T45 -> T58 [ label=]; + T45 -> T61 [ label=]; + T64 [ label="S0(1) R3(1) Attesa(<Master_01>) Elabora(<Master_00>) Buffer_input(<Master_01>) +|Master_00|=1 |Master_01|=2 +"]; + T45 -> T64 [ label=]; + T45 -> T63 [ label=]; + T46 -> T62 [ label=]; + T46 -> T64 [ label=]; + T46 -> T59 [ label=]; + T65 [ label="R0(1) S1_b(<Master_02>) S2_a(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T47 -> T65 [ label=]; + T66 [ label="S1_b(<Master_02>) R3(1) S2_a(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_02>) Elabora(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T47 -> T66 [ label=]; + T67 [ label="S1_b(<Master_02>) R3(1) S2_a(<Master_02>) Attesa(<Master_00>+<Master_01>+<Master_02>) Buffer_input(<Master_01>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T47 -> T67 [ label=]; + T68 [ label="R3(1) S2_b(<Master_02>) S2_a(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T47 -> T68 [ label=]; + T69 [ label="R_2(<Master_02>) S3(1) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_output(<Master_00>) +|Master_01|=1 |Master_00|=1 |Master_02|=1 +"]; + T48 -> T69 [ label=]; + T70 [ label="R_2(<Master_02>) S2_b(<Master_01>) S2_a(<Master_01>) Attesa(<Master_00>+<Master_01>+<Master_02>) Buffer_input(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T48 -> T70 [ label=]; + T48 -> T68 [ label=]; + T49 -> T70 [ label=]; + T49 -> T67 [ label=]; + T71 [ label="R_1(<Master_02>) S3(1) Attesa(<Master_00>+<Master_01>+<Master_02>) Buffer_input(<Master_01>) Buffer_output(<Master_00>) +|Master_01|=1 |Master_00|=1 |Master_02|=1 +"]; + T50 -> T71 [ label=]; + T50 -> T70 [ label=]; + T51 -> T60 [ label=]; + T72 [ label="R_1(<Master_02>) S3(1) Richiesta(<Master_01>) Attesa(<Master_02>) Elabora(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T51 -> T72 [ label=]; + T51 -> T69 [ label=]; + T51 -> T71 [ label=]; + T73 [ label="R0(1) S3(1) Richiesta(<Master_01>) Attesa(<Master_00>) Buffer_input(<Master_00>) +|Master_01|=2 |Master_00|=1 +"]; + T52 -> T73 [ label=]; + T74 [ label="R0(1) S3(1) Attesa(<Master_01>) Elabora(<Master_00>) Buffer_input(<Master_01>) +|Master_00|=1 |Master_01|=2 +"]; + T52 -> T74 [ label=]; + T52 -> T72 [ label=]; + T52 -> T61 [ label=]; + T53 -> T71 [ label=]; + T53 -> T74 [ label=]; + T53 -> T62 [ label=]; + T54 -> T1 [ label=]; + T54 -> T73 [ label=]; + T75 [ label="R0(1) S1_a(<Master_02>) S2_b(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_00>+<Master_02>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T55 -> T75 [ label=]; + T76 [ label="S1_a(<Master_02>) R3(1) S2_b(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_02>) Elabora(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T55 -> T76 [ label=]; + T77 [ label="S1_a(<Master_02>) R3(1) S2_b(<Master_02>) Attesa(<Master_00>+<Master_01>+<Master_02>) Buffer_input(<Master_01>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T55 -> T77 [ label=]; + T55 -> T68 [ label=]; + T56 -> T70 [ label=]; + T56 -> T77 [ label=]; + T78 [ label="R0(1) S1_a(<Master_02>) S1_b(<Master_02>) Attesa(<Master_00>+<Master_01>+<Master_02>) Buffer_input(<Master_01>) Buffer_output(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T57 -> T78 [ label=]; + T57 -> T75 [ label=]; + T57 -> T65 [ label=]; + T79 [ label="R0(1) S1_a(<Master_02>) S1_b(<Master_02>) Richiesta(<Master_01>) Attesa(<Master_02>) Elabora(<Master_00>) +|Master_00|=1 |Master_01|=1 |Master_02|=1 +"]; + T57 -> T79 [ label=]; + T80 [ label="S1_a(<Master_01>) S1_b(<Master_01>) R3(1) Richiesta(<Master_00>) Attesa(<Master_01>) +|Master_01|=1 |Master_00|=2 +"]; + T58 -> T80 [ label=]; + T81 [shape=none label="..."]; + T58 -> T81 [ label=]; + T58 -> T76 [ label=]; + T58 -> T66 [ label=]; + T58 -> T79 [ label=]; + T59 -> T77 [ label=]; + T59 -> T67 [ label=]; + T81 [shape=none label="..."]; + T59 -> T81 [ label=]; + T59 -> T78 [ label=]; + T82 [shape=none label="..."]; + T60 -> T82 [ label=]; + T83 [shape=none label="..."]; + T60 -> T83 [ label=]; + T84 [shape=none label="..."]; + T60 -> T84 [ label=]; + T61 -> T2 [ label=]; + T85 [shape=none label="..."]; + T61 -> T85 [ label=]; + T84 [shape=none label="..."]; + T61 -> T84 [ label=]; + T61 -> T79 [ label=]; + T85 [shape=none label="..."]; + T62 -> T85 [ label=]; + T83 [shape=none label="..."]; + T62 -> T83 [ label=]; + T62 -> T78 [ label=]; + T63 -> T80 [ label=]; + T86 [shape=none label="..."]; + T63 -> T86 [ label=]; + T63 -> T2 [ label=]; + T86 [shape=none label="..."]; + T64 -> T86 [ label=]; + T85 [shape=none label="..."]; + T64 -> T85 [ label=]; + T81 [shape=none label="..."]; + T64 -> T81 [ label=]; + T87 [shape=none label="..."]; + T65 -> T87 [ label=]; + T88 [shape=none label="..."]; + T65 -> T88 [ label=]; + T89 [shape=none label="..."]; + T65 -> T89 [ label=]; + T90 [shape=none label="..."]; + T66 -> T90 [ label=]; + T91 [shape=none label="..."]; + T66 -> T91 [ label=]; + T92 [shape=none label="..."]; + T66 -> T92 [ label=]; + T89 [shape=none label="..."]; + T66 -> T89 [ label=]; + T93 [shape=none label="..."]; + T67 -> T93 [ label=]; + T92 [shape=none label="..."]; + T67 -> T92 [ label=]; + T88 [shape=none label="..."]; + T67 -> T88 [ label=]; + T94 [shape=none label="..."]; + T68 -> T94 [ label=]; + T93 [shape=none label="..."]; + T68 -> T93 [ label=]; + T91 [shape=none label="..."]; + T68 -> T91 [ label=]; + T87 [shape=none label="..."]; + T68 -> T87 [ label=]; + T82 [shape=none label="..."]; + T69 -> T82 [ label=]; + T95 [shape=none label="..."]; + T69 -> T95 [ label=]; + T94 [shape=none label="..."]; + T69 -> T94 [ label=]; + T96 [shape=none label="..."]; + T69 -> T96 [ label=]; + T93 [shape=none label="..."]; + T70 -> T93 [ label=]; + T96 [shape=none label="..."]; + T70 -> T96 [ label=]; + T83 [shape=none label="..."]; + T71 -> T83 [ label=]; + T97 [shape=none label="..."]; + T71 -> T97 [ label=]; + T96 [shape=none label="..."]; + T71 -> T96 [ label=]; + T98 [shape=none label="..."]; + T72 -> T98 [ label=]; + T97 [shape=none label="..."]; + T72 -> T97 [ label=]; + T95 [shape=none label="..."]; + T72 -> T95 [ label=]; + T84 [shape=none label="..."]; + T72 -> T84 [ label=]; + T73 -> T2 [ label=]; + T98 [shape=none label="..."]; + T73 -> T98 [ label=]; + T99 [shape=none label="..."]; + T73 -> T99 [ label=]; + T85 [shape=none label="..."]; + T74 -> T85 [ label=]; + T97 [shape=none label="..."]; + T74 -> T97 [ label=]; + T99 [shape=none label="..."]; + T74 -> T99 [ label=]; + T87 [shape=none label="..."]; + T75 -> T87 [ label=]; + T100 [shape=none label="..."]; + T75 -> T100 [ label=]; + T101 [shape=none label="..."]; + T75 -> T101 [ label=]; + T102 [shape=none label="..."]; + T76 -> T102 [ label=]; + T91 [shape=none label="..."]; + T76 -> T91 [ label=]; + T103 [shape=none label="..."]; + T76 -> T103 [ label=]; + T101 [shape=none label="..."]; + T76 -> T101 [ label=]; + T93 [shape=none label="..."]; + T77 -> T93 [ label=]; + T103 [shape=none label="..."]; + T77 -> T103 [ label=]; + T100 [shape=none label="..."]; + T77 -> T100 [ label=]; + T104 [shape=none label="..."]; + T78 -> T104 [ label=]; + T105 [shape=none label="..."]; + T78 -> T105 [ label=]; + T88 [shape=none label="..."]; + T78 -> T88 [ label=]; + T100 [shape=none label="..."]; + T78 -> T100 [ label=]; + T79 -> T3 [ label=]; + T89 [shape=none label="..."]; + T79 -> T89 [ label=]; + T101 [shape=none label="..."]; + T79 -> T101 [ label=]; + T105 [shape=none label="..."]; + T79 -> T105 [ label=]; + T80 -> T3 [ label=]; + T90 [shape=none label="..."]; + T80 -> T90 [ label=]; + T102 [shape=none label="..."]; + T80 -> T102 [ label=]; + T106 [shape=none label="..."]; + T80 -> T106 [ label=]; +report [ style = "filled, bold" penwidth = 5 fillcolor = "white" shape=box label=<
Symbolic Reachability Graph
OPEN GRAPH: Showing a subset of markings.
Total markings:80 out of 232
> ]; +} diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.mark b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.mark new file mode 100644 index 0000000..8bed6ca Binary files /dev/null and b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.mark differ diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.minval b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.minval new file mode 100644 index 0000000..8c64d05 --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.minval @@ -0,0 +1 @@ +*0*0*0*0*0*0*0*3*0*3*0 \ No newline at end of file diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.net b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.net new file mode 100644 index 0000000..715ccbe --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.net @@ -0,0 +1,107 @@ +|0| +| +f 4 15 0 12 0 0 0 +N -7134 6.135416666666667 1.0989583333333333 0 +Sn -7134 6.505208333333333 1.0989583333333333 0 +Rn -7134 6.848958333333333 1.0989583333333333 0 +n -7134 7.296875 1.0989583333333333 0 +S0 -2 10.0 2.5 9.96125 2.1122916666666667 0 +R0 -3 13.5 2.5 13.450833333333334 2.1122916666666667 0 +S1_a 0 9.0 3.5 8.205 3.6956249999999997 0 9.200000000000001 3.6666666666666665 Master +S1_b 0 11.0 3.6666666666666665 10.194583333333334 3.8622916666666662 0 11.200000000000001 3.8333333333333335 Master +R_1 0 13.5 4.0 13.257083333333334 3.9456249999999997 0 13.700000000000001 4.166666666666667 Master +R_2 0 13.5 5.333333333333333 13.340416666666668 5.278958333333333 0 13.700000000000001 5.5 Master +R3 0 13.5 6.666666666666667 13.450833333333334 6.862291666666667 0 +S2_b 0 11.0 5.333333333333333 9.444583333333332 5.028958333333333 0 11.200000000000001 5.5 Master +S3 0 10.0 6.5 9.96125 6.695625 0 +S2_a 0 9.0 5.333333333333333 8.955 5.278958333333333 0 9.200000000000001 5.5 Master +Richiesta -10003 5.0 2.3333333333333335 3.809166666666666 2.6122916666666667 0 5.2 2.5 Master +Attesa 0 5.0 4.166666666666667 4.069583333333333 4.445625 0 5.2 4.333333333333333 Master +Elabora 0 5.0 5.833333333333333 3.9758333333333327 6.112291666666667 0 5.2 6.0 Master +Buffer_input 0 6.833333333333333 3.1666666666666665 5.496666666666666 2.778958333333333 0 7.033333333333334 3.3333333333333335 Master +Buffer_output 0 6.833333333333333 6.0 5.402916666666666 6.195625 0 7.033333333333334 6.166666666666667 Master +T3 1.0 0 0 2 0 10.0 3.1666666666666665 9.479166666666666 3.2239583333333335 10.083333333333334 3.234375 0 + 1 1 0 0 + 1 14 0 0 0.000000 0.000000 + 2 + 1 3 0 0 0.000000 0.000000 + 1 4 0 0 0.000000 0.000000 + 0 +T4 1.0 0 0 1 0 9.0 4.5 9.3125 4.557291666666667 9.083333333333334 4.567708333333333 0 + 1 3 0 0 0.000000 0.000000 + 1 + 1 10 0 0 0.000000 0.000000 + 0 +T5 1.0 0 0 1 0 11.0 4.5 10.645833333333334 4.557291666666667 11.083333333333334 4.567708333333333 0 + 1 4 0 0 0.000000 0.000000 + 1 + 1 8 0 0 0.000000 0.000000 + 0 +T6 1.0 0 0 2 0 10.0 6.0 9.979166666666666 5.723958333333333 10.083333333333334 6.067708333333333 0 + 1 10 1 0 0.000000 0.000000 +10.0 5.916666666666667 + 1 8 0 0 0.000000 0.000000 + 2 + 1 9 0 0 + 1 15 3 0 0.000000 0.000000 +8.666666666666666 6.0 +8.666666666666666 6.0 +8.75 6.0 + 0 +T9 1.0 0 0 2 0 13.5 3.1666666666666665 13.8125 3.2239583333333335 13.583333333333334 3.234375 0 + 1 2 0 0 + 1 14 3 0 0.000000 0.000000 +12.5 3.1666666666666665 +12.5 1.8333333333333333 +8.083333333333334 1.8333333333333333 + 1 + 1 5 0 0 0.000000 0.000000 + 0 +T8 1.0 0 0 1 0 13.5 4.666666666666667 13.895833333333334 4.723958333333333 13.583333333333334 4.734375 0 + 1 5 0 0 0.000000 0.000000 + 1 + 1 6 0 0 0.000000 0.000000 + 0 +T7 1.0 0 0 1 0 13.5 6.0 13.8125 6.057291666666667 13.583333333333334 6.067708333333333 0 + 1 6 0 0 0.000000 0.000000 + 2 + 1 7 0 0 + 1 15 3 0 0.000000 0.000000 +12.75 6.0 +12.75 7.166666666666667 +6.833333333333333 7.166666666666667 + 0 +Reset_s 1.0 0 0 1 1 10.833333333333334 2.5 10.640625 2.3072916666666665 10.916666666666666 2.5677083333333335 0 + 1 9 2 0 +11.833333333333334 2.5 +11.833333333333334 6.416666666666667 + 1 + 1 1 0 0 + 0 +Reset_r 1.0 0 0 1 1 14.333333333333334 2.5 14.140625 2.2239583333333335 14.416666666666666 2.5677083333333335 0 + 1 7 2 0 +14.833333333333334 2.5 +14.833333333333334 6.666666666666667 + 1 + 1 2 0 0 + 0 +T1 1.0 0 0 1 0 5.0 3.1666666666666665 5.145833333333333 2.890625 5.083333333333333 3.234375 0 + 1 11 0 0 0.000000 0.000000 + 2 + 1 12 1 0 0.000000 0.000000 +5.0 3.6666666666666665 + 1 14 0 0 0.000000 0.000000 + 0 +T2 1.0 0 0 2 0 5.0 5.0 4.979166666666667 4.807291666666667 5.083333333333333 5.067708333333333 0 + 1 12 0 0 0.000000 0.000000 + 1 15 1 0 0.000000 0.000000 +6.833333333333333 5.0 + 1 + 1 13 0 0 0.000000 0.000000 + 0 +T0 1.0 0 0 1 1 4.0 5.833333333333333 3.9791666666666665 5.640625 4.083333333333333 5.901041666666667 0 + 1 13 0 0 0.000000 0.000000 + 1 + 1 11 1 0 0.000000 0.000000 +4.0 2.3333333333333335 + 0 diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.outtype b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.outtype new file mode 100644 index 0000000..56a6051 --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.outtype @@ -0,0 +1 @@ +1 \ No newline at end of file diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.sc b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.sc new file mode 100644 index 0000000..13f36a6 --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.sc @@ -0,0 +1,12 @@ +1 5 +0 +0 +0 +1 1 +0 +0 +0 +0 +0 +0 +0 diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.srgMaster1 b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.srgMaster1 new file mode 100644 index 0000000..2d5c034 --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.srgMaster1 @@ -0,0 +1,332 @@ +S0(1)R0(1)Richiesta(1<Master_00>) +|Master_00|=1 +MARKING T1 (tangible) +[T1 ( 0 + + *************************************** diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.srgMaster3 b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.srgMaster3 new file mode 100644 index 0000000..957597d --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.srgMaster3 @@ -0,0 +1,4244 @@ +S0(1)R0(1)Richiesta(1<Master_00>) +|Master_00|=3 +MARKING T1 (tangible) +[T1 ( 0 + + *************************************** diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.string b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.string new file mode 100644 index 0000000..e69de29 diff --git a/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.val b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.val new file mode 100644 index 0000000..ce664da --- /dev/null +++ b/anno3/vpc/consegne/2.b/ReteE-SRG of CPN.solution/CPN.val @@ -0,0 +1 @@ +*0*1*0*0*1*2*1*2*0*0*0 \ No newline at end of file diff --git a/anno3/vpc/consegne/2.b/ReteE.PNPRO b/anno3/vpc/consegne/2.b/ReteE.PNPRO index 22e0cba..fa07f37 100644 --- a/anno3/vpc/consegne/2.b/ReteE.PNPRO +++ b/anno3/vpc/consegne/2.b/ReteE.PNPRO @@ -1,9 +1,9 @@ - + - - + + @@ -27,14 +27,14 @@ - - - + + +