Para esta entrega escogí el problema 2.15 que dice lo siguiente:
Along all paths, p is true in every other state.
Utilizamos los siguientes operadores:
A =∀ = Siempre
U = Hasta
X = Siguiente
Along all paths, p is true in every other state.
Traducido:
A lo largo de todos los caminos, p es verdadero en todos los demás estados.
Resultado
2 comentarios:
Notación improvisada. La igualdad no vale usarla así y la U falta su parte final. Además "every other" significa cada dos estados. Algo como A((p v Xp) ^ no (p V Xp)) o sea A(p xor Xp) podría servir, queriendo decir que siempre o es válida p ahora mismo o en el estado siguiente. Lo tuyo tiene poco sentido. Van 2 pts por el intento.
Ahora improvisé yo notación. Sería AG, no A.
Publicar un comentario