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