1		% (c) 2009-2023 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		:- module(b_show_history,[write_history_to_file/1, write_full_history_to_file/1, write_history_to_file/2,
6		write_history_to_user_output/1,
7		write_values_to_file/1,write_all_values_to_dir/1]).
8
9		:- use_module(module_information,[module_info/2]).
10		:- module_info(group,misc).
11		:- module_info(description,'Write animator history into a file in B format.').
12
13		:- use_module(library(lists)).
14
15		:- use_module(state_space, [transition/4,visited_expression/2, op_trace_ids/1,
16		current_expression/2, get_state_id_trace/1]).
17		:- use_module(specfile, [%state_corresponds_to_initialised_b_machine/1,
18		expand_to_constants_and_variables/3]).
19		:- use_module(translate, [translate_bvalue/2,
20		translate_bvalue_with_type/3,
21		translate_event/2]).
22		%:- use_module(bmachine, [b_get_machine_operation/4]).
23		%:- use_module(bsyntaxtree, [get_texpr_expr/2]).
24		%:- use_module(kernel_waitflags, [init_wait_flags/1,ground_wait_flags/1]).
25		%:- use_module(b_state_model_check, [set_up_transition/7]).
26
27		:- use_module(error_manager, [add_internal_error/2]).
28
29		:- use_module(preferences).
30
31		:- use_module(tools_io).
32		:- use_module(tools, [ajoin/2]).
33		:- use_module(debug).
34		%:- use_module(store,[lookup_value/3]).
35
36		write_history_to_file(Filename) :-
37		write_history_to_file(Filename,[show_init]).
38		write_full_history_to_file(Filename) :-
39		write_history_to_file(Filename,[show_init,show_states]).
40		write_history_to_file(Filename,Options) :-
41		debug_println(9,write_history_to_file(Filename,Options)),
42		assert_options(Options),
43		safe_intelligent_open_file(Filename,write,_,[alias(histout)]),
44		get_preference(expand_avl_upto,Max),
45		set_preference(expand_avl_upto,-1), % means no limit
46		call_cleanup(write_history, (safe_intelligent_close_file(Filename,histout),
47		set_preference(expand_avl_upto,Max))).
48
49		%write_history_to_user_output :- write_history_to_user_output([show_init]).
50		write_history_to_user_output(Options) :-
51		assert_options(Options),
52		write_history.
53
54		assert_options(Options) :-
55		retractall(option(_)),
56		maplist(assert_option,(Options)).
57		assert_option(Option) :-
58		(valid_option(Option) -> assertz(option(Option)) ; add_internal_error('unknown history option',assert_option(Option))).
59
60		:- volatile option/1.
61		:- dynamic option/1.
62		valid_option(show_init).
63		valid_option(show_states).
64		%valid_option(show_any_vars).
65
66
67		write_history :-
68		get_state_id_trace(StateIds),
69		op_trace_ids(OpIds), %print(Tuples),nl,
70		reverse(OpIds,ForwardOpIds),
71		%print(write(StateIds,ForwardOpIds)),nl,
72		write_history_state(StateIds,ForwardOpIds,not_initialized).
73
74		% alternate between writing states and operations
75		write_history_state([],Ops,LastStateInit) :- % we have reached the last state
76		(Ops=[] -> true ; add_internal_error('Extra ops: ',write_history_state([],Ops,LastStateInit))).
77		write_history_state([StateID|T],Ops,LastStateInit) :- %print(stateid(StateID)),nl,
78		(option(show_states)
79		-> write_state_id(StateID,Init)
80		; (option(show_init), LastStateInit=not_initialized)
81		-> write_state_id(StateID,Init)
82		; Init = initialized
83		),
84		write_history_op(Ops,T,StateID,Init).
85
86		% now write an operation, and then call write_history_state to print the next state
87		write_history_op([],States,_,_) :-
88		(States=[] -> true ; add_internal_error('Extra states: ',write_history_op([],States,_,_))).
89		write_history_op([OpID|T],States,StateID,Init) :- %print(op(OpID)),nl,
90		(OpID=jump(Dest)
91		-> hwrite('/* JUMPING TO ANOTHER STATE : '), hwrite(Dest), hwrite('*/\n')
92		% TO DO: check after jumping whether constants have changed in case states are written out
93		; transition(StateID,OperationTerm,OpID,_),
94		write_operation(OperationTerm,T)
95		),
96		write_history_state(States,T,Init).
97
98
99		write_state_id(root,Init) :- !, Init=not_initialized.
100		write_state_id(ID,Init) :- visited_expression(ID,S), write_state(S,Init),!.
101		write_state_id(ID,Init) :- add_internal_error('Failed: ',write_state_id(ID,Init)),
102		Init=initialized.
103
104		:- use_module(probsrc(specfile),[csp_mode/0, animation_mode/1]).
105		:- use_module(probsrc(translate),[translate_cspm_state/2]).
106		write_state(csp_and_b_root,Init) :- !, Init=not_initialized.
107		write_state(csp_and_b(_CSP,BState),Init) :- !, write_state(BState,Init).
108		write_state(concrete_constants(CstStore),not_initialized) :- write_store(CstStore,'Constants').
109		write_state(const_and_vars(_ID,VarStore),initialized) :- write_store(VarStore,'Variables').
110		write_state([],initialized) :- write_store([],'Variables').
111		write_state([H|T],initialized) :- write_store([H|T],'Variables').
112		write_state(CSP,initialized) :- csp_mode, translate_cspm_state(CSP,S),!,hwrite(S),hnl.
113		write_state(S,initialized) :- animation_mode(xtl),!,hwrite(S),hnl.
114
115		write_operation(F,_) :- functor(F,'$setup_constants',_),!.
116		write_operation(F,_) :- functor(F,'$initialise_machine',_),!,
117		((option(show_states) ; option(show_init)) -> hwrite('/* Initialisation */\n') ; true).
118		write_operation('$JUMP'(J),_) :- !, hwrite('/* JUMPING TO ANOTHER STATE : '),
119		hwrite(J), hwrite('*/\n').
120		write_operation(Operation,T) :- write_operation1(Operation),
121		(T==[] -> hnl ; hwrite(';\n')).
122		write_operation1(Operation) :-
123		(translate_event(Operation,OpStr) ->
124		hwrite(OpStr) ; add_internal_error('Failed: ',translate_event(Operation,_))).
125
126
127
128
129		write_store(Store,Info) :-
130		hwrite('/* '),hwrite(Info),hnl,
131		write_store2(Store),
132		hwrite('*/\n').
133		write_store2(Bindings) :- write_store3(Bindings,head).
134
135		:- use_module(bmachine,[b_is_variable/2, b_is_constant/2]).
136		write_store3([],_).
137		write_store3([bind(Name,Value)|Srest],Pos) :-
138		( Pos==head -> hwrite(' '); Pos==tail -> hwrite(' & ')),
139		hwrite(Name),hwrite(' = '),
140		((b_is_variable(Name,Type) ; b_is_constant(Name,Type)) % what about constants ?
141		-> translate_bvalue_with_type(Value,Type,ValStr)
142		; translate_bvalue(Value,ValStr)),
143		hwrite(ValStr),hnl,
144		write_store3(Srest,tail).
145
146
147
148		% catch exception to allow to call write_history directly and write to user_output
149		hwrite(X) :-
150		catch(
151		write(histout,X),
152		error(domain_error(stream_or_alias,histout),_),
153		write(user_output,X)).
154		hnl :-
155		catch(
156		nl(histout),
157		error(domain_error(stream_or_alias,histout),_),
158		nl(user_output)).
159
160		% write all values of variables and constants of all discovered states to files in directly
161		% failure driven loop over all discovered states
162		write_all_values_to_dir(Directory) :-
163		visited_expression(ID,Store),
164		ajoin([ID,'.txt'],Path),
165		absolute_file_name(Path, AbsolutePath, [relative_to(Directory)]),
166		write_values_to_file(AbsolutePath,Store),
167		fail.
168		write_all_values_to_dir(_).
169
170		% write all values of variables and constants to a file
171		write_values_to_file(Filename) :-
172		current_expression(_,CurStore),
173		write_values_to_file(Filename,CurStore).
174
175		:- use_module(probsrc(preferences),[temporary_set_preference/3, reset_temporary_preference/2]).
176		write_values_to_file(Filename,Store) :-
177		safe_intelligent_open_file(Filename,write,_,[alias(histout)]),
178		temporary_set_preference(expand_avl_upto,-1,Chng), % means no limit
179		call_cleanup(write_all_values(Store),
180		(safe_intelligent_close_file(Filename,histout),
181		reset_temporary_preference(expand_avl_upto,Chng))).
182
183		write_all_values(Store) :-
184		expand_to_constants_and_variables(Store,ConstStore,VarStore),
185		(ConstStore = [] -> H=head ; hwrite('/* Constants */\n'), write_store2(ConstStore),H=tail),
186		(VarStore = [] -> true ; hwrite('/* Variables */\n'), write_store3(VarStore,H)).