che coglioni

anno3/vpc/orale/orale2.org

@@ -0,0 +1,5 @@
+(l, v)
+
+v: C → R₀⁺
+
+(l,v)

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'

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

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

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