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 |