Context Navigation

debug_trace_abs

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

Rev	Line
[4]	1	# MC: formula failed --- (o1=0 + AF(o2=1))
	2	# MC: Calling debugger for trace 1
	3	--State
	4	machine_concret1_a1.state:machine_concret1_Abs1_STATE_19
	5	o1:1
	6	o2:0
	7	r_i1:0
	8	fails (o1=0 + AF(o2=1)).
	9
	10	--State
	11	machine_concret1_a1.state:machine_concret1_Abs1_STATE_19
	12	o1:1
	13	o2:0
	14	r_i1:0
	15	fails o1=0.
	16
	17	--State
	18	machine_concret1_a1.state:machine_concret1_Abs1_STATE_19
	19	o1:1
	20	o2:0
	21	r_i1:0
	22	fails AF(o2=1)
	23
	24	--A fair path on which o2=1 is always false:
	25	--Counter example begins
	26	--Fair path stem:
	27	--State 0:
	28	machine_concret1_a1.state:machine_concret1_Abs1_STATE_19
	29	o1:1
	30	o2:0
	31	r_i1:0
	32
	33	--Goes to state 1:
	34	machine_concret1_a1.state:machine_concret1_Abs1_STATE_20
	35	--On input:
	36	machine_concret1_a1.nd_aff0:1
	37	machine_concret1_a1.nd_aff1:0
	38	machine_concret1_a1.nd_o1:1
	39	machine_concret1_a1.nd_o2:0
	40	machine_concret1_a1.nd_r_i1:0
	41	machine_concret1_a1.state$raw_na$initial$_nb:machine_concret1_Abs1_STATE_25
	42
	43	--Goes to state 2:
	44	machine_concret1_a1.state:machine_concret1_Abs1_STATE_13
	45	--On input:
	46	<Unchanged>
	47
	48	--Fair path cycle:
	49	--State 0:
	50	machine_concret1_a1.state:machine_concret1_Abs1_STATE_13
	51	o1:1
	52	o2:0
	53	r_i1:0
	54
	55	--Goes to state 1:
	56	<Unchanged>
	57	--On input:
	58	machine_concret1_a1.nd_aff0:1
	59	machine_concret1_a1.nd_aff1:0
	60	machine_concret1_a1.nd_o1:1
	61	machine_concret1_a1.nd_o2:0
	62	machine_concret1_a1.nd_r_i1:0
	63	machine_concret1_a1.state$raw_na$initial$_nb:machine_concret1_Abs1_STATE_25
	64
	65
	66	--Counter example ends
	67
	68	--State
	69	machine_concret1_a1.state:machine_concret1_Abs1_STATE_19
	70	o1:1
	71	o2:0
	72	r_i1:0
	73	fails o2=1.
	74
	75	--State
	76	machine_concret1_a1.state:machine_concret1_Abs1_STATE_20
	77	o1:1
	78	o2:0
	79	r_i1:0
	80	fails o2=1.
	81
	82	--State
	83	machine_concret1_a1.state:machine_concret1_Abs1_STATE_13
	84	o1:1
	85	o2:0
	86	r_i1:0
	87	fails o2=1.
	88
	89
	90	# MC: formula failed --- AG(o2=0)
	91	# MC: Calling debugger for trace 1
	92	--State
	93	machine_concret1_a1.state:machine_concret1_Abs1_STATE_25
	94	o1:0
	95	o2:1
	96	r_i1:0
	97	fails AG(o2=0)
	98
	99	since o2=0 is false at this state
	100	--State
	101	machine_concret1_a1.state:machine_concret1_Abs1_STATE_25
	102	o1:0
	103	o2:1
	104	r_i1:0
	105	fails o2=0.
	106
	107

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

Download in other formats:

Original Format