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 | :- module(state_viewer_images,[tcltk_get_image_list/6, | |
5 | ||
6 | tcltk_can_react_to_item_right_click/2, | |
7 | tcltk_react_to_item_right_click/2, | |
8 | ||
9 | tcltk_can_react_to_item_drag/3, | |
10 | tcltk_react_to_item_drag/2, | |
11 | ||
12 | get_animation_images/1, % only get animation image list | |
13 | get_animation_image_grid/6, | |
14 | get_react_to_item_right_click_options/4, | |
15 | react_to_item_right_click/6, | |
16 | ||
17 | html_print_history/1, html_print_history/2 | |
18 | ]). | |
19 | ||
20 | /* ------------------------------------------------------------------ */ | |
21 | ||
22 | :- use_module(module_information). | |
23 | :- module_info(group,visualization). | |
24 | :- module_info(description,'This module can provide a Tk graphical representation of a B state.'). | |
25 | ||
26 | ||
27 | ||
28 | :- use_module(bmachine,[b_get_machine_animation_function/2, | |
29 | b_get_definition_string_from_machine/2, | |
30 | get_animation_image/2]). | |
31 | ||
32 | /* First argument: image list of pairs: ImageName, ImageFilePath | |
33 | Second argument: list of triplets {type framename label} | |
34 | */ | |
35 | ||
36 | :- use_module(error_manager). | |
37 | :- use_module(debug). | |
38 | :- use_module(state_space,[current_expression/2]). | |
39 | ||
40 | ||
41 | eval_definition_funs([],_,[]). | |
42 | eval_definition_funs([anim_fun(_Nr,AnimFunction1)|T],BState,Result) :- | |
43 | eval_definition_fun(AnimFunction1, BState, FunctionRes1), | |
44 | eval_definition_funs(T,BState,FunctionRes0), | |
45 | override_anim_fun(FunctionRes1,FunctionRes0,Result). | |
46 | ||
47 | :- use_module(xtl_interface,[xtl_animation_function_result/2, xtl_animation_image/2]). | |
48 | :- use_module(specfile,[animation_mode/1, b_or_z_mode/0]). | |
49 | ||
50 | ||
51 | tcltk_get_image_list(list(ImageList),MinRow,MaxRow,MinCol,MaxCol,list(FramesAndItems)) :- | |
52 | animation_mode(Mode), | |
53 | get_animation_images(Mode,ImageList), | |
54 | current_expression(_CurID,State), | |
55 | evaluate_animation_function(Mode,State,FunctionRes), | |
56 | get_min_max_col(FunctionRes,MinCol,MaxCol), | |
57 | display_animation_function_result(FunctionRes,MinRow,MaxRow,FramesAndItems). | |
58 | ||
59 | :- use_module(specfile,[state_corresponds_to_fully_setup_b_machine/2]). | |
60 | ||
61 | evaluate_animation_function(xtl,State,FunctionRes) :- !, | |
62 | xtl_animation_function_result(State,FunctionRes). | |
63 | evaluate_animation_function(_,State,FunctionRes) :- % Mode will be 'b' | |
64 | state_corresponds_to_fully_setup_b_machine(State,BState), | |
65 | findall(anim_fun(Nr,AF),b_get_machine_animation_function(AF,Nr),AnimFuns), | |
66 | AnimFuns \= [], | |
67 | sort(AnimFuns,SAnimFuns), | |
68 | %print(animation_images(ImageList)), | |
69 | % print('Animation Function: '), | |
70 | % translate:print_bexpr(SAnimFuns), | |
71 | eval_definition_funs(SAnimFuns, BState, FunctionRes). | |
72 | % print('full_fun'(FunctionRes)),nl. | |
73 | ||
74 | display_animation_function_result(FunctionRes,MinRow,MaxRow,FramesAndItems) :- | |
75 | get_min_max_row(FunctionRes,MinRow,MaxRow), | |
76 | debug_println(9,visualization_matrix_min_max(MinRow,MaxRow)), | |
77 | setup_frames(MinRow,MaxRow,Frames), %debug_println(9,frames(Frames)), | |
78 | sort(FunctionRes,SortedFR), | |
79 | get_frame_items(SortedFR,Items), | |
80 | % print(items(Items)),nl, | |
81 | pad_text_frame_items(Items,PItems), | |
82 | append(Frames,PItems,FramesAndItems). | |
83 | ||
84 | ||
85 | :- use_module(tools,[ split_last/4, split_chars/3 ]). | |
86 | tcltk_can_react_to_item_right_click(TkPath,list(Names)) :- | |
87 | convert_tk_path_to_coordinates(TkPath,XCoord,YCoord), | |
88 | animation_mode(M), | |
89 | current_state_id(CurID), | |
90 | debug_println(19,start_right_clicked_object(XCoord,YCoord,mode(M),state(CurID))), | |
91 | findall(Name,can_react_to_item_right_click(CurID,M,XCoord,YCoord,_,Name,_),Names). | |
92 | ||
93 | % for ProB 2: | |
94 | get_react_to_item_right_click_options(CurID,XCoord,YCoord,Names) :- | |
95 | animation_mode(M), | |
96 | findall(Name,can_react_to_item_right_click(CurID,M,XCoord,YCoord,_,Name,_),Names). | |
97 | ||
98 | tcltk_react_to_item_right_click(TkPath,ActionStr) :- | |
99 | % print(right_clicked_tk_path(TkPath)),nl, | |
100 | convert_tk_path_to_coordinates(TkPath,XCoord,YCoord), | |
101 | current_state_id(CurID), | |
102 | react_to_item_right_click(CurID,XCoord,YCoord,ActionStr,_,_). | |
103 | ||
104 | :- use_module(state_space,[current_state_id/1, transition/4]). | |
105 | :- use_module(xtl_interface,[xtl_animation_image_right_click_transition/3]). | |
106 | :- use_module(translate,[translate_event_with_src_and_target_id/4]). | |
107 | :- use_module(bmachine,[b_get_definition/5,type_with_errors/4]). | |
108 | :- use_module(library(lists),[maplist/3]). | |
109 | :- use_module(preferences,[temporary_set_preference/3,reset_temporary_preference/2]). | |
110 | ||
111 | can_react_to_item_right_click(CurID,Mode,X,Y,TransitionTemplateList,Str,TransitionID) :- | |
112 | get_right_click_template(Mode,CurID,X,Y,TransitionTemplateList), | |
113 | get_template(TransitionTemplateList,Template), % deals with list templates | |
114 | transition(CurID,TransitionTerm,TransitionID,DestID), | |
115 | match_template(Template,TransitionTerm), | |
116 | translate_event_with_src_and_target_id(TransitionTerm,CurID,DestID,Str). | |
117 | ||
118 | match_template(T,T) :- !. | |
119 | match_template(Template,Action) :- | |
120 | atom(Template), % with get_preference(show_eventb_any_arguments,true) we have extra arguments | |
121 | functor(Action,Template,_). | |
122 | ||
123 | get_right_click_template(xtl,_,ColX,RowY,Template) :- | |
124 | xtl_animation_image_right_click_transition(RowY,ColX,Template). | |
125 | get_right_click_template(b,CurID,X,Y,Template) :- | |
126 | Def_Name = 'ANIMATION_RIGHT_CLICK', | |
127 | b_get_definition(Def_Name,substitution,[_,_],RawSubst,_Deps), | |
128 | arg(1,RawSubst,Pos), | |
129 | temporary_set_preference(allow_local_operation_calls,true,CHNG), | |
130 | Scope = [prob_ids(visible),operation_bodies], % do not include variables; otherwise clash warnings | |
131 | % type definition call: | |
132 | type_with_errors(definition(Pos,'ANIMATION_RIGHT_CLICK',[integer(Pos,X),integer(Pos,Y)]),Scope,subst,Typed), | |
133 | reset_temporary_preference(allow_local_operation_calls,CHNG), | |
134 | get_b_template_for(CurID,Typed,[],Template). | |
135 | ||
136 | % ANIMATION_RIGHT_CLICK can use the following in B: | |
137 | % ANY, LET: to introduce wild cards; predicates will not (yet) be evaluated !! | |
138 | % IF-ELSIF-ELSE: conditions have to be evaluable using the parameters only | |
139 | % CHOICE: to provide multiple right click actions | |
140 | ||
141 | % Operation Calls: the arguments must evaluable without access to variables and constants at the moment | |
142 | ||
143 | :- use_module(specfile, [state_corresponds_to_set_up_constants/2]). | |
144 | get_b_template_for(CurID,Subst,LV,Template) :- | |
145 | visited_expression(CurID,State), | |
146 | state_corresponds_to_set_up_constants(State,BState), | |
147 | % expand_const_and_vars_to_full_store | |
148 | get_b_template(Subst,LV,BState,Template). | |
149 | ||
150 | ||
151 | get_b_template(b(E,subst,_),LocalVars,State,Template) :- get_b_template_aux(E,LocalVars,State,Template). | |
152 | ||
153 | :- use_module(bsyntaxtree, [get_texpr_id/2, def_get_texpr_id/2]). | |
154 | get_b_template_aux(any(Paras,_Pred,Body),LocalVars,State,Template) :- !, | |
155 | append(Paras,LocalVars,LV2), | |
156 | get_b_template(Body,LV2,State,Template). | |
157 | get_b_template_aux(let(Paras,_Pred,Body),LocalVars,State,Template) :- !, | |
158 | append(Paras,LocalVars,LV2), | |
159 | get_b_template(Body,LV2,State,Template). | |
160 | get_b_template_aux(choice(Options),LocalVars,State,Template) :- !, | |
161 | member(A,Options), | |
162 | get_b_template(A,LocalVars,State,Template). | |
163 | get_b_template_aux(if(Options),LocalVars,State,Template) :- !, | |
164 | get_b_template_for_if(Options,LocalVars,State,Template). | |
165 | get_b_template_aux(operation_call(TOpID,_Result,Parameters),LocalVars,State,Template) :- !, | |
166 | def_get_texpr_id(TOpID,op(OpID)), | |
167 | % TO DO: deal with Result | |
168 | maplist(eval_parameter(LocalVars,State),Parameters,TemplateArgs), | |
169 | Template =.. [OpID|TemplateArgs]. | |
170 | get_b_template_aux(Subst,_LocalVars,_State,_) :- | |
171 | add_error('ANIMATION_RIGHT_CLICK','Uncovered substitution: ',Subst),fail. | |
172 | ||
173 | :- use_module(b_interpreter,[b_test_boolean_expression_wf/3, b_compute_expression_nowf/4]). | |
174 | get_b_template_for_if([b(if_elsif(Test,Body),_,_)|_], LocalVars,State,Template) :- | |
175 | b_test_boolean_expression_wf(Test,[],State),!, | |
176 | get_b_template(Body,LocalVars,State,Template). | |
177 | get_b_template_for_if([_|T],LV,State,Template) :- get_b_template_for_if(T,LV,State,Template). | |
178 | ||
179 | eval_parameter(LocalVars,_State,Parameter,Result) :- | |
180 | get_texpr_id(Parameter,PID), | |
181 | member(LV,LocalVars), get_texpr_id(LV,PID), | |
182 | !, | |
183 | Result = _. | |
184 | eval_parameter(_LocalVars,State,Parameter,Result) :- | |
185 | b_compute_expression_nowf(Parameter,[],State,Result). | |
186 | ||
187 | ||
188 | react_to_item_right_click(CurID,X,Y,ActionStr,ResTransitionID,ResNewID) :- % print(react(CurID,X,Y,ActionStr)),nl, | |
189 | animation_mode(Mode), | |
190 | ( can_react_to_item_right_click(CurID,Mode,X,Y,TransitionTemplateList,ActionStr,TransitionID), | |
191 | get_template(TransitionTemplateList,TransitionTemplate), | |
192 | user:tcltk_perform_action(CurID,TransitionTerm,TransitionID,NewID), | |
193 | match_template(TransitionTemplate,TransitionTerm) | |
194 | -> format('Performed: ~w~n',[TransitionTemplate]), | |
195 | (get_template_rest(TransitionTemplateList,Rest) | |
196 | -> % there are other actions to execute (automatically after a user-click; useful for chess,...) | |
197 | execute_rest(Rest,TT), % currently only happens in XTL mode | |
198 | ResTransitionID = [TransitionID|TT], ResNewID = unknown | |
199 | % NewID points to first NewID, not to target; TO DO: modify command in case we support XTL in ProB2 UI | |
200 | ; ResTransitionID = TransitionID, ResNewID=NewID | |
201 | ) | |
202 | ; format('Cannot execute transition ~w~n Right-Click on (~w,~w)~n',[ActionStr,X,Y]), | |
203 | fail | |
204 | ). | |
205 | ||
206 | % note: a single click is also a item_drag from an object to itself | |
207 | tcltk_can_react_to_item_drag(FromTkPath,ToTkPath,Image) :- | |
208 | animation_mode(M), | |
209 | convert_tk_path_to_coordinates(FromTkPath,FromX,FromY), | |
210 | convert_tk_path_to_coordinates(ToTkPath,ToX,ToY), | |
211 | can_react_to_item_drag(M,FromX,FromY,ToX,ToY,ImageNr), | |
212 | (ImageNr=none -> Image='' | |
213 | ; get_animation_image_and_label(M,ImageNr,_,Lbl) -> Image=Lbl | |
214 | ; Image=''). | |
215 | ||
216 | tcltk_react_to_item_drag(FromTkPath,ToTkPath) :- | |
217 | convert_tk_path_to_coordinates(FromTkPath,FromX,FromY), | |
218 | convert_tk_path_to_coordinates(ToTkPath,ToX,ToY), | |
219 | debug_println(20,dragged_object(FromX,FromY,ToX,ToY)), | |
220 | animation_mode(M), | |
221 | react_to_item_drag(M,FromX,FromY,ToX,ToY). | |
222 | ||
223 | :- use_module(xtl_interface,[xtl_animation_image_click_transition/6]). | |
224 | can_react_to_item_drag(Mode,FromX,FromY,ToX,ToY,ImageNr) :- | |
225 | current_state_id(CurID), | |
226 | get_item_drag_template_and_image(Mode,FromX,FromY,ToX,ToY,TransitionTemplateList,ImageNr), | |
227 | get_template(TransitionTemplateList,TransitionTemplate), | |
228 | transition(CurID,TransitionTemplate,_ActId,_DestID). | |
229 | ||
230 | % transition templates can also be lists; we just check if first action is feasible | |
231 | get_template([H|_],Template) :- !, % in XTL mode we allow lists of actions | |
232 | Template=H. | |
233 | get_template(Template,Template). % in B,TLA,Z,... mode we only execute a single event | |
234 | ||
235 | get_template_rest([_|T],T). | |
236 | ||
237 | get_item_drag_template_and_image(xtl,ColFromX,RowFromY,ToX,ToY,TransitionTemplate,ImageNr) :- !, | |
238 | xtl_animation_image_click_transition(RowFromY,ColFromX,ToY,ToX,TransitionTemplate,ImageNr). | |
239 | get_item_drag_template_and_image(b,FromX,FromY,ToX,ToY,Template,1000) :- | |
240 | % TO DO: provide a way to return image number | |
241 | Def_Name = 'ANIMATION_CLICK', | |
242 | b_get_definition(Def_Name,substitution,ARGS,RawSubst,_Deps), | |
243 | arg(1,RawSubst,Pos), | |
244 | (ARGS = [_,_,_,_] -> true % we need four arguments | |
245 | ; add_warning(state_viewer_images,'DEFINITION needs four arguments: ','ANIMATION_CLICK',Pos),fail | |
246 | ), | |
247 | temporary_set_preference(allow_local_operation_calls,true,CHNG), | |
248 | Scope = [prob_ids(visible),operation_bodies], % do not include variables; otherwise clash warnings; variables already included in operation_bodies | |
249 | type_with_errors(definition(Pos,'ANIMATION_CLICK', | |
250 | [integer(Pos,FromX),integer(Pos,FromY),integer(Pos,ToX),integer(Pos,ToY)]),Scope,subst,Typed), | |
251 | reset_temporary_preference(allow_local_operation_calls,CHNG), | |
252 | State = [], % TO DO: get full state like for right click | |
253 | get_b_template(Typed,[],State,Template). | |
254 | ||
255 | react_to_item_drag(Mode,FromX,FromY,ToX,ToY) :- | |
256 | get_item_drag_template_and_image(Mode,FromX,FromY,ToX,ToY,Templ1,_), | |
257 | !, | |
258 | ((get_item_drag_template_and_image(Mode,FromX,FromY,ToX,ToY,TransitionTemplateList,_), | |
259 | get_template(TransitionTemplateList,TransitionTemplate), | |
260 | user:tcltk_perform_action(TransitionTemplate,_)) | |
261 | -> (get_template_rest(TransitionTemplateList,Rest) | |
262 | -> % there are other actions to execute | |
263 | execute_rest(Rest,_) | |
264 | ; true | |
265 | ) | |
266 | ; format('Cannot execute transition ~w~n Mouse Drag (~w,~w)->(~w,~w)~n',[Templ1,FromX,FromY,ToX,ToY]), | |
267 | fail | |
268 | ). | |
269 | react_to_item_drag(_,_,_,_,_) :- fail. | |
270 | ||
271 | % execute remaining templates of action | |
272 | execute_rest([],Res) :- !, Res=[]. | |
273 | execute_rest([H|T],[TransitionID|TT]) :- !, | |
274 | current_state_id(CurID), %print(try_auto_play(CurID,H)),nl, | |
275 | user:compute_all_transitions_if_necessary, | |
276 | current_state_id(CurID), | |
277 | user:tcltk_perform_action(CurID,H,TransitionID,_NewID), %print(perf(H,_NewID)),nl, | |
278 | execute_rest(T,TT). | |
279 | execute_rest(T,[]) :- format('~n*** Cannot execute rest of transition template ~w~n',[T]). | |
280 | ||
281 | % if successful convert a Tk Widget Path like .stateviewer.sviewFrame.frame1.item1_3 | |
282 | % to coordinates of the state_viewer module: (1,3) | |
283 | convert_tk_path_to_coordinates(TkPath,XCoord,YCoord) :- | |
284 | split_last(TkPath,'.',_,NameOfItemClicked), | |
285 | atom_codes(NameOfItemClicked,Codes), | |
286 | get_suffix(Codes,Rest), | |
287 | !, | |
288 | split_chars(Rest,"_",[YCC,XCC]), % note: coordinates reversed in label | |
289 | number_codes(XCoord,XCC), | |
290 | number_codes(YCoord,YCC). | |
291 | convert_tk_path_to_coordinates(TkPath,_,_) :- format('*** Cannot convert TkPath ~w~n',[TkPath]),fail. | |
292 | ||
293 | get_suffix(Codes,Rest) :- append("item",Rest,Codes),!. | |
294 | get_suffix(Codes,Rest) :- append("text",Rest,Codes),!. | |
295 | get_suffix(Codes,Rest) :- append("frame",Rest,Codes),!. | |
296 | ||
297 | :- use_module(custom_explicit_sets,[try_expand_custom_set/2, is_set_value/2]). | |
298 | ||
299 | eval_definition_fun(AnimFunction,BState, FunctionRes) :- | |
300 | on_enumeration_warning( | |
301 | b_interpreter:b_compute_expression_nowf(AnimFunction,[],BState,FunctionResCl), | |
302 | fail), | |
303 | %% nl, print('FunctionResult'(FunctionResCl)),nl, | |
304 | is_set_value(FunctionResCl,eval_definition_fun), | |
305 | try_expand_custom_set(FunctionResCl, ExpCl), | |
306 | (translate_to_ints(ExpCl, FunctionRes) | |
307 | -> true /* already translate to ints so that override will work properly */ | |
308 | ; check_anim_function(ExpCl),fail | |
309 | ) % ,print('fres'(FunctionRes)),nl | |
310 | . | |
311 | ||
312 | check_anim_function([]) :- !. | |
313 | %check_anim_function(int(_)) :- !. % just a single picture; now gets converted by translate_to_ints | |
314 | check_anim_function([H|_]) :- !, | |
315 | (H = (RowCol,_Img), get_pair(RowCol,Row,Col) -> | |
316 | ((get_int(Row,_),get_int(Col,_) -> true | |
317 | ; add_error(state_viewer_images,'Elements of ANIMATION_FUNCTION should be convertible to (INT*INT)*INT: ',H)) | |
318 | ) | |
319 | ; H = (Row,ColImg), get_pair(ColImg,Col,_Img) -> | |
320 | ((get_int(Row,_),get_int(Col,_) -> true | |
321 | ; add_error(state_viewer_images,'Elements of ANIMATION_FUNCTION should be convertible to INT*(INT*INT): ',H)) | |
322 | ) | |
323 | ; add_error(state_viewer_images, | |
324 | 'Elements of the ANIMATION_FUNCTION should be of type (INT*INT)*INT: ',H) | |
325 | ). | |
326 | check_anim_function((A,B)) :- !, | |
327 | add_error(state_viewer_images,'ANIMATION_FUNCTION should be a set of pairs, not a pair: ',(A,B)). | |
328 | check_anim_function(X) :- !, | |
329 | add_error(state_viewer_images,'ANIMATION_FUNCTION should be of type (INT*INT) +-> INT (or similar): ',X). | |
330 | ||
331 | :- use_module(library(avl)). | |
332 | ||
333 | translate_to_ints(In,Out) :- empty_avl(E),translate_to_ints(In,E,Out). | |
334 | translate_to_ints([],_,[]) :-!. | |
335 | translate_to_ints(X,_,Res) :- get_int(X,IX),!,Res=[((1,1),int(IX))]. % a single picture | |
336 | translate_to_ints([H|T], AVL, Res) :- | |
337 | translate_element(H,AVL, NewAVL, Res, NewRes), | |
338 | translate_to_ints(T,NewAVL,NewRes). | |
339 | ||
340 | translate_element((RowCol,Img),AVL, NewAVL, Res, NewRes) :- get_pair(RowCol,Row,Col),!, | |
341 | get_int(Row,RI), get_int(Col,CI), (Img=II), | |
342 | add_image(RI,CI,II, AVL, NewAVL, Res, NewRes). | |
343 | translate_element((Row,ColImg),AVL, NewAVL, Res, NewRes) :- get_pair(ColImg,Col,Img),!, | |
344 | translate_element(((Row,Col),Img), AVL, NewAVL, Res, NewRes). | |
345 | translate_element((Row,Set),AVL,NewAVL,Res,NewRes) :- % Set can be relation or sequence | |
346 | % expand Set and associate elements with Row | |
347 | is_set_value(Set,translate_element), | |
348 | try_expand_custom_set(Set, ESet), | |
349 | findall((Row,El),member(El,ESet),All), | |
350 | l_translate(All,AVL,NewAVL,Res,NewRes). | |
351 | ||
352 | ||
353 | ||
354 | l_translate([],AVL,AVL,Res,Res). | |
355 | l_translate([H|T],AVL,NewAVL,Res,NewRes) :- translate_element(H,AVL,NewAVL1,Res,NewRes1), | |
356 | l_translate(T,NewAVL1,NewAVL,NewRes1,NewRes). | |
357 | ||
358 | add_image(RI,CI,II, AVL, NewAVL, Res, NewRes) :- | |
359 | (avl_fetch((RI,CI),AVL,ExistingValue) | |
360 | -> add_error(state_viewer_images, | |
361 | 'Animation function defines two images for (Row,Col):[img1,img2] = ',((RI,CI):[ExistingValue,II])), | |
362 | NewAVL = AVL, Res=NewRes | |
363 | ; avl_store((RI,CI),AVL,II,NewAVL), Res=[((RI,CI),II)|NewRes] | |
364 | ). | |
365 | ||
366 | /* a version of override which does not worry about correct typing */ | |
367 | % override_anim_fun(Fun1, Fun2, Res) :: Fun2 overrides Fun1 | |
368 | override_anim_fun([],Fun2,Res) :- !, Res=Fun2. | |
369 | override_anim_fun(int(_),Fun2,Res) :- !, Res=Fun2. | |
370 | override_anim_fun([((RowT,Col),Img)|T],Fun2,Res) :- !, | |
371 | (member(((RowT,Col),_),Fun2) | |
372 | -> Res = ResT % we use version from Fun2 | |
373 | ; Res = [((RowT,Col),Img)|ResT] | |
374 | ), override_anim_fun(T,Fun2,ResT). | |
375 | override_anim_fun(X,F,R) :- | |
376 | add_error(state_viewer_images,'Unknown Format for ANIMATION_FUNCTION_DEFAULT', X), | |
377 | R=F. | |
378 | ||
379 | % get minimum and maximum index for rows | |
380 | get_min_max_row([((Row,_Col),_Img)|T],Min,Max) :- !, | |
381 | number(Row), % this is already in a format for Tcl/Tk; not int(.) | |
382 | get_min_max_row2(T,Row,Row,Min,Max). | |
383 | get_min_max_row([],_,_) :- !, | |
384 | print('**** Empty ANIMATION_FUNCTION result'),nl, fail. | |
385 | get_min_max_row(Res,_,_) :- | |
386 | add_error(state_viewer_images, | |
387 | 'Unknown Format for ANIMATION_FUNCTION result, must be of type INT or (INT*INT)+->INT',Res), | |
388 | fail. | |
389 | ||
390 | get_min_max_row2([],Min,Max,Min,Max). | |
391 | get_min_max_row2([((Row,_Col),_Img)|T],Min,Max,MinR,MaxR) :- | |
392 | (Row<Min -> Min1=Row ; Min1=Min), | |
393 | (Row>Max -> Max1=Row ; Max1=Max), | |
394 | get_min_max_row2(T,Min1,Max1,MinR,MaxR). | |
395 | ||
396 | % get minimum and maximum index for columns | |
397 | get_min_max_col([((_Row,Col),_Img)|T],Min,Max) :- !, | |
398 | number(Col), % this is already in a format for Tcl/Tk; not int(.) | |
399 | get_min_max_col2(T,Col,Col,Min,Max). | |
400 | get_min_max_col2([],Min,Max,Min,Max). | |
401 | get_min_max_col2([((_Row,Col),_Img)|T],Min,Max,MinR,MaxR) :- | |
402 | (Col<Min -> Min1=Col ; Min1=Min), | |
403 | (Col>Max -> Max1=Col ; Max1=Max), | |
404 | get_min_max_col2(T,Min1,Max1,MinR,MaxR). | |
405 | ||
406 | get_int(Nr,R) :- number(Nr),!,R=Nr. | |
407 | get_int(int(R),R). | |
408 | get_int(fd(R,_Name),R). | |
409 | get_int(pred_true /* bool_true */,1). | |
410 | get_int(pred_false /* bool_false */,0). | |
411 | /* can sometimes do unwanted conversions and show images where we do not want them: | |
412 | get_int(string(A),Integer) :- % convert something like "Train1" -> 1 | |
413 | atom_codes(A,Codes), reverse(Codes,RC), | |
414 | get_number_prefix(RC,Prefix), | |
415 | Prefix \= [], reverse(Prefix,RP), | |
416 | number_codes(Integer,RP). | |
417 | ||
418 | get_number_prefix([N|T],[N|RT]) :- N >= 48, N =< 57, % Ascii of a digit 0-9 | |
419 | !, get_number_prefix(T,RT). | |
420 | get_number_prefix(_,[]). | |
421 | */ | |
422 | ||
423 | get_pair((A,B),A,B). | |
424 | get_pair(avl_set(node((int(1),A),true,1,empty,node((int(2),B),true,0,empty,empty))),A,B). % in TLA: <<a,b>> sometimes translated as sequence | |
425 | ||
426 | ||
427 | :- use_module(bmachine,[b_get_true_expression_definition/1]). | |
428 | % add extra whitespace to make all text fields the same length | |
429 | % TO DO: maybe only pad within a column; not overall | |
430 | pad_text_frame_items(FrameItems,NewFrameItems) :- b_or_z_mode, | |
431 | (b_get_true_expression_definition('ANIMATION_STR_JUSTIFY_LEFT') ; | |
432 | b_get_true_expression_definition('ANIMATION_STR_JUSTIFY_RIGHT') ), | |
433 | longest_text(FrameItems,0,Len), | |
434 | Len>0, | |
435 | !, | |
436 | %print(longest(Len)),nl, | |
437 | pad_text_frame_items_to(FrameItems,Len,NewFrameItems). | |
438 | pad_text_frame_items(F,F). | |
439 | ||
440 | ||
441 | pad_text_frame_items_to([],_,[]). | |
442 | pad_text_frame_items_to([ItemLabel,Frame,Text|TR],Len,[ItemLabel,Frame,NewText|NTR]) :- | |
443 | (is_text_type(ItemLabel) | |
444 | -> atom_codes(Text,Codes), | |
445 | length(Codes,TLen), | |
446 | AdditionalSpaces is Len-TLen, gen_spaces(AdditionalSpaces,AS), | |
447 | (b_get_true_expression_definition('ANIMATION_STR_JUSTIFY_RIGHT') | |
448 | -> append(AS,Codes,NewCodes) | |
449 | ; append(Codes,AS,NewCodes) % 34 -> ' 39 -> " | |
450 | ), | |
451 | atom_codes(NewText,NewCodes) | |
452 | ; NewText=Text), | |
453 | pad_text_frame_items_to(TR,Len,NTR). | |
454 | ||
455 | gen_spaces(Nr,R) :- Nr<1,R=[]. % 34 -> ' | |
456 | gen_spaces(Nr,[32|T]) :- N1 is Nr-1, gen_spaces(N1,T). | |
457 | ||
458 | ||
459 | % find longest text label; so that we can pad the other ones with spaces | |
460 | longest_text([],R,R). | |
461 | longest_text([ItemLabel,_Frame,Text|TR],Acc,R) :- | |
462 | is_text_type(ItemLabel),!, | |
463 | atom_length(Text,Len), | |
464 | (Len>Acc -> NAcc = Len ; NAcc=Acc), | |
465 | longest_text(TR,NAcc,R). | |
466 | longest_text([_,_,_|TR],Acc,R) :- longest_text(TR,Acc,R). | |
467 | ||
468 | is_text_type(ItemLabel) :- atom_codes(ItemLabel,Codes), append("text",_,Codes). | |
469 | ||
470 | get_frame_items([],[]). | |
471 | get_frame_items([((Row,Col),Img)|T],[ItemLbl,FrameLbl,ImageLbl|TR]) :- | |
472 | convert_nr_into_tk_label(Row,"frame",FrameLbl), | |
473 | (get_int(Img,ImgNr),images(ImgNr,_,ImageLbl) | |
474 | -> convert_2nr_into_tk_label(Row,Col,"item",ItemLbl) | |
475 | ; convert_2nr_into_tk_label(Row,Col,"text",ItemLbl), | |
476 | (get_int(Img,ImgNr),get_animation_string(ImgNr,ImageLbl) -> true | |
477 | ; translate_value_for_tk_text(Img,ImageLbl) | |
478 | ) | |
479 | ), | |
480 | get_frame_items(T,TR). | |
481 | ||
482 | setup_frames(Min,Max,[]) :- Min>Max,!. | |
483 | setup_frames(Min,Max,[frame, FrameLbl, top |T]) :- | |
484 | convert_nr_into_tk_label(Min,"frame",FrameLbl), M1 is Min+1, | |
485 | setup_frames(M1,Max,T). | |
486 | ||
487 | :- dynamic images/3. | |
488 | ||
489 | ||
490 | get_animation_images(Mode,Res) :- clear_animation_images, | |
491 | findall( img(Nr,ImgFilename,Lbl), get_animation_image_and_label(Mode,Nr,ImgFilename,Lbl), List), | |
492 | flatten_img_list(List,Res). | |
493 | clear_animation_images :- retractall(images(_,_,_)). | |
494 | ||
495 | flatten_img_list([],[]). | |
496 | flatten_img_list([img(Nr,ImgFilename,Lbl)|T],[Lbl,ImgFilename|FT]) :- | |
497 | assert(images(Nr,ImgFilename,Lbl)), flatten_img_list(T,FT). | |
498 | ||
499 | ||
500 | get_animation_image_and_label(Mode,Nr,ImgFilename,Lbl) :- | |
501 | get_animation_image_in_mode(Mode,Nr,ImgFilename), | |
502 | convert_nr_into_tk_label(Nr,"IMG",Lbl). | |
503 | ||
504 | get_animation_image_in_mode(xtl,Nr,S) :- !, xtl_animation_image(Nr,S). | |
505 | get_animation_image_in_mode(b,Nr,S) :- !, get_animation_image(Nr,S). | |
506 | get_animation_image_in_mode(csp_and_b,Nr,S) :- get_animation_image(Nr,S). | |
507 | % csp not covered | |
508 | ||
509 | get_animation_string(Nr,S) :- b_or_z_mode, | |
510 | number_codes(Nr,TailCodes), | |
511 | /* ANIMATION_STR */ | |
512 | atom_codes(Def_Name,[65,78,73,77,65,84,73,79,78,95,83,84,82|TailCodes]), | |
513 | b_get_definition_string_from_machine(Def_Name,S). | |
514 | ||
515 | ||
516 | convert_nr_into_tk_label(Nr,Prefix,Label) :- number_codes(Nr,Codes), | |
517 | append(Prefix,Codes,C), | |
518 | atom_codes(Label,C). | |
519 | ||
520 | convert_2nr_into_tk_label(Nr1,Nr2,Prefix,Label) :- | |
521 | number_codes(Nr1,Codes1), number_codes(Nr2,Codes2), | |
522 | append("_",Codes2,C2), append(Codes1,C2,Codes), | |
523 | append(Prefix,Codes,C), | |
524 | atom_codes(Label,C). | |
525 | ||
526 | % -------------------------- | |
527 | ||
528 | % a function for Java FX or other graphical frameworks | |
529 | % | ?- get_animation_images(L). | |
530 | % L = [image_file(0,'images/empty_box_white.gif'),...,image_file(6,'images/F.gif')] ? | |
531 | ||
532 | get_animation_images(SList) :- | |
533 | animation_mode(Mode), | |
534 | findall( image_file(Nr,File), get_animation_image_in_mode(Mode,Nr,File), List), | |
535 | sort(List,SList). | |
536 | ||
537 | get_animation_image_numbers(SList) :- | |
538 | animation_mode(Mode), | |
539 | findall( Nr, get_animation_image_in_mode(Mode,Nr,_File), List), % TO DO: also get animation strings | |
540 | sort(List,SList). | |
541 | ||
542 | % a function for Java FX or other graphical frameworks | |
543 | % | ?- get_animation_image_grid(1,G,M,X). | |
544 | %G = [entry(1,1,image(0)),entry(1,2,image(0)),entry(1,3,image(0)),entry(1,4,image(0)),...,entry(Row,Col,image(...)),(...,...)|...], | |
545 | %M = 1, | |
546 | %X = 6 ? | |
547 | ||
548 | :- use_module(state_space,[visited_expression/2]). | |
549 | :- use_module(library(lists)). | |
550 | get_animation_image_grid(ID,Matrix,MinRow,MaxRow,MinCol,MaxCol) :- | |
551 | visited_expression(ID,State), | |
552 | animation_mode(Mode), | |
553 | evaluate_animation_function(Mode,State,FunctionRes), | |
554 | get_min_max_row(FunctionRes,MinRow,MaxRow), | |
555 | get_min_max_col(FunctionRes,MinCol,MaxCol), | |
556 | get_animation_image_numbers(ImageNumbers), | |
557 | maplist(convert_animation_function(Mode,ImageNumbers),FunctionRes,Matrix). | |
558 | ||
559 | ||
560 | :- use_module(library(ordsets),[ord_member/2]). | |
561 | :- use_module(library(codesio),[write_to_codes/2]). | |
562 | ||
563 | convert_animation_function(Mode,ImageNumbers,((Row,Col),Res), | |
564 | entry(Row,Col,TranslatedRes)) :- | |
565 | convert_aux(Mode,ImageNumbers,Res,TranslatedRes). | |
566 | convert_aux(_Mode,ImageNumbers,Img,image(ImgNr)) :- get_int(Img,ImgNr),ord_member(ImgNr,ImageNumbers),!. | |
567 | convert_aux(_Mode,_,Str,text(StringLbl)) :- get_int(Str,StrNr),get_animation_string(StrNr,StringLbl),!. | |
568 | convert_aux(b,_,Value,text(PPValue)) :- translate_value_for_tk_text(Value,PPValue),!. | |
569 | convert_aux(_,_,Value,text(AtomValue)) :- compound(Value), | |
570 | !, | |
571 | write_to_codes(Value,VC), atom_codes(AtomValue,VC). | |
572 | convert_aux(_,_,Value,text(Value)). | |
573 | ||
574 | translate_value_for_tk_text(string(Str),Res) :- !, % show string without quotes | |
575 | Res=Str. % TO DO: do we need to escape something here? | |
576 | translate_value_for_tk_text(Value,PPValue) :- translate:translate_bvalue(Value,PPValue),!. | |
577 | ||
578 | % export to HTML | |
579 | %html_print_animation_image_grid(ID) :- html_print_animation_image_grid(user_output,ID,''). | |
580 | ||
581 | html_print_animation_image_grid(Stream,ID,FilePrefix) :- | |
582 | get_animation_image_grid(ID,Matrix,MinRow,_MaxRow,_MinCol,_MaxCol), | |
583 | sort(Matrix,SortedMatrix), | |
584 | start_tag(Stream,table), | |
585 | start_tag(Stream,tr),animation_mode(Mode), | |
586 | html_print(SortedMatrix,Stream,MinRow,Mode,FilePrefix), | |
587 | end_tag(Stream,table). | |
588 | ||
589 | html_print([],Stream,_,_,_FilePrefix) :- end_tag(Stream,tr). | |
590 | html_print([entry(Row,_Col,Img)|T],Stream,LastRow,Mode,FilePrefix) :- | |
591 | (Row>LastRow -> end_tag(Stream,tr),start_tag(Stream,tr) ; true), | |
592 | % TO DO: insert empty cells when we jump over Columns | |
593 | html_image(Img,Stream,Mode,FilePrefix), | |
594 | html_print(T,Stream,Row,Mode,FilePrefix). | |
595 | ||
596 | html_image(image(ImgNr),Stream,Mode,FilePrefix) :- get_animation_image_in_mode(Mode,ImgNr,File),!, | |
597 | ((FilePrefix='' ; is_absolute_path(File)) | |
598 | -> format(Stream,' <th><img src="~w"></th>~n',[File]) | |
599 | ; format(Stream,' <th><img src="~w~w"></th>~n',[FilePrefix,File]) | |
600 | ). | |
601 | html_image(text(T),Stream,_,_) :- !, | |
602 | format(Stream,' <th><tt>~w</tt></th>~n',[T]). | |
603 | html_image(T,Stream,_,_) :- | |
604 | format(Stream,' <th>ERROR: ~w</th>~n',[T]). | |
605 | ||
606 | start_tag(Stream,T) :- format(Stream,'<~w>~n',[T]). | |
607 | end_tag(Stream,T) :- format(Stream,'</~w>~n',[T]). | |
608 | ||
609 | :- use_module(bmachine,[b_get_machine_animation_expression/1]). | |
610 | :- use_module(translate,[translate_bvalue/2,translate_bexpression/2]). | |
611 | html_print_animation_expression(Stream,StateID) :- | |
612 | get_animation_expression_label_and_value(StateID,S1,S2), | |
613 | format(Stream,'~w=~w~n',[S1,S2]). | |
614 | html_print_animation_expression(_,_). | |
615 | ||
616 | get_animation_expression_label_and_value(StateID,S1,S2) :- b_or_z_mode, | |
617 | b_get_machine_animation_expression(AExpr), | |
618 | visited_expression(StateID,State), | |
619 | state_corresponds_to_fully_setup_b_machine(State,BState), | |
620 | b_interpreter:b_compute_expression_nowf(AExpr,[],BState,AValue), | |
621 | translate_bexpression(AExpr,S1), | |
622 | translate_bvalue(AValue,S2). | |
623 | ||
624 | :- use_module(state_space, [transition/4,visited_expression/2, | |
625 | current_expression/2, current_state_id/1, | |
626 | get_action_term_trace/1, get_state_id_trace/1]). | |
627 | ||
628 | ||
629 | html_print_history(File) :- html_print_history(File,3). | |
630 | html_print_history(File,MaxOpDebugLevel) :- | |
631 | get_state_id_trace([root|StateIds]), | |
632 | get_action_term_trace(RAT), reverse(RAT,Actions), | |
633 | % TO DO: adapt path of images so that they work in File | |
634 | (currently_opened_file(SpecFile) | |
635 | -> get_parent_directory(SpecFile,SParent), | |
636 | absolute_file_name(SParent, SAbsParent), %, [relative_to(Directory)]), | |
637 | get_parent_directory(File,TParent), | |
638 | absolute_file_name(TParent, TAbsParent), %, [relative_to(Directory)]), | |
639 | compute_prefix(SAbsParent,TAbsParent,FilePrefix) | |
640 | ; SpecFile=unknown, FilePrefix='.'), | |
641 | open(File,write,Stream,[encoding('UTF-8')]), | |
642 | html_header(Stream,true), | |
643 | html_info(Stream,Actions,SpecFile), | |
644 | html_print_history2(Stream,1,Actions,StateIds,none,FilePrefix,MaxOpDebugLevel), | |
645 | html_footer(Stream), | |
646 | close(Stream). | |
647 | ||
648 | :- use_module(tools_strings,[ajoin_with_sep/3]). | |
649 | :- use_module(tools,[split_atom/3,is_absolute_path/1]). | |
650 | ||
651 | % compute a file prefix that needs to be added to relocate relative path for OldPath to paths for NewPath: | |
652 | compute_prefix(OldPath,NewPath,FilePrefix) :- | |
653 | %print(old(OldPath)),nl, print(new(NewPath)),nl, | |
654 | split_atom(OldPath,['/'],O1), | |
655 | split_atom(NewPath,['/'],N1), | |
656 | max_prefix(O1,N1,_CommonPrefix,O2,N2), %print(common(CommonPrefix)),nl, | |
657 | maplist(gendotdot,N2,N3), | |
658 | append(N3,O2,UpdatePath), | |
659 | (UpdatePath=[] -> FilePrefix = '' | |
660 | ; append(UpdatePath,[''],U1), | |
661 | ajoin_with_sep(U1,'/',FilePrefix)), | |
662 | debug_println(9,update_prefix_for_images(FilePrefix)). | |
663 | ||
664 | gendotdot(_,'..'). | |
665 | ||
666 | max_prefix([H|T],[H|T2],[H|PT],Suffix1,Suffix2) :- !, | |
667 | max_prefix(T,T2,PT,Suffix1,Suffix2). | |
668 | max_prefix(S1,S2,[],S1,S2). | |
669 | ||
670 | html_print_state(Stream,ID,FilePrefix) :- | |
671 | (html_print_animation_image_grid(Stream,ID,FilePrefix) | |
672 | -> true ; format(Stream,'No visualisation available for state id ~w~n',[ID])), | |
673 | html_print_animation_expression(Stream,ID). | |
674 | ||
675 | :- use_module(translate,[translate_event/2]). | |
676 | html_print_history2(_,_,[],[],_,_,_). | |
677 | html_print_history2(Stream,_,[],[ID|_],_,FilePrefix,_) :- | |
678 | html_print_state(Stream,ID,FilePrefix). | |
679 | html_print_history2(Stream,StepNr,[Action|AT],[ID|T],PreviousID,FilePrefix,MaxOpDebugLevel) :- | |
680 | translate_event(Action,AS), | |
681 | format(Stream,'~n~n<h2>~w. ~w</h2>~n',[StepNr,AS]), flush_output(Stream), | |
682 | html_print_action(Stream,Action,PreviousID,ID,MaxOpDebugLevel), | |
683 | html_print_state(Stream,ID,FilePrefix), | |
684 | S1 is StepNr+1, | |
685 | html_print_history2(Stream,S1,AT,T,ID,FilePrefix,MaxOpDebugLevel). | |
686 | ||
687 | :- use_module(specfile,[get_operation_name/2]). %get_operation_arguments | |
688 | :- use_module(bvisual2,[html_debug_operation_for_stateid/4]). | |
689 | html_print_action(Stream,Action,PreviousID,_ID,MaxLevel) :- | |
690 | MaxLevel > 0, PreviousID \= none, | |
691 | get_operation_name(Action,OpName), | |
692 | !, | |
693 | % print operation guards up to MaxLevel nesting, TODO: use parameter values for this action | |
694 | (html_debug_operation_for_stateid(Stream,OpName,PreviousID,MaxLevel) % fails for INITIALISATION, SETUP_CONSTANTS | |
695 | -> true | |
696 | ; true). %add_internal_error('Failed: ',html_debug_operation_for_stateid(OpName,ID,MaxLevel))). | |
697 | html_print_action(_,_,_,_,_). | |
698 | ||
699 | html_header(Stream,Border) :- | |
700 | format(Stream,'<html>~n<head>~n<style>~ntable, th, td {~n',[]), | |
701 | (Border=true -> format(Stream,' border: 1px solid black;~n',[]) ; true), | |
702 | format(Stream,' border-collapse: collapse;~n}~nth, td {~n padding: 0px;~n}~n</style>~n</head>~n<body>',[]). | |
703 | ||
704 | ||
705 | html_footer(Stream) :- | |
706 | format(Stream,'</body>~n</html>~n',[]). | |
707 | ||
708 | :- use_module(version, [version_str/1, revision/1, lastchangeddate/1]). | |
709 | :- use_module(library(system),[ datime/1]). | |
710 | :- use_module(specfile,[currently_opened_file/1]). | |
711 | html_info(Stream,A,SpecFile) :- | |
712 | format(Stream,'<h2>Information</h2>~n<ul>~n',[]), | |
713 | datime(datime(Year,Month,Day,Hour,Min,_Sec)), | |
714 | format(Stream,' <li>Trace generated on ~w.~w.~w at ~w:~w</li>~n',[Day,Month,Year,Hour,Min]), | |
715 | length(A,Len), | |
716 | format(Stream,' <li>Trace length: ~w</li>~n',[Len]), | |
717 | animation_mode(Mode), | |
718 | format(Stream,' <li>Specification file (~w): ~w</li>~n',[Mode,SpecFile]), | |
719 | ((SpecFile \= unknown,get_file_revision_info(SpecFile,GitRev)) | |
720 | -> format(Stream,' <li>Git revision of file: ~s</li>~n',[GitRev]) ; true), | |
721 | ((SpecFile \= unknown,get_HEAD_revision_info(SpecFile,GitHeadRev)) | |
722 | -> format(Stream,' <li>Git revision of repository HEAD: ~s</li>~n',[GitHeadRev]) ; true), | |
723 | version_str(V), revision(R), lastchangeddate(LD), | |
724 | format(Stream,' <li>ProB version: ~w</li>~n',[V]), | |
725 | format(Stream,' <li>ProB revision: ~w (~w)</li>~n',[R, LD]), | |
726 | format(Stream,'</ul>~n',[]). | |
727 | ||
728 | % b_get_main_filename -> Project Info:, Model Version/Revision ? Can we ask git ? | |
729 | % git ls-files -s VSS_TrainStatus_HL3.mch diff | |
730 | % git rev-parse HEAD | |
731 | ||
732 | :- use_module(system_call,[get_command_path/2, system_call_env/6]). | |
733 | :- use_module(tools,[get_parent_directory/2]). | |
734 | ||
735 | get_file_revision_info(File,GitOutputText) :- | |
736 | get_parent_directory(File,CurWorkingDir), | |
737 | run_git_command(['ls-files','-s',File],CurWorkingDir,GitOutputText). | |
738 | get_HEAD_revision_info(ReferenceFile,GitOutputText) :- | |
739 | get_parent_directory(ReferenceFile,CurWorkingDir), | |
740 | run_git_command(['rev-parse','HEAD'],CurWorkingDir,GitOutputText). | |
741 | ||
742 | ||
743 | run_git_command(COMMAND,CurWorkingDir,GitOutputText) :- | |
744 | get_command_path(git,GitPath), | |
745 | (debug_mode(on) -> format(user_output,'Git: ~w with CWD: ~w~n',[GitPath,CurWorkingDir]) ; true), | |
746 | on_exception(E, | |
747 | system_call_env(GitPath,COMMAND,[cwd(CurWorkingDir)],GitOutputText,GitError,ExitCode), | |
748 | (debug_format(9,'Git exception: ~w~n',[E]),fail)), | |
749 | (debug_mode(on) | |
750 | -> format(user_output,'git command ~w~n:~s~nError: ~s~nExitCode:~w~n', | |
751 | [COMMAND,GitOutputText,GitError,ExitCode]) ; true), | |
752 | ExitCode = exit(0), GitError=[]. | |
753 | ||
754 |