Diferencia entre revisiones de «IngSoft2 2recu 05-12-22»
De Cuba-Wiki
(Página creada con «=== Ejercicio 1 === ==== a) Dibuje los LTS para A, B y AB ==== <pre> property A = (a -> c -> A) + {b}. B = (c -> B). ||AB = (A || B). </pre> ===== Resolución ===== '''TO…») |
|||
| Línea 44: | Línea 44: | ||
'''TODO''' | '''TODO''' | ||
=== Ejercicio 4 | === Ejercicio 4 === | ||
==== Se perdio en la matrix porque lo escribieron en el pizarron ¯\_(ツ)_/¯ ==== | ==== Se perdio en la matrix porque lo escribieron en el pizarron ¯\_(ツ)_/¯ ==== | ||
Revisión actual - 14:34 10 dic 2022
Ejercicio 1
a) Dibuje los LTS para A, B y AB
property A = (a -> c -> A) + {b}.
B = (c -> B).
||AB = (A || B).
Resolución
TODO
b) Diga si los siguientes LTS son bisimilares. Justifique
A = (a -> (b -> A | c -> A)). B = (a -> b -> B | a -> c -> B).
Resolución
TODO
Ejercicio 2
En el siguiente ejemplo, el proceso TWOCOIN satisface las propiedades P y Q? Explique.
TWOCOIN = (pick -> COIN | pick -> TRICK).
TRICK = (toss -> heads -> TRICK |
toss -> heads -> TWOCOIN).
COIN = (toss -> heads -> COIN |
toss -> tails -> COIN).
assert P = []<>tails.
assert Q = ([]<>pick) -> ([]<>tails)
Resolución
TODO
Ejercicio 3
Verdadero o Falso? Justifique.
- a) []<>p es una propiedad de safety y una propiedad de liveness.
- b) ([]p) -> <>q es equivalente a [](p -> <>q).
Resolución
TODO
Ejercicio 4
Se perdio en la matrix porque lo escribieron en el pizarron ¯\_(ツ)_/¯
Resolución
TODO
Ejercicio 5
Dado el büchi generalizado definido mas abajo, aplique el procedimiento para definir un büchi no-generalizado
- Estados = {0, 1}
- Alfabeto = {a, b}
- Transiciones = {(0, a, 1), (1, b, 0), (0, b, 0)}
- Estado inicial = 0
- Estados de aceptacion = {{0}, {1}}
Resolucion
TODO
