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