Context Navigation

debug_trace_crt

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

Rev	Line
[4]	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.