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