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		*/