Ver el código de «Segundo parcial 24/11/2022 (IngSoft2)»

=== Ejercicio 1 ===
==== a) Dibuje los LTS para AB y ABC ====
<pre>
A = (a -> c -> A).
B = (b -> d -> B).

||AB = (A||B)\{c,d}.

C = (c -> C).

||ABC = (AB || C).
</pre>

===== Resolución =====
[[Archivo:IngSoft2 2parcial 24-11-2022 1aLTSAB.jpg|miniaturadeimagen|alt=LTS composición de A y B, con cuatro estados: 0,1,2 y 3. Las transiciones son: 0 a 1 con etiqueta b, 1 a 0 con tau, 1 a 2 con a, 2 a 1 con tau, 2 a 3 con tau, 3 a 2 con b, 0 a 3 con a, y 3 a 0 con tau.|LTS AB - ejercicio 1a 2parcial 2c2022 IngSoft2]]

[[Archivo:IngSoft2 2parcial 24-11-2022 1aLTSABC.jpg|miniaturadeimagen|alt=LTS composición de AB y C. Igual al de AB, pero con una transición saliente extra por nodo, que sale del nodo y vuelve al mismo nodo con etiqueta c.|LTS ABC - ejercicio 1a 2parcial 2c2022 IngSoft2]]

==== b) Proponga un LTS que sea débilmente equivalente a AB pero con menos estados. Demuestre que son equivalentes ====

===== Resolución =====

[[Archivo:IngSoft2 2parcial 24-11-2022 1bLTSABbisimilar.jpg|miniaturadeimagen|alt=LTS con un nodo, 0 con dos transiciones salientes hacia sí mismo, con etiquetas a y b.|LTS débilmente bisimilar a AB - ejercicio 1b 2parcial 2c2022 IngSoft2]]

Para demostrar que son débilmente bisimilaresbasta con dar la relación de bisimilitud: [(0,0), (1,0), (2,0), (3,0)].

(Puede ser difícil ver por qué valen (1,0), (2,0) y (3,0), dejo la justificación de (1,0) a partir de la definición formal, las otras dos son análogas:
<pre>
Sea Q el LTS de un nodo, 0ab el estado 0 del LTS AB y 0q el estado 0 de Q:
- 1ab -a-> 2ab y  0q =a=> 0q y (2,0) esta en la relacion
-  0q -b-> 0q  y 1ab =b=> 1ab (porque 1 -tau-> 0 -b-> 1) y (1,0) esta en la relacion
-  0q -a-> 0q  y 1ab =a=> 2ab y (2,0) esta en la relacion
</pre>
)

=== Ejercicio 2 ===
==== En el siguiente ejemplo, el proceso TWOCOIN satisface la propiedad de profreso TAILS? Explique. ====
<pre>
TWOCOIN = (pick ->COIN | pick ->TRICK).
TRICK = (toss -> heads -> TRICK |
         toss -> heads -> TWOCOIN).
COIN = (toss -> heads -> COIN |
        toss -> tails -> COIN).

progress TAILS = {tails}.
</pre>

===== Resolución =====
La única forma de que TAILS nunca se cumpla es que siempre que estemos en el estado TWOCOIN se elija el camino a TRICK o elijamos la moneda TRICK una vez y de ahí siempre hagamos toss con esa misma moneda.
Pero bajo fair choice, sabemos que cuando un estado es visitado infinitas veces, todas sus transiciones salientes también lo son. En las situaciones que mencioné antes, estaríamos visitando TWOCOIN y/o TRICK infinitas veces, por lo que eventualmente se seleccionará la moneda justa (COIN, que contiene tails) y se usará de ahí en más, cumpliendo la propiedad TAILS.

=== 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. ====
<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 ===
==== 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 ===
==== 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.