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

Line
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