diff --git a/anno3/vpc/3.logica/extra.08.uniroma.pdf b/anno3/vpc/3.logica/extra.08.uniroma.pdf new file mode 100644 index 0000000..a9ba44f Binary files /dev/null and b/anno3/vpc/3.logica/extra.08.uniroma.pdf differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_012778b8b059cf4680057a6c41b26c9bc84dd32a.png b/anno3/vpc/orale/ltximg/org-ltximg_012778b8b059cf4680057a6c41b26c9bc84dd32a.png new file mode 100644 index 0000000..1494217 Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_012778b8b059cf4680057a6c41b26c9bc84dd32a.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_0cf5d70c79f2803c12fa3d2679b73ddb17d16817.png b/anno3/vpc/orale/ltximg/org-ltximg_0cf5d70c79f2803c12fa3d2679b73ddb17d16817.png new file mode 100644 index 0000000..16ab4b6 Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_0cf5d70c79f2803c12fa3d2679b73ddb17d16817.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_10231efdfc4cb2c2547c59e42929b6d72e08d207.png b/anno3/vpc/orale/ltximg/org-ltximg_10231efdfc4cb2c2547c59e42929b6d72e08d207.png new file mode 100644 index 0000000..56508e3 Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_10231efdfc4cb2c2547c59e42929b6d72e08d207.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_1ac98c4af938c84f8fca79bc738f1bd7bf0e9bde.png b/anno3/vpc/orale/ltximg/org-ltximg_1ac98c4af938c84f8fca79bc738f1bd7bf0e9bde.png new file mode 100644 index 0000000..f70290e Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_1ac98c4af938c84f8fca79bc738f1bd7bf0e9bde.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_3a25104356c451d265d445b331880ba6f9139859.png b/anno3/vpc/orale/ltximg/org-ltximg_3a25104356c451d265d445b331880ba6f9139859.png new file mode 100644 index 0000000..3b922af Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_3a25104356c451d265d445b331880ba6f9139859.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_3f1d461baf849836e900330ecd79aaa791843e5d.png b/anno3/vpc/orale/ltximg/org-ltximg_3f1d461baf849836e900330ecd79aaa791843e5d.png new file mode 100644 index 0000000..c5b521d Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_3f1d461baf849836e900330ecd79aaa791843e5d.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_4c2f8b79bffaf430a857f0948d7ce3fbdbedb049.png b/anno3/vpc/orale/ltximg/org-ltximg_4c2f8b79bffaf430a857f0948d7ce3fbdbedb049.png new file mode 100644 index 0000000..a14f238 Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_4c2f8b79bffaf430a857f0948d7ce3fbdbedb049.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_54305deb63be1832e8b46c5f0ea19e974b3564ac.png b/anno3/vpc/orale/ltximg/org-ltximg_54305deb63be1832e8b46c5f0ea19e974b3564ac.png new file mode 100644 index 0000000..5652525 Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_54305deb63be1832e8b46c5f0ea19e974b3564ac.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_559aa6ba091f0160ea1e394cc1d0df9cc1644125.png b/anno3/vpc/orale/ltximg/org-ltximg_559aa6ba091f0160ea1e394cc1d0df9cc1644125.png new file mode 100644 index 0000000..43ca25a Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_559aa6ba091f0160ea1e394cc1d0df9cc1644125.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_6692d4c5d3be24047e32835aa1f90daf674e3728.png b/anno3/vpc/orale/ltximg/org-ltximg_6692d4c5d3be24047e32835aa1f90daf674e3728.png new file mode 100644 index 0000000..2c061bb Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_6692d4c5d3be24047e32835aa1f90daf674e3728.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_7159e370f3bc4d3d40b961010d25239025434fe2.png b/anno3/vpc/orale/ltximg/org-ltximg_7159e370f3bc4d3d40b961010d25239025434fe2.png new file mode 100644 index 0000000..6df0bbf Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_7159e370f3bc4d3d40b961010d25239025434fe2.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_7a2ff50b7ced02956eeff4794cf48daca5ff9c49.png b/anno3/vpc/orale/ltximg/org-ltximg_7a2ff50b7ced02956eeff4794cf48daca5ff9c49.png new file mode 100644 index 0000000..ebca669 Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_7a2ff50b7ced02956eeff4794cf48daca5ff9c49.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_a78fe411872c69834cf11b35fa958d60f4f63d22.png b/anno3/vpc/orale/ltximg/org-ltximg_a78fe411872c69834cf11b35fa958d60f4f63d22.png new file mode 100644 index 0000000..8254d50 Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_a78fe411872c69834cf11b35fa958d60f4f63d22.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_b072533a42fd05bf099d44e25618a6b38737c573.png b/anno3/vpc/orale/ltximg/org-ltximg_b072533a42fd05bf099d44e25618a6b38737c573.png new file mode 100644 index 0000000..43ca25a Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_b072533a42fd05bf099d44e25618a6b38737c573.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_e07fd96afb5997688b5b6749dc761e989cd5b595.png b/anno3/vpc/orale/ltximg/org-ltximg_e07fd96afb5997688b5b6749dc761e989cd5b595.png new file mode 100644 index 0000000..12f085b Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_e07fd96afb5997688b5b6749dc761e989cd5b595.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_fd341c4a323bcf81792cc59bd3bd5d3165f4b8b2.png b/anno3/vpc/orale/ltximg/org-ltximg_fd341c4a323bcf81792cc59bd3bd5d3165f4b8b2.png new file mode 100644 index 0000000..2bd0971 Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_fd341c4a323bcf81792cc59bd3bd5d3165f4b8b2.png differ diff --git a/anno3/vpc/orale/preparazione.org b/anno3/vpc/orale/preparazione.org index 17f36d3..58357a4 100644 --- a/anno3/vpc/orale/preparazione.org +++ b/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 = +- 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 = +| reset(x in y)(y) = v(y) if y ≠ x else 0 +| v ⊧ x≤c iff v(x)≤c +| v ⊧ x +- 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. diff --git a/media.py b/media.py index d3ede41..ca7f12b 100644 --- a/media.py +++ b/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)) diff --git a/todo.org b/todo.org index 2c0ef70..aa56e6e 100644 --- a/todo.org +++ b/todo.org @@ -1,25 +1,18 @@ * TODO VPC [23/24] -- [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 == -- [-] Teoria [26/29] +- [-] Teoria [31/36] + - [ ] PN consistente? + - [ ] vedi perche \neg\models != \models\neg + - [X] Pronuncia / nome P_m(S) + - [X] In ctl come dico: M,s ⊧ φ if ∀σ| σ₀ = s, σ ⊧ φ (ogni path + - [ ] ripeti fairness + - [ ] fai buchi + - [X] fai equivalenze + - [ ] Vedi step semantic e enabling degree - [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