riduzione + trace_eq

anno3/vpc/consegne/3/analisi.org

@@ -88,7 +88,7 @@ AG (#Q1==1 -> EF (#Q3 == 1))
 \includepdf{3.2.jpg}
 ** Algebra dei processi
 Riportiamo il modello dell'algoritmo 3.2 secondo l'algebra dei
-processi.
+processi CSP.
 | System = {(P₁ \vert{}\vert{} Q₁) \vert{}\vert{} Tₚ} \ttvar{/ }Sync
 | S =  {localₚ, local_{q}, criticalₚ, critical_{q}}
 | Sync = {isₚ, is_{q}, setₚ, set_{q}}
@@ -654,7 +654,6 @@ seguente formula CTL:
 che conferma la presenza di deadlock causata dalle due variabili
 booleane.
 \includepdf{3.9.jpg}
-** TODO CCS
 ** Risultati
 Nella tabella mostriamo i risultati ottenuti
 |                     | NuSMV | GreatSPN |
@@ -937,11 +936,12 @@ NuSMV non possiamo rispettare il requisito di fairness.
 | Assenza di deadlock | true  | false    |
 | No Starvation       | true  | false    |
 
-* Bisimulazione
+* Equivalenza in algebra dei processi
 Precedentemente abbiamo modellato usando l'algebra dei processi
 l'algoritmo 3.2 e l'algoritmo 3.6.
 Entrambi hanno le seguenti azioni:
 | S = {localₚ, criticalₚ, local_{q}, critical_{q}} ∪ {τ}
+** Bisimulazione
 Si applica l'algoritmo del partizionamento per verificare
 l'equivalenza tramite bisimulazione.
 Questo lo stato iniziale
@@ -970,6 +970,18 @@ modelli, l'algoritmo raggiunge la terminazione quando non e` piu`
 possibile partizionare gli insieme in base alle azioni comuni e
 abbiamo come risultato che in ogni set compare uno stato di un modello
 insieme ad uno o piu` stati dell'altro.
+** Trace equivalence
+La trace equivalence e` piu` debole della bisimulation equivalence:
+| p ∼ q → p ⋍_{T} q
+ma non viceversa
+| p ∼ q ↛ p ⋍_{T} q
+notiamo subito che una sequenza /s/ dove /criticalₚ/ e /critical_{q}/
+appaiono in successione, non e` una sequenza valida per il modello
+dell'algoritmo 3.2 ma lo e` per il modello dell'algoritmo 3.6.
+| s = ...criticalₚcritical_{q}... 
+| s = ...critical_{q}criticalₚ...
+Questo ci permette di dire che non c'e` trace equivalence fra i due modelli.
+
 * Riduzione
 Le reti dell'algoritmo 3.6 e 3.8 differiscono per la successione delle
 istruzioni di /setTrue/ e /await/ e permettono simmetricamente le

anno3/vpc/consegne/conv/conv.py

@@ -4,7 +4,7 @@ from sys import argv
 
 allsymbols = json.load(open('/home/user/UNITO/anno3/vpc/consegne/conv/unicode-latex.json'))
     
-mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀',  'ε', '₀', '₂', '₁', '₃', '₄', '₅', 'ₐ', 'ₖ', 'ᵥ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒', '∩', '∉', '⋃', 'ᵏ', 'ₗ', 'ˡ', 'ₒ', 'ᵣ', 'ᴵ', '≈', '⊆', '↦', '∪', '⊂', '℘', 'ᶜ', '⁺', 'ⁿ', 'Σ', '⁻', '∑', 'ₚ', 'τ' ]
+mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀',  'ε', '₀', '₂', '₁', '₃', '₄', '₅', 'ₐ', 'ₖ', 'ᵥ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒', '∩', '∉', '⋃', 'ᵏ', 'ₗ', 'ˡ', 'ₒ', 'ᵣ', 'ᴵ', '≈', '⊆', '↦', '∪', '⊂', '℘', 'ᶜ', '⁺', 'ⁿ', 'Σ', '⁻', '∑', 'ₚ', 'τ', '↛', '→', '⋍', '∼' ]
 extrasymbols = {'∈': '\in',
                 '〚': '\llbracket',
                 '〛': r'\rrbracket',

todo.org

@@ -1,4 +1,5 @@
-* TODO VPC [16/19]
+* TODO VPC [16/20]
+- [ ] Controlla good latex
 - [X] chiedi della riduzione
 - [X] calcolo semiflussi come da mail
 - [X] chiedi dell'esame
@@ -18,14 +19,16 @@
   - [ ] Vedi da relazioni procedure dimostrazione deadlock
   - [ ] Impara equivalenze come le spiega lei
   - [ ] Formalizza algoritmo bisimulazione
-- [X] rete A, b, c, d [3/3]
+- [-] rete A, b, c, d [4/5]
   - [X] Spiega p-t-semiflows analysis: deadlock e liveness, boundness
   - [X] sulle slide, quando si chiede come deve  decidere il master
   - [X] Sistema screenshots di GSPN non tagliati
+  - [X] Controlla riduzione se hai fuso posti con archi uscenti
+  - [ ] Rifai la riduzione e controlla fusione con archi uscenti
 - [X] rete E, F -> Controlla sia finito
-- [-] Analisi [19/25]
+- [X] Analisi [26/26]
-  - [ ] Riduzione???
+  - [X] Riduzione???
-  - [ ] Inverti S14 e S13
+  - [X] Inverti S14 e S13
   - [X] Derivation graph errori [5/5]
     - [X] Derivation graph 3.6: aggiungi label local_q R0
     - [X] Derivation graph 3.6: aggiungi label tau R5
@@ -37,12 +40,13 @@
   - [X] Specifica all'inizio che usi condizione piu` bassa per deadlock
   - [X] Riformula liveness
   - [X] Chiedi perche` non riesci a riprodurre i variable ordering mostrati da euristica
-  - [-] Algebra processi [2/3]
+  - [X] Algebra processi [3/3]
     - [X] modellazione
     - [X] rg vs dg
-    - [ ] equivalenza e bisimulazione
+    - [X] equivalenza e bisimulazione
   - [X] 3.2, 3.5 rifai immagini e ctl con nuovi nomi spazi / transizioni
-  - [ ] E` algebra CSP? Specifica
+  - [X] E` algebra CSP? Specifica
+  - [X] metti trace equivalence
   - [X] Vedi necessita` di Sync e /
   - [X] Controlla in 3.6 Starvation: nusmv no, greatspn si`
   - [X] 3.6, deadlock: correttezza spiegazione della differenza greatspn nusmv?
@@ -51,12 +55,12 @@
   - [X] 3.10: si puo` fare model checking senza unfolding?
   - [X] 3.10: correggi GSPN: starvation false???
   - [X] Correggi latex deadlock: G(wₚ|wp' → ...)
-  - [ ] Risolvi riduzione_eliminazione2.jpg
+  - [X] Risolvi riduzione_eliminazione2.jpg
   - [X] Risolvi \ttvar per #
   - [X] non mette i file inclusi nel pdf :(
   - [X] Cosa significa FAIRNESS running alla fine dei .smv
   - [X] chiedi a lei di safety, liveness, fairness
-  - [ ] mi sa non finito
+  - [X] mi sa non finito
 - [X] uppal, es 4 [4/4]
   - [X] Galla`: su uppaal e` stato lui a scegliere i valori numerici_tempo
   - [X] Come si prende intervallo attesa richiesto da Donatelli?