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