1		% (c) 2015-2022 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(module_information)).
8		:- module_info(group,symbolic_model_checker).
9		:- module_info(description,'Replay symbolically generated traces.').
10
11		:- use_module(probsrc(state_space),[state_space_reset/0]).
12		:- use_module(probsrc(error_manager),[add_error/3]).
13
14		:- use_module(symbolic_model_checker(predicate_handling), [create_state_predicate/2,
15		create_constants_state_predicate/2,
16		deprime_state/2]).
17
18		:- use_module(probsrc(b_trace_checking),[find_successor_state/4]).
19		% Sol is a single state with potentially primed variables; unprimed variables are the first state,
20		% simply primed ones the second, doubly primed the third state, ...
21		replay_counter_example(Sol) :-
22		length(Sol,Len),format('Replaying counter example with ~w bindings found by symbolic model checker~n',[Len]),
23		state_space_reset,
24	?	(replay_aux(Sol,_) -> true
25		; add_error(symbolic_model_checker,'Could not replay counter example: ',Sol)
26		).
27
28		replay_aux(Sol,CurId) :-
29	?	create_constants_state_predicate(Sol,ConstantsStatePred), !,
30		find_successor_state(CurId,ConstantsStatePred,SuccID,0),
31	?	replay_aux2(Sol,SuccID,1).
32		replay_aux(Sol,CurId) :-
33		replay_aux2(Sol,CurId,1).
34
35		replay_aux2([],_,_) :- !.
36		replay_aux2(Sol,CurId,LineNr) :-
37	?	create_state_predicate(Sol,StatePred),
38		% print(find(CurId,LineNr,Sol)),nl, translate:print_bexpr(StatePred),nl,
39		find_successor_state(CurId,StatePred,SuccID,LineNr),
40		deprime_state(Sol,DPSol),
41		L1 is LineNr+1,
42	?	replay_aux2(DPSol,SuccID,L1).