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