* Rete A
M master identici e S slave identici di tipo 1.

#+CAPTION: Modello della reteA
[[./reteA.jpg]]

La figura rappresenta la rete di Petri P/T dell'esercizio A. Il master
è modellato dai posti M0, M1, M2, M3 e dalle transizioni
Azione_Locale, Richiesta_Servizio, Attesa_Elaborazione e Reset_M
Lo slave è modellato dai posti S0, S1_a, S1_b, S2_a, S2_b e
S3 e dalle transizioni Inizio_Servizio, Azione_Locale_Sa,
Azione_Locale_Sb, Fine_Servizio e Reset_S. La richiesta del servizio
verso lo slave e` gestita attraverso due buffer, posti Buffer_Input e
posto Buffer_Output.

** Risultati
Nella tabella vengono mostrate il numero di archi e di nodi al variare
dei parametri M e S. Le cifre sono indicative dell'aumentare della
dimensione dello spazio degli stati proporzionalmente al numero di
marcature.

| master, slaves |    Nodi |    Archi |
|----------------+---------+----------|
| 1, 1           |      14 |       19 |
| 2, 2           |      94 |      222 |
| 3, 3           |     426 |      334 |
| 4, 4           |    1500 |     5610 |
| 5, 5           |    4422 |    18720 |
| 6, 6           |   11418 |    52998 |
| 7, 7           |   26598 |   132594 |
| 8, 8           |   57057 |   301158 |
| 9, 9           |  114400 |   632775 |
| 10, 10         |  216788 |  1246960 |
| 11, 11         |  391612 |  2328612 |
| 12, 12         |  678912 |  4153916 |
| 13, 13         | 1135668 |  7123272 |
| 14, 14         | 1841100 | 11802420 |
| 15, 15         | 2903124 | 18973020 |

** Considerazioni su Fork/Join
Il modello non garantisce che avvenga il join di due processi dello
stesso padre quando la marcatura degli slave e` maggiore di 2.
Si puo` garantire che avvenga il join di due processi forkati dallo
stesso padre nei seguenti modi:
- attraverso differenti strutture slaves
- usando reti WN


** Riduzione
Una rete di petri puo` essere ridotta usando le seguendi tecniche:
- fusione
- eliminazione
- rimozione dei loop
Nelle figure vengono mostrate alcune fasi di riduzione della rete in
analisi; in ordine sono stati applicati:
- fusione di alcuni posti
- fusione di alcune transizioni
- eliminazione di alcuni posti
- eliminazione di alcune transizioni
- riduzione di self loop

[[./riduzione/fusione1.jpg]]
[[./riduzione/fusione2.jpg]]
[[./riduzione/eliminazione1.jpg]]
# [[./riduzione/eliminazione2.jpg]]
[[./riduzione/rimozione1.jpg]]
** P e T invarianti
Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi

#+CAPTION: T-semiflows
[[./semiflowsAT.jpg]]
#+CAPTION: P-semiflows
[[./semiflowsAP.jpg]]

Gli P-semiflussi sono i seguenti:
| S0 + S1_a + S2_a + S3
| S0 + S1_b + S2_b + S3
| M0 + M1 + M2 + M3
| S1_a + S2_a + Buffer_output + Buffer_input + M0 + M1 + M3
| S1_b + S2_b + Buffer_output + Buffer_input + M0 + M1 + M3
Il T-semiflusso e` il seguente:
\[
Inizio_servizio + azione_locale_sa + azione_locale_sb + \\
Fine_servizio + Reset_s + azione_locale_m + Richiesta_servizio +  \\
Attesa_elaborazione + Reset_m + Reset_s
\]
e dato che comprende tutte le transizioni, il sistema rispetta la
proprieta` di liveness.
Dato che la reteA e` interamente coperta dagli P-semiflussi, possiamo
affermare che la rete sia bounded.
Gli P-semiflussi ci permettono di ricavare i seguenti invarianti
lineari relativi ai marking /m/:
| m[S0] + m[S1ₐ] + m[S2ₐ] + m[S3] = 1
| m[S0] + m[S1_{b}] + m[S2_{b}] + m[S3] = 1
| m[M0] + m[M1] + m[M2] + m[M3] = 1
| m[S1ₐ] + m[S2ₐ] + m[Buffer_output] + m[Buffer_input] + m[M0] + m[M1] + m[M3] = 1
| m[S1_{b}] + m[S2_{b}] + m[Buffer_output] + m[Buffer_input] + m[M0] + m[M1] + m[M3] = 1
Dato che ∀p ∈ P, m[p] ≥ 0 possiamo affermare, a partire dalle
precedenti uguaglianze che:
- ogni posto nei seguenti insieme e` in mutua esclusione con gli
  elementi dello stesso insieme:
  | {S0, S1ₐ, S2ₐ, S3}
  | {S0, S1_{b}, S2_{b}, S3}
  | {M0, M1, M2, M3}
  | {S1ₐ, S2ₐ, Buffer_output, Buffer_input, M0, M1, M3}
  | {S1_{b}, S2_{b}, Buffer_output, Buffer_input, M0, M1, M3}
- ∀pᵢ∈P, m[pᵢ]≤1 (bounds)
- dato che i posti che sono gli unici /enablers/ di una transizione
  sono i seguenti:
  | S1ₐ, S1_{b}, S3, M0, M1, M3
  e quindi possiamo provare a dimostrare l'assenza di deadlock
  partendo dagli invarianti lineari relativi ai marking:
  | m[S0] + m[S2ₐ] = 1
  | m[S0] + m[S2_{b}] = 1
  | m[M2] = 1
  | m[S2ₐ] + m[Buffer_output] + m[Buffer_input] = 1
  | m[S2_{b}] + m[Buffer_output] + m[Buffer_input] = 1
  Dato che M2 e` marcata, per far si` che /attesa_elaborazione/ non
  venga abilitata:
  | m[Buffer_output] = 0
  Inoltre per far si` che /Inizio_Servizio/ e /Fine_Servizio/ non vengano abilitate:
  | m[Buffer_input] + M[S0] ≤ 1
  | m[S2ₐ] + m[S2_{b}] ≤ 1
  Riassumendo, il sistema e` il seguente:
  | m[S0] + m[S2ₐ] = 1
  | m[S0] + m[S2_{b}] = 1
  | m[S2ₐ] + m[Buffer_input] = 1
  | m[S2_{b}] + m[Buffer_input] = 1
  | m[Buffer_input] + M[S0] ≤ 1
  | m[S2ₐ] + m[S2_{b}] ≤ 1
  che per la legge di conservazione dei token, non puo` essere
  soddisfatto. Quindi nel sistema non vi e` la possibilita` di deadlock.

* Rete B
M master identici, uno slave di tipo 1 e uno slave di tipo 1 scelti
liberamente dai master.

#+CAPTION: Modello della reteB
[[./reteB.jpg]]

La figura rappresenta la rete di Petri P/T dell'esercizio B. Il master
è modellato dai posti M0, M1, M2, M3 e dalle transizioni
Azione_Locale, Richiesta_Servizio, Attesa_Elaborazione e Reset_M
Lo slave di tipo 1 è modellato dai posti S0, S1_a, S1_b, S2_a, S2_b e
S3 e dalle transizioni Inizio_Servizio, Azione_Locale_Sa,
Azione_Locale_Sb, Fine_Servizio e Reset_S. 
Lo slave di tipo 2 è modellato dai posti R0, R1_a, R1_b, R2_a, R2_b e
R3 e dalle transizioni Inizio_Servizio_R, Azione_Locale_R, Fine_Servizio e Reset_R. 
La richiesta del servizio
verso lo slave scelto e` gestita attraverso due buffer, posti
FreeChoice e Risultato.


** Risultati
| master, slaves |  Stati |  Archi |
|----------------+--------+--------|
| 1, 2           |     40 |     76 |
| 2, 2           |    204 |    544 |
| 3, 2           |    728 |   2400 |
| 4, 2           |   2072 |   7896 |
| 5, 2           |   5040 |  21336 |
| 6, 2           |  10920 |  50064 |
| 7, 2           |  21648 | 105648 |
| 8, 2           |  39996 | 205260 |
| 9, 2           |  69784 | 373252 |
| 10, 2          | 116116 | 642928 |

Parametrizzando anche il numero di slaves:
| master, slaves |   Stati |    Archi |
|----------------+---------+----------|
| 1, 2           |      40 |       76 |
| 2, 2           |     204 |      544 |
| 4, 4           |    7265 |    32674 |
| 6, 6           |  113464 |   664234 |
| 8, 8           | 1073226 |  7405654 |
| 10, 10         | 7212128 | 55762000 |

** Considerazioni su Fork/Join
Lo slave di tipo 1 processa una sola richiesta alla volta.
Il master in attesa del risultato (M2) potrebbe ricevere il risultato
di un lavoro richiesto da un altro master.

** P e T invarianti
Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi

#+CAPTION: T-semiflows
[[./semiflowsBT.jpg]]
#+CAPTION: P-semiflows
[[./semiflowsBP.jpg]]

Gli P-invarianti sono i seguenti:
| S0 + S1_a + S2_a + S3
| S0 + S1_b + S2_b + S3
| R0 + R1 + R2 + R3
| M0 + M1 + M2 + M3
| S1_a + S2_a + R1 + R2 + M0 + M1 + M3 + Freechoice + P0 + P1 + Risultato
| S1_b + S2_b + R1 + R2 + M0 + M1 + M3 + Freechoice + P0 + P1 + Risultato
Gli T-invarianti sono i seguenti:
\[
Inizio_servizio_R + azione_locale_R + \\
Fine_servizio_R + Reset_R + azione_locale_m + Richiesta_servizio +  \\
Attesa_elaborazione + Reset_M + Scelta_2
\]
\[
Inizio_servizio_S + azione_locale_sa + azione_locale_sb + \\
Fine_servizio_S + Reset_s + azione_locale_m + Richiesta_servizio +  \\
Attesa_elaborazione + Reset_m + Scelta_1
\]
Dato che ci sono due semiflussi, ognuno relativo alle transizioni dei
due diversi slaves, c'e` possibilita` di starvation.
Possiamo infatti immaginare una traccia di esecuzione in cui il master
in seguito a FreeChoice sceglie sempre il primo slave.
Questo non succederebbe in un sistema fair, ovvero se si obbliga
un'automa che entra in uno stato infinite volte ad eseguire tutte le
possibili transizioni da quello stato.
In tal caso non avremmo starvation e la proprieta` di liveness sarebbe rispettata.

Dato che la reteB e` interamente coperta dagli P-semiflussi, possiamo
affermare che la rete sia bounded.
Dimostriamo invece che la rete non ha possibilita` di deadlock.
| m[S0] + m[S1_a] + m[S2_a] + m[S3] = 1
| m[S0] + m[S1_{b}] + m[S2_{b}] + m[S3] = 1
| m[R0] + m[R1] + m[R2] + m[R3] = 1
| m[M0] + m[M1] + m[M2] + m[M3] = 1
| m[S1_a] + m[S2_a] + m[R1] + m[R2] + m[M0] + m[M1] + m[M3] + m[Freechoice] + m[P0] + m[P1] + m[Risultato] = 1
| m[S1_{b}] + m[S2_{b}] + m[R1] + m[R2] + m[M0] + m[M1] + m[M3] + m[Freechoice] + m[P0] + m[P1] + m[Risultato] = 1
I posti che sono gli unici enablers di una sola transizione sono:
|  M0, M1, M3, R1, R2, R3, FreeChoice, S1ₐ, S1_{b}, S3
Gli invarianti lineari dei marking diventano:
| m[S0] + m[S2_a] = 1
| m[S0] + m[S2_{b}] = 1
| m[R0] = 1
| m[M2] = 1
| m[S2_a] + m[P0] + m[P1] + m[Risultato] = 1
| m[S2_{b}] m[P0] + m[P1] + m[Risultato] = 1
Dati i marking in R0 e M2, per far si` che /Inizio_Servizio_R/,
/Attesa_Elaborazione/, /Fine_Servizioₛ/ e /Inizio_Servizioₛ/ non vengano abilitati:
| m[P0] = 0
| m[Risultato] = 0
| m[S2ₐ] + m[S2_{b}] ≤ 1
| m[P1] + m[S0] ≤ 1
Il sistema si riduce a:
| m[S0] + m[S2_a]= 1
| m[S0] + m[S2_{b}] = 1
| m[S2_a] + m[P1] = 1
| m[S2_{b}] + m[P1] = 1
| m[S2ₐ] + m[S2_{b}] ≤ 1
| m[P1] + m[S0] ≤ 1
che non puo` essere soddisfatto per la legge di conservazione dei token.

* Rete C
Due master identici, uno slave di tipo 1 e uno slave di tipo 1 scelti
liberamente dai master.

#+CAPTION: Modello della reteC
[[./reteC.jpg]]

La figura rappresenta la rete di Petri P/T dell'esercizio C. Il master
è modellato dai posti M0, M1, M2, M3 e dalle transizioni
Azione_Locale, Richiesta_Servizio, Attesa_Elaborazione e Reset_M
Lo slave di tipo 1 è modellato dai posti S0, S1_a, S1_b, S2_a, S2_b e
S3 e dalle transizioni Inizio_Servizio, Azione_Locale_Sa,
Azione_Locale_Sb, Fine_Servizio e Reset_S (il secondo master e` una
copia del primo). 
Lo slave di tipo 2 è modellato dai posti R0, R1_a, R1_b, R2_a, R2_b e
R3 e dalle transizioni Inizio_Servizio_R, Azione_Locale_R, Fine_Servizio e Reset_R. 
La richiesta del servizio
verso lo slave scelto e` gestita attraverso due buffer, posti
FreeChoice e Risultato.
** P e T invarianti
Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi

#+CAPTION: T-semiflows
[[./semiflowsCT.jpg]]
#+CAPTION: P-semiflows
[[./semiflowsCP.jpg]]

Gli P-invarianti sono i seguenti:
- S0 + S1ₐ + S2ₐ + S3
- S0 + S1_{b} + S2_{b} + S3
- R0 + R1 + R2 + R3
- M0 + M1 + M2 + M3
- copy_M0 + copy_M1 + copy_M2 + copy_M3
- S1ₐ + S2ₐ + R1 + R2 + M0 + M1 + M3 + Freechoice + P0 + P1 +
  Risultato + copy_M0 + copy_M1 + copy_M3
- S1_{b} + S2_{b} + R1 + R2 + M0 + M1 + M3 + Freechoice + P0 + P1 +
  Risultato + copy_M0 + copy_M1 + copy_M3
Dato che la reteC e` interamente coperta dagli P-semiflussi, possiamo
affermare che la rete sia bounded.
Gli P-semiflussi ci permettono di ricavare i seguenti invarianti
lineari relativi ai marking /m/:
| m[S0] + m[S1ₐ] + m[S2ₐ] + m[S3] = 1
| m[S0] + m[S1_{b}] + m[S2_{b}] + m[S3] = 1
| m[R0] + m[R1] + m[R2] + m[R3] = 1
| m[M0] + m[M1] + m[M2] + m[M3] = 1
| m[copy_M0] + m[copy_M1] + m[copy_M2] + m[copy_M3] = 1
\[
  m[S1ₐ] + m[S2ₐ] + m[R1] + m[R2] + m[M0] + m[M1] + m[M3] + m[Freechoice] + m[P0] + m[P1] +
  m[Risultato] + m[copy_M0] + m[copy_M1] + m[copy_M3] = 1
\]
\[
  m[S1_{b}] + m[S2_{b}] + m[R1] + m[R2] + m[M0] + m[M1] + m[M3] + m[Freechoice] + m[P0] + m[P1] +
  m[Risultato] + m[copy_M0] + m[copy_M1] + m[copy_M3] = 1
\]
Gli spazi /enablers/ di una sola transizione sono i seguenti:
| R1, R2, R3, S1ₐ, S1_{b}, S3, Risultato, M0, M1, M3, copy_M0, copy_M1, copy_M3, FreeChoice
il sistema precedente diventa:
| m[S0] + m[S2ₐ] = 1
| m[S0] + m[S2_{b}] = 1
| m[R0] = 1
| m[M2] = 1
| m[copy_M2] = 1
| m[S2_{b}] + m[P0] + m[P1] = 1
| m[S2_{a}] + m[P0] + m[P1] = 1
Dati i marking in R0 e M2 e copy_M2, per far si` che /Inizio_Servizio_R/,
/Attesa_Elaborazione/, /copy_Attesa_Elaborazione/, /Fine_Servizioₛ/ e /Inizio_Servizioₛ/ non vengano abilitati:
| m[P0] = 0
| m[Risultato] = 0
| m[S2ₐ] + m[S2_{b}] ≤ 1
| m[P1] + m[S0] ≤ 1
Il sistema si riduce allo stesso della precedente rete B:
| m[S0] + m[S2ₐ] = 1
| m[S0] + m[S2_{b}] = 1
| m[S2_{b}] + m[P1] = 1
| m[S2_{a}] + m[P1] = 1
| m[S2ₐ] + m[S2_{b}] ≤ 1
| m[P1] + m[S0] ≤ 1
e non puo` essere soddisfatto per la legge di conservazione dei token.

Gli T-invarianti sono i seguenti:
- Inizio_Servizioᵣ + Azione_Locale + Fine_Servizioᵣ + T3 +
  azione_localeₘ + Richiesta_Servizio + Attesa_Elaborazione + Reset_M + Scelta₁
- Inizio_Servizioₛ + Azione_Locale_{sa} + Azione_Locale_{sb} + Fine_Servizioₛ + T3 +
  azione_localeₘ + Richiesta_Servizio + Attesa_Elaborazione +
  Reset_M + Scelta₁
- Inizio_Servizioᵣ + Azione_Locale + Fine_Servizioᵣ + T3 + Scelta₂ +
  copyₐzione_localeₘ + copy_Richiesta_Servizio +
  copy_Attesa_Elaborazione + copy_Resetₘ
- Inizio_Servizioₛ + Azione_Locale_{sa} + Azione_Locale_{sb} +
  Fine_Servizioₛ + Reset + Scelta₁ + copy_azione_localeₘ +
  copy_Richiesta_Servizio + copy_Attesa_Elaborazione + copy_Resetₘ
Come nella rete B, in assenza di fairness non possiamo rispettare la
condizione di liveness e c'e` possibilita` di starvation.

* Rete D
Due master identici, uno slave di tipo 1 e uno slave di tipo 1 scelti
associati ciascuno ad un master diverso.

#+CAPTION: Modello della reteD
[[./reteD.jpg]]

** P e T invarianti
Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi

#+CAPTION: T-semiflows
[[./semiflowsDT.jpg]]
#+CAPTION: P-semiflows
[[./semiflowsDP.jpg]]

Gli P-invarianti sono i seguenti:
- S0 + S1ₐ + S2ₐ + S3
- S0 + S1_{b} + S2_{b} + S3
- R0 + R1 + R2 + R3
- M0 + M1 + M2 + M3
- S1ₐ + S2ₐ + M0 + M1 + M3 + Bufferₛ + Risultato
- S1_{b} + S2_{b} + M0 + M1 + M3 + Bufferₛ + Risultato
- M0₂ + M1₂ + M3₂
- R1 + R2 + M0₂ + M1₂ + M3₂ + Buffer₂ + Risultato₂
Ai fini della dimostrazione dell'assenza di deadlock, possiamo notare
che lo slave di tipo 2 e` equivalente allo slave di tipo 1 se
si applicano due riduzioni alla rete (vengono fusi in un unico posto
S1ₐ-S2ₐ e S1_{b}-S2_{b}, poi eliminata la fork).
Inoltre i master sono indipendenti fra di loro e ciascuno rispetta l'assenza
di deadlock come gia` dimostrato nella rete A.
Gli T-invarianti sono i seguenti:
- Inizio_Servizioₛ + azione_locale_{sa} + azione_locale_{sb} +
  Fine_Servizioₛ + Reset + azione_localeₘ + Richiesta_Servizio +
  Attesa_Elaborazione + Resetₘ
- Inizio_Servizioᵣ + Azione_locale + Fine_Servizioᵣ + T3
  azione_locale_{m2} + Richiesta_Servizio₂ + Attesa_Elaborazione₂ +
  Reset_{m2}
Come nella rete B, in assenza di fairness non possiamo rispettare la
condizione di liveness e c'e` possibilita` di starvation.

** Decision Diagram
L'efficacia dei decision diagram sulla generazione dello stato degli
spazi dipende fortemente dall'ordine delle variabili.
Di seguito vengono mostrati i decision diagram usando per le
assegnazioni i seguenti algoritmi:
- Sloan: un algoritmo di riduzione della banda di matrici sparse con
  una buona performance
- (advanced) Cuthill-McKee: un altro algoritmo di riduzione della banda di
  matrici sparse
-  Tovchigrechko e Noack: due algoritmo appositamente ideati per le reti
  di Petri, anch'essi con una buona performance
- P-chaining: un algoritmo che sfrutta le informazioni strutturali
  della rete ma ha una bassa performance
- Gradient-P
- Gibbs-Poole-Stockmeier: un altro algoritmo matriciale che nella rete
  in analisi ha restituito il risultato peggiore
 
#+CAPTION: Algoritmo di Sloan
[[./diagrammi/sloan.jpg]]
#+CAPTION: Algoritmo di Cuthull-McKee
[[./diagrammi/mckee.jpg]]
#+CAPTION: Algoritmo di Tovchigrechko
[[./diagrammi/tovchi.jpg]]
#+CAPTION: Algoritmo di Noack
[[./diagrammi/noack.jpg]]
#+CAPTION: Algoritmo P-Chain
[[./diagrammi/p-chain.jpg]]
#+CAPTION: Algoritmo Gradient-P
[[./diagrammi/gradient.jpg]]
#+CAPTION: Algoritmo di Gibbs-Poole-Stockmeier
[[./diagrammi/gibbs.jpg]]