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