Diferencia entre revisiones de «Segundo parcial 24/11/2022 (IngSoft2)»
m (minor) |
(ejercicio 2 2p InsgSoft2 2c2022) |
||
| Línea 31: | Línea 31: | ||
) | ) | ||
=== Ejercicio 2 === | === 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 === | === Ejercicio 3 === | ||
=== Ejercicio 4 === | === Ejercicio 4 === | ||
=== Ejercicio 5 === | === Ejercicio 5 === | ||
=== Ejercicio 6 === | === Ejercicio 6 === | ||
Revisión del 17:02 4 dic 2022
Ejercicio 1
a) Dibuje los LTS para AB y ABC
A = (a -> c -> A).
B = (b -> d -> B).
||AB = (A||B)\{c,d}.
C = (c -> C).
||ABC = (AB || C).
b) Proponga un LTS que sea débilmente equivalente a AB pero con menos estados. Demuestre que son equivalentes
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:
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
)
Ejercicio 2
En el siguiente ejemplo, el proceso TWOCOIN satisface la propiedad de profreso TAILS? Explique.
TWOCOIN = (pick ->COIN | pick ->TRICK).
TRICK = (toss -> heads -> TRICK |
toss -> heads -> TWOCOIN).
COIN = (toss -> heads -> COIN |
toss -> tails -> COIN).
progress TAILS = {tails}.
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.
