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