1 | start(s0). | |
2 | %start(state(s(s(0)),0,s(s(0)))). | |
3 | ||
4 | prop(s0,open). | |
5 | prop(s1,closed). | |
6 | prop(s2,closed). | |
7 | prop(s2,heat). | |
8 | ||
9 | trans(close_door,s0,s1). | |
10 | trans(open_door,s1,s0). | |
11 | trans(start,s1,s2). | |
12 | trans(open_door,s2,s0). | |
13 | trans(stop,s2,s1). | |
14 | ||
15 | prob_pragma_string('ASSERT_LTL','G ({closed} or {open})'). | |
16 | prob_pragma_string('ASSERT_CTL','AG ({closed} or {open})'). | |
17 | prob_pragma_string('ASSERT_CTL2','EF ( EG ({closed}))'). | |
18 | prob_pragma_string('ASSERT_CTL3','EF ({closed})'). | |
19 | prob_pragma_string('ASSERT_CTL4','EF ({heat})'). | |
20 | ||
21 | /* | |
22 | ASSERT_CTL5 == "( EG ({closed}))"; // wrong | |
23 | */ |