reteF quasi

This commit is contained in:
Francesco Mecca 2020-05-05 15:06:01 +02:00
parent 0eac2b81c7
commit ec0110f88c
54 changed files with 52775 additions and 47 deletions

View file

@ -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

View file

@ -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

View file

@ -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
))

View file

@ -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=<T1&gt;>];
T3 [ label="S0(1) R0(1) Richiesta(&lt;m1&gt;+&lt;m3&gt;) Attesa(&lt;m2&gt;) Buffer_input(&lt;m2&gt;)
"];
T1 -> T3 [ label=<T1&gt;>];
T4 [ label="S0(1) R0(1) Richiesta(&lt;m1&gt;+&lt;m2&gt;) Attesa(&lt;m3&gt;) Buffer_input(&lt;m3&gt;)
"];
T1 -> T4 [ label=<T1&gt;>];
T5 [ label="R0(1) S1_a(&lt;m1&gt;) S1_b(&lt;m1&gt;) Richiesta(&lt;m2&gt;+&lt;m3&gt;) Attesa(&lt;m1&gt;)
"];
T2 -> T5 [ label=<T3&gt;>];
T6 [ label="S0(1) R_1(&lt;m1&gt;) Richiesta(&lt;m2&gt;+&lt;m3&gt;) Attesa(&lt;m1&gt;)
"];
T2 -> T6 [ label=<T9&gt;>];
T7 [ label="S0(1) R0(1) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;) Buffer_input(&lt;m1&gt;+&lt;m2&gt;)
"];
T2 -> T7 [ label=<T1&gt;>];
T8 [ label="S0(1) R0(1) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;) Buffer_input(&lt;m1&gt;+&lt;m3&gt;)
"];
T2 -> T8 [ label=<T1&gt;>];
T9 [ label="R0(1) S1_a(&lt;m2&gt;) S1_b(&lt;m2&gt;) Richiesta(&lt;m1&gt;+&lt;m3&gt;) Attesa(&lt;m2&gt;)
"];
T3 -> T9 [ label=<T3&gt;>];
T10 [ label="S0(1) R_1(&lt;m2&gt;) Richiesta(&lt;m1&gt;+&lt;m3&gt;) Attesa(&lt;m2&gt;)
"];
T3 -> T10 [ label=<T9&gt;>];
T3 -> T7 [ label=<T1&gt;>];
T11 [ label="S0(1) R0(1) Richiesta(&lt;m1&gt;) Attesa(&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m2&gt;+&lt;m3&gt;)
"];
T3 -> T11 [ label=<T1&gt;>];
T12 [ label="R0(1) S1_a(&lt;m3&gt;) S1_b(&lt;m3&gt;) Richiesta(&lt;m1&gt;+&lt;m2&gt;) Attesa(&lt;m3&gt;)
"];
T4 -> T12 [ label=<T3&gt;>];
T13 [ label="S0(1) R_1(&lt;m3&gt;) Richiesta(&lt;m1&gt;+&lt;m2&gt;) Attesa(&lt;m3&gt;)
"];
T4 -> T13 [ label=<T9&gt;>];
T4 -> T8 [ label=<T1&gt;>];
T4 -> T11 [ label=<T1&gt;>];
T14 [ label="R0(1) S1_b(&lt;m1&gt;) S2_a(&lt;m1&gt;) Richiesta(&lt;m2&gt;+&lt;m3&gt;) Attesa(&lt;m1&gt;)
"];
T5 -> T14 [ label=<T4&gt;>];
T15 [ label="R0(1) S1_a(&lt;m1&gt;) S2_b(&lt;m1&gt;) Richiesta(&lt;m2&gt;+&lt;m3&gt;) Attesa(&lt;m1&gt;)
"];
T5 -> T15 [ label=<T5&gt;>];
T16 [ label="R0(1) S1_a(&lt;m1&gt;) S1_b(&lt;m1&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;) Buffer_input(&lt;m3&gt;)
"];
T5 -> T16 [ label=<T1&gt;>];
T17 [ label="R0(1) S1_a(&lt;m1&gt;) S1_b(&lt;m1&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;) Buffer_input(&lt;m2&gt;)
"];
T5 -> T17 [ label=<T1&gt;>];
T18 [ label="S0(1) R_2(&lt;m1&gt;) Richiesta(&lt;m2&gt;+&lt;m3&gt;) Attesa(&lt;m1&gt;)
"];
T6 -> T18 [ label=<T8&gt;>];
T19 [ label="S0(1) R_1(&lt;m1&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;) Buffer_input(&lt;m3&gt;)
"];
T6 -> T19 [ label=<T1&gt;>];
T20 [ label="S0(1) R_1(&lt;m1&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;) Buffer_input(&lt;m2&gt;)
"];
T6 -> T20 [ label=<T1&gt;>];
T21 [ label="S0(1) R0(1) Attesa(&lt;m1&gt;+&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m1&gt;+&lt;m2&gt;+&lt;m3&gt;)
"];
T7 -> T21 [ label=<T1&gt;>];
T7 -> T20 [ label=<T9&gt;>];
T22 [ label="S0(1) R_1(&lt;m2&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;) Buffer_input(&lt;m1&gt;)
"];
T7 -> T22 [ label=<T9&gt;>];
T7 -> T17 [ label=<T3&gt;>];
T23 [ label="R0(1) S1_a(&lt;m2&gt;) S1_b(&lt;m2&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;) Buffer_input(&lt;m1&gt;)
"];
T7 -> T23 [ label=<T3&gt;>];
T8 -> T21 [ label=<T1&gt;>];
T8 -> T19 [ label=<T9&gt;>];
T24 [ label="S0(1) R_1(&lt;m3&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;) Buffer_input(&lt;m1&gt;)
"];
T8 -> T24 [ label=<T9&gt;>];
T8 -> T16 [ label=<T3&gt;>];
T25 [ label="R0(1) S1_a(&lt;m3&gt;) S1_b(&lt;m3&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;) Buffer_input(&lt;m1&gt;)
"];
T8 -> T25 [ label=<T3&gt;>];
T26 [ label="R0(1) S1_b(&lt;m2&gt;) S2_a(&lt;m2&gt;) Richiesta(&lt;m1&gt;+&lt;m3&gt;) Attesa(&lt;m2&gt;)
"];
T9 -> T26 [ label=<T4&gt;>];
T27 [ label="R0(1) S1_a(&lt;m2&gt;) S2_b(&lt;m2&gt;) Richiesta(&lt;m1&gt;+&lt;m3&gt;) Attesa(&lt;m2&gt;)
"];
T9 -> T27 [ label=<T5&gt;>];
T28 [ label="R0(1) S1_a(&lt;m2&gt;) S1_b(&lt;m2&gt;) Richiesta(&lt;m1&gt;) Attesa(&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m3&gt;)
"];
T9 -> T28 [ label=<T1&gt;>];
T9 -> T23 [ label=<T1&gt;>];
T29 [ label="S0(1) R_2(&lt;m2&gt;) Richiesta(&lt;m1&gt;+&lt;m3&gt;) Attesa(&lt;m2&gt;)
"];
T10 -> T29 [ label=<T8&gt;>];
T30 [ label="S0(1) R_1(&lt;m2&gt;) Richiesta(&lt;m1&gt;) Attesa(&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m3&gt;)
"];
T10 -> T30 [ label=<T1&gt;>];
T10 -> T22 [ label=<T1&gt;>];
T11 -> T21 [ label=<T1&gt;>];
T11 -> T30 [ label=<T9&gt;>];
T31 [ label="S0(1) R_1(&lt;m3&gt;) Richiesta(&lt;m1&gt;) Attesa(&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m2&gt;)
"];
T11 -> T31 [ label=<T9&gt;>];
T11 -> T28 [ label=<T3&gt;>];
T32 [ label="R0(1) S1_a(&lt;m3&gt;) S1_b(&lt;m3&gt;) Richiesta(&lt;m1&gt;) Attesa(&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m2&gt;)
"];
T11 -> T32 [ label=<T3&gt;>];
T33 [ label="R0(1) S1_b(&lt;m3&gt;) S2_a(&lt;m3&gt;) Richiesta(&lt;m1&gt;+&lt;m2&gt;) Attesa(&lt;m3&gt;)
"];
T12 -> T33 [ label=<T4&gt;>];
T34 [ label="R0(1) S1_a(&lt;m3&gt;) S2_b(&lt;m3&gt;) Richiesta(&lt;m1&gt;+&lt;m2&gt;) Attesa(&lt;m3&gt;)
"];
T12 -> T34 [ label=<T5&gt;>];
T12 -> T32 [ label=<T1&gt;>];
T12 -> T25 [ label=<T1&gt;>];
T35 [ label="S0(1) R_2(&lt;m3&gt;) Richiesta(&lt;m1&gt;+&lt;m2&gt;) Attesa(&lt;m3&gt;)
"];
T13 -> T35 [ label=<T8&gt;>];
T13 -> T31 [ label=<T1&gt;>];
T13 -> T24 [ label=<T1&gt;>];
T36 [ label="R0(1) S1_b(&lt;m1&gt;) S2_a(&lt;m1&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;) Buffer_input(&lt;m2&gt;)
"];
T14 -> T36 [ label=<T1&gt;>];
T37 [ label="R0(1) S1_b(&lt;m1&gt;) S2_a(&lt;m1&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;) Buffer_input(&lt;m3&gt;)
"];
T14 -> T37 [ label=<T1&gt;>];
T38 [ label="R0(1) S2_b(&lt;m1&gt;) S2_a(&lt;m1&gt;) Richiesta(&lt;m2&gt;+&lt;m3&gt;) Attesa(&lt;m1&gt;)
"];
T14 -> T38 [ label=<T5&gt;>];
T39 [ label="R0(1) S1_a(&lt;m1&gt;) S2_b(&lt;m1&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;) Buffer_input(&lt;m2&gt;)
"];
T15 -> T39 [ label=<T1&gt;>];
T40 [ label="R0(1) S1_a(&lt;m1&gt;) S2_b(&lt;m1&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;) Buffer_input(&lt;m3&gt;)
"];
T15 -> T40 [ label=<T1&gt;>];
T15 -> T38 [ label=<T4&gt;>];
T41 [ label="S1_a(&lt;m1&gt;) S1_b(&lt;m1&gt;) R_1(&lt;m3&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;)
"];
T16 -> T41 [ label=<T9&gt;>];
T42 [ label="R0(1) S1_a(&lt;m1&gt;) S1_b(&lt;m1&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m2&gt;+&lt;m3&gt;)
"];
T16 -> T42 [ label=<T1&gt;>];
T16 -> T40 [ label=<T5&gt;>];
T16 -> T37 [ label=<T4&gt;>];
T43 [ label="S1_a(&lt;m1&gt;) S1_b(&lt;m1&gt;) R_1(&lt;m2&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;)
"];
T17 -> T43 [ label=<T9&gt;>];
T17 -> T42 [ label=<T1&gt;>];
T17 -> T39 [ label=<T5&gt;>];
T17 -> T36 [ label=<T4&gt;>];
T44 [ label="S0(1) R3(1) Richiesta(&lt;m2&gt;+&lt;m3&gt;) Attesa(&lt;m1&gt;) Buffer_output(&lt;m1&gt;)
"];
T18 -> T44 [ label=<T7&gt;>];
T45 [ label="S0(1) R_2(&lt;m1&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;) Buffer_input(&lt;m2&gt;)
"];
T18 -> T45 [ label=<T1&gt;>];
T46 [ label="S0(1) R_2(&lt;m1&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;) Buffer_input(&lt;m3&gt;)
"];
T18 -> T46 [ label=<T1&gt;>];
T47 [ label="S1_a(&lt;m3&gt;) S1_b(&lt;m3&gt;) R_1(&lt;m1&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;)
"];
T19 -> T47 [ label=<T3&gt;>];
T48 [ label="S0(1) R_1(&lt;m1&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m2&gt;+&lt;m3&gt;)
"];
T19 -> T48 [ label=<T1&gt;>];
T19 -> T46 [ label=<T8&gt;>];
T49 [ label="S1_a(&lt;m2&gt;) S1_b(&lt;m2&gt;) R_1(&lt;m1&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;)
"];
T20 -> T49 [ label=<T3&gt;>];
T20 -> T48 [ label=<T1&gt;>];
T20 -> T45 [ label=<T8&gt;>];
T21 -> T42 [ label=<T3&gt;>];
T50 [ label="R0(1) S1_a(&lt;m2&gt;) S1_b(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m1&gt;+&lt;m3&gt;)
"];
T21 -> T50 [ label=<T3&gt;>];
T51 [ label="R0(1) S1_a(&lt;m3&gt;) S1_b(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m1&gt;+&lt;m2&gt;)
"];
T21 -> T51 [ label=<T3&gt;>];
T21 -> T48 [ label=<T9&gt;>];
T52 [ label="S0(1) R_1(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m1&gt;+&lt;m3&gt;)
"];
T21 -> T52 [ label=<T9&gt;>];
T53 [ label="S0(1) R_1(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m1&gt;+&lt;m2&gt;)
"];
T21 -> T53 [ label=<T9&gt;>];
T54 [ label="S0(1) R_2(&lt;m2&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;) Buffer_input(&lt;m1&gt;)
"];
T22 -> T54 [ label=<T8&gt;>];
T22 -> T43 [ label=<T3&gt;>];
T22 -> T52 [ label=<T1&gt;>];
T55 [ label="R0(1) S1_b(&lt;m2&gt;) S2_a(&lt;m2&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;) Buffer_input(&lt;m1&gt;)
"];
T23 -> T55 [ label=<T4&gt;>];
T56 [ label="R0(1) S1_a(&lt;m2&gt;) S2_b(&lt;m2&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;) Buffer_input(&lt;m1&gt;)
"];
T23 -> T56 [ label=<T5&gt;>];
T23 -> T49 [ label=<T9&gt;>];
T23 -> T50 [ label=<T1&gt;>];
T57 [ label="S0(1) R_2(&lt;m3&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;) Buffer_input(&lt;m1&gt;)
"];
T24 -> T57 [ label=<T8&gt;>];
T24 -> T41 [ label=<T3&gt;>];
T24 -> T53 [ label=<T1&gt;>];
T58 [ label="R0(1) S1_b(&lt;m3&gt;) S2_a(&lt;m3&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;) Buffer_input(&lt;m1&gt;)
"];
T25 -> T58 [ label=<T4&gt;>];
T59 [ label="R0(1) S1_a(&lt;m3&gt;) S2_b(&lt;m3&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;) Buffer_input(&lt;m1&gt;)
"];
T25 -> T59 [ label=<T5&gt;>];
T25 -> T47 [ label=<T9&gt;>];
T25 -> T51 [ label=<T1&gt;>];
T26 -> T55 [ label=<T1&gt;>];
T60 [ label="R0(1) S1_b(&lt;m2&gt;) S2_a(&lt;m2&gt;) Richiesta(&lt;m1&gt;) Attesa(&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m3&gt;)
"];
T26 -> T60 [ label=<T1&gt;>];
T61 [ label="R0(1) S2_b(&lt;m2&gt;) S2_a(&lt;m2&gt;) Richiesta(&lt;m1&gt;+&lt;m3&gt;) Attesa(&lt;m2&gt;)
"];
T26 -> T61 [ label=<T5&gt;>];
T27 -> T56 [ label=<T1&gt;>];
T62 [ label="R0(1) S1_a(&lt;m2&gt;) S2_b(&lt;m2&gt;) Richiesta(&lt;m1&gt;) Attesa(&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m3&gt;)
"];
T27 -> T62 [ label=<T1&gt;>];
T27 -> T61 [ label=<T4&gt;>];
T63 [ label="S1_a(&lt;m2&gt;) S1_b(&lt;m2&gt;) R_1(&lt;m3&gt;) Richiesta(&lt;m1&gt;) Attesa(&lt;m2&gt;+&lt;m3&gt;)
"];
T28 -> T63 [ label=<T9&gt;>];
T28 -> T50 [ label=<T1&gt;>];
T28 -> T62 [ label=<T5&gt;>];
T28 -> T60 [ label=<T4&gt;>];
T64 [ label="S0(1) R3(1) Richiesta(&lt;m1&gt;+&lt;m3&gt;) Attesa(&lt;m2&gt;) Buffer_output(&lt;m2&gt;)
"];
T29 -> T64 [ label=<T7&gt;>];
T29 -> T54 [ label=<T1&gt;>];
T65 [ label="S0(1) R_2(&lt;m2&gt;) Richiesta(&lt;m1&gt;) Attesa(&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m3&gt;)
"];
T29 -> T65 [ label=<T1&gt;>];
T66 [ label="S1_a(&lt;m3&gt;) S1_b(&lt;m3&gt;) R_1(&lt;m2&gt;) Richiesta(&lt;m1&gt;) Attesa(&lt;m2&gt;+&lt;m3&gt;)
"];
T30 -> T66 [ label=<T3&gt;>];
T30 -> T52 [ label=<T1&gt;>];
T30 -> T65 [ label=<T8&gt;>];
T67 [ label="S0(1) R_2(&lt;m3&gt;) Richiesta(&lt;m1&gt;) Attesa(&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m2&gt;)
"];
T31 -> T67 [ label=<T8&gt;>];
T31 -> T63 [ label=<T3&gt;>];
T31 -> T53 [ label=<T1&gt;>];
T68 [ label="R0(1) S1_b(&lt;m3&gt;) S2_a(&lt;m3&gt;) Richiesta(&lt;m1&gt;) Attesa(&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m2&gt;)
"];
T32 -> T68 [ label=<T4&gt;>];
T69 [ label="R0(1) S1_a(&lt;m3&gt;) S2_b(&lt;m3&gt;) Richiesta(&lt;m1&gt;) Attesa(&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m2&gt;)
"];
T32 -> T69 [ label=<T5&gt;>];
T32 -> T66 [ label=<T9&gt;>];
T32 -> T51 [ label=<T1&gt;>];
T33 -> T58 [ label=<T1&gt;>];
T33 -> T68 [ label=<T1&gt;>];
T70 [ label="R0(1) S2_b(&lt;m3&gt;) S2_a(&lt;m3&gt;) Richiesta(&lt;m1&gt;+&lt;m2&gt;) Attesa(&lt;m3&gt;)
"];
T33 -> T70 [ label=<T5&gt;>];
T34 -> T59 [ label=<T1&gt;>];
T34 -> T69 [ label=<T1&gt;>];
T34 -> T70 [ label=<T4&gt;>];
T71 [ label="S0(1) R3(1) Richiesta(&lt;m1&gt;+&lt;m2&gt;) Attesa(&lt;m3&gt;) Buffer_output(&lt;m3&gt;)
"];
T35 -> T71 [ label=<T7&gt;>];
T35 -> T57 [ label=<T1&gt;>];
T35 -> T67 [ label=<T1&gt;>];
T72 [ label="S1_b(&lt;m1&gt;) R_1(&lt;m2&gt;) S2_a(&lt;m1&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;)
"];
T36 -> T72 [ label=<T9&gt;>];
T73 [ label="R0(1) S2_b(&lt;m1&gt;) S2_a(&lt;m1&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;) Buffer_input(&lt;m2&gt;)
"];
T36 -> T73 [ label=<T5&gt;>];
T74 [ label="R0(1) S1_b(&lt;m1&gt;) S2_a(&lt;m1&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m2&gt;+&lt;m3&gt;)
"];
T36 -> T74 [ label=<T1&gt;>];
T75 [ label="S1_b(&lt;m1&gt;) R_1(&lt;m3&gt;) S2_a(&lt;m1&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;)
"];
T37 -> T75 [ label=<T9&gt;>];
T76 [ label="R0(1) S2_b(&lt;m1&gt;) S2_a(&lt;m1&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;) Buffer_input(&lt;m3&gt;)
"];
T37 -> T76 [ label=<T5&gt;>];
T37 -> T74 [ label=<T1&gt;>];
T77 [ label="R0(1) S3(1) Richiesta(&lt;m2&gt;+&lt;m3&gt;) Attesa(&lt;m1&gt;) Buffer_output(&lt;m1&gt;)
"];
T38 -> T77 [ label=<T6&gt;>];
T38 -> T76 [ label=<T1&gt;>];
T38 -> T73 [ label=<T1&gt;>];
T78 [ label="S1_a(&lt;m1&gt;) R_1(&lt;m2&gt;) S2_b(&lt;m1&gt;) Richiesta(&lt;m3&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;)
"];
T39 -> T78 [ label=<T9&gt;>];
T39 -> T73 [ label=<T4&gt;>];
T79 [ label="R0(1) S1_a(&lt;m1&gt;) S2_b(&lt;m1&gt;) Attesa(&lt;m1&gt;+&lt;m2&gt;+&lt;m3&gt;) Buffer_input(&lt;m2&gt;+&lt;m3&gt;)
"];
T39 -> T79 [ label=<T1&gt;>];
T80 [ label="S1_a(&lt;m1&gt;) R_1(&lt;m3&gt;) S2_b(&lt;m1&gt;) Richiesta(&lt;m2&gt;) Attesa(&lt;m1&gt;+&lt;m3&gt;)
"];
T40 -> T80 [ label=<T9&gt;>];
T40 -> T76 [ label=<T4&gt;>];
T40 -> T79 [ label=<T1&gt;>];
T81 [shape=none label="..."];
T41 -> T81 [ label=<T8&gt;>];
T41 -> T75 [ label=<T4&gt;>];
T41 -> T80 [ label=<T5&gt;>];
T82 [shape=none label="..."];
T41 -> T82 [ label=<T1&gt;>];
T42 -> T74 [ label=<T4&gt;>];
T42 -> T79 [ label=<T5&gt;>];
T83 [shape=none label="..."];
T42 -> T83 [ label=<T9&gt;>];
T82 [shape=none label="..."];
T42 -> T82 [ label=<T9&gt;>];
T84 [shape=none label="..."];
T43 -> T84 [ label=<T8&gt;>];
T43 -> T72 [ label=<T4&gt;>];
T43 -> T78 [ label=<T5&gt;>];
T83 [shape=none label="..."];
T43 -> T83 [ label=<T1&gt;>];
T85 [shape=none label="..."];
T44 -> T85 [ label=<Reset_r>];
T86 [shape=none label="..."];
T44 -> T86 [ label=<T2&gt;>];
T87 [shape=none label="..."];
T44 -> T87 [ label=<T1&gt;>];
T88 [shape=none label="..."];
T44 -> T88 [ label=<T1&gt;>];
T89 [shape=none label="..."];
T45 -> T89 [ label=<T3&gt;>];
T90 [shape=none label="..."];
T45 -> T90 [ label=<T1&gt;>];
T88 [shape=none label="..."];
T45 -> T88 [ label=<T7&gt;>];
T91 [shape=none label="..."];
T46 -> T91 [ label=<T3&gt;>];
T90 [shape=none label="..."];
T46 -> T90 [ label=<T1&gt;>];
T87 [shape=none label="..."];
T46 -> T87 [ label=<T7&gt;>];
T92 [shape=none label="..."];
T47 -> T92 [ label=<T4&gt;>];
T93 [shape=none label="..."];
T47 -> T93 [ label=<T5&gt;>];
T91 [shape=none label="..."];
T47 -> T91 [ label=<T8&gt;>];
T94 [shape=none label="..."];
T47 -> T94 [ label=<T1&gt;>];
T90 [shape=none label="..."];
T48 -> T90 [ label=<T8&gt;>];
T95 [shape=none label="..."];
T48 -> T95 [ label=<T3&gt;>];
T94 [shape=none label="..."];
T48 -> T94 [ label=<T3&gt;>];
T96 [shape=none label="..."];
T49 -> T96 [ label=<T4&gt;>];
T97 [shape=none label="..."];
T49 -> T97 [ label=<T5&gt;>];
T89 [shape=none label="..."];
T49 -> T89 [ label=<T8&gt;>];
T95 [shape=none label="..."];
T49 -> T95 [ label=<T1&gt;>];
T98 [shape=none label="..."];
T50 -> T98 [ label=<T4&gt;>];
T99 [shape=none label="..."];
T50 -> T99 [ label=<T5&gt;>];
T95 [shape=none label="..."];
T50 -> T95 [ label=<T9&gt;>];
T100 [shape=none label="..."];
T50 -> T100 [ label=<T9&gt;>];
T101 [shape=none label="..."];
T51 -> T101 [ label=<T4&gt;>];
T102 [shape=none label="..."];
T51 -> T102 [ label=<T5&gt;>];
T94 [shape=none label="..."];
T51 -> T94 [ label=<T9&gt;>];
T103 [shape=none label="..."];
T51 -> T103 [ label=<T9&gt;>];
T104 [shape=none label="..."];
T52 -> T104 [ label=<T8&gt;>];
T83 [shape=none label="..."];
T52 -> T83 [ label=<T3&gt;>];
T103 [shape=none label="..."];
T52 -> T103 [ label=<T3&gt;>];
T105 [shape=none label="..."];
T53 -> T105 [ label=<T8&gt;>];
T82 [shape=none label="..."];
T53 -> T82 [ label=<T3&gt;>];
T100 [shape=none label="..."];
T53 -> T100 [ label=<T3&gt;>];
T106 [shape=none label="..."];
T54 -> T106 [ label=<T7&gt;>];
T104 [shape=none label="..."];
T54 -> T104 [ label=<T1&gt;>];
T84 [shape=none label="..."];
T54 -> T84 [ label=<T3&gt;>];
T98 [shape=none label="..."];
T55 -> T98 [ label=<T1&gt;>];
T96 [shape=none label="..."];
T55 -> T96 [ label=<T9&gt;>];
T107 [shape=none label="..."];
T55 -> T107 [ label=<T5&gt;>];
T99 [shape=none label="..."];
T56 -> T99 [ label=<T1&gt;>];
T97 [shape=none label="..."];
T56 -> T97 [ label=<T9&gt;>];
T107 [shape=none label="..."];
T56 -> T107 [ label=<T4&gt;>];
T108 [shape=none label="..."];
T57 -> T108 [ label=<T7&gt;>];
T105 [shape=none label="..."];
T57 -> T105 [ label=<T1&gt;>];
T81 [shape=none label="..."];
T57 -> T81 [ label=<T3&gt;>];
T101 [shape=none label="..."];
T58 -> T101 [ label=<T1&gt;>];
T92 [shape=none label="..."];
T58 -> T92 [ label=<T9&gt;>];
T109 [shape=none label="..."];
T58 -> T109 [ label=<T5&gt;>];
T102 [shape=none label="..."];
T59 -> T102 [ label=<T1&gt;>];
T93 [shape=none label="..."];
T59 -> T93 [ label=<T9&gt;>];
T109 [shape=none label="..."];
T59 -> T109 [ label=<T4&gt;>];
T110 [shape=none label="..."];
T60 -> T110 [ label=<T9&gt;>];
T111 [shape=none label="..."];
T60 -> T111 [ label=<T5&gt;>];
T98 [shape=none label="..."];
T60 -> T98 [ label=<T1&gt;>];
T112 [shape=none label="..."];
T61 -> T112 [ label=<T6&gt;>];
T111 [shape=none label="..."];
T61 -> T111 [ label=<T1&gt;>];
T107 [shape=none label="..."];
T61 -> T107 [ label=<T1&gt;>];
T113 [shape=none label="..."];
T62 -> T113 [ label=<T9&gt;>];
T111 [shape=none label="..."];
T62 -> T111 [ label=<T4&gt;>];
T99 [shape=none label="..."];
T62 -> T99 [ label=<T1&gt;>];
T114 [shape=none label="..."];
T63 -> T114 [ label=<T8&gt;>];
T110 [shape=none label="..."];
T63 -> T110 [ label=<T4&gt;>];
T113 [shape=none label="..."];
T63 -> T113 [ label=<T5&gt;>];
T100 [shape=none label="..."];
T63 -> T100 [ label=<T1&gt;>];
T115 [shape=none label="..."];
T64 -> T115 [ label=<Reset_r>];
T116 [shape=none label="..."];
T64 -> T116 [ label=<T2&gt;>];
T117 [shape=none label="..."];
T64 -> T117 [ label=<T1&gt;>];
T106 [shape=none label="..."];
T64 -> T106 [ label=<T1&gt;>];
T118 [shape=none label="..."];
T65 -> T118 [ label=<T3&gt;>];
T104 [shape=none label="..."];
T65 -> T104 [ label=<T1&gt;>];
T117 [shape=none label="..."];
T65 -> T117 [ label=<T7&gt;>];
T119 [shape=none label="..."];
T66 -> T119 [ label=<T4&gt;>];
T120 [shape=none label="..."];
T66 -> T120 [ label=<T5&gt;>];
T118 [shape=none label="..."];
T66 -> T118 [ label=<T8&gt;>];
T103 [shape=none label="..."];
T66 -> T103 [ label=<T1&gt;>];
T121 [shape=none label="..."];
T67 -> T121 [ label=<T7&gt;>];
T105 [shape=none label="..."];
T67 -> T105 [ label=<T1&gt;>];
T114 [shape=none label="..."];
T67 -> T114 [ label=<T3&gt;>];
T101 [shape=none label="..."];
T68 -> T101 [ label=<T1&gt;>];
T119 [shape=none label="..."];
T68 -> T119 [ label=<T9&gt;>];
T122 [shape=none label="..."];
T68 -> T122 [ label=<T5&gt;>];
T102 [shape=none label="..."];
T69 -> T102 [ label=<T1&gt;>];
T120 [shape=none label="..."];
T69 -> T120 [ label=<T9&gt;>];
T122 [shape=none label="..."];
T69 -> T122 [ label=<T4&gt;>];
T123 [shape=none label="..."];
T70 -> T123 [ label=<T6&gt;>];
T122 [shape=none label="..."];
T70 -> T122 [ label=<T1&gt;>];
T109 [shape=none label="..."];
T70 -> T109 [ label=<T1&gt;>];
T124 [shape=none label="..."];
T71 -> T124 [ label=<Reset_r>];
T125 [shape=none label="..."];
T71 -> T125 [ label=<T2&gt;>];
T121 [shape=none label="..."];
T71 -> T121 [ label=<T1&gt;>];
T108 [shape=none label="..."];
T71 -> T108 [ label=<T1&gt;>];
T126 [shape=none label="..."];
T72 -> T126 [ label=<T8&gt;>];
T127 [shape=none label="..."];
T72 -> T127 [ label=<T1&gt;>];
T128 [shape=none label="..."];
T72 -> T128 [ label=<T5&gt;>];
T129 [shape=none label="..."];
T73 -> T129 [ label=<T6&gt;>];
T130 [shape=none label="..."];
T73 -> T130 [ label=<T1&gt;>];
T128 [shape=none label="..."];
T73 -> T128 [ label=<T9&gt;>];
T130 [shape=none label="..."];
T74 -> T130 [ label=<T5&gt;>];
T127 [shape=none label="..."];
T74 -> T127 [ label=<T9&gt;>];
T131 [shape=none label="..."];
T74 -> T131 [ label=<T9&gt;>];
T132 [shape=none label="..."];
T75 -> T132 [ label=<T8&gt;>];
T131 [shape=none label="..."];
T75 -> T131 [ label=<T1&gt;>];
T133 [shape=none label="..."];
T75 -> T133 [ label=<T5&gt;>];
T134 [shape=none label="..."];
T76 -> T134 [ label=<T6&gt;>];
T130 [shape=none label="..."];
T76 -> T130 [ label=<T1&gt;>];
T133 [shape=none label="..."];
T76 -> T133 [ label=<T9&gt;>];
T85 [shape=none label="..."];
T77 -> T85 [ label=<Reset_s>];
T135 [shape=none label="..."];
T77 -> T135 [ label=<T2&gt;>];
T129 [shape=none label="..."];
T77 -> T129 [ label=<T1&gt;>];
T134 [shape=none label="..."];
T77 -> T134 [ label=<T1&gt;>];
T136 [shape=none label="..."];
T78 -> T136 [ label=<T8&gt;>];
T137 [shape=none label="..."];
T78 -> T137 [ label=<T1&gt;>];
T128 [shape=none label="..."];
T78 -> T128 [ label=<T4&gt;>];
T130 [shape=none label="..."];
T79 -> T130 [ label=<T4&gt;>];
T137 [shape=none label="..."];
T79 -> T137 [ label=<T9&gt;>];
T138 [shape=none label="..."];
T79 -> T138 [ label=<T9&gt;>];
T139 [shape=none label="..."];
T80 -> T139 [ label=<T8&gt;>];
T138 [shape=none label="..."];
T80 -> T138 [ label=<T1&gt;>];
T133 [shape=none label="..."];
T80 -> T133 [ label=<T4&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">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 1024</td></tr></table>> ];
}

View file

@ -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 <m>
2
1 3 0 0 0.000000 0.000000 <m>
1 4 0 0 0.000000 0.000000 <m>
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 <m>
1
1 10 0 0 0.000000 0.000000 <m>
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 <m>
1
1 8 0 0 0.000000 0.000000 <m>
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 <m>
10.0 5.916666666666667
1 8 0 0 0.000000 0.000000 <m>
2
1 9 0 0
1 15 3 0 0.000000 0.000000 <m>
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 <m>
12.5 3.1666666666666665
12.5 1.8333333333333333
8.083333333333334 1.8333333333333333
1
1 5 0 0 0.000000 0.000000 <m>
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 <m>
1
1 6 0 0 0.000000 0.000000 <m>
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 <m>
2
1 7 0 0
1 15 3 0 0.000000 0.000000 <m>
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 <m>
2
1 12 1 0 0.000000 0.000000 <m>
5.0 3.6666666666666665
1 14 0 0 0.000000 0.000000 <m>
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 <m>
1 15 1 0 0.000000 0.000000 <m>
6.833333333333333 5.0
1
1 13 0 0 0.000000 0.000000 <m>
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 <m>
1
1 11 1 0 0.000000 0.000000 <m>
4.0 2.3333333333333335
0

View file

@ -0,0 +1 @@
0

View file

@ -0,0 +1,12 @@
1 5
0
0
0
1 1
0
0
0
0
0
0
0

View file

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

File diff suppressed because it is too large Load diff

View file

@ -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

View file

@ -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
))

View file

@ -0,0 +1,551 @@
digraph RG {
T1 [ label="S0(1) R0(1) Richiesta(&lt;Master_00&gt;)
|Master_00|=3
"];
T2 [ label="S0(1) R0(1) Richiesta(&lt;Master_01&gt;) Attesa(&lt;Master_00&gt;) Buffer_input(&lt;Master_00&gt;)
|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>> ];
}

View file

@ -0,0 +1 @@
*0*0*0*0*0*0*0*3*0*3*0

View file

@ -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 <m>
2
1 3 0 0 0.000000 0.000000 <m>
1 4 0 0 0.000000 0.000000 <m>
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 <m>
1
1 10 0 0 0.000000 0.000000 <m>
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 <m>
1
1 8 0 0 0.000000 0.000000 <m>
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 <m>
10.0 5.916666666666667
1 8 0 0 0.000000 0.000000 <m>
2
1 9 0 0
1 15 3 0 0.000000 0.000000 <m>
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 <m>
12.5 3.1666666666666665
12.5 1.8333333333333333
8.083333333333334 1.8333333333333333
1
1 5 0 0 0.000000 0.000000 <m>
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 <m>
1
1 6 0 0 0.000000 0.000000 <m>
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 <m>
2
1 7 0 0
1 15 3 0 0.000000 0.000000 <m>
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 <m>
2
1 12 1 0 0.000000 0.000000 <m>
5.0 3.6666666666666665
1 14 0 0 0.000000 0.000000 <m>
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 <m>
1 15 1 0 0.000000 0.000000 <m>
6.833333333333333 5.0
1
1 13 0 0 0.000000 0.000000 <m>
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 <m>
1
1 11 1 0 0.000000 0.000000 <m>
4.0 2.3333333333333335
0

View file

@ -0,0 +1 @@
1

View file

@ -0,0 +1,12 @@
1 5
0
0
0
1 1
0
0
0
0
0
0
0

View file

@ -0,0 +1,332 @@
S0(1)R0(1)Richiesta(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T1 (tangible)
[T1 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T2 # ordinary markings : 1
S0(1)R0(1)Attesa(1&lt;Master_00&gt;)Buffer_input(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T2 (tangible)
[T3 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T3 # ordinary markings : 1
R0(1)S1_a(1&lt;Master_00&gt;)S1_b(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T2 (tangible)
[T9 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T4 # ordinary markings : 1
S0(1)R_1(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T3 (tangible)
[T4 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T5 # ordinary markings : 1
R0(1)S1_b(1&lt;Master_00&gt;)S2_a(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T3 (tangible)
[T5 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T6 # ordinary markings : 1
R0(1)S1_a(1&lt;Master_00&gt;)S2_b(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T4 (tangible)
[T8 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T7 # ordinary markings : 1
S0(1)R_2(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T5 (tangible)
[T5 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T8 # ordinary markings : 1
R0(1)S2_b(1&lt;Master_00&gt;)S2_a(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T6 (tangible)
[T4 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T8 # ordinary markings : 1
R0(1)S2_b(1&lt;Master_00&gt;)S2_a(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T7 (tangible)
[T7 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T9 # ordinary markings : 1
S0(1)R3(1)Attesa(1&lt;Master_00&gt;)Buffer_output(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T8 (tangible)
[T6 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T10 # ordinary markings : 1
R0(1)S3(1)Attesa(1&lt;Master_00&gt;)Buffer_output(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T9 (tangible)
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T11 # ordinary markings : 1
S0(1)R0(1)Attesa(1&lt;Master_00&gt;)Buffer_output(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T9 (tangible)
[T2 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T12 # ordinary markings : 1
S0(1)R3(1)Elabora(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T10 (tangible)
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T11 # ordinary markings : 1
S0(1)R0(1)Attesa(1&lt;Master_00&gt;)Buffer_output(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T10 (tangible)
[T2 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T13 # ordinary markings : 1
R0(1)S3(1)Elabora(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T11 (tangible)
[T2 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T14 # ordinary markings : 1
S0(1)R0(1)Elabora(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T12 (tangible)
[T0 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T15 # ordinary markings : 1
S0(1)R3(1)Richiesta(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T12 (tangible)
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T14 # ordinary markings : 1
S0(1)R0(1)Elabora(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T13 (tangible)
[T0 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T16 # ordinary markings : 1
R0(1)S3(1)Richiesta(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T13 (tangible)
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T14 # ordinary markings : 1
S0(1)R0(1)Elabora(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T14 (tangible)
[T0 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T1 # ordinary markings : 1
S0(1)R0(1)Richiesta(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T15 (tangible)
[T1 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T17 # ordinary markings : 1
S0(1)R3(1)Attesa(1&lt;Master_00&gt;)Buffer_input(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T15 (tangible)
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T1 # ordinary markings : 1
S0(1)R0(1)Richiesta(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T16 (tangible)
[T1 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T18 # ordinary markings : 1
R0(1)S3(1)Attesa(1&lt;Master_00&gt;)Buffer_input(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T16 (tangible)
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T1 # ordinary markings : 1
S0(1)R0(1)Richiesta(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T17 (tangible)
[T3 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T19 # ordinary markings : 1
S1_a(1&lt;Master_00&gt;)S1_b(1&lt;Master_00&gt;)R3(1)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T17 (tangible)
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T2 # ordinary markings : 1
S0(1)R0(1)Attesa(1&lt;Master_00&gt;)Buffer_input(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T18 (tangible)
[T9 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T20 # ordinary markings : 1
R_1(1&lt;Master_00&gt;)S3(1)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T18 (tangible)
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T2 # ordinary markings : 1
S0(1)R0(1)Attesa(1&lt;Master_00&gt;)Buffer_input(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T19 (tangible)
[T4 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T21 # ordinary markings : 1
S1_b(1&lt;Master_00&gt;)R3(1)S2_a(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T19 (tangible)
[T5 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T22 # ordinary markings : 1
S1_a(1&lt;Master_00&gt;)R3(1)S2_b(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T19 (tangible)
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T3 # ordinary markings : 1
R0(1)S1_a(1&lt;Master_00&gt;)S1_b(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T20 (tangible)
[T8 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T23 # ordinary markings : 1
R_2(1&lt;Master_00&gt;)S3(1)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T20 (tangible)
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T4 # ordinary markings : 1
S0(1)R_1(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T21 (tangible)
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T5 # ordinary markings : 1
R0(1)S1_b(1&lt;Master_00&gt;)S2_a(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T21 (tangible)
[T5 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T24 # ordinary markings : 1
R3(1)S2_b(1&lt;Master_00&gt;)S2_a(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T22 (tangible)
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T6 # ordinary markings : 1
R0(1)S1_a(1&lt;Master_00&gt;)S2_b(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T22 (tangible)
[T4 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T24 # ordinary markings : 1
R3(1)S2_b(1&lt;Master_00&gt;)S2_a(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T23 (tangible)
[T7 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T25 # ordinary markings : 1
R3(1)S3(1)Attesa(1&lt;Master_00&gt;)Buffer_output(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T23 (tangible)
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T7 # ordinary markings : 1
S0(1)R_2(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T24 (tangible)
[T6 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T25 # ordinary markings : 1
R3(1)S3(1)Attesa(1&lt;Master_00&gt;)Buffer_output(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T24 (tangible)
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T8 # ordinary markings : 1
R0(1)S2_b(1&lt;Master_00&gt;)S2_a(1&lt;Master_00&gt;)Attesa(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T25 (tangible)
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T10 # ordinary markings : 1
R0(1)S3(1)Attesa(1&lt;Master_00&gt;)Buffer_output(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T25 (tangible)
[T2 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T26 # ordinary markings : 1
R3(1)S3(1)Elabora(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T25 (tangible)
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T9 # ordinary markings : 1
S0(1)R3(1)Attesa(1&lt;Master_00&gt;)Buffer_output(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T26 (tangible)
[T0 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T27 # ordinary markings : 1
R3(1)S3(1)Richiesta(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T26 (tangible)
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T12 # ordinary markings : 1
S0(1)R3(1)Elabora(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T26 (tangible)
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T13 # ordinary markings : 1
R0(1)S3(1)Elabora(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T27 (tangible)
[T1 (<ORDINARY INSTANCES : 1 - BINDING : m <-- Master_00
MARKING T28 # ordinary markings : 1
R3(1)S3(1)Attesa(1&lt;Master_00&gt;)Buffer_input(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T27 (tangible)
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T16 # ordinary markings : 1
R0(1)S3(1)Richiesta(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T27 (tangible)
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T15 # ordinary markings : 1
S0(1)R3(1)Richiesta(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T28 (tangible)
[Reset_s (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T17 # ordinary markings : 1
S0(1)R3(1)Attesa(1&lt;Master_00&gt;)Buffer_input(1&lt;Master_00&gt;)
|Master_00|=1
MARKING T28 (tangible)
[Reset_r (<ORDINARY INSTANCES : 1 - NO BINDING (non-colored)
MARKING T18 # ordinary markings : 1
R0(1)S3(1)Attesa(1&lt;Master_00&gt;)Buffer_input(1&lt;Master_00&gt;)
|Master_00|=1
***** Symbolic Reachability Graph *****
TANGIBLE MARKINGS : 28
VANISHING MARKINGS : 0
DEAD MARKINGS : 0
TOTAL MARKINGS : 28
***************************************
Ordinary tangible markings : 28
Ordinary vanishing markings : 0
Ordinary dead markings : 0
The initial marking is a home state
Time required ----------> 0
***************************************

File diff suppressed because it is too large Load diff

View file

@ -0,0 +1 @@
*0*1*0*0*1*2*1*2*0*0*0

View file

@ -1,9 +1,9 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?> <?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="ReteE" version="121"> <!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="ReteE" version="121">
<gspn name="CPN" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false" zoom="75"> <gspn name="CPN" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false">
<nodes> <nodes>
<place label-y="-2.0" marking="R1" name="S0" x="59.0" y="14.0"/> <place label-y="-2.0" marking="Sn" name="S0" x="59.0" y="14.0"/>
<place label-y="-2.0" marking="R2" name="R0" x="80.0" y="14.0"/> <place label-y="-2.0" marking="Rn" name="R0" x="80.0" y="14.0"/>
<place domain="Master" name="S1_a" x="53.0" y="20.0"/> <place domain="Master" name="S1_a" x="53.0" y="20.0"/>
<place domain="Master" name="S1_b" x="65.0" y="21.0"/> <place domain="Master" name="S1_b" x="65.0" y="21.0"/>
<place domain="Master" label-x="3.0" label-y="0.0" name="R_1" x="80.0" y="23.0"/> <place domain="Master" label-x="3.0" label-y="0.0" name="R_1" x="80.0" y="23.0"/>
@ -27,14 +27,14 @@
<place domain="Master" label-y="2.0" name="Elabora" x="29.0" y="34.0"/> <place domain="Master" label-y="2.0" name="Elabora" x="29.0" y="34.0"/>
<transition name="T2" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="29.55" y="29.0"/> <transition name="T2" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="29.55" y="29.0"/>
<transition name="T0" nservers-x="0.5" type="EXP" x="23.55" y="34.0"/> <transition name="T0" nservers-x="0.5" type="EXP" x="23.55" y="34.0"/>
<place domain="Master" label-y="-2.0" name="Buffer_input" x="49.0" y="18.0"/> <place domain="Master" label-y="-2.0" name="Buffer_input" x="40.0" y="18.0"/>
<place domain="Master" name="Buffer_output" x="44.0" y="35.0"/> <place domain="Master" name="Buffer_output" x="40.0" y="35.0"/>
<color-class definition="m{1..k}" name="Master" x="35.3125" y="8.0"/> <color-class definition="m{1..n}" name="Master" x="35.3125" y="8.0"/>
<color-var domain="Master" name="m" x="35.9375" y="10.0"/> <color-var domain="Master" name="m" x="35.9375" y="10.0"/>
<template last-binding="1" name="N" type="INTEGER" x="36.0" y="6.0"/> <template last-binding="1" name="N" type="INTEGER" x="36.0" y="6.0"/>
<template last-binding="2" name="R1" type="INTEGER" x="38.0" y="6.0"/> <template last-binding="2" name="Sn" type="INTEGER" x="38.0" y="6.0"/>
<template last-binding="2" name="R2" type="INTEGER" x="40.0" y="6.0"/> <template last-binding="2" name="Rn" type="INTEGER" x="40.0" y="6.0"/>
<template last-binding="3" name="k" type="INTEGER" x="79.0" y="35.0"/> <template last-binding="3" name="n" type="INTEGER" x="43.0" y="6.0"/>
</nodes> </nodes>
<edges> <edges>
<arc head="T3" kind="INPUT" tail="S0"/> <arc head="T3" kind="INPUT" tail="S0"/>
@ -83,26 +83,26 @@
<point x="24.0" y="14.0"/> <point x="24.0" y="14.0"/>
</arc> </arc>
<arc head="T2" kind="INPUT" mult="&lt;m&gt;" tail="Buffer_output"> <arc head="T2" kind="INPUT" mult="&lt;m&gt;" tail="Buffer_output">
<point x="45.0" y="30.0"/> <point x="41.0" y="30.0"/>
</arc> </arc>
<arc head="T9" kind="INPUT" mult="&lt;m&gt;" mult-k="1.2639648437500002" tail="Buffer_input"> <arc head="T9" kind="INPUT" mult="&lt;m&gt;" mult-k="1.2639648437500002" tail="Buffer_input">
<point x="50.0" y="11.0"/> <point x="48.5" y="11.0"/>
<point x="76.5" y="11.0"/> <point x="75.0" y="11.0"/>
<point x="76.5" y="19.0"/> <point x="75.0" y="19.0"/>
</arc> </arc>
<arc head="Buffer_output" kind="OUTPUT" mult="&lt;m&gt;" mult-k="2.28427734375" mult-x="-0.5402589824786475" mult-y="3.6422181113892265" tail="T7"> <arc head="Buffer_output" kind="OUTPUT" mult="&lt;m&gt;" mult-k="2.28427734375" mult-x="-0.5402589824786475" mult-y="3.6422181113892265" tail="T7">
<point x="76.5" y="36.0"/> <point x="76.5" y="36.0"/>
<point x="76.5" y="43.0"/> <point x="76.5" y="43.0"/>
<point x="45.0" y="42.5"/> <point x="41.0" y="43.0"/>
</arc> </arc>
</edges> </edges>
</gspn> </gspn>
<measures gspn-name="CPN" name="RG of CPN" rapid-type="BUILD_RG" simplified-UI="true"> <measures gspn-name="CPN" name="RG of CPN" rapid-type="BUILD_RG" simplified-UI="true">
<assignments> <assignments>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="N"/> <assignment bind-model="SINGLE_VALUE" single-val="3" type="INTEGER" varname="N"/>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="R1"/> <assignment bind-model="SINGLE_VALUE" single-val="3" type="INTEGER" varname="n"/>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="R2"/> <assignment bind-model="SINGLE_VALUE" single-val="2" type="INTEGER" varname="Rn"/>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="k"/> <assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="Sn"/>
</assignments> </assignments>
<greatspn/> <greatspn/>
<formulas> <formulas>
@ -110,17 +110,63 @@
<formula language="RG"/> <formula language="RG"/>
</formulas> </formulas>
</measures> </measures>
<measures gspn-name="CPN" name="SRG of CPN" rapid-type="BUILD_SYMRG" simplified-UI="true"> <measures gspn-name="CPN" log-uuid="1a3972fe-9e68-4c1c-a4e5-87f483887240" name="SRG of CPN" rapid-type="BUILD_SYMRG" simplified-UI="true">
<assignments> <assignments>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="N"/> <assignment bind-model="SINGLE_VALUE" single-val="3" type="INTEGER" varname="N"/>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="R1"/> <assignment bind-model="RANGE" range-from="3" range-step="1" range-to="6" type="INTEGER" varname="n"/>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="R2"/> <assignment bind-model="SINGLE_VALUE" single-val="2" type="INTEGER" varname="Rn"/>
<assignment bind-model="SINGLE_VALUE" single-val="6" type="INTEGER" varname="k"/> <assignment bind-model="SINGLE_VALUE" single-val="2" type="INTEGER" varname="Sn"/>
</assignments> </assignments>
<greatspn mode="SWN_SYM"/> <greatspn mode="SWN_SYM"/>
<formulas> <formulas>
<formula language="STAT"/> <formula language="STAT">
<result-table>
<stat-result name="STAT">
<bindings>
<binding name="Sn" value="2"/>
<binding name="Rn" value="2"/>
<binding name="N" value="3"/>
<binding name="n" value="3"/>
</bindings>
<stat key="build_time" value="332 seconds"/>
<stat key="home_state" value="True"/>
<stat key="num_dead_markings" value="0"/>
<stat key="num_ordinary_dead_markings" value="0"/>
<stat key="num_ordinary_tangible_markings" value="3151680"/>
<stat key="num_ordinary_vanishing_markings" value="0"/>
<stat key="num_tangible_markings" value="538380"/>
<stat key="num_vanishing_markings" value="0"/>
</stat-result>
<stat-result failure_reason="&lt;not computed&gt;" name="STAT" state="FAIL_COMPUTE">
<bindings>
<binding name="Sn" value="2"/>
<binding name="Rn" value="2"/>
<binding name="N" value="3"/>
<binding name="n" value="4"/>
</bindings>
</stat-result>
<stat-result name="STAT" state="NOT_YET_COMPUTED">
<bindings>
<binding name="Sn" value="2"/>
<binding name="Rn" value="2"/>
<binding name="N" value="3"/>
<binding name="n" value="5"/>
</bindings>
</stat-result>
<stat-result name="STAT" state="NOT_YET_COMPUTED">
<bindings>
<binding name="Sn" value="2"/>
<binding name="Rn" value="2"/>
<binding name="N" value="3"/>
<binding name="n" value="6"/>
</bindings>
</stat-result>
</result-table>
</formula>
<formula language="RG"/> <formula language="RG"/>
</formulas> </formulas>
</measures> </measures>
<resource-list>
<document-log uuid="1a3972fe-9e68-4c1c-a4e5-87f483887240">rO0ABXNyABRqYXZhLnV0aWwuTGlua2VkTGlzdAwpU11KYIgiAwAAeHB3BAAAAEJ0AKUbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vV05TUkcgIi9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzIuYi9SZXRlRS1TUkcgb2YgQ1BOLnNvbHV0aW9uL0NQTiIgLW1wYXIgTiAzIC1tcGFyIFJuIDIgLW1wYXIgU24gMiAtbXBhciBuIDMgIC1ndWktc3RhdAp0ACtPdmVycmlkaW5nIG1hcmtpbmcgcGFyYW1ldGVyIE4gdG8gdmFsdWUgMy4KdAAsT3ZlcnJpZGluZyBtYXJraW5nIHBhcmFtZXRlciBSbiB0byB2YWx1ZSAyLgp0ACxPdmVycmlkaW5nIG1hcmtpbmcgcGFyYW1ldGVyIFNuIHRvIHZhbHVlIDIuCnQAK092ZXJyaWRpbmcgbWFya2luZyBwYXJhbWV0ZXIgbiB0byB2YWx1ZSAzLgp0AGMtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLQp0AB1VU0UgOiBXTlNSRyBuZXRuYW1lIFstb11bLW1dCnQAAQp0AC1UbyBwbG90IHRoZSBnZW5lcmF0ZWQgUkcgaW4gR3JhcGh2aXogZm9ybWF0Ogp0ADQgICAgICBbLWRvdC1GIGZpbGVuYW1lLmRvdF0gWy1tYXgtZG90LW1hcmtpbmdzIG1heF0KdAA0UGFyYW1ldHJpYyBtYXJraW5nL3JhdGUgcGFyYW1ldGVycyBjYW4gYmUgc2V0IHdpdGg6CnQAOSAgICAgIFstbXBhciBwYXJhbV9uYW1lIHZhbHVlXSAgWy1ycGFyIHBhcmFtX25hbWUgdmFsdWVdCnQAYy0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tCnQAL1NlbmQgZmlsZXMgbmV0bmFtZS5uZXQsIC5kZWYgdG8gZS1tYWlsIGFkZHJlc3MKdAAqZ3JlYXRzcG5AZGkudW5pdG8uaXQgaWYgeW91IGZpbmQgYW55IGJ1Zy4KdABjLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0KdAABCnQAUVdBUk5JTkcgOiBhIGRlZmF1bHQgZHluYW1pYyBzdWJjbGFzcyBoYXMgYmVlbiBhZGRlZCBmb3Igc3RhdGljIHN1YmNsYXNzIE1hc3Rlcl8wCnQAC1QxMDAwMDAgVjAKdAALVDMwMDAwMCBWMAp0AAtUMzAwMDAwIFYwCnQAC1Q0MDAwMDAgVjAKdAABCnQAKiAqKioqKiBTeW1ib2xpYyBSZWFjaGFiaWxpdHkgR3JhcGggKioqKiogCnQAAQp0ABxUQU5HSUJMRSBNQVJLSU5HUyAgOiA1MzgzODAKdAAXVkFOSVNISU5HIE1BUktJTkdTIDogMAp0ABdERUFEIE1BUktJTkdTICAgICAgOiAwCnQAAQp0ABxUT1RBTCBNQVJLSU5HUyAgICAgOiA1MzgzODAKdAABCnQAKiAqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKiogCnQAAQp0ACVPcmRpbmFyeSB0YW5naWJsZSBtYXJraW5ncyA6IDMxNTE2ODAKdAAgT3JkaW5hcnkgdmFuaXNoaW5nIG1hcmtpbmdzIDogMAp0ABtPcmRpbmFyeSBkZWFkIG1hcmtpbmdzIDogMAp0ACRUaGUgaW5pdGlhbCBtYXJraW5nIGlzIGEgaG9tZSBzdGF0ZQp0AB5UaW1lIHJlcXVpcmVkIC0tLS0tLS0tLS0+IDMzMgp0AAEKdAAqICoqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKiAKdAAnG1swWBtbMzJtIFBST0NFU1MgRVhJVEVEIE5PUk1BTExZLhtbMG0KdAAFG1syWAp0AKUbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vV05TUkcgIi9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzIuYi9SZXRlRS1TUkcgb2YgQ1BOLnNvbHV0aW9uL0NQTiIgLW1wYXIgTiAzIC1tcGFyIFJuIDIgLW1wYXIgU24gMiAtbXBhciBuIDQgIC1ndWktc3RhdAp0ACtPdmVycmlkaW5nIG1hcmtpbmcgcGFyYW1ldGVyIE4gdG8gdmFsdWUgMy4KdAAsT3ZlcnJpZGluZyBtYXJraW5nIHBhcmFtZXRlciBSbiB0byB2YWx1ZSAyLgp0ACxPdmVycmlkaW5nIG1hcmtpbmcgcGFyYW1ldGVyIFNuIHRvIHZhbHVlIDIuCnQAK092ZXJyaWRpbmcgbWFya2luZyBwYXJhbWV0ZXIgbiB0byB2YWx1ZSA0Lgp0AGMtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLQp0AB1VU0UgOiBXTlNSRyBuZXRuYW1lIFstb11bLW1dCnQAAQp0AC1UbyBwbG90IHRoZSBnZW5lcmF0ZWQgUkcgaW4gR3JhcGh2aXogZm9ybWF0Ogp0ADQgICAgICBbLWRvdC1GIGZpbGVuYW1lLmRvdF0gWy1tYXgtZG90LW1hcmtpbmdzIG1heF0KdAA0UGFyYW1ldHJpYyBtYXJraW5nL3JhdGUgcGFyYW1ldGVycyBjYW4gYmUgc2V0IHdpdGg6CnQAOSAgICAgIFstbXBhciBwYXJhbV9uYW1lIHZhbHVlXSAgWy1ycGFyIHBhcmFtX25hbWUgdmFsdWVdCnQAYy0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tCnQAL1NlbmQgZmlsZXMgbmV0bmFtZS5uZXQsIC5kZWYgdG8gZS1tYWlsIGFkZHJlc3MKdAAqZ3JlYXRzcG5AZGkudW5pdG8uaXQgaWYgeW91IGZpbmQgYW55IGJ1Zy4KdABjLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0KdAABCnQAUVdBUk5JTkcgOiBhIGRlZmF1bHQgZHluYW1pYyBzdWJjbGFzcyBoYXMgYmVlbiBhZGRlZCBmb3Igc3RhdGljIHN1YmNsYXNzIE1hc3Rlcl8wCnQAC1QzMDAwMDAgVjAKdAALVDMwMDAwMCBWMAp0AAtUMzAwMDAwIFYwCnQAC1Q0MDAwMDAgVjAKdAAjG1sxWBtbMzFtIFBST0NFU1MgSU5URVJSVVBURUQuG1swbQp0AC0bWzFYG1szMW0gRElEIE5PVCBDT01QTEVURSBUSEUgU09MVVRJT04uG1swbQp4c3EAfgAAdwQAAABCc3IAEWphdmEubGFuZy5Cb29sZWFuzSBygNWc+u4CAAFaAAV2YWx1ZXhwAXEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZxAH4ARnEAfgBGcQB+AEZ4</document-log>
</resource-list>
</project> </project>

File diff suppressed because one or more lines are too long

View file

@ -0,0 +1,27 @@
|256
%
|
(Master c 0.5520833333333334 0.8333333333333334 (@c
u M1,M2
))
(M1 c 1.21875 0.8333333333333334 (@c
{m1,m3}
))
(M2 c 1.8854166666666667 0.8333333333333334 (@c
{m2}
))
(Slave c 0.5 0.5 (@c
u Slave1,Slave2
))
(Slave1 c 1.1666666666666667 0.5 (@c
{ID1}
))
(Slave2 c 1.8333333333333333 0.5 (@c
{ID2}
))
(m_0 m 10.0 2.0 (@m
R1<S Slave1>+R1<S Slave2>
))
(m_1 m 10.0 3.0 (@m
N S
))

View file

@ -0,0 +1,72 @@
|0|
|
f 3 11 0 8 0 0 0
N -7134 0.6354166666666666 0.4322916666666667 0
n -7134 0.9635416666666666 0.4322916666666667 0
R1 -7134 1.328125 0.4322916666666667 0
S0 -10007 6.0 2.0 5.434166666666666 1.6122916666666667 0 6.2 2.1666666666666665 Slave
S1_a 0 5.0 3.1666666666666665 3.7883333333333327 3.3622916666666662 0 5.2 3.3333333333333335 Master,Slave
S1_b 0 7.0 3.1666666666666665 5.694583333333333 3.3622916666666662 0 7.2 3.3333333333333335 Master,Slave
S2_b 0 7.0 4.833333333333333 4.944583333333333 4.528958333333333 0 7.2 5.0 Master,Slave
S3 0 6.0 6.0 5.434166666666666 6.195625 0 6.2 6.166666666666667 Slave
S2_a 0 5.0 4.833333333333333 4.454999999999999 4.778958333333333 0 5.2 5.0 Master,Slave
Richiesta -10008 1.8333333333333333 1.8333333333333333 0.6425000000000001 2.1122916666666667 0 2.033333333333333 2.0 Master
Attesa 0 1.8333333333333333 3.6666666666666665 0.9029166666666667 3.9456249999999997 0 2.033333333333333 3.8333333333333335 Master
Elabora 0 1.8333333333333333 5.333333333333333 0.8091666666666667 5.612291666666667 0 2.033333333333333 5.5 Master
Buffer_input 0 3.6666666666666665 2.6666666666666665 2.3299999999999996 2.278958333333333 0 3.8666666666666667 2.8333333333333335 Master
Buffer_output 0 3.6666666666666665 5.5 2.2362499999999996 5.695625 0 3.8666666666666667 5.666666666666667 Master
T3 1.0 0 0 2 0 6.0 2.6666666666666665 5.645833333333333 2.5572916666666665 6.083333333333333 2.734375 0 5.28125 0.8177083333333334 [(d(m) = M1 and id = ID1) or (d(m) = M2 and id = ID2)]
1 1 0 0 0.000000 0.000000 <id>
1 10 0 0 0.000000 0.000000 <m>
2
1 2 0 0 0.000000 0.000000 <m,id>
1 3 0 0 0.000000 0.000000 <m,id>
0
T4 1.0 0 0 1 0 5.0 4.0 5.3125 4.057291666666667 5.083333333333333 4.067708333333333 0
1 2 0 0 0.000000 0.000000 <m,id>
1
1 6 0 0 0.000000 0.000000 <m,id>
0
T5 1.0 0 0 1 0 7.0 4.0 6.645833333333333 4.057291666666667 7.083333333333333 4.067708333333333 0
1 3 0 0 0.000000 0.000000 <m,id>
1
1 4 0 0 0.000000 0.000000 <m,id>
0
T6 1.0 0 0 2 0 6.0 5.5 5.979166666666667 5.223958333333333 6.083333333333333 5.567708333333333 0
1 6 1 0 0.000000 0.000000 <m,id>
6.0 5.416666666666667
1 4 0 0 0.000000 0.000000 <m,id>
2
1 5 0 0 0.000000 0.000000 <id>
1 11 3 0 0.000000 0.000000 <m>
4.666666666666667 5.5
4.666666666666667 5.5
4.75 5.5
0
Reset_s 1.0 0 0 1 1 6.833333333333333 2.0 6.640625 1.8072916666666667 6.916666666666667 2.0677083333333335 0
1 5 2 0 0.000000 0.000000 <id>
8.0 2.0833333333333335
8.0 6.0
1
1 1 0 0 0.000000 0.000000 <id>
0
T1 1.0 0 0 1 0 1.8333333333333333 2.6666666666666665 1.9791666666666667 2.390625 1.9166666666666667 2.734375 0
1 7 0 0 0.000000 0.000000 <m>
2
1 8 1 0 0.000000 0.000000 <m>
1.8333333333333333 3.1666666666666665
1 10 0 0 0.000000 0.000000 <m>
0
T2 1.0 0 0 2 0 1.8333333333333333 4.5 1.8125 4.307291666666667 1.9166666666666667 4.567708333333333 0
1 8 0 0 0.000000 0.000000 <m>
1 11 1 0 0.000000 0.000000 <m>
3.6666666666666665 4.5
1
1 9 0 0 0.000000 0.000000 <m>
0
T0 1.0 0 0 1 1 0.8333333333333334 5.333333333333333 0.8125 5.140625 0.9166666666666666 5.401041666666667 0
1 9 0 0 0.000000 0.000000 <m>
1
1 7 1 0 0.000000 0.000000 <m>
0.8333333333333334 1.8333333333333333
0

View file

@ -0,0 +1,79 @@
# 1 "/home/user/UNITO/anno3/vpc/consegne/2.b/ReteF-RG of CPN.solution/CPN.ntp"
# 1 "<built-in>"
# 1 "<command-line>"
# 31 "<command-line>"
# 1 "/usr/include/stdc-predef.h" 1 3 4
# 32 "<command-line>" 2
# 1 "/home/user/UNITO/anno3/vpc/consegne/2.b/ReteF-RG of CPN.solution/CPN.ntp"
|0|
|
f 3 11 0 8 0 0 0
N -7134 0.6354166666666666 0.4322916666666667 0
n -7134 0.9635416666666666 0.4322916666666667 0
R1 -7134 1.328125 0.4322916666666667 0
S0 -10007 6.0 2.0 5.434166666666666 1.6122916666666667 0 6.2 2.1666666666666665 Slave
S1_a 0 5.0 3.1666666666666665 3.7883333333333327 3.3622916666666662 0 5.2 3.3333333333333335 Master,Slave
S1_b 0 7.0 3.1666666666666665 5.694583333333333 3.3622916666666662 0 7.2 3.3333333333333335 Master,Slave
S2_b 0 7.0 4.833333333333333 4.944583333333333 4.528958333333333 0 7.2 5.0 Master,Slave
S3 0 6.0 6.0 5.434166666666666 6.195625 0 6.2 6.166666666666667 Slave
S2_a 0 5.0 4.833333333333333 4.454999999999999 4.778958333333333 0 5.2 5.0 Master,Slave
Richiesta -10008 1.8333333333333333 1.8333333333333333 0.6425000000000001 2.1122916666666667 0 2.033333333333333 2.0 Master
Attesa 0 1.8333333333333333 3.6666666666666665 0.9029166666666667 3.9456249999999997 0 2.033333333333333 3.8333333333333335 Master
Elabora 0 1.8333333333333333 5.333333333333333 0.8091666666666667 5.612291666666667 0 2.033333333333333 5.5 Master
Buffer_input 0 3.6666666666666665 2.6666666666666665 2.3299999999999996 2.278958333333333 0 3.8666666666666667 2.8333333333333335 Master
Buffer_output 0 3.6666666666666665 5.5 2.2362499999999996 5.695625 0 3.8666666666666667 5.666666666666667 Master
T3 1.0 0 0 2 0 6.0 2.6666666666666665 5.645833333333333 2.5572916666666665 6.083333333333333 2.734375 0 5.28125 0.8177083333333334 [(d(m) = M1 and id = ID1) or (d(m) = M2 and id = ID2)]
1 1 0 0 0.000000 0.000000 <id>
1 10 0 0 0.000000 0.000000 <m>
2
1 2 0 0 0.000000 0.000000 <m,id>
1 3 0 0 0.000000 0.000000 <m,id>
0
T4 1.0 0 0 1 0 5.0 4.0 5.3125 4.057291666666667 5.083333333333333 4.067708333333333 0
1 2 0 0 0.000000 0.000000 <m,id>
1
1 6 0 0 0.000000 0.000000 <m,id>
0
T5 1.0 0 0 1 0 7.0 4.0 6.645833333333333 4.057291666666667 7.083333333333333 4.067708333333333 0
1 3 0 0 0.000000 0.000000 <m,id>
1
1 4 0 0 0.000000 0.000000 <m,id>
0
T6 1.0 0 0 2 0 6.0 5.5 5.979166666666667 5.223958333333333 6.083333333333333 5.567708333333333 0
1 6 1 0 0.000000 0.000000 <m,id>
6.0 5.416666666666667
1 4 0 0 0.000000 0.000000 <m,id>
2
1 5 0 0 0.000000 0.000000 <id>
1 11 3 0 0.000000 0.000000 <m>
4.666666666666667 5.5
4.666666666666667 5.5
4.75 5.5
0
Reset_s 1.0 0 0 1 1 6.833333333333333 2.0 6.640625 1.8072916666666667 6.916666666666667 2.0677083333333335 0
1 5 2 0 0.000000 0.000000 <id>
8.0 2.0833333333333335
8.0 6.0
1
1 1 0 0 0.000000 0.000000 <id>
0
T1 1.0 0 0 1 0 1.8333333333333333 2.6666666666666665 1.9791666666666667 2.390625 1.9166666666666667 2.734375 0
1 7 0 0 0.000000 0.000000 <m>
2
1 8 1 0 0.000000 0.000000 <m>
1.8333333333333333 3.1666666666666665
1 10 0 0 0.000000 0.000000 <m>
0
T2 1.0 0 0 2 0 1.8333333333333333 4.5 1.8125 4.307291666666667 1.9166666666666667 4.567708333333333 0
1 8 0 0 0.000000 0.000000 <m>
1 11 1 0 0.000000 0.000000 <m>
3.6666666666666665 4.5
1
1 9 0 0 0.000000 0.000000 <m>
0
T0 1.0 0 0 1 1 0.8333333333333334 5.333333333333333 0.8125 5.140625 0.9166666666666666 5.401041666666667 0
1 9 0 0 0.000000 0.000000 <m>
1
1 7 1 0 0.000000 0.000000 <m>
0.8333333333333334 1.8333333333333333
0

View file

@ -0,0 +1,3 @@
0*999*
6*0*0*0*0*1*0*0*1*0*1*0**0*0*0*0*1*0*0*1*0*1*0**5*
7*1*0*0*0*0*0*0*1*0*1*0**1*0*0*0*0*0*0*1*0*1*0**1*

View file

@ -0,0 +1,8 @@
1 3
1 3
2 4 6
1 8
2 6 8
1 7
1 5
2 1 2

View file

@ -0,0 +1,27 @@
|256
%
|
(Master c 0.5520833333333334 0.8333333333333334 (@c
u M1,M2
))
(M1 c 1.21875 0.8333333333333334 (@c
{m1,m3}
))
(M2 c 1.8854166666666667 0.8333333333333334 (@c
{m2}
))
(Slave c 3.6666666666666665 1.1666666666666667 (@c
u Slave1,Slave2
))
(Slave1 c 4.333333333333333 1.1666666666666667 (@c
ID{10-n}
))
(Slave2 c 5.0 1.1666666666666667 (@c
ID{20-n1}
))
(m_0 m 10.0 2.0 (@m
R1<S Slave1>+R1<S Slave2>
))
(m_1 m 10.0 3.0 (@m
N S
))

View file

@ -0,0 +1,682 @@
digraph RG {
T1 [ label="S0(3&lt;Slave10&gt;+3&lt;Slave21&gt;) Richiesta(&lt;M10&gt;+&lt;M22&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T2 [ label="S0(3&lt;Slave10&gt;+3&lt;Slave21&gt;) Richiesta(&lt;M11&gt;+&lt;M22&gt;) Attesa(&lt;M10&gt;) Buffer_input(&lt;M10&gt;)
|M11|=1 |M10|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T1 -> T2 [ label=<T1&gt;>];
T3 [ label="S0(3&lt;Slave10&gt;+3&lt;Slave21&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M22&gt;) Buffer_input(&lt;M22&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T1 -> T3 [ label=<T1&gt;>];
T4 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;) S1_b(&lt;M11,Slave10&gt;) Richiesta(&lt;M10&gt;+&lt;M22&gt;) Attesa(&lt;M11&gt;)
|M11|=1 |M10|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T2 -> T4 [ label=<T55&gt;>];
T5 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;) S1_b(&lt;M10,Slave21&gt;) Richiesta(&lt;M11&gt;+&lt;M22&gt;) Attesa(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T2 -> T5 [ label=<T55&gt;>];
T6 [ label="S0(3&lt;Slave10&gt;+3&lt;Slave21&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;) Buffer_input(&lt;M10&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T2 -> T6 [ label=<T1&gt;>];
T7 [ label="S0(3&lt;Slave10&gt;+3&lt;Slave21&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T2 -> T7 [ label=<T1&gt;>];
T8 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M22,Slave10&gt;) S1_b(&lt;M22,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M22&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T3 -> T8 [ label=<T55&gt;>];
T9 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M22,Slave21&gt;) S1_b(&lt;M22,Slave21&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M22&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T3 -> T9 [ label=<T55&gt;>];
T3 -> T7 [ label=<T1&gt;>];
T10 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_b(&lt;M11,Slave10&gt;) S2_a(&lt;M11,Slave10&gt;) Richiesta(&lt;M10&gt;+&lt;M22&gt;) Attesa(&lt;M11&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T4 -> T10 [ label=<T4&gt;>];
T11 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;) S2_b(&lt;M11,Slave10&gt;) Richiesta(&lt;M10&gt;+&lt;M22&gt;) Attesa(&lt;M11&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T4 -> T11 [ label=<T5&gt;>];
T12 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;) S1_b(&lt;M11,Slave10&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;) Buffer_input(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T4 -> T12 [ label=<T1&gt;>];
T13 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;) S1_b(&lt;M11,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;) Buffer_input(&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T4 -> T13 [ label=<T1&gt;>];
T14 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_b(&lt;M10,Slave21&gt;) S2_a(&lt;M10,Slave21&gt;) Richiesta(&lt;M11&gt;+&lt;M22&gt;) Attesa(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T5 -> T14 [ label=<T4&gt;>];
T15 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;) S2_b(&lt;M10,Slave21&gt;) Richiesta(&lt;M11&gt;+&lt;M22&gt;) Attesa(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T5 -> T15 [ label=<T5&gt;>];
T16 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;) S1_b(&lt;M10,Slave21&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;) Buffer_input(&lt;M11&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T5 -> T16 [ label=<T1&gt;>];
T17 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;) S1_b(&lt;M10,Slave21&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T5 -> T17 [ label=<T1&gt;>];
T18 [ label="S0(3&lt;Slave10&gt;+3&lt;Slave21&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;+&lt;M22&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T6 -> T18 [ label=<T1&gt;>];
T6 -> T12 [ label=<T55&gt;>];
T6 -> T16 [ label=<T55&gt;>];
T7 -> T18 [ label=<T1&gt;>];
T19 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M22,Slave10&gt;) S1_b(&lt;M22,Slave10&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T7 -> T19 [ label=<T55&gt;>];
T20 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M22,Slave21&gt;) S1_b(&lt;M22,Slave21&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T7 -> T20 [ label=<T55&gt;>];
T7 -> T13 [ label=<T55&gt;>];
T7 -> T17 [ label=<T55&gt;>];
T21 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_b(&lt;M22,Slave10&gt;) S2_a(&lt;M22,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M22&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T8 -> T21 [ label=<T4&gt;>];
T22 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M22,Slave10&gt;) S2_b(&lt;M22,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M22&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T8 -> T22 [ label=<T5&gt;>];
T8 -> T19 [ label=<T1&gt;>];
T23 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_b(&lt;M22,Slave21&gt;) S2_a(&lt;M22,Slave21&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M22&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T9 -> T23 [ label=<T4&gt;>];
T24 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M22,Slave21&gt;) S2_b(&lt;M22,Slave21&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M22&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T9 -> T24 [ label=<T5&gt;>];
T9 -> T20 [ label=<T1&gt;>];
T25 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_b(&lt;M11,Slave10&gt;) S2_a(&lt;M11,Slave10&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;) Buffer_input(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T10 -> T25 [ label=<T1&gt;>];
T26 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_b(&lt;M11,Slave10&gt;) S2_a(&lt;M11,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;) Buffer_input(&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T10 -> T26 [ label=<T1&gt;>];
T27 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S2_b(&lt;M11,Slave10&gt;) S2_a(&lt;M11,Slave10&gt;) Richiesta(&lt;M10&gt;+&lt;M22&gt;) Attesa(&lt;M11&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T10 -> T27 [ label=<T5&gt;>];
T28 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;) S2_b(&lt;M11,Slave10&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;) Buffer_input(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T11 -> T28 [ label=<T1&gt;>];
T29 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;) S2_b(&lt;M11,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;) Buffer_input(&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T11 -> T29 [ label=<T1&gt;>];
T11 -> T27 [ label=<T4&gt;>];
T30 [ label="S0(&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M10,Slave10&gt;) S1_b(&lt;M10,Slave10&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T12 -> T30 [ label=<T55&gt;>];
T31 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;+&lt;M11,Slave10&gt;) S1_b(&lt;M10,Slave21&gt;+&lt;M11,Slave10&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T12 -> T31 [ label=<T55&gt;>];
T32 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;) S1_b(&lt;M11,Slave10&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T12 -> T32 [ label=<T1&gt;>];
T12 -> T28 [ label=<T5&gt;>];
T12 -> T25 [ label=<T4&gt;>];
T33 [ label="S0(&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;+&lt;M22,Slave10&gt;) S1_b(&lt;M11,Slave10&gt;+&lt;M22,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T13 -> T33 [ label=<T55&gt;>];
T34 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;+&lt;M22,Slave21&gt;) S1_b(&lt;M11,Slave10&gt;+&lt;M22,Slave21&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T13 -> T34 [ label=<T55&gt;>];
T13 -> T32 [ label=<T1&gt;>];
T13 -> T29 [ label=<T5&gt;>];
T13 -> T26 [ label=<T4&gt;>];
T35 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_b(&lt;M10,Slave21&gt;) S2_a(&lt;M10,Slave21&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;) Buffer_input(&lt;M11&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T14 -> T35 [ label=<T1&gt;>];
T36 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_b(&lt;M10,Slave21&gt;) S2_a(&lt;M10,Slave21&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T14 -> T36 [ label=<T1&gt;>];
T37 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S2_b(&lt;M10,Slave21&gt;) S2_a(&lt;M10,Slave21&gt;) Richiesta(&lt;M11&gt;+&lt;M22&gt;) Attesa(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T14 -> T37 [ label=<T5&gt;>];
T38 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;) S2_b(&lt;M10,Slave21&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;) Buffer_input(&lt;M11&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T15 -> T38 [ label=<T1&gt;>];
T39 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;) S2_b(&lt;M10,Slave21&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T15 -> T39 [ label=<T1&gt;>];
T15 -> T37 [ label=<T4&gt;>];
T16 -> T31 [ label=<T55&gt;>];
T40 [ label="S0(3&lt;Slave10&gt;+&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;) S1_b(&lt;M10,Slave21&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T16 -> T40 [ label=<T55&gt;>];
T41 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;) S1_b(&lt;M10,Slave21&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;+&lt;M22&gt;) Buffer_input(&lt;M11&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T16 -> T41 [ label=<T1&gt;>];
T16 -> T38 [ label=<T5&gt;>];
T16 -> T35 [ label=<T4&gt;>];
T42 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;+&lt;M22,Slave10&gt;) S1_b(&lt;M10,Slave21&gt;+&lt;M22,Slave10&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T17 -> T42 [ label=<T55&gt;>];
T43 [ label="S0(3&lt;Slave10&gt;+&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;+&lt;M22,Slave21&gt;) S1_b(&lt;M10,Slave21&gt;+&lt;M22,Slave21&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T17 -> T43 [ label=<T55&gt;>];
T17 -> T41 [ label=<T1&gt;>];
T17 -> T39 [ label=<T5&gt;>];
T17 -> T36 [ label=<T4&gt;>];
T44 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M22,Slave10&gt;) S1_b(&lt;M22,Slave10&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T18 -> T44 [ label=<T55&gt;>];
T45 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M22,Slave21&gt;) S1_b(&lt;M22,Slave21&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T18 -> T45 [ label=<T55&gt;>];
T18 -> T32 [ label=<T55&gt;>];
T18 -> T41 [ label=<T55&gt;>];
T46 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_b(&lt;M22,Slave10&gt;) S2_a(&lt;M22,Slave10&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T19 -> T46 [ label=<T4&gt;>];
T47 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M22,Slave10&gt;) S2_b(&lt;M22,Slave10&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T19 -> T47 [ label=<T5&gt;>];
T19 -> T33 [ label=<T55&gt;>];
T19 -> T42 [ label=<T55&gt;>];
T19 -> T44 [ label=<T1&gt;>];
T48 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_b(&lt;M22,Slave21&gt;) S2_a(&lt;M22,Slave21&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T20 -> T48 [ label=<T4&gt;>];
T49 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M22,Slave21&gt;) S2_b(&lt;M22,Slave21&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T20 -> T49 [ label=<T5&gt;>];
T20 -> T34 [ label=<T55&gt;>];
T20 -> T43 [ label=<T55&gt;>];
T20 -> T45 [ label=<T1&gt;>];
T21 -> T46 [ label=<T1&gt;>];
T50 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S2_b(&lt;M22,Slave10&gt;) S2_a(&lt;M22,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M22&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T21 -> T50 [ label=<T5&gt;>];
T22 -> T47 [ label=<T1&gt;>];
T22 -> T50 [ label=<T4&gt;>];
T23 -> T48 [ label=<T1&gt;>];
T51 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S2_b(&lt;M22,Slave21&gt;) S2_a(&lt;M22,Slave21&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M22&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T23 -> T51 [ label=<T5&gt;>];
T24 -> T49 [ label=<T1&gt;>];
T24 -> T51 [ label=<T4&gt;>];
T52 [ label="S0(&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;) S1_b(&lt;M10,Slave10&gt;+&lt;M11,Slave10&gt;) S2_a(&lt;M10,Slave10&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;)
|M11|=1 |M10|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T25 -> T52 [ label=<T55&gt;>];
T53 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;) S1_b(&lt;M10,Slave21&gt;+&lt;M11,Slave10&gt;) S2_a(&lt;M11,Slave10&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T25 -> T53 [ label=<T55&gt;>];
T54 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S2_b(&lt;M11,Slave10&gt;) S2_a(&lt;M11,Slave10&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;) Buffer_input(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T25 -> T54 [ label=<T5&gt;>];
T55 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_b(&lt;M11,Slave10&gt;) S2_a(&lt;M11,Slave10&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T25 -> T55 [ label=<T1&gt;>];
T56 [ label="S0(&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M22,Slave10&gt;) S1_b(&lt;M11,Slave10&gt;+&lt;M22,Slave10&gt;) S2_a(&lt;M11,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T26 -> T56 [ label=<T55&gt;>];
T57 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M22,Slave21&gt;) S1_b(&lt;M11,Slave10&gt;+&lt;M22,Slave21&gt;) S2_a(&lt;M11,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T26 -> T57 [ label=<T55&gt;>];
T58 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S2_b(&lt;M11,Slave10&gt;) S2_a(&lt;M11,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;) Buffer_input(&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T26 -> T58 [ label=<T5&gt;>];
T26 -> T55 [ label=<T1&gt;>];
T59 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S3(&lt;Slave10&gt;) Richiesta(&lt;M11&gt;+&lt;M22&gt;) Attesa(&lt;M10&gt;) Buffer_output(&lt;M10&gt;)
|M11|=1 |M10|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T27 -> T59 [ label=<T6&gt;>];
T27 -> T54 [ label=<T1&gt;>];
T27 -> T58 [ label=<T1&gt;>];
T60 [ label="S0(&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M10,Slave10&gt;+&lt;M11,Slave10&gt;) S1_b(&lt;M11,Slave10&gt;) S2_b(&lt;M10,Slave10&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;)
|M11|=1 |M10|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T28 -> T60 [ label=<T55&gt;>];
T61 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;+&lt;M11,Slave10&gt;) S1_b(&lt;M10,Slave21&gt;) S2_b(&lt;M11,Slave10&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T28 -> T61 [ label=<T55&gt;>];
T28 -> T54 [ label=<T4&gt;>];
T62 [ label="S0(2&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;) S2_b(&lt;M11,Slave10&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T28 -> T62 [ label=<T1&gt;>];
T63 [ label="S0(&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;+&lt;M22,Slave10&gt;) S1_b(&lt;M22,Slave10&gt;) S2_b(&lt;M11,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T29 -> T63 [ label=<T55&gt;>];
T64 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;+&lt;M22,Slave21&gt;) S1_b(&lt;M22,Slave21&gt;) S2_b(&lt;M11,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T29 -> T64 [ label=<T55&gt;>];
T29 -> T58 [ label=<T4&gt;>];
T29 -> T62 [ label=<T1&gt;>];
T30 -> T52 [ label=<T4&gt;>];
T30 -> T60 [ label=<T5&gt;>];
T65 [ label="S0(&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M10,Slave10&gt;) S1_b(&lt;M10,Slave10&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M22&gt;)
|M10|=2 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T30 -> T65 [ label=<T1&gt;>];
T66 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;) S1_b(&lt;M10,Slave21&gt;+&lt;M11,Slave10&gt;) S2_a(&lt;M10,Slave21&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T31 -> T66 [ label=<T4&gt;>];
T31 -> T53 [ label=<T4&gt;>];
T67 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;+&lt;M11,Slave10&gt;) S1_b(&lt;M11,Slave10&gt;) S2_b(&lt;M10,Slave21&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T31 -> T67 [ label=<T5&gt;>];
T31 -> T61 [ label=<T5&gt;>];
T68 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M10,Slave21&gt;+&lt;M11,Slave10&gt;) S1_b(&lt;M10,Slave21&gt;+&lt;M11,Slave10&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;+&lt;M22&gt;) Buffer_input(&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T31 -> T68 [ label=<T1&gt;>];
T32 -> T55 [ label=<T4&gt;>];
T32 -> T62 [ label=<T5&gt;>];
T69 [ label="S0(&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;+&lt;M22,Slave10&gt;) S1_b(&lt;M11,Slave10&gt;+&lt;M22,Slave10&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T32 -> T69 [ label=<T55&gt;>];
T70 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;+&lt;M22,Slave21&gt;) S1_b(&lt;M11,Slave10&gt;+&lt;M22,Slave21&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;+&lt;M22&gt;) Buffer_input(&lt;M10&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T32 -> T70 [ label=<T55&gt;>];
T32 -> T65 [ label=<T55&gt;>];
T32 -> T68 [ label=<T55&gt;>];
T33 -> T56 [ label=<T4&gt;>];
T71 [ label="S0(&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;) S1_b(&lt;M11,Slave10&gt;+&lt;M22,Slave10&gt;) S2_a(&lt;M22,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T33 -> T71 [ label=<T4&gt;>];
T33 -> T63 [ label=<T5&gt;>];
T72 [ label="S0(&lt;Slave10&gt;+3&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;+&lt;M22,Slave10&gt;) S1_b(&lt;M11,Slave10&gt;) S2_b(&lt;M22,Slave10&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T33 -> T72 [ label=<T5&gt;>];
T33 -> T69 [ label=<T1&gt;>];
T34 -> T57 [ label=<T4&gt;>];
T73 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;) S1_b(&lt;M11,Slave10&gt;+&lt;M22,Slave21&gt;) S2_a(&lt;M22,Slave21&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T34 -> T73 [ label=<T4&gt;>];
T34 -> T64 [ label=<T5&gt;>];
T74 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M11,Slave10&gt;+&lt;M22,Slave21&gt;) S1_b(&lt;M11,Slave10&gt;) S2_b(&lt;M22,Slave21&gt;) Richiesta(&lt;M10&gt;) Attesa(&lt;M11&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T34 -> T74 [ label=<T5&gt;>];
T34 -> T70 [ label=<T1&gt;>];
T35 -> T66 [ label=<T55&gt;>];
T75 [ label="S0(3&lt;Slave10&gt;+&lt;Slave21&gt;) S1_a(&lt;M11,Slave21&gt;) S1_b(&lt;M10,Slave21&gt;+&lt;M11,Slave21&gt;) S2_a(&lt;M10,Slave21&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T35 -> T75 [ label=<T55&gt;>];
T76 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S2_b(&lt;M10,Slave21&gt;) S2_a(&lt;M10,Slave21&gt;) Richiesta(&lt;M22&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;) Buffer_input(&lt;M11&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T35 -> T76 [ label=<T5&gt;>];
T77 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_b(&lt;M10,Slave21&gt;) S2_a(&lt;M10,Slave21&gt;) Attesa(&lt;M10&gt;+&lt;M11&gt;+&lt;M22&gt;) Buffer_input(&lt;M11&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T35 -> T77 [ label=<T1&gt;>];
T78 [ label="S0(2&lt;Slave10&gt;+2&lt;Slave21&gt;) S1_a(&lt;M22,Slave10&gt;) S1_b(&lt;M10,Slave21&gt;+&lt;M22,Slave10&gt;) S2_a(&lt;M10,Slave21&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T36 -> T78 [ label=<T55&gt;>];
T79 [ label="S0(3&lt;Slave10&gt;+&lt;Slave21&gt;) S1_a(&lt;M22,Slave21&gt;) S1_b(&lt;M10,Slave21&gt;+&lt;M22,Slave21&gt;) S2_a(&lt;M10,Slave21&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T36 -> T79 [ label=<T55&gt;>];
T80 [ label="S0(3&lt;Slave10&gt;+2&lt;Slave21&gt;) S2_b(&lt;M10,Slave21&gt;) S2_a(&lt;M10,Slave21&gt;) Richiesta(&lt;M11&gt;) Attesa(&lt;M10&gt;+&lt;M22&gt;) Buffer_input(&lt;M22&gt;)
|M10|=1 |M11|=1 |M22|=1 |Slave10|=1 |Slave21|=1
"];
T36 -> T80 [ label=<T5&gt;>];
T36 -> T77 [ label=<T1&gt;>];
T81 [shape=none label="..."];
T37 -> T81 [ label=<T6&gt;>];
T37 -> T76 [ label=<T1&gt;>];
T37 -> T80 [ label=<T1&gt;>];
T38 -> T67 [ label=<T55&gt;>];
T82 [shape=none label="..."];
T38 -> T82 [ label=<T55&gt;>];
T38 -> T76 [ label=<T4&gt;>];
T83 [shape=none label="..."];
T38 -> T83 [ label=<T1&gt;>];
T84 [shape=none label="..."];
T39 -> T84 [ label=<T55&gt;>];
T85 [shape=none label="..."];
T39 -> T85 [ label=<T55&gt;>];
T39 -> T80 [ label=<T4&gt;>];
T83 [shape=none label="..."];
T39 -> T83 [ label=<T1&gt;>];
T40 -> T75 [ label=<T4&gt;>];
T82 [shape=none label="..."];
T40 -> T82 [ label=<T5&gt;>];
T86 [shape=none label="..."];
T40 -> T86 [ label=<T1&gt;>];
T41 -> T77 [ label=<T4&gt;>];
T83 [shape=none label="..."];
T41 -> T83 [ label=<T5&gt;>];
T87 [shape=none label="..."];
T41 -> T87 [ label=<T55&gt;>];
T88 [shape=none label="..."];
T41 -> T88 [ label=<T55&gt;>];
T41 -> T68 [ label=<T55&gt;>];
T86 [shape=none label="..."];
T41 -> T86 [ label=<T55&gt;>];
T42 -> T78 [ label=<T4&gt;>];
T89 [shape=none label="..."];
T42 -> T89 [ label=<T4&gt;>];
T84 [shape=none label="..."];
T42 -> T84 [ label=<T5&gt;>];
T90 [shape=none label="..."];
T42 -> T90 [ label=<T5&gt;>];
T87 [shape=none label="..."];
T42 -> T87 [ label=<T1&gt;>];
T43 -> T79 [ label=<T4&gt;>];
T91 [shape=none label="..."];
T43 -> T91 [ label=<T4&gt;>];
T85 [shape=none label="..."];
T43 -> T85 [ label=<T5&gt;>];
T92 [shape=none label="..."];
T43 -> T92 [ label=<T5&gt;>];
T88 [shape=none label="..."];
T43 -> T88 [ label=<T1&gt;>];
T93 [shape=none label="..."];
T44 -> T93 [ label=<T4&gt;>];
T94 [shape=none label="..."];
T44 -> T94 [ label=<T5&gt;>];
T44 -> T69 [ label=<T55&gt;>];
T87 [shape=none label="..."];
T44 -> T87 [ label=<T55&gt;>];
T95 [shape=none label="..."];
T45 -> T95 [ label=<T4&gt;>];
T96 [shape=none label="..."];
T45 -> T96 [ label=<T5&gt;>];
T45 -> T70 [ label=<T55&gt;>];
T88 [shape=none label="..."];
T45 -> T88 [ label=<T55&gt;>];
T93 [shape=none label="..."];
T46 -> T93 [ label=<T1&gt;>];
T46 -> T71 [ label=<T55&gt;>];
T89 [shape=none label="..."];
T46 -> T89 [ label=<T55&gt;>];
T97 [shape=none label="..."];
T46 -> T97 [ label=<T5&gt;>];
T94 [shape=none label="..."];
T47 -> T94 [ label=<T1&gt;>];
T47 -> T72 [ label=<T55&gt;>];
T90 [shape=none label="..."];
T47 -> T90 [ label=<T55&gt;>];
T97 [shape=none label="..."];
T47 -> T97 [ label=<T4&gt;>];
T95 [shape=none label="..."];
T48 -> T95 [ label=<T1&gt;>];
T48 -> T73 [ label=<T55&gt;>];
T91 [shape=none label="..."];
T48 -> T91 [ label=<T55&gt;>];
T98 [shape=none label="..."];
T48 -> T98 [ label=<T5&gt;>];
T96 [shape=none label="..."];
T49 -> T96 [ label=<T1&gt;>];
T49 -> T74 [ label=<T55&gt;>];
T92 [shape=none label="..."];
T49 -> T92 [ label=<T55&gt;>];
T98 [shape=none label="..."];
T49 -> T98 [ label=<T4&gt;>];
T99 [shape=none label="..."];
T50 -> T99 [ label=<T6&gt;>];
T97 [shape=none label="..."];
T50 -> T97 [ label=<T1&gt;>];
T100 [shape=none label="..."];
T51 -> T100 [ label=<T6&gt;>];
T98 [shape=none label="..."];
T51 -> T98 [ label=<T1&gt;>];
T101 [shape=none label="..."];
T52 -> T101 [ label=<T4&gt;>];
T102 [shape=none label="..."];
T52 -> T102 [ label=<T1&gt;>];
T103 [shape=none label="..."];
T52 -> T103 [ label=<T5&gt;>];
T104 [shape=none label="..."];
T52 -> T104 [ label=<T5&gt;>];
T105 [shape=none label="..."];
T53 -> T105 [ label=<T4&gt;>];
T106 [shape=none label="..."];
T53 -> T106 [ label=<T1&gt;>];
T107 [shape=none label="..."];
T53 -> T107 [ label=<T5&gt;>];
T108 [shape=none label="..."];
T53 -> T108 [ label=<T5&gt;>];
T109 [shape=none label="..."];
T54 -> T109 [ label=<T6&gt;>];
T110 [shape=none label="..."];
T54 -> T110 [ label=<T1&gt;>];
T103 [shape=none label="..."];
T54 -> T103 [ label=<T55&gt;>];
T108 [shape=none label="..."];
T54 -> T108 [ label=<T55&gt;>];
T110 [shape=none label="..."];
T55 -> T110 [ label=<T5&gt;>];
T111 [shape=none label="..."];
T55 -> T111 [ label=<T55&gt;>];
T112 [shape=none label="..."];
T55 -> T112 [ label=<T55&gt;>];
T102 [shape=none label="..."];
T55 -> T102 [ label=<T55&gt;>];
T106 [shape=none label="..."];
T55 -> T106 [ label=<T55&gt;>];
T113 [shape=none label="..."];
T56 -> T113 [ label=<T4&gt;>];
T111 [shape=none label="..."];
T56 -> T111 [ label=<T1&gt;>];
T114 [shape=none label="..."];
T56 -> T114 [ label=<T5&gt;>];
T115 [shape=none label="..."];
T56 -> T115 [ label=<T5&gt;>];
T116 [shape=none label="..."];
T57 -> T116 [ label=<T4&gt;>];
T112 [shape=none label="..."];
T57 -> T112 [ label=<T1&gt;>];
T117 [shape=none label="..."];
T57 -> T117 [ label=<T5&gt;>];
T118 [shape=none label="..."];
T57 -> T118 [ label=<T5&gt;>];
T119 [shape=none label="..."];
T58 -> T119 [ label=<T6&gt;>];
T110 [shape=none label="..."];
T58 -> T110 [ label=<T1&gt;>];
T114 [shape=none label="..."];
T58 -> T114 [ label=<T55&gt;>];
T117 [shape=none label="..."];
T58 -> T117 [ label=<T55&gt;>];
T120 [shape=none label="..."];
T59 -> T120 [ label=<Reset_s&gt;>];
T121 [shape=none label="..."];
T59 -> T121 [ label=<T2&gt;>];
T109 [shape=none label="..."];
T59 -> T109 [ label=<T1&gt;>];
T119 [shape=none label="..."];
T59 -> T119 [ label=<T1&gt;>];
T122 [shape=none label="..."];
T60 -> T122 [ label=<T5&gt;>];
T123 [shape=none label="..."];
T60 -> T123 [ label=<T1&gt;>];
T103 [shape=none label="..."];
T60 -> T103 [ label=<T4&gt;>];
T104 [shape=none label="..."];
T60 -> T104 [ label=<T4&gt;>];
T124 [shape=none label="..."];
T61 -> T124 [ label=<T5&gt;>];
T125 [shape=none label="..."];
T61 -> T125 [ label=<T1&gt;>];
T126 [shape=none label="..."];
T61 -> T126 [ label=<T4&gt;>];
T108 [shape=none label="..."];
T61 -> T108 [ label=<T4&gt;>];
T110 [shape=none label="..."];
T62 -> T110 [ label=<T4&gt;>];
T127 [shape=none label="..."];
T62 -> T127 [ label=<T55&gt;>];
T128 [shape=none label="..."];
T62 -> T128 [ label=<T55&gt;>];
T123 [shape=none label="..."];
T62 -> T123 [ label=<T55&gt;>];
T125 [shape=none label="..."];
T62 -> T125 [ label=<T55&gt;>];
T129 [shape=none label="..."];
T63 -> T129 [ label=<T5&gt;>];
T127 [shape=none label="..."];
T63 -> T127 [ label=<T1&gt;>];
T114 [shape=none label="..."];
T63 -> T114 [ label=<T4&gt;>];
T130 [shape=none label="..."];
T63 -> T130 [ label=<T4&gt;>];
T131 [shape=none label="..."];
T64 -> T131 [ label=<T5&gt;>];
T128 [shape=none label="..."];
T64 -> T128 [ label=<T1&gt;>];
T117 [shape=none label="..."];
T64 -> T117 [ label=<T4&gt;>];
T132 [shape=none label="..."];
T64 -> T132 [ label=<T4&gt;>];
T133 [shape=none label="..."];
T65 -> T133 [ label=<T55&gt;>];
T134 [shape=none label="..."];
T65 -> T134 [ label=<T55&gt;>];
T123 [shape=none label="..."];
T65 -> T123 [ label=<T5&gt;>];
T102 [shape=none label="..."];
T65 -> T102 [ label=<T4&gt;>];
T135 [shape=none label="..."];
T66 -> T135 [ label=<T1&gt;>];
T136 [shape=none label="..."];
T66 -> T136 [ label=<T5&gt;>];
T126 [shape=none label="..."];
T66 -> T126 [ label=<T5&gt;>];
T105 [shape=none label="..."];
T66 -> T105 [ label=<T4&gt;>];
T137 [shape=none label="..."];
T67 -> T137 [ label=<T1&gt;>];
T124 [shape=none label="..."];
T67 -> T124 [ label=<T5&gt;>];
T136 [shape=none label="..."];
T67 -> T136 [ label=<T4&gt;>];
T107 [shape=none label="..."];
T67 -> T107 [ label=<T4&gt;>];
T138 [shape=none label="..."];
T68 -> T138 [ label=<T55&gt;>];
T139 [shape=none label="..."];
T68 -> T139 [ label=<T55&gt;>];
T137 [shape=none label="..."];
T68 -> T137 [ label=<T5&gt;>];
T125 [shape=none label="..."];
T68 -> T125 [ label=<T5&gt;>];
T135 [shape=none label="..."];
T68 -> T135 [ label=<T4&gt;>];
T106 [shape=none label="..."];
T68 -> T106 [ label=<T4&gt;>];
T133 [shape=none label="..."];
T69 -> T133 [ label=<T55&gt;>];
T138 [shape=none label="..."];
T69 -> T138 [ label=<T55&gt;>];
T127 [shape=none label="..."];
T69 -> T127 [ label=<T5&gt;>];
T140 [shape=none label="..."];
T69 -> T140 [ label=<T5&gt;>];
T111 [shape=none label="..."];
T69 -> T111 [ label=<T4&gt;>];
T141 [shape=none label="..."];
T69 -> T141 [ label=<T4&gt;>];
T134 [shape=none label="..."];
T70 -> T134 [ label=<T55&gt;>];
T139 [shape=none label="..."];
T70 -> T139 [ label=<T55&gt;>];
T128 [shape=none label="..."];
T70 -> T128 [ label=<T5&gt;>];
T142 [shape=none label="..."];
T70 -> T142 [ label=<T5&gt;>];
T112 [shape=none label="..."];
T70 -> T112 [ label=<T4&gt;>];
T143 [shape=none label="..."];
T70 -> T143 [ label=<T4&gt;>];
T141 [shape=none label="..."];
T71 -> T141 [ label=<T1&gt;>];
T130 [shape=none label="..."];
T71 -> T130 [ label=<T5&gt;>];
T144 [shape=none label="..."];
T71 -> T144 [ label=<T5&gt;>];
T113 [shape=none label="..."];
T71 -> T113 [ label=<T4&gt;>];
T140 [shape=none label="..."];
T72 -> T140 [ label=<T1&gt;>];
T129 [shape=none label="..."];
T72 -> T129 [ label=<T5&gt;>];
T115 [shape=none label="..."];
T72 -> T115 [ label=<T4&gt;>];
T144 [shape=none label="..."];
T72 -> T144 [ label=<T4&gt;>];
T143 [shape=none label="..."];
T73 -> T143 [ label=<T1&gt;>];
T132 [shape=none label="..."];
T73 -> T132 [ label=<T5&gt;>];
T145 [shape=none label="..."];
T73 -> T145 [ label=<T5&gt;>];
T116 [shape=none label="..."];
T73 -> T116 [ label=<T4&gt;>];
T142 [shape=none label="..."];
T74 -> T142 [ label=<T1&gt;>];
T131 [shape=none label="..."];
T74 -> T131 [ label=<T5&gt;>];
T118 [shape=none label="..."];
T74 -> T118 [ label=<T4&gt;>];
T145 [shape=none label="..."];
T74 -> T145 [ label=<T4&gt;>];
T146 [shape=none label="..."];
T75 -> T146 [ label=<T4&gt;>];
T147 [shape=none label="..."];
T75 -> T147 [ label=<T1&gt;>];
T148 [shape=none label="..

View file

@ -0,0 +1,74 @@
|0|
|
f 4 11 0 8 0 0 0
N -7134 0.6354166666666666 0.4322916666666667 0
n -7134 0.9635416666666666 0.4322916666666667 0
R1 -7134 1.328125 0.4322916666666667 0
n1 -7134 0.8229166666666666 1.5989583333333333 0
S0 -10007 6.0 2.0 5.434166666666666 1.6122916666666667 0 6.2 2.1666666666666665 Slave
S1_a 0 5.0 3.1666666666666665 3.7883333333333327 3.3622916666666662 0 5.2 3.3333333333333335 Master,Slave
S1_b 0 7.0 3.1666666666666665 5.694583333333333 3.3622916666666662 0 7.2 3.3333333333333335 Master,Slave
S2_b 0 7.0 4.833333333333333 4.944583333333333 4.528958333333333 0 7.2 5.0 Master,Slave
S3 0 6.0 6.0 5.434166666666666 6.195625 0 6.2 6.166666666666667 Slave
S2_a 0 5.0 4.833333333333333 4.454999999999999 4.778958333333333 0 5.2 5.0 Master,Slave
Richiesta -10008 1.8333333333333333 1.8333333333333333 0.6425000000000001 2.1122916666666667 0 2.033333333333333 2.0 Master
Attesa 0 1.8333333333333333 3.6666666666666665 0.9029166666666667 3.9456249999999997 0 2.033333333333333 3.8333333333333335 Master
Elabora 0 1.8333333333333333 5.333333333333333 0.8091666666666667 5.612291666666667 0 2.033333333333333 5.5 Master
Buffer_input 0 3.6666666666666665 2.6666666666666665 2.3299999999999996 2.278958333333333 0 3.8666666666666667 2.8333333333333335 Master
Buffer_output 0 3.6666666666666665 5.5 2.2362499999999996 5.695625 0 3.8666666666666667 5.666666666666667 Master
T4 1.0 0 0 1 0 5.0 4.0 5.3125 4.057291666666667 5.083333333333333 4.067708333333333 0
1 2 0 0 0.000000 0.000000 <m,id>
1
1 6 0 0 0.000000 0.000000 <m,id>
0
T5 1.0 0 0 1 0 7.0 4.0 6.645833333333333 4.057291666666667 7.083333333333333 4.067708333333333 0
1 3 0 0 0.000000 0.000000 <m,id>
1
1 4 0 0 0.000000 0.000000 <m,id>
0
T6 1.0 0 0 2 0 6.0 5.5 5.979166666666667 5.223958333333333 6.083333333333333 5.567708333333333 0
1 6 1 0 0.000000 0.000000 <m,id>
6.0 5.416666666666667
1 4 0 0 0.000000 0.000000 <m,id>
2
1 5 0 0 0.000000 0.000000 <id>
1 11 3 0 0.000000 0.000000 <m>
4.666666666666667 5.5
4.666666666666667 5.5
4.75 5.5
0
Reset_s 1.0 0 0 1 1 6.833333333333333 2.0 6.640625 1.8072916666666667 6.916666666666667 2.0677083333333335 0
1 5 2 0 0.000000 0.000000 <id>
8.0 2.0833333333333335
8.0 6.0
1
1 1 0 0 0.000000 0.000000 <id>
0
T1 1.0 0 0 1 0 1.8333333333333333 2.6666666666666665 1.9791666666666667 2.390625 1.9166666666666667 2.734375 0
1 7 0 0 0.000000 0.000000 <m>
2
1 8 1 0 0.000000 0.000000 <m>
1.8333333333333333 3.1666666666666665
1 10 0 0 0.000000 0.000000 <m>
0
T2 1.0 0 0 2 0 1.8333333333333333 4.5 1.8125 4.307291666666667 1.9166666666666667 4.567708333333333 0
1 8 0 0 0.000000 0.000000 <m>
1 11 1 0 0.000000 0.000000 <m>
3.6666666666666665 4.5
1
1 9 0 0 0.000000 0.000000 <m>
0
T0 1.0 0 0 1 1 0.8333333333333334 5.333333333333333 0.8125 5.140625 0.9166666666666666 5.401041666666667 0
1 9 0 0 0.000000 0.000000 <m>
1
1 7 1 0 0.000000 0.000000 <m>
0.8333333333333334 1.8333333333333333
0
T55 1.0 0 0 2 1 6.0 2.8333333333333335 5.953125 2.640625 6.083333333333333 2.9010416666666665 0 4.364583333333333 2.984375 [((d(m) = M1) and (d(id) = Slave1)) or ((d(m) = M2) and (d(id) = Slave2))]
1 1 0 0 0.000000 0.000000 <id>
1 10 1 0 0.000000 0.000000 <m>
5.333333333333333 2.6666666666666665
2
1 2 0 0 0.000000 0.000000 <m,id>
1 3 0 0 0.000000 0.000000 <m,id>
0

View file

@ -0,0 +1 @@
1

View file

@ -0,0 +1,8 @@
0
0
0
0
0
0
0
0

File diff suppressed because it is too large Load diff

View file

@ -0,0 +1 @@
*0*0*0*0*1*0*0*1*0*1*0

View file

@ -0,0 +1,103 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="ReteE" version="121">
<gspn name="CPN" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false" zoom="125">
<nodes>
<place domain="Slave" label-y="-2.0" marking="R1&lt;Slave1&gt;+R1&lt;Slave2&gt;" name="S0" x="35.0" y="11.0"/>
<place domain="D" label-x="0.5" name="S1_a" x="29.0" y="18.0"/>
<place domain="D" name="S1_b" x="41.0" y="18.0"/>
<place domain="D" label-x="-4.5" label-y="-1.5" name="S2_b" x="41.0" y="28.0"/>
<place domain="Slave" name="S3" x="35.0" y="35.0"/>
<place domain="D" label-x="4.5" label-y="0.0" name="S2_a" x="29.0" y="28.0"/>
<transition label-x="2.0" label-y="0.0" name="T4" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="29.55" y="23.0"/>
<transition label-x="-2.0" label-y="0.0" name="T5" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="41.55" y="23.0"/>
<transition label-y="-2.0" name="T6" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="35.55" y="32.0"/>
<transition name="Reset_s" nservers-x="0.5" type="EXP" x="40.55" y="11.0"/>
<transition label-x="1.0" label-y="-2.0" name="T1" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="10.55" y="15.0"/>
<place domain="Master" label-x="-0.5" label-y="2.0" marking="N&lt;All&gt;" name="Richiesta" x="10.0" y="10.0"/>
<place domain="Master" label-y="2.0" name="Attesa" x="10.0" y="21.0"/>
<place domain="Master" label-y="2.0" name="Elabora" x="10.0" y="31.0"/>
<transition name="T2" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="10.55" y="26.0"/>
<transition name="T0" nservers-x="0.5" type="EXP" x="4.55" y="31.0"/>
<place domain="Master" label-y="-2.0" name="Buffer_input" x="21.0" y="15.0"/>
<place domain="Master" name="Buffer_output" x="21.0" y="32.0"/>
<color-class definition="{m1,m3} is M1 + {m2} is M2" name="Master" x="3.3125" y="5.0"/>
<color-var domain="Master" name="m" x="25.9375" y="9.0"/>
<template last-binding="1" name="N" type="INTEGER" x="3.0" y="2.0"/>
<template last-binding="3" name="n" type="INTEGER" x="5.0" y="2.0"/>
<color-class definition="{ID1} is Slave1 + {ID2} is Slave2" name="Slave" x="3.0" y="3.0"/>
<color-var domain="Slave" name="id" x="21.9375" y="3.0"/>
<color-class definition="Master*Slave" name="D" x="3.125" y="7.0"/>
<text-box bold="true" border-color="none" fill-color="none" name="__textBox0" shadow="true" shape="ROUND_RECTANGLE" text-color="#000000" x="33.0" y="4.0">Condizione booleana FORK:</text-box>
<template last-binding="1" name="R1" type="INTEGER" x="7.0" y="2.0"/>
<transition guard="((m in M1) &amp;&amp; (id in Slave1)) || ((m in M2) &amp;&amp; (id in Slave2))" name="T55" nservers-x="0.5" type="EXP" x="35.55" y="16.0"/>
</nodes>
<edges>
<arc head="S2_a" kind="OUTPUT" mult="&lt;m,id&gt;" tail="T4"/>
<arc head="T4" kind="INPUT" mult="&lt;m,id&gt;" tail="S1_a"/>
<arc head="T6" kind="INPUT" mult="&lt;m,id&gt;" tail="S2_a">
<point x="36.0" y="32.5"/>
</arc>
<arc head="S2_b" kind="OUTPUT" mult="&lt;m,id&gt;" tail="T5"/>
<arc head="T5" kind="INPUT" mult="&lt;m,id&gt;" tail="S1_b"/>
<arc head="T6" kind="INPUT" mult="&lt;m,id&gt;" tail="S2_b"/>
<arc head="S3" kind="OUTPUT" mult="&lt;id&gt;" mult-x="2.0" mult-y="0.0" tail="T6"/>
<arc head="Reset_s" kind="INPUT" mult="&lt;id&gt;" tail="S3">
<point x="48.0" y="36.0"/>
<point x="48.0" y="12.5"/>
</arc>
<arc head="S0" kind="OUTPUT" mult="&lt;id&gt;" tail="Reset_s"/>
<arc head="T1" kind="INPUT" mult="&lt;m&gt;" mult-x="0.5" tail="Richiesta"/>
<arc head="Attesa" kind="OUTPUT" mult="&lt;m&gt;" mult-k="1.2018554687500003" tail="T1">
<point x="11.0" y="19.0"/>
</arc>
<arc head="T2" kind="INPUT" mult="&lt;m&gt;" tail="Attesa"/>
<arc head="Elabora" kind="OUTPUT" mult="&lt;m&gt;" tail="T2"/>
<arc head="Buffer_input" kind="OUTPUT" mult="&lt;m&gt;" tail="T1"/>
<arc head="Buffer_output" kind="OUTPUT" mult="&lt;m&gt;" mult-k="0.8393554687500001" tail="T6">
<point x="28.0" y="33.0"/>
<point x="28.0" y="33.0"/>
<point x="28.5" y="33.0"/>
</arc>
<arc head="T0" kind="INPUT" mult="&lt;m&gt;" tail="Elabora"/>
<arc head="Richiesta" kind="OUTPUT" mult="&lt;m&gt;" mult-y="0.01853809374530968" tail="T0">
<point x="5.0" y="11.0"/>
</arc>
<arc head="T2" kind="INPUT" mult="&lt;m&gt;" tail="Buffer_output">
<point x="22.0" y="27.0"/>
</arc>
<arc head="S1_a" kind="OUTPUT" mult="&lt;m,id&gt;" tail="T55"/>
<arc head="S1_b" kind="OUTPUT" mult="&lt;m,id&gt;" tail="T55"/>
<arc head="T55" kind="INPUT" mult="&lt;id&gt;" tail="S0"/>
<arc head="T55" kind="INPUT" mult="&lt;m&gt;" tail="Buffer_input">
<point x="32.0" y="16.0"/>
</arc>
</edges>
</gspn>
<measures gspn-name="CPN" name="RG of CPN" rapid-type="BUILD_RG" simplified-UI="true">
<assignments>
<assignment bind-model="SINGLE_VALUE" single-val="3" type="INTEGER" varname="N"/>
<assignment bind-model="SINGLE_VALUE" single-val="3" type="INTEGER" varname="n"/>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="R1"/>
</assignments>
<greatspn/>
<formulas>
<formula language="STAT"/>
<formula language="RG"/>
</formulas>
</measures>
<measures gspn-name="CPN" name="SRG of CPN" rapid-type="BUILD_SYMRG" simplified-UI="true">
<assignments>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="N"/>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="n"/>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="R1"/>
</assignments>
<greatspn mode="SWN_SYM"/>
<formulas>
<formula language="STAT"/>
<formula language="RG"/>
</formulas>
</measures>
<resource-list>
<document-log uuid="fb288565-cb5a-47e3-8b86-2f9f2339b566">rO0ABXNyABRqYXZhLnV0aWwuTGlua2VkTGlzdAwpU11KYIgiAwAAeHB3BAAAACd0AJobWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vV05TUkcgIi9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzIuYi9SZXRlRi1TUkcgb2YgQ1BOLnNvbHV0aW9uL0NQTiIgLW1wYXIgTiAxIC1tcGFyIFIxIDEgLW1wYXIgbiAxICAtZ3VpLXN0YXQKdAArT3ZlcnJpZGluZyBtYXJraW5nIHBhcmFtZXRlciBOIHRvIHZhbHVlIDEuCnQALE92ZXJyaWRpbmcgbWFya2luZyBwYXJhbWV0ZXIgUjEgdG8gdmFsdWUgMS4KdAArT3ZlcnJpZGluZyBtYXJraW5nIHBhcmFtZXRlciBuIHRvIHZhbHVlIDEuCnQAYy0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tCnQAHVVTRSA6IFdOU1JHIG5ldG5hbWUgWy1vXVstbV0KdAABCnQALVRvIHBsb3QgdGhlIGdlbmVyYXRlZCBSRyBpbiBHcmFwaHZpeiBmb3JtYXQ6CnQANCAgICAgIFstZG90LUYgZmlsZW5hbWUuZG90XSBbLW1heC1kb3QtbWFya2luZ3MgbWF4XQp0ADRQYXJhbWV0cmljIG1hcmtpbmcvcmF0ZSBwYXJhbWV0ZXJzIGNhbiBiZSBzZXQgd2l0aDoKdAA5ICAgICAgWy1tcGFyIHBhcmFtX25hbWUgdmFsdWVdICBbLXJwYXIgcGFyYW1fbmFtZSB2YWx1ZV0KdABjLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0KdAAvU2VuZCBmaWxlcyBuZXRuYW1lLm5ldCwgLmRlZiB0byBlLW1haWwgYWRkcmVzcwp0ACpncmVhdHNwbkBkaS51bml0by5pdCBpZiB5b3UgZmluZCBhbnkgYnVnLgp0AGMtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLQp0AAEKdABLV0FSTklORyA6IGEgZGVmYXVsdCBkeW5hbWljIHN1YmNsYXNzIGhhcyBiZWVuIGFkZGVkIGZvciBzdGF0aWMgc3ViY2xhc3MgTTEKdABLV0FSTklORyA6IGEgZGVmYXVsdCBkeW5hbWljIHN1YmNsYXNzIGhhcyBiZWVuIGFkZGVkIGZvciBzdGF0aWMgc3ViY2xhc3MgTTIKdABPV0FSTklORyA6IGEgZGVmYXVsdCBkeW5hbWljIHN1YmNsYXNzIGhhcyBiZWVuIGFkZGVkIGZvciBzdGF0aWMgc3ViY2xhc3MgU2xhdmUxCnQAT1dBUk5JTkcgOiBhIGRlZmF1bHQgZHluYW1pYyBzdWJjbGFzcyBoYXMgYmVlbiBhZGRlZCBmb3Igc3RhdGljIHN1YmNsYXNzIFNsYXZlMgp0AAEKdAAqICoqKioqIFN5bWJvbGljIFJlYWNoYWJpbGl0eSBHcmFwaCAqKioqKiAKdAABCnQAGlRBTkdJQkxFIE1BUktJTkdTICA6IDEyOTYKdAAXVkFOSVNISU5HIE1BUktJTkdTIDogMAp0ABdERUFEIE1BUktJTkdTICAgICAgOiAwCnQAAQp0ABpUT1RBTCBNQVJLSU5HUyAgICAgOiAxMjk2CnQAAQp0ACogKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqIAp0AAEKdAAiT3JkaW5hcnkgdGFuZ2libGUgbWFya2luZ3MgOiA0MDk2CnQAIE9yZGluYXJ5IHZhbmlzaGluZyBtYXJraW5ncyA6IDAKdAAbT3JkaW5hcnkgZGVhZCBtYXJraW5ncyA6IDAKdAAkVGhlIGluaXRpYWwgbWFya2luZyBpcyBhIGhvbWUgc3RhdGUKdAAcVGltZSByZXF1aXJlZCAtLS0tLS0tLS0tPiAwCnQAAQp0ACogKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqIAp0ACcbWzBYG1szMm0gUFJPQ0VTUyBFWElURUQgTk9STUFMTFkuG1swbQp4c3EAfgAAdwQAAAAnc3IAEWphdmEubGFuZy5Cb29sZWFuzSBygNWc+u4CAAFaAAV2YWx1ZXhwAXEAfgArcQB+ACtxAH4AK3EAfgArcQB+ACtxAH4AK3EAfgArcQB+ACtxAH4AK3EAfgArcQB+ACtxAH4AK3EAfgArcQB+ACtxAH4AK3EAfgArcQB+ACtxAH4AK3EAfgArcQB+ACtxAH4AK3EAfgArcQB+ACtxAH4AK3EAfgArcQB+ACtxAH4AK3EAfgArcQB+ACtxAH4AK3EAfgArcQB+ACtxAH4AK3EAfgArcQB+ACtxAH4AK3EAfgArcQB+ACt4</document-log>
</resource-list>
</project>

Binary file not shown.

After

Width:  |  Height:  |  Size: 64 KiB

View file

@ -0,0 +1,151 @@
digraph structs {
newrank=true;
size="5,5";
subgraph cluster1 { style=invis;
node [shape=record, height=0.8, width=0.5, fontsize=50, penwidth=4, fillcolor=white, style=filled];
edge [arrowhead=vee, minlen=1, penwidth=4, color=blue];
n89 [label="<i0>0|<i1>1"];
n89:i0 -> n85:n;
n89:i1 -> n88:n;
n85 [label="<i0>0|<i1>1"];
n85:i0 -> n84:n;
n85:i1 -> n77:n;
n84 [label="<i0>0|<i1>1"];
n84:i0 -> n83:n;
n84:i1 -> n76:n;
n83 [label="<i1>1"];
n83:i1 -> n82:n;
n82 [label="<i0>0|<i1>1"];
n82:i0 -> n81:n;
n82:i1 -> n70:n;
n81 [label="<i0>0|<i1>1"];
n81:i0 -> n80:n;
n81:i1 -> n66:n;
n80 [label="<i0>0|<i1>1"];
n80:i0 -> n79:n;
n80:i1 -> n68:n;
n79 [label="<i0>0"];
n79:i0 -> n78:n;
n78 [label="<i0>0|<i1>1"];
n78:i0 -> n59:n;
n78:i1 -> n63:n;
n59 [label="<i1>1"];
n59:i1 -> n58:n;
n58 [label="<i0>0|<i1>1"];
n58:i0 -> n52:n;
n58:i1 -> n57:n;
n52 [label="<i0>0|<i1>1"];
n52:i0 -> n51:n;
n52:i1 -> n42:n;
n51 [label="<i0>0|<i1>1"];
n51:i0 -> n50:n;
n51:i1 -> n41:n;
n50 [label="<i0>0"];
n50:i0 -> n49:n;
n49 [label="<i0>0"];
n49:i0 -> n48:n;
n48 [label="<i1>1"];
n48:i1 -> n47:n;
n47 [label="<i0>0|<i1>1"];
n47:i0 -> n46:n;
n47:i1 -> n30:n;
n46 [label="<i0>0|<i1>1"];
n46:i0 -> n45:n;
n46:i1 -> n29:n;
n45 [label="<i0>0|<i1>1"];
n45:i0 -> n44:n;
n45:i1 -> n25:n;
n44 [label="<i0>0"];
n44:i0 -> n43:n;
n43 [label="<i0>0|<i1>1"];
n43:i0 -> n1:n;
n43:i1 -> n23:n;
n1 [label="<i1>1"];
n23 [label="<i0>0"];
n25 [label="<i0>0"];
n25:i0 -> n24:n;
n24 [label="<i0>0"];
n24:i0 -> n23:n;
n29 [label="<i0>0"];
n29:i0 -> n28:n;
n28 [label="<i1>1"];
n28:i1 -> n24:n;
n30 [label="<i0>0"];
n30:i0 -> n29:n;
n41 [label="<i0>0|<i1>1"];
n41:i0 -> n40:n;
n41:i1 -> n39:n;
n40 [label="<i1>1"];
n40:i1 -> n38:n;
n38 [label="<i0>0"];
n38:i0 -> n37:n;
n37 [label="<i0>0"];
n37:i0 -> n30:n;
n39 [label="<i0>0"];
n39:i0 -> n38:n;
n42 [label="<i0>0"];
n42:i0 -> n41:n;
n57 [label="<i0>0"];
n57:i0 -> n56:n;
n56 [label="<i0>0"];
n56:i0 -> n55:n;
n55 [label="<i0>0"];
n55:i0 -> n54:n;
n54 [label="<i0>0"];
n54:i0 -> n53:n;
n53 [label="<i0>0"];
n53:i0 -> n47:n;
n63 [label="<i0>0"];
n63:i0 -> n58:n;
n68 [label="<i1>1"];
n68:i1 -> n64:n;
n64 [label="<i0>0"];
n64:i0 -> n63:n;
n66 [label="<i0>0"];
n66:i0 -> n65:n;
n65 [label="<i0>0"];
n65:i0 -> n64:n;
n70 [label="<i0>0"];
n70:i0 -> n69:n;
n69 [label="<i0>0"];
n69:i0 -> n68:n;
n76 [label="<i0>0"];
n76:i0 -> n75:n;
n75 [label="<i0>0"];
n75:i0 -> n70:n;
n77 [label="<i0>0"];
n77:i0 -> n76:n;
n88 [label="<i0>0"];
n88:i0 -> n87:n;
n87 [label="<i0>0"];
n87:i0 -> n86:n;
n86 [label="<i0>0"];
n86:i0 -> n82:n;
}
subgraph cluster2 { style=invis;
node [shape=none, fontsize=60, margin="0.5,0.1"];
P12 [label="S0"];
P9 [label="S1_a"];
P11 [label="S1_b"];
P8 [label="S2_a"];
P10 [label="S2_b"];
P7 [label="S3"];
P22 [label="R0"];
P21 [label="R1"];
P20 [label="R2"];
P19 [label="R3"];
P1 [label="M0"];
P4 [label="M1"];
P3 [label="M2"];
P2 [label="M3"];
P6 [label="Buffer_s"];
P5 [label="Risultato"];
P13 [label="M0_2"];
P17 [label="M1_2"];
P15 [label="M2_2"];
P14 [label="M3_2"];
P18 [label="Buffer_2"];
P16 [label="Risultato_2"];
}
{rank=same n89 P22} -> {rank=same n85 n88 P21} -> {rank=same n84 n77 n87 P20} -> {rank=same n83 n76 n86 P19} -> {rank=same n82 n75 P18} -> {rank=same n81 n70 P17} -> {rank=same n80 n66 n69 P16} -> {rank=same n79 n68 n65 P15} -> {rank=same n78 n64 P14} -> {rank=same n59 n63 P13} -> {rank=same n58 P12} -> {rank=same n52 n57 P11} -> {rank=same n51 n42 n56 P10} -> {rank=same n50 n41 n55 P9} -> {rank=same n49 n40 n39 n54 P8} -> {rank=same n48 n38 n53 P7} -> {rank=same n47 n37 P6} -> {rank=same n46 n30 P5} -> {rank=same n45 n29 P4} -> {rank=same n44 n25 n28 P3} -> {rank=same n43 n24 P2} -> {rank=same n1 n23 P1} [style=invis]
}

Binary file not shown.

File diff suppressed because one or more lines are too long

View file

@ -1,11 +1,45 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?> <?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="EsE" version="121"> <!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="EsE" version="121">
<gspn name="CPN" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false"> <gspn name="CPN" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false">
<nodes/> <nodes>
<edges/> <place label-x="-1.0" label-y="2.0" marking="N&lt;All&gt;" name="P0" x="26.0" y="27.0"/>
<place name="P1" x="32.0" y="27.0"/>
<place name="P2" x="38.0" y="27.0"/>
<transition name="T0" nservers-x="0.5" type="EXP" x="22.55" y="27.0"/>
<transition name="T1" nservers-x="0.5" type="EXP" x="29.55" y="27.0"/>
<transition name="T2" nservers-x="0.5" type="EXP" x="35.55" y="27.0"/>
<color-class definition="m{1..k}" name="Master" x="21.125" y="20.0"/>
<template name="k" type="INTEGER" x="29.0" y="18.0"/>
<template name="R2" type="INTEGER" x="27.0" y="18.0"/>
<template name="R1" type="INTEGER" x="25.0" y="18.0"/>
<template name="N" type="INTEGER" x="23.0" y="18.0"/>
<color-var domain="Master" name="m" x="20.9375" y="16.0"/>
</nodes>
<edges>
<arc head="P0" kind="OUTPUT" mult="&lt;m&gt;" tail="T0"/>
<arc head="T1" kind="INPUT" mult="&lt;m&gt;" tail="P0"/>
<arc head="P1" kind="OUTPUT" mult="&lt;m&gt;" mult-k="0.74990234375" tail="T1">
<point x="32.00006103515625" y="28.0"/>
</arc>
<arc head="T2" kind="INPUT" mult="&lt;m&gt;" tail="P1"/>
<arc head="P2" kind="OUTPUT" mult="&lt;m&gt;" tail="T2"/>
<arc head="T0" kind="INPUT" mult="&lt;m&gt;" mult-k="0.49990234375" tail="P2">
<point x="39.0" y="31.5"/>
<point x="32.938187931395056" y="31.5"/>
<point x="31.750112153838394" y="31.5"/>
<point x="28.251127266931146" y="31.5"/>
<point x="26.500402888524228" y="31.5"/>
<point x="23.0" y="31.5"/>
</arc>
</edges>
</gspn> </gspn>
<measures gspn-name="CPN" name="Measures" simplified-UI="false"> <measures gspn-name="CPN" name="Measures" simplified-UI="false">
<assignments/> <assignments>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="k"/>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="R2"/>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="R1"/>
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="N"/>
</assignments>
<greatspn/> <greatspn/>
<formulas> <formulas>
<formula comment="Basic statistics of the toolchain execution." language="STAT"/> <formula comment="Basic statistics of the toolchain execution." language="STAT"/>

View file

@ -1,17 +0,0 @@
* VPC
chiede delle decisioni
chiedi della riduzione
chiedi dell'esame
same for meo
galla reti WN con marking simbolici
esercizi
* Prog Mobile
* Apprendimento Automatico
* Tesi

Binary file not shown.

View file

@ -1,6 +1,7 @@
* VPC [2/9] * VPC [2/9]
- [ ] sulle slide, quando si chiede come deve decidere il master - [ ] sulle slide, quando si chiede come deve decidere il master
- [X] chiedi della riduzione - [X] chiedi della riduzione
- [ ] calcolo semiflussi come da mail
- [ ] chiedi dell'esame - [ ] chiedi dell'esame
- [X] Es1: definizioni - [X] Es1: definizioni
- [ ] rete A, b, c, d - [ ] rete A, b, c, d
@ -8,6 +9,8 @@
- [ ] analisi - [ ] analisi
- [ ] uppal - [ ] uppal
- [ ] controlla esercizi nuovi - [ ] controlla esercizi nuovi
- [ ] Controlla bene e studia Symbolic Reachability Graph: perche`
cosi` buono?
* TODO Prog Mobile [2/4] * TODO Prog Mobile [2/4]
- [X] Api all songs - [X] Api all songs