Exemplos usados para testar o trabalho1 sobre CTL

README.md

Os 4 exemplos contêm uma mesma maquina de estados e diferentes propriedades.

Os numeros no nome dos arquivos descrevem quais estados não satisfazem a prioridade. Modelo e propriedades validados usando NuSMV

ex_1.txt

6
1 3 alive chase flee 2 2 4
2 3 alive eat flee 4 1 2 3 5
3 0 2 1 6
4 3 alive move chase 1 1 
5 4 alive eat move flee 1 2
6 1 move 1 3
((flee)->(eat))

ex_123456.txt

6
1 3 alive chase flee 2 2 4
2 3 alive eat flee 4 1 2 3 5
3 0 2 1 6
4 3 alive move chase 1 1 
5 4 alive eat move flee 1 2
6 1 move 1 3
(AG(((alive)->(((chase)&(!(flee)))|((!(chase))&(flee))))))

ex_13456.txt

6
1 3 alive chase flee 2 2 4
2 3 alive eat flee 4 1 2 3 5
3 0 2 1 6
4 3 alive move chase 1 1 
5 4 alive eat move flee 1 2
6 1 move 1 3
(((alive)&(eat))&(!(move)))

ex_none.txt

6
1 3 alive chase flee 2 2 4
2 3 alive eat flee 4 1 2 3 5
3 0 2 1 6
4 3 alive move chase 1 1 
5 4 alive eat move flee 1 2
6 1 move 1 3
(AG(((move)->(AX((!(move)))))))