1 | | % (c) 2009-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
2 | | % Heinrich Heine Universitaet Duesseldorf |
3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
4 | | |
5 | | |
6 | | :- module(b_trace_checking, [tcltk_check_state_sequence_from_file/1, |
7 | | tcltk_check_state_sequence_from_file_state_id/3, |
8 | | tcltk_check_sequence_from_file/3, |
9 | | check_default_trace_for_specfile/1, |
10 | | get_default_trace_file/2, get_default_trace_file/3, |
11 | | print_trace_as_fdr_check/0, |
12 | | tcltk_save_history_as_trace_file/2, tcltk_save_history_as_trace_file/3, |
13 | | perform_initialisation/0, |
14 | | find_successor_state/4, |
15 | | value_cannot_be_pretty_printed_safely/2 |
16 | | ]). |
17 | | |
18 | | :- use_module(library(lists)). |
19 | | |
20 | | :- use_module(tools). |
21 | | :- use_module(module_information,[module_info/2]). |
22 | | :- module_info(group,testing). |
23 | | :- module_info(description,'Replay saved traces; raise error if not possible. Used in regression testing.'). |
24 | | |
25 | | :- use_module(bsyntaxtree, [get_texpr_type/2, conjunct_predicates/2]). |
26 | | :- use_module(bmachine,[b_machine_name/1, b_is_operation_name/1, b_get_machine_operation_typed_parameters/2]). |
27 | | :- use_module(b_global_sets,[lookup_global_constant/2]). |
28 | | :- use_module(error_manager). |
29 | | :- use_module(debug). |
30 | | :- use_module(preferences,[get_preference/2,preference/2, |
31 | | temporary_set_preference/3,reset_temporary_preference/2, get_prob_application_type/1]). |
32 | | :- use_module(specfile,[b_or_z_mode/0, csp_mode/0, get_operation_name/2, get_operation_return_values_and_arguments/3]). |
33 | | :- use_module(translate,[translate_event/2]). |
34 | | :- use_module(state_space,[current_options/1, current_state_id/1, current_expression/2, |
35 | | max_reached_for_node/1, not_all_transitions_added/1,time_out_for_node/3]). |
36 | | :- use_module(junit_tests). |
37 | | :- use_module(tools_printing,[print_red/1, print_green/1, format_with_colour_nl/4]). |
38 | | :- use_module(tools_files,[read_file_codes/2]). |
39 | | :- use_module(store,[lookup_value_for_existing_id/3]). |
40 | | :- use_module(tcltk_interface,[tcltk_reset/0,tcltk_add_user_executed_operation_typed/4, |
41 | | tcltk_get_options/1]). |
42 | | |
43 | | :- use_module(runtime_profiler,[profile_single_call/3]). |
44 | | :- use_module(tools,[start_ms_timer/1, stop_ms_timer_with_msg/2]). |
45 | | :- use_module(bsyntaxtree, [def_get_texpr_ids/2, def_get_texpr_id/2]). |
46 | | |
47 | | % -------------------------------- |
48 | | |
49 | | % replay trace with state predicates; one predicate per line |
50 | | |
51 | | % b_trace_checking:tcltk_check_state_sequence_from_file('~/Desktop/scheduler6.ptrace'). |
52 | | |
53 | | tcltk_check_state_sequence_from_file(File) :- |
54 | | current_state_id(ID), |
55 | | tcltk_check_state_sequence_from_file_state_id(File,ID,_DestID). |
56 | | |
57 | | tcltk_check_state_sequence_from_file_state_id(File,ID,DestID) :- nonvar(ID), |
58 | | open(File,read,Stream,[encoding(utf8)]), |
59 | | format(user_output,'Opened predicate list file: ~w~n Starting from state ~w.~n',[File,ID]), |
60 | | call_cleanup(tcltk_check_state_sequence_from_file_aux(File,0,Stream,ID,DestID), |
61 | | (format(user_output,'Finished processing list file: ~w~n',[File]), |
62 | | close(Stream))). |
63 | | |
64 | | tcltk_check_state_sequence_from_file_aux(File,LineNr,Stream,ID,DestID) :- read_line(Stream,Codes), |
65 | | Codes \= end_of_file, |
66 | | L1 is LineNr+1, |
67 | | !, %print(codes(Codes)),nl, |
68 | | process_line(File,L1,Stream,Codes,ID,DestID). |
69 | | tcltk_check_state_sequence_from_file_aux(_,LineNr,_,ID,ID) :- printsilent('reached EOF at line: '), printsilent(LineNr),nls. |
70 | | |
71 | | :- use_module(bmachine,[b_parse_wo_type_machine_predicate_from_codes_to_raw_expr/2, |
72 | | b_type_check_raw_expr/4]). |
73 | | :- use_module(translate_keywords). |
74 | | |
75 | | % TO DO: also allow operation names, parameters to be specified? |
76 | | process_line(File,LineNr,Stream,Codes,ID,DestID) :- |
77 | | % insert newlines to ensure error message correct: |
78 | | insert_nl_prefix(LineNr,Codes,CodesNL), |
79 | | b_parse_wo_type_machine_predicate_from_codes_to_raw_expr(CodesNL,Parsed), |
80 | | % in case we did translate keywords (e.g., in Event-B mode); translate them back: |
81 | | translate_keywords:raw_backtranslate_keyword_ids(Parsed,Parsed2), |
82 | | % now type check the raw expression: |
83 | | b_type_check_raw_expr(Parsed2,[prob_ids(all),variables],Pred,closed), |
84 | | % bmachine:b_parse_machine_predicate_from_codes(CodesNL,[prob_ids(all),variables],Pred), |
85 | | !, |
86 | | format('Line ~w : ~w --?--> ',[LineNr,ID]),translate:print_bexpr(Pred),nl, |
87 | | find_successor_state(ID,Pred,SuccID,LineNr), |
88 | | tcltk_check_state_sequence_from_file_aux(File,LineNr,Stream,SuccID,DestID). |
89 | | process_line(_File,LineNr,_Stream,Codes,_ID,_DestID) :- |
90 | | atom_codes(Atom,Codes), |
91 | | add_error(tcltk_check_state_sequence_from_file,'Could not parse state predicate: ',Atom), |
92 | | add_error(tcltk_check_state_sequence_from_file,'Line: ',LineNr), |
93 | | %add_error(tcltk_check_state_sequence_from_file,'File: ',File), |
94 | | fail. |
95 | | |
96 | | insert_nl_prefix(N,Acc,Acc) :- N =< 1,!. |
97 | | insert_nl_prefix(N,Acc,[10,13|Res]) :- N1 is N-1, insert_nl_prefix(N1,Acc,Res). |
98 | | |
99 | | :- use_module(b_global_sets,[add_prob_deferred_set_elements_to_store/3]). |
100 | | :- use_module(specfile,[expand_const_and_vars_to_full_store/2]). |
101 | | :- use_module(state_space,[visited_expression/2, |
102 | | max_reached_for_node/1, max_reached_or_timeout_for_node/1, time_out_for_node/1]). |
103 | | :- use_module(library(codesio),[format_to_codes/3]). |
104 | | :- use_module(eventhandling, [announce_event/1]). |
105 | | |
106 | | find_successor_state(ID,Pred,NewID,_) :- |
107 | | % transition(ID,ActionOpAsTerm,OpID,SuccID), |
108 | | tcltk_get_options(_), |
109 | | current_options(Options), % print(Options),nl, |
110 | ? | member( (_,Action,ActionOpAsTerm,NewID), Options), |
111 | | state_space:visited_expression(NewID,State), |
112 | | expand_const_and_vars_to_full_store(State,EState), |
113 | | % print(try(NewID,State)),nl, |
114 | | add_prob_deferred_set_elements_to_store(EState,DEState,all), |
115 | | announce_event(start_solving), |
116 | | b_interpreter:b_test_boolean_expression_cs(Pred,[],DEState,'find successor state',ID), % deferred |
117 | | announce_event(end_solving), |
118 | | debug_println(19,successor_found(NewID)), |
119 | | print(' --> '),my_print_event(ActionOpAsTerm,_),nl,nl, |
120 | | my_perform_action_as_string(Action,ActionOpAsTerm,NewID), |
121 | | !. |
122 | | find_successor_state(ID,Pred,NewID,_LineNr) :- |
123 | ? | max_reached_or_timeout_for_node(ID), % we have not computed all options |
124 | | get_op_name_for_state(ID,OpName), print(try_providing_custom_predicate(OpName)),nl, |
125 | | tcltk_add_user_executed_operation_typed(OpName,_,Pred,NewID), % The Pred can only talk about parameters and the state before; thus this only works for setup_constants and initialise_machine |
126 | | (silent_mode(on) -> true |
127 | | ; print_green(successor_found(NewID)),nl, |
128 | | print(' --> '),print(OpName),nl), |
129 | | !. |
130 | | find_successor_state(ID,Pred,_,LineNr) :- |
131 | | % we could try and execute operation by predicate here; in case max_reached_for_node(ID) or time_out_for_node(ID) |
132 | | format('State ID = ~w; line number = ~w~n',[ID,LineNr]), |
133 | | (max_reached_for_node(ID) |
134 | | -> format_to_codes('Try increasing the MAX_OPERATIONS preference. No successor found satisfying predicate at step ~w of replay: ',[LineNr],Codes) |
135 | | ; time_out_for_node(ID) -> format_to_codes('TIME-OUT occurred. No successor found satisfying predicate at step ~w of replay: ',[LineNr],Codes) |
136 | | ; format_to_codes('No successor found satisfying predicate at step ~w of replay: ',[LineNr],Codes) |
137 | | ), |
138 | | atom_codes(Msg,Codes), |
139 | | translate:translate_bexpression(Pred,TP), |
140 | | add_error(tcltk_check_state_sequence_from_file,Msg,TP), |
141 | | fail. |
142 | | |
143 | | :- use_module(bmachine,[b_machine_has_constants_or_properties/0]). |
144 | | get_op_name_for_state(root,OP) :- !, |
145 | | (b_machine_has_constants_or_properties -> OP='$setup_constants' ; OP='$initialise_machine'). |
146 | | get_op_name_for_state(ID,'$initialise_machine') :- |
147 | | visited_expression(ID,concrete_constants(_)),!. |
148 | | %get_op_name_for_state(ID,OpName) :- bmachine:b_top_level_operation(OpName). % not supported yet |
149 | | |
150 | | % -------------------------------- |
151 | | |
152 | | check_default_trace_for_specfile(File) :- get_default_trace_file(File,TFile), |
153 | | tcltk_check_sequence_from_file(prolog,TFile,default_trace_replay). |
154 | | |
155 | | get_default_trace_file(File,TraceFile) :- |
156 | | get_default_trace_file(File,'.trace',TraceFile). |
157 | | get_default_trace_file(File,Ext,TraceFile) :- |
158 | | split_filename(File,FN,_MchExt), |
159 | | string_concatenate(FN,Ext,TraceFile). |
160 | | |
161 | | :- use_module(tools_printing,[print_error/1]). |
162 | | % valid Style: prolog, json |
163 | | % valid Mode: deterministic_trace_replay or backtracking_trace_replay or default_trace_replay |
164 | | tcltk_check_sequence_from_file(Style,File,Mode) :- get_mode_value(Mode,Val,Msg),!, |
165 | | temporary_set_preference(deterministic_trace_replay,Val,CHNG), |
166 | | format(Msg,[File]), |
167 | | (tcltk_check_sequence_from_file2(Style,File) |
168 | | -> reset_temporary_preference(deterministic_trace_replay,CHNG) |
169 | | ; reset_temporary_preference(deterministic_trace_replay,CHNG)). |
170 | | tcltk_check_sequence_from_file(Style,File,_DetOrBacktrack) :- |
171 | | tcltk_check_sequence_from_file2(Style,File). |
172 | | |
173 | | get_mode_value(deterministic_trace_replay,true,Msg) :- |
174 | | Msg = 'Performing deterministic replay (lower memory usage, but no backtracking in case replay fails) for file: ~w~n'. |
175 | | get_mode_value(backtracking_trace_replay,false,Msg) :- |
176 | | Msg = 'Performing replay with backtracking for file: ~w~n'. |
177 | | get_mode_value(Other,_,_) :- Other \= default_trace_replay, |
178 | | add_error(b_trace_checking,'Illegal replay mode: ',Other),fail. |
179 | | |
180 | | :- use_module(tools, [get_modulename_filename/2]). |
181 | | tcltk_check_sequence_from_file2(Style,File) :- |
182 | | read_trace_file(Style,File,MachineName,Trace), |
183 | | length(Trace,Len), |
184 | | (b_or_z_mode -> b_machine_name(OurName) ; true), |
185 | | (OurName=MachineName -> true |
186 | | ; MachineName = 'dummy(uses)' % old trace files have these |
187 | | -> printsilent_message('Checking file for machine: '), printsilent_message(OurName) |
188 | | ; atom_concat('MAIN_MACHINE_FOR_',MachineName,OurName) -> true |
189 | | ; print_error('### Trace File has been generated for different machine: '), |
190 | | print_error(MachineName), |
191 | | print_error('### Our machine: '), print_error(OurName) |
192 | | ), |
193 | | formatsilent('Starting trace check of length ~w~n',[Len]), |
194 | | statistics(walltime,[Time1,_]), |
195 | ? | (perform_sequence_of_operations(Trace) |
196 | | -> nls,print_green('Trace checking successful !'),nl |
197 | | ; nls, |
198 | | length(Trace,Len), max_nr_replayed(Replayed), |
199 | | ajoin(['Trace Checking was not successful for ', MachineName, |
200 | | ', replayed ',Replayed,'/',Len,' operations from:'],Msg), |
201 | | add_error(trace_checking_fails,Msg,File) |
202 | | %% ,throw(trace_checking_failed(MachineName)) % comment in if you want to stop immediately upon such an error |
203 | | ), |
204 | | statistics(walltime,[Time2,_]), Time is Time2-Time1, |
205 | | formatsilent('Walltime: ~w ms~n',[Time]), |
206 | | (csp_mode -> print_trace_as_fdr_check ; true), |
207 | | |
208 | | (junit_mode(_) -> (get_error(trace_checking,Errors) -> V=error([Errors]) ; V=pass), |
209 | | get_modulename_filename(MachineName, Module), |
210 | | create_and_print_junit_result(['Trace_checking',Module], File, Time, V) |
211 | | ; true). |
212 | | |
213 | | :- use_module(extrasrc(json_parser),[json_parse_file/3]). |
214 | | read_trace_file(prolog,File,MachineName,Trace) :- |
215 | | formatsilent('% Opening trace file: ~w~n',[File]), |
216 | | my_see(File), |
217 | | parse_trace_file(MachineName,Trace),!, |
218 | | seen. |
219 | | read_trace_file('B',File,MachineName,Trace) :- !, |
220 | | MachineName = 'dummy(uses)', % name not stored in B operation call files |
221 | | format('Parsing operation calls from file: ~w~n',[File]), |
222 | | read_file_codes(File,Codes), |
223 | | %parsercall:parse_substitution(Codes,Tree), tools_printing:nested_print_term(Tree),nl, |
224 | | bmachine:b_parse_machine_subsitutions_from_codes(Codes,[operation_bodies,prob_ids(visible)], |
225 | | Typed,_Type,true,Error), |
226 | | (Error=none -> true ; add_error(read_trace_file,'Error occured while parsing substitution: ',Error),fail), |
227 | | %translate:print_subst(Typed),nl, |
228 | | translate_substition_to_trace(Typed,T2), %print(t2(T2)),nl, |
229 | | Trace=['$initialise_machine'|T2]. |
230 | | read_trace_file('JSON',File,MachineName,Trace) :- !, |
231 | | read_trace_file(json,File,MachineName,Trace). |
232 | | read_trace_file(json,File,MachineName,Trace) :- |
233 | | MachineName = 'dummy(uses)', % name not stored in JSON files |
234 | | json_parse_file(File,Term,[rest(_),strings_as_atoms(false)]), |
235 | | !, |
236 | | (translate_json_term(Term,Trace) -> true |
237 | | ; add_error(trace_checking_fails,'Could not translate JSON transitionList: ',Term), |
238 | | %trace, translate_json_term(Term,Trace), |
239 | | Trace = []). |
240 | | read_trace_file(Style,_,_,_) :- Style \= json, Style \= prolog, !, |
241 | | add_error(trace_checking_fails,'Illegal trace file format (must be json, prolog or B): ',Style),fail. |
242 | | read_trace_file(_,File,_,_) :- |
243 | | add_error(trace_checking_fails,'Could not read trace file: ',File),fail. |
244 | | |
245 | | my_see(File) :- |
246 | | catch(see(File), |
247 | | error(existence_error(_,_),_), |
248 | | add_error_fail(my_see,'File does not exist: ',File)). |
249 | | |
250 | | % ------------------------ |
251 | | |
252 | | % translate a B substitution to a trace to be replayed: |
253 | | translate_substition_to_trace(b(sequence(T),subst,_),Trace) :- !, maplist(translate_b2p,T,Trace). |
254 | | translate_substition_to_trace(Subst,[T]) :- translate_b2p(Subst,T). |
255 | | |
256 | | % translate a single B substitution to one Prolog trace replay term |
257 | | translate_b2p(b(S,_,I),Res) :- translate_b2p(S,I,Res). |
258 | | translate_b2p(operation_call(Operation,OpCallResults,OpCallParas),_,Res) :- |
259 | | OpCallResults = [], % TODO: treat return values |
260 | | !, |
261 | | maplist(translate_para,OpCallParas,PrologParas), |
262 | | def_get_texpr_id(Operation,op(OpName)), |
263 | | Res =.. [OpName|PrologParas]. |
264 | | translate_b2p(A,I,_) :- |
265 | | add_error(trace_replay,'Uncovered substitution in trace file: ',b(A,subst,I),I),fail. |
266 | | |
267 | | translate_para(TExpr,Value) :- % TODO: maybe allow constants? variables ??? local variables in trace file?? |
268 | | b_interpreter:b_compute_expression_nowf(TExpr,[],[],Value,'none',0). |
269 | | |
270 | | % ------------------------ |
271 | | |
272 | | % parse Prolog trace file |
273 | | parse_trace_file(MName,Trace) :- |
274 | | safe_read(Term),!, |
275 | | (Term = end_of_file -> (Trace = []) |
276 | | ; (Term = machine(MName) |
277 | | -> Trace = T |
278 | | ; Trace = [Term|T] |
279 | | ), |
280 | | parse_trace_file(MName,T) |
281 | | ). |
282 | | |
283 | | safe_read(T) :- |
284 | | catch(read(T), E, ( |
285 | | add_error(safe_read,'Exception while reading input:',[E]), |
286 | | T=end_of_file |
287 | | )). |
288 | | |
289 | | %------------------------- |
290 | | |
291 | | translate_json_term(json(ObjList),Trace) :- |
292 | | member('='(transitionList,array(List)),ObjList), |
293 | | !, |
294 | | % TODO: why is this not a call_cleanup? |
295 | | temporary_set_preference(repl_cache_parsing,true,CHNG), |
296 | | eval_strings:turn_normalising_off, |
297 | | maplist(translate_json_operation,List,Trace), |
298 | | eval_strings:turn_normalising_on, |
299 | | reset_temporary_preference(repl_cache_parsing,CHNG). |
300 | | |
301 | | % no transitionList => just use empty list |
302 | | translate_json_term(json(_),[]) :- !. |
303 | | |
304 | | translate_json_operation(json(OperationObj), Operation) :- % new style |
305 | | member('='(name,string(OpNameC)), OperationObj), % name is required! |
306 | | !, |
307 | | %print(json(OperationObj)),nl, |
308 | | get_parameters(OperationObj,Paras), |
309 | | atom_codes(OpName,OpNameC), debug_println(9,json_translate_operation(OpName)), |
310 | | (bmachine:b_get_machine_operation_parameter_names(OpName,OpParameterNames) -> true |
311 | | ; add_error(translate_json_operation,'Unknown operation: ',OpName),fail), |
312 | | maplist(translate_json_para,Paras,Bindings), |
313 | | order_paras(OpParameterNames,OpName,Bindings,BValues), % put the parameters into the order expected |
314 | | Op =.. [OpName|BValues], |
315 | | (bmachine:b_get_machine_operation(OpName,OpResults,_P,_Body,_OType,_OpPos), |
316 | | OpResults \= [] % we have return values |
317 | | -> Operation = '-->'(Op,BResValues), |
318 | | (member('='(results,json(ResParas)),OperationObj) % we could provide this as an option: check results or not |
319 | | -> maplist(translate_json_para,ResParas,Bindings2), |
320 | | def_get_texpr_ids(OpResults,OpResultNames), |
321 | | order_paras(OpResultNames,OpName,Bindings2,BResValues) |
322 | | ; true) |
323 | | ; Operation = Op). %, print(translated(Op)),nl. |
324 | | |
325 | | get_parameters(OperationObj,Paras) :- member('='(params,json(Paras)),OperationObj),!. |
326 | | get_parameters(_,[]) :- !. % e.g., for initialise machine |
327 | | |
328 | | order_paras([],OpName,Rest,[]) :- (Rest=[] -> true ; format('*** Unknown parameters for ~w: ~w~n',[OpName,Rest])). |
329 | | order_paras([ID|T],OpName,Env,[Val|TVal]) :- |
330 | | (select(bind(ID,Val),Env,Env2) -> order_paras(T,OpName,Env2,TVal) |
331 | | ; %add_error(translate_json_operation,'Parameter not specified: ',ID:Env), % keep Val a variable |
332 | | format('*** Parameter not specified for ~w: ~w~n',[OpName,ID]), |
333 | | order_paras(T,OpName,Env,TVal) |
334 | | ). |
335 | | |
336 | | % TO DO: using eval_strings is very ugly, use a better API predicate |
337 | | translate_json_para('='(Name,string(C)),bind(Name,Value)) :- !, |
338 | | eval_strings:eval_expression_codes(C,_Res,_EnumWarning,_LocalState,_Typed,_TypeInfo,[silent_no_string_result]), |
339 | | eval_strings:last_expression_value(Value). |
340 | | translate_json_para(Para,_) :- add_error(translate_json_para,'Unknown JSON para:',Para),fail. |
341 | | |
342 | | is_a_reset_operation(start_cspm_MAIN). |
343 | | is_a_reset_operation(start_csp_MAIN). |
344 | | is_a_reset_operation(Op) :- functor(Op,'$setup_constants',_). |
345 | | is_a_reset_operation(Op) :- functor(Op,Functor,_), |
346 | | unify_functor(Functor,'$initialise_machine',root), |
347 | | b_or_z_mode, \+ b_machine_has_constants_or_properties. |
348 | | |
349 | | :- use_module(bmachine, [b_machine_has_constants_or_properties/0]). |
350 | | perform_initialisation :- b_or_z_mode, b_machine_has_constants_or_properties,!, |
351 | | perform_sequence_of_operations(['$setup_constants','$initialise_machine']). |
352 | | perform_initialisation :- perform_sequence_of_operations(['$initialise_machine']). |
353 | | |
354 | | :- dynamic max_nr_replayed/1. |
355 | | update_max_nr_replayed(Ident) :- |
356 | | (max_nr_replayed(Nr),Nr >= Ident -> true |
357 | | ; retract(max_nr_replayed(_)), assertz(max_nr_replayed(Ident))). |
358 | | |
359 | | |
360 | | perform_sequence_of_operations(Trace) :- |
361 | | retractall(max_nr_replayed(_)), |
362 | | assertz(max_nr_replayed(0)), |
363 | ? | perform_sequence_of_operations2(Trace,0). |
364 | | |
365 | | perform_sequence_of_operations2([],Ident) :- |
366 | | (silent_mode(on) -> true ; ident(Ident),print('SUCCESS'),nl). |
367 | | perform_sequence_of_operations2([Op|T],Ident) :- |
368 | | get_error_context(Context), |
369 | | current_state_id(ID),get_operation_name(Op,FOP), |
370 | | set_error_context(operation(FOP,ID)), |
371 | ? | perform_one_operation_in_sequence(Op,Ident), |
372 | | update_max_nr_replayed(Ident), |
373 | | restore_error_context(Context), |
374 | | Ident1 is Ident+1, |
375 | | (get_preference(deterministic_trace_replay,true) -> ! ; true), |
376 | ? | perform_sequence_of_operations2(T,Ident1). |
377 | | |
378 | | |
379 | | perform_one_operation_in_sequence('$non_det_modified_vars'(ActionAsTerm,NonDetVars),Ident) :- !, |
380 | | current_expression(_CurID,State), |
381 | | current_options(Options), |
382 | | member( (_Id,Action,ActionOpAsTerm,NewID), Options), |
383 | | unify_action_as_term(ActionAsTerm,ActionOpAsTerm,State), |
384 | | %ident(Ident), format('checking non_det_modified_vars for ~w in ~w~n',[ActionAsTerm,NewID]),nl, |
385 | | check_non_det_vars(NewID,NonDetVars), |
386 | | !, |
387 | | perform_action_tclk(Action,ActionOpAsTerm,NewID,Ident). |
388 | | perform_one_operation_in_sequence('$non_det_modified_vars'(Op,_),Ident) :- !, |
389 | | ident(Ident), format('ignoring non_det_modified_vars for ~w~n',[Op]), % TO DO: use constraint-based finding of successor |
390 | | perform_one_operation_in_sequence(Op,Ident). |
391 | | perform_one_operation_in_sequence('$check_value'(ID,VAL),Ident) :- !, |
392 | ? | ident(Ident), format('checking value of ~w ',[ID]), |
393 | | state_space:current_expression(_,State), |
394 | | expand_const_and_vars_to_full_store(State,EState), |
395 | | lookup_value_for_existing_id(ID,EState,StoredVal), |
396 | | translate:print_bvalue(StoredVal), |
397 | | (unify(StoredVal,VAL) -> print_green(' ok'),nl |
398 | | ; print_red(' failed'),nl, %print(StoredVal),nl, print(VAL),nl, |
399 | | fail). |
400 | | perform_one_operation_in_sequence(Op,Ident) :- |
401 | | (silent_mode(on) -> true |
402 | | ; ident(Ident),print('<- '),print(Ident), print(': '), my_print_event(Op,OpStr), |
403 | | print(' :: '), |
404 | | current_state_id(CurID), print(CurID),nl |
405 | | ), |
406 | ? | (is_a_reset_operation(Op) |
407 | | -> tcltk_reset, %tcltk_goto_state(reset,root), % reset animation history |
408 | | tcltk_get_options(_) |
409 | | ; true), |
410 | | convert_action(Op,COp), |
411 | ? | if(perform_single_operation(COp,Ident),true, |
412 | | (silent_mode(off), |
413 | | ident(Ident), print_red(' **** FAIL ****'),nl, |
414 | | fail)), |
415 | | (get_preference(deterministic_trace_replay,true) -> ! ; true), |
416 | | (silent_mode(on) -> true |
417 | | ; ident(Ident), print(' | '), print(Ident), print(': '), print(OpStr), |
418 | | %functor(Op,OpName,_), print(OpName), |
419 | | %((OpName = '-->', arg(1,Op,A1), functor(A1,RealOpName,_)) -> print(RealOpName) ; true), |
420 | | print_green(' success -->'), |
421 | | current_state_id(NewCurID), |
422 | | statistics(walltime,[Tot,Delta]), |
423 | | format('~w [~w (Delta ~w) ms]~n',[NewCurID,Tot,Delta]) |
424 | | ). |
425 | | |
426 | | my_print_event(Op,OpStrTA) :- |
427 | | temporary_set_preference(expand_avl_upto,4,CHNG), |
428 | | translate_event(Op,OpStr), |
429 | | truncate_atom(OpStr,100,OpStrTA), |
430 | | reset_temporary_preference(expand_avl_upto,CHNG), |
431 | | write(OpStrTA). |
432 | | |
433 | | /* convert global constants such as b with S={a,b,c} into fd(2,'S') */ |
434 | | convert_action(V,R) :- var(V),!,R=V. |
435 | | convert_action(io(V,Ch),R) :- !, strip_dots(V,SV),R=io(SV,Ch,_SRCSPAN). |
436 | | convert_action(io(V,Ch,_),R) :- !, strip_dots(V,SV),R=io(SV,Ch,_SRCSPAN). |
437 | | convert_action(tick(_SRCSPAN),R) :- !, R = tick(_). |
438 | | convert_action(X,Res) :- nonvar(X),X=..[F|Args],!, |
439 | | l_convert_term(Args,CArgs),Res=..[F|CArgs]. |
440 | | convert_action(X,X). |
441 | | |
442 | | convert_term(V,R) :- var(V),!,R=V. |
443 | | convert_term(closure(A,B,C),R) :- !, R=closure(A,B,C). % we may mess with identifiers; see test 1575 |
444 | | convert_term(term(bool(0)),R) :- !, R=pred_false /* bool_false */. |
445 | | convert_term(term(bool(1)),R) :- !, R=pred_true /* bool_true */. |
446 | | convert_term(bool_true,pred_true /* bool_true */) :- !. |
447 | | convert_term(bool_false,pred_false /* bool_false */) :- !. |
448 | | convert_term(string(S),R) :- !, R=string(S). |
449 | | convert_term(X,Representation) :- atomic(X), lookup_global_constant(X,Representation),!. |
450 | | convert_term(X,Res) :- nonvar(X),X=..[F|Args],!, |
451 | | l_convert_term(Args,CArgs),Res=..[F|CArgs]. |
452 | | convert_term(X,X). |
453 | | |
454 | | l_convert_term([],[]). |
455 | | l_convert_term([H|T],[CH|CT]) :- convert_term(H,CH), l_convert_term(T,CT). |
456 | | |
457 | | /* newer version of ProB no longer has dot() constructor */ |
458 | | strip_dots([],[]). |
459 | | strip_dots([H|T],[X|ST]) :- (H=dot(X) -> true ; X=H), strip_dots(T,ST). |
460 | | strip_dots(tail_in(X),[in(XR)]) :- |
461 | | (X=dotTuple(R) -> XR=tuple(R) ; XR = X). /* we also no longer use tail_in */ |
462 | | |
463 | | get_state(concrete_constants(X),R) :- !, R=X. |
464 | | get_state(const_and_vars(_,X),R) :- !, R=X. |
465 | | get_state(X,X). |
466 | | |
467 | | % check whether state NewID contains all the bindings in NonDetVars |
468 | | check_non_det_vars(NewID,NonDetVars) :- |
469 | | visited_expression(NewID,State), |
470 | | get_state(State,VarState), |
471 | | maplist(check_non_det_bind(VarState),NonDetVars). |
472 | | |
473 | | check_non_det_bind(State,bind(Var,Val)) :- member(bind(Var,StoredVal),State), unify(StoredVal,Val). |
474 | | |
475 | | :- use_module(state_space,[current_state_id/1, current_expression/2, visited_expression_id/1]). |
476 | | perform_single_operation('$jump'(TO,FROM),Ident) :- !, |
477 | | current_state_id(ID), |
478 | | print_red('Warning: trace file contains JUMP!'),nl, |
479 | | (ID=FROM -> true ; ident(Ident),format('Cannot perform jump from ~w (to ~w)~n',[FROM,TO])), |
480 | | (visited_expression_id(TO) -> tcltk_interface:tcltk_goto_state(jump,TO) |
481 | | ; add_error(trace_checking_fails,'State ID does not exist for jump:',TO),fail |
482 | | ). |
483 | | perform_single_operation(ActionAsTerm,Ident) :- |
484 | | % tools_printing:print_term_summary(perform_single_op(ActionAsTerm)), |
485 | | current_expression(_CurID,State), |
486 | | current_options(Options), |
487 | ? | ( if( find_action_in_options(ActionAsTerm,Options,State, Action,ActionOpAsTerm,NewID), |
488 | ? | perform_action_tclk(Action,ActionOpAsTerm,NewID,Ident), |
489 | ? | if(perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,State), |
490 | ? | perform_action_tclk(Action,_AlternateActionOpAsTerm,NewID,Ident), |
491 | | if(perform_custom_operation_retry(ActionAsTerm,_NewID),true, |
492 | | (replace_result_by_variable(ActionAsTerm,A2), |
493 | ? | find_action_in_options(A2,Options,State, Action,_,NewID), |
494 | | (silent_mode(on) -> true ; format_with_colour_nl(user_output,[red],'Result of operation call in trace does not match, e.g., ~w leading to state ~w',[Action,NewID])), |
495 | | fail |
496 | | ) |
497 | | ) |
498 | | ) |
499 | | |
500 | | ) |
501 | | ; |
502 | | single_operation_skip(ActionAsTerm,Ident) |
503 | | ), |
504 | | (get_preference(deterministic_trace_replay,true) -> ! ; true). |
505 | | perform_single_operation(ActionAsTerm,Ident) :- |
506 | | current_options(Options), |
507 | | member( (_Id,PActionS,'*permute*',NewID), Options), /* permute action from symmetry reduction */ |
508 | | perform_action_tclk(PActionS,'*permute*',NewID,Ident), !, |
509 | | (silent_mode(on) -> true |
510 | | ; ident(Ident), print(' | ** PERMUTING **'),nl), |
511 | | perform_single_operation(ActionAsTerm,Ident). |
512 | | perform_single_operation(ActionAsTerm,Ident) :- |
513 | | %%user:current_expression(CurID,State), |
514 | | \+ functor(ActionAsTerm,tau,1), |
515 | | current_options(Options), %print(options(Options)),nl, |
516 | ? | member( (_Id,AX,tau(X),NewID), Options), |
517 | | (silent_mode(on) -> true |
518 | | ; ident(Ident), print(' | ** SKIPPING ADDITIONAL TAU in SPEC. **'),nl), |
519 | ? | perform_action_tclk(AX,tau(X),NewID,Ident), |
520 | ? | perform_single_operation(ActionAsTerm,Ident). |
521 | | %perform_single_operation(ActionAsTerm,Ident) :- |
522 | | % ident(Ident),print(unsuccessful(ActionAsTerm)),nl,fail. |
523 | | |
524 | | |
525 | | perform_action_tclk(Action,ActionOpAsTerm,NewID,_Ident) :- |
526 | ? | my_perform_action_as_string(Action,ActionOpAsTerm,NewID), |
527 | | tcltk_get_options(_). |
528 | | perform_action_tclk(_Action,_ActionOpAsTerm,_NewID,Ident) :- % undo action |
529 | | current_state_id(FromID), |
530 | | tcltk_interface:tcltk_backtrack, |
531 | | tcltk_get_options(_), |
532 | | current_state_id(ToID), |
533 | | silent_mode(off), |
534 | | ident(Ident), |
535 | | print(backtrack_from_to(FromID,ToID)),nl, |
536 | | fail. |
537 | | |
538 | | % a more flexible version: allow string representations of ProB to evolve compared to when test suites where stored |
539 | | my_perform_action_as_string(ActionStr,ActionOpAsTerm,NewID) :- |
540 | ? | tcltk_interface:tcltk_perform_action_string(ActionStr,ActionOpAsTerm,NewID). |
541 | | |
542 | | % succeeds if we have an operation with results and then replaces results by fresh variable |
543 | | replace_result_by_variable('-->'(Op,_),'-->'(Op,_)). |
544 | | |
545 | | find_action_in_options(ActionAsTerm,Options,State, Action,ActionOpAsTerm,NewID) :- |
546 | ? | member( (_Id,Action,ActionOpAsTerm,NewID), Options), |
547 | | unify_action_as_term(ActionAsTerm,ActionOpAsTerm,State). |
548 | | |
549 | | :- use_module(library(avl)). |
550 | | unify_action_as_term(A,A,_) :- !. |
551 | | unify_action_as_term('-->'(Op,Results),'-->'(Op2,Results2),State) :- !, |
552 | | unify_action_as_term(Op,Op2,State), |
553 | | l_unify(Results,Results2). |
554 | | unify_action_as_term(A,B,State) :- functor(A,F,N), functor(B,F2,N2), |
555 | | unify_functor(F,F2,State), |
556 | | (N=N2 -> true |
557 | | ; formatsilent('*** SAME EVENT WITH VARYING ARITY: ~w : ~w vs ~w arguments ***~n',[F,N,N2]), |
558 | | % Probably due to show_eventb_any_arguments differently set ? or initalisation old format |
559 | | fail), |
560 | | A=..[F|AA], B=..[F2|BB], |
561 | | l_unify(AA,BB). |
562 | | l_unify([],[]). |
563 | | l_unify([H|T],[I|S]) :- unify(H,I), l_unify(T,S). |
564 | | |
565 | | |
566 | | unify_functor('initialise_machine','$initialise_machine',_) :- !. % old-style format |
567 | | unify_functor('setup_constants','$setup_constants',root) :- !. % old-style format |
568 | | unify_functor(X,X,_). |
569 | | |
570 | | %:- use_module(custom_explicit_sets,[equal_explicit_sets/4]). |
571 | | :- use_module(debug). |
572 | | unify(A,A) :- !. |
573 | | unify(A,avl_set(B)) :- %print(exp(A,B)),nl, |
574 | | expand_explicit_set(A,AA), |
575 | | %nl,translate:print_bvalue(AA),nl, translate:print_bvalue(avl_set(B)),nl, % print(chck(A,AA,B)),nl, |
576 | | AA = avl_set(B),!. |
577 | | %unify(A,B) :- print(unify(A,B)),nl,fail. |
578 | | unify(C1,C2) :- is_a_set(C1),(C2=closure(_P,_T,_B) ; C2=global_set(_)), |
579 | | %print(unify_closure(C1,C2)),nl, |
580 | | (C1=[_|_] -> custom_explicit_sets:convert_to_avl(C1,C11) ; C11=C1), % TO DO: replace by proper expansion predicate |
581 | | (unify_explicit_sets(C11,C2) |
582 | | -> true |
583 | | ; print(ko_unify_closure),nl, translate:print_bvalue(C11),nl, translate:print_bvalue(C2),nl, |
584 | | %terms:term_hash((C1,C2),H), print(hash(H)),nl, (H=140674321 -> trace, unify_explicit_sets(C11,C2)), |
585 | | fail),!. |
586 | | %avl_domain(B,R), print(chck(A,B,R)),nl,l_unify(A,R). |
587 | | unify(C1,C2) :- %tools_printing:print_term_summary(fail(C1,C2)),nl, |
588 | | debug_println(9,unify_failed(C1,C2)),fail. |
589 | | |
590 | | is_a_set(closure(_,_,_)). |
591 | | is_a_set([]). |
592 | | is_a_set([_|_]). |
593 | | is_a_set(global_set(_)). |
594 | | is_a_set(avl_set(_)). |
595 | | |
596 | | expand_explicit_set([H|T],AA) :- !, custom_explicit_sets:convert_to_avl([H|T],AA). |
597 | | expand_explicit_set(A,AA) :- |
598 | | on_enumeration_warning(custom_explicit_sets:try_expand_and_convert_to_avl_if_smaller_than(A,AA,200), fail). |
599 | | unify_explicit_sets(C1,C2) :- |
600 | | ALLOW=no_expansion, %(C1 = avl_set(_) -> ALLOW=allow_expansion ; ALLOW=no_expansion), |
601 | | on_enumeration_warning(custom_explicit_sets:equal_explicit_sets4(C1,C2,ALLOW,no_wf_available), fail). |
602 | | |
603 | | |
604 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,root) :- |
605 | | functor(ActionAsTerm,'setup_constants',_), !, % rename to new format |
606 | | nl,print('DEPRECATED TRACE FILE'),nl,nl,nl, |
607 | | ActionAsTerm =.. [_|Args], ActionAsTerm2 =..['$setup_constants'|Args], |
608 | ? | perform_single_operation_retry(Options,ActionAsTerm2,Action,NewID). |
609 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,State) :- |
610 | | (State=root ; State=concrete_constants(_)), |
611 | | functor(ActionAsTerm,'initialise_machine',_), !, % rename to new format |
612 | | nl,print('DEPRECATED TRACE FILE'),nl,nl,nl, |
613 | | ActionAsTerm =.. [_|Args], ActionAsTerm2 =..['$initialise_machine'|Args], |
614 | ? | perform_single_operation_retry(Options,ActionAsTerm2,Action,NewID). |
615 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,_State) :- |
616 | ? | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID). |
617 | | |
618 | | |
619 | | % check that parameters provided for setup_constants in trace file can be found in State |
620 | | %check_initialised_args([],_). |
621 | | %check_initialised_args([V|T],State) :- |
622 | | % select(bind(_,V2),State,Rest), |
623 | | % unify(V,V2), |
624 | | % %print('SELECTED: '),translate:print_bvalue(V2),nl, |
625 | | % !, |
626 | | % check_initialised_args(T,Rest). |
627 | | %check_initialised_args([V|T],State) :- |
628 | | % print('MISMATCH'),nl, %print(mismatch(V,C)),nl, |
629 | | % print('COULD NOT FIND: '), translate:print_bvalue(V),nl, |
630 | | % tools_printing:print_term_summary(V),nl, |
631 | | % %print(V),nl, print(State),nl, |
632 | | % V=closure(_,_,_), memberchk(bind(_,closure(_,_,_)),State), |
633 | | % check_initialised_args(T,State). |
634 | | |
635 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :- |
636 | | functor(ActionAsTerm,'$setup_constants',_), !, |
637 | | (get_prob_application_type(tcltk) -> OTHER = ['$partial_setup_constants'] ; OTHER = []), |
638 | ? | perform_alternative_op_with_same_functor(Options, ['$setup_constants' | OTHER], |
639 | | 'set up constants', 'initialisation of constants', |
640 | | ActionAsTerm, Action, NewID), |
641 | | %visited_expression(NewID,concrete_constants(C)), ActionAsTerm =.. [_|Args], |
642 | | % check that state NewID corresponds to parameters provided for setup_constants in trace file |
643 | | %print(check_args),nl, check_initialised_args(Args,C), print('argsok'),nl. % TO DO: try and enable this for all tests |
644 | | true. |
645 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :- |
646 | | functor(ActionAsTerm,'$initialise_machine',_),!, |
647 | ? | perform_alternative_op_with_same_functor(Options, ['$initialise_machine'], |
648 | | 'initialise', 'initialisation', |
649 | | ActionAsTerm, Action, NewID), |
650 | | true. %visited_expression(NewID,S), (S=const_and_vars(_,VS) -> true ; VS=S), ActionAsTerm =.. [_|Args], |
651 | | %check_initialised_args(Args,VS), print('initargsok'),nl. |
652 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :- |
653 | | functor(ActionAsTerm,tau,_), arg(1,ActionAsTerm,Arg), nonvar(Arg),!, |
654 | ? | perform_alternative_op_with_same_functor(Options, [tau], |
655 | | tau, tau, |
656 | | ActionAsTerm, Action, NewID). |
657 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :- |
658 | | functor(ActionAsTerm,F,0), preference(show_eventb_any_arguments,true), |
659 | | /* then allow also the same operation name but with more arguments */ |
660 | | member( (_Id,Action,ActionAsTerm2,NewID), Options), |
661 | | functor(ActionAsTerm2,F,FArity), FArity>0, |
662 | | formatsilent('% Allowing extra Event-B style ANY arguments.~n',[]). |
663 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :- |
664 | | functor(ActionAsTerm,F,N),N>0, preference(show_eventb_any_arguments,false), |
665 | | /* then allow also the same operation name but with more arguments */ |
666 | ? | member( (_Id,Action,F,NewID), Options), |
667 | | formatsilent('% Allowing operation without Event-B style ANY arguments.~n',[]). |
668 | | %perform_single_operation_retry(Options,_ActionsAsTerm,_Action,_NewID) :- |
669 | | % print_message('No more options: '), print(Options),nl,fail. |
670 | | |
671 | | |
672 | | perform_custom_operation_retry(OpName,NewID) :- |
673 | | (OpName = '$initialise_machine' ; OpName = '$setup_constants'), |
674 | | !, |
675 | | current_state_id(CurID), |
676 | | (max_reached_for_node(CurID) ; not_all_transitions_added(CurID)), |
677 | | preferences:get_preference(maxNrOfInitialisations,0), |
678 | | tcltk_add_user_executed_operation_typed(OpName,_,b(truth,pred,[]),NewID), |
679 | | (get_preference(deterministic_trace_replay,true) -> ! ; true), |
680 | | print_green(init_found(NewID)),nl. |
681 | | perform_custom_operation_retry(ActionAsTerm,NewID) :- |
682 | | (ActionAsTerm = '-->'(_,_) % for operations with return types we cannot provide a predicate to solve yet |
683 | | -> preferences:get_preference(maxNrOfEnablingsPerOperation,0) |
684 | | ; true), |
685 | | current_state_id(CurID), |
686 | | get_operation_name(ActionAsTerm,OpName), |
687 | | (max_reached_for_node(CurID) ; time_out_for_node(CurID,OpName,_) ; not_all_transitions_added(CurID)), |
688 | | debug_println(9,try_custom(CurID,ActionAsTerm)), % Execute operation by predicate |
689 | | % (state_space:transition(CurID,AA,BB,CC),format('Successor of ~w: ~w --~w--> ~w~n',[CurID,AA,BB,CC]),fail ; true), |
690 | | get_operation_return_values_and_arguments(ActionAsTerm,ExpectedResults,OpArgs), |
691 | | % TO DO: optionally check return values |
692 | | (OpArgs = [] -> Pred = b(truth,pred,[]) |
693 | | ; \+ b_is_operation_name(OpName) |
694 | | -> add_error(trace_checking_fails,'Operation does not exist in loaded specification:',OpName),fail |
695 | ? | ; b_get_machine_operation_typed_parameters(OpName,TArgParas), |
696 | | l_generate_predicate(OpArgs,TArgParas,OpName,Conjuncts), |
697 | | conjunct_predicates(Conjuncts,Pred) |
698 | | ), |
699 | | !, |
700 | | %print('PRED: '),translate:print_bexpr(Pred),nl, |
701 | | start_ms_timer(Timer), |
702 | | profile_single_call(OpName,CurID, |
703 | | tcltk_interface:tcltk_add_user_executed_operation_typed(OpName,OpTerm,Pred,NewID) % The Pred can only talk about parameters and the state before; thus this only works for setup_constants and initialise_machine |
704 | | ), |
705 | | (get_preference(deterministic_trace_replay,true) -> ! ; true), % by preventing backtracking we can reduce memory consumption |
706 | | print_green(successor_found(NewID, OpName)),nl, |
707 | | get_operation_return_values_and_arguments(OpTerm,ActualResults,_), |
708 | | (l_unify(ExpectedResults,ActualResults) -> true |
709 | | ; ajoin(['Result values for ',OpName,' do not match for transition from ',CurID,' to ',NewID,':'],Msg), |
710 | | translate_bvalue(ExpectedResults,ER), |
711 | | translate_bvalue(ActualResults,AR), |
712 | | add_warning(b_trace_checking,Msg,[expected(ER),actual(AR)]) |
713 | | ), |
714 | | (debug_mode(on) -> stop_ms_timer_with_msg(Timer,'Custom: ') ; true), |
715 | | garbage_collect, % important to keep memory consumption down for long traces e.g. for Innotrans VBF traces |
716 | | (debug_mode(on) -> print_memory_used_wo_gc,nl ; true), |
717 | | tcltk_get_options(_). |
718 | | |
719 | | l_generate_predicate([],[],_,[]) :- !. |
720 | | l_generate_predicate([],_,Op,[]) :- !, add_warning(b_trace_checking,'Trace file contains too few parameters for: ',Op). |
721 | | l_generate_predicate(_,[],Op,[]) :- !, add_warning(b_trace_checking,'Trace file contains too many parameters for: ',Op). |
722 | | l_generate_predicate([ArgVal|TArg],[TypedPara|TPar],OpName,[Pred|TPred]) :- |
723 | | generate_predicate(ArgVal,TypedPara,Pred), |
724 | | l_generate_predicate(TArg,TPar,OpName,TPred). |
725 | | generate_predicate(ArgVal,TypedPara,b(equal(TypedPara,TVal),pred,[])) :- |
726 | | get_texpr_type(TypedPara,Type), |
727 | | TVal = b(value(ArgVal),Type,[]). |
728 | | |
729 | | perform_alternative_op_with_same_functor(Options,Functors,ActionMsg,AltMsg,ActionAsTerm,Action,NewID) :- |
730 | | \+ member( (_,_,ActionAsTerm,_), Options), |
731 | | (silent_mode(on) -> true |
732 | | ; ajoin(['Could not ', ActionMsg, ' with parameters from trace file.'], Msg1), |
733 | | ajoin(['Will attempt any possible ', AltMsg, '.'], Msg2), |
734 | | print_message(Msg1), print_message(Msg2) |
735 | | ), |
736 | | %print(ActionAsTerm),nl, print(Options),nl,nl, |
737 | ? | member( (_,ActionStr,MachineActionAsTerm,NewID), Options), |
738 | | functor(MachineActionAsTerm,Functor,_), |
739 | | member(Functor,Functors), |
740 | | (Action=ActionStr -> true ; print(cannot_match(Action,ActionStr)),nl,fail). |
741 | | |
742 | | single_operation_skip(tau(_),Ident) :- |
743 | | (silent_mode(on) -> true |
744 | | ; ident(Ident), print(' | *** TRYING TO SKIP TAU IN TRACE FILE'),nl). |
745 | | |
746 | | |
747 | | |
748 | | ident(0). |
749 | | ident(N) :- N > 40, !, N1 is N mod 40, ident(N1). |
750 | ? | ident(N) :- N>0, print('- '), N1 is N-1, ident(N1). |
751 | | |
752 | | |
753 | | /* ------------------------------------------------------------------ */ |
754 | | |
755 | | :- use_module(state_space,[get_action_trace/1]). |
756 | | print_trace_as_fdr_check :- silent_mode(on),!. |
757 | | print_trace_as_fdr_check :- |
758 | | print('-- Trace Check Generated by ProB:'),nl, |
759 | | get_action_trace(T), |
760 | | reverse(T,RT), |
761 | | print('PROB_TEST_TRACE = '),print_fdr(RT), |
762 | | nl, |
763 | | print('assert MAIN [T= PROB_TEST_TRACE'),nl. |
764 | | |
765 | | print_fdr([]) :- print('STOP'),nl. |
766 | | print_fdr([jump|T]) :- print_fdr(T). |
767 | | print_fdr([action(Str,Term)|T]) :- |
768 | | (Term = i(_) |
769 | | -> (nl,print(' ( STOP /\\ ')) |
770 | | ; (Term = tick(_) |
771 | | -> print('SKIP ; ') |
772 | | ; ((Term = tau(_) ; Term = 'start_cspm_MAIN') |
773 | | -> true |
774 | | ; (print(Str), print(' -> ')) |
775 | | ) |
776 | | )), |
777 | | print_fdr(T), |
778 | | (Term = i(_) |
779 | | -> print(' )') |
780 | | ; true |
781 | | ). |
782 | | |
783 | | % ----------------------- |
784 | | |
785 | | tcltk_save_history_as_trace_file(Style,File) :- |
786 | | tcltk_save_history_as_trace_file(Style,[],File). |
787 | | |
788 | | tcltk_save_history_as_trace_file(Style,Options,File) :- |
789 | | formatsilent('% Saving history (~w format) to: ~w~n',[Style,File]), |
790 | | open(File,write,Stream,[encoding(utf8)]), |
791 | | currently_opened_specification_name(OurName), |
792 | | (Style=prolog -> format(Stream,'machine(\'~w\').~n',[OurName]) ; true), |
793 | | call_cleanup(print_trace_for_replay(Style,Options,Stream), |
794 | | (close(Stream),print_message(done))). |
795 | | |
796 | | :- use_module(state_space,[transition/4, op_trace_ids/1]). % transition(CurID,Term,TransId,DestID) |
797 | | |
798 | | % print the animator's history trace for later replay |
799 | | % prolog style is currently used by ProB Tcl/Tk |
800 | | % json style is used by ProB2 UI |
801 | | print_trace_for_replay(Style,Options,Stream) :- |
802 | | op_trace_ids(OpIds), |
803 | | reverse(OpIds,Trace), |
804 | | print_trace_for_replay(Style,Trace,Options,Stream). |
805 | | |
806 | | print_trace_for_replay(prolog,Trace,_,Stream) :- !, print_transition_list_prolog(Trace,Stream). |
807 | | print_trace_for_replay(json,Trace,Options,Stream) :- !, print_transition_list_json(Trace,Options,Stream). |
808 | | print_trace_for_replay(Style,_,_,_Stream) :- |
809 | | add_internal_error('Style not supported: ',print_trace_for_replay(Style,_,_,_)). |
810 | | |
811 | | print_transition_list_prolog(Trace,Stream) :- |
812 | ? | member(OpId,Trace), |
813 | | transition(PrevId,Op,OpId,SuccId), |
814 | | (atomic(Op), |
815 | | ( b_or_z_mode, |
816 | | transition(PrevId,Op,_,SuccId2), SuccId2 \= SuccId -> true), % another transition with same label Op exists |
817 | | translate:get_non_det_modified_vars_in_target_id(Op,SuccId,NonDetVars) |
818 | | -> print_quoted(Stream,'$non_det_modified_vars'(Op,NonDetVars)) |
819 | | ; print_quoted(Stream, Op) |
820 | | ), |
821 | | format(Stream,'.~n',[]), |
822 | | fail. |
823 | | print_transition_list_prolog(_,_). |
824 | | |
825 | | :- use_module(version, [version_str/1, revision/1]). % , lastchangeddate/1 |
826 | | :- use_module(library(system),[ datime/1, environ/2]). |
827 | | :- use_module(specfile,[currently_opened_file/1, currently_opened_specification_name/1]). |
828 | | :- use_module(tools_strings,[number_codes_min_length/3]). |
829 | | :- use_module(tools_lists,[get_member_option/3]). |
830 | | :- use_module(tools,[get_tail_filename/2]). |
831 | | |
832 | | |
833 | | :- use_module(extrasrc(json_parser),[json_write_stream/3]). |
834 | | % print list in JSON format for ProB2 UI: |
835 | | % this is formatVersion 1 |
836 | | print_transition_list_json(Trace,Options,Stream) :- |
837 | | get_prob_application_type(ApplType), |
838 | | (get_member_option(description,Options,Desc) -> true |
839 | | ; ApplType=probcli -> Desc = 'File created by probcli' |
840 | | ; ApplType=tcltk -> Desc = 'File created by ProB Tcl/Tk' |
841 | | ; Desc = 'File created by ProB' |
842 | | ), |
843 | | temporary_set_preference(expand_avl_upto,-1,CHNG), |
844 | | call_cleanup( |
845 | | print_json_list(Trace,root,TransitionList), % print list of transitions in JSON format |
846 | | reset_temporary_preference(expand_avl_upto,CHNG)), |
847 | | format_current_iso_time(Timestamp), |
848 | | (nonmember(privacy_mode,Options),environ('USER',User) |
849 | | -> ajoin([ApplType,' (',User,')'],Creator) |
850 | | ; Creator = ApplType), |
851 | | version_str(Version), |
852 | | revision(Rev), |
853 | | currently_opened_file(File), |
854 | | (nonmember(privacy_mode,Options) -> StoredFile=File |
855 | | ; get_tail_filename(File,StoredFile) % do not store full path |
856 | | ), |
857 | | currently_opened_specification_name(Model), |
858 | | Json = json([ |
859 | | description=string(Desc), |
860 | | transitionList=array(TransitionList), |
861 | | metadata=json([ |
862 | | fileType=string('Trace'), |
863 | | formatVersion=number(1), |
864 | | savedAt=string(Timestamp), % TODO: rename to createdAt and make optional for testing |
865 | | creator=string(Creator), |
866 | | proBCliVersion=string(Version), |
867 | | proBCliRevision=string(Rev), % not used by Java Kernel |
868 | | modelName=string(Model), |
869 | | modelFile=string(StoredFile) % not used by Java Kernel |
870 | | ]) |
871 | | ]), |
872 | | (json_write_stream(Stream,Json,[pretty(true)]) |
873 | | -> true |
874 | | ; add_error(print_transition_list_json,'Writing json trace failed'), fail). |
875 | | % to do: maybe also save types of variables, constants, operation parameters, ... |
876 | | % and modification time of modelFile, SHA of model, ... |
877 | | |
878 | | % example: "2020-12-23T14:33:00Z", |
879 | | format_current_iso_time(TimestampAtom) :- |
880 | | % TODO: this is incorrect |
881 | | % datime is the time in the current timezone, but does not include that zone |
882 | | % we put Z behind the ISO-8601 datetime to mark it as UTC which is incorrect! |
883 | | datime(datime(Yr,Mon,Day,Hr,Min,Sec)), |
884 | | number_codes_min_length(Yr,4,YrC), |
885 | | number_codes_min_length(Mon,2,MonC), |
886 | | number_codes_min_length(Day,2,DayC), |
887 | | number_codes_min_length(Hr,2,HrC), |
888 | | number_codes_min_length(Min,2,MinC), |
889 | | number_codes_min_length(Sec,2,SecC), |
890 | | format_to_codes('~s-~s-~sT~s:~s:~sZ',[YrC,MonC,DayC,HrC,MinC,SecC],TimestampCodes), |
891 | | atom_codes(TimestampAtom,TimestampCodes). |
892 | | |
893 | | % print a list of transition ids in JSON format |
894 | | print_json_list([],_,[]). |
895 | | print_json_list([H|T],FromID,[JsonH|JsonT]) :- |
896 | | (H=jump(NewID) -> true |
897 | | ; print_json_opid(H,JsonH,FromID,NewID) -> true |
898 | | ; add_error(print_json_list,'Writing operation failed, transition id is: ',H), NewID=FromID |
899 | | ), |
900 | | print_json_list(T,NewID,JsonT). |
901 | | |
902 | | :- use_module(specfile,[get_operation_internal_name/2, |
903 | | get_operation_return_values_and_arguments/3, |
904 | | get_operation_description_for_transition/4, |
905 | | get_possible_language_specific_top_level_event/3, |
906 | | xtl_mode/0]). |
907 | | |
908 | | % print an operation id (transition id) for a JSON Trace |
909 | | print_json_opid(OpId,Json,PrevId,SuccId) :- |
910 | | (transition(PrevId,Op,OpId,SuccId) -> PrevId1=PrevId |
911 | | ; add_warning(print_json_list,'Cannot find operation id from given source id: ',OpId:from(PrevId):to(SuccId)), |
912 | | transition(PrevId1,Op,OpId,SuccId) |
913 | | ), |
914 | | get_operation_internal_name(Op,OpName), % TO DO: currently this is INITIALISATION instead of $initialise_machine |
915 | | (get_possible_language_specific_top_level_event(OpName,ResultNames,ParaNames) -> true |
916 | | ; ResultNames=unknown, ParaNames=unknown), |
917 | | get_operation_return_values_and_arguments(Op,ReturnValues,Paras), |
918 | | % TO DO: extract variables and constants for $initialise_machine, $setup_constants |
919 | | Json = json([name=string(OpName)|T1]), |
920 | | (get_operation_description_for_transition(PrevId,Op,SuccId,Desc) |
921 | | -> T1=[description=string(Desc)|T2] |
922 | | ; T2=T1), |
923 | | (Paras = [] |
924 | | -> T3=T2 % do not print Paras to reduce memory in JSON file |
925 | | ; xtl_mode |
926 | | -> length(Paras,PLen), |
927 | | xtl_param_names(PLen,PNames2), |
928 | | print_json_paras(Paras,PNames2,OpName,JsonParams), |
929 | | T2=[params=JsonParams|T3] |
930 | | ; get_preference(show_eventb_any_arguments,true), |
931 | | \+ same_length(Paras,ParaNames) |
932 | | -> % we cannot easily use the parameters during replay; ANY parameters are currently only added when there are no other parameters |
933 | | add_warning(json_export,'Parameter mismatch: ',OpName:ParaNames,Paras), |
934 | | T3=T2 |
935 | | ; print_json_paras(Paras,ParaNames,OpName,JsonParams), |
936 | | T2=[params=JsonParams|T3] |
937 | | ), |
938 | | ((xtl_mode ; ReturnValues = []) |
939 | | -> T4=T3 % do not print results to reduce memory in JSON file |
940 | | ; print_json_paras(ReturnValues,ResultNames,OpName,JsonResults), |
941 | | T3=[results=JsonResults|T4] |
942 | | ), |
943 | | get_change_list(PrevId1,SuccId,ChangedVarNames,ChangedValues), |
944 | | (xtl_mode % special case for XTL: "xtl_state": "destStateTerm" |
945 | | -> visited_expression(SuccId,SuccState), |
946 | | print_json_paras([SuccState],[xtl_state],OpName,JsonDestState), |
947 | | T4=[destState=JsonDestState|T5] |
948 | | ; (ChangedVarNames = [] |
949 | | -> T5=T4 |
950 | | ; print_json_paras(ChangedValues,ChangedVarNames,OpName,JsonDestState), |
951 | | T4=[destState=JsonDestState|T5] |
952 | | ) |
953 | | ), |
954 | | get_unchanged_list(PrevId1,SuccId,UnChangedVarNames), |
955 | | (UnChangedVarNames = [] |
956 | | -> T6=T5 |
957 | | ; print_json_names(UnChangedVarNames,JsonDestStateNotChanged), |
958 | | T5=[destStateNotChanged=JsonDestStateNotChanged|T6] |
959 | | ), |
960 | | T6=[]. |
961 | | |
962 | | :- use_module(library(between),[between/3]). |
963 | | xtl_param_names(Nr,ParamNames) :- |
964 | | findall(N,between(1,Nr,N),Nrs), |
965 | | maplist(nr_to_para,Nrs,ParamNames). |
966 | | |
967 | | nr_to_para(Nr,Para) :- ajoin([para,Nr],Para). |
968 | | |
969 | | :- use_module(translate, [translate_xtl_value/2, translate_bvalue/2, translate_bvalue_to_parseable_classicalb/2]). |
970 | | mytranslate(H,S) :- |
971 | | xtl_mode, !, |
972 | | translate_xtl_value(H,S0), |
973 | | ajoin([S0, '.'],S). |
974 | | mytranslate(H,S) :- |
975 | | !, |
976 | | % should we use unicode mode to avoid more ambiguities? |
977 | | translate_bvalue_to_parseable_classicalb(H,S). |
978 | | |
979 | | print_json_paras(Values,Names,OpName,json(JsonList)) :- |
980 | | filter_json_paras(Values,Names,OpName,FValues,FNames), |
981 | | print_json_paras_aux(FValues,1,FNames,JsonList). |
982 | | % filter out parameters (e.g., large constants or symbolic values that cannot be read back in) |
983 | | % TODO: complete |
984 | | filter_json_paras([],Names,OpName,[],[]) :- |
985 | | (Names = [] -> true |
986 | | ; ajoin(['Missing values for arguments to operation ',OpName,':'],Msg), |
987 | | add_error(filter_json_paras,Msg,Names)). |
988 | | filter_json_paras([Val|TV],InNames,OpName,Vals,Names) :- |
989 | | (InNames = [Name|TN] |
990 | | -> |
991 | | (do_not_print_value(Val,Name,OpName) |
992 | | -> filter_json_paras(TV,TN,OpName,Vals,Names) |
993 | | ; Vals = [Val|RV], Names=[Name|RN], |
994 | | filter_json_paras(TV,TN,OpName,RV,RN) |
995 | | ) |
996 | | ; add_error(filter_json_paras,'Too many values:',[Val|TV]), Vals=[] |
997 | | ). |
998 | | |
999 | | :- use_module(memoization,[is_memoization_closure/4]). |
1000 | | :- use_module(probsrc(kernel_freetypes),[registered_freetype/2, freetype_case_db/3]). |
1001 | | do_not_print_value(Value,Name,_OpName) :- |
1002 | | value_cannot_be_pretty_printed_safely(Value,Name),!. |
1003 | | do_not_print_value(_,Name,'$setup_constants') :- % Do not save constants generated for freetypes and their cases |
1004 | | ( registered_freetype(Name,_) -> add_debug_message(save_trace_file,'Not saving FREETYPE to trace file: ',Name) |
1005 | | ; freetype_case_db(Name,_,_) -> add_debug_message(save_trace_file,'Not saving FREETYPE case to trace file: ',Name) |
1006 | | ). |
1007 | | % TODO: we could also improve pretty-printing for memoization closures and external_function_calls |
1008 | | % TO DO: maybe do not print huge AVL sets, in particular constants |
1009 | | |
1010 | | |
1011 | | :- use_module(probsrc(bsyntaxtree),[map_over_bexpr/2]). |
1012 | | :- use_module(external_function_declarations,[external_function_library/4]). |
1013 | | % at the moment we cannot read-in symbolic closures with external function/pred calls |
1014 | | % unless they are also automatically visibile in the REPL, VisB, ... |
1015 | | cannot_pretty_print(external_function_call(Name,_Paras)) :- |
1016 | | \+ external_function_library(Name,_Arity,expression,_Lib). |
1017 | | cannot_pretty_print(external_pred_call(Name,_Paras)) :- |
1018 | | \+ external_function_library(Name,_Arity,predicate,_Lib). |
1019 | | |
1020 | | % check if we can safely print and read-back in a value |
1021 | | value_cannot_be_pretty_printed_safely(closure(P,T,B),Name) :- |
1022 | | closure_cannot_be_pretty_printed_safely(P,T,B,Name). |
1023 | | value_cannot_be_pretty_printed_safely((A,B),Name) :- |
1024 | | (value_cannot_be_pretty_printed_safely(A,Name) -> true ; value_cannot_be_pretty_printed_safely(B,Name)). |
1025 | | value_cannot_be_pretty_printed_safely(rec(Fields),Name) :- |
1026 | | member(field(_,FVal),Fields), value_cannot_be_pretty_printed_safely(FVal,Name). |
1027 | | value_cannot_be_pretty_printed_safely([H|T],Name) :- |
1028 | | member(FVal,[H|T]), value_cannot_be_pretty_printed_safely(FVal,Name). |
1029 | | % TODO: freevals |
1030 | | |
1031 | | % check if we can pretty-print a symbolic closure and read-it back safely |
1032 | | closure_cannot_be_pretty_printed_safely(P,T,B,ValueName) :- is_memoization_closure(P,T,B,_), |
1033 | | add_message(save_trace_file,'Not saving memoization closure value to trace file: ',ValueName). |
1034 | | closure_cannot_be_pretty_printed_safely(_,_,Body,ValueName) :- |
1035 | | map_over_bexpr(cannot_pretty_print,Body), |
1036 | | add_message(save_trace_file,'Not saving symbolic closure with external function calls to trace file: ',ValueName). |
1037 | | |
1038 | | % print_json_paras_aux(ListOfValues,ParameterNr,ListOfParameterNames) |
1039 | | print_json_paras_aux([],_,_,[]) :- !. |
1040 | | print_json_paras_aux([H|T],Nr,[HName|NT],[JsonH|JsonT]) :- !, Nr1 is Nr+1, |
1041 | | mytranslate(H,HValue), |
1042 | | JsonH = (HName=string(HValue)), |
1043 | | print_json_paras_aux(T,Nr1,NT,JsonT). |
1044 | | print_json_paras_aux(P,Nr,PN,[]) :- |
1045 | | add_internal_error('Cannot print JSON parameters:',print_json_paras_aux(P,Nr,PN)). |
1046 | | |
1047 | | % print a list of identifier names for JSON |
1048 | | print_json_names(Names,array(JsonList)) :- print_json_names_aux(Names,JsonList). |
1049 | | print_json_names_aux([],[]). |
1050 | | print_json_names_aux([HName|T],[string(HName)|JsonT]) :- |
1051 | | print_json_names_aux(T,JsonT). |
1052 | | |
1053 | | % find change bindings in the state |
1054 | | changed_binding(FromId,ToId,Bind) :- |
1055 | | visited_expression(FromId,FromState), |
1056 | | visited_expression(ToId,ToState), |
1057 | | get_id_binding(ToState,Bind), |
1058 | | \+ get_id_binding(FromState,Bind). |
1059 | | |
1060 | | % find variables which have not been modified in the state |
1061 | | unchanged_binding(FromId,ToId,Bind) :- |
1062 | | visited_expression(FromId,FromState), % slightly inefficient to expand states again |
1063 | | visited_expression(ToId,ToState), |
1064 | | get_id_binding(ToState,Bind), |
1065 | | get_id_binding(FromState,Bind). |
1066 | | |
1067 | | get_change_list(FromId,ToId,ChangedVarNames,ChangedValues) :- |
1068 | | findall(Bind,changed_binding(FromId,ToId,Bind),List), |
1069 | | maplist(decompose_binding,List,ChangedVarNames,ChangedValues). |
1070 | | get_unchanged_list(FromId,ToId,UnChangedVarNames) :- |
1071 | | findall(Bind,unchanged_binding(FromId,ToId,Bind),List), |
1072 | | maplist(decompose_binding,List,UnChangedVarNames,_). |
1073 | | |
1074 | | decompose_binding(bind(ID,Val),ID,Val). |
1075 | | |
1076 | | |
1077 | | get_id_binding(const_and_vars(_,List),Bind) :- !, member(Bind,List). |
1078 | | get_id_binding(concrete_constants(List),Bind) :- !, member(Bind,List). |
1079 | | get_id_binding(List,Bind) :- !, member(Bind,List). |
1080 | | |