| Revisión actual |
Tu texto |
| Línea 51: |
Línea 51: |
|
| |
|
| === Ejercicio 3 === | | === Ejercicio 3 === |
| ==== Una solución clásica al problema de deadlock de los filósofos es que cada filósofo pueda hacer un timeout y devolver su palillo si no consigue su segundo palillo. Modifique el FSP dado a continuación para modelar esta solución clásica. ====
| | === Ejercicio 4 === |
| <pre>
| |
| FORK = (get -> put -> FORK).
| |
| PHIL = (sitdown->left.get->right.get
| |
| ->eat->left.put->right.put
| |
| ->arise->PHIL).
| |
| ||DINERS(N=5)=
| |
| forall [i:0..N-1]
| |
| (phil[i]:PHIL ||
| |
| {phil[i].left,phil[((i-1)+N)%N].right}::FORK
| |
| ).
| |
| </pre>
| |
| | |
| ===== Resolución =====
| |
| <pre>
| |
| const T=10.
| |
| TIMER = (right.get->TIMER[N]),
| |
| TIMER[0] = (timeout->TIMER),
| |
| TIMER[i:1..N]=(left.get->TIMER | tick->TIMER[i-1])\{tick}.
| |
| | |
| PHIL = (sitdown->right.get->WAIT),
| |
| WAIT = (timeout->right.put->arise->PHIL
| |
| | left.get->eat->left.put->right.put->arise->PHIL).
| |
| | |
| FORK = (get -> put -> FORK).
| |
| | |
| const N = 5.
| |
| ||DINERS=
| |
| forall [i:0..N-1](
| |
| phil[i]:PHIL
| |
| || phil[i]:TIMER
| |
| || {phil[i].left,phil[((i-1)+N)%N].right}::FORK
| |
| ).
| |
| </pre>
| |
| | |
| === Ejercicio 4: Verdadero o Falso? Justifique === | |
| ==== a) p W q es una propiedad de safety y no es una propiedad de liveness. (Recuerde que Φ W Ψ se define como (Φ U Ψ) || []Φ) ====
| |
| | |
| ===== Resolución =====
| |
| El ejercicio 4 lo hicimos regular o mal todos los que entregamos menos alguien que no conozco, así que no tengo la resolución chequeada. Confirmé con Uchitel que es verdadero (la propiedad es de safety y no de liveness), pero se esperaba que demostraramos utilizando las definiciones de que los contraejemplos de las propiedades de safety son trazas finitas/trazas infinitas para las propiedades de liveness.
| |
| Si alguien lo hizo bien por favor agregue la resolución.
| |
| | |
| ==== b) ([]p) U q es equivalente a [](p U q) ====
| |
| (Este lo hablé con Uchitel y me dijo que era correcto resolver así, pero no fue como lo hice en el parcial así que no lo tengo confirmado con corrección) La traza p, {p, q}, {p, ¬q}, {p, ¬q}, {p, ¬q}, .... cumple la primer propiedad pero no la segunda, porque la segunda habla de que siempre cuando vale p eventualmente valdrá q, en cambio la primera solo pide que si valió []p en algún momento, valga q una vez después.
| |
| | |
| === Ejercicio 5 === | | === Ejercicio 5 === |
| ==== Escriba una estructura de kripke que satisfaga la fórmula AG EX p y no satisfaga la fórmula AG AX p ====
| |
| 1) AG EX p: "Para todo camino, siempre vale que existe un camino donde en el próximo estado vale p"
| |
| 2) AG AX p: "Para todo camino, siempre vale que en todo camino en el próximo estado vale p"
| |
|
| |
| Una estructura de Kripke que satisfaga 1) pero no 2) sería
| |
| [[Archivo:IngSoft2 2parcial 24-11-2022 5-kripke.jpg|miniaturadeimagen|alt=Estructura de Kripke con dos estados: q0 de aceptaciónn y q1. Hay transición de q0 a q1 con la etiqueta "vale p, vale ¬p". Hay otra transición igual de q1 a q0.|Estructura de Kripke que cumple AG EX p pero no cumple AG AX p]]
| |
|
| |
| El árbol de cómputo es:
| |
| [[Archivo:IngSoft2 2parcial 24-11-2022 5-arbol-computo.jpg|miniaturadeimagen|alt=Árbol de cómputo donde de cada nodo salen dos transiciones, una hacia un estado en que vale p y la otra hacia un estado en que p no vale.|Árbol de computo para la estructura de Kripke dada]]
| |
|
| |
| Siempre hay un próximo estado donde vale p, pero no en todos los próximos estados vale p.
| |
|
| |
| === Ejercicio 6 === | | === Ejercicio 6 === |
| ==== Escriba un büchi no generalizado que capture la propiedad [](p=>Xq) ====
| |
| [[Archivo:IngSoft2 2parcial 24-11-2022 6buchi.jpg.jpg|miniaturadeimagen|Autómata de buchi no generalizado que captura la propiedad [](p=>Xq)]]
| |
| Mientras no ocurra p vale, pero si ocurre p en el siguiente momento debe volver q.
| |
