diff --git a/anno3/vpc/consegne/3/analisi.org b/anno3/vpc/consegne/3/analisi.org index c636992..5fea12c 100644 --- a/anno3/vpc/consegne/3/analisi.org +++ b/anno3/vpc/consegne/3/analisi.org @@ -946,16 +946,16 @@ Entrambi hanno le seguenti azioni: Si applica l'algoritmo del partizionamento per verificare l'equivalenza tramite bisimulazione. Questo lo stato iniziale -| {S0, R0}, {S1, S2, S3, S4, S5, S6, S7, S8, S9, S10, S11, S12, S13, S14 +| {S0, R0}, {S1, S2, S3, S4, S5, S6, S7, S8, S9, S10, S11, S12, S14, S13 | R1, R2, R2, R3, R4, R5, R6, R7, R8, R9, R10, R11, R12, R13, R14, R15, | R16, R17, R18, R19, R20, R21, R22, R23, R24} Applico lo split considerando l'azione /criticalâ‚š/ | {S0, R0}, {S4, S5, R4, R14, R18, R19, R24} -| {S1, S2, S3, S6, S7, S8, S9, S10, S11, S12, S13, R1, R2, R3, R5, R6, +| {S1, S2, S3, S6, S7, S8, S9, S10, S11, S12, S14, R1, R2, R3, R5, R6, | R7, R8, R9, R10, R11, R12, R13, R15, R16, R17, R20, R21, R22, R23} Applico lo split considerando l'azione /critical_{q}/ -| {S0, R0}, {S4, S5, R4, R14, R19, R24}, {R18}, {S11, S14, R9, R11, R16, R22} -| {S1, S2, S3, S6, S7, S8, S9, S10, S12, S13, R1, R2, R3, R5, R6, +| {S0, R0}, {S4, S5, R4, R14, R19, R24}, {R18}, {S11, S13, R9, R11, R16, R22} +| {S1, S2, S3, S6, S7, S8, S9, S10, S12, S14, R1, R2, R3, R5, R6, | R7, R8, R10, R12, R13, R15, R17, R20, R21, R23} Notiamo che R18 compare come unico elemento di un insieme. Benche` l'algoritmo non sia terminato, questo ci basta per concludere che non diff --git a/anno3/vpc/consegne/3/analisi.pdf b/anno3/vpc/consegne/3/analisi.pdf index a11b253..5f8649a 100644 Binary files a/anno3/vpc/consegne/3/analisi.pdf and b/anno3/vpc/consegne/3/analisi.pdf differ diff --git a/anno3/vpc/consegne/3/derivation_3.2.jpg b/anno3/vpc/consegne/3/derivation_3.2.jpg index af266dd..ee13f75 100644 Binary files a/anno3/vpc/consegne/3/derivation_3.2.jpg and b/anno3/vpc/consegne/3/derivation_3.2.jpg differ diff --git a/anno3/vpc/consegne/3/derivation_3.6.jpg b/anno3/vpc/consegne/3/derivation_3.6.jpg index ac2e85d..36f721c 100644 Binary files a/anno3/vpc/consegne/3/derivation_3.6.jpg and b/anno3/vpc/consegne/3/derivation_3.6.jpg differ diff --git a/todo.org b/todo.org index 34ea7b3..4a9590e 100644 --- a/todo.org +++ b/todo.org @@ -23,7 +23,15 @@ - [X] sulle slide, quando si chiede come deve decidere il master - [X] Sistema screenshots di GSPN non tagliati - [X] rete E, F -> Controlla sia finito -- [-] Analisi [18/22] +- [-] Analisi [19/25] + - [ ] Riduzione??? + - [ ] 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