1 % (c) 2009-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- 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 ; add_internal_error('Inconsistent history, transition does not exist:',
96 transition(StateID,_,OpID,_)),fail
97 ),
98 write_history_state(States,T,Init).
99
100
101 write_state_id(root,Init) :- !, Init=not_initialized.
102 write_state_id(ID,Init) :- visited_expression(ID,S), write_state(S,Init),!.
103 write_state_id(ID,Init) :- add_internal_error('Failed: ',write_state_id(ID,Init)),
104 Init=initialized.
105
106 :- use_module(probsrc(specfile),[csp_mode/0, animation_mode/1]).
107 :- use_module(probsrc(translate),[translate_cspm_state/2]).
108 write_state(csp_and_b_root,Init) :- !, Init=not_initialized.
109 write_state(csp_and_b(_CSP,BState),Init) :- !, write_state(BState,Init).
110 write_state(concrete_constants(CstStore),not_initialized) :- write_store(CstStore,'Constants').
111 write_state(const_and_vars(_ID,VarStore),initialized) :- write_store(VarStore,'Variables').
112 write_state([],initialized) :- write_store([],'Variables').
113 write_state([H|T],initialized) :- write_store([H|T],'Variables').
114 write_state(CSP,initialized) :- csp_mode, translate_cspm_state(CSP,S),!,hwrite(S),hnl.
115 write_state(S,initialized) :- animation_mode(xtl),!,hwrite(S),hnl.
116
117 write_operation(F,_) :- functor(F,'$setup_constants',_),!.
118 write_operation(F,_) :- functor(F,'$initialise_machine',_),!,
119 ((option(show_states) ; option(show_init)) -> hwrite('/* Initialisation */\n') ; true).
120 write_operation('$JUMP'(J),_) :- !, hwrite('/* JUMPING TO ANOTHER STATE : '),
121 hwrite(J), hwrite('*/\n').
122 write_operation(Operation,T) :- write_operation1(Operation),
123 (T==[] -> hnl ; hwrite(';\n')).
124 write_operation1(Operation) :-
125 (translate_event(Operation,OpStr) ->
126 hwrite(OpStr) ; add_internal_error('Failed: ',translate_event(Operation,_))).
127
128
129
130
131 write_store(Store,Info) :-
132 hwrite('/* '),hwrite(Info),hnl,
133 write_store2(Store),
134 hwrite('*/\n').
135 write_store2(Bindings) :- write_store3(Bindings,head).
136
137 :- use_module(bmachine,[b_is_variable/2, b_is_constant/2]).
138 write_store3([],_).
139 write_store3([bind(Name,Value)|Srest],Pos) :-
140 ( Pos==head -> hwrite(' '); Pos==tail -> hwrite(' & ')),
141 hwrite(Name),hwrite(' = '),
142 ((b_is_variable(Name,Type) ; b_is_constant(Name,Type)) % what about constants ?
143 -> translate_bvalue_with_type(Value,Type,ValStr)
144 ; translate_bvalue(Value,ValStr)),
145 hwrite(ValStr),hnl,
146 write_store3(Srest,tail).
147
148
149
150 % catch exception to allow to call write_history directly and write to user_output
151 hwrite(X) :-
152 catch(
153 write(histout,X),
154 error(domain_error(stream_or_alias,histout),_),
155 write(user_output,X)).
156 hnl :-
157 catch(
158 nl(histout),
159 error(domain_error(stream_or_alias,histout),_),
160 nl(user_output)).
161
162 % write all values of variables and constants of all discovered states to files in directly
163 % failure driven loop over all discovered states
164 write_all_values_to_dir(Directory) :-
165 visited_expression(ID,Store),
166 ajoin([ID,'.txt'],Path),
167 absolute_file_name(Path, AbsolutePath, [relative_to(Directory)]),
168 write_values_to_file(AbsolutePath,Store),
169 fail.
170 write_all_values_to_dir(_).
171
172 % write all values of variables and constants to a file
173 write_values_to_file(Filename) :-
174 current_expression(_,CurStore),
175 write_values_to_file(Filename,CurStore).
176
177 :- use_module(probsrc(preferences),[temporary_set_preference/3, reset_temporary_preference/2]).
178 write_values_to_file(Filename,Store) :-
179 safe_intelligent_open_file(Filename,write,_,[alias(histout)]),
180 temporary_set_preference(expand_avl_upto,-1,Chng), % means no limit
181 call_cleanup(write_all_values(Store),
182 (safe_intelligent_close_file(Filename,histout),
183 reset_temporary_preference(expand_avl_upto,Chng))).
184
185 write_all_values(Store) :-
186 expand_to_constants_and_variables(Store,ConstStore,VarStore),
187 (ConstStore = [] -> H=head ; hwrite('/* Constants */\n'), write_store2(ConstStore),H=tail),
188 (VarStore = [] -> true ; hwrite('/* Variables */\n'), write_store3(VarStore,H)).