Context Navigation

debug_trace_crt @ 4

Last change on this file since 4 was 4, checked in by syed, 14 years ago
input files added
File size: 531 bytes

Line
1	# MC: formula failed --- AG(o2=0)
2	# MC: Calling debugger for trace 1
3	--State
4	machine_concret1.m_state:S0
5	o1:0
6	o2:0
7	r_i1:0
8	fails AG(o2=0)
9
10	--Counter example is a path to a state where o2=0 is false
11	--Counter example begins
12	--State 0:
13	machine_concret1.m_state:S0
14	o1:0
15	o2:0
16	r_i1:0
17
18	--Goes to state 1:
19	machine_concret1.m_state:S1
20	o1:1
21	r_i1:1
22	--On input:
23	i1:1
24
25	--Goes to state 2:
26	machine_concret1.m_state:S2
27	o1:0
28	o2:1
29	--On input:
30	<Unchanged>
31
32	--Counter example ends
33
34	--State
35	machine_concret1.m_state:S2
36	o1:0
37	o2:1
38	r_i1:1
39	fails o2=0.
40
41

Note: See TracBrowser for help on using the repository browser.