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). |