source: cegar_dev/cegar/abstract_model/debug_trace_abs @ 4

# MC: formula failed --- (o1=0 + AF(o2=1))
# MC: Calling debugger for trace 1
--State
machine_concret1_a1.state:machine_concret1_Abs1_STATE_19
o1:1
o2:0
r_i1:0
fails (o1=0 + AF(o2=1)).

--State
machine_concret1_a1.state:machine_concret1_Abs1_STATE_19
o1:1
o2:0
r_i1:0
fails o1=0.

--State
machine_concret1_a1.state:machine_concret1_Abs1_STATE_19
o1:1
o2:0
r_i1:0
fails AF(o2=1)

--A fair path on which o2=1 is always false:
 --Counter example begins
--Fair path stem:
--State 0:
machine_concret1_a1.state:machine_concret1_Abs1_STATE_19
o1:1
o2:0
r_i1:0

--Goes to state 1:
machine_concret1_a1.state:machine_concret1_Abs1_STATE_20
--On input:
machine_concret1_a1.nd_aff0:1
machine_concret1_a1.nd_aff1:0
machine_concret1_a1.nd_o1:1
machine_concret1_a1.nd_o2:0
machine_concret1_a1.nd_r_i1:0
machine_concret1_a1.state$raw_na$initial$_nb:machine_concret1_Abs1_STATE_25

--Goes to state 2:
machine_concret1_a1.state:machine_concret1_Abs1_STATE_13
--On input:
<Unchanged>

--Fair path cycle:
--State 0:
machine_concret1_a1.state:machine_concret1_Abs1_STATE_13
o1:1
o2:0
r_i1:0

--Goes to state 1:
<Unchanged>
--On input:
machine_concret1_a1.nd_aff0:1
machine_concret1_a1.nd_aff1:0
machine_concret1_a1.nd_o1:1
machine_concret1_a1.nd_o2:0
machine_concret1_a1.nd_r_i1:0
machine_concret1_a1.state$raw_na$initial$_nb:machine_concret1_Abs1_STATE_25


 --Counter example ends

--State
machine_concret1_a1.state:machine_concret1_Abs1_STATE_19
o1:1
o2:0
r_i1:0
fails o2=1.

--State
machine_concret1_a1.state:machine_concret1_Abs1_STATE_20
o1:1
o2:0
r_i1:0
fails o2=1.

--State
machine_concret1_a1.state:machine_concret1_Abs1_STATE_13
o1:1
o2:0
r_i1:0
fails o2=1.


# MC: formula failed --- AG(o2=0)
# MC: Calling debugger for trace 1
--State
machine_concret1_a1.state:machine_concret1_Abs1_STATE_25
o1:0
o2:1
r_i1:0
fails AG(o2=0)

since o2=0 is false at this state
--State
machine_concret1_a1.state:machine_concret1_Abs1_STATE_25
o1:0
o2:1
r_i1:0
fails o2=0.