preparazione orale

anno3/vpc/orale/preparazione.org

@@ -1,11 +1,13 @@
 * Simboli:
 - sqcap: ⊓
-- box: □
+- Box: □
 - a\b: a̱
 - Vert: ‖
 - $\underrightarrow{a}$ (toggle latex fragment): $\underrightarrow{a}$
 - varphi: φ
 - models: ⊧
+- Delta: Δ
+- approx: ≈
 
 * 1.1 Petri Nets
 ** Definizione
@@ -116,6 +118,8 @@ La rete si dice conservativa quando:
 La rete si dice consistente quando:
 | ∃x | ||x|| = T
 I flussi sono canonici quando il gcd degli elementi non nulli e` 1.
+Un p-semiflusso o t-semiflusso si dice minimo quando il suo supporto
+non contiene strettamente il supporto di nessun altro semiflusso.
 
 Un insieme generatore Ψ_y e` un insieme del numero minimo di
 p-semiflussi, detti minimi, tali che e` possibile generare gli altri sommandoli
@@ -123,7 +127,7 @@ moltiplicati per un k
 | ∀y: y = ∑ⱼ kⱼyⱼ, kⱼ∈Q, yⱼ∈Ψ
 ** Invarianti
 Legge di conservazione dei token:
-| ∀m: ∀p ∑ₚ y(p)m(p) = ∑ₚy(p)m₀(p)
+| ∀m₀, ∀m∈RS(N.m₀): ∀p ∑ₚ y(p)m(p) = ∑ₚy(p)m₀(p)
 | ∀m: ym = ym₀
 Legge del comportamente ciclico:
 | ∃m₀, ∃σ∈L(S) | mₒ[σ>m₀ ∧ σ=x
@@ -197,7 +201,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'
@@ -233,7 +237,7 @@ E\S $\underrightarrow{\tau}$ E'\S
 ** LTL: grammatica
 | φ ::=  p | (φ) | ¬φ | φ ∧ φ | φ ∨ φ | φ U φ | Gφ | Xφ | Fφ
 Set adeguato di operatori:
-| U ∧ X
+| {U, X}
 - X e` necessario
 - Fφ = true U φ
 - Gφ = ¬F¬φ
@@ -259,4 +263,139 @@ Diciamo che R⁰(s) = s, Rⁿ⁺¹ = R(Rⁿ(s))
 | M,s ⊧ Xφ if R(S) ⊧ φ
 | M,s ⊧ Fφ if ∃j≥0| Rʲ(s) ⊧ φ
 | M,s ⊧ Gφ if ∀j≥0| Rʲ(s) ⊧ φ
-| M,s ⊧ φUψ if ∃j=0, ..., i-1| Rʲ ⊧ φ ∧ Rⁱ ⊧ ψ
+| M,s ⊧ φUψ if ∃j=0, ..., i-1| Rʲ(s) ⊧ φ ∧ Rⁱ(s) ⊧ ψ
+(induzione strutturale su ϕ)
+* 3.2 Computational Tree Logic
+| φ ::= p | ¬φ | φ ∧ φ  | φ ∨ φ | EXφ | EFφ | EGφ | E[φUψ] | AXφ | AFφ | AGφ | A[φUψ] 
+Insieme adeguato di operatori:
+| {EU} ∪ {AX | EX} ∪ {EG | AF | AU}
+Data una struttura M, definiamo un path σ = s₀, s₁, s₂, ... tale che
+| (sᵢ, sᵢ₊₁) ∈ R
+| σᵢ = sᵢ
+| Pₘ(s) = {σ ∈ Sʷ| σ₀ = s}
+Per induzione strutturale su ϕ:
+| M,s ⊧ p iff p∈L(S)
+| M,s ⊧ ¬φ iff ¬(M,s ⊧ φ)
+| or e and
+| M,s ⊧ EXφ iff ∃σ∈Pₘ(s)| σ₁ ⊧ φ
+| M,s ⊧ AXφ iff ∀σ∈Pₘ(s)| σ₁ ⊧ φ
+| M,s ⊧ EFφ iff ∃σ∈Pₘ(s), ∃i≥0| σᵢ ⊧ φ
+| M,s ⊧ AFφ iff ∀σ∈Pₘ(s), ∃i≥0| σᵢ ⊧ φ
+| M,s ⊧ EGφ iff ∃σ∈Pₘ(s), ∀i≥0| σᵢ ⊧ φ
+| M,s ⊧ AGφ iff ∀σ∈Pₘ(s), ∀i≥0| σᵢ ⊧ φ
+| M,s ⊧ E[φUψ] iff ∃σ∈Pₘ(s), ∃i≥0| ∀j=0, ...,i-1 σⱼ ⊧ φ ∧ σᵢ ⊧ ψ
+| M,s ⊧ E[φUψ] iff ∀σ∈Pₘ(s), ∃i≥0| ∀j=0, ...,i-1 σⱼ ⊧ φ ∧ σᵢ ⊧ ψ
+** Comparing LTL and CTL
+| φ_ctl ≡ φ_ltl iff ∀M, M⊧φ(ctl) iff M⊧φ(ltl)
+Data una formula ctl φ e ψ una formula ltl ottenuta rimuovendo gli
+operatori di path da φ:
+| ψ ≡ φ ∨ ∄ (equivalent ltl formula)
+* CTL*
+(state)
+| φ ::= p | ¬φ | φ ∨ φ | φ ∧ φ | Eψ | Aψ
+(path)
+| ψ ::= φ | ¬ψ | ψ ∨ ψ | ψ ∧ ψ | Xψ | Gψ | Fψ | ψUψ
+* 4.1 Time
+Def: a clock is a variable ranging over r⁺. Clock constraints:
+| x < c | x ≤ c | α∈Cstr(C) | ¬α | α ∧ α 
+The set of clock constraints over C is Ψ(C) or Cstr(C).
+** Timed Automata
+Is a 7-uple:
+| A = <Loc, E, L₀, Label, C, Reset, Guard, Inv>
+- L: insieme delle locazioni
+- E: insieme degli archi ⊆ L×L
+- L₀: stato iniziale
+- Label: labeling function L → 2ᴬᴾ
+- C: insieme dei clock
+- Reset: E → 2ᶜ, assegna ad ogni arco il clock da resettare
+- Guard: E → Cstr(c), guardie sugli archi
+- Inv: S → Cstr(c), invarianti delle locazioni
+Definisco /clock valuation/ la funzione
+| v: C → R⁺
+dove v(x) restituisce il valore corrente del clock x.
+| A = <L, v>
+| reset(x in y)(y) = v(y) if y ≠ x else 0
+| v ⊧ x≤c iff v(x)≤c
+| v ⊧ x<c iff v(x)<c
+| v ⊧ ¬α  iff v¬⊧α
+| v ⊧ α∧β iff v⊧α ∧ v⊧β
+** Timed Transition System
+| M(A) = <S, s₀, →>
+- S = {(l, v) ∈ L×V(C) | v⊧inv(l)}
+- s₀ = (l₀, v₀), v₀(x) = 0 ∀x
+- → ⊆ S × R∪{*} × S:
+  1. (l,v)$\underrightarrow{*}$(l', (reset Reset(edge) in v)):
+     + edge ∈ E
+     + v⊧guard(edge)
+     + (reset Reset(edge) in v)⊧inv(l')
+  2. (l,v)$\underrightarrow{d}$(l,v+d):
+     + ∀d'≤d: v+d' ⊧ inv(l)
+*** Path
+Definiamo il path σ di un TTS come una sequenza infinita s₀ →a₀→ s₁,
+...
+dove ∀i sᵢ→aᵢ→sᵢ₊₁ e` una transizione nel TTS.
+il tempo trascorso ▵(s,i) e` definito ricorsivamente come:
+| ▵(s,0) = 0
+| ▵(s,i+1) = ▵(s,i) + aᵢ if aᵢ∈R⁺ else 0 (aᵢ = *)
+σ si dice time divergent se lim(i→∞)▵(σ,i) = ∞
+** TCTL
+CTL + Formula clocks, definito su TTS.
+D = set formula clocks
+| ϕ ::= p | ¬(ϕ) | ϕ∨ϕ | E[ϕUϕ] | A[ϕUϕ] | α∈Cstr(C∪D) | z in ϕ
+- z in ϕ, z∈D: freeze indentifier:
+ | z in ϕ is valid in state s if ϕ holds in s where clock z start from 0
+Esempi:
+| E (ϕ $U^{\le{n}}$ ψ) = reset z in E (ϕ U (z≤n ∧ ψ))
+| $AF^{=n}(\phi)$ = reset z in AF(z = n ∧ ϕ)
+*** TCTL secondo induzione strutturale
+Dati s = (l,v), w∈V(D):
+| s,w ⊧ p if p∈Label(l)
+| s,w ⊧ α if v∪w ⊧ α
+| s,w ⊧ ¬ϕ if ¬(s,w ⊧ ϕ)
+| s,w ⊧ ϕ ∨ ψ if (s,w⊧ϕ ∨ s,w⊧(ψ)
+| s,w ⊧ z in ϕ if s,reset z in w ⊧ ϕ
+| s,w ⊧ E(ϕUψ) if ∃σ∈Pₘ(s), ∃(i,d)∈Pos(σ): 
+       | ∀(j,d')≤(i,d) σ(j,d'),wⱼ ⊧ ϕ    ∧   σ(i,d),wᵢ⊧ψ
+     (dove wⱼ = w+▵(σ,j), wᵢ = w+▵(σ,i))
+| s,w ⊧ E(ϕUψ) if ∀σ∈Pₘ(s), ∃(i,d)∈Pos(σ): 
+       | ∀(j,d')≤(i,d) σ(j,d'),wⱼ ⊧ ϕ    ∧   σ(i,d),wᵢ⊧ψ
+     (dove wⱼ = w+▵(σ,j), wᵢ = w+▵(σ,i))
+
+σ e` una RT trajectory: sequenza infinita di stati
+| σ = s₀ →δ₀→ s₁ →δ₁→ s₂ →...
+| pos di σ = coppia (i,δ)
+| loc(i,δ) = lᵢ
+| val(i,δ) = vᵢ+δ
+| state(i,δ) = (loc,val)
+* Equivalenze
+trace: stesso sequenza di azioni
+trace decorate: stessa sequenza di azioni e una volta eseguite stesso
+insieme di azioni possibili
+bisimulazione: stessa sequenza di azioni e ricorsivamente stesso
+comportamento
+- Failure:
+  definisco Fail(P) = (σ,X):
+  dopo aver eseguito σ, tutte le azioni in X non possono piu` essere
+  abilitate.
+- Simulazione: ∀p,q⊆P×P
+  p ~ q iff ( ∀a: p $\underrightarrow{a}$ p' → ∃q:
+  q\underrightarrow{a}$q' ∧ p' ~ q')
+- Bisimulazione: ∀p,q⊆P×P
+  p≈q iff ∀a: p $\underrightarrow{a}$ p' → ∃q: q $\underrightarrow{a}$  q'
+  and
+          ∀a: q $\underrightarrow{a}$ q' → ∃p: p $\underrightarrow{a}$p'
+** Congruenza
+La bisimulazione e` una congruenza, ovvero 
+B≈ᶜC → A≈A[B/C]
+* Fairness
+- Absolute Fairness: GF(exᵢ)
+  un processo puo` essere eseguitp infinite volte.
+- Strong Fairness: GF(enᵢ) → GF(exᵢ)
+  un processo abilitato infinite volte puo` essere eseguito infinite volte.
+- Weak Fairness: FG(enᵢ) → GF(exᵢ)
+  un processo che da un punto in avanti e` sempre abilitato puo`
+  essere eseguito infinite volte
+La weak fairness e` piu` stringente perche` richiede che da un punto
+in avanti il processo rimanga in stato di abilitazione.
+La strong fairness rilassa questo vincolo "e si accontenta" che il
+processo vada in stato di abilitazione prima di essere eseguito.

media.py

@@ -9,7 +9,9 @@ voti = [
     (24, 9), # ling. formali
     (30, 6), # mcad
     (30, 6), # scpd
-    (26, 9)  # vpc 
+    (26, 9), # vpc 
+    (26, 6), # progmobile 
+    (26, 6)  # meo 
     ]
 
 crediti, voto = sum(map(lambda x: x[1], voti)), sum(map(lambda x: x[0]*x[1], voti))

todo.org

@@ -1,25 +1,18 @@
 * TODO VPC [23/24]
-- [X] Controlla good latex
+- [-] Teoria [31/36]
-- [X] Uppaal muovi cartella file
+  - [ ] PN consistente?
-- [X] Rimuovi "Contents" da ogni .org
+  - [ ] vedi perche \neg\models != \models\neg
-- [X] chiedi della riduzione
+  - [X] Pronuncia / nome P_m(S)
-- [X] calcolo semiflussi come da mail
+  - [X] In ctl come dico:  M,s ⊧ φ if ∀σ| σ₀ = s, σ ⊧ φ (ogni path
-- [X] chiedi dell'esame
+  - [ ] ripeti fairness
-- [X] Es1: definizioni
+  - [ ] fai buchi
-- [X] Rimuovi parte in cui parli di archi inibitori
+  - [X] fai equivalenze
-- [X] Chiedi a Daniel come da p-semiflows deadlock
+  - [ ] Vedi step semantic e enabling degree
-- [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 ==
-- [-] Teoria [26/29]
   - [X] Come metti a parole \to ?
   - [X] Hierarchy of equivalences
   - [X] Automa di Buchi
   - [X] Ultimo pacco BDD e CTL
-  - [ ] Prodotto relazionale BDD
+  - [X] Prodotto relazionale BDD
   - [X] Def formale struttura Kripke
   - [X] algebra.extra.lucca: internal/external choices
   - [X] Observer e testing equivalence
@@ -39,11 +32,25 @@
   - [X] Equivalenza clock. Davvero mantissa e parte frazionaria?
   - [X] Galla`: che devo dire sulle WN?
   - [X] Rivedi WN
-  - [ ] Pagina 2: fondo state eq
+  - [X] Pagina 2: fondo state eq
   - [X] Ripeti preset e postset
-  - [ ] PN consistente?
   - [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
@@ -99,11 +106,11 @@
 - [X] Confrontare esercizi con Galla`
 
 
-* Prog Mobile [3/6]
+* Prog Mobile [4/6]
 - [X] Api all songs
 - [X] relazione
 - [X] slides
-- [ ] teoria
+- [X] teoria
 - [ ] account prof
 - [ ] Vnc sul fisso