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