Diferencia entre revisiones de «Segundo parcial 24/11/2022 (IngSoft2)»

De Cuba-Wiki
(ejercicio 1 2p InsgSoft2 2c2022)
 
m (minor)
Línea 30: Línea 30:
</pre>
</pre>
)
)
=== Ejercicio 2 ===
=== Ejercicio 3 ===
=== Ejercicio 4 ===
=== Ejercicio 5 ===
=== Ejercicio 6 ===

Revisión del 16:56 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).
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
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

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:

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

Ejercicio 3

Ejercicio 4

Ejercicio 5

Ejercicio 6