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