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