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