1		% (c) 2015-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(ce_replay,[replay_counter_example/1]).
6
7		:- use_module(probsrc(state_space),[state_space_reset/0]).
8
9		:- use_module(symbolic_model_checker(predicate_handling), [create_state_predicate/2,
10		create_constants_state_predicate/2,
11		deprime_state/2]).
12
13		:- use_module(probsrc(b_trace_checking),[find_successor_state/4]).
14		replay_counter_example(Sol) :-
15		state_space_reset,replay_aux(Sol,_).
16		replay_aux(Sol,CurId) :-
17		create_constants_state_predicate(Sol,ConstantsStatePred), !,
18		find_successor_state(CurId,ConstantsStatePred,SuccID,0),
19		replay_aux2(Sol,SuccID,1).
20		replay_aux(Sol,CurId) :-
21		replay_aux2(Sol,CurId,1).
22		replay_aux2([],_,_).
23		replay_aux2(Sol,CurId,LineNr) :-
24		create_state_predicate(Sol,StatePred),
25		% print(find(CurId,LineNr,Sol)),nl, translate:print_bexpr(StatePred),nl,
26		find_successor_state(CurId,StatePred,SuccID,LineNr),
27		deprime_state(Sol,DPSol),
28		L1 is LineNr+1,
29		replay_aux2(DPSol,SuccID,L1).