diff --git a/anno3/vpc/orale/ltximg/org-ltximg_035cd81a788468f06e94ceaf1bcc888daf9b8e07.png b/anno3/vpc/orale/ltximg/org-ltximg_035cd81a788468f06e94ceaf1bcc888daf9b8e07.png new file mode 100644 index 0000000..4ee33bf Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_035cd81a788468f06e94ceaf1bcc888daf9b8e07.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_112772627fc638b1a45a569879b263aaca288549.png b/anno3/vpc/orale/ltximg/org-ltximg_112772627fc638b1a45a569879b263aaca288549.png new file mode 100644 index 0000000..b0b6c42 Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_112772627fc638b1a45a569879b263aaca288549.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_1a25a5f7412ac897b89550cfa140bd552096e690.png b/anno3/vpc/orale/ltximg/org-ltximg_1a25a5f7412ac897b89550cfa140bd552096e690.png new file mode 100644 index 0000000..e4bb9ae Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_1a25a5f7412ac897b89550cfa140bd552096e690.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_3a9fdeb01110ec14c7bffa4c6a8fed9ec0808a92.png b/anno3/vpc/orale/ltximg/org-ltximg_3a9fdeb01110ec14c7bffa4c6a8fed9ec0808a92.png new file mode 100644 index 0000000..154c0cd Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_3a9fdeb01110ec14c7bffa4c6a8fed9ec0808a92.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_473db1ac1c325d5bc8d7cd1dc3dad0c07f04f6ea.png b/anno3/vpc/orale/ltximg/org-ltximg_473db1ac1c325d5bc8d7cd1dc3dad0c07f04f6ea.png new file mode 100644 index 0000000..a209ece Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_473db1ac1c325d5bc8d7cd1dc3dad0c07f04f6ea.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_8cf209fcfdb130dab2a94745cc0ad4a89cd8473a.png b/anno3/vpc/orale/ltximg/org-ltximg_8cf209fcfdb130dab2a94745cc0ad4a89cd8473a.png new file mode 100644 index 0000000..1e35234 Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_8cf209fcfdb130dab2a94745cc0ad4a89cd8473a.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_8d2ef59494ab562668f62e8fd37e221b73911bd0.png b/anno3/vpc/orale/ltximg/org-ltximg_8d2ef59494ab562668f62e8fd37e221b73911bd0.png new file mode 100644 index 0000000..b0b6c42 Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_8d2ef59494ab562668f62e8fd37e221b73911bd0.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_9b0669b9580491eba5b675749eedc0d22eb3b790.png b/anno3/vpc/orale/ltximg/org-ltximg_9b0669b9580491eba5b675749eedc0d22eb3b790.png new file mode 100644 index 0000000..ebf26fe Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_9b0669b9580491eba5b675749eedc0d22eb3b790.png differ diff --git a/anno3/vpc/orale/ltximg/org-ltximg_bfedb4894e8e75a4705ce103a7c613641a996893.png b/anno3/vpc/orale/ltximg/org-ltximg_bfedb4894e8e75a4705ce103a7c613641a996893.png new file mode 100644 index 0000000..8b3c979 Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_bfedb4894e8e75a4705ce103a7c613641a996893.png differ diff --git a/anno3/vpc/orale/preparazione.org b/anno3/vpc/orale/preparazione.org new file mode 100644 index 0000000..e526060 --- /dev/null +++ b/anno3/vpc/orale/preparazione.org @@ -0,0 +1,222 @@ +* Simboli: +- sqcap: ⊓ +- box: □ +- a\b: a̱ +- Vert: ‖ +- $\underrightarrow{a}$ (toggle latex fragment): $\underrightarrow{a}$ + +* 1.1 Petri Nets +** Definizione +Petri net N: 4-tuple. +| N = +- P = {p| p is a place} (state variables) +- T = {t| t is a transition} (change of states) +- → (Flow function) ⊂ P×T ∪ T×P +- W: Flow → N⁺ +Visualizzabile come grafo bipartito. +** Altra definizione +Posso sostituire → e W con due vettori ∈ Nᴾˣᵀ +| N = +- Pre: funzione P×T → N; rappresenta gli input delle transizioni + | Pre(p,t) = W(p,t) if (p,t)∈→ else 0 +- Post: funzione P×T → N + | Post(p,t) = W(t,p) if (t,p)∈→ else 0 +Da Pre e Post posso generare la matrice di incidenza C +| C: P×T → Z +| C = Post - Pre +** Marking di una rete +Definiamo Marking m (vettore ∈ Nᴾ) la funzione +| m: P → N +| m(p) = n: ci sono n token nel posto p +** Sistema P/N +Un sistema P/N S e` dato da una rete di Petri e il suo stato iniziale +(marking m₀) +| S = +| Stato composito: unione degli stati dei singoli posti +L'evoluzione del sistema e` determinata dallo scattare delle +transizioni. +Una transizione puo` scattare quando: +| ∀p, m(p) ≥ W(p,t) ∧ (p,t) ∈ → +| m ≥ Pre[-,t] +Possiamo calcolare il nuovo marking m' allo scattare di una +transizione t come: +| m' = m + C[-,t] +| m' = m - Pre[-,t] + Post[-,t] +| ∀p, m'(p) = m(p) - W(p,t) + W(t,p) +Si scrive: +| m[t>m' +Posso definire postset e preset di una transizione o posto come: +| •t = {p∈P| (p,t) ∈ →} (preset di t, ovvero al posto di • p) +| •p = {t∈T| (t,p) ∈ →} (postset di t, ovvero al posto di • t) +| t• = {p∈P| (t,p) ∈ →} (preset di p, ovvero al posto di • p) +| p• = {t∈T| (p,t) ∈ →} (postset di p, ovvero al posto di • t) +| ∀p∈•t, m(p) ≥ W(p,t) → t e` abilitata +** Sequenza di scatti +La sequenza di scatti σ nella marcatura m e`definita come: +| σ = [t₁, t₂, ..., tₙ], tᵢ∈T +Scriviamo +| m[σ>m' if ∃{m₁, m₂, ..., mₙ}: ∀i ∃mᵢ| mᵢ₋₁[tᵢ>mᵢ +Possiamo dire (state equation): +| ∃σ| m[σm' → m' = m + C•σ (integrale di C su sequenza σ) +| ∃σ| m[σm' ↚ m' = m + C•σ (m non permette di eseguire σ) +** Linguaggio di un sistema P/N +Un linguaggio L(S) di un sistema P/N e` definito come: +| L(S) = {σ| σ valido per S in m₀} +** Reachability Set +Il Reachability Set RS(S) e` definito come: +| RS(S) = {m: ∃σ∈L(S)| m₀[σm} +Il Reachability Graph RG e` generato usando come nodi i vari marking, +e come archi le transizioni che collegano un marking al precedente. +*** Proprieta` di RS e RG +- Boundedness: + definito il bound di un place come + | bound(p) = max {m(p)| m∈RS(S)} + | ∀p∈P, bound(p) < ∞ +- Liveness: + ogni transizione puo` essere eseguita infinite volte + | ∀t∈T: ∀m∈RS(S) ∃σ| m[σ>m' ∧ m'[t> +- Reversible: + da ogni marcatura si puo` tornare alla marcatura iniziale + | ∀m∈RS(S), ∃σ| m[σ>m₀ +- Home state: + un marking m e` detto home state quando + | ∀m'∈RS(S), ∃σ| m'[σ>m +** Step Semantic +Step s: multiset di transizioni +s e` abilitato in m se: m ≥ Pre • s +| m' = m + C•s +La sequenza di scatti sigma e` ridefinita usando s +*** Enabling degree +Numero di volte che una transizione puo` scattare in parallelo +eₜ(m) = max {k∈N⁺ | m≥ k•Pre[-,t]} +* 1.2 Reti di Petri colorate +Una rete di petri colorata e` definita come: +| N = +- C e` l'insieme dei colori +- cd: P∪T → C (definisce il dominio di colore dei posti e transizioni) +- Pre[p,t], Post[p,t]: cd(t) → bag(cd(p)) +Una transizione e` abilitata quando in ogni transizione del +preset i token di colore cd(p) hanno molteplicita` ≥ Pre[p,t](c) +| ∀p∈•t, cd(p) ≥ Pre[p,t](c) +| m ≥ Pre[-,t](c) +* 1.3 Tecniche Strutturali +** Flussi +Definiamo p-flow come un vettore: +| y: P → Q | y.C = 0 +Definiamo t-flow come un vettore: +| x: T → Q | C.x = 0 +quando non negativi: p-semiflusso e t-semiflusso +Definiamo il supporto come: +| ||y|| = {p∈P | y(p) > 0} +| ||x|| = {t∈T | x(t) > 0} +La rete si dice conservativa quando: +| ∃y | ||y|| = P +La rete si dice consistente quando: +| ∃x | ||x|| = T +I flussi sono canonici quando il gcd degli elementi non nulli e` 1. + +Un insieme generatore Ψ_y e` un insieme del numero minimo di +p-semiflussi, detti minimi, tali che e` possibile generare gli altri sommandoli +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: ym = ym₀ +Legge del comportamente ciclico: +| ∃m₀, ∃σ∈L(S) | mₒ[σ>m₀ ∧ σ=x +* 2.1 Algebra dei Processi +Descrizione astratta di sistemi concorrenti e non deterministici. +Si focalizza sulle transizioni eseguite piu` che sugli stati raggiunti. +** CCS: Calculus of Communicating Systems +- A, B, C: agenti +- a, b, c: azioni +- a̱, ḇ, c̱: co-azioni +- τ: azione silente (τ=τ̱) +Grammatica: +| E := nil | (E) | a.E | E + E' | E‖E' | E\L | E[f] +** CSP: Communicating Sequential Processes +Due primitive: eventi (azioni) e processi. +| P := STOP | skip | a → P | P + Q | P ⊓ Q | P □ Q | P ‖ₛ Q | E / a +A lezione abbiamo visto: +| P := nil | a.P | P + Q | P ‖ₛ Q | E / a +** Structural Operational Semantics +*** Prefixing (assioma) + +——————— +a.E $\underrightarrow{a}$ E +*** Mixed Choice +Composizione non deterministica con scelte miste: +ogni azione, τ inclusa sono offerte all'ambiente (solo le azioni +visibili possono essere controllate). + +E $\underrightarrow{\mu}$ E' +—————————— +E + F $\underrightarrow{\mu}$ E' + +F $\underrightarrow{\mu}$ F' +—————————— +E + F $\underrightarrow{\mu}$ F' +*** Internal Choice +Due assiomi che mostrano che il sistema puo` evolvere in uno dei sottocomponenti. + +—————————— +E ⊓ F $\underrightarrow{\tau}$ E' + + +—————————— +E ⊓ F $\underrightarrow{\tau}$ F' +*** External Choice +Come nel caso delle scelte miste, ma nel caso di un'operazione silente +le sottocomponenti non vengono scartate. + +E $\underrightarrow{\mu}$ E' +—————————— (μ ≠ τ) +E □ F $\underrightarrow{\mu}$ E' + +F $\underrightarrow{\mu}$ F' +—————————— (μ ≠ τ) +E □ F $\underrightarrow{\mu}$ F' + +E $\underrightarrow{\tau}$ E' +—————————————— +E □ F $\underrightarrow{\tau}$ E' □ F + +F $\underrightarrow{\tau}$ F' +—————————————– +E □ F $\underrightarrow{\tau}$ E □ F' +*** Evoluzione Indipendente + +E $\underrightarrow{\mu}$ E' +—————————————– +E ‖ F $\underrightarrow{\mu}$ E' ‖ F + +F $\underrightarrow{\mu}$ F' +————————————–– +E ‖ F $\underrightarrow{\mu}$ E ‖ F' +*** Evoluzione con sincronizzazione +E $\underrightarrow{a} E' +F $\underrightarrow{\underline{a}}$ F' +————————————–––(a≠τ) (CCS) +E ‖ F $\underrightarrow{\tau}$ E' ‖ F' + +E $\underrightarrow{a}$ E' +F $\underrightarrow{a}$ F' +————————————–––($a\in{S}$) (CSP) +E ‖ₛ F $\underrightarrow{\tau}$ E' ‖ₛ F' +*** Restrizione (CCS) +E $\underrightarrow{\mu}$ E' +—————————–(μ,μ̱ ∉ R) +E\R $\underrightarrow{\mu}$ E'\R +*** Relabeling (CCS) +E $\underrightarrow{a}$ E' +———————————— +E[f] $\underrightarrow{f[a]}$ E'[f] +*** Hiding (CSP) +E $\underrightarrow{\mu}$ E' +—————————–(μ ∉ S) +E\S $\underrightarrow{\mu}$ E'\S + +E $\underrightarrow{\mu}$ E' +—————————–(μ ∈ S) +E\S $\underrightarrow{\tau}$ E'\S diff --git a/todo.org b/todo.org index 3737887..1affa56 100644 --- a/todo.org +++ b/todo.org @@ -99,17 +99,18 @@ - [X] Confrontare esercizi con Galla` -* Prog Mobile [2/5] +* Prog Mobile [3/6] - [X] Api all songs - [X] relazione -- [ ] slides +- [X] slides - [ ] teoria - [ ] account prof +- [ ] Vnc sul fisso -* Apprendimento Automatico [1/2] +* Apprendimento Automatico [2/2] - [X] Scrivile per date di esame -- [ ] Richiedi date esame +- [X] Richiedi date esame * Tesi [3/27]