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)). |