1		% (c) 2021-2025 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(b_intelligent_trace_replay, [get_transition_details/6,
6		perform_single_replay_step/5,
7		replay_json_trace_file/2, replay_json_trace_file/5,
8		read_json_trace_file/3,
9		tcltk_replay_json_trace_file/3,
10		replay_prolog_trace_file/1,
11
12		% API for interactive JSON trace replay:
13		load_json_trace_file_for_ireplay/1,
14		tk_get_stored_json_trace_description/1,
15		get_stored_json_replay_steps/1,
16		get_ireplay_status/3,
17		replay_of_current_step_is_possible/5,
18		replay_of_current_step_is_possible_with_trans/5,
19		replay_current_step/1,
20		replay_current_step_with_trans/6,
21		ireplay_fast_forward/1,
22		ireplay_fast_forward_with_trans/6,
23		skip_current_ireplay_step/1]).
24
25		:- use_module(module_information,[module_info/2]).
26		:- module_info(group,testing).
27		:- module_info(description,'Replay saved (JSON) traces in a flexible way.').
28		% successor to b_trace_checking
29
30		:- meta_predicate exclude_and_collect_errors(2,-,-,-,-).
31
32		:- use_module(state_space,[current_state_id/1, transition/4, visited_expression/2]). % transition(CurID,Term,TransId,DestID)
33
34		:- use_module(tools_strings,[ajoin/2,ajoin_with_sep/3]).
35		:- use_module(specfile,[extract_variables_from_state/2, get_state_for_b_formula/3, b_or_z_mode/0, xtl_mode/0,
36		get_local_states_for_operation_transition/4, create_local_store_for_operation/4,
37		get_operation_name/2]).
38		:- use_module(error_manager).
39		:- use_module(debug).
40		:- use_module(probsrc(state_space), [extend_trace_by_transition_ids/1]).
41
42		% A single step is a list of informations about the step
43		% name/OperationName
44		% paras/List of =(Name,Value)
45
46		% TO DO: for match_spec use mutable counter for number of matches instead of used parameter
47
48		:- use_module(tcltk_interface,[compute_all_transitions_if_necessary/2]).
49
50		:- use_module(probsrc(bmachine),[b_get_operation_non_det_modifies/2, b_is_operation_name/1]).
51		:- use_module(probsrc(bsyntaxtree), [def_get_texpr_id/2, get_texpr_ids/2, get_texpr_id/2, get_texpr_type/2]).
52		:- use_module(probsrc(tools_matching), [get_possible_fuzzy_matches_and_completions_msg/3]).
53		:- use_module(probsrc(b_interpreter),[b_test_boolean_expression_for_ground_state/5]).
54
55		perform_single_replay_step(FromID,TransID,DestID,MatchSpec,TransSpec) :-
56		%format('* FROM: ~w ',[FromID]),portray_match_spec(MatchSpec),nl,
57		(match_spec_has_optimize_field(MatchSpec)
58		-> findall(sol(MM,TID,DID),
59		perform_single_replay_step_statespace(FromID,TID,DID,MatchSpec,TransSpec,MM),
60		Sols),
61		mark_match_spec_as_used(MatchSpec),
62		length(Sols,NrSols),
63		min_member(sol(Mismatches,TransID,DestID),Sols),
64		format('Min. nr of mismatches found ~w among ~w candidate steps (starting from state ~w). ~n',[Mismatches,NrSols,FromID])
65		; % just find first solution:
66		perform_single_replay_step_statespace(FromID,TransID,DestID,MatchSpec,TransSpec,_)
67		).
68		perform_single_replay_step(FromID,TransID,DestID,MatchSpec,TransSpec) :-
69		perform_single_replay_step_by_pred(FromID,TransID,DestID,MatchSpec,TransSpec).
70
71
72
73
74		% Assumption: ParaStore and ResultStore are sorted
75		% returns the number of mismatches for those Keys marked as optimize
76		perform_single_replay_step_statespace(FromID,TransID,DestID,
77		MatchSpec,
78		transition_spec(OpName, _, ParaStore, ResultStore, DestStore, UnchangedVars, Preds, _Postconditions),
79		Mismatches) :-
80		mark_match_spec_as_used(MatchSpec),
81		get_opt_match_spec_val(opname,MatchSpec,OpMatch),
82		compute_all_transitions_if_necessary(FromID,false), % could be made optional
83		(OpMatch==match -> TOpName=OpName ; true),
84		get_sorted_transition_details(FromID,TransID,DestID,TOpName,FullParaStore,FullResultStore),
85		(xtl_mode
86		-> transition(FromID,OpTerm,TransID,DestID),
87		ground(OpTerm) % if not ground: fail here and try to instantiate non-ground params by replay by predicate
88		; true),
89		(TOpName=OpName -> MM0 = 0 ; MM0=1, assert_mismatch(OpMatch)),
90		count_store_mismatches(FullParaStore,ParaStore,paras,MatchSpec,MM0,MM1), % check if parameters match
91		count_store_mismatches(FullResultStore,ResultStore,results,MatchSpec,MM1,MM2), % check if operation return values match
92		get_unchanged_store(FromID,UnchangedVars,UnchangedStore),
93		(DestStore=[], UnchangedStore=[]
94		-> MM6=MM2
95		; % check if variables in destination state match
96		visited_expression(DestID,DestState),
97		get_dest_store(DestState,FullDestStore),
98		count_store_mismatches(FullDestStore,DestStore,dest,MatchSpec,MM2,MM3),
99		count_store_mismatches(FullDestStore,UnchangedStore,unchanged,MatchSpec,MM3,MM4),
100		(b_or_z_mode, get_match_spec_val(nondet_vars,MatchSpec,_)
101		-> b_get_op_non_det_modifies(OpName,NonDetModifies),
102		include(b_intelligent_trace_replay:bind_id_is_element_of(NonDetModifies),DestStore,D1),
103		count_store_mismatches(FullDestStore,D1,nondet_vars,MatchSpec,MM4,MM5),
104		include(b_intelligent_trace_replay:bind_id_is_element_of(NonDetModifies),UnchangedStore,D2),
105		count_store_mismatches(FullDestStore,D2,nondet_vars,MatchSpec,MM5,MM6)
106		; MM6=MM4
107		)
108		),
109		Mismatches = MM6,
110		(Preds=[] -> true
111		; get_match_spec_val(preds,MatchSpec,match)
112		-> bsyntaxtree:conjunct_predicates(Preds,Pred),
113		format('Testing preds in destination state ~w after ~w: ',[FromID,DestID]),translate:print_bexpr(Pred),nl,
114		% TODO: insert_before_substitution_variables for $0 vars; check that it is consistent with Tcl/Tk and ProB2-UI
115		% maybe use annotate_becomes_such_vars or find_used_primed_ids
116		append(FullResultStore,FullParaStore,LocalStore),
117		b_test_boolean_expression_for_ground_state(Pred,LocalStore,FullDestStore,'trace replay', OpName)
118		; true
119		).
120
121		node_not_fully_explored(FromID,OpName) :-
122		(max_reached_for_node(FromID)
123		; not_all_transitions_added(FromID)
124		; not_interesting(FromID)
125		; time_out_for_node(FromID,OpName,_)).
126
127		:- use_module(probsrc(preferences),[get_time_out_preference_with_factor/2]).
128		% lookup in state space failed; try perform by predicate
129		% Note: does not use optimize keys (yet), only match keys
130		perform_single_replay_step_by_pred(FromID,TransID,DestID,
131		MatchSpec,
132		transition_spec(OpName, _, ParaStore, ResultStore, DestStore, UnchangedVars, Preds,
133		_Postconditions)) :-
134		nonvar(OpName), % we currently cannot execute by predicate without knowing OpName
135		((node_not_fully_explored(FromID,OpName) ; xtl_mode) -> true % TODO: improve max_reached_for_node for xtl_mode
136		; debug_format(19,'Node ~w fully explored for ~w; no use in attempting execute by predicate~n',[FromID,OpName]),
137		fail
138		),
139		mark_match_spec_as_used(MatchSpec),
140		!,
141		(ParaStore \= [], % check parameters of operation
142		get_match_spec_val(paras,MatchSpec,match)
143		-> b_get_operation_typed_paras(OpName,Parameters),
144		generate_predicates_from_store(operation_parameters,Parameters,ParaStore,ParaPreds)
145		; ParaPreds = []),
146		(ResultStore \= [], % check return values of operation
147		get_match_spec_val(results,MatchSpec,match)
148		-> b_get_operation_typed_results(OpName,Results),
149		generate_predicates_from_store(operation_results,Results,ResultStore,ResultPreds)
150		; ResultPreds = []),
151		get_machine_identifiers(OpName,TVars),
152		(DestStore = [] -> DestPreds=[]
153		; get_match_spec_val(dest,MatchSpec,match)
154		-> generate_predicates_from_store(dest_variables,TVars,DestStore,DestPreds)
155		; get_match_spec_val(nondet_vars,MatchSpec,match)
156		-> b_get_op_non_det_modifies(OpName,NonDetModifies),
157		include(b_intelligent_trace_replay:id_is_element_of(NonDetModifies),TVars,NDVars),
158		generate_predicates_from_store(non_det_vars,NDVars,DestStore,DestPreds)
159		; DestPreds=[]
160		),
161		get_unchanged_store(FromID,UnchangedVars,UnchangedStore),
162		(UnchangedStore = [] -> UnchangedPreds=[]
163		; get_match_spec_val(unchanged,MatchSpec,match) ->
164		generate_predicates_from_store(unchanged_vars,TVars,UnchangedStore,UnchangedPreds)
165		; get_match_spec_val(nondet_vars,MatchSpec,match) ->
166		include(b_intelligent_trace_replay:id_is_element_of(NonDetModifies),TVars,NDVars),
167		generate_predicates_from_store(non_det_vars,NDVars,UnchangedStore,UnchangedPreds)
168		; UnchangedPreds=[]
169		),
170		(get_match_spec_val(preds,MatchSpec,match) -> AddPreds=Preds ; AddPreds=[]),
171		append([ParaPreds,ResultPreds,DestPreds,UnchangedPreds,AddPreds],AllPreds),
172		conjunct_predicates(AllPreds,Pred),
173		format('Trying to execute ~w in state ~w by predicate: ',[OpName,FromID]), translate:print_bexpr(Pred),nl,flush_output,
174		get_time_out_preference_with_factor(5,TO), % TODO: store this in meta JSON info or options
175		safe_time_out(tcltk_interface:tcltk_add_user_executed_operation_typed(OpName,FromID,_,Pred,TransID,DestID),
176		TO, TimeOutRes),
177		(TimeOutRes = time_out
178		-> format_with_colour(user_output,[orange],'==> Timeout when executing ~w by predicate in state ~w~n',[OpName,FromID]),fail
179		; true).
180
181		get_unchanged_store(_,[],UnchangedStore) :- !, UnchangedStore=[].
182		get_unchanged_store(FromID,UnchangedVars,UnchangedStore) :-
183		% copy old values to UnchangedStore
184		visited_expression(FromID,FromState),
185		extract_variables_from_state(FromState,FullFromStore),
186		sort(FullFromStore,SortedStore),
187		% TODO: generate warning when unchanged variable does not exist?
188		include(b_intelligent_trace_replay:bind_id_is_element_of(UnchangedVars),SortedStore,UnchangedStore).
189
190		:- use_module(library(codesio),[write_to_codes/2]).
191		generate_predicate_from_bind(Kind,TypedIDs,json_bind(ID,Val,Type,Pos),b(Res,pred,[])) :-
192		(member(b(identifier(ID),ExpectedType,_),TypedIDs) ->
193		(unify_types_strict(ExpectedType,Type)
194		-> TID = b(identifier(ID),ExpectedType,[]),
195		(xtl_mode
196		-> (write_to_codes(Val,ValC),
197		atom_codes(ValA,ValC),
198		TVal = b(external_function_call('STRING_TO_TERM',[b(string(ValA),string,[])]),ExpectedType,[]))
199		; TVal = b(value(Val),ExpectedType,[])),
200		Res = equal(TID,TVal)
201		; pretty_type(ExpectedType,ETS), pretty_type(Type,TS), write(clash(Kind,ID,ETS,TS)),nl,
202		% error should probably be caught earlier:
203		add_warning(b_intelligent_trace_replay,'Ignoring value for stored identifier due to type clash: ',ID,Pos),
204		Res = truth
205		)
206		; % the identifier is not in the list and should be ignored here; sanity checks are made somewhere else
207		Res = truth
208		).
209		generate_predicate_from_bind(Kind,TypedIDs,bind(ID,Val),R) :- % bind without type infos, e.g., from unchanged store
210		generate_predicate_from_bind(Kind,TypedIDs,json_bind(ID,Val,any,unkown),R).
211
212		generate_predicates_from_store(Kind,TVars,DestStore,DestPreds) :-
213		maplist(b_intelligent_trace_replay:generate_predicate_from_bind(Kind,TVars),DestStore,DestPreds).
214
215		get_machine_identifiers(_,[]) :- \+ b_or_z_mode, !.
216		get_machine_identifiers(Op,TConsts) :- is_setup_constants_op(Op), !, b_get_machine_constants(TConsts).
217		get_machine_identifiers(_,TVars) :- b_get_machine_variables(TVars).
218
219		is_setup_constants_op('$setup_constants').
220		is_setup_constants_op('$partial_setup_constants').
221
222		b_get_op_non_det_modifies(_,[]) :- \+ b_or_z_mode, !.
223		b_get_op_non_det_modifies(Op,NonDetModifies) :- is_setup_constants_op(Op),
224		!,% return all constants as non-det modifies
225		b_get_machine_constants(TConsts),get_texpr_ids(TConsts,ND),
226		sort(ND,NonDetModifies).
227		b_get_op_non_det_modifies(OpName,NonDetModifies) :- b_get_operation_non_det_modifies(OpName,NonDetModifies).
228
229		fix_operation_name(OpName,OpName2) :- \+ b_is_operation_name(OpName),
230		fix_operation_name2(OpName,OpName2).
231		fix_operation_name2('SETUP_CONSTANTS','$setup_constants').
232		fix_operation_name2('INITIALISATION','$initialise_machine').
233		% TODO: maybe provide more automatic fixes, list of automatic re-names when parameters stay identical,...
234
235		% wrappers to deal with a few special transitions; TO DO: extend for CSP||B
236		b_get_operation_typed_results('$setup_constants',Results) :- !,
237		Results=[]. % for trace replay we assume setup_constants to have no result variables
238		b_get_operation_typed_results('$initialise_machine',Results) :- !, Results=[]. % ditto
239		b_get_operation_typed_results('$partial_setup_constants',Results) :- !, Results=[]. % ditto
240		b_get_operation_typed_results(OpName,Results) :- b_or_z_mode, !, b_get_machine_operation_typed_results(OpName,Results).
241		b_get_operation_typed_results(_,[]).
242
243		:- use_module(xtl_interface,[xtl_transition_parameters/2]).
244		b_get_operation_typed_paras('$setup_constants',Paras) :- !,
245		Paras=[]. % for trace replay we assume setup_constants to have no parameters
246		b_get_operation_typed_paras('$initialise_machine',Paras) :- !, Paras=[]. % ditto
247		b_get_operation_typed_paras('$partial_setup_constants',Paras) :- !, Paras=[]. % ditto
248		b_get_operation_typed_paras(OpName,Paras) :- b_or_z_mode,!,
249		b_get_machine_operation_typed_parameters_for_animation(OpName,Paras).
250		b_get_operation_typed_paras(OpName,Paras) :- xtl_mode,!,
251		xtl_transition_parameters(OpName,Paras0),
252		maplist(b_intelligent_trace_replay:para_to_typed_id_string,Paras0,Paras).
253		b_get_operation_typed_paras(OpName,[]) :-
254		add_message(replay_json_trace_file,'Not in B mode, cannot obtain parameter info for: ',OpName).
255
256		para_to_typed_id_string(Para,b(identifier(Para),string,[])).
257		% -------------------
258
259		% now a version with multiple MatchSpecs to be tried in order
260		% Flag can be used to see how many alternatives were tried
261		flexible_perform_single_replay_step(FromID,TransID,DestID,[MatchSpec1|TMS],TransitionSpec,MName) :-
262		skip_match_spec(FromID,TransitionSpec,MatchSpec1),!,
263		debug_println(9,skipping_redundant_failing_check(MatchSpec1)),
264		flexible_perform_single_replay_step(FromID,TransID,DestID,TMS,TransitionSpec,MName).
265		flexible_perform_single_replay_step(FromID,TransID,DestID,[MatchSpec1|TMS],TransitionSpec,MName) :-
266		if(perform_single_replay_step(FromID,TransID,DestID,MatchSpec1,TransitionSpec),
267		get_match_spec_txt(MatchSpec1,MName),
268		flexible_perform_single_replay_step(FromID,TransID,DestID,TMS,TransitionSpec,MName)
269		).
270
271		% -------------------
272
273
274		% we only assert mismatches; if a variable remains untouched we matched perfectly
275		assert_mismatch(Var) :- var(Var),!, Var=optimize.
276		assert_mismatch(require_mismatch). % probably not useful; difficult to support by predicate
277		assert_mismatch(optimize).
278
279		precise_match_spec(match_spec(_,precise,KeyVals)) :-
280		KeyVals = [dest/match,opname/match,paras/match,preds/match,results/match,unchanged/match].
281		ignore_dest_match_spec(match_spec(_,params_and_results,KeyVals)) :-
282		KeyVals = [opname/match,paras/match,preds/match,results/match,nondet_vars/match,dest/optimize,unchanged/optimize].
283		%ignore_return_match_spec(match_spec(_,parameters_only,KeyVals)) :-
284		% KeyVals = [opname/match,paras/match,results/optimize,nondet_vars/optimize].
285		opname_optimize_match_spec(match_spec(_,keep_name,KeyVals)) :-
286		KeyVals = [opname/match,paras/optimize,results/optimize,nondet_vars/optimize,dest/optimize,unchanged/optimize].
287
288		% conditions on when to skip certain match_specs
289		% (we assume that the precise_match_spec was tried before)
290		skip_match_spec(root,TS,match_spec(_,params_and_results,_)) :- get_transition_spec_op(TS,'$setup_constants').
291		% for setup_constants: nondet_vars are all constants; so this is equivalent to precise
292		% for initialise_machine: paras are all variables
293		skip_match_spec(_,TS,match_spec(_,MS,_)) :- MS \= precise,
294		get_transition_spec_meta(TS,Meta),
295		% for an unknown operation we only try a precise replay (e.g., if operation just renamed), otherwise we skip it
296		member(unknown_operation/_,Meta).
297		% TODO: skip parameters_only if an operation has not results and no nondet_vars
298
299		match_spec_was_used(match_spec(UsedFlag,_,_)) :- UsedFlag==used.
300		mark_match_spec_as_used(match_spec(used,_,_)).
301
302		get_match_spec_txt(match_spec(_,Name,_),Name).
303		get_match_spec_val(Key,match_spec(_,_,List),Res) :- member(Key/Val,List),!,Res=Val.
304
305		get_opt_match_spec_val(Key,MS,Res) :- get_match_spec_val(Key,MS,Val),!, Res=Val.
306		get_opt_match_spec_val(_,_,optimize).
307
308		% check if it is useful to optimize the mismatches
309		match_spec_has_optimize_field(match_spec(_,_,KeyVals)) :- member(_/optimize,KeyVals).
310
311		:- public valid_match_spec_key/1.
312		valid_match_spec_key(dest).
313		valid_match_spec_key(nondet_vars).
314		valid_match_spec_key(opname).
315		valid_match_spec_key(paras).
316		valid_match_spec_key(results).
317		valid_match_spec_key(unchanged).
318
319		:- public portray_match_spec/1.
320		portray_match_spec(match_spec(UsedFlag,Name,List)) :-
321		(UsedFlag==used -> U=used ; U=not_yet_used),
322		format('~w (~w): ~w~n',[Name,U,List]).
323
324		% -------------------
325
326		get_dest_store(concrete_constants(C),SC) :- !, sort(C,SC).
327		get_dest_store(Store,Vars) :- b_or_z_mode,!, extract_variables_from_state(Store,Vars).
328		get_dest_store(State,XTLState) :- xtl_mode, !, XTLState = [bind(xtl_state,State)]. % special identifier xtl_state only exists in JSON traces
329		get_dest_store(_,[]). % CSP,... has no concept of variables
330
331
332		% count the number of mismatches for a given key and MatchSpec
333		% if MatchSpec requires match (perfect match) it will fail if Mismatches are 0
334		% it accumulates the global number of mismatches in a DCG style accumulator
335		count_store_mismatches(FullStore,PartialStore,Key,MatchSpec,MismatchesIn,MismatchesOut) :-
336		get_match_spec_val(Key,MatchSpec,MatchVal), !,
337		(MatchVal=match
338		-> MismatchesIn=MismatchesOut,
339		count_mismatches(FullStore,Key,PartialStore,0)
340		; count_mismatches(FullStore,Key,PartialStore,Mismatches),
341		MismatchesOut is MismatchesIn+Mismatches,
342		%print(new_mm(MismatchesOut,Key,MatchVal,Mismatches)),nl,
343		(Mismatches=0 -> true
344		; assert_mismatch(MatchVal))
345		).
346		count_store_mismatches(_,_,_Key,_,M,M). % key does not exist; no matching required
347
348		% for maplist, include, exclude:
349		bind_id_is_element_of(Vars,Bind) :- is_bind(Bind,ID,_), member(ID,Vars). % we could use ord_member
350		id_is_element_of(Vars,TID) :- def_get_texpr_id(TID,ID), member(ID,Vars).
351
352		is_bind(bind(ID,Val),ID,Val).
353		is_bind(json_bind(ID,Val,_,_),ID,Val).
354
355		%check_no_mismatches(FullStore,Key,PartialStore) :- count_mismatches(FullStore,Key,PartialStore,0).
356
357		count_mismatches(FullStore,Key,PartialStore,Mismatches) :-
358		count_mismatches_aux(FullStore,Key,PartialStore,0,Mismatches).
359		:- use_module(probsrc(translate), [translate_bvalue_with_limit/3]).
360		% count mismatches in FullStore compared to partial reference store
361		% if result is set to 0, it will fail after first mismatch
362		count_mismatches_aux(_,_,[],Acc,Res) :- !,Res=Acc.
363		count_mismatches_aux([],Key,PartialStore,_,_) :- b_or_z_mode, !,
364		ajoin(['Saved trace step contains unknown bindings for ',Key,': '],Msg),
365		add_error(b_intelligent_trace_replay,Msg,PartialStore),
366		fail.
367		count_mismatches_aux([],[_|_],_,Acc,Res) :- xtl_mode, !, % in XTL mode we can have multiple transitions with the same name => no error, try next for param match
368		inc_mismatches(Acc,Acc1,Res),
369		count_mismatches_aux(_,_,_,Acc1,Res).
370		count_mismatches_aux([Bind1|T],Key,[Bind2|T2],Acc,Res) :-
371		is_bind(Bind1,ID,Val), is_bind(Bind2,ID,Val2),!,
372		(check_value_equal(ID,Val,Val2)
373		-> count_mismatches_aux(T,Key,T2,Acc,Res)
374		; ((debug_mode(off) ; \+ b_or_z_mode) -> true
375		; translate_bvalue_with_limit(Val,200,V1), translate_bvalue_with_limit(Val2,200,V2),
376		formatsilent_with_colour(user_output,[red],'==> Mismatch for ~w ~w:~n ~w~n (trace) ~w~n',[Key,ID,V1,V2])
377		%nl,print(Val),nl,nl,print(Val2),nl,nl,
378		),
379		inc_mismatches(Acc,Acc1,Res),
380		count_mismatches_aux(T,Key,T2,Acc1,Res)
381		).
382		count_mismatches_aux([_ID|T],Key,PartialStore,Acc,Res) :- count_mismatches_aux(T,Key,PartialStore,Acc,Res).
383
384		inc_mismatches(X,_,Res) :- number(Res),X>Res,!,fail. % we will never reach Res; could be 0 for perfect match
385		inc_mismatches(Acc,Acc1,_) :- Acc1 is Acc+1.
386
387		% check if saved value and actual value is identical
388		:- use_module(kernel_objects,[equal_object/3]).
389		check_value_equal(ID,Val1,Val2) :-
390		temporary_set_preference(allow_enumeration_of_infinite_types,true,OldValueOfPref),
391		call_cleanup(check_value_equal_aux(ID,Val1,Val2),
392		reset_temporary_preference(allow_enumeration_of_infinite_types,OldValueOfPref)).
393
394		% what if trace was saved with different SYMBOLIC pref value?
395		:- use_module(b_ast_cleanup, [clean_up/3]).
396		:- use_module(custom_explicit_sets, [same_closure/2]).
397		:- use_module(debug, [debug_mode/1]).
398		check_value_equal_aux(ID,closure(P1,T1,B1),C2) :- C2 = closure(P2,T2,B2),
399		C1 = closure(P1,T1,B1),
400		!, % we have two symbolic values
401		(same_closure(C1,C2)
402		-> true
403		; % simple comparison failed, now try and normalize the symbolic values and compare again
404		temporary_set_preference(normalize_ast,true,CHANGE),
405		% normalize_ast_sort_commutative should probably be false, unless we improve the sorting
406		%print(compiling_cur_value(ID)),nl,
407		clean_up(B1,[],B1C),
408		%we could call: b_compiler:b_compile_closure(closure(P1,T1,B1C),closure(P12,T12,B12)),
409		%print(compiling_trace_value(ID)),nl,
410		clean_up(B2,[],B2C),
411		reset_temporary_preference(normalize_ast,CHANGE),
412		(same_closure(closure(P1,T1,B1C),closure(P2,T2,B2C))
413		-> true
414		; Val=closure(P1,T1,B1C), Val2 = closure(P2,T2,B2C),
415		debug_mode(on),
416		translate_bvalue_with_limit(Val,500,V1), translate_bvalue_with_limit(Val2,500,V2),
417		formatsilent_with_colour(user_output,[red],'==> Symbolic Mismatch for ~w:~n ~w~n (trace) ~w~n',[ID,V1,V2]),
418		% trace, same_closure(closure(P1,T1,B1C),closure(P2,T2,B2C)),
419		fail
420		)
421		).
422		%check_value_equal_aux(ID,Val1,Val2) :- !, equal_object(Val1,Val2,ID).
423		check_value_equal_aux(ID,Val1,Val2) :-
424		catch(
425		equal_object_time_out(Val1,Val2,ID,2500),
426		enumeration_warning(_A,_B,_C,_D,_E),
427		(format_with_colour(user_output,[red],'==> Enumeration warning when comparing values for ~w~n',[ID]),fail)
428		).
429		check_value_equal_aux(_ID,Val1,Val2) :- xtl_mode, !,
430		Val1 = Val2.
431
432		:- use_module(tools_meta,[safe_time_out/3]).
433		equal_object_time_out(Val1,Val2,ID,TO) :-
434		safe_time_out(equal_object(Val1,Val2,ID),TO,TimeOutRes),
435		(TimeOutRes = time_out
436		-> format_with_colour(user_output,[red],'==> Timeout when comparing values for ~w~n',[ID]),fail
437		; true).
438
439
440		:- use_module(specfile,[get_operation_internal_name/2,
441		state_corresponds_to_set_up_constants_only/2]).
442		:- use_module(bmachine,[b_get_machine_operation_parameter_names_for_animation/2,
443		b_get_machine_operation_typed_parameters_for_animation/2,
444		b_get_machine_operation_result_names/2,
445		b_get_machine_operation_typed_results/2,
446		b_get_machine_variables/1, b_get_machine_constants/1,
447		bmachine_is_precompiled/0, b_top_level_operation/1,
448		b_machine_name/1, b_is_variable/1, b_is_variable/2, b_is_constant/1, b_is_constant/2]).
449		:- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2]).
450
451		:- use_module(probsrc(state_space),[max_reached_for_node/1, not_all_transitions_added/1,
452		time_out_for_node/3, not_interesting/1,
453		try_set_trace_by_transition_ids/1]).
454
455		:- use_module(library(lists)).
456
457		% get the information of a B state_space transition in more detailed form
458		% we get a store of parameter values and a store of result values and the operation name
459		get_transition_details(FromID,TransID,DestID,OpName,ParaStore,ResultStore) :-
460		transition(FromID,OperationTerm,TransID,DestID),
461		get_operation_internal_name(OperationTerm,OpName),
462		get_transition_details_aux(OpName,OperationTerm,DestID,ParaStore,ResultStore).
463
464		get_transition_details_aux('$setup_constants',_,DestID,ParaStore,ResultStore) :- !,
465		ResultStore=[],
466		visited_expression(DestID,DestState),
467		state_corresponds_to_set_up_constants_only(DestState,ParaStore).
468		get_transition_details_aux('$initialise_machine',_,DestID,ParaStore,ResultStore) :- !,
469		ResultStore=[],
470		visited_expression(DestID,DestState),
471		extract_variables_from_state(DestState,ParaStore).
472		get_transition_details_aux(OpName,OperationTerm,_,ParaStore,ResultStore) :-
473		get_local_states_for_operation_transition(OpName,OperationTerm,ParaStore,ResultStore).
474
475		get_transition_name(FromID,TransID,OpName) :-
476		transition(FromID,OperationTerm,TransID,_),
477		get_operation_name(OperationTerm,OpName).
478
479
480
481		% a variation where the two stores are sorted according to Prolog order:
482		get_sorted_transition_details(FromID,TransID,DestID,TOpName,SortedPS,SortedRS) :-
483		get_transition_details(FromID,TransID,DestID,TOpName,FullParaStore,FullResultStore),
484		sort(FullParaStore,SortedPS),
485		sort(FullResultStore,SortedRS).
486
487		% ------------------------
488
489		get_transition_spec_op(transition_spec(OpName, _, _, _, _, _, _, _),OpName).
490		get_transition_spec_meta(transition_spec(_, Meta, _, _, _, _, _, _),Meta).
491
492		% get textual representation of transition spec (portray/translate)
493		get_transition_spec_txt(transition_spec(OpName, Meta, ParaStore, ResultStore,
494		_DestStore, _Unchanged, _Preds, _Postconditions),Txt) :-
495		(member(description/Desc,Meta) -> ajoin([Desc,' :: '],DescTxt) ; DescTxt = ''),
496		(nonvar(OpName), OpName \= '' -> OpTxt=OpName
497		; member(unknown_operation/op(OldOpName,OldParas,OldResults),Meta)
498		-> translate_unknown_operation(OldOpName,OldParas,OldResults,OpTxt)
499		; OpTxt='?'),
500		(ParaStore = [] -> ParaText1='', ParaText2=''
501		; ParaText1=' paras: ',
502		maplist(get_bind_txt,ParaStore,Paras),
503		ajoin_with_sep(Paras,',',ParaText2)
504		),
505		(ResultStore = [] -> ResultText1='', ResultText2=''
506		; ResultText1=' results: ',
507		maplist(get_bind_txt,ResultStore,Results),
508		ajoin_with_sep(Results,',',ResultText2)
509		),!,
510		ajoin([DescTxt,OpTxt,ParaText1,ParaText2,ResultText1,ResultText2],Txt).
511		get_transition_spec_txt(TS,'???') :- add_internal_error('Unknown transition spec:',TS).
512
513
514		translate_unknown_operation(OldOpName,OldParas,[],OpTxt) :- !,
515		translate_bindings(OldParas,OPS),
516		append(OPS,[')'],OpParaAtoms),
517		ajoin(['?',OldOpName,'('|OpParaAtoms],OpTxt).
518		translate_unknown_operation(OldOpName,OldParas,OldResults,OpTxt) :-
519		translate_bindings(OldResults,OPR),
520		translate_unknown_operation(OldOpName,OldParas,[],Op1),
521		ajoin([Op1,'-->'|OPR],OpTxt).
522
523		% translate a list of json_bind terms into a list for use with ajoin for pretty-priting
524		translate_bindings([],[]).
525		translate_bindings([json_bind(ID,Val,_Type,_Pos)|TJ],[ID,'=',TVal|TT]) :-
526		translate_bvalue_with_limit(Val,50,TVal),
527		(TJ = [] -> TT=[]
528		; TT = [','|TT2], translate_bindings(TJ,TT2)).
529
530
531		get_bind_txt(Bind,Txt) :- is_bind(Bind,Id,Val),
532		simple_val(Val), !, % TODO: add parameter for short/long text
533		translate_bvalue_with_limit(Val,100,V1),
534		ajoin([Id,'=',V1],Txt).
535		get_bind_txt(Bind,Id) :- is_bind(Bind,Id,_).
536
537		simple_val(V) :- var(V),!,fail.
538		simple_val(int(_)).
539		simple_val(pred_false).
540		simple_val(pred_true).
541		simple_val(string(_)).
542		simple_val(fd(_,_)).
543
544
545		% perform some static checks on a transition spec: check if operations, parameters, variables exist
546		check_and_adapt_trace_step(transition_spec(OpName, Meta, ParaStore, _, DestStore, UnchangedVars,Preds, Postconditions), Step,
547		transition_spec(OpName, Meta, ParaStore2, [], DestStore2,UnchangedVars2,Preds, Postconditions)) -->
548		{\+ b_or_z_mode},!,
549		exclude_and_collect_errors(unknown_para_binding(OpName,_,'parameter',Step),ParaStore,ParaStore2),
550		exclude_and_collect_errors(unknown_variable_binding(Step,OpName),DestStore,DestStore2),
551		exclude_and_collect_errors(unknown_variable(Step,OpName),UnchangedVars,UnchangedVars2).
552		check_and_adapt_trace_step(transition_spec(OpName, Meta, ParaStore,ResultStore, DestStore, UnchangedVars,Preds, Postconditions),
553		Step,
554		transition_spec(OpName2,Meta2,ParaStore2,ResultStore2,DestStore2,UnchangedVars2,Preds2, Postconditions2)) -->
555		({fix_operation_name(OpName,OpName2)}
556		-> add_replay_error('Fixed unknown operation name to: ',OpName2) ; {OpName2=OpName}),
557		{b_get_operation_typed_results(OpName,TOpResults)},
558		{b_get_operation_typed_paras(OpName,TOpParas)},
559		!,
560		{Meta2=Meta}, % TO DO: include excluded infos
561		{Preds2=Preds}, %TO DO: check if all identifiers bound
562		{Postconditions2=Postconditions}, % TODO Check operation names and predicate identifiers
563		exclude_and_collect_errors(unknown_para_binding(OpName,TOpParas,'parameter',Step),ParaStore,ParaStore2),
564		exclude_and_collect_errors(unknown_para_binding(OpName,TOpResults,'result variable',Step),ResultStore,ResultStore2),
565		({is_setup_constants_op(OpName)}
566		-> exclude_and_collect_errors(unknown_constant_binding(Step),DestStore,DestStore2),
567		{UnchangedVars2 = []},
568		({UnchangedVars = []} -> []
569		; {add_error(b_intelligent_trace_replay,'Illegal unchanged info for SETUP_CONSTANTS',UnchangedVars)}
570		)
571		; exclude_and_collect_errors(unknown_variable_binding(Step,OpName),DestStore,DestStore2),
572		exclude_and_collect_errors(unknown_variable(Step,OpName),UnchangedVars,UnchangedVars2)
573		).
574		check_and_adapt_trace_step(transition_spec('', Meta, PS, RS, DestStore, UnchangedVars,Preds, Postconditions), Step,
575		transition_spec(_, Meta2, [], [], DestStore2, UnchangedVars2,Preds, Postconditions)) -->
576		% Empty Operation name, treat as wildcard
577		!,
578		{Meta2 = [unknown_operation/op('',PS,RS) | Meta]},
579		( {PS=[]} -> "" ; add_replay_error('Parameters cannot be checked for unknown operation name: ',PS)),
580		( {RS=[]} -> "" ; add_replay_error('Result values cannot be checked for unknown operation name: ',PS)),
581		exclude_and_collect_errors(unknown_variable_binding(Step,OpName),DestStore,DestStore2),
582		exclude_and_collect_errors(unknown_variable(Step,OpName),UnchangedVars,UnchangedVars2).
583		check_and_adapt_trace_step(transition_spec(OpName, Meta, PS, RS, DestStore, UnchangedVars,Preds, Postconditions), Step,
584		transition_spec(_, Meta2, [], [], DestStore2, UnchangedVars2,Preds, Postconditions)) -->
585		add_replay_error('Unknown operation: ',OpName), % TODO treat $JUMP
586		{Meta2 = [unknown_operation/op(OpName,PS,RS) | Meta],
587		findall(KOpid,b_top_level_operation(KOpid),Ops),
588		(get_possible_fuzzy_matches_and_completions_msg(OpName,Ops,FMsg)
589		-> ajoin(['Unknown operation in replay step ',Step,' (did you mean the operation ',FMsg,' ?) : '], Msg)
590		; ajoin(['Unknown operation in replay step ',Step,': '], Msg)),
591		(member(pos/Pos,Meta) -> true ; Pos=unknown),
592		add_error(b_intelligent_trace_replay,Msg,OpName,Pos)
593		},
594		% TODO: maybe do a fuzzy match and check if a new operation not used in the trace file exists
595		exclude_and_collect_errors(unknown_variable_binding(Step,OpName),DestStore,DestStore2),
596		exclude_and_collect_errors(unknown_variable(Step,OpName),UnchangedVars,UnchangedVars2).
597
598		check_step_postconditions(transition_spec(_, _, _, _, _, _, _, Postconditions),StateID) -->
599		check_postconditions(Postconditions,1,StateID).
600
601		check_postconditions([],_,_) --> [].
602		check_postconditions([Postcondition|Postconditions],Nr,StateID) -->
603		check_postcondition(Postcondition,Nr,StateID),
604		{Nr1 is Nr+1},
605		check_postconditions(Postconditions,Nr1,StateID).
606
607		check_postcondition(state_predicate(Pred),Nr,StateID) -->
608		{get_state_for_b_formula(StateID,Pred,State)},
609		({b_test_boolean_expression_for_ground_state(Pred,[],State,'trace replay postconditions',Nr)} ->
610		[]
611		;
612		add_replay_error('Failed postcondition (predicate):',Nr)
613		).
614		check_postcondition(operation_enabled(OpName,Pred,Enabled),Nr,StateID) -->
615		{
616		precise_match_spec(MatchSpec),
617		TransitionSpec = transition_spec(OpName,[],[],[],[],[],[Pred],[]),
618		(perform_single_replay_step(StateID,_,_,MatchSpec,TransitionSpec) -> Actual = enabled ; Actual = disabled)
619		},
620		({Enabled == Actual} ->
621		[]
622		;
623		{ajoin(['Failed postcondition (operation ',OpName,' should be ',Enabled,'):'],Msg)},
624		add_replay_error(Msg,Nr)
625		).
626
627		% a version of exclude which also collects errors
628		exclude_and_collect_errors(_Pred,[],[]) --> [].
629		exclude_and_collect_errors(Pred,[H|T],Res) --> {call(Pred,H,Error)},!,
630		[Error],
631		exclude_and_collect_errors(Pred,T,Res).
632		exclude_and_collect_errors(Pred,[H|T],[H|Res]) --> % include item
633		exclude_and_collect_errors(Pred,T,Res).
634
635
636		add_replay_error(Msg,Term) --> {gen_replay_error(Msg,Term,Err)}, [Err].
637		gen_replay_error(Msg,Term,rerror(FullMSg)) :- ajoin([Msg,Term],FullMSg).
638		replay_error_occured(Errors) :- member(rerror(_),Errors).
639		get_replay_error(rerror(Msg),Msg).
640
641		:- use_module(probsrc(btypechecker), [unify_types_strict/2]).
642		:- use_module(probsrc(kernel_objects), [infer_value_type/2]).
643		:- use_module(probsrc(translate), [pretty_type/2]).
644
645		unknown_para_binding(OpName,TParas,Kind,Step,json_bind(ID,Value,ValType,ValPos),ErrorTerm) :- b_or_z_mode, !,
646		( get_texpr_id(TID,ID),
647		member(TID,TParas), get_texpr_type(TID,Type)
648		-> illegal_type(ID,Type,Value,ValType,ValPos,Kind,Step,ErrorTerm)
649		; ajoin(['Ignoring unknown ',Kind,' for operation ',OpName,' at step ', Step, ': '],Msg),
650		gen_replay_error(Msg,ID,ErrorTerm)
651		).
652		unknown_para_binding(OpName,_,Kind,Step,json_bind(ID,_,any,_),ErrorTerm) :- xtl_mode, !,
653		(xtl_transition_parameters(OpName,ParaIDs)
654		-> \+ memberchk(ID,ParaIDs)
655		; \+ is_xtl_param(ID)),
656		ajoin(['Ignoring unknown ',Kind,' for operation ',OpName,' at step ', Step, ': '],Msg),
657		gen_replay_error(Msg,ID,ErrorTerm).
658		unknown_variable_binding(Step,_OpName,json_bind(Var,Value,ValType,ValPos),ErrorTerm) :- b_or_z_mode, b_is_variable(Var,Type),!,
659		illegal_type(Var,Type,Value,ValType,ValPos,'variable',Step,ErrorTerm).
660		unknown_variable_binding(Step,OpName,json_bind(Var,_,_,_),ErrorTerm) :- unknown_variable(Step,OpName,Var,ErrorTerm).
661		unknown_variable(Step,OpName,Var,ErrorTerm) :- xtl_mode, !,
662		Var \= xtl_state,
663		ajoin(['Ignoring unknown variable at step ', Step, ' for ', OpName, ': '],Msg),
664		gen_replay_error(Msg,Var,ErrorTerm).
665		unknown_variable(Step,OpName,Var,ErrorTerm) :- \+ b_is_variable(Var),
666		(b_is_constant(Var)
667		-> ajoin(['Ignoring constant at step ', Step, ' for ', OpName, ' (a variable is expected here): '],Msg)
668		; b_get_machine_variables(TVars),get_texpr_ids(TVars,Vars),
669		get_possible_fuzzy_matches_and_completions_msg(Var,Vars,FMsg)
670		-> ajoin(['Ignoring unknown variable (did you mean ',FMsg,' ?) at step ', Step, ' for ', OpName, ': '],Msg)
671		; ajoin(['Ignoring unknown variable at step ', Step, ' for ', OpName, ': '],Msg)
672		),
673		gen_replay_error(Msg,Var,ErrorTerm).
674		unknown_constant_binding(Step,json_bind(Var,Value,ValType,ValPos),ErrorTerm) :- b_is_constant(Var,Type),!,
675		illegal_type(Var,Type,Value,ValType,ValPos,'constant',Step,ErrorTerm).
676		unknown_constant_binding(Step,json_bind(Var,_,_,_),ErrorTerm) :-
677		(b_is_variable(Var)
678		-> ajoin(['Ignoring variable at step ', Step, ' (a constant is expected here): '],Msg)
679		; b_get_machine_constants(TVars),get_texpr_ids(TVars,Vars),
680		get_possible_fuzzy_matches_and_completions_msg(Var,Vars,FMsg)
681		-> ajoin(['Ignoring unknown constant (did you mean ',FMsg,' ?) at step ', Step, ': '],Msg)
682		; ajoin(['Ignoring unknown constant at step ', Step, ': '],Msg)
683		),
684		gen_replay_error(Msg,Var,ErrorTerm).
685
686
687		illegal_type(Var,Type,_Value,ValType,_ValPos,Kind,Step,ErrorTerm) :-
688		\+ unify_types_strict(Type,ValType),
689		pretty_type(ValType,VTS), pretty_type(Type,TS),
690		ajoin(['Ignoring ',Kind, ' at step ', Step,
691		' due to unexpected type of value (', VTS, ' instead of ',TS,') for: '],ErrMsg),
692		gen_replay_error(ErrMsg,Var,ErrorTerm).
693
694		is_xtl_param(ID) :- atom_chars(ID,['p','a','r','a'|T]), number_chars(_,T).
695		/*
696		| ?- perform_single_replay_step(X,TID,Dest,Match,transition_spec(Op,[],[],[],[active])).
697		X = 3,
698		TID = 86,
699		Dest = 5,
700		Match = match_spec(match,match,match,match,match),
701		Op = new ?
702		yes
703
704		*/
705
706		% ------------------
707		%precise_replay_trace(Trace,FromID,TransIds,DestID) :-
708		% precise_match_spec(MatchSpec), % require precise replay
709		% replay_trace(Trace,[MatchSpec],[],1,FromID,TransIds,DestID,[],_). % Todo : check errors
710
711		:- use_module(tools_printing,[format_with_colour/4]).
712		:- use_module(probsrc(debug),[formatsilent_with_colour/4]).
713		% Note if we leave RestSpecs as a variable this will always do deterministic replay
714		% to achieve backtracking RestSpecs must be set to []
715		replay_trace([],_MatchSpecs,_Opts,_,ID,[],ID,[],[]).
716		replay_trace([TransSpec|T],MatchSpecs,Options,Step,FromID,TransIds,DestID,RestSpecs,
717		[replay_step(MatchInfo,Errors)|OtherMatches]) :-
718		get_transition_spec_txt(TransSpec,TTxt),
719		formatsilent_with_colour(user_output,[blue],'==> Replay step ~w: from state ~w for ~w~n',[Step,FromID,TTxt]),
720		statistics(walltime,[W1|_]),
721		% first perform static check of step:
722		phrase(check_and_adapt_trace_step(TransSpec,Step,CorrectedTransSpec),Errors,Errors1),
723		if((TransIds=[TransID|TTrans],
724		flexible_perform_single_replay_step(FromID,TransID,ID2,MatchSpecs,CorrectedTransSpec,MatchInfo)),
725		(phrase(check_step_postconditions(CorrectedTransSpec,ID2),Errors1),
726		statistics(walltime,[W2|_]), WTime is W2-W1,
727		get_transition_name(FromID,TransID,OpName), % show operation name used as feedback in case errors occur
728		(Errors == [] ->
729		formatsilent_with_colour(user_output,[green],'==> Replay step ~w successful (~w, ~w ms) leading to state ~w~n',[Step,MatchInfo,WTime,ID2])
730		; Errors = [rerror(OneErr)] ->
731		formatsilent_with_colour(user_output,[red,bold],'==> Replay step ~w successful WITH ERROR (~w, ~w, ~w ms) leading to state ~w via ~w~n',[Step,MatchInfo,OneErr,WTime,ID2,OpName])
732		;
733		length(Errors,NrErrors), Errors = [rerror(OneErr)|_],
734		formatsilent_with_colour(user_output,[red,bold],'==> Replay step ~w successful WITH ERRORS (~w, ~w errors [~w,...], ~w ms) leading to state ~w via ~w~n',[Step,MatchInfo,NrErrors,OneErr,WTime,ID2,OpName])
735		;
736		length(Errors,NrErrors),
737		formatsilent_with_colour(user_output,[red,bold],'==> Replay step ~w successful WITH ERRORS (~w, ~w errors, ~w ms) leading to state ~w via ~w~n',[Step,MatchInfo,NrErrors,WTime,ID2,OpName])
738		),
739		(get_preference(deterministic_trace_replay,true) -> !
740		% TO DO: use info from MatchSpec? (e.g., det for perfect match)
741		; true
742		; formatsilent_with_colour(user_output,[orange],'==> Backtracking replay step ~w (~w) leading to state ~w~n',[Step,MatchInfo,ID2])),
743		S1 is Step+1,
744		replay_trace(T,MatchSpecs,Options,S1,ID2,TTrans,DestID,RestSpecs,OtherMatches)
745		),
746		(format_with_colour(user_output,[red,bold],'==> Replay step ~w FAILED~n',[Step]),
747		get_transition_spec_txt(TransSpec,Txt), formatsilent_with_colour(user_output,[red,bold],' ~w~n',[Txt]),
748		Errors1=[],
749		MatchInfo=failed,
750
751		(T = [_|_], nonmember(stop_at_failure,Options)
752		-> % try and skip this step and continue replay
753		RestSpecs=[TransSpec|RT],
754		TransIds=[skip|TTrans], % -1 signifies skipped transition
755		S1 is Step+1,
756		replay_trace(T,MatchSpecs,Options,S1,FromID,TTrans,DestID,RT,OtherMatches)
757		; RestSpecs=[TransSpec|T], % the steps that were not replayed
758		TransIds=[], DestID=FromID,
759		OtherMatches=[]
760		)
761		)
762		).
763
764		% ------------------
765
766
767		tcltk_replay_json_trace_file(FileName,ReplayStatus,list([Header|Entries])) :-
768		replay_json_trace_file_with_check(FileName,TransSpecs,ReplayStatus,TransIds,MatchInfoList),
769		try_set_trace_by_transition_ids(TransIds),
770		Header = list(['Step', 'TraceFile','Replayed', 'Match','Mismatches','Errors','State ID']),
771		(tk_get_trace_info(TransSpecs,root,1,TransIds,MatchInfoList,Entries)
772		-> true
773		; add_internal_error('Could not compute replay table:',TransSpecs), Entries=[]).
774
775
776		:- use_module(probsrc(translate),[translate_event_with_limit/3]).
777
778		tk_get_trace_info([],_,_,_,_,[]).
779		tk_get_trace_info([TransSpec|TS2],CurID,Step,TransIds,MatchInfoList,
780		[list([Step,Txt,OpTxt,MI,list(DeltaList),list(Errors),CurID])|RestInfo]) :-
781		get_from_match_list(MatchInfoList,MI,Errors,MIL2),
782		get_transition_spec_txt(TransSpec,Txt),
783		(TransIds=[TID1|TI2], transition(CurID,OperationTerm,TID1,ToID)
784		-> %get_operation_internal_name(OperationTerm,OpName)
785		translate_event_with_limit(OperationTerm,30,OpTxt),
786		analyse_step_match(TransSpec,CurID,TID1,DeltaList)
787		; TransIds=[TID1|TI2],
788		(number(TID1) -> TID1<0 ; true) % not a valid transition number; -1 or skip
789		-> ToID=CurID, OpTxt='skipped', DeltaList=[]
790		; TI2=[], ToID=CurID, OpTxt='-', DeltaList=[]
791		),
792		Step1 is Step+1,
793		tk_get_trace_info(TS2,ToID,Step1,TI2,MIL2,RestInfo).
794
795		get_from_match_list([replay_step(MI,Errors)|T],MatchInfo,TkErrors,T) :-
796		maplist(get_replay_error,Errors,TkErrors),
797		(MI=precise,TkErrors=[_|_] -> MatchInfo=precise_with_errs ; MatchInfo=MI).
798		get_from_match_list([],'-',['-'],[]).
799
800		% analyse how good a step matches the transition spec
801		% useful after replay to provide explanations to the user
802		analyse_step_match(TransSpec,FromID,TransID,DeltaList) :-
803		TransSpec = transition_spec(OpName, _, ParaStore, ResultStore, DestStore, _UnchangedVars, _Preds, _Postconditions),
804		get_sorted_transition_details(FromID,TransID,DestID,TOpName,FullParaStore,FullResultStore),
805		(TOpName=OpName -> DeltaList=DL1 ; DeltaList=['Name'|DL1]),
806		delta_store_match(FullParaStore,paras,ParaStore,DL1,DL2),
807		delta_store_match(FullResultStore,results,ResultStore,DL2,DL3),
808		visited_expression(DestID,DestState),
809		get_dest_store(DestState,FullDestStore),
810		delta_store_match(FullDestStore,dest,DestStore,DL3,DL4),
811		% TO DO: UnchangedVars and _Preds
812		DL4=[],!.
813		analyse_step_match(TransSpec,FromID,TransID,DeltaList) :-
814		add_internal_error('Call failed:',analyse_step_match(TransSpec,FromID,TransID,DeltaList)),
815		DeltaList=['??ERROR??'].
816
817		delta_store_match(_,_,[]) --> !.
818		delta_store_match([],_Key,Rest)
819		--> add_rest(Rest). % these bindings were probably filtered out during replay and error messages were generated
820		delta_store_match([Bind1|T],Key,[Bind2|T2]) -->
821		{is_bind(Bind1,ID,Val), is_bind(Bind2,ID,Val2)},
822		!,
823		({check_value_equal(ID,Val,Val2)}
824		-> []
825		; %translate_bvalue_with_limit(Val,100,V1), translate_bvalue_with_limit(Val2,100,V2),
826		[ID] % TO DO: provided detailed explanation using values
827		),delta_store_match(T,Key,T2).
828		delta_store_match([_ID|T],Key,PartialStore) --> delta_store_match(T,Key,PartialStore).
829
830		add_rest([]) --> [].
831		add_rest([Bind|T]) --> {is_bind(Bind,ID,_)}, [ID], add_rest(T).
832
833		% -----------------------
834
835		replay_json_trace_file(FileName,ReplayStatus) :-
836		replay_json_trace_file_with_check(FileName,_,ReplayStatus,TransIds,_),
837		try_set_trace_by_transition_ids(TransIds).
838
839
840		% generate error/warning for imperfect or partial replay
841		replay_json_trace_file_with_check(FileName,Trace,ReplayStatus,TransIds,MatchInfoList) :-
842		replay_json_trace_file(FileName,Trace,ReplayStatus,TransIds,MatchInfoList),
843		length(TransIds,Steps),
844		length(Trace,AllSteps),
845		check_replay_status(ReplayStatus,Steps,AllSteps).
846
847		check_replay_status(imperfect,Steps,_) :- !,
848		ajoin(['Imperfect replay, steps replayed: '],Msg),
849		add_warning(replay_json_trace_file,Msg, Steps).
850		check_replay_status(partial,Steps,AllSteps) :- !,
851		ajoin(['Replay of all ',AllSteps,' steps not possible, steps replayed: '],Msg),
852		add_error(replay_json_trace_file,Msg, Steps).
853		check_replay_status(perfect,Steps,_) :-
854		add_message(replay_json_trace_file,'Perfect replay possible, steps replayed: ', Steps).
855
856		% ------------
857
858		:- use_module(tools,[start_ms_timer/1, stop_ms_timer_with_msg/2]).
859		:- use_module(bmachine_construction,[dummy_machine_name/2]).
860
861		replay_json_trace_file(FileName,Trace,ReplayStatus,TransIds,MatchInfoList) :- \+ bmachine_is_precompiled,!,
862		add_error(replay_json_trace_file,'No specification loaded, cannot replay trace file:',FileName),
863		Trace=[], TransIds=[], ReplayStatus=partial, MatchInfoList=[].
864		replay_json_trace_file(FileName,Trace,ReplayStatus,TransIds,MatchInfoList) :-
865		start_ms_timer(T1),
866		read_json_trace_file(FileName,ModelName,Trace),
867		stop_ms_timer_with_msg(T1,'Loading JSON trace file'),
868		precise_match_spec(MatchSpec), % require precise replay
869		ignore_dest_match_spec(MS2),
870		opname_optimize_match_spec(MS3),
871		% was ignore_return_match_spec(MS3), % TODO: when no return and no non-det vars: do not try MS3
872		start_ms_timer(T2),
873		temporary_set_preference(deterministic_trace_replay,true,CHNG),
874		replay_trace(Trace,[MatchSpec,MS2,MS3],[],1,root,TransIds,_DestID,RestTrace,MatchInfoList),
875		reset_temporary_preference(deterministic_trace_replay,CHNG),
876		stop_ms_timer_with_msg(T2,'Replaying JSON trace file'),
877		!,
878		(RestTrace = []
879		-> ((match_spec_was_used(MS3) % Grade=3
880		; match_spec_was_used(MS2) %Grade=2
881		; member(replay_step(_,Errs),MatchInfoList), replay_error_occured(Errs)
882		)
883		-> ReplayStatus=imperfect,
884		check_model_name(ModelName)
885		; ReplayStatus=perfect
886		)
887		; ReplayStatus=partial,
888		check_model_name(ModelName)
889		).
890
891		:- use_module(specfile,[currently_opened_specification_name/1]).
892		check_model_name(ModelName) :-
893		currently_opened_specification_name(CurModelName),!,
894		(CurModelName=ModelName -> true
895		; dummy_machine_name(ModelName,CurModelName) % CurModelName = MAIN_MACHINE_FOR_...
896		-> true
897		; ModelName = 'dummy(uses)'
898		-> true % if modelName is "null" this is the value used
899		; prob2_ui_suffix(ModelName,CurModelName) ->
900		% happens when ProB2-UI saves trace files; sometimes it adds (2), ... suffix, see issue #243
901		add_message(replay_json_trace_file, 'JSON trace file model name has a ProB2-UI suffix: ', ModelName)
902		; ajoin(['JSON trace file model name ',ModelName,' does not match current model name: '],MMsg),
903		add_warning(replay_json_trace_file, MMsg, CurModelName)
904		).
905		check_model_name(ModelName) :-
906		add_warning(replay_json_trace_file, 'Cannot determine current model name to check stored name:', ModelName).
907
908		:- set_prolog_flag(double_quotes, codes).
909		:- use_module(self_check).
910		:- assert_must_succeed(b_intelligent_trace_replay:prob2_ui_suffix('b_mch', 'b')).
911		:- assert_must_succeed(b_intelligent_trace_replay:prob2_ui_suffix('b_mch (2)', 'b')).
912		:- assert_must_succeed(b_intelligent_trace_replay:prob2_ui_suffix('b (2)', 'b')).
913		:- assert_must_fail(b_intelligent_trace_replay:prob2_ui_suffix('b', 'bc')).
914		:- assert_must_fail(b_intelligent_trace_replay:prob2_ui_suffix('b (2)', 'bc')).
915		% check if name matches current model name catering for ProB2-UI quirks
916		prob2_ui_suffix(JSONModelName,CurModelName) :-
917		atom_codes(JSONModelName,JCodes),
918		atom_codes(CurModelName,TargetCodes),
919		append(TargetCodes,After,JCodes),
920		(append("_mch",After2,After)
921		-> true % .eventb package file name
922		; append(".mch",After2,After) -> true
923		; After2=After),
924		valid_prob2_ui_suffix(After2).
925
926		valid_prob2_ui_suffix([]) :- !.
927		valid_prob2_ui_suffix([32|_]). % we could check that we have (2), ... after; but is it necessary?
928
929
930		error_occured_during_replay(MatchInfoList) :-
931		member(replay_step(_,Errs),MatchInfoList), replay_error_occured(Errs),!.
932
933		% ---------------------------------
934
935		replay_prolog_trace_file(FileName) :-
936		start_ms_timer(T1),
937		read_prolog_trace_file(FileName,_ModelName,Trace),
938		stop_ms_timer_with_msg(T1,'Loading Prolog trace file'),
939		replay_prolog2(FileName,Trace).
940
941		replay_prolog2(FileName,Trace) :-
942		precise_match_spec(MatchSpec),
943		start_ms_timer(T2),
944		replay_trace(Trace,[MatchSpec],[stop_at_failure],1,root,TransIds,_DestID,RestTrace,MatchInfoList),
945		stop_ms_timer_with_msg(T2,'Replaying JSON trace file'),
946		RestTrace=[], % will initiate backtracking
947		try_set_trace_by_transition_ids(TransIds),
948		(error_occured_during_replay(MatchInfoList)
949		-> add_error(replay_prolog_trace_file,'Errors occurred during replay of file:',FileName)
950		; true).
951		replay_prolog2(FileName,_Trace) :-
952		add_error(replay_prolog_trace_file,'Could not fully replay file:',FileName).
953
954		read_prolog_trace_file(FileName,ModelName,Trace) :-
955		open(FileName,read,Stream,[encoding(utf8)]),
956		call_cleanup(parse_prolog_trace_file(FileName,Stream,ModelName,Trace),
957		close(Stream)).
958
959		parse_prolog_trace_file(File,Stream,ModelName,Trace) :-
960		safe_read_stream(Stream,0,Term),!,
961		(Term = end_of_file
962		-> Trace = [], ModelName = 'dummy(uses)',
963		add_warning(read_prolog_trace_file,'Empty trace file: ',File)
964		; (Term = machine(ModelName)
965		-> Trace = T
966		; Trace = [Term|T],
967		add_warning(read_prolog_trace_file,'File does not start with a machine/1 fact: ',Term)
968		),
969		parse_prolog_trace_file_body(Stream,1,T)
970		).
971
972		parse_prolog_trace_file_body(Stream,Step,Trace) :-
973		safe_read_stream(Stream,Step,Term),!,
974		(Term = end_of_file
975		-> Trace = []
976		; skip_prolog_term(Term)
977		-> add_message(read_prolog_trace_file,'Skipping: ',Term),
978		parse_prolog_trace_file_body(Stream,Step,Trace)
979		; Trace = [TransSpec|T],
980		convert_prolog_trace_step(Term,TransSpec),
981		S1 is Step + 1,
982		parse_prolog_trace_file_body(Stream,S1,T)
983		).
984
985		safe_read_stream(Stream,Step,T) :-
986		catch(read(Stream,T), E, (
987		ajoin(['Exception while reading step ', Step, 'of trace file: '], Msg),
988		add_error(read_prolog_trace_file,Msg,[E]),
989		T=end_of_file
990		)).
991
992		skip_prolog_term('$check_value'(_ID,_Val)).
993		convert_prolog_trace_step(Fact,
994		transition_spec(OpName,Meta,ParaStore,ResultStore,DestStore,Unchanged,PredList,[])) :-
995		PredList=[], Unchanged=[], Meta=[], DestStore = [],
996		decompose_operation(Fact,OpName,ParaStore,ResultStore).
997		% TODO: deal with '$check_value'(ID,Val)
998		% decompose an operation term into name, parameter store and result store
999		decompose_operation('-->'(OpTerm,Results),OpName,ParaStore,ResultStore) :- !,
1000		decompose_operation2(OpTerm,OpName,ParaStore),
1001		(b_get_machine_operation_result_names(OpName,ResultNames)
1002		-> create_sorted_store(ResultNames,Results,OpName,ResultStore)
1003		; ResultStore = []).
1004		decompose_operation(OpTerm,OpName,ParaStore,[]) :- decompose_operation2(OpTerm,OpName,ParaStore).
1005
1006		is_setup_or_init('$initialise_machine','$initialise_machine').
1007		is_setup_or_init(initialise_machine,'$initialise_machine'). % old style
1008		is_setup_or_init(setup_constants,'$setup_constants'). % old style
1009		is_setup_or_init(Op,Op) :- is_setup_constants_op(Op).
1010
1011		decompose_operation2(OpTerm,OpName,ParaStore) :-
1012		functor(OpTerm,Functor,Arity),
1013		is_setup_or_init(Functor,OpName),
1014		!,
1015		% the order of constants, variables etc has changed in ProB;
1016		% in general we cannot reconstruct the association of the arguments to variables or constants
1017		(Arity=0 -> true
1018		; add_message(b_intelligent_trace_replay,'Ignoring parameters of:',OpName)),
1019		ParaStore=[].
1020		decompose_operation2(OpTerm,OpName,ParaStore) :-
1021		OpTerm =.. [OpName|Paras],
1022		(b_get_machine_operation_parameter_names_for_animation(OpName,ParaNames)
1023		-> create_sorted_store(ParaNames,Paras,OpName,ParaStore)
1024		; ParaStore = [],
1025		add_error(read_prolog_trace_file,'Unknown operation in trace file:',OpName)
1026		).
1027
1028
1029		create_sorted_store([],Paras,OpName,SortedParaStore) :- Paras = [_|_],
1030		get_preference(show_eventb_any_arguments,false),!,
1031		add_message(b_intelligent_trace_replay,'Prolog trace file contains values for virtual parameters (set SHOW_EVENTB_ANY_VALUES to TRUE to better replay this trace file): ',OpName),
1032		SortedParaStore = [].
1033		create_sorted_store(ParaNames,[],_OpName,SortedParaStore) :- ParaNames = [_|_],
1034		get_preference(show_eventb_any_arguments,true),!,
1035		add_message(b_intelligent_trace_replay,'Prolog trace file contains no values for parameters (maybe SHOW_EVENTB_ANY_VALUES was FALSE when trace file was created): ',ParaNames),
1036		SortedParaStore = [].
1037		create_sorted_store(ParaNames,Paras,OpName,SortedParaStore) :-
1038		create_local_store_for_operation(ParaNames,Paras,OpName,ParaStore),
1039		sort(ParaStore,SortedParaStore).
1040
1041
1042
1043		% ------------------------
1044
1045		:- use_module(extrasrc(json_parser),[json_parse_file/3]).
1046
1047		% read a JSON ProB2-UI trace file and extract model name and transition_spec list
1048		read_json_trace_file(FileName,ModelName,Trace) :-
1049		json_parse_file(FileName,Term,[rest(_),position_infos(true),strings_as_atoms(false)]),
1050		%nl,print(Term),nl,nl,
1051		!,
1052		(extract_json_model_name(Term,M) -> ModelName=M ; ModelName = 'dummy(uses)'),
1053		(translate_json_trace_term(Term,FileName,Trace) -> true
1054		; add_error(read_json_trace_file,'Could not translate JSON transitionList: ',Term),
1055		Trace = []).
1056
1057		% small JSON utilities; to do: merge with VisB utilities and factor out
1058		get_json_attribute(Attr,ObjList,Value) :- member(Equality,ObjList),
1059		is_json_equality_attr(Equality,Attr,Value).
1060		get_json_attribute_with_pos(Attr,ObjList,File,Value,Pos) :-
1061		member(Equality,ObjList),
1062		is_json_equality_attr_with_pos(Equality,File,Attr,Value,Pos).
1063
1064		is_json_equality_attr('='(Attr,Val),Attr,Val).
1065		is_json_equality_attr('='(Attr,Val,_Pos),Attr,Val). % we have position infos
1066
1067		is_json_equality_attr_with_pos('='(Attr,Val),_File,Attr,Val,unknown).
1068		is_json_equality_attr_with_pos('='(Attr,Val,JPos),File,Attr,Val,ProBPos) :- create_position(JPos,File,ProBPos).
1069
1070		create_position(From-To,File,ProBPos) :-
1071		ProBPos=src_position_with_filename_and_ec(From,1,To,1,File).
1072		% --------
1073
1074		:- use_module(probsrc(preferences), [reset_temporary_preference/2,temporary_set_preference/3, get_preference/2]).
1075		translate_json_trace_term(json(ObjList),FileName,Trace) :-
1076		get_json_key_list(transitionList,ObjList,List),
1077		List \= [], % optimization, dont set preferences
1078		!,
1079		% TODO: why is this not a call_cleanup?
1080		temporary_set_preference(repl_cache_parsing,true,CHNG),
1081		eval_strings:turn_normalising_off,
1082		maplist(translate_json_operation(FileName),List,Trace),
1083		eval_strings:turn_normalising_on,
1084		reset_temporary_preference(repl_cache_parsing,CHNG).
1085
1086		% no transitionList => just use empty list
1087		translate_json_trace_term(json(_),_,[]) :- !.
1088
1089		% extract model name from metadata which looks like this
1090		/*
1091		"metadata": {
1092		"fileType": "Trace",
1093		"formatVersion": 1,
1094		"savedAt": "2021-10-13T13:38:02Z",
1095		"creator": "tcltk (leuschel)",
1096		"proBCliVersion": "1.11.1-nightly",
1097		"proBCliRevision": "3cb800bbadfeaf4f581327245507a55ae5a5e66d",
1098		"modelName": "scheduler",
1099		"modelFile": "/Users/bourkaki/B/Benchmarks/scheduler.mch"
1100		}
1101		*/
1102
1103		extract_json_model_name(json(ObjList),MachineName) :-
1104		get_json_key_object(metadata,ObjList,List),
1105		get_json_attribute(modelName,List,string(MC)),
1106		atom_codes(MachineName,MC).
1107
1108
1109		% translate a single JSON transition entry into a transition_spec term for replay_trace
1110		/* here is a typical entry for the scheduler model:
1111		{
1112		"name": "ready",
1113		"params": {
1114		"rr": "process3"
1115		},
1116		"results": {
1117		},
1118		"destState": {
1119		"active": "{process3}",
1120		"waiting": "{}"
1121		},
1122		"destStateNotChanged": [
1123		"ready"
1124		],
1125		"preds": null
1126		},
1127		*/
1128		translate_json_operation(FileName,json(Json),
1129		transition_spec(OpName,Meta,
1130		ParaStore,ResultStore,DestStore,Unchanged,PredList,Postconditions) ) :-
1131		(get_json_attribute_with_pos(name,Json,FileName,string(OpNameC),Position)
1132		-> atom_codes(OpName,OpNameC)
1133		; get_json_attribute_with_pos(_SomeOtherAttr,Json,FileName,_,Position)
1134		-> add_message(translate_json_operation,'Transition has no JSON "name" attribute','',Position),
1135		OpName = ''
1136		; OpName = '', Position=unknown,
1137		add_error(translate_json_operation,'Transition has no JSON "name" or other attribute in file: ',FileName,Position)
1138		),
1139		(debug_mode(off) -> true ; add_message(translate_json_operation,'Processing operation: ',OpName,Position)),
1140		(get_json_key_object(params,Json,Paras)
1141		-> translate_json_paras(Paras,params(OpName),FileName,OpName,Bindings),
1142		sort(Bindings,ParaStore) % put the parameters into the standard Prolog order
1143		; ParaStore = []
1144		),
1145		(get_json_key_object(results,Json,ResParas)
1146		-> translate_json_paras(ResParas,results(OpName),FileName,OpName,Bindings2),
1147		sort(Bindings2,ResultStore)
1148		; ResultStore = []
1149		),
1150		(get_json_key_object(destState,Json,DestState)
1151		-> translate_json_paras(DestState,destState,FileName,OpName,Bindings3),
1152		sort(Bindings3,DestStore)
1153		; DestStore = []
1154		),
1155		(get_json_key_list(destStateNotChanged,Json,UnchList)
1156		-> maplist(translate_json_string,UnchList,UnchAtoms),
1157		sort(UnchAtoms,Unchanged)
1158		; Unchanged = []
1159		),
1160		(get_json_key_list(preds,Json,JPredList)
1161		-> (maplist(translate_json_pred,JPredList,PredList) -> true
1162		; add_error(translate_json_operation,'Unable to parse predicates for operation:',OpName,Position),
1163		PredList = []
1164		)
1165		; PredList = []
1166		),
1167		(get_json_key_list(postconditions,Json,PostconditionList)
1168		-> maplist(translate_postcondition,PostconditionList,Postconditions)
1169		; Postconditions = []
1170		),
1171		(get_json_attribute(description,Json,string(DescCodes))
1172		-> atom_codes(Desc,DescCodes), Meta = [description/Desc,pos/Position]
1173		; Meta = [pos/Position]
1174		).
1175
1176		translate_postcondition(Json,Postcondition) :-
1177		get_json_attribute(kind,Json,string(KindCodes)),
1178		atom_codes(Kind,KindCodes),
1179		(translate_postcondition_kind(Kind,Json,Postcondition) -> true ; add_error(translate_postcondition,'translate_postcondition_kind failed',Json), fail).
1180
1181		translate_postcondition_kind('PREDICATE',Json,state_predicate(TPred)) :-
1182		!,
1183		get_json_attribute(predicate,Json,PredString),
1184		translate_json_pred(PredString,TPred).
1185		translate_postcondition_kind(Kind,Json,operation_enabled(OpName,TPred,Enabled)) :-
1186		enabled_kind(Kind,Enabled),
1187		!,
1188		get_json_attribute(operation,Json,string(OpNameCodes)),
1189		atom_codes(OpName,OpNameCodes),
1190		get_json_attribute(predicate,Json,PredString),
1191		(PredString = string([]) -> TPred = b(truth,pred,[])
1192		; translate_json_pred(PredString,TPred)
1193		).
1194
1195		enabled_kind('ENABLEDNESS',enabled).
1196		enabled_kind('DISABLEDNESS',disabled).
1197
1198
1199		get_json_key_object(Key,JSON,Object) :-
1200		get_json_attribute(Key,JSON,JObject),
1201		JObject \= @(null),
1202		(JObject = json(Object) -> true
1203		; add_internal_error('Illegal JSON object for key:',Key:JObject),
1204		fail
1205		).
1206		get_json_key_list(Key,JSON,List) :-
1207		get_json_attribute(Key,JSON,JList),
1208		JList \= @(null),
1209		(JList = array(List) -> true
1210		; add_internal_error('Illegal JSON list for key:',Key:JList),
1211		fail
1212		).
1213
1214		translate_json_string(string(AtomCodes),Atom) :- atom_codes(Atom,AtomCodes).
1215
1216		translate_json_paras([],_,_,_,R) :- !, R=[].
1217		translate_json_paras([Eq|T],Kind,FileName,OpName,[Bind|BT]) :-
1218		translate_json_para(Eq,Kind,FileName,OpName,Bind),!,
1219		translate_json_paras(T,Kind,FileName,OpName,BT).
1220		translate_json_paras([_|T],Kind,FileName,OpName,BT) :- translate_json_paras(T,Kind,FileName,OpName,BT).
1221
1222
1223		:- use_module(library(codesio),[read_from_codes/2]).
1224		:- use_module(probsrc(b_global_sets),[add_prob_deferred_set_elements_to_store/3]).
1225		translate_json_para(Equality,_Kind,FileName,OpName,json_bind(Name,Value,any,Pos)) :-
1226		xtl_mode,
1227		is_json_equality_attr_with_pos(Equality,FileName,Name,string(ExprCodes0),Pos),
1228		!,
1229		(append(_,[46],ExprCodes0) % add dot: 46 = '.' if required
1230		-> ExprCodes1 = ExprCodes0
1231		; append(ExprCodes0,[46],ExprCodes1)
1232		),
1233		catch(read_from_codes(ExprCodes1,Value),_E,
1234		(add_parameter_error('read term from JSON failed',Name,ExprCodes0,OpName,Pos),
1235		Value = '')).
1236		% TO DO: using eval_strings is very ugly, use a better API predicate
1237		translate_json_para(Equality,Kind,FileName,OpName,json_bind(Name,Value,Type,Pos)) :-
1238		\+ xtl_mode,
1239		is_json_equality_attr_with_pos(Equality,FileName,Name,string(ExpressionCodes),Pos),
1240		!,
1241		%format('Translating JSON Para ~w : ~s~n',[Name,C]),
1242		(eval_strings:repl_parse_expression(ExpressionCodes,Typed,Type,Error)
1243		-> (Error \= none -> add_parameter_error(Error,Name,ExpressionCodes,OpName,Pos)
1244		; Type = pred -> add_parameter_error('use of predicate instead of expression',Name,ExpressionCodes,OpName,Pos)
1245		; Type = subst -> add_parameter_error('unexpected substitution',Name,ExpressionCodes,OpName,Pos)
1246		; (add_prob_deferred_set_elements_to_store([],EState,visible), % value should not depend on any state
1247		eval_strings:eval_expression_direct(Typed,EState,Value)
1248		-> \+ illegal_json_binding_type(Kind,Name,Type,Pos)
1249		; add_parameter_error('evaluation error',Name,ExpressionCodes,OpName,Pos)
1250		)
1251		)
1252		; add_parameter_error('parsing failed error',Name,ExpressionCodes,OpName,Pos)
1253		).
1254		translate_json_para(Para,_,_,_,_) :-
1255		add_error(translate_json_para,'Unknown JSON para:',Para),fail.
1256
1257		:- use_module(specfile,[translate_operation_name/2]).
1258		add_parameter_error(Error,Name,ExpressionCodes,OpName,Pos) :-
1259		translate_operation_name(OpName,TOp),
1260		ajoin(['Ignoring JSON value for parameter ',Name,' of ',TOp,' due to ',Error,':'], Msg),
1261		atom_codes(A,ExpressionCodes),
1262		add_error(translate_json_para,Msg,A,Pos),fail.
1263
1264		%evaluate_codes_value(ExpressionCodes,Type,Value) :-
1265		% eval_strings:repl_parse_expression(ExpressionCodes,Typed,Type,Error), Error=none,
1266		% eval_strings:eval_expression_direct(Typed,Value).
1267
1268		illegal_json_binding_type(destState,ID,Type,Pos) :- get_expected_type(ID,Kind,ExpectedType),!,
1269		\+ unify_types_strict(Type,ExpectedType), pretty_type(Type,TS), pretty_type(ExpectedType,ETS),
1270		ajoin(['Ignoring JSON destState value for ',Kind,' ',ID,' due to illegal type ',TS, ', expected:'], Msg),
1271		add_error(translate_json_para,Msg,ETS,Pos).
1272		illegal_json_binding_type(destState,ID,_Type,Pos) :-
1273		add_error(translate_json_para,'Ignoring JSON destState value for unknown identifier:',ID,Pos).
1274		% unknown operations are now dealt with later in check_and_adapt_trace_step
1275		%illegal_json_binding_type(params(Op),ID,_Type,Pos) :-
1276		% b_or_z_mode, % otherwise no types available
1277		% \+ b_top_level_operation(Op), !,
1278		% findall(KOpid,b_top_level_operation(KOpid),Ops),
1279		% (get_possible_fuzzy_matches_and_completions_msg(Op,Ops,FMsg)
1280		% -> ajoin(['Ignoring JSON value for parameter ',ID,' of unknown operation (did you mean the operation ',FMsg,' ?) : '], Msg)
1281		% ; ajoin(['Ignoring JSON value for parameter ',ID,' of unknown operation: '], Msg)),
1282		% add_error(translate_json_para,Msg,Op,Pos).
1283		illegal_json_binding_type(params(Op),ID,Type,Pos) :-
1284		b_or_z_mode, % otherwise no types available
1285		b_top_level_operation(Op),
1286		b_get_machine_operation_typed_parameters_for_animation(Op,Params),
1287		member(b(identifier(ID),ExpectedType,_),Params),!,
1288		\+ unify_types_strict(Type,ExpectedType), pretty_type(Type,TS), pretty_type(ExpectedType,ETS),
1289		ajoin(['Ignoring JSON value for parameter ',ID,' of operation ', Op, ' due to illegal type ',TS, ', expected:'], Msg),
1290		add_error(translate_json_para,Msg,ETS,Pos).
1291		illegal_json_binding_type(params(Op),ID,_Type,Pos) :-
1292		b_or_z_mode, % otherwise show_eventb_any_arguments makes no sense
1293		b_top_level_operation(Op),
1294		(b_get_machine_operation_typed_parameters_for_animation(Op,[]),
1295		get_preference(show_eventb_any_arguments,false)
1296		% TODO: check if ID is a valid virtual parameter, or if trace file was generated with preference set to true
1297		-> ajoin(['Ignoring JSON value for parameter ',ID,', operation has no parameters (setting SHOW_EVENTB_ANY_VALUES to TRUE may help):'],Msg)
1298		; ajoin(['Ignoring JSON value for unknown parameter ',ID,' for:'],Msg)
1299		),
1300		add_error(translate_json_para,Msg,Op,Pos).
1301		illegal_json_binding_type(results(Op),ID,Type,Pos) :-
1302		b_or_z_mode, % otherwise there are no typred results available
1303		b_get_machine_operation_typed_results(Op,Results), member(b(identifier(ID),ExpectedType,_),Results),!,
1304		\+ unify_types_strict(Type,ExpectedType), pretty_type(Type,TS), pretty_type(ExpectedType,ETS),
1305		ajoin(['Ignoring JSON value for result ',ID,' of operation ', Op, ' due to illegal type ',TS], Msg),
1306		add_error(translate_json_para,Msg,ETS,Pos).
1307		% unknown operations are now dealt with later in check_and_adapt_trace_step
1308		%illegal_json_binding_type(results(_Op),ID,_Type,Pos) :-
1309		% add_error(translate_json_para,'Ignoring JSON value for unknown operation result:',ID,Pos).
1310
1311		get_expected_type(ID,variable,ExpectedType) :- bmachine_is_precompiled, b_is_variable(ID,ExpectedType).
1312		get_expected_type(ID,constant,ExpectedType) :- bmachine_is_precompiled, b_is_constant(ID,ExpectedType).
1313
1314		% TODO: already check results, ...
1315
1316		translate_json_pred(string(PredCodes),TPred) :-
1317		OuterQuantifier = no_quantifier,
1318		% TO DO: parse in context of operation ! otherwise we get type error for pp=pp for example where pp is a parameter
1319		eval_strings:repl_parse_predicate(PredCodes,OuterQuantifier,TPred,_TypeInfo). % , print(pred_ok(TPred)),nl.
1320
1321		/*
1322		after reading a JSON ProB2-UI file looks like this:
1323
1324		json([description=string([70,105,108,101,32,99,114,101,97,116,101,100,32,98,121,32,80,114,111,66,32,84,99,108,47,84,107]),transitionList=array([json([name=string([36,105,110,105,116,105,97,108,105,115,101,95,109,97,99,104,105,110,101]),params=json([]),results=json([]),destState=json([active=string([123,125]),ready=string([123,125]),waiting=string([123,125])]),destStateNotChanged=array([]),preds=@(null)]),json([name=string([110,101,119]),params=json([pp=string([112,114,111,99,101,115,115,51])]),results=json([]),destState=json([waiting=string([123,112,114,111,99,101,115,115,51,125])]),destStateNotChanged=array([string([97,99,116,105,118,101]),string([114,101,97,100,121])]),preds=@(null)]),json([name=string([114,101,97,100,121]),params=json([rr=string([112,114,111,99,101,115,115,51])]),results=json([]),destState=json([active=string([123,112,114,111,99,101,115,115,51,125]),waiting=string([123,125])]),destStateNotChanged=array([string([114,101,97,100,121])]),preds=@(null)]),json([name=string([115,119,97,112]),params=json([]),results=json([]),destState=json([active=string([123,125]),waiting=string([123,112,114,111,99,101,115,115,51,125])]),destStateNotChanged=array([string([114,101,97,100,121])]),preds=@(null)]),json([name=string([110,101,119]),params=json([pp=string([112,114,111,99,101,115,115,50])]),results=json([]),destState=json([waiting=string([123,112,114,111,99,101,115,115,50,44,112,114,111,99,101,115,115,51,125])]),destStateNotChanged=array([string([97,99,116,105,118,101]),string([114,101,97,100,121])]),preds=@(null)])]),metadata=json([fileType=string([84,114,97,99,101]),formatVersion=number(1),savedAt=string([50,48,50,49,45,49,48,45,49,51,84,49,51,58,51,56,58,48,50,90]),creator=string([116,99,108,116,107,32,40,108,101,117,115,99,104,101,108,41]),proBCliVersion=string([49,46,49,49,46,49,45,110,105,103,104,116,108,121]),proBCliRevision=string([51,99,98,56,48,48,98,98,97,100,102,101,97,102,52,102,53,56,49,51,50,55,50,52,53,53,48,55,97,53,53,97,101,53,97,53,101,54,54,100]),modelName=string([115,99,104,101,100,117,108,101,114]),modelFile=string([47,85,115,101,114,115,47,108,101,117,115,99,104,101,108,47,103,105,116,95,114,111,111,116,47,112,114,111,98,95,101,120,97,109,112,108,101,115,47,112,117,98,108,105,99,95,101,120,97,109,112,108,101,115,47,66,47,66,101,110,99,104,109,97,114,107,115,47,115,99,104,101,100,117,108,101,114,46,109,99,104])])])
1325
1326		*/
1327
1328		% -------------------------
1329
1330		% Interactive Trace Replay API
1331
1332		% load a trace file and store it for interactive replay
1333		load_json_trace_file_for_ireplay(FileName) :-
1334		read_json_trace_file(FileName,ModelName,Trace),
1335		reset_json_trace_replay,
1336		store_json_trace(Trace,0,Len),
1337		assert(current_replay_step(1)),
1338		assert(loaded_json_trace_file(FileName,ModelName,Len)).
1339
1340		:- dynamic loaded_json_trace_file/3, json_trace_replay_step/3.
1341		:- dynamic current_replay_step/1, json_trace_replayed_info/2.
1342
1343
1344		:- use_module(eventhandling,[register_event_listener/3]).
1345		:- register_event_listener(clear_specification,reset_json_trace_replay,
1346		'Reset interactive trace replay.').
1347
1348		reset_json_trace_replay :-
1349		retractall(current_replay_step(_)),
1350		retractall(loaded_json_trace_file(_,_,_)),
1351		retractall(json_trace_replay_step(_,_,_)),
1352		retractall(json_trace_replayed_info(_,_)).
1353
1354		store_json_trace([],L,L).
1355		store_json_trace([TransSpec|T],StepNr,Len) :-
1356		S1 is StepNr + 1,
1357		get_transition_spec_txt(TransSpec,TTxt),
1358		formatsilent_with_colour(user_output,[blue],'==> Trace step ~w: ~w~n',[S1,TTxt]),
1359		phrase(check_and_adapt_trace_step(TransSpec,S1,CorrectedTransSpec),StaticErrors),
1360		assert(json_trace_replay_step(S1,CorrectedTransSpec,StaticErrors)),
1361		store_json_trace(T,S1,Len).
1362
1363		get_trace_step_info(StepNr,StepDescr) :-
1364		json_trace_replay_step(StepNr,TransSpec,StaticErrors),
1365		get_transition_spec_txt(TransSpec,TTxt),
1366		(StaticErrors = [] -> StaticTT=[]
1367		; length(StaticErrors,NrStaticErrors),
1368		StaticTT = [' (static errors: ',NrStaticErrors,')']
1369		),
1370		(json_trace_replayed_info(StepNr,Info),
1371		get_replay_info_text(Info,TextAtoms)
1372		-> append(StaticTT,TextAtoms,TT),
1373		ajoin([StepNr,': ',TTxt | TT],StepDescr)
1374		; ajoin([StepNr,': ',TTxt | StaticTT],StepDescr)
1375		).
1376
1377		get_replay_info_text(replay(FromID,TransID,MatchInfo,Errors),TextAtoms) :-
1378		transition(FromID,OperationTerm,TransID,_ToID),
1379		translate_event_with_limit(OperationTerm,40,OpTxt),
1380		!,
1381		(Errors=[] -> TextAtoms = [' * REPLAYED (', MatchInfo,') : ',OpTxt]
1382		; length(Errors,NrErrors),
1383		TextAtoms = [' * REPLAYED (', MatchInfo, ', errors: ',NrErrors,') : ', OpTxt]
1384		).
1385		get_replay_info_text(skipped,[' SKIPPED']) :- !.
1386		get_replay_info_text(X,[X]).
1387
1388		tk_get_stored_json_trace_description(list(List)) :-
1389		findall(StepDescr,get_trace_step_info(_,StepDescr),List).
1390
1391		get_stored_json_replay_steps(List) :-
1392		findall(ireplay_step(StepNr,TTxt,StaticErrors),
1393		(json_trace_replay_step(StepNr,TransSpec,RErrors),
1394		maplist(get_rerror,RErrors,StaticErrors),
1395		get_transition_spec_txt(TransSpec,TTxt)),
1396		List).
1397
1398		try_replay_next_step(MatchSpecs,CurStepNr,FromID,TransID,DestId,MatchInfo,TkTransInfos,TkErrors) :-
1399		(var(CurStepNr) -> current_replay_step(CurStepNr) ; true), % allow to pass a fixed Nr from ProB2
1400		(var(FromID) -> current_state_id(FromID) ; true), % allow to pass a fixed ID from ProB2
1401		json_trace_replay_step(CurStepNr,TransSpec,StaticErrors),
1402		flexible_perform_single_replay_step(FromID,TransID,DestId,MatchSpecs,TransSpec,MatchInfo),
1403		phrase(check_step_postconditions(TransSpec,DestId),Errors,StaticErrors),
1404		get_transition_name(FromID,TransID,OpName),
1405		length(Errors,NrErrs),
1406		formatsilent_with_colour(user_output,[green], '==> Replay step ~w (~w) ~w leading to state ~w~n',[CurStepNr,MatchInfo,OpName,DestId]),
1407		(NrErrs>0 -> formatsilent_with_colour(user_output,[orange],' Errors (~w): ~w~n',[NrErrs,Errors]) ; true),
1408		findall(TInfo,get_transition_info(TransSpec,TInfo),TkTransInfos),
1409		maplist(get_rerror,Errors,TkErrors). % make errors atomic for Tk
1410
1411		get_rerror(Err,Msg) :- get_replay_error(Err,Msg),!.
1412		get_rerror(Err,Msg) :- atom(Err),!,Msg=Err.
1413		get_rerror(Err,F) :- functor(Err,F,_).
1414
1415		:- use_module(translate,[translate_bexpression_with_limit/3]).
1416		% get text descriptions for a transition_spec, to be shown to user e.g. in Tk listbox:
1417		get_transition_info(transition_spec(_Op, _Meta, Paras, Results, DestStore,_UnchangedVars,_Preds,_Post),InfoTxt) :-
1418		(Kind=para, List=Paras
1419		; Kind=result, List=Results
1420		; Kind=dest, List=DestStore),
1421		get_binding_txt(List,Txt),
1422		ajoin([Kind,' : ',Txt],InfoTxt).
1423		get_transition_info(transition_spec(_Op, _, _, _, _,UnchangedVars,_,_),InfoTxt) :-
1424		member(ID,UnchangedVars),
1425		ajoin(['unchanged : ',ID],InfoTxt).
1426		get_transition_info(transition_spec(_Op, _, _, _, _,_,Preds,_),InfoTxt) :-
1427		member(TP,Preds),
1428		translate_bexpression_with_limit(TP,250,TPS),
1429		ajoin(['pred : ',TPS],InfoTxt).
1430
1431		get_binding_txt(List,BindingText) :-
1432		member(json_bind(Var,Value,_ValType,_ValPos),List),
1433		translate_bvalue_with_limit(Value,200,VS),
1434		ajoin([Var,'=',VS],BindingText).
1435
1436		default_match_specs([MatchSpec,MS2,MS3]) :-
1437		precise_match_spec(MatchSpec), % require precise replay
1438		ignore_dest_match_spec(MS2),
1439		opname_optimize_match_spec(MS3).
1440
1441		%:- public ireplay/0.
1442		%ireplay :- default_match_specs(MS),
1443		% ireplay(MS).
1444		%
1445		%
1446		%ireplay(MatchSpecs) :-
1447		% replay_current_step(MatchSpecs,_),!,
1448		% ireplay(MatchSpecs).
1449		%ireplay(MatchSpecs) :-
1450		% skip_current_ireplay_step(_),
1451		% ireplay(MatchSpecs).
1452
1453		% get information about how the status of replaying a loaded trace is:
1454		get_ireplay_status(CurStepNr,Steps,Finished) :-
1455		loaded_json_trace_file(_,_,Steps),
1456		current_replay_step(CurStepNr),
1457		(CurStepNr =< Steps
1458		-> Finished=not_finished
1459		; Finished=finished).
1460
1461		replay_of_current_step_is_possible(CurStepNr,OpName,MatchInfo,list(TransInfos),list(Errors)) :- % Tk
1462		default_match_specs(MS),
1463		try_replay_next_step(MS,CurStepNr,FromID,TransID,_DestId,MatchInfo,TransInfos,Errors),
1464		get_transition_name(FromID,TransID,OpName).
1465
1466		replay_of_current_step_is_possible_with_trans(CurStepNr,FromID,OpTerm,MatchInfo,list(Errors)) :- % ProB2
1467		default_match_specs(MS),
1468		try_replay_next_step(MS,CurStepNr,FromID,TransID,DestID,MatchInfo,_TransInfos,Errors),
1469		create_op_transition(FromID,TransID,DestID,OpTerm).
1470
1471		create_op_transition(FromID,TransID,DestID,op(TransID,OpName,FromID,DestID)) :-
1472		get_transition_name(FromID,TransID,OpName).
1473
1474		% try and replay as much as possible
1475		ireplay_fast_forward(NrReplayed) :-
1476		default_match_specs(MS), ireplay_fast_forward(MS,0,NrReplayed).
1477
1478		ireplay_fast_forward(MatchSpecs,Nr,NrReplayed) :-
1479		replay_current_step(MatchSpecs,_),!,
1480		N1 is Nr+1,
1481		ireplay_fast_forward(MatchSpecs,N1,NrReplayed).
1482		ireplay_fast_forward(_,NrReplayed,NrReplayed).
1483
1484		ireplay_fast_forward_with_trans(CurStepNr,FromID,NrReplayed,Transitions,MatchInfos,Errors) :- % for ProB2
1485		default_match_specs(MS),
1486		ireplay_fast_forward_with_trans(MS,CurStepNr,FromID,0,NrReplayed,Transitions,MatchInfos,Errors).
1487		ireplay_fast_forward_with_trans(MS,CurStepNr,FromID,Nr,NrReplayed,[OpTerm|T1],[MatchInfo|M1],[Errors|E1]) :-
1488		replay_current_step_with_trans(MS,CurStepNr,FromID,OpTerm,MatchInfo,Errors),!,
1489		OpTerm = op(_,_,_,DestID),
1490		N1 is Nr+1,
1491		NextStepNr is CurStepNr+1,
1492		ireplay_fast_forward_with_trans(MS,NextStepNr,DestID,N1,NrReplayed,T1,M1,E1).
1493		ireplay_fast_forward_with_trans(_,_,_,NrReplayed,NrReplayed,[],[],[]).
1494
1495		% replay the currently selected step of the JSON trace, matching one step of the trace with one animation step
1496		replay_current_step(CurStepNr) :- % Tk
1497		default_match_specs(MS), replay_current_step(MS,CurStepNr).
1498
1499		% try and replay current step according to match specifications
1500		replay_current_step(MatchSpecs,CurStepNr) :-
1501		try_replay_next_step(MatchSpecs,CurStepNr,FromID,TransID,_DestID,MatchInfo,_,Errors),!,
1502		extend_trace_by_transition_ids([TransID]), % update state space
1503		assert(json_trace_replayed_info(CurStepNr,replay(FromID,TransID,MatchInfo,Errors))),
1504		increase_step_nr.
1505
1506		%replay_current_step_with_trans(FromID,OpTerm,MatchInfo,Errors) :- % ProB2
1507		% default_match_specs(MS),
1508		% replay_current_step_with_trans(MS,FromID,OpTerm,MatchInfo,Errors).
1509		replay_current_step_with_trans(MatchSpecs,CurStepNr,FromID,OpTerm,MatchInfo,Errors) :- % ProB2
1510		try_replay_next_step(MatchSpecs,CurStepNr,FromID,TransID,DestID,MatchInfo,_,Errors),!,
1511		create_op_transition(FromID,TransID,DestID,OpTerm).
1512
1513		% skip the current replay step and go to the next one
1514		skip_current_ireplay_step(CurStepNr) :-
1515		current_replay_step(CurStepNr),
1516		json_trace_replay_step(CurStepNr,TransSpec,_StaticErrors),
1517		get_transition_spec_txt(TransSpec,TTxt),
1518		formatsilent_with_colour(user_output,[orange],'Skipping replay step ~w : ~w~n',[CurStepNr,TTxt]),
1519		assert(json_trace_replayed_info(CurStepNr,skipped)),
1520		increase_step_nr.
1521
1522		increase_step_nr :-
1523		retract(current_replay_step(CurStepNr)),
1524		S1 is CurStepNr+1,
1525		assert(current_replay_step(S1)).
1526
1527		% :- b_intelligent_trace_replay:load_json_trace_file_for_interactive_replay('/Users/leuschel/git_root/prob_examples/public_examples/B/CBC/ConstantsAndVars/MyAwesomeLift.prob2trace'), b_intelligent_trace_replay:ireplay.
1528
1529
1530