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		; B = '$setup_constants' -> true % old trace format; SETUP_CONSTANTS without arguments
558		; B = '$initialise_machine' -> true % ditto for INITIALISATION
559		; formatsilent('*** SAME EVENT WITH VARYING ARITY: ~w : ~w vs ~w arguments ***~n',[F,N,N2]),
560		% Probably due to show_eventb_any_arguments differently set?
561		fail),
562		A=..[F|AA], B=..[F2|BB],
563		l_unify(AA,BB).
564		l_unify([],[]).
565		l_unify([H|T],[I|S]) :- unify(H,I), l_unify(T,S).
566
567
568		unify_functor('initialise_machine','$initialise_machine',_) :- !. % old-style format
569		unify_functor('setup_constants','$setup_constants',root) :- !. % old-style format
570		unify_functor(X,X,_).
571
572		%:- use_module(custom_explicit_sets,[equal_explicit_sets/4]).
573		:- use_module(debug).
574		unify(A,A) :- !.
575		unify(A,avl_set(B)) :- %print(exp(A,B)),nl,
576		expand_explicit_set(A,AA),
577		%nl,translate:print_bvalue(AA),nl, translate:print_bvalue(avl_set(B)),nl, % print(chck(A,AA,B)),nl,
578		AA = avl_set(B),!.
579		%unify(A,B) :- print(unify(A,B)),nl,fail.
580		unify(C1,C2) :- is_a_set(C1),(C2=closure(_P,_T,_B) ; C2=global_set(_)),
581		%print(unify_closure(C1,C2)),nl,
582		(C1=[_|_] -> custom_explicit_sets:convert_to_avl(C1,C11) ; C11=C1), % TO DO: replace by proper expansion predicate
583		(unify_explicit_sets(C11,C2)
584		-> true
585		; print(ko_unify_closure),nl, translate:print_bvalue(C11),nl, translate:print_bvalue(C2),nl,
586		%terms:term_hash((C1,C2),H), print(hash(H)),nl, (H=140674321 -> trace, unify_explicit_sets(C11,C2)),
587		fail),!.
588		%avl_domain(B,R), print(chck(A,B,R)),nl,l_unify(A,R).
589		unify(C1,C2) :- %tools_printing:print_term_summary(fail(C1,C2)),nl,
590		debug_println(9,unify_failed(C1,C2)),fail.
591
592		is_a_set(closure(_,_,_)).
593		is_a_set([]).
594		is_a_set([_|_]).
595		is_a_set(global_set(_)).
596		is_a_set(avl_set(_)).
597
598		expand_explicit_set([H|T],AA) :- !, custom_explicit_sets:convert_to_avl([H|T],AA).
599		expand_explicit_set(A,AA) :-
600		on_enumeration_warning(custom_explicit_sets:try_expand_and_convert_to_avl_if_smaller_than(A,AA,200), fail).
601		unify_explicit_sets(C1,C2) :-
602		ALLOW=no_expansion, %(C1 = avl_set(_) -> ALLOW=allow_expansion ; ALLOW=no_expansion),
603		on_enumeration_warning(custom_explicit_sets:equal_explicit_sets4(C1,C2,ALLOW,no_wf_available), fail).
604
605
606		perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,root) :-
607		functor(ActionAsTerm,'setup_constants',_), !, % rename to new format
608		nl,print('DEPRECATED TRACE FILE'),nl,nl,nl,
609		ActionAsTerm =.. [_|Args], ActionAsTerm2 =..['$setup_constants'|Args],
610		perform_single_operation_retry(Options,ActionAsTerm2,Action,NewID).
611		perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,State) :-
612		(State=root ; State=concrete_constants(_)),
613		functor(ActionAsTerm,'initialise_machine',_), !, % rename to new format
614		nl,print('DEPRECATED TRACE FILE'),nl,nl,nl,
615		ActionAsTerm =.. [_|Args], ActionAsTerm2 =..['$initialise_machine'|Args],
616		perform_single_operation_retry(Options,ActionAsTerm2,Action,NewID).
617		perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,_State) :-
618		perform_single_operation_retry(Options,ActionAsTerm,Action,NewID).
619
620
621		% check that parameters provided for setup_constants in trace file can be found in State
622		%check_initialised_args([],_).
623		%check_initialised_args([V|T],State) :-
624		% select(bind(_,V2),State,Rest),
625		% unify(V,V2),
626		% %print('SELECTED: '),translate:print_bvalue(V2),nl,
627		% !,
628		% check_initialised_args(T,Rest).
629		%check_initialised_args([V|T],State) :-
630		% print('MISMATCH'),nl, %print(mismatch(V,C)),nl,
631		% print('COULD NOT FIND: '), translate:print_bvalue(V),nl,
632		% tools_printing:print_term_summary(V),nl,
633		% %print(V),nl, print(State),nl,
634		% V=closure(_,_,_), memberchk(bind(_,closure(_,_,_)),State),
635		% check_initialised_args(T,State).
636
637		perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
638		functor(ActionAsTerm,'$setup_constants',_), !,
639		(get_prob_application_type(tcltk) -> OTHER = ['$partial_setup_constants'] ; OTHER = []),
640		perform_alternative_op_with_same_functor(Options, ['$setup_constants' | OTHER],
641		'set up constants', 'initialisation of constants',
642		ActionAsTerm, Action, NewID),
643		%visited_expression(NewID,concrete_constants(C)), ActionAsTerm =.. [_|Args],
644		% check that state NewID corresponds to parameters provided for setup_constants in trace file
645		%print(check_args),nl, check_initialised_args(Args,C), print('argsok'),nl. % TO DO: try and enable this for all tests
646		true.
647		perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
648		functor(ActionAsTerm,'$initialise_machine',_),!,
649		perform_alternative_op_with_same_functor(Options, ['$initialise_machine'],
650		'initialise', 'initialisation',
651		ActionAsTerm, Action, NewID),
652		true. %visited_expression(NewID,S), (S=const_and_vars(_,VS) -> true ; VS=S), ActionAsTerm =.. [_|Args],
653		%check_initialised_args(Args,VS), print('initargsok'),nl.
654		perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
655		functor(ActionAsTerm,tau,_), arg(1,ActionAsTerm,Arg), nonvar(Arg),!,
656		perform_alternative_op_with_same_functor(Options, [tau],
657		tau, tau,
658		ActionAsTerm, Action, NewID).
659		perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
660		functor(ActionAsTerm,F,0), preference(show_eventb_any_arguments,true),
661		/* then allow also the same operation name but with more arguments */
662		member( (_Id,Action,ActionAsTerm2,NewID), Options),
663		functor(ActionAsTerm2,F,FArity), FArity>0,
664		formatsilent('% Allowing extra Event-B style ANY arguments.~n',[]).
665		perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
666		functor(ActionAsTerm,F,N),N>0, preference(show_eventb_any_arguments,false),
667		/* then allow also the same operation name but with more arguments */
668		member( (_Id,Action,F,NewID), Options),
669		formatsilent('% Allowing operation without Event-B style ANY arguments.~n',[]).
670		%perform_single_operation_retry(Options,_ActionsAsTerm,_Action,_NewID) :-
671		% print_message('No more options: '), print(Options),nl,fail.
672
673
674		perform_custom_operation_retry(OpName,NewID) :-
675		(OpName = '$initialise_machine' ; OpName = '$setup_constants'),
676		!,
677		current_state_id(CurID),
678		(max_reached_for_node(CurID) ; not_all_transitions_added(CurID)),
679		preferences:get_preference(maxNrOfInitialisations,0),
680		tcltk_add_user_executed_operation_typed(OpName,_,b(truth,pred,[]),NewID),
681		(get_preference(deterministic_trace_replay,true) -> ! ; true),
682		print_green(init_found(NewID)),nl.
683		perform_custom_operation_retry(ActionAsTerm,NewID) :-
684		(ActionAsTerm = '-->'(_,_) % for operations with return types we cannot provide a predicate to solve yet
685		-> preferences:get_preference(maxNrOfEnablingsPerOperation,0)
686		; true),
687		current_state_id(CurID),
688		get_operation_name(ActionAsTerm,OpName),
689		(max_reached_for_node(CurID) ; time_out_for_node(CurID,OpName,_) ; not_all_transitions_added(CurID)),
690		debug_println(9,try_custom(CurID,ActionAsTerm)), % Execute operation by predicate
691		% (state_space:transition(CurID,AA,BB,CC),format('Successor of ~w: ~w --~w--> ~w~n',[CurID,AA,BB,CC]),fail ; true),
692		get_operation_return_values_and_arguments(ActionAsTerm,ExpectedResults,OpArgs),
693		% TO DO: optionally check return values
694		(OpArgs = [] -> Pred = b(truth,pred,[])
695		; \+ b_is_operation_name(OpName)
696		-> add_error(trace_checking_fails,'Operation does not exist in loaded specification:',OpName),fail
697		; b_get_machine_operation_typed_parameters(OpName,TArgParas),
698		l_generate_predicate(OpArgs,TArgParas,OpName,Conjuncts),
699		conjunct_predicates(Conjuncts,Pred)
700		),
701		!,
702		%print('PRED: '),translate:print_bexpr(Pred),nl,
703		start_ms_timer(Timer),
704		profile_single_call(OpName,CurID,
705		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
706		),
707		(get_preference(deterministic_trace_replay,true) -> ! ; true), % by preventing backtracking we can reduce memory consumption
708		print_green(successor_found(NewID, OpName)),nl,
709		get_operation_return_values_and_arguments(OpTerm,ActualResults,_),
710		(l_unify(ExpectedResults,ActualResults) -> true
711		; ajoin(['Result values for ',OpName,' do not match for transition from ',CurID,' to ',NewID,':'],Msg),
712		translate_bvalue(ExpectedResults,ER),
713		translate_bvalue(ActualResults,AR),
714		add_warning(b_trace_checking,Msg,[expected(ER),actual(AR)])
715		),
716		(debug_mode(on) -> stop_ms_timer_with_msg(Timer,'Custom: ') ; true),
717		garbage_collect, % important to keep memory consumption down for long traces e.g. for Innotrans VBF traces
718		(debug_mode(on) -> print_memory_used_wo_gc,nl ; true),
719		tcltk_get_options(_).
720
721		l_generate_predicate([],[],_,[]) :- !.
722		l_generate_predicate([],_,Op,[]) :- !, add_warning(b_trace_checking,'Trace file contains too few parameters for: ',Op).
723		l_generate_predicate(_,[],Op,[]) :- !, add_warning(b_trace_checking,'Trace file contains too many parameters for: ',Op).
724		l_generate_predicate([ArgVal|TArg],[TypedPara|TPar],OpName,[Pred|TPred]) :-
725		generate_predicate(ArgVal,TypedPara,Pred),
726		l_generate_predicate(TArg,TPar,OpName,TPred).
727		generate_predicate(ArgVal,TypedPara,b(equal(TypedPara,TVal),pred,[])) :-
728		get_texpr_type(TypedPara,Type),
729		TVal = b(value(ArgVal),Type,[]).
730
731		perform_alternative_op_with_same_functor(Options,Functors,ActionMsg,AltMsg,ActionAsTerm,Action,NewID) :-
732		\+ member( (_,_,ActionAsTerm,_), Options),
733		(silent_mode(on) -> true
734		; ajoin(['Could not ', ActionMsg, ' with parameters from trace file.'], Msg1),
735		ajoin(['Will attempt any possible ', AltMsg, '.'], Msg2),
736		print_message(Msg1), print_message(Msg2)
737		),
738		%print(ActionAsTerm),nl, print(Options),nl,nl,
739		member( (_,ActionStr,MachineActionAsTerm,NewID), Options),
740		functor(MachineActionAsTerm,Functor,_),
741		member(Functor,Functors),
742		(Action=ActionStr -> true ; print(cannot_match(Action,ActionStr)),nl,fail).
743
744		single_operation_skip(tau(_),Ident) :-
745		(silent_mode(on) -> true
746		; ident(Ident), print(' | *** TRYING TO SKIP TAU IN TRACE FILE'),nl).
747
748
749
750		ident(0).
751		ident(N) :- N > 40, !, N1 is N mod 40, ident(N1).
752		ident(N) :- N>0, print('- '), N1 is N-1, ident(N1).
753
754
755		/* ------------------------------------------------------------------ */
756
757		:- use_module(state_space,[get_action_trace/1]).
758		print_trace_as_fdr_check :- silent_mode(on),!.
759		print_trace_as_fdr_check :-
760		print('-- Trace Check Generated by ProB:'),nl,
761		get_action_trace(T),
762		reverse(T,RT),
763		print('PROB_TEST_TRACE = '),print_fdr(RT),
764		nl,
765		print('assert MAIN [T= PROB_TEST_TRACE'),nl.
766
767		print_fdr([]) :- print('STOP'),nl.
768		print_fdr([jump|T]) :- print_fdr(T).
769		print_fdr([action(Str,Term)|T]) :-
770		(Term = i(_)
771		-> (nl,print(' ( STOP /\\ '))
772		; (Term = tick(_)
773		-> print('SKIP ; ')
774		; ((Term = tau(_) ; Term = 'start_cspm_MAIN')
775		-> true
776		; (print(Str), print(' -> '))
777		)
778		)),
779		print_fdr(T),
780		(Term = i(_)
781		-> print(' )')
782		; true
783		).
784
785		% -----------------------
786
787		tcltk_save_history_as_trace_file(Style,File) :-
788		tcltk_save_history_as_trace_file(Style,[],File).
789
790		tcltk_save_history_as_trace_file(Style,Options,File) :-
791		formatsilent('% Saving history (~w format) to: ~w~n',[Style,File]),
792		open(File,write,Stream,[encoding(utf8)]),
793		currently_opened_specification_name(OurName),
794		(Style=prolog -> format(Stream,'machine(\'~w\').~n',[OurName]) ; true),
795		call_cleanup(print_trace_for_replay(Style,Options,Stream),
796		(close(Stream),print_message(done))).
797
798		:- use_module(state_space,[transition/4, op_trace_ids/1]). % transition(CurID,Term,TransId,DestID)
799
800		% print the animator's history trace for later replay
801		% prolog style is currently used by ProB Tcl/Tk
802		% json style is used by ProB2 UI
803		print_trace_for_replay(Style,Options,Stream) :-
804		op_trace_ids(OpIds),
805		reverse(OpIds,Trace),
806		print_trace_for_replay(Style,Trace,Options,Stream).
807
808		print_trace_for_replay(prolog,Trace,_,Stream) :- !, print_transition_list_prolog(Trace,Stream).
809		print_trace_for_replay(json,Trace,Options,Stream) :- !, print_transition_list_json(Trace,Options,Stream).
810		print_trace_for_replay(Style,_,_,_Stream) :-
811		add_internal_error('Style not supported: ',print_trace_for_replay(Style,_,_,_)).
812
813		print_transition_list_prolog(Trace,Stream) :-
814		member(OpId,Trace),
815		transition(PrevId,Op,OpId,SuccId),
816		(atomic(Op),
817		( b_or_z_mode,
818		transition(PrevId,Op,_,SuccId2), SuccId2 \= SuccId -> true), % another transition with same label Op exists
819		translate:get_non_det_modified_vars_in_target_id(Op,SuccId,NonDetVars)
820		-> print_quoted(Stream,'$non_det_modified_vars'(Op,NonDetVars))
821		; print_quoted(Stream, Op)
822		),
823		format(Stream,'.~n',[]),
824		fail.
825		print_transition_list_prolog(_,_).
826
827		:- use_module(version, [version_str/1, revision/1]). % , lastchangeddate/1
828		:- use_module(library(system),[ datime/1, environ/2]).
829		:- use_module(specfile,[currently_opened_file/1, currently_opened_specification_name/1]).
830		:- use_module(tools_strings,[number_codes_min_length/3]).
831		:- use_module(tools_lists,[get_member_option/3]).
832		:- use_module(tools,[get_tail_filename/2]).
833
834
835		:- use_module(extrasrc(json_parser),[json_write_stream/3]).
836		% print list in JSON format for ProB2 UI:
837		% this is formatVersion 1
838		print_transition_list_json(Trace,Options,Stream) :-
839		get_prob_application_type(ApplType),
840		(get_member_option(description,Options,Desc) -> true
841		; ApplType=probcli -> Desc = 'File created by probcli'
842		; ApplType=tcltk -> Desc = 'File created by ProB Tcl/Tk'
843		; Desc = 'File created by ProB'
844		),
845		temporary_set_preference(expand_avl_upto,-1,CHNG),
846		call_cleanup(
847		print_json_list(Trace,root,TransitionList), % print list of transitions in JSON format
848		reset_temporary_preference(expand_avl_upto,CHNG)),
849		format_current_iso_time(Timestamp),
850		(nonmember(privacy_mode,Options),environ('USER',User)
851		-> ajoin([ApplType,' (',User,')'],Creator)
852		; Creator = ApplType),
853		version_str(Version),
854		revision(Rev),
855		currently_opened_file(File),
856		(nonmember(privacy_mode,Options) -> StoredFile=File
857		; get_tail_filename(File,StoredFile) % do not store full path
858		),
859		currently_opened_specification_name(Model),
860		Json = json([
861		description=string(Desc),
862		transitionList=array(TransitionList),
863		metadata=json([
864		fileType=string('Trace'),
865		formatVersion=number(1),
866		savedAt=string(Timestamp), % TODO: rename to createdAt and make optional for testing
867		creator=string(Creator),
868		proBCliVersion=string(Version),
869		proBCliRevision=string(Rev), % not used by Java Kernel
870		modelName=string(Model),
871		modelFile=string(StoredFile) % not used by Java Kernel
872		])
873		]),
874		(json_write_stream(Stream,Json,[pretty(true)])
875		-> true
876		; add_error(print_transition_list_json,'Writing json trace failed'), fail).
877		% to do: maybe also save types of variables, constants, operation parameters, ...
878		% and modification time of modelFile, SHA of model, ...
879
880		% example: "2020-12-23T14:33:00Z",
881		format_current_iso_time(TimestampAtom) :-
882		% TODO: this is incorrect
883		% datime is the time in the current timezone, but does not include that zone
884		% we put Z behind the ISO-8601 datetime to mark it as UTC which is incorrect!
885		datime(datime(Yr,Mon,Day,Hr,Min,Sec)),
886		number_codes_min_length(Yr,4,YrC),
887		number_codes_min_length(Mon,2,MonC),
888		number_codes_min_length(Day,2,DayC),
889		number_codes_min_length(Hr,2,HrC),
890		number_codes_min_length(Min,2,MinC),
891		number_codes_min_length(Sec,2,SecC),
892		format_to_codes('~s-~s-~sT~s:~s:~sZ',[YrC,MonC,DayC,HrC,MinC,SecC],TimestampCodes),
893		atom_codes(TimestampAtom,TimestampCodes).
894
895		% print a list of transition ids in JSON format
896		print_json_list([],_,[]).
897		print_json_list([H|T],FromID,[JsonH|JsonT]) :-
898		(H=jump(NewID) -> true
899		; print_json_opid(H,JsonH,FromID,NewID) -> true
900		; add_error(print_json_list,'Writing operation failed, transition id is: ',H), NewID=FromID
901		),
902		print_json_list(T,NewID,JsonT).
903
904		:- use_module(specfile,[get_operation_internal_name/2,
905		get_operation_return_values_and_arguments/3,
906		get_operation_description_for_transition/4,
907		get_possible_language_specific_top_level_event/3,
908		xtl_mode/0]).
909
910		% print an operation id (transition id) for a JSON Trace
911		print_json_opid(OpId,Json,PrevId,SuccId) :-
912		(transition(PrevId,Op,OpId,SuccId) -> PrevId1=PrevId
913		; add_warning(print_json_list,'Cannot find operation id from given source id: ',OpId:from(PrevId):to(SuccId)),
914		transition(PrevId1,Op,OpId,SuccId)
915		),
916		get_operation_internal_name(Op,OpName), % TO DO: currently this is INITIALISATION instead of $initialise_machine
917		(get_possible_language_specific_top_level_event(OpName,ResultNames,ParaNames) -> true
918		; ResultNames=unknown, ParaNames=unknown),
919		get_operation_return_values_and_arguments(Op,ReturnValues,Paras),
920		% TO DO: extract variables and constants for $initialise_machine, $setup_constants
921		Json = json([name=string(OpName)|T1]),
922		(get_operation_description_for_transition(PrevId,Op,SuccId,Desc)
923		-> T1=[description=string(Desc)|T2]
924		; T2=T1),
925		(Paras = []
926		-> T3=T2 % do not print Paras to reduce memory in JSON file
927		; xtl_mode
928		-> (ParaNames=unknown
929		-> length(Paras,PLen),
930		xtl_param_names(PLen,PNames2)
931		; PNames2 = ParaNames),
932		print_json_paras(Paras,PNames2,OpName,JsonParams),
933		T2=[params=JsonParams|T3]
934		; get_preference(show_eventb_any_arguments,true),
935		\+ same_length(Paras,ParaNames)
936		-> % we cannot easily use the parameters during replay; ANY parameters are currently only added when there are no other parameters
937		add_warning(json_export,'Parameter mismatch: ',OpName:ParaNames,Paras),
938		T3=T2
939		; print_json_paras(Paras,ParaNames,OpName,JsonParams),
940		T2=[params=JsonParams|T3]
941		),
942		((xtl_mode ; ReturnValues = [])
943		-> T4=T3 % do not print results to reduce memory in JSON file
944		; print_json_paras(ReturnValues,ResultNames,OpName,JsonResults),
945		T3=[results=JsonResults|T4]
946		),
947		get_change_list(PrevId1,SuccId,ChangedVarNames,ChangedValues),
948		(xtl_mode % special case for XTL: "xtl_state": "destStateTerm"
949		-> visited_expression(SuccId,SuccState),
950		print_json_paras([SuccState],[xtl_state],OpName,JsonDestState),
951		T4=[destState=JsonDestState|T5]
952		; (ChangedVarNames = []
953		-> T5=T4
954		; print_json_paras(ChangedValues,ChangedVarNames,OpName,JsonDestState),
955		T4=[destState=JsonDestState|T5]
956		)
957		),
958		get_unchanged_list(PrevId1,SuccId,UnChangedVarNames),
959		(UnChangedVarNames = []
960		-> T6=T5
961		; print_json_names(UnChangedVarNames,JsonDestStateNotChanged),
962		T5=[destStateNotChanged=JsonDestStateNotChanged|T6]
963		),
964		T6=[].
965
966		:- use_module(library(between),[between/3]).
967		xtl_param_names(Nr,ParamNames) :-
968		findall(N,between(1,Nr,N),Nrs),
969		maplist(nr_to_para,Nrs,ParamNames).
970
971		nr_to_para(Nr,Para) :- ajoin([para,Nr],Para).
972
973		:- use_module(translate, [translate_xtl_value/2, translate_bvalue/2, translate_bvalue_to_parseable_classicalb/2]).
974		mytranslate(H,S) :-
975		xtl_mode, !,
976		translate_xtl_value(H,S0),
977		ajoin([S0, '.'],S).
978		mytranslate(H,S) :-
979		!,
980		% should we use unicode mode to avoid more ambiguities?
981		translate_bvalue_to_parseable_classicalb(H,S).
982
983		print_json_paras(Values,Names,OpName,json(JsonList)) :-
984		filter_json_paras(Values,Names,OpName,FValues,FNames),
985		print_json_paras_aux(FValues,1,FNames,JsonList).
986		% filter out parameters (e.g., large constants or symbolic values that cannot be read back in)
987		% TODO: complete
988		filter_json_paras([],Names,OpName,[],[]) :-
989		(Names = [] -> true
990		; ajoin(['Missing values for arguments to operation ',OpName,':'],Msg),
991		add_error(filter_json_paras,Msg,Names)).
992		filter_json_paras([Val|TV],InNames,OpName,Vals,Names) :-
993		(InNames = [Name|TN]
994		->
995		(do_not_print_value(Val,Name,OpName)
996		-> filter_json_paras(TV,TN,OpName,Vals,Names)
997		; Vals = [Val|RV], Names=[Name|RN],
998		filter_json_paras(TV,TN,OpName,RV,RN)
999		)
1000		; add_error(filter_json_paras,'Too many values:',[Val|TV]), Vals=[]
1001		).
1002
1003		:- use_module(memoization,[is_memoization_closure/4]).
1004		:- use_module(probsrc(kernel_freetypes),[registered_freetype/2, freetype_case_db/3]).
1005		do_not_print_value(Value,Name,_OpName) :-
1006		value_cannot_be_pretty_printed_safely(Value,Name),!.
1007		do_not_print_value(_,Name,'$setup_constants') :- % Do not save constants generated for freetypes and their cases
1008		( registered_freetype(Name,_) -> add_debug_message(save_trace_file,'Not saving FREETYPE to trace file: ',Name)
1009		; freetype_case_db(Name,_,_) -> add_debug_message(save_trace_file,'Not saving FREETYPE case to trace file: ',Name)
1010		).
1011		% TODO: we could also improve pretty-printing for memoization closures and external_function_calls
1012		% TO DO: maybe do not print huge AVL sets, in particular constants
1013
1014
1015		:- use_module(probsrc(bsyntaxtree),[map_over_bexpr/2]).
1016		:- use_module(external_function_declarations,[external_function_library/4]).
1017		% at the moment we cannot read-in symbolic closures with external function/pred calls
1018		% unless they are also automatically visibile in the REPL, VisB, ...
1019		cannot_pretty_print(external_function_call(Name,_Paras)) :-
1020		\+ external_function_library(Name,_Arity,expression,_Lib).
1021		cannot_pretty_print(external_pred_call(Name,_Paras)) :-
1022		\+ external_function_library(Name,_Arity,predicate,_Lib).
1023
1024		% check if we can safely print and read-back in a value
1025		value_cannot_be_pretty_printed_safely(closure(P,T,B),Name) :-
1026		closure_cannot_be_pretty_printed_safely(P,T,B,Name).
1027		value_cannot_be_pretty_printed_safely((A,B),Name) :-
1028		(value_cannot_be_pretty_printed_safely(A,Name) -> true ; value_cannot_be_pretty_printed_safely(B,Name)).
1029		value_cannot_be_pretty_printed_safely(rec(Fields),Name) :-
1030		member(field(_,FVal),Fields), value_cannot_be_pretty_printed_safely(FVal,Name).
1031		value_cannot_be_pretty_printed_safely([H|T],Name) :-
1032		member(FVal,[H|T]), value_cannot_be_pretty_printed_safely(FVal,Name).
1033		% TODO: freevals
1034
1035		% check if we can pretty-print a symbolic closure and read-it back safely
1036		closure_cannot_be_pretty_printed_safely(P,T,B,ValueName) :- is_memoization_closure(P,T,B,_),
1037		add_message(save_trace_file,'Not saving memoization closure value to trace file: ',ValueName).
1038		closure_cannot_be_pretty_printed_safely(_,_,Body,ValueName) :-
1039		map_over_bexpr(cannot_pretty_print,Body),
1040		add_message(save_trace_file,'Not saving symbolic closure with external function calls to trace file: ',ValueName).
1041
1042		% print_json_paras_aux(ListOfValues,ParameterNr,ListOfParameterNames)
1043		print_json_paras_aux([],_,_,[]) :- !.
1044		print_json_paras_aux([H|T],Nr,[HName|NT],[JsonH|JsonT]) :- !, Nr1 is Nr+1,
1045		mytranslate(H,HValue),
1046		JsonH = (HName=string(HValue)),
1047		print_json_paras_aux(T,Nr1,NT,JsonT).
1048		print_json_paras_aux(P,Nr,PN,[]) :-
1049		add_internal_error('Cannot print JSON parameters:',print_json_paras_aux(P,Nr,PN)).
1050
1051		% print a list of identifier names for JSON
1052		print_json_names(Names,array(JsonList)) :- print_json_names_aux(Names,JsonList).
1053		print_json_names_aux([],[]).
1054		print_json_names_aux([HName|T],[string(HName)|JsonT]) :-
1055		print_json_names_aux(T,JsonT).
1056
1057		% find change bindings in the state
1058		changed_binding(FromId,ToId,Bind) :-
1059		visited_expression(FromId,FromState),
1060		visited_expression(ToId,ToState),
1061		get_id_binding(ToState,Bind),
1062		\+ get_id_binding(FromState,Bind).
1063
1064		% find variables which have not been modified in the state
1065		unchanged_binding(FromId,ToId,Bind) :-
1066		visited_expression(FromId,FromState), % slightly inefficient to expand states again
1067		visited_expression(ToId,ToState),
1068		get_id_binding(ToState,Bind),
1069		get_id_binding(FromState,Bind).
1070
1071		get_change_list(FromId,ToId,ChangedVarNames,ChangedValues) :-
1072		findall(Bind,changed_binding(FromId,ToId,Bind),List),
1073		maplist(decompose_binding,List,ChangedVarNames,ChangedValues).
1074		get_unchanged_list(FromId,ToId,UnChangedVarNames) :-
1075		findall(Bind,unchanged_binding(FromId,ToId,Bind),List),
1076		maplist(decompose_binding,List,UnChangedVarNames,_).
1077
1078		decompose_binding(bind(ID,Val),ID,Val).
1079
1080
1081		get_id_binding(const_and_vars(_,List),Bind) :- !, member(Bind,List).
1082		get_id_binding(concrete_constants(List),Bind) :- !, member(Bind,List).
1083		get_id_binding(List,Bind) :- !, member(Bind,List).
1084