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 | */ |