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