diff --git a/anno3/vpc/orale/ltximg/org-ltximg_ca3554cbe8c0a6f9882a2ded38b78d4678296f5c.png b/anno3/vpc/orale/ltximg/org-ltximg_ca3554cbe8c0a6f9882a2ded38b78d4678296f5c.png new file mode 100644 index 0000000..e4551ed Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_ca3554cbe8c0a6f9882a2ded38b78d4678296f5c.png differ diff --git a/anno3/vpc/orale/orale2.org b/anno3/vpc/orale/orale2.org new file mode 100644 index 0000000..9155e24 --- /dev/null +++ b/anno3/vpc/orale/orale2.org @@ -0,0 +1,5 @@ +(l, v) + +v: C → R₀⁺ + +(l,v) diff --git a/anno3/vpc/orale/preparazione.org b/anno3/vpc/orale/preparazione.org index cb9c6a6..c1d1156 100644 --- a/anno3/vpc/orale/preparazione.org +++ b/anno3/vpc/orale/preparazione.org @@ -204,7 +204,7 @@ F $\underrightarrow{\mu}$ F' ————————————–– E ‖ F $\underrightarrow{\mu}$ E ‖ F' *** Evoluzione con sincronizzazione -E \underrightarrow{a} E' +E $\underrightarrow{a}$ E' F $\underrightarrow{\underline{a}}$ F' ————————————–––(a≠τ) (CCS) E ‖ F $\underrightarrow{\tau}$ E' ‖ F' diff --git a/anno3/vpc/orale/ripeti.org b/anno3/vpc/orale/ripeti.org index 1fcd51c..9ee55e9 100644 --- a/anno3/vpc/orale/ripeti.org +++ b/anno3/vpc/orale/ripeti.org @@ -14,6 +14,9 @@ Diciamo che R⁰(s) = s, Rⁿ⁺¹ = R(Rⁿ(s)) Per induzione strutturale su ϕ: | M,s ⊧ p iff p∈L(S) | M,s ⊧ ¬φ iff ¬(M,s ⊧ φ) +** Operatori derivati +- EGφ = ¬AF¬φ +- AXφ = ¬EX¬φ ** TCTL CTL + Formula clocks, definito su TTS. D = set formula clocks diff --git a/media.py b/media.py index ca7f12b..8ce8307 100644 --- a/media.py +++ b/media.py @@ -9,9 +9,9 @@ voti = [ (24, 9), # ling. formali (30, 6), # mcad (30, 6), # scpd - (26, 9), # vpc - (26, 6), # progmobile - (26, 6) # meo + (27, 9), # vpc + (30, 6), # progmobile + (28, 6) # meo ] crediti, voto = sum(map(lambda x: x[1], voti)), sum(map(lambda x: x[0]*x[1], voti)) diff --git a/todo.org b/todo.org index 57a266d..b71218d 100644 --- a/todo.org +++ b/todo.org @@ -1,111 +1,3 @@ -* TODO VPC [24/24] -- [X] Teoria [36/36] - - [X] PN consistente? - - [X] vedi perche \neg\models != \models\neg - - [X] fai buchi - - [X] Vedi step semantic e enabling degree - - [X] Pronuncia / nome P_m(S) - - [X] In ctl come dico: M,s ⊧ φ if ∀σ| σ₀ = s, σ ⊧ φ (ogni path - - [X] ripeti fairness - - [X] fai equivalenze - - [X] Come metti a parole \to ? - - [X] Hierarchy of equivalences - - [X] Automa di Buchi - - [X] Ultimo pacco BDD e CTL - - [X] Prodotto relazionale BDD - - [X] Def formale struttura Kripke - - [X] algebra.extra.lucca: internal/external choices - - [X] Observer e testing equivalence - - [X] Vedi bene legge conservazione token - - [X] Vedi bene fairness, liveness come formule? - - [X] Vedi da relazioni procedure dimostrazione deadlock - - [X] Impara equivalenze come le spiega lei - - [X] Formalizza algoritmo bisimulazione - - [X] Vedi slide 42 ltl: liveness, safety, fairness, anche in CTL - - [X] CTL e LTL: set operatori minimo per derivare altri - - [X] Manca CTL* ? - - [X] Pstate? stato che appartiene al linguaggio (o set di label) - - [X] BDD e decision diagrams, tutto Amparore - - [X] Galla`: TCTL z in \phi - - [X] Slide 44 TCTL? reset? - - [X] Slides 49-50 di TCTL - - [X] Equivalenza clock. Davvero mantissa e parte frazionaria? - - [X] Galla`: che devo dire sulle WN? - - [X] Rivedi WN - - [X] Pagina 2: fondo state eq - - [X] Ripeti preset e postset - - [X] Perche` sono utili gli t-semiflussi? PN consistente? - - [X] Assicurati di sapere le sigle -- [X] Controlla good latex -- [X] Uppaal muovi cartella file -- [X] Rimuovi "Contents" da ogni .org -- [X] chiedi della riduzione -- [X] calcolo semiflussi come da mail -- [X] chiedi dell'esame -- [X] Es1: definizioni -- [X] Rimuovi parte in cui parli di archi inibitori -- [X] Chiedi a Daniel come da p-semiflows deadlock -- [X] Chiedi a Daniel come da p-semiflows liveness -- [X] spiega nelle relazioni che bounded se RS finito -- [X] spiega nelle relazioni che bounded quando coperta da p-semiflows -- [X] Vedi bisimulazione ed equivalenze in teoria analisi -- [X] Che significa urgente in uppaal? -- [X] Uppaal: x = 0 come guardia, non == -- [X] rete A, b, c, d [6/6] - + [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 - + [X] Rifai la riduzione e controlla fusione con archi uscenti - + [X] chiedi Daniel riduzione -- [X] rete E, F -> Controlla sia finito -- [X] Analisi [27/27] - - [X] clearpage su ultime immagini - - [X] Riduzione??? - - [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 - - [X] Derivation graph 3.6: aggiungi label critical_q R16 - - [X] Derivation graph 3.6: aggiungi label local_q R20 - - [X] Derivation graph 3.2: aggiungi label S14 - - [X] Spiega perche` non hai usato process - - [X] Riguardo RGGMED4, non posso scrivere ltl equiparabile a ctl? - - [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 - - [X] Algebra processi [3/3] - - [X] modellazione - - [X] rg vs dg - - [X] equivalenza e bisimulazione - - [X] 3.2, 3.5 rifai immagini e ctl con nuovi nomi spazi / transizioni - - [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? - - [X] 3.6, starvation: perche` nusmv con processi non ha starvation? - - [X] 3.6, inserisci controesempi dove necessario - - [X] 3.10: si puo` fare model checking senza unfolding? - - [X] 3.10: correggi GSPN: starvation false??? - - [X] Correggi latex deadlock: G(wₚ|wp' → ...) - - [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 - - [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? - - [X] Fai intervallo attesa - - [X] Cambia nomi -- [X] CSP: che significa sync? -- [X] controlla esercizi nuovi -- [X] Controlla bene e studia Symbolic Reachability Graph: perche` cosi` buono? -- [X] Confrontare esercizi con Galla` - - * Prog Mobile [4/6] - [X] Api all songs - [X] relazione