1 % Heinrich Heine Universitaet Duesseldorf
2 % (c) 2021-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(visb_visualiser,[load_visb_file/1, load_visb_file_if_necessary/1,
6 visb_file_is_loaded/1, visb_file_is_loaded/3,
7 visb_current_state_can_be_visualised/0,
8 get_default_visb_file/2, extended_static_check_default_visb_file/0,
9 load_default_visb_file_if_necessary/0,
10 generate_visb_html_for_history/1, generate_visb_html_for_history/2,
11 generate_visb_html_for_history_with_vars/1,
12 generate_visb_html_for_history_with_source/1,
13 generate_visb_html_for_current_state/1, generate_visb_html_for_current_state/2,
14 generate_visb_html_codes_for_states/3,
15 generate_visb_html/3,
16 tcltk_get_visb_items/1, tcltk_get_visb_events/1,
17 tcltk_get_visb_objects/1, tcltk_get_visb_hovers/1,
18 get_visb_items/1, get_visb_attributes_for_state/2,
19 get_visb_click_events/1, get_visb_hovers/1,
20 perform_visb_click_event/4,
21 tcltk_perform_visb_click_event/1,
22 get_visb_default_svg_file_contents/1,
23 get_visb_svg_objects/1]).
24
25 :- use_module(probsrc(module_information),[module_info/2]).
26 :- module_info(group,visualization).
27 :- module_info(description,'This module provides VisB visualisation functionality.').
28
29
30 :- meta_predicate process_repeat(-,-,-,2,-).
31
32 :- use_module(extrasrc(json_parser),[json_parse_file/3]).
33 :- use_module(library(lists)).
34
35 :- use_module(probsrc(error_manager)).
36 :- use_module(probsrc(preferences),[get_preference/2]).
37 :- use_module(probsrc(debug)).
38 :- use_module(probsrc(state_space), [visited_expression/2, visited_state_corresponds_to_initialised_b_machine/1,
39 get_constants_id_for_state_id/2, get_constants_state_id_for_id/2,
40 set_context_state/2, clear_context_state/0,
41 transition/3, transition/4,
42 multiple_concrete_constants_exist/0, is_concrete_constants_state_id/1]).
43 :- use_module(probsrc(translate), [translate_bvalue_to_codes/2, translate_bvalue_with_limit/3]).
44 :- use_module(probsrc(specfile),[eventb_mode/0,
45 state_corresponds_to_initialised_b_machine/2,
46 state_corresponds_to_fully_setup_b_machine/2,
47 state_corresponds_to_set_up_constants_only/2,
48 expand_to_constants_and_variables/3]).
49
50 :- use_module(probsrc(tools),[start_ms_timer/1,stop_ms_walltimer_with_msg/2]).
51 :- use_module(probsrc(tools_io),[safe_open_file/4, with_open_stream_to_codes/4]).
52 :- use_module(probsrc(bmachine), [b_machine_name/1, b_get_definition/5,
53 determine_type_of_formula/2, determine_type_of_formula/3]).
54 :- use_module(probsrc(bsyntaxtree), [get_texpr_ids/2]).
55 :- use_module(probsrc(tools_lists),[include_maplist/3]).
56 :- use_module(probsrc(tools),[split_list/4, html_escape/2]).
57 :- use_module(probsrc(tools_matching),[get_all_svg_attributes/1, is_svg_attribute/1,
58 is_svg_number_attribute/2, is_svg_color_attribute/1]).
59
60 % --------------------------
61
62 % facts storing loaded JSON VisB file:
63 :- dynamic visb_file_loaded/3, visb_svg_file/5, visb_empty_svg_box_height_width/3,
64 visb_definition/6, visb_special_definition/6,
65 visb_item/7,
66 visb_event/6, visb_hover/5, visb_has_hovers/1,
67 visb_event_enable_list/5,
68 visb_svg_object/6,
69 visb_svg_child/2.
70 :- dynamic auxiliary_visb_event/5.
71 % visb_svg_file(SVGFile, AbsolutePathSVGFile, JSONFileFromWhichWeImportSVG,PosTerm,ModLocTime)
72 % visb_item(SVGID,Attribute,TypedExpression,UsedIds,Description/Comment,StartPos,OtherMetaInfos)
73 % visb_event(SVGID,Event,PredicateList,TypedPredicate,File,Pos)
74 % visb_svg_object(SVGID,SVG_Class,AttrList,ChildList,Description/Comment,Pos) ; AttrList contains svg_attribute(Attr,Val)
75
76 reset_visb :-
77 retractall(visb_file_loaded(_,_,_)),
78 retractall(visb_empty_svg_box_height_width(_,_,_)),
79 retractall(visb_svg_file(_,_,_,_,_)),
80 retractall(visb_definition(_,_,_,_,_,_)),
81 retractall(visb_special_definition(_,_,_,_,_,_)),
82 retractall(visb_item(_,_,_,_,_,_,_)),
83 retractall(visb_event(_,_,_,_,_,_)),
84 retractall(visb_hover(_,_,_,_,_)),
85 retractall(visb_has_hovers(_)),
86 retractall(visb_event_enable_list(_,_,_,_,_)),
87 retractall(auxiliary_visb_event(_,_,_,_,_)),
88 retractall(visb_svg_object(_,_,_,_,_,_)),
89 retractall(visb_svg_child(_,_)).
90
91 visb_file_is_loaded(JSONFile) :-
92 visb_file_is_loaded(JSONFile,_,true).
93 visb_file_is_loaded(JSONFile,SVGFile,AllowEmpty) :-
94 visb_file_loaded(JSONFile,_,_),
95 (visb_svg_file(_,SVGFile,_,_,_) -> true
96 ; visb_empty_svg_box_height_width(_,_,_) -> SVGFile = ''
97 ; user_has_defined_visb_objects -> SVGFile = ''
98 ; JSONFile='' ->
99 AllowEmpty=true,
100 add_warning(visb_visualiser,'No VISB_SVG_FILE or VISB_SVG_OBJECTS specified in DEFINITIONS',''),
101 % Note: warning also generated below No VisB JSON file is specified and no VISB_SVG_OBJECTS were created
102 SVGFile = ''
103 ; add_warning(visb_visualiser,'No SVG file or objects specified for VisB file:',JSONFile),
104 AllowEmpty=true,
105 SVGFile = ''
106 ).
107
108 :- use_module(probsrc(state_space),[current_state_id/1,
109 current_state_corresponds_to_setup_constants_b_machine/0]).
110 visb_current_state_can_be_visualised :-
111 %visb_file_is_loaded(_), % no longer checked; Tcl/Tk will automatically load VisB file if required
112 (b_or_z_mode -> current_state_corresponds_to_setup_constants_b_machine
113 ; \+ current_state_id(root)
114 ).
115
116 :- use_module(probsrc(eventhandling),[register_event_listener/3]).
117 :- register_event_listener(reset_specification,reset_visb,'Reset VisB information').
118 :- register_event_listener(reset_prob,reset_visb,'Reset VisB information').
119
120 %static_check_visb :- % now done when adding items and not storing multiple items
121 % visb_item(ID,Attr,F1,_,_,Pos1), visb_item(ID,Attr,F2,_,Pos2), F1 @< F2,
122 % add_warning(visb_visualiser,'Multiple formulas for SVG identifier and attribute:',ID/Attr,Pos1),
123 % add_message(visb_visualiser,'Location of second formula for:',ID/Attr,Pos2),
124 % fail.
125 % TO DO: some sanity checks on attributes and values
126 static_check_visb.
127 % --------------------------
128
129 :- use_module(probsrc(tools),[read_string_from_file/2]).
130
131 % store templates as facts, so that compiled version of probcli does not need to find files
132 :- dynamic visb_template_file_codes/2.
133
134 assert_from_template(Filename) :- %formatsilent('Loading ~w~n',[Filename]),
135 absolute_file_name(visbsrc(Filename), Absolute, []),
136 read_string_from_file(Absolute,String),
137 assertz(visb_template_file_codes(Filename,String)).
138
139 :- assert_from_template('visb_template_header.html').
140 :- assert_from_template('visb_template_middle.html').
141 :- assert_from_template('visb_template_footer.html').
142
143 write_visb_template(HtmlFile,Stream) :-
144 visb_template_file_codes(HtmlFile,Codes),
145 format(Stream,'~s~n',[Codes]).
146
147
148 % --------------------------
149
150 :- use_module(probsrc(pref_definitions),[b_get_definition_string_from_spec/3]).
151 get_default_visb_file(Path, Pos) :-
152 (b_get_definition_string_from_spec('VISB_JSON_FILE', Pos, Path)
153 -> true % user provided explicit path to VISB JSON file
154 ; get_default_visb_svg_file(_,Pos)
155 -> Path='' % user provided SVG file path
156 ; user_has_defined_visb_objects_in_defs
157 -> Path='' % user provided SVG object definitions
158 ).
159
160 user_has_defined_visb_objects :-
161 (visb_svg_object(_,_,_,_,_,_) -> true % created in JSON file
162 ; user_has_defined_visb_objects_in_defs).
163
164 user_has_defined_visb_objects_in_defs :-
165 b_sorted_b_definition_prefixed(expression,'VISB_SVG_OBJECTS',_,_).
166
167 % you should do b_absolute_file_name_relative_to_main_machine
168 get_default_visb_svg_file(Path, Pos) :-
169 b_get_definition_string_from_spec('VISB_SVG_FILE', Pos, Path).
170
171
172 % load devault VISB_JSON_FILE if it is specified and not already loaded
173 load_default_visb_file_if_necessary :-
174 get_default_visb_file(File, Pos),!,
175 (load_visb_file_if_necessary(File) -> true
176 ; add_error(visb_visualiser,'Could not load VISB_JSON_FILE:',File,Pos)).
177 load_default_visb_file_if_necessary :-
178 (eventb_mode -> true ; add_message(visb_visualiser,'No VISB_JSON_FILE DEFINITION provided')).
179
180 % --------------------------
181 % Loading a JSON VisB file:
182
183
184 load_visb_file(File) :-
185 reset_visb,
186 load_visb_from_definitions(no_inlining), % TODO: pass InlineObjects?
187 start_ms_timer(T),
188 (File='' % No JSON file
189 -> (get_default_visb_svg_file(SvgFile,_)
190 -> (SvgFile='' -> AbsFile=SvgFile % just dummy empty string provided by user
191 ; b_absolute_file_name_relative_to_main_machine(SvgFile,AbsFile)
192 ),
193 add_visb_svg_file(SvgFile,AbsFile,'')
194 ; check_objects_created(File) % no JSON and SVG file; check we have created objects
195 )
196 ; add_visb_file(File,[])
197 ),
198 stop_ms_walltimer_with_msg(T,'loading VisB file: '),
199 static_check_visb,
200 (File = ''
201 -> ModTime=0, ModLocTime=0 % We could get modification time of files with VISB_SVG_OBJECTS, ... DEFINITIONS
202 ; file_property(File, modify_timestamp, ModTime),
203 file_property(File, modify_localtime, ModLocTime)
204 ),
205 assertz(visb_file_loaded(File,ModTime,ModLocTime)).
206
207 check_objects_created(File) :-
208 (visb_svg_object(_,_,_,_,_,_) -> true
209 ; add_warning(visb_visualiser,'No VisB JSON file is specified and no VISB_SVG_OBJECTS were created:',File)
210 ).
211
212 load_visb_from_definitions(InlineObjects) :-
213 start_ms_timer(T),
214 get_svg_objects_from_definitions(InlineObjects),
215 (get_SVG_BOX_definition(InlineObjects) -> true ; true),
216 stop_ms_walltimer_with_msg(T,'extracting VisB infos from DEFINITIONS: ').
217
218 :- use_module(library(file_systems),[file_exists/1, file_property/3]).
219 %:- use_module(library(system),[now/1, datime/2]).
220 load_visb_file_if_necessary(File) :-
221 visb_file_loaded(File,ModTime1,_), % this file is already loaded
222 (File = '' -> true
223 ; file_exists(File),
224 file_property(File, modify_timestamp, ModTime2), % check if it has the same time stamp
225 debug_println(19,visb_json_already_loaded(File,ModTime1,ModTime2)),
226 ModTime1=ModTime2
227 ),
228 !.
229 load_visb_file_if_necessary(File) :- load_visb_file(File).
230
231
232 :- use_module(probsrc(bmachine),[set_additional_filename_as_parsing_default/3, reset_filename_parsing_default/2]).
233
234 add_visb_file(File,LoadedFiles) :- member(File,LoadedFiles),!,
235 add_error(visb_visualiser,'Circular inclusion of JSON files:',[File|LoadedFiles]).
236 add_visb_file(File,_) :- \+ file_exists(File),!,
237 add_error(visb_visualiser,'JSON file does not exist:',File), fail.
238 add_visb_file(File,LoadedFiles) :-
239 debug_format(19,'Loading JSON File: ~w~n',[File]),
240 set_additional_filename_as_parsing_default(File,NewNr,OldNr),
241 call_cleanup(add_visb_file2(File,LoadedFiles), reset_filename_parsing_default(NewNr,OldNr)).
242
243 add_visb_file2(File,LoadedFiles) :-
244 json_parse_file(File, [strings_as_atoms(true),position_infos(true)],json(List2)),
245 % tools_printing:trace_print(List2),nl,nl,
246 process_json(List2,File),
247 !,
248 (get_attr_with_pos(include,List2,JsonFile,File,Pos)
249 -> check_atom(JsonFile,include,Pos),
250 absolute_file_name(JsonFile,AF,[relative_to(File)]),
251 formatsilent('Including JSON file: ~w~n',[JsonFile]),
252 add_visb_file(AF,[File|LoadedFiles])
253 ; true
254 ),
255 (LoadedFiles=[], % only check for main included file
256 get_attr_with_pos('model-name',List2,ModelName,File,MPos),
257 b_machine_name(Main), Main \= ModelName
258 -> ajoin(['VisB JSON file expects model-name ',ModelName,' instead of: '],MMsg),
259 add_warning(visb_visualiser,MMsg,Main,MPos)
260 ; true
261 ).
262 add_visb_file2(File,_) :-
263 add_error(visb_visualiser,'Unable to process JSON file:',File),
264 fail.
265
266 % process json content of a VisB file:
267 process_json(List,JSONFile) :- visb_svg_file(_,_,_,_,_),!, % we have already determined the SVG file
268 process_json2(List,JSONFile).
269 process_json(List,JSONFile) :-
270 get_attr_with_pos(svg_box,List,json(BoxList),JSONFile,Pos),
271 % json([=(width,400,3-3),=(height,400,3-3)])
272 (get_attr(svg,List,SvgFile) -> SvgFile='' ; true), % check if svg attr empty or non-existant
273 force_get_attr_nr(height,BoxList,H,JSONFile),
274 force_get_attr_nr(width,BoxList,W,JSONFile),!, % TODO: also set viewBox
275 (get_attr(viewBox,BoxList,VB) -> ViewBox=VB ; ViewBox=''),
276 add_message(visb_visualiser,'Will create empty SVG image with specified dimensions: ',H:W,Pos),
277 assert_visb_empty_svg_box_height_width(H,W,ViewBox,Pos),
278 process_json2(List,JSONFile).
279 process_json(List,JSONFile) :-
280 get_attr_with_pos(svg,List,File,JSONFile,Pos),
281 check_atom(File,svg,Pos),
282 (File = '' -> get_default_visb_svg_file(SvgFile, _)
283 ; get_default_visb_svg_file(SvgFile, DPos)
284 -> add_message(visb_visualiser,'Overriding svg file specified in JSON file: ',File,DPos)
285 ; SvgFile=File),
286 !,
287 absolute_file_name(SvgFile,AbsFile,[relative_to(JSONFile)]),
288 add_visb_svg_file(SvgFile,AbsFile,JSONFile),
289 process_json2(List,JSONFile).
290 process_json(List,JSONFile) :-
291 get_default_visb_svg_file(SvgFile, _), SvgFile \= '',
292 !,
293 absolute_file_name(SvgFile,AbsFile,[]), % relative to B machine??
294 add_visb_svg_file(SvgFile,AbsFile,JSONFile),
295 process_json2(List,JSONFile).
296 process_json(List,JSONFile) :-
297 process_json2(List,JSONFile),
298 (get_SVG_BOX_definition(no_inlining) -> true % TODO: pass (InlineObjects)
299 ; get_attr_with_pos(svg,List,_,JSONFile,Pos) -> % File is empty
300 add_message(visb_visualiser,'Creating empty SVG image. You can add a declaration like "svg_box": {"width":W,"height":H} to specify dimensions in: ',JSONFile,Pos)
301 ; add_warning(visb_visualiser,'Creating empty SVG image. The JSON file contains no svg attribute (pointing to the SVG file): ',JSONFile)
302 ).
303
304 add_visb_svg_file(SvgFile,AbsFile,JSONFile) :-
305 formatsilent('SVG file = ~w (~w)~n',[SvgFile, AbsFile]),
306 (SvgFile='' -> add_message(visb_visualiser,'Empty VisB SVG file:',SvgFile,Pos)
307 ; file_exists(AbsFile)
308 -> file_property(AbsFile, modify_localtime, ModLocTime)
309 ; add_error(visb_visualiser,'The specified VisB SVG file does not exist:',SvgFile,Pos),
310 ModLocTime=unknown
311 ),
312 assertz(visb_svg_file(SvgFile,AbsFile,JSONFile,Pos,ModLocTime)).
313
314 process_json2(List,JSONFile) :-
315 process_json_definitions(List,JSONFile),
316 process_json_items(List,JSONFile),
317 process_json_events(List,JSONFile),
318 process_json_new_svg_objects(List,JSONFile).
319
320 :- use_module(probsrc(tools_strings),[ajoin/2]).
321 check_atom(Atom,_,_) :- atom(Atom),!.
322 check_atom(Term,Attr,Pos) :-
323 ajoin(['Illegal JSON attribute ',Attr,', expected a JSON string:'],Msg),
324 add_error(visb_visualiser,Msg,Term,Pos),fail.
325 % ----------------
326
327 % B definitions that can help write items, events more compactly
328 process_json_definitions(List,File) :-
329 get_attr(definitions,List,Defs),!,
330 length(Defs,Len),
331 formatsilent('VisB Definitions: ~w~n',[Len]),
332 maplist(process_json_definition(File),Defs).
333 process_json_definitions(_,_File).
334
335 % VisB items which modify attributes of SVG objects
336 process_json_items(List,File) :-
337 get_attr(items,List,Items),!,
338 length(Items,Len),
339 formatsilent('VisB Item declarations: ~w~n',[Len]),
340 maplist(process_json_item(File),Items).
341 process_json_items(_,File) :- \+ visb_special_definition(visb_updates,_,_,_,_,_),!,
342 add_message(visb_visualiser,'The JSON file contains no items: ',File).
343 process_json_items(_,_).
344
345 % VisB events which react to clicks on SVG objects and display hovers
346 process_json_events(List,File) :-
347 get_attr(events,List,Items),!,
348 length(Items,Len),
349 formatsilent('VisB Event declarations: ~w~n',[Len]),
350 maplist(process_json_event(File),Items).
351 process_json_events(_,_).
352
353 % VisB additional SVG objects added to SVG file
354 process_json_new_svg_objects(List,File) :-
355 get_attr(svg_objects,List,Items),!,
356 length(Items,Len),
357 formatsilent('VisB additional SVG object declarations: ~w~n',[Len]),
358 maplist(process_json_svg_object(File),Items).
359 process_json_new_svg_objects(List,File) :-
360 get_attr_with_pos(objects,List,Items,File,Pos),!,
361 add_warning(visb_visualiser,'Use "svg_objects" attribute instead of "objects" in: ',File,Pos),
362 maplist(process_json_svg_object(File),Items).
363 process_json_new_svg_objects(_,_).
364
365 :- use_module(probsrc(custom_explicit_sets),[try_expand_custom_set_with_catch/3, is_set_value/2]).
366 % evaluate all VISB_SVG_OBJECTS... DEFINITIONS and try and extract SVG objects
367 % this must be a set of records with at least id and svg_class field
368 get_svg_objects_from_definitions(InlineObjects) :-
369 find_visb_DEFINITION('VISB_SVG_OBJECTS', SVG_ID, AttrList, Desc, DefName, DefPos,InlineObjects,allow_separation),
370 add_visb_object_from_definition(visb_objects, SVG_ID, AttrList, Desc, DefName, DefPos),
371 %formatsilent('Generating new SVG object ~w with class ~w and attrs ~w~n',[SVG_ID,SVG_Class,AttrList2]),
372 fail.
373 get_svg_objects_from_definitions(InlineObjects) :-
374 find_visb_DEFINITION('VISB_SVG_EVENTS', SVG_ID, AttrList, Desc, DefName, DefPos,InlineObjects,no_separation),
375 add_visb_object_from_definition(visb_events, SVG_ID, AttrList, Desc, DefName, DefPos),
376 fail.
377 get_svg_objects_from_definitions(InlineObjects) :-
378 find_visb_DEFINITION('VISB_SVG_HOVERS', SVG_ID, AttrList, Desc, DefName, DefPos,InlineObjects,no_separation),
379 add_visb_object_from_definition(visb_hovers, SVG_ID, AttrList, Desc, DefName, DefPos),
380 fail.
381 get_svg_objects_from_definitions(_InlineObjects) :- precompile_svg_object_updates.
382
383 % add a VisB record object from a HOVER or OBJECT definition:
384 add_visb_object_from_definition(visb_objects,SVG_ID, AttrList, Desc, DefName, DefPos) :- !,
385 (select(svg_attribute(svg_class,SVG_Class),AttrList,AttrList2)
386 -> true % maybe we should call svg_class svg_shape
387 ; add_warning(visb_visualiser,'SVG objects have no svg_class field:',DefName,DefPos),
388 fail
389 ),
390 assert_visb_svg_object(SVG_ID,SVG_Class,AttrList2,Desc,DefPos).
391 add_visb_object_from_definition(visb_hovers,SVG_ID, AttrList, _Desc, _DefName, DefPos) :-
392 (select(svg_attribute(trigger_id,TriggerID),AttrList,AttrList2) -> true
393 ; select(svg_attribute('trigger-id',TriggerID),AttrList,AttrList2) -> true
394 ; TriggerID = SVG_ID, AttrList2=AttrList),
395 member(svg_attribute(Attr,EnterVal),AttrList2),
396 (visb_svg_object(SVG_ID,_,StaticAttrList,_Childs,_,ExitPos)
397 -> (member(svg_attribute(Attr,ExitVal),StaticAttrList) -> true
398 ; Attr = 'svg_class'
399 -> add_warning(visb_visualiser,
400 'svg_class cannot be set in hover for: ',SVG_ID,ExitPos),
401 ExitVal=EnterVal
402 ; add_warning(visb_visualiser,
403 'No static (exit) value can be retrieved for hover for attribute: ',Attr,ExitPos),
404 ExitVal=EnterVal
405 )
406 ; add_warning(visb_visualiser,'No VISB_SVG_OBJECT for: ',SVG_ID:Attr,DefPos),
407 ExitVal=EnterVal
408 ),
409 assert_visb_hover(TriggerID,SVG_ID,Attr,EnterVal,ExitVal).
410 add_visb_object_from_definition(visb_events,SVG_ID, AttrList, _Desc, DefName, DefPos) :- !,
411 (select(svg_attribute(event,Event),AttrList,AttrList1) -> true
412 ; add_warning(visb_visualiser,'Missing event attribute in VisB definition: ',DefName,DefPos),
413 fail
414 ),
415 (select(svg_attribute(predicate,Pred),AttrList1,_AttrList2) -> Preds=[Pred]
416 ; Preds=[] %, AttrList2=AttrList1
417 ),
418 EnableItems=[],
419 % TODO extract from AttrList2: visb_enable_item(SvgID,Attr,EnabledValExpr,DisabledValExpr,PosAttr)
420 (error_manager:extract_file_number_and_name(DefPos,_,File) -> true ; File='?'),
421 add_visb_event(SVG_ID,Event,Preds,EnableItems,[],File,DefPos,[]).
422
423 % is called in process_json when no SVG file specified
424 % VISB_SVG_BOX == rec(width:1000,height:1000,viewBox:"minx miny w h"),
425 get_SVG_BOX_definition(InlineObjects) :-
426 get_and_eval_special_definition('VISB_SVG_BOX','VISB_SVG_BOX',visb_box,DefPos,ResValue,InlineObjects),
427 (ResValue=(BH,BW) -> ViewBox=''
428 ; get_VISB_record_fields(ResValue,Fields),
429 member(field(height,BH),Fields),
430 member(field(width,BW),Fields)
431 -> (member(field(viewBox,string(VB)),Fields) -> ViewBox=VB ; ViewBox='')
432 % Viewbox is "mx my w h" string, ie: minimum_x, minimum_y, width and height
433 % TODO: some sanity checking and check if there are other fields
434 ; add_error(visb_visualiser,'Ignoring VISB_SVG_BOX, must be record or pair of integers (height,width):',ResValue,DefPos)),
435 (get_number_from_bvalue(BH,H) -> true
436 ; add_error(visb_visualiser,'VISB_SVG_BOX Height is not a number:',ResValue,DefPos)),
437 (get_number_from_bvalue(BW,W) -> true
438 ; add_error(visb_visualiser,'VISB_SVG_BOX Width is not a number:',ResValue,DefPos)),
439 !,
440 assert_visb_empty_svg_box_height_width(H,W,ViewBox,DefPos).
441
442
443
444
445 assert_visb_empty_svg_box_height_width(H,W,_ViewBox,Pos) :-
446 retract(visb_empty_svg_box_height_width(OldH,OldW,_)),
447 (OldH,OldW) \= (H,W),
448 add_message(visb_visualiser,'Overriding VisB SVG_BOX default dimensions: ',(OldH,OldW),Pos),
449 fail.
450 assert_visb_empty_svg_box_height_width(H,W,ViewBox,_Pos) :-
451 %add_message(visb_visualiser,'Setting VisB SVG_BOX default dimensions: ',(H,W,ViewBox),Pos),
452 assert(visb_empty_svg_box_height_width(H,W,ViewBox)).
453
454 :- use_module(probsrc(bmachine),[b_sorted_b_definition_prefixed/4, b_get_typed_definition/3]).
455 % find DEFINITION with given prefix in name, evaluate it and return SVG_ID and attribute list:
456 % AllowSep = allow_seperation means that the record fields can be separated into static objects and dynamic updates
457 % and only static ones will be retained (dynamic ones dealt with later)
458 find_visb_DEFINITION(DEFPREFIX, SVG_ID, AttrList,Desc, DefName, DefPos,InlineObjects,AllowSep) :-
459 b_sorted_b_definition_prefixed(expression,DEFPREFIX,DefName,DefPos),
460 get_typed_static_definition_with_constants_state(DefName,Body,DefPos,ConstantsState,InlineObjects,AllowSep),
461 get_visb_DEFINITION_svg_object(DefName,Body,DefPos,ConstantsState,SVG_ID,AttrList,Desc).
462
463 % evaluate a typed body expressions evaluating to a record or set of records
464 % and translate into SVG attribute lists:
465 get_visb_static_svg_object_for_typed_expr(DefName,Body,DefPos,SVG_ID,AttrList,Desc) :-
466 AllowSep=no_separation,
467 Inline=no_inlining,
468 get_typed_static_definition_with_constants_state2(DefName,Body,ResBody,DefPos,ConstState,Inline,AllowSep),
469 get_visb_DEFINITION_svg_object(DefName,ResBody,DefPos,ConstState,SVG_ID,AttrList,Desc).
470
471
472 get_typed_static_definition_with_constants_state(DefName,ResBody,DefPos,ConstState,InlineObjects,AllowSep) :-
473 b_get_typed_definition(DefName,[variables],Body),
474 get_typed_static_definition_with_constants_state2(DefName,Body,ResBody,DefPos,ConstState,InlineObjects,AllowSep).
475
476 get_typed_static_definition_with_constants_state2(DefName,Body,ResBody,DefPos,ConstantsState,InlineObjects,AllowSep) :-
477 determine_type_of_visb_formula(Body,TIds,Class),
478 debug_format(19,'Detected VisB DEFINITION ~w (~w)~n',[DefName,Class]),
479 (%Class=requires_variables, % now also useful if event field present
480 AllowSep=allow_separation, % allowed for VISB_SVG_OBJECTS
481 separate_into_static_and_dynamic_part(DefName,Body,StaticBody,DynamicBody,EventBody),
482 determine_type_of_visb_formula(StaticBody,SIds,SClass),
483 get_unique_initial_state_for_visb(SClass,DefName,DefPos,SIds,ConstantsState)
484 -> Separated=true, ResBody=StaticBody,
485 add_debug_message(visb_visualiser,'Automatically separated fields into static and dynamic: ',DefName,DefPos),
486 %write('STATIC: '),translate:print_bexpr(StaticBody),nl, write('DYNAMIC: '),translate:print_bexpr(DynamicBody),nl,
487 assert_visb_udpate_def_body(DefName,DynamicBody,DefPos),
488 add_visb_events_from_def_body(DefName,EventBody,DefPos)
489 ; get_unique_initial_state_for_visb(Class,DefName,DefPos,TIds,ConstantsState)
490 -> ResBody=Body
491 ; ResBody=Body,
492 (Class=requires_constants ->
493 get_texpr_ids(TIds,Ids),
494 % we could check if values of Ids are identical in all constants solutions
495 (is_concrete_constants_state_id(_)
496 -> BMsg='multiple solutions for used constants exist: '
497 ; BMsg='but no constants were found or setup yet: '
498 ),
499 ajoin(['DEFINITION ',DefName, ' requires constants but ',BMsg],Msg),
500 (get_a_constants_state(ConstantsState,StateID,InlineObjects)
501 -> (member(CstID,Ids),
502 other_constant_value_exists_for(CstID,ConstantsState,StateID)
503 -> add_warning(visb_visualiser,Msg,CstID,DefPos)
504 ; ajoin(['DEFINITION ',DefName,
505 ' requires constants and all SETUP_CONSTANTS solutions have same value thus far: '],Msg2),
506 % constraint-based checks or execute by predicate could later create others !
507 add_message(visb_visualiser,Msg2,Ids,DefPos)
508 )
509 ; add_error(visb_visualiser,Msg,Ids,DefPos), ConstantsState=[]
510 )
511 ; ConstantsState=[]
512 )
513 ),
514 (Class=requires_variables, Separated=false
515 -> (get_preference(visb_allow_variables_for_objects,false)
516 -> add_warning(visb_visualiser,'Ignoring DEFINITION which requires variables:',DefName,DefPos),fail
517 ; ConstantsState=[] -> add_warning(visb_visualiser,'Ignoring DEFINITION which requires variables, could not find unique initial state:',DefName,DefPos),fail
518 ; add_message(visb_visualiser,'DEFINITION requires variables, exporting history to HTML may not work correctly:',DefName,DefPos)
519 )
520 ; true).
521
522 % separate/split/filter VISB_SVG_OBJECTS definitions into a static part and a dynamic part depending on variables
523 % (aka updates/items)
524 separate_into_static_and_dynamic_part(DefName,TExpr,
525 b(StaticSetComp,set(ST),I),
526 b(DynamicSetComp,set(DT),I),
527 b(EventsSetComp,set(ET),I)) :-
528 bsyntaxtree:is_eventb_comprehension_set(TExpr,Ids,Pred,Expr),
529 !,
530 determine_type_of_visb_formula(b(exists(Ids,Pred),pred,[]),SIds,Class),
531 get_unique_initial_state_for_visb(Class,DefName,Pred,SIds,_), % The predicate must be statically executable
532 separate_into_static_and_dynamic_part(DefName,Expr,StaticRec,DynamicRec,EventRec),
533 get_texpr_type(StaticRec,ST),
534 get_texpr_type(DynamicRec,DT),
535 get_texpr_type(EventRec,ET),
536 bsyntaxtree:get_texpr_info(TExpr,I),
537 b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,StaticRec,Pred, set(ST), StaticSetComp),
538 b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,DynamicRec,Pred,set(DT), DynamicSetComp),
539 b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,EventRec,Pred,set(ET), EventsSetComp).
540 separate_into_static_and_dynamic_part(DefName,b(rec(Fields),_,Info),
541 b(rec(StaticFields),record(SFT),Info), % VISB_OBJECTS (static)
542 b(rec(AllDynamicFields),record(DFT),Info), % VISB_UPDATES (dynamic)
543 b(rec(AllEventFields),record(EFT),Info) % VISB_EVENTS
544 ) :-
545 split_list(is_visb_event_field,Fields,EventFields,ObjectFields),
546 separate_fields(ObjectFields,StaticFields0,DynamicFields,DefName),
547 (member(field(id,SVGID),StaticFields0)
548 -> (DynamicFields \= [] ; EventFields \= []),
549 StaticFields = StaticFields0
550 ; member(field(id,SVGID),DynamicFields)
551 -> add_warning(visb_visualiser,'SVG id field is not static in: ',DefName,SVGID),
552 fail
553 ; gensym(svg_id,GenID), SVGID = b(string(GenID),string,[]),
554 ajoin(['Generated id ',GenID, ' for SVG object without id field in: '],Msg),
555 add_message(visb_visualiser,Msg,DefName,Info),
556 StaticFields = [field(id,SVGID) | StaticFields0]
557 ),
558 maplist(get_field_type,StaticFields,SFT),
559 sort([field(id,SVGID)|DynamicFields],AllDynamicFields), % TODO: use kernel_records
560 maplist(get_field_type,AllDynamicFields,DFT),
561 sort([field(id,SVGID)|EventFields],AllEventFields), % ditto
562 maplist(get_field_type,AllEventFields,EFT).
563
564 is_visb_event_field(field(Name,_)) :- is_visb_event_field_name(Name).
565 is_visb_event_field_name(event).
566 is_visb_event_field_name(predicate).
567 % not yet supported:
568 %is_visb_event_field_name(hovers).
569 %is_visb_event_field_name(items). % enable items
570 %is_visb_event_field_name(optional).
571 %is_visb_event_field_name(override).
572
573
574 get_field_type(field(Name,Expr),field(Name,T)) :- get_texpr_type(Expr,T).
575
576 % separate fields from a SVG/VISB_SVG_OBJECT record into static part and dynamic update expressions
577 separate_fields([],[],[],_).
578 separate_fields([field(Field,Expr)|T],[field(Field,Expr)|TS],TD,DefName) :-
579 is_static_expr(Expr,Field,DefName),!,
580 separate_fields(T,TS,TD,DefName).
581 separate_fields([field(Field,Expr)|T],[field(Field,Default)|TS],[field(Field,Expr)|TD],DefName) :-
582 requires_static_default_value(Field,Default), !,
583 separate_fields(T,TS,TD,DefName).
584 separate_fields([H|T],TS,[H|TD],DefName) :-
585 separate_fields(T,TS,TD,DefName).
586
587 % fields which require a static default value; here to set up child SVG objects of title
588 % static default values could also be useful for hovers in general?
589 requires_static_default_value(title,b(string('-title-not-set-'),string,[])).
590
591 is_static_expr(Expr,Field,DefName) :-
592 determine_type_of_visb_formula(Expr,_TIds,Class), % TODO pass local variables from exists above
593 (Class=requires_nothing -> true
594 ; Class=requires_constants,
595 \+ multiple_concrete_constants_exist, % TODO: check if _TIds have multiple solutions
596 is_concrete_constants_state_id(_) -> true
597 ; ajoin(['Detected dynamic expression for field ',Field,' in ',DefName,': '],Msg),
598 add_debug_message(visb_visualiser,Msg,Expr,Expr),fail
599 ).
600
601 % --------
602
603
604 extract_attribute_from_record(DefPos,field(OrigName,Value),svg_attribute(Name,SVal)) :-
605 opt_rewrite_field_name(OrigName,Name),
606 extract_attribute_value(DefPos,Name,Value,SVal).
607 extract_attribute_from_record(DefPos,F,_) :-
608 add_error(bvisualiser,'Extract SVG attribute failed: ',F,DefPos),fail.
609
610 % extract a value for a particular field Name
611 extract_attribute_value(DefPos,Name,Value,SVal) :-
612 (deconstruct_singleton_set(Name,Value,Element)
613 -> Element \= '$optional_field_absent',
614 extract_attr_value(Name,Element,SVal,DefPos)
615 ; extract_attr_value(Name,Value,SVal,DefPos)
616 ).
617
618 :- use_module(probsrc(specfile), [classical_b_mode/0]).
619
620 % in TLA+ mode optional record fields have {TRUE|->VALUE} rather than VALUE
621 % this can also be useful in B to allow mixing different SVG records in a set
622 % for Alloy mode we may want to also support singleton sets as scalars
623 deconstruct_singleton_set(Name,Set,Res) :-
624 singleton_set(Set,El),
625 detect_partial_records_for_field(Name),
626 (El=(pred_true,El2)
627 -> Val=El2 % TLA2B encoding for optional fields that are present
628 ; Val=El), % Alloy
629 !,
630 Res = Val.
631 deconstruct_singleton_set(Name,[],Res) :-
632 detect_partial_records_for_field(Name),
633 Res = '$optional_field_absent'.
634
635 detect_partial_records_for_field(children) :- !, fail. % children field for groups is a set of ids
636 detect_partial_records_for_field(Name) :-
637 is_svg_number_attribute(Name),!. % sets never sensible as a numerical value
638 detect_partial_records_for_field(Name) :- is_id_or_text_attribute(Name),!. % ditto for ids
639 detect_partial_records_for_field(Name) :- is_svg_color_attribute(Name),!. % ditto for colors
640 detect_partial_records_for_field(_) :-
641 \+ classical_b_mode. % TODO: check that we are in TLA or Alloy mode?
642 % TODO: ensure ProB2 sets animation minor mode for TLA
643
644 :- use_module(probsrc(tools),[split_chars/3, safe_number_codes/2,safe_atom_codes/2]).
645 :- use_module(extrasrc(external_functions_svg),[svg_points/4]).
646 extract_attr_value(Name,Value,SVal,DefPos) :-
647 is_svg_number_attribute(Name),!, % we could try and extract svg_class from attribute list above
648 (get_number_from_bvalue(Value,NrVal)
649 -> SVal=NrVal % convert to atom?
650 ; b_value_to_string(Value,SVal),
651 (is_special_svg_number_form(SVal) -> true
652 ; atom_codes(SVal,CC),
653 safe_number_codes(_NrVal,CC) -> true
654 ; ajoin(['The value of the SVG attribute "',Name,
655 '" is not a number: '],Msg),
656 add_warning(visb_visualiser,Msg,SVal,DefPos)
657 )
658 ).
659 extract_attr_value(children,Value,SVal,DefPos) :- !,
660 (is_set_value(Value,extract_attr_value)
661 -> (try_expand_custom_set_with_catch(Value,ExpandedSet,extract_attr_value),
662 maplist(b_value_to_id_string,ExpandedSet,SVal) -> true
663 ; add_warning(visb_visualiser,'The children attribute should be a finite set of identifiers: ',Value,DefPos),
664 SVal=[]
665 )
666 ; add_warning(visb_visualiser,'The children attribute should be a set of identifiers: ',Value,DefPos),
667 SVal=[]).
668 extract_attr_value(points,Value,SVal,DefPos) :- % Class should be polygon or polyline
669 % automatically translate sequences of pairs of numbers to SVG string format
670 (Value = [(int(_),_)|_] ; Value = avl_set(node((int(_),_),_,_,_,_))), % TODO: check typing
671 svg_points(Value,Str,DefPos,no_wf_available),!,
672 string(SVal)=Str.
673 extract_attr_value(points,Value,SVal,_DefPos) :- Value = [],!, SVal = ''.
674 extract_attr_value(Name,Value,_,DefPos) :-
675 is_svg_color_attribute(Name),
676 illegal_color(Value),
677 ajoin(['The value of the SVG attribute "',Name,
678 '" is not a colour: ' ],Msg),
679 add_warning(visb_visualiser,Msg,Value,DefPos),fail.
680 extract_attr_value(Name,Value,SVal,_) :-
681 is_id_or_text_attribute(Name),!,
682 (is_text_attribute(Name)
683 -> b_value_to_text_string(Value,SVal)
684 ; b_value_to_id_string(Value,SVal)).
685 extract_attr_value(_Name,Value,SVal,_) :-
686 b_value_to_string(Value,SVal).
687
688
689 % now checked by check_attribute_type for updates, we could later check strings, currentcolor is allowed
690 illegal_color(pred_false).
691 illegal_color(pred_true).
692 illegal_color([]).
693 illegal_color(avl_set(_)).
694 illegal_color([_|_]).
695 illegal_color(closure(_,_,_)).
696 illegal_color(term(floating(_))).
697
698 % evaluate a DEFINITION to a set of B records representing SVG objects
699 get_visb_DEFINITION_svg_object(DefName,Body,DefPos,ExpandedState,SVG_ID,AttrList,Desc) :-
700 evaluate_visb_formula(Body,DefName,'',ExpandedState,ResValue,DefPos),
701 %formatsilent('Result for ~w~n',[DefName]), translate:print_bvalue(ResValue),nl,
702 (is_set_value(ResValue,get_visb_DEFINITION_svg_object)
703 -> try_expand_custom_set_with_catch(ResValue,ExpandedSet,get_visb_DEFINITION_svg_object),
704 (ExpandedSet = [(_,_)|_] % we have a relation, probably partial function STRING +-> STRING
705 -> Expanded = [ExpandedSet]
706 ; Expanded = ExpandedSet) % we should have a set of records
707 ; Expanded = [ResValue] % just create a singleton set with hopefully a record
708 ),
709 (Expanded = [] -> add_message(visb_visualiser,'Empty set of SVG object records: ',DefName,DefPos)
710 ; Expanded = [Record|_] ->
711 (get_VISB_record_fields(Record,Fs)
712 -> (member(field(id,_),Fs)
713 -> true
714 ; add_message(visb_visualiser,'DEFINITION needs an `id` field if you want to use updates: ',DefName,DefPos)
715 )
716 ; add_warning(visb_visualiser,'DEFINITION should evaluate to a set of records:',DefName,DefPos)
717 )
718 ; ajoin(['Could not expand ', DefName,' to a finite set of SVG object records: '],ErrMsg),
719 add_warning(visb_visualiser,ErrMsg,Expanded,DefPos),fail
720 ),
721 member(Records,Expanded),
722 get_VISB_record_fields(Records,Fields),
723 (select(field(id,VID),Fields,F1) -> extract_attribute_value(DefPos,id,VID,SVG_ID)
724 ; gensym(svg_id,SVG_ID), F1=Fields),
725 (select(field(comment,CC),F1,F2), b_value_to_string(CC,Desc) -> true
726 ; Desc = '', F2=F1),
727 include_maplist(extract_attribute_from_record(DefPos),F2,AttrList),
728 (select(svg_attribute(svg_class,SVG_Class),AttrList,A2)
729 -> maplist(check_attribute_is_supported(SVG_Class,DefPos),A2) ; true).
730
731 % get the fields of a B value record
732 % also transparently handles alternative representations, like a function from STRING to STRING
733 get_VISB_record_fields(rec(Fields),Res) :- !, Res=Fields.
734 get_VISB_record_fields(StringFunction,Fields) :-
735 is_set_value(StringFunction,get_visb_DEFINITION_svg_object),
736 try_expand_custom_set_with_catch(StringFunction,Expanded,get_visb_DEFINITION_svg_object),
737 % TODO: check we have no duplicates
738 maplist(convert_to_field,Expanded,Fields).
739 % TODO: support records as generated by READ_XML:
740 % rec(attributes:{("fill"|->"#90ee90"),("height"|->"360px"),("id"|->"background_rect"),("width"|->"600px"),("x"|->"1px"),("y"|->"2px")},element:"rect",meta:{("xmlLineNumber"|->"3")},pId:5,recId:6)
741 % for <rect height="360px" x="1px" y="2px" id="background_rect" width="600px" fill="#90ee90"></rect>
742
743 convert_to_field((string(FieldName),Value),field(FieldName,Value)).
744 % TODO: maybe handle enumerated set values as field names
745
746 is_record_for_visb(rec(_)).
747 is_record_for_visb(avl_set(_)). % TODO: check if fun from STRING
748 is_record_for_visb([(string(_),_)|_]).
749
750 % already extract and type-check VISB_SVG_UPDATES definitions
751 precompile_svg_object_updates :-
752 b_sorted_b_definition_prefixed(expression,'VISB_SVG_UPDATES',DefName,DefPos),
753 b_get_typed_definition(DefName,[variables],TypedExpr),
754 assert_visb_udpate_def_body(DefName,TypedExpr,DefPos),
755 fail.
756 precompile_svg_object_updates.
757
758 % assert VisB updates from B DEFINITION, either from VISB_SVG_UPDATES or dynamic parts of VISB_SVG_OBJECTS:
759 assert_visb_udpate_def_body(DefName,TypedExpr,DefPos) :-
760 get_texpr_type(TypedExpr,Type),
761 determine_type_of_visb_formula(TypedExpr,_,FormulaClass),
762 debug_format(19,'Detected updates: ~w (~w)~n',[DefName,FormulaClass]),
763 assertz(visb_special_definition(visb_updates,DefName,Type,TypedExpr,FormulaClass,DefPos)),
764 check_visb_update_type(Type,DefName,DefPos).
765
766 % assert VisB events from B DEFINITION, from part of VISB_SVG_OBJECTS:
767 % supporting event attribute and optional predicate attribute
768 add_visb_events_from_def_body(DefName,Body,DefPos) :-
769 get_texpr_type(Body,Type),
770 (Type = record([_,_|_]) ; Type=set(record([_,_|_]))), % at least one more field than just id field
771 get_visb_static_svg_object_for_typed_expr(DefName,Body,DefPos,SVG_ID,AttrList,Desc),
772 add_visb_object_from_definition(visb_events, SVG_ID, AttrList, Desc, DefName, DefPos),
773 fail.
774 add_visb_events_from_def_body(_,_,_).
775
776 get_svg_object_updates_from_definitions(ExpandedBState,SVG_ID,SvgAttribute,Value,DefPos) :-
777 visb_special_definition(visb_updates,DefName,_Type,BodyTypedExpr,_Class,DefPos),
778 get_visb_DEFINITION_svg_object(DefName,BodyTypedExpr,DefPos,ExpandedBState,SVG_ID,AttrList,_Desc),
779 member(svg_attribute(SvgAttribute,Value),AttrList).
780
781 check_visb_update_type(Type,DefName,DefPos) :-
782 (Type = set(record(Fields)) -> true
783 ; Type = record(Fields) -> true
784 % other types are STRING +-> STRING, ...; this will be checked in get_visb_DEFINITION_svg_object
785 ),
786 (memberchk(field('svg_class',_),Fields)
787 -> add_warning(visb_visualiser,'VisB updates should not set svg_class:',DefName,DefPos)
788 ; true),
789 member(field(Name,FieldType),Fields),
790 check_attribute_type(FieldType,Name,DefName,_Class,DefPos),
791 fail.
792 check_visb_update_type(_,_,_).
793
794 :- use_module(probsrc(translate), [pretty_type/2]).
795 % check B type of a field for an SVG update or object
796 check_attribute_type(Type,Name,DefName,Class,DefPos) :-
797 check_is_number_attribute(Name,Class,DefPos),!,
798 illegal_number_type(Type),
799 ajoin(['Type of field ',Name,' of ', DefName, ' is not a number: '],Msg),
800 pretty_type(Type,TS),
801 add_warning(visb_visualiser,Msg,TS,DefPos).
802 check_attribute_type(Type,Name,DefName,_,DefPos) :-
803 is_svg_color_attribute(Name),!,
804 illegal_col_type(Type),
805 ajoin(['Type of field ',Name,' of ', DefName, ' is not a color: '],Msg),
806 pretty_type(Type,TS),
807 add_warning(visb_visualiser,Msg,TS,DefPos).
808
809 illegal_nr_or_col_type(boolean).
810 illegal_nr_or_col_type(set(_)).
811 illegal_nr_or_col_type(seq(_)).
812 illegal_nr_or_col_type(record(_)).
813 illegal_nr_or_col_type(couple(A,B)) :- (illegal_nr_or_col_type(A) -> true ; illegal_nr_or_col_type(B)).
814 % check if couple types can work by concatenating string representations
815
816 illegal_col_type(X) :- illegal_nr_or_col_type(X),!.
817 illegal_col_type(real).
818 % integer ? or can we map integers to colours using a color scheme like in DOT?
819
820 illegal_number_type(X) :- illegal_nr_or_col_type(X),!.
821 %illegal_number_type(global(_)). % what if we use a global set with weird constants using back-quotes ?
822
823 % ----------------
824
825 % parse and load an individual JSON VisB item, e.g, :
826 % { "name":"xscale",
827 % "value" : "(100.0 / real(TrackElementNumber))"
828 % }
829
830 process_json_definition(File,json(List)) :-
831 (get_attr_true(ignore,List,File) -> true % ignore this definition
832 ; process_json_def_lst(File,List)).
833
834 :- use_module(probsrc(bsyntaxtree), [get_texpr_type/2]).
835 process_json_def_lst(File,List) :-
836 force_del_attr_with_pos(name,List,ID,L1,File,NamePos),
837 force_del_attr_with_pos(value,L1,Formula,L2,File,VPos),
838 debug_format(19,' Processing definition for ~w with value-formula (lines ~w):~w~n',[ID,VPos,Formula]),
839 !,
840 atom_codes(Formula,FCodes),
841 set_error_context(visb_error_context(definition,ID,'value',VPos)),
842 set_gen_parse_errors(L2,VPos,GenParseErrors),
843 (b_get_definition(ID,_DefType,_Args,_RawExpr,_Deps)
844 -> add_warning(visb_visualiser,'Ignoring VisB definition, DEFINITION of the same name already exists:',ID,NamePos)
845 ; parse_expr(FCodes,TypedExpr,GenParseErrors)
846 -> get_texpr_type(TypedExpr,Type),
847 determine_type_of_visb_formula(TypedExpr,TIds,Class),
848 (try_eval_static_def(Class,'static definition', ID,TypedExpr,TIds,StaticValue,VPos)
849 -> get_texpr_type(TypedExpr,Type),StaticValueExpr = b(value(StaticValue),Type,[]),
850 assert_visb_json_definition(ID,Type,StaticValueExpr,TIds,Class,VPos)
851 ; assert_visb_json_definition(ID,Type,TypedExpr,TIds,Class,VPos)
852 )
853 ; GenParseErrors=false -> formatsilent('Ignoring optional VisB definition for ~w due to error in B formula~n',[ID])
854 ; add_error(visb_visualiser,'Cannot parse or typecheck VisB formula for definition',ID,VPos)
855 ),
856 clear_error_context.
857 process_json_def_lst(File,List) :- get_pos_from_list(List,File,Pos),
858 add_error(visb_visualiser,'Illegal VisB Definition:',List,Pos).
859
860 % assert a VisB definition stemming from the JSON definitions section:
861 assert_visb_json_definition(DefName,Type,TypedExpr,UsedTIds,Class,DefPos) :-
862 (is_special_visb_def_name(DefName,SpecialClass) -> true ; SpecialClass = regular_def),
863 assertz(visb_definition(DefName,Type,TypedExpr,Class,DefPos,SpecialClass)),
864 (SpecialClass \= regular_def
865 -> formatsilent('Detected special ~w definition ~w (~w)~n',[SpecialClass,DefName,Class]),
866 add_special_json_definition(SpecialClass,DefName,Type,TypedExpr,UsedTIds,Class,DefPos)
867 ; true
868 ).
869
870 % register some special definitions, in which a set of objects/hovers/updates can be specified
871 % by a single definition returning a set of records
872 add_special_json_definition(visb_updates,DefName,Type,TypedExpr,_,Class,DefPos) :- !,
873 check_visb_update_type(Type,DefName,DefPos),
874 assertz(visb_special_definition(visb_updates,DefName,Type,TypedExpr,Class,DefPos)). % will be evaluated later
875 add_special_json_definition(visb_contents,DefName,Type,TypedExpr,_,Class,DefPos) :- !,
876 assertz(visb_special_definition(visb_contents,DefName,Type,TypedExpr,Class,DefPos)).
877 add_special_json_definition(visb_box,DefName,Type,TypedExpr,_,Class,DefPos) :- !,
878 assertz(visb_special_definition(visb_box,DefName,Type,TypedExpr,Class,DefPos)).
879 add_special_json_definition(visb_objects,DefName,_Type,TypedExpr,_UsedTIds,_Class,DefPos) :- !,
880 AllowSep=allow_separation, % TODO: we re-determine the class and used ids below:
881 get_typed_static_definition_with_constants_state2(DefName,TypedExpr,ResBody,DefPos,CS,no_inlining,AllowSep),
882 get_visb_DEFINITION_svg_object(DefName,ResBody,DefPos,CS,SVG_ID,AttrList,Desc),
883 %formatsilent('Adding ~w : ~w (from ~w)~n',[visb_objects,SVG_ID,DefName]),
884 add_visb_object_from_definition(visb_objects, SVG_ID, AttrList, Desc, DefName, DefPos).
885 add_special_json_definition(SpecialClass,DefName,_Type,TypedExpr,UsedTIds,Class,DefPos) :-
886 (get_unique_initial_state_for_visb(Class,DefName,DefPos,UsedTIds,ConstantsState) -> true
887 ; ConstantsState=[]),
888 get_static_visb_state(ConstantsState,FullState), % add static VisB Defs
889 (Class=requires_variables,
890 (get_preference(visb_allow_variables_for_objects,false) ; ConstantsState=[])
891 -> add_warning(visb_visualiser,'Ignoring VisB definition which requires variables:',DefName,DefPos)
892 ; get_visb_DEFINITION_svg_object(DefName,TypedExpr,DefPos,FullState,SVG_ID,AttrList,Desc),
893 %formatsilent('Adding ~w : ~w (from ~w)~n',[SpecialClass,SVG_ID,DefName]),
894 add_visb_object_from_definition(SpecialClass, SVG_ID, AttrList, Desc, DefName, DefPos)
895 ; true).
896
897 is_special_visb_def_name(DefName,visb_updates) :- atom_concat('VISB_SVG_UPDATES',_,DefName).
898 is_special_visb_def_name(DefName,visb_hovers) :- atom_concat('VISB_SVG_HOVERS',_,DefName).
899 is_special_visb_def_name(DefName,visb_objects) :- atom_concat('VISB_SVG_OBJECTS',_,DefName).
900 is_special_visb_def_name(DefName,visb_contents) :- atom_concat('VISB_SVG_CONTENTS',_,DefName).
901 is_special_visb_def_name('VISB_SVG_BOX',visb_box).
902 % TODO: maybe provide VISB_HTML_CONTENTS which appear after the SVG
903
904 % evaluate static VisB defs only once or evaluate expressions in svg_objects and loop bounds
905 eval_static_def(Class,VisBKind,ID,TypedExpr,UsedTIds,StaticValue,VPos) :-
906 get_unique_initial_state_for_visb(Class,ID,VPos,UsedTIds,ConstantsState),
907 evaluate_static_visb_formula(TypedExpr,VisBKind,ID,ConstantsState,StaticValue,VPos).
908
909 % only evaluate statically if possible; no warnings/messages if not possible (just fail)
910 try_eval_static_def(requires_variables,_VisBKind,_ID,_TypedExpr,_UsedTIds,_StaticValue,_VPos) :- !,
911 fail. % do not try to evaluate statically; events will change the variable values anyway
912 try_eval_static_def(Class,VisBKind,ID,TypedExpr,UsedTIds,StaticValue,VPos) :-
913 % TODO: disable messages for multiple constants values; just fail
914 eval_static_def(Class,VisBKind,ID,TypedExpr,UsedTIds,StaticValue,VPos).
915
916 % check if a unique constant value exists for a model
917 get_unique_initial_state_for_visb(requires_nothing,_,_,_,State) :- !, State=[].
918 get_unique_initial_state_for_visb(Class,DefName,DefPos,_,State) :-
919 \+ multiple_concrete_constants_exist,
920 is_concrete_constants_state_id(StateID),!,
921 (Class=requires_variables
922 -> unique_initialisation_id_exists_from(StateID,DefName,DefPos,State)
923 ; visited_expression(StateID,StateTerm),
924 state_corresponds_to_set_up_constants_only(StateTerm,State)).
925 get_unique_initial_state_for_visb(requires_constants,DefName,DefPos,Ids,State) :- Ids \= all,
926 % try and see if all values for Ids are the same; TODO: also support requires_variables
927 is_concrete_constants_state_id(StateID),!,
928 visited_expression(StateID,StateTerm),
929 state_corresponds_to_set_up_constants_only(StateTerm,State),
930 (member(C,Ids), get_texpr_id(C,CstID),
931 other_constant_value_exists_for(CstID,State,StateID)
932 -> ajoin(['Multiple values for constant ',CstID, ' in context of: '],Msg),
933 add_message(visb_visualiser,Msg,DefName,DefPos),fail
934 ; true).
935
936 get_a_constants_state(State,StateID,inline_objects(SingleStateId)) :-
937 get_constants_state_id_for_id(SingleStateId,StateID),!,
938 visited_expression(StateID,StateTerm),
939 state_corresponds_to_set_up_constants_only(StateTerm,State).
940 get_a_constants_state(State,StateID,InlineObjects) :-
941 check_inlining(InlineObjects),
942 is_concrete_constants_state_id(StateID),!,
943 visited_expression(StateID,StateTerm),
944 state_corresponds_to_set_up_constants_only(StateTerm,State).
945
946 check_inlining(no_inlining) :- !.
947 check_inlining(inline_objects(_SingleStateId)) :- !.
948 check_inlining(X) :- add_internal_error('Invalid inlining value:',check_inlining(X)).
949
950 :- use_module(probsrc(store), [lookup_value_for_existing_id/3]).
951 other_constant_value_exists_for(CstID,State,StateId) :-
952 lookup_value_for_existing_id(CstID,State,Val1),
953 is_concrete_constants_state_id(StateId2), StateId2 \= StateId,
954 visited_expression(StateId2,StateTerm2),
955 state_corresponds_to_set_up_constants_only(StateTerm2,State2),
956 lookup_value_for_existing_id(CstID,State2,Val2),
957 Val2 \= Val1.
958
959
960 unique_initialisation_id_exists_from(FromStateId,DefName,DefPos,State) :-
961 transition(FromStateId,_,StateID),!,
962 (transition(FromStateId,_,StateID2),
963 StateID2 \= StateID
964 -> ajoin(['Multiple initialisations exists (state ids ',StateID,',',StateID2,') for: '],Msg),
965 add_message(visb_visualiser,Msg,DefName,DefPos),fail
966 ; true),
967 visited_expression(StateID,StateTerm),
968 state_corresponds_to_initialised_b_machine(StateTerm,State).
969
970 parse_expr_for_visb(Formula,JsonList,Pos,TypedExpr) :-
971 set_gen_parse_errors(JsonList,Pos,GenParseErrors),
972 parse_expr(Formula,TypedExpr,GenParseErrors).
973
974 set_gen_parse_errors(JSonList,Pos,GenParseErrors) :-
975 (get_attr(optional,JSonList,_)
976 -> GenParseErrors=false
977 ; %get_pos_from_list(JSonList,File,Position),
978 GenParseErrors=gen_parse_errors_for(Pos)).
979
980 % ----------------
981
982 % parse and load an individual JSON SVG object listed under svg_objects, e.g, :
983 % {
984 % "svg_class":"rect",
985 % "id":"train_rect",
986 % "x":"0",
987 % "y":"0",
988 % "comment":"..."
989 % },
990 process_json_svg_object(File,json(List)) :-
991 (get_attr_true(ignore,List,File) -> true % ignore this item
992 ; process_json_svg_obj_lst(File,List) -> true).
993
994
995
996 process_json_svg_obj_lst(File,List) :-
997 (force_del_attr_with_pos(svg_class,List,SVG_Class,L1,File,Pos1) -> true % shape: line, rect, ...
998 ; infer_svg_class(List,SVG_Class,File,Pos1)
999 -> add_message(visb_visualiser,'Inferred svg_class: ',SVG_Class,Pos1),L1=List),
1000 force_del_attr(id,L1,ID,L2,File),
1001 (del_attr(comment,L2,Desc,JsonList3) -> true ; Desc = '', JsonList3=L2),
1002 debug_format(19,' Creating new SVG object ~w with id:~w~n',[SVG_Class,ID]),
1003 % TO DO: get remaining attributes and put into Codes so that repeat can be applied to other attributes ?!
1004 maplist(atom_codes,[ID,SVG_Class],Codes),
1005 % first perform all for/repeat loops and then add VisB items
1006 % TODO: we could pre-process all attributes not depending on %0, %1, ...
1007 split_list(svg_attr_has_no_repeat_pattern,JsonList3,StaticJsonList,DynamicJsonList),
1008 % already compute the attributes that do not depend on a repeat pattern:
1009 maplist(get_svg_attr(SVG_Class,File),StaticJsonList,StaticAttrList),
1010 process_repeat(Codes,0, DynamicJsonList, add_visb_json_svg_object(Desc,Pos1,File,StaticAttrList),File).
1011 process_json_svg_obj_lst(File,Term) :-
1012 get_pos_from_list(Term,File,Pos),
1013 add_error(visb_visualiser,'Illegal VisB additional SVG object:',Term,Pos).
1014
1015 infer_svg_class(List,line,File,Pos) :- get_attr_with_pos(x1,List,_,File,Pos),!.
1016 infer_svg_class(List,circle,File,Pos) :- get_attr_with_pos(r,List,_,File,Pos),!.
1017 infer_svg_class(List,rect,File,Pos) :- get_attr_with_pos(height,List,_,File,Pos),!.
1018 infer_svg_class(List,rect,File,Pos) :- get_attr_with_pos(width,List,_,File,Pos),!.
1019 infer_svg_class(List,ellipse,File,Pos) :- get_attr_with_pos(rx,List,_,File,Pos),!. % could also be rect
1020 infer_svg_class(List,text,File,Pos) :- get_attr_with_pos(text,List,_,File,Pos),!.
1021 infer_svg_class(List,g,File,Pos) :- get_attr_with_pos(children,List,_,File,Pos),!.
1022 infer_svg_class(List,use,File,Pos) :- get_attr_with_pos(href,List,_,File,Pos),!. % href can also be used with image, pattern, ...
1023
1024 add_visb_json_svg_object(Desc,Pos1,File,StaticAttrList,[IDC,SVG_ClassC],JsonList) :-
1025 atom_codes(ID,IDC), atom_codes(SVG_Class,SVG_ClassC),
1026 add_debug_message(visb_visualiser,'New object: ',ID,Pos1),
1027 % TODO: split off attributes that depend on variables and transform into visb_items for updates
1028 maplist(get_svg_attr(SVG_Class,File),JsonList,DynamicAttrList),
1029 append(StaticAttrList,DynamicAttrList,AttrList), % the dynamic ones depend on for or repeat loop iterators
1030 %formatsilent('Adding SVG Object ~w with ID ~w (~w): ~w~n',[SVG_Class,ID,Desc,AttrList]),
1031 assert_visb_svg_object(ID,SVG_Class,AttrList,Desc,Pos1).
1032
1033 % assert a new SVG object to be created upon SETUP_CONSTANTS/INITIALISATION:
1034 assert_visb_svg_object(ID,_SVG_Class,_AttrList,_Desc,Pos1) :-
1035 visb_svg_object(ID,_,_,_,_,_Pos0),!,
1036 add_warning(visb_visualiser,'SVG object with same id already created:',ID,Pos1).
1037 assert_visb_svg_object(_ID,_SVG_Class,AttrList,_Desc,Pos1) :-
1038 \+ (AttrList=[] ; AttrList=[_|_]),!,
1039 add_error(visb_visualiser,'SVG objects attributes are not a list:',AttrList,Pos1).
1040 assert_visb_svg_object(ID,SVG_Class,AttrList,Desc,Pos1) :-
1041 check_svg_shape_class(SVG_Class,Pos1),
1042 sort(AttrList,SAttrList),
1043 get_all_children(SAttrList,Children,RestAttrs,Pos1),
1044 (Children = [] -> true
1045 ; svg_shape_can_have_children(SVG_Class) -> true
1046 ; Children = [C1_ID|_], visb_svg_object(C1_ID,title,_,_,_,_) -> true
1047 ; add_message(visb_visualiser,'Children attribute only useful for certain classes such as groups (g) or when adding title objects (as tooltips): ',Children,Pos1)
1048 ),
1049 assertz(visb_svg_object(ID,SVG_Class,RestAttrs,Children,Desc,Pos1)),
1050 maplist(assert_visb_svg_child(ID,Pos1),Children).
1051
1052 % register an SVG ID as child of a group
1053 assert_visb_svg_child(_ParentId,Pos,ChildID) :- visb_svg_child(ChildID,OldParent),!,
1054 ajoin(['SVG object already child of group ',OldParent,': '],Msg),
1055 add_warning(visb_visualiser,Msg,ChildID,Pos).
1056 assert_visb_svg_child(ParentId,Pos,ChildID) :- visb_svg_child(ParentId,ChildID),!, % TODO: full cycle detection
1057 ajoin(['SVG object already parent of group ',ParentId,' (cycle): '],Msg),
1058 add_warning(visb_visualiser,Msg,ChildID,Pos).
1059 assert_visb_svg_child(ParentId,_Pos,ChildID) :-
1060 assertz(visb_svg_child(ChildID,ParentId)).
1061
1062
1063 :- use_module(probsrc(gensym),[gensym/2]).
1064 % we need to translate a title attribute to a separate title object and add it as a child
1065 % see also post_process_visb_item which dispatches title updates to the child object
1066 get_all_children(SAttrList,Children,Rest,Pos) :-
1067 select(svg_attribute(title,Title),SAttrList,SList2),!,
1068 gensym(visb_title,TitleID),
1069 assert_visb_svg_object(TitleID,'title',[svg_attribute(text,Title)],'',Pos),
1070 add_debug_message(visb_visualiser,'Adding virtual title child object: ',TitleID,Pos),
1071 Children=[TitleID|TChilds],
1072 get_children_attribute(SList2,TChilds,Rest,Pos).
1073 get_all_children(SAttrList,Children,Rest,Pos) :-
1074 % get the children explicitly defined by the user:
1075 get_children_attribute(SAttrList,Children,Rest,Pos).
1076
1077 get_children_attribute(SAttrList,Children,Rest,Pos) :-
1078 select(svg_attribute(children,C),SAttrList,R),!,
1079 (is_list(C) -> Children=C
1080 ; add_warning(visb_visualiser,'Children attribute should be a list (of SVG ids): ',C,Pos),
1081 Children=[]),
1082 Rest=R.
1083 get_children_attribute(SAttrList,[],SAttrList,_).
1084
1085 svg_shape_class(circle).
1086 svg_shape_class(ellipse).
1087 svg_shape_class(foreignObject). % can have HTML as children, body, table, tr, th, td
1088 svg_shape_class(g). % group
1089 svg_shape_class(image). % SVG files displayed with <image> cannot be interactive, include dynamic elements with <use>
1090 svg_shape_class(line).
1091 svg_shape_class(path).
1092 svg_shape_class(polygon).
1093 svg_shape_class(polyline).
1094 svg_shape_class(rect).
1095 svg_shape_class(text).
1096 svg_shape_class(title). % useful when adding as children to other objects
1097 svg_shape_class(use).
1098 % Note: one can also create <svg>, ... and HTML tags such as with document.createElementNS
1099
1100 html_class(body).
1101 html_class(li).
1102 html_class(ol).
1103 html_class(table).
1104 html_class(td). % table data
1105 html_class(th). % table header
1106 html_class(tr). % table row
1107 html_class(ul).
1108
1109 svg_shape_can_have_children(g).
1110 svg_shape_can_have_children(foreignObject).
1111 svg_shape_can_have_children(X) :- html_class(X).
1112
1113
1114
1115 check_svg_shape_class(Shape,Pos) :-
1116 (svg_shape_class(Shape) -> true
1117 ; html_class(Shape) -> add_message(visb_visualiser,'HTML entity as svg_class: ',Shape,Pos)
1118 ; add_message(visb_visualiser,'Unknown svg_class shape: ',Shape,Pos)
1119 ).
1120
1121 % check if attribute is not affected by a repeat
1122 svg_attr_has_no_repeat_pattern('='(Attr,AttrVal,_Pos)) :-
1123 Attr \= 'for',
1124 Attr \= 'repeat',
1125 (number(AttrVal) -> true
1126 ; atom(AttrVal),atom_codes(AttrVal,Codes),
1127 nonmember(0'%, Codes)
1128 ).
1129
1130 % get SVG attribute for an svg_object:
1131 get_svg_attr(SVG_Class,File,'='(Attr,AttrVal,Pos),svg_attribute(Attr,Val)) :- !,
1132 construct_prob_pos_term(Pos,File,PosTerm),
1133 get_svg_static_attribute_value(Attr,SVG_Class,AttrVal,Val,PosTerm).
1134 get_svg_attr(_,File,Json,_) :-
1135 get_pos_from_list([Json],File,Position),
1136 add_error(visb_visualiser,'Illegal SVG object attribute',Json,Position),fail.
1137
1138 get_svg_static_attribute_value(Attr,SVG_Class,AttrVal,Nr,Pos) :-
1139 check_is_number_attribute(Attr,SVG_Class,Pos),
1140 \+ is_special_svg_number_form(AttrVal),
1141 !,
1142 (get_number_value(AttrVal,Nr,Attr,Pos) -> true
1143 ; add_error(visb_visualiser,'Illegal number value:',AttrVal,Pos), Nr=0).
1144 get_svg_static_attribute_value(_,_,Val,Val,_).
1145
1146
1147 % detect special SVG number forms, like 50%
1148 is_special_svg_number_form(Atom) :- atom(Atom), atom_codes(Atom,Codes),
1149 special_svg_number(Codes,[]).
1150
1151 :- use_module(probsrc(self_check)).
1152 :- assert_must_succeed(visb_visualiser:special_svg_number("10%",[])).
1153 :- assert_must_succeed(visb_visualiser:special_svg_number("10 %",[])).
1154 :- assert_must_succeed(visb_visualiser:special_svg_number(" 99em ",[])).
1155 :- assert_must_succeed(visb_visualiser:special_svg_number("1.0em",[])).
1156 :- assert_must_fail(visb_visualiser:special_svg_number("10",[])).
1157 :- assert_must_fail(visb_visualiser:special_svg_number("10+nrcols+%0",[])).
1158 special_svg_number --> " ",!, special_svg_number.
1159 special_svg_number --> [X], {digit(X)},!, special_svg_number2.
1160 special_svg_number --> "auto".
1161 special_svg_number2 --> [X], {digit(X)},!, special_svg_number2.
1162 special_svg_number2 --> ".",!, special_svg_number2. % TODO: only allow one dot; + accept e notation?
1163 ?special_svg_number2 --> optws,!, svg_unit,!, optws.
1164
1165 % using info from https://oreillymedia.github.io/Using_SVG/guide/units.html
1166 svg_unit --> "%".
1167 svg_unit --> "ch".
1168 svg_unit --> "cm".
1169 svg_unit --> "em".
1170 svg_unit --> "ex".
1171 svg_unit --> "in".
1172 svg_unit --> "mm".
1173 svg_unit --> "pc".
1174 svg_unit --> "pt".
1175 svg_unit --> "px".
1176 svg_unit --> "deg". % angle units
1177 svg_unit --> "grad".
1178 svg_unit --> "rad".
1179 svg_unit --> "turn".
1180 svg_unit --> "rem". % root em
1181 svg_unit --> "vh". % viewport height unit (1%)
1182 svg_unit --> "vw". % viewport width unit (1%)
1183 svg_unit --> "vmin". % min ov vh, vw
1184 svg_unit --> "vmax". % max ov vh, vw
1185
1186
1187 optws --> " ",!,optws.
1188 optws --> [].
1189
1190 digit(X) :- X >= 48, X =< 57.
1191
1192 is_svg_number_attribute(Attr) :- is_svg_number_attribute(Attr,_).
1193
1194
1195 :- use_module(probsrc(tools_matching), [get_possible_fuzzy_matches_and_completions_msg/3]).
1196 % some checks to see whether the attribute is supported by the given SVG class
1197 check_attribute_is_supported(SVG_Class,DefPos,svg_attribute(Name,_)) :- nonvar(SVG_Class),
1198 check_is_number_attribute(Name,SVG_Class,DefPos),!.
1199 % TODO: check color and other attributes, see also check_attribute_type
1200 check_attribute_is_supported(_,DefPos,svg_attribute(Name,_V)) :- \+ is_svg_attribute(Name),
1201 get_all_svg_attributes(Attrs),
1202 !,
1203 (get_possible_fuzzy_matches_and_completions_msg(Name,Attrs,FMsg)
1204 -> ajoin(['Unknown SVG attribute (did you mean ',FMsg,' ?): '],Msg),
1205 add_warning(visb_visualiser,Msg,Name,DefPos) % create warning, as it is likely we have made an error
1206 ; add_message(visb_visualiser,'Unknown SVG attribute: ',Name,DefPos)).
1207 check_attribute_is_supported(_,_,_).
1208
1209
1210 % succeed if attribute is a number attribute and perform a check the attribute is supported by the class
1211 check_is_number_attribute(Attr,Class,Pos) :-
1212 is_svg_number_attribute(Attr,ClassList),
1213 (nonvar(Class), nonmember(Class,ClassList)
1214 -> (equivalent_attribute(Attr,List2,NewAttr), member(Class,List2)
1215 -> ajoin(['The number attribute ',Attr,' is not supported for SVG class ',Class,', use: '],Msg),
1216 add_warning(visb_visualiser,Msg,NewAttr,Pos)
1217 ; ajoin(['The number attribute ',Attr,' is not supported for this SVG class: '],Msg),
1218 add_warning(visb_visualiser,Msg,Class,Pos)
1219 )
1220 ; true
1221 ).
1222
1223 % optionally rewrite record field to alternative spelling
1224 opt_rewrite_field_name(Name,Res) :-
1225 (alternative_spelling(Name,Alt) -> Res=Alt ; Res=Name).
1226
1227 % these alternatives are useful e.g. in TLA+ without backquote:
1228 alternative_spelling(colour,'color').
1229 alternative_spelling(font_size,'font-size').
1230 alternative_spelling(stroke_opacity,'stroke-opacity').
1231 alternative_spelling(stroke_dasharray,'stroke-dasharray').
1232 %alternative_spelling('stroke-dash-array','stroke-dasharray').
1233 alternative_spelling(stroke_linecap,'stroke-linecap').
1234 alternative_spelling(stroke_width,'stroke-width').
1235
1236
1237
1238 % used to suggest fixing unsupported attributes in SVG objects:
1239 equivalent_attribute(cx,[rect],x).
1240 equivalent_attribute(cy,[rect],y).
1241 equivalent_attribute(x,[circle,ellipse],cx).
1242 equivalent_attribute(x,[line],x1).
1243 equivalent_attribute(y,[circle,ellipse],cy).
1244 equivalent_attribute(y,[line],y1).
1245 equivalent_attribute(rx,[circle],r).
1246 equivalent_attribute(width,[circle],r).
1247 equivalent_attribute(width,[ellipse],rx).
1248 equivalent_attribute(height,[ellipse],ry).
1249
1250
1251
1252
1253 % ----------------
1254
1255 % parse and load an individual JSON VisB item, e.g, :
1256 % {
1257 % "id":"train_info_text",
1258 % "attr":"x",
1259 % "value":"real(train_rear_end)*100.0/real(TrackElementNumber+1)",
1260 % "comment":"move info field above train"
1261 % },
1262 process_json_item(File,json(List)) :-
1263 (get_attr_true(ignore,List,File) -> true % ignore this item
1264 ; process_json_item_lst(File,List) -> true).
1265
1266 process_json_item_lst(File,List) :-
1267 del_attr_with_pos(id,List,ID,L1,File,PosStartOfItem),!,
1268 process_json_item_id(File,L1,ID,PosStartOfItem).
1269 process_json_item_lst(File,Term) :-
1270 %formatsilent('Cannot treat JSON Visb Item:~n ',[]),json_write(user_error,json(Term)),
1271 get_pos_from_list(Term,File,Pos),
1272 add_error(visb_visualiser,'VisB Item has no id attribute:',Term,Pos).
1273
1274 process_json_item_id(File,L1,ID,PosStartOfItem) :-
1275 del_attr(attr,L1,Attr,L2), % VisB has attr and value infos
1276 force_del_attr_with_pos(value,L2,Formula,L3,File,PosFormula),
1277 (get_attr(comment,L3,Desc) -> true ; Desc = ''),
1278 debug_format(19,' Processing id:~w attr:~w : value-formula:~w~n',[ID,Attr,Formula]),
1279 !,
1280 process_visb_item(ID,Attr,Formula,Desc,L3,PosStartOfItem,PosFormula,File).
1281 process_json_item_id(File,L1,ID,PosStartOfItem) :-
1282 (get_attr(SomeSVGAttr,L1,_V), is_svg_attribute(SomeSVGAttr) -> true),
1283 debug_format(19,'Detected new style id:~w SVG attr:~w~n',[ID,SomeSVGAttr]),
1284 !,
1285 include(is_visb_loop_attribute,L1,LoopAttrs),
1286 ((del_attr(comment,L1,Desc,L2) -> true ; Desc = '',L2=L1),
1287 non_det_del_attr_with_pos(SVGATTR,L2,Formula,_,File,PosFormula),
1288 is_visb_item_svg_attribute(PosFormula,SVGATTR,Formula),
1289 debug_format(19,' -> Processing new style id:~w attr:~w : value-formula:~w~n',[ID,SVGATTR,Formula]),
1290 process_visb_item(ID,SVGATTR,Formula,Desc,LoopAttrs,PosStartOfItem,PosFormula,File),
1291 fail
1292 ;
1293 true).
1294 process_json_item_id(_File,_,ID,PosStartOfItem) :-
1295 add_error(visb_visualiser,'Illegal VisB Item without attr and value fields:',ID,PosStartOfItem).
1296
1297 is_visb_loop_attribute('='(Attr,_,_)) :- loop_attribute(Attr).
1298 loop_attribute(for).
1299 loop_attribute(repeat).
1300
1301 is_visb_item_svg_attribute(Pos,Attr,Val) :- \+ loop_attribute(Attr),
1302 (is_svg_attribute(Attr) -> true
1303 ; atomic(Val) -> formatsilent('Treating as SVG attribute: ~w~n',[Attr])
1304 ; add_warning(visb_visualiser,'Ignoring unknown attribute: ',Attr,Pos),
1305 fail
1306 ).
1307
1308 :- use_module(probsrc(tools_strings),[safe_name/2]).
1309 process_visb_item(ID,Attr,Formula,Desc,JSonList,PosStartOfItem,PosFormula,File) :-
1310 maplist(atom_codes,[ID,Attr,Formula],Codes),
1311 % first perform all for/repeat loops and then add VisB items
1312 process_repeat(Codes,0, JSonList, add_visb_item(Desc,PosStartOfItem,PosFormula,File),File).
1313
1314 add_visb_item(Desc,PosStartOfItem,PosFormula,File,[IDC,AttrC,Formula],JsonList) :-
1315 atom_codes(ID,IDC), atom_codes(Attr,AttrC),
1316 set_error_context(visb_error_context(item,ID,Attr,PosFormula)),
1317 (parse_expr_for_visb(Formula,JsonList,PosFormula,TypedExpr)
1318 % TO DO: if optional attribute present: avoid generating errors in b_parse_machine_expression_from_codes
1319 -> assert_visb_item(ID,Attr,TypedExpr,Desc,PosStartOfItem,JsonList,File)
1320 ; get_attr_with_pos(optional,JsonList,_,File,Pos)
1321 -> formatsilent('Ignoring optional VisB item for ~w (lines ~w) due to error in B formula~n',[ID,Pos])
1322 ; ajoin(['Cannot parse or typecheck VisB formula for ',ID,' and attribute ',Attr,':'],Msg),
1323 atom_codes(FF,Formula),
1324 add_error(visb_visualiser,Msg,FF,PosFormula)
1325 ), clear_error_context.
1326
1327
1328 :- use_module(probsrc(bsyntaxtree), [find_identifier_uses/3]).
1329 % assert a VISB item (aka VISB_SVG_UPDATE)
1330 assert_visb_item(ID,Attr,_TypedExpr,_Desc,PosStartOfItem,_,_) :-
1331 visb_item(ID,Attr,_,_,_,Pos2,Meta2),
1332 !,
1333 get_file_name_msg(PosStartOfItem,From1,File1),
1334 (member(override,Meta2)
1335 -> ajoin(['Overriding VisB item',From1,File1,' for same SVG ID ',ID,' and attribute '],Msg),
1336 add_debug_message(visb_visualiser,Msg,Attr,Pos2)
1337 ; ajoin(['Overriding VisB item',From1,File1,' for same SVG ID ',ID,
1338 '. Add an \"override\" attribute to remove this warning. Overriden attribute '],Msg),
1339 add_warning(visb_visualiser,Msg,Attr,Pos2),
1340 % error_context already includes attribute and ID
1341 add_message(visb_visualiser,'Overriding this stored formula for ',ID,PosStartOfItem) % provide detailed info
1342 ).
1343 assert_visb_item(ID,Attr,_TypedExpr,_Desc,PosStartOfItem,_JsonList,_File) :-
1344 illegal_attribute_for_visb_item(ID,Attr),!,
1345 add_warning(visb_visualiser,'This attribute cannot be modified in a VisB item: ',Attr,PosStartOfItem).
1346 assert_visb_item(ID,Attr,TypedExpr,Desc,PosStartOfItem,JsonList,File) :-
1347 (get_attr_true(override,JsonList,File) -> Meta = [override] ; Meta=[]),
1348 % determine_type_of_visb_formula(TypedExpr,_,Class) now does take definitions into account; TODO: save info
1349 find_identifier_uses(TypedExpr,[],UsedIds),
1350 assertz(visb_item(ID,Attr,TypedExpr,UsedIds,Desc,PosStartOfItem,Meta)).
1351
1352 illegal_attribute_for_visb_item(_,children).
1353 illegal_attribute_for_visb_item(_,id).
1354 illegal_attribute_for_visb_item(_,svg_class).
1355
1356
1357 get_file_name_msg(Pos1,' from ',File1) :- extract_tail_file_name(Pos1,File1),!.
1358 get_file_name_msg(_,'',''). % no file info
1359
1360 % ----
1361
1362 get_attr_true(Attr,JsonList,File) :-
1363 get_attr_with_pos(Attr,JsonList,TRUE,File,Pos),
1364 (json_true_value(TRUE) -> true
1365 ; json_false_value(TRUE) -> fail
1366 ; ajoin(['Value for attribute ',Attr,' is not true or false: '],Msg),
1367 add_warning(visb_visualiser,Msg,TRUE,Pos)
1368 ).
1369
1370 json_true_value(true).
1371 json_true_value(1).
1372
1373 json_false_value(false).
1374 json_false_value(0).
1375
1376 % ----------------
1377 % FOR-LOOP / REPEAT processing
1378
1379 %process_repeat( ListOfCodesList, RepCounter, JSonList, FinalCall to be executed repeatedly for each instance)
1380 % RepCounter tells us which of %0, %1, ... should be replaced next
1381
1382 process_repeat(Codes,RepCount,JSonList,FinalCall,File) :-
1383 del_attr_with_pos(FOR_REP,JSonList,Value,RestJsonList,File,ForRepPos),
1384 % find first for or repeat and process it
1385 (FOR_REP=for ; FOR_REP = repeat),
1386 !,
1387 process_first_repeat(FOR_REP,Value,Codes,RepCount,RestJsonList,FinalCall,File,ForRepPos).
1388 process_repeat(FinalCodes,_RepCount,JSonList,FinalCall,_File) :-
1389 % we have processed all for/repeat loops: now perform the final call on the transformed codes
1390 call(FinalCall,FinalCodes,JSonList).
1391
1392
1393 process_first_repeat(for,json(ForList),Codes,RepCount,L2,FinalCall,File,ForPos) :-
1394 !, % we have a for loop like "for": {"from":1, "to":4}
1395 force_get_attr_nr(from,ForList,From,File),
1396 force_get_attr_nr(to,ForList,To,File),
1397 (get_attr_with_pos(step,ForList,StepAttrVal,File,StepPos),
1398 get_number_value(StepAttrVal,Step,step,StepPos)
1399 -> true % there is an explicit step attribute
1400 ; Step=1),
1401 debug_format(19,' -> Iterating %~w from ~w to ~w with step ~w~n',[RepCount,From,To, Step]),
1402 R1 is RepCount+1,
1403 number_codes(RepCount,Pat),
1404 check_between(From,To,Step,ForPos), % check whether step value makes sense
1405 ( between(From,To,Step,IterElem),
1406 number_codes(IterElem,IterElemC), % we will replace the text %Pat by the text of the number IterElem
1407 maplist(replace_codes(Pat,IterElemC),Codes,Codes2),
1408 maplist(replace_in_json(Pat,IterElemC),L2,L3), % replace within other for/repeat loops, but also other attributes
1409 process_repeat(Codes2,R1,L3,FinalCall,File), % now process next loop or finish
1410 fail
1411 ; true).
1412 process_first_repeat(repeat,RepList,Codes,RepCount,L2,FinalCall,File,RepPos) :-
1413 !, % we have a repetition like "repeat": ["tr1","tr2"] or "repeat": [ ["1","2"] , ...]
1414 (RepList=[ L1|_], length(L1,Len)
1415 -> NewRepCount is RepCount+Len, % we have a multi-repeat with list of values to be replaced
1416 RP1 is NewRepCount-1,
1417 debug_format(19,' -> Iterating repat (%~w,...,%~w) over ~w~n',[RepCount,RP1,RepList]),
1418 check_all_same_length(RepList,Len,RepPos)
1419 ; NewRepCount is RepCount+1, % next replacement starts at $(RepCount+1)
1420 debug_format(19,' -> Iterating repeat (%~w) over ~w~n',[RepCount,RepList])
1421 ),
1422 ( member(IterElem,RepList),
1423 multi_replace_codes(RepCount,IterElem,Codes,Codes2),
1424 multi_replace_in_json(IterElem,RepCount,L2,L3), % replace within other for/repeat loops, but also other attributes
1425 process_repeat(Codes2,NewRepCount,L3,FinalCall,File), % now process next loop or finish
1426 fail
1427 ; true).
1428
1429 % replace (possibly)= multiple) patterns at once
1430 multi_replace_in_json([],_,L1,L2) :- !, L2=L1.
1431 multi_replace_in_json([IterElem1|TIT],RepCount,L1,L3) :- !,
1432 number_codes(RepCount,Pat),
1433 safe_name(IterElem1,IterElemC),
1434 %format('Replacing in JSON: ~s -> ~s~n',[Pat,IterElemC]),
1435 maplist(replace_in_json(Pat,IterElemC),L1,L2),
1436 R1 is RepCount+1,
1437 multi_replace_in_json(TIT,R1,L2,L3).
1438 multi_replace_in_json(IterElem,RepCount,L1,L2) :- % an atom, not a list
1439 number_codes(RepCount,Pat),
1440 safe_name(IterElem,IterElemC),
1441 %format('Replacing in JSON: ~s -> ~s~n',[Pat,IterElemC]),
1442 maplist(replace_in_json(Pat,IterElemC),L1,L2).
1443
1444 check_all_same_length(List,ExpectedLen,Pos) :-
1445 nth1(Nr,List,SubList),
1446 (length(SubList,Len) -> Len \= ExpectedLen ; Len='not a list'),
1447 !,
1448 ajoin(['The element number ',Nr,' of the repeat list has not the expected length of ',ExpectedLen,', length is: '],Msg),
1449 add_warning(visb_visualiser,Msg,Len,Pos).
1450 check_all_same_length(_,_,_).
1451
1452 % a version of replace codes which can deal with non-atomic list of replacements ["a","b"]
1453 % Codes is a list of codes lists
1454 multi_replace_codes(_,[],Codes,NewCodes) :- !, NewCodes=Codes.
1455 multi_replace_codes(RepCount,[RepStr1|TRepStr],Codes,NewCodes) :- !,
1456 number_codes(RepCount,Pat),
1457 safe_name(RepStr1,IterElemC),
1458 maplist(replace_codes(Pat,IterElemC),Codes,Codes2),
1459 R1 is RepCount+1, % switch to next pattern variable, i.e., %0 to %1
1460 multi_replace_codes(R1,TRepStr,Codes2,NewCodes).
1461 multi_replace_codes(RepCount,RepStr,Codes,NewCodes) :-
1462 number_codes(RepCount,Pat),
1463 safe_name(RepStr,IterElemC),
1464 maplist(replace_codes(Pat,IterElemC),Codes,NewCodes).
1465
1466 check_between(_,_,Step,ForPos) :- Step =< 0, !,
1467 add_error(visb_visualiser,'The step of a for loop must be positive:',Step,ForPos),fail.
1468 check_between(From,To,Step,ForPos) :- Iters is (To-From)/Step,
1469 Iters > 100000,!,
1470 add_error(visb_visualiser,'Very large for loop:',Iters,ForPos),fail.
1471 check_between(_,_,_,_).
1472
1473
1474 % ----------------
1475
1476 % parse and load VisB events
1477 % A VisB Event looks like:
1478 % {
1479 % "id": "button",
1480 % "event": "toggle_button",
1481 % "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
1482 % { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
1483 % }
1484
1485 process_json_event(File,json(List)) :-
1486 (get_attr_true(ignore,List,File) -> true % ignore this item
1487 ; process_json_event_lst(File,List)
1488 ).
1489
1490 process_json_event_lst(File,List) :-
1491 get_pos_from_list(List,File,Pos),
1492 force_del_attr(id,List,ID,L0,File), % for items it could make sense to not specify an id
1493 (del_attr(event,L0,Event,L1) -> true ; Event='', L1=L0),
1494 (del_attr_with_pos(predicates,L1,Preds,L2,File,PredPos) -> true
1495 ; del_attr_with_pos(preds,L1,Preds,L2,File,PredPos) -> true
1496 ; Preds=[], L2=L1, PredPos=unknown),
1497 (del_attr(hovers,L2,Hovers,L3) -> true ; Hovers=[],L3=L2),
1498 (del_attr(items,L3,EI,L4)
1499 -> (empty_b_event(Event)
1500 -> EnableItems=[],
1501 add_warning(visb_visualiser,'Ignoring enable items; you need to provide an event name: ',ID,Pos)
1502 ; EnableItems=EI)
1503 ; EnableItems=[],L4=L3),
1504 debug_format(19,' Processing id:~w event:~w preds:~w : hovers:~w~n',[ID,Event,Preds,Hovers]),
1505 !,
1506 process_visb_event(ID,Event,Preds,Hovers,EnableItems,L4,File,Pos,PredPos).
1507 process_json_event_lst(File,List) :-
1508 %formatsilent('Cannot treat JSON Visb Event:~n ',[]),json_write(user_error,json(List)),
1509 get_pos_from_list(List,File,Pos),
1510 add_error(visb_visualiser,'Illegal VisB Event:',List,Pos).
1511
1512
1513 process_visb_event(ID,Event,Preds,Hovers,EnableItems,JSonList,File,Pos,PredPos) :-
1514 maplist(atom_codes,[ID,Event],[IDC,EventC]),
1515 % first perform all for/repeat loops and then add VisB events
1516 process_repeat([IDC,EventC,json(Preds),json(EnableItems)|Hovers],0, JSonList, add_visb_json_event(File,Pos,PredPos),File).
1517
1518 :- use_module(probsrc(bmachine), [b_is_operation_name/1]).
1519 add_visb_json_event(File,Pos,_PredPos,[IDC,EventC,json(Preds),json(EnableItems)|Hovers],JsonList) :-
1520 atom_codes(ID,IDC), atom_codes(Event,EventC),
1521 %formatsilent(' adding VisB event ~w -> ~w preds:~w~n',[ID,Event,Preds]),
1522 % TODO: pass predicate position down
1523 add_visb_event(ID,Event,Preds,EnableItems,Hovers,File,Pos,JsonList).
1524
1525 add_visb_event(ID,Event,Preds,EnableItems,Hovers,File,Pos,JsonList) :-
1526 (retract(visb_event(ID,OldEvent,OldPreds,OldTypedPred,OldFile,OldPos))
1527 -> (get_attr_true(override,JsonList,File)
1528 -> ajoin(['Overriding VisB event from file ',OldFile,' for ID: '],Msg),
1529 add_debug_message(visb_visualiser,Msg,ID,Pos),
1530 retractall(visb_hover(ID,_,_,_,_))
1531 ; (OldFile=File
1532 -> ajoin(['No override attribute: adding VisB event ',Event,
1533 ' (first event ',OldEvent,') for ID: '],Msg)
1534 ; ajoin(['No override attribute: adding VisB event ',Event,
1535 ' (first event ',OldEvent,' in file ',OldFile,') for ID: '],Msg)
1536 ),
1537 add_debug_message(visb_visualiser,Msg,ID,Pos),
1538 assertz(auxiliary_visb_event(ID,OldEvent,OldPreds,OldTypedPred,OldPos))
1539 ),
1540 assert_visb_event(ID,Event,Preds,EnableItems,Hovers,File,Pos,JsonList)
1541 % ProB2-UI cannot currently support multiple events associated with the same id
1542 % TODO: merge visb_events if we have no override attribute
1543 ; b_is_operation_name_or_external_subst(Event) ->
1544 assert_visb_event(ID,Event,Preds,EnableItems,Hovers,File,Pos,JsonList)
1545 ; (empty_b_event(Event) ; \+ b_or_z_mode)
1546 -> % for empty event we just want hovers
1547 (Preds = [] -> true
1548 ; add_warning(visb_visualiser,'Ignoring preds for VisB event for SVG ID: ',ID,Pos)
1549 ),
1550 assert_visb_event(ID,Event,[],EnableItems,Hovers,File,Pos,JsonList)
1551 ; get_attr_with_pos(optional,JsonList,_,File,Pos) ->
1552 formatsilent('Ignoring optional VisB event for ~w (lines ~w) due to unknown B operation ~w~n',[ID,Pos,Event])
1553 ; detect_op_call_with_paras(Event,OpName) ->
1554 add_warning(visb_visualiser,'Ignoring parameters provided in event; use predicates to specify parameters: ',Event,Pos),
1555 assert_visb_event(ID,OpName,Preds,EnableItems,Hovers,File,Pos,JsonList)
1556 ; ajoin(['Unknown B operation ', Event, ' in VisB for SVG ID: '],Msg),
1557 add_warning(visb_visualiser,Msg,ID,Pos)
1558 ).
1559
1560 b_is_operation_name_or_external_subst(OpName) :- b_is_operation_name(OpName).
1561 b_is_operation_name_or_external_subst(Special) :- special_operation(Special).
1562
1563 % maybe we should provide those via the external substitution interface:
1564 % these are all schedulers which choose among existing enabled operations in some manner
1565 special_operation('MCTS_AUTO_PLAY').
1566 special_operation('RANDOM_ANIMATE').
1567 % maybe other special names like random_animate with nr of steps, LTL until, ...
1568 special_operation_enabled('MCTS_AUTO_PLAY',_,_,_) :- mcts_auto_play_available.
1569 special_operation_enabled('RANDOM_ANIMATE',_,_,_). % TODO: check if a transition exists
1570
1571 % detect operation call with parameters
1572 detect_op_call_with_paras(Event,OpName) :- atom_codes(Event,Codes), parse_op_call_name(OpC,Codes,_),!,
1573 atom_codes(OpName,OpC),
1574 b_is_operation_name(OpName).
1575
1576 parse_op_call_name([X|T]) --> alpha(X), parse_op_call_name2(T).
1577 parse_op_call_name2([]) --> "(".
1578 parse_op_call_name2([H|T]) --> alphadigit(H), parse_op_call_name2(T).
1579
1580 alpha(X) --> [X],{X>=97, X=<122}.
1581 alphadigit(X) --> [X], ({X>=97,X=<122} ; {X>=65, X=<90} ; {X=95} ; {X>=48, X=<57}).
1582
1583 empty_b_event('').
1584
1585 assert_visb_event(ID,Event,Preds,EnableItems,Hovers,File,Pos,JsonList) :-
1586 check_additional_args(JsonList,File),
1587 construct_pre_post_predicate(ID,Event,Preds,TypedPred,Pos),
1588 % This does not deal with %shiftKey, %pageX, %metaKey...
1589 assertz(visb_event(ID,Event,Preds,TypedPred,File,Pos)),
1590 (get_json_hover(ID,Hovers,HoverID,Attr,EnterVal,ExitVal,File),
1591 assert_visb_hover(ID,HoverID,Attr,EnterVal,ExitVal),fail
1592 ; true),
1593 % now process any additional items with disabled and enabled values
1594 (EnableItems \= [],
1595 maplist(process_enabling_item_in_visb_event(ID,Event,File),EnableItems,VisBEnableList)
1596 -> (debug_mode(off) -> true
1597 ; format('Associating enabling/disabling list with event ~w and predicate:',[Event]),
1598 translate:print_bexpr(TypedPred),nl),
1599 assert(visb_event_enable_list(Event,TypedPred,VisBEnableList,File,Pos))
1600 ; true
1601 ).
1602
1603 get_json_hover(OriginID,HoverList,ID,Attr,EnterVal,LeaveVal,File) :-
1604 member(json(Hover),HoverList),
1605 force_del_attr(attr,Hover,Attr,H2,File),
1606 force_del_attr_with_pos(enter,H2,EV,H3,File,EnterPos),
1607 force_del_attr_with_pos(leave,H3,LV,H4,File,ExitPos),
1608 (is_svg_number_attribute(Attr) % we evaluate number attributes
1609 -> get_number_value(EV,EnterVal,Attr,EnterPos),
1610 get_number_value(LV,LeaveVal,Attr,ExitPos)
1611 ; EnterVal=EV, LeaveVal=LV % return string as is; TODO: also evaluate other attributes
1612 ),
1613 (get_attr(id,H4,ID) -> true ; ID=OriginID).
1614
1615
1616 assert_visb_hover(TriggerID,SVG_ID,Attr,EnterVal,ExitVal) :-
1617 assert(visb_hover(TriggerID,SVG_ID,Attr,EnterVal,ExitVal)),
1618 (visb_has_hovers(TriggerID) -> true ; assert(visb_has_hovers(TriggerID))),
1619 debug_format(19,'Adding hover for ~w : ~w.~w -> ~w <- ~w~n',[TriggerID,SVG_ID,Attr,EnterVal,ExitVal]).
1620
1621
1622 % process items in event which get translated to enabling/disabling predicates
1623 % "items":[ {"attr":"stroke-width","enabled":"10", "disabled":"1"} ]
1624 process_enabling_item_in_visb_event(ID,Event,File,json(JsonList),
1625 visb_enable_item(SvgID,Attr,EnabledValExpr,DisabledValExpr,PosAttr)) :-
1626 force_del_attr_with_pos(attr,JsonList,Attr,L2,File,PosAttr),
1627 force_del_attr_with_pos('enabled',L2,EnVal,L3,File,EPos),
1628 force_del_attr_with_pos('disabled',L3,DisVal,L4,File,DPos),
1629 (del_attr(id,L4,SvgID,L5) -> true ; SvgID=ID, L4=L5),
1630 atom_codes(EnVal,EC),
1631 parse_expr_for_visb(EC,L5,EPos,EnabledValExpr),
1632 atom_codes(DisVal,DC),
1633 parse_expr_for_visb(DC,L5,DPos,DisabledValExpr),
1634 (debug_mode(off) -> true
1635 ; translate_bexpression_with_limit(EnabledValExpr,30,EVS),
1636 translate_bexpression_with_limit(DisabledValExpr,30,DVS),
1637 formatsilent('Enabling item for event ~w and SVG ID ~w and attribute ~w : ~w <-> ~w~n',[Event,SvgID,Attr,EVS,DVS])
1638 ),
1639 (visb_item(SvgID,Attr,_,_,_Desc,DuplicatePos,_)
1640 -> (extract_span_description(DuplicatePos,DuplPos) -> true ; DuplPos=DuplicatePos),
1641 ajoin(['VisB conflict for SVG ID ',SvgID,' and attribute ',Attr,
1642 '. Conflict between VisB item (',DuplPos,') and VisB enable/disable entry for event: '],Msg),
1643 add_warning(visb_visualiser,Msg,Event,PosAttr)
1644 ; true).
1645
1646
1647
1648
1649 valid_additional_attributes(comment).
1650 valid_additional_attributes(description).
1651 valid_additional_attributes(optional).
1652 valid_additional_attributes(override).
1653
1654 % check if there are additional unprocessed args and generate a warning
1655 check_additional_args(JsonList,File) :-
1656 get_attr_with_pos(Attr,JsonList,_,File,Pos),
1657 \+ valid_additional_attributes(Attr),
1658 add_warning(visb_visualiser,'Ignoring unknown JSON field: ',Attr,Pos),
1659 fail.
1660 check_additional_args(_,_).
1661
1662 :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2]).
1663 % construct a pre-post typed predicate for a VisB Event
1664 construct_pre_post_predicate(SvgID,OpName,Preds,TypedPred,Pos) :-
1665 set_error_context(visb_error_context(event,SvgID,OpName,Pos)),
1666 maplist(construct_pre_post_pred(OpName,Pos),Preds,TL),
1667 clear_error_context,
1668 conjunct_predicates(TL,TypedPred).
1669
1670 :- use_module(probsrc(bmachine), [b_parse_machine_operation_pre_post_predicate/5]).
1671 construct_pre_post_pred(OpName,Pos,String,TypedPred) :- empty_b_event(OpName),!,
1672 add_error(visb_visualiser,'Cannot parse VisB event predicate without event name:',String,Pos),
1673 TypedPred = b(truth,pred,[]).
1674 construct_pre_post_pred(OpName,Pos,String,TypedPred) :-
1675 atom_codes(String,Codes), replace_special_patterns(Codes,RCodes),
1676 %format("Replaced : ~S~n",[RCodes]),
1677 get_visb_extra_scope(ExtraScope),
1678 (b_parse_machine_operation_pre_post_predicate(RCodes,ExtraScope,TypedPred,OpName,gen_parse_errors_for(Pos))
1679 -> true
1680 ; add_error(visb_visualiser,'Error for VisB event predicate:',String,Pos),
1681 TypedPred = b(truth,pred,[])
1682 ).
1683
1684 % replace special patterns by dummy values to avoid error messages in ProB2-UI
1685 replace_special_patterns([],[]).
1686 replace_special_patterns([37|T],Res) :- !, % percentage sign %
1687 replace_aux(T,Res).
1688 replace_special_patterns([H|T],[H|RT]) :- replace_special_patterns(T,RT).
1689
1690 replace_aux(Input,Res) :- replace_pat(PAT,Replacement),
1691 append(PAT,T,Input),!,
1692 append(Replacement,ResT,Res),
1693 replace_special_patterns(T,ResT).
1694 replace_aux(Input,[37|Res]) :- replace_special_patterns(Input,Res).
1695
1696 replace_pat("shiftKey","FALSE").
1697 replace_pat("metaKey","FALSE").
1698 replace_pat("pageX","0").
1699 replace_pat("pageY","0").
1700
1701
1702
1703 % small utils:
1704 % ----------------
1705
1706 % a variation of between/3 with a step argument
1707 between(From,To,_,_) :- From > To, !,fail.
1708 between(From,_,_,From).
1709 between(From,To,Step,Elem) :- F1 is From+Step, between(F1,To,Step,Elem).
1710
1711 :- use_module(probsrc(tools_strings),[is_simple_classical_b_identifier_codes/1]).
1712 :- use_module(probsrc(preferences), [reset_temporary_preference/2,temporary_set_preference/3]).
1713 parse_expr(ExprCodes,TypedExpr,_GenParseErrors) :-
1714 is_simple_classical_b_identifier_codes(ExprCodes),
1715 atom_codes(DefID,ExprCodes),
1716 visb_definition(DefID,Type,_DefFormula,Class,_VPos,_),
1717 !,
1718 TypedExpr = b(identifier(DefID),Type,[type_of_formula(Class)]).
1719 parse_expr(ExprCodes,TypedExpr,GenParseErrors) :-
1720 temporary_set_preference(allow_arith_operators_on_reals,true,CHNG),
1721 get_visb_extra_scope(ExtraScope),
1722 % formatsilent('Parsing: ~s (extra ids: ~w)~n',[ExprCodes,ExtraScope]), start_ms_timer(T1),
1723 call_cleanup(bmachine:b_parse_machine_expression_from_codes_with_prob_ids(ExprCodes,ExtraScope,TypedExpr,
1724 GenParseErrors),
1725 reset_temporary_preference(allow_arith_operators_on_reals,CHNG)).
1726 %stop_ms_walltimer_with_msg(T1,'parsing: ').
1727 % TODO: we could share a machine parameter M like in prob2_interface
1728 % so that b_type_expression_for_full_b_machine will load machine only once
1729 % cf b_type_open_predicate_for_full_b_machine
1730
1731 determine_type_of_visb_formula(b(_,_,[type_of_formula(Class)]),all,Res) :- !,
1732 Res = Class. % generated by VisB, TODO: store UsedTIds in type_of_formula(.)
1733 determine_type_of_visb_formula(TypedExpr,TIds,Class) :-
1734 determine_type_of_formula_with_visb_defs(TypedExpr,TIds,Class).
1735
1736 %check for used_ids inside TypedExpr an see what type of visb_definition are used
1737 determine_type_of_formula_with_visb_defs(TypedExpr,TIds,ResClass) :-
1738 determine_type_of_formula(TypedExpr,TIds,Class1), % compute class w/o knowledge of VisB definitions
1739 (class_more_general_than(Class2,Class1),
1740 required_by_visb_def(TIds,Class2) -> Class=Class2
1741 ; Class=Class1),
1742 (Class=requires_variables -> ResClass=Class
1743 ; expression_requires_state(TypedExpr) -> ResClass = requires_variables
1744 ; ResClass=Class).
1745
1746 :- use_module(probsrc(bsyntaxtree),[map_over_bexpr/2]).
1747 :- use_module(probsrc(external_functions),[external_function_requires_state/1]).
1748 expression_requires_state(TypedExpr) :-
1749 (map_over_bexpr(sub_expression_requires_state,TypedExpr) -> true ; fail).
1750 % TODO: should we also check is_not_declarative/1 ?
1751 sub_expression_requires_state(external_pred_call(P,_)) :- external_function_requires_state(P).
1752 sub_expression_requires_state(external_function_call(P,_)) :- external_function_requires_state(P).
1753
1754
1755 class_more_general_than(requires_variables,requires_nothing).
1756 class_more_general_than(requires_variables,requires_constants).
1757 class_more_general_than(requires_constants,requires_nothing).
1758
1759 required_by_visb_def(TIds,Class) :-
1760 member(TID,TIds), get_texpr_id(TID,ID),visb_definition(ID,_,_,Class,_,_).
1761
1762
1763 get_visb_extra_scope([identifier(ExtraIDs)]) :-
1764 get_visb_extra_identifiers(ExtraIDs).
1765 get_visb_extra_identifiers(ExtraIDs) :-
1766 findall(b(identifier(ID),Type,[visb_generated]),visb_definition(ID,Type,_,_,_,_),ExtraIDs).
1767
1768 % replace a pattern code prefixed by % by another code list
1769 % we can either replace in json(List) or a CodesList
1770 replace_codes(Pattern,RepStr,json(List),json(NewList)) :- !, % used for hovers
1771 maplist(replace_in_json(Pattern,RepStr),List,NewList).
1772 replace_codes(_,_,[],NewCodes) :- !, NewCodes=[].
1773 replace_codes(Pattern,RepStr,Codes,NewCodes) :- Codes = [_|_],!,
1774 replace_pat(Pattern,RepStr,NewCodes,Codes,[]).
1775 replace_codes(Pattern,RepStr,Codes,NewCodes) :-
1776 add_internal_error('Illegal argument for replace_codes:',replace_codes(Pattern,RepStr,Codes,NewCodes)),
1777 NewCodes=Codes.
1778
1779 % within a repeat we have atoms or lists of atoms
1780 replace_in_repeat(Pattern,RepStr,Atom,NewAtom) :- atom(Atom), !,
1781 atom_codes(Atom,AC),
1782 replace_pat(Pattern,RepStr,NewCodes,AC,[]),
1783 atom_codes(NewAtom,NewCodes).
1784 replace_in_repeat(Pattern,RepStr,Atoms,NewAtoms) :- Atoms = [_|_],!,
1785 maplist(replace_in_repeat(Pattern,RepStr),Atoms,NewAtoms).
1786 replace_in_repeat(_,_,A,A).
1787
1788
1789 replace_in_json(Pattern,RepStr,'='(for,json(List),Pos),'='(for,json(NewList),Pos)) :- !, % nested loops
1790 maplist(replace_in_json(Pattern,RepStr),List,NewList).
1791 replace_in_json(Pattern,RepStr,'='(repeat,List,Pos),'='(repeat,NewList,Pos)) :- !, % nested loops
1792 maplist(replace_in_repeat(Pattern,RepStr),List,NewList).
1793 replace_in_json(Pattern,RepStr,'='(Attr,Val,Pos),'='(Attr,NewVal,Pos)) :- atom(Val),!, % from hovers
1794 replace_atom(Pattern,RepStr,Val,NewVal).
1795 replace_in_json(Pattern,RepStr,'='(children,Vals,Pos),'='(children,NewVals,Pos)) :- maplist(atom,Vals),!,
1796 maplist(replace_atom(Pattern,RepStr),Vals,NewVals).
1797 replace_in_json(Pattern,RepStr,Val,NewVal) :- atom(Val),!, % from preds (list of atoms)
1798 replace_atom(Pattern,RepStr,Val,NewVal).
1799 replace_in_json(Pattern,RepStr,json(List),json(NewList)) :- !,
1800 maplist(replace_in_json_attrs(Pattern,RepStr ),List,NewList).
1801 replace_in_json(_,_,Pair,Pair). % number (no replacement necessary) or nested structure
1802
1803 replace_atom(Pattern,RepStr,Val,NewVal) :-
1804 atom_codes(Val,Codes),
1805 replace_pat(Pattern,RepStr,NewCodes,Codes,[]),
1806 atom_codes(NewVal,NewCodes). % TO DO: keep as codes for efficiency
1807
1808 % item enable lists inside VisB events
1809 replace_in_json_attrs(Pattern,RepStr,'='(Attr,Val,Pos),'='(Attr,NewVal,Pos)) :- atom(Val),!, % from items inside events
1810 % attributes are id, optional, attr, enabled, disabled
1811 atom_codes(Val,Codes),
1812 replace_pat(Pattern,RepStr,NewCodes,Codes,[]),
1813 atom_codes(NewVal,NewCodes). % TO DO: keep as codes for efficiency
1814 replace_in_json_attrs(_,_,Pair,Pair).
1815
1816 :- assert_must_succeed((visb_visualiser: replace_pat("0","_1_",Res,"ab%0cd",[]), Res == "ab_1_cd")).
1817 :- assert_must_succeed((visb_visualiser: replace_pat("0","",Res,"ab%0%0cd%0",[]), Res == "abcd")).
1818 % dcg utility to replace %Pat by NewStr constructing Res
1819 replace_pat(Pat,NewStr,Res) --> "%", Pat, !, {append(NewStr,TR,Res)}, replace_pat(Pat,NewStr,TR).
1820 replace_pat(Pat,RepStr,[H|T]) --> [H],!, replace_pat(Pat,RepStr,T).
1821 replace_pat(_,_,[]) --> [].
1822
1823
1824 % small JSON utils:
1825 % ----------------
1826
1827 get_attr(Attr,List,Val) :- member('='(Attr,Val,_),List).
1828 get_attr_with_pos(Attr,List,Val,File,Pos) :-
1829 El = '='(Attr,Val,_),
1830 member(El,List),
1831 get_pos_from_list([El],File,Pos).
1832
1833 del_attr(Attr,List,Val,Rest) :- select('='(Attr,Val,_Pos),List,Rest).
1834 %del_attr_with_pos(Attr,List,Val,Rest,Pos) :- select('='(Attr,Val,Pos),List,Rest).
1835 del_attr_with_pos(Attr,List,Val,Rest,File,PosTerm) :- select('='(Attr,Val,From-To),List,Rest),!,
1836 PosTerm = src_position_with_filename_and_ec(From,1,To,1,File).
1837 non_det_del_attr_with_pos(Attr,List,Val,Rest,File,PosTerm) :- select('='(Attr,Val,From-To),List,Rest),
1838 PosTerm = src_position_with_filename_and_ec(From,1,To,1,File).
1839
1840 force_del_attr(Attr,List,Val,Rest,File) :- force_del_attr_with_pos(Attr,List,Val,Rest,File,_).
1841
1842 force_del_attr_with_pos(Attr,List,Val,Rest,File,PosTerm) :- select('='(Attr,Val,From-To),List,Rest),!,
1843 %TODO: we would ideally want to extract the exact column position of Val, for this we need to extend the JSON parser first
1844 PosTerm = src_position_with_filename_and_ec(From,1,To,1,File).
1845 force_del_attr_with_pos(Attr,List,_,_,File,_) :- get_pos_from_list(List,File,Pos),!,
1846 add_error(visb_visualiser,'The JSON object has no attribute:',Attr,Pos),fail.
1847
1848 construct_prob_pos_term(From-To,File,PosTerm) :- !,
1849 PosTerm = src_position_with_filename_and_ec(From,1,To,1,File).
1850 construct_prob_pos_term(Pos,_,Pos).
1851
1852 force_get_attr_nr(Attr,List,Nr,File) :-
1853 force_del_attr_with_pos(Attr,List,AttrVal,_,File,Pos),!,
1854 get_number_value(AttrVal,Nr,Attr,Pos).
1855
1856 get_number_value(AttrVal,Nr,Attr,Pos) :-
1857 (number(AttrVal) -> Nr=AttrVal
1858 ; atom(AttrVal),
1859 atom_codes(AttrVal,AttrValC),
1860 parse_expr(AttrValC,TypedExpr,gen_parse_errors_for(Pos)),
1861 determine_type_of_visb_formula(TypedExpr,UsedTIds,Class)
1862 % Class = requires_nothing, requires_constants, requires_variables
1863 ->
1864 (Class = requires_variables
1865 -> ajoin(['The JSON formula for the attribute"',Attr,
1866 '" must not depend on variables:'],Msg),
1867 add_error(visb_visualiser,Msg,AttrVal,Pos),fail
1868 ; Class = requires_constants,
1869 \+ is_concrete_constants_state_id(_)
1870 -> ajoin(['The JSON formula for the attribute"',Attr,
1871 '" depends on constants which have not been set up (via SETUP_CONSTANTS):'],Msg),
1872 add_error(visb_visualiser,Msg,AttrVal,Pos),fail
1873 ; Class = requires_constants,
1874 multiple_concrete_constants_exist,
1875 ajoin(['The JSON formula for the attribute"',Attr,
1876 '" depends on constants and multiple solutions for SETUP_CONSTANTS exist:'],Msg),
1877 add_warning(visb_visualiser,Msg,AttrVal,Pos),fail
1878 ; get_texpr_type(TypedExpr,Type),
1879 is_number_type(Type)
1880 -> eval_static_def(Class,'VisB attribute',Attr,TypedExpr,UsedTIds,ResVal,Pos),
1881 get_number_from_bvalue(ResVal,Nr)
1882 ; get_texpr_type(TypedExpr,Type),
1883 % it could produce a string which is a number; we could try and convert to a number
1884 ajoin(['The type ',Type,' of the JSON value formula for the attribute "',Attr,
1885 '" is not a number:'],Msg),
1886 add_error(visb_visualiser,Msg,AttrVal,Pos),fail
1887 )
1888 ; ajoin(['The JSON value for the attribute "',Attr,'" cannot be parsed as a number:'],Msg),
1889 add_error(visb_visualiser,Msg,AttrVal,Pos),fail).
1890
1891 is_number_type(integer).
1892 is_number_type(real).
1893 :- use_module(probsrc(kernel_reals),[is_real/2]).
1894 :- use_module(probsrc(custom_explicit_sets),[singleton_set/2]).
1895 get_number_from_bvalue(int(Nr),Res) :- !, Res=Nr.
1896 get_number_from_bvalue(Term,Res) :- is_real(Term,Nr),!,Res=Nr.
1897
1898
1899 get_pos_from_list([H|T],File,RPos) :- H='='(_,_,From-_), last([H|T],'='(_,_,_-To)),!,
1900 RPos=src_position_with_filename_and_ec(From,1,To,1,File).
1901 get_pos_from_list(_,File,File). % should we provide another term
1902
1903 % ----------------------------------
1904
1905 :- use_module(probsrc(b_global_sets),[add_prob_deferred_set_elements_to_store/3]).
1906 :- use_module(probsrc(tools),[b_string_escape_codes/2]).
1907
1908 % computing updates to SVG for a given StateId:
1909 % predicate to obtain required setAttribute changes to visualise StateId
1910 % looks up visb_item facts but also evaluates VISB_SVG_UPDATE definitions
1911 get_change_attribute_for_state(StateId,SvgID,SvgAttribute,Value) :-
1912 set_error_context(checking_context('VisB:','computing attributes for state')),
1913 get_expanded_bstate(StateId,ExpandedBState),
1914 set_context_state(StateId,get_change_attribute_for_state), % also sets it for external functions
1915 % TODO: also set history so that get_current_history in external_functions is more reliable
1916 call_cleanup(get_change_aux(StateId,ExpandedBState,SvgID,SvgAttribute,Value),
1917 (clear_context_state,clear_error_context)).
1918
1919 get_change_aux(StateId,ExpandedBState,SvgID,SvgAttribute,Value) :-
1920 get_aux2(StateId,ExpandedBState,SvgID0,SvgAttribute0,Value0,DefPos),
1921 post_process_visb_item(SvgID0,SvgAttribute0,Value0,DefPos,SvgID,SvgAttribute,Value).
1922 get_aux2(StateId,ExpandedBState,SvgID,SvgAttribute,Value,DefPos) :-
1923 % first get updates from DEFINITIONS which usually return sets of records
1924 get_svg_object_updates_from_definitions(ExpandedBState,SvgID,SvgAttribute,Value,DefPos),
1925 debug_format(19,' VISB_SVG_UPDATE ~w:~w = ~w (in state ~w)~n',[SvgID,SvgAttribute,Value,StateId]).
1926 get_aux2(StateId,ExpandedBState,SvgID,SvgAttribute,Value,Pos) :-
1927 get_visb_item_formula(SvgID,SvgAttribute,Formula,Pos,ExpandedBState),
1928 % TODO: if UsedIds=[] only set attribute once, if it requires_only_constants : ditto
1929 evaluate_visb_formula(Formula,'VisB item',SvgID,ExpandedBState,FValue,Pos),
1930 %b_value_to_string(FValue,Value),
1931 extract_attr_value(SvgAttribute,FValue,Value,Pos),
1932 debug_format(19,' VisB item ~w:~w = ~w (in state ~w)~n',[SvgID,SvgAttribute,Value,StateId]).
1933
1934 % post-process certain items, like title to adapt the value and id:
1935 % SVG does not support a title attribute; we need a title child and set its text attribute
1936 post_process_visb_item(SvgID,title,Value,Pos,NewID,text,Value) :-
1937 visb_svg_object(SvgID,_SVG_Class,_RestAttrs,Children,_Desc,_Pos1),
1938 (Children=[TitleID|_], visb_svg_object(TitleID,title,_,_,_,_)
1939 -> NewID=TitleID,
1940 debug_format(9,'Redirecting title update for ~w to child object ~w~n',[SvgID,TitleID])
1941 ; add_warning(visb_visualiser,'Could not find title child object, be sure to define a static title attribute for SVG object: ',SvgID,Pos),
1942 fail
1943 ),!.
1944 post_process_visb_item(SvgID,Attr,Value,_,SvgID,Attr,Value).
1945
1946 % ------------------
1947
1948 % convert B value to Json String
1949 b_value_to_string(string(SValue),Res) :- !, Res=SValue. % What about quoting,...?
1950 b_value_to_string(FValue,Res) :-
1951 translate_bvalue_to_codes(FValue,ValCodes),
1952 atom_codes(Res,ValCodes).
1953
1954 % attributes for which we convert pairs to the concatenation of strings
1955 is_id_or_text_attribute(id).
1956 is_id_or_text_attribute('trigger_id').
1957 is_id_or_text_attribute('trigger-id').
1958 is_id_or_text_attribute(A) :- is_text_attribute(A).
1959 % children
1960 is_text_attribute('text').
1961 is_text_attribute('transform').
1962 is_text_attribute('event'). % for VISB_SVG_EVENTS
1963 is_text_attribute('predicate'). % for VISB_SVG_EVENTS
1964 is_text_attribute('svg_class').
1965
1966
1967 b_value_to_id_string(Val,String) :- b_val_to_id_string_aux(Val,add_underscore,String).
1968 b_value_to_text_string(Val,String) :- b_val_to_id_string_aux(Val,no_underscore,String).
1969
1970 % a special string conversion which e.g., allows to use things like ("ab",2) as id which gets translated to ab2
1971 % also useful for text attributes
1972 b_val_to_id_string_aux(string(SValue),_,Res) :- !, Res=SValue.
1973 b_val_to_id_string_aux((A,B),Add,Res) :- !,
1974 b_val_to_id_string_aux(A,Add,VA), b_val_to_id_string_aux(B,Add,VB),
1975 (Add=add_underscore
1976 -> atom_concat('_',VB,VB1) % introduce separator; in case we have things like numbers so that (12,3) /= (1,23)
1977 ; VB1=VB % for fields like predicate, transform, ... we do not want additional underscores
1978 ),
1979 atom_concat(VA,VB1,Res).
1980 b_val_to_id_string_aux(Set,Add,Res) :- singleton_set(Set,El),!, b_val_to_id_string_aux(El,Add,Res).
1981 % TODO: maybe convert sequence of values using conc
1982 b_val_to_id_string_aux(FValue,_,Res) :-
1983 translate_bvalue_to_codes(FValue,ValCodes),
1984 atom_codes(Res,ValCodes).
1985
1986 % get either a regular VisB item or an item associated with a VisB event and its enabled status
1987 get_visb_item_formula(SvgID,SvgAttribute,Formula,Pos,_ExpandedBState) :-
1988 visb_item(SvgID,SvgAttribute,Formula,_UsedIds,_Desc,Pos,_). % regular VisB item
1989 get_visb_item_formula(SvgID,SvgAttribute,Formula,Pos,ExpandedBState) :- % item within VisB event
1990 visb_event_enable_list(OpName,TypedPred,EnableList,_,ItemPos),
1991 debug_format(19,'Checking enabledness of VisB event ~w~n',[OpName]),
1992 (check_enabled(OpName,TypedPred,ExpandedBState,ItemPos)
1993 -> Formula=EnabledValExpr
1994 ; Formula=DisabledValExpr
1995 ),
1996 member(visb_enable_item(SvgID,SvgAttribute,EnabledValExpr,DisabledValExpr,Pos), EnableList).
1997
1998 check_enabled(OpName,Pred,ExpandedBState,Pos) :-
1999 special_operation(OpName),!,
2000 special_operation_enabled(OpName,Pred,ExpandedBState,Pos).
2001 check_enabled(OpName,Pred,ExpandedBState,Pos) :-
2002 b_is_operation_name(OpName),
2003 execute_operation_by_predicate_in_state_with_pos(ExpandedBState,OpName,Pred,_OpTerm,_NewState,Pos).
2004
2005
2006 get_expanded_bstate(StateId,ExpandedBState) :-
2007 \+ b_or_z_mode,!,
2008 StateId \= root,
2009 % in XTL mode we need to access the state via external functions like STATE_PROPERTY
2010 get_static_visb_state([],ExpandedBState).
2011 get_expanded_bstate(StateId,ExpandedBState) :-
2012 visited_expression(StateId,State),
2013 state_corresponds_to_initialised_b_machine(State,BState),
2014 debug_format(19,'Adding VisB definitions to state: ~w~n',[StateId]),
2015 add_prob_deferred_set_elements_to_store(BState,BState2,visible), % add prob_ids
2016 findall(visb_definition(DefID,Type,DefFormula,Class,VPos,Special),
2017 visb_definition(DefID,Type,DefFormula,Class,VPos,Special),DefList),
2018 eval_defs(DefList,BState2,ExpandedBState).
2019
2020
2021 :- use_module(probsrc(b_interpreter), [ b_compute_expression_nowf/7]).
2022
2023 evaluate_static_visb_formula(Formula,Kind,Nr,InState,ResValue,Pos) :-
2024 get_static_visb_state(InState,StaticState),
2025 evaluate_visb_formula(Formula,Kind,Nr,StaticState,ResValue,Pos).
2026
2027 evaluate_visb_formula(Formula,Kind,Nr,BState2,ResValue,Pos) :-
2028 % add_message(visb,'Evaluating: ',Kind:Nr,Pos), debug:nl_time, %set_prolog_flag(profiling,on), print_profile,
2029 (b_compute_expression_nowf(Formula,[],BState2,ResValue,Kind,Nr,Pos) -> true
2030 ; add_error(visb_visualiser,'Evaluation of VisB formula failed:',Formula,Pos),
2031 fail).
2032
2033 % evaluate VisB definitions in order one by one, adding values to state
2034 eval_defs([],State,State).
2035 eval_defs([visb_definition(ID,_,TypedExpr,_Class,VPos,Special)|T],State0,State2) :-
2036 (Special \= regular_def
2037 -> State1=State0 % ignore special defs; they are processed separately
2038 ; b_compute_expression_nowf(TypedExpr,[],State0,ResValue,'VisB definition',ID,VPos),
2039 State1 = [bind(ID,ResValue)|State0], % store value for later definitions and VisB items
2040 (debug_mode(off) -> true
2041 ; translate_bvalue_to_codes(ResValue,RC),
2042 formatsilent(' VisB definition ~w == ~s~n',[ID,RC]))
2043 ),
2044 eval_defs(T,State1,State2).
2045
2046 % check if we have a static value for a VisB definition:
2047 visb_def_static_value(DefID,Value) :- visb_definition(DefID,_,b(value(Value),_,_),Class,_,_),
2048 (Class = requires_nothing ; Class = requires_constants). % probably we do not need to check this, as we have value/1
2049
2050 get_static_visb_state(InState,FullState) :-
2051 findall(bind(DefID,Value),visb_def_static_value(DefID,Value),FullState,InState).
2052 % TO DO: get state with deferred_set_elements,...
2053
2054 % ----------------------------------
2055
2056 % generate a stand-alone HTML file with a visualisation for all states in the list
2057
2058 generate_visb_html(StateIds,File,Options) :-
2059 safe_open_file(File,write,Stream,[encoding(utf8)]),
2060 generate_html_to_stream(StateIds,Stream,[html_file/File|Options]),
2061 close(Stream).
2062
2063 generate_visb_html_to_codes(StateIds,Options,Codes) :-
2064 with_open_stream_to_codes(
2065 generate_html_to_stream(StateIds,Stream,Options),
2066 Stream,Codes,[]).
2067
2068
2069 % generate an HTML file to visualise the given StateId
2070 generate_html_to_stream(StateIds,Stream,Options) :-
2071 set_id_namespace_prefix_for_states(StateIds,Options),
2072 write_visb_template('visb_template_header.html',Stream),
2073 format(Stream,' <script>~n',[]),
2074 retractall(js_generated_function(_)),
2075 length(StateIds,Len),
2076 maplist(gen_visb_visualise_function(Stream,Options,Len),StateIds),
2077 gen_runAll_script(Stream,StateIds),
2078 format(Stream,' </script>~n~n',[]),
2079 gen_registerHovers_scipt(Stream,Options),
2080 write_visb_template('visb_template_middle.html',Stream),
2081 (member(no_header,Options) -> true
2082 ; format(Stream,' <button type="button" class="collapsible collapsible-style">SVG Visualisation</button>~n',[]),
2083 format(Stream,' <div text-align="left">~n',[])
2084 ),
2085 %format(Stream,' <fieldset> <legend>Visualisation:</legend>~n',[]), % comment in to draw a border
2086 (StateIds = [SingleStateId] -> GenForState=SingleStateId ; GenForState=root),
2087 copy_svg_file_and_gen_objects(Stream,GenForState,_SVGinlined),
2088 % TO DO: avoid creating JS code below if _SVGinlined
2089 %format(Stream,' </fieldset>~n',[]),
2090 format(Stream,' </div>~n',[]),
2091 (Len>1
2092 -> %format(Stream,'~n<h3>Run Trace</h3>~n',[]),
2093 format(Stream,' <button type="button" class="collapsible-style">Replay Trace</button>~n',[]),
2094 format(Stream,' <div class="coll-content-vis">~n',[]),
2095 format(Stream,' <button onclick="backStep()">« Back</button>~n',[]),
2096 format(Stream,' <button onclick="forwardStep()">Forward »</button>~n',[]),
2097 format(Stream,' <button onclick="runAll(10)">Run Trace (10 ms delay)</button>~n',[]),
2098 format(Stream,' <button onclick="runAll(500)">Run Trace (500 ms delay)</button>~n',[]),
2099 % We could decide to provide an option/preference for generating the visb_debug_messages field:
2100 % (check that ProB2-UI also generates this text field)
2101 format(Stream,' <br><text id="visb_debug_messages" class="visb-messages"> </text>~n',[]),
2102 format(Stream,' </div>~n',[]),
2103 format(Stream,' <progress id="trace_meter" min="0" max="~w" value="0"></progress>~n',[Len]) % progress of trace replay; note <meter> element also works
2104 ; true
2105 ),
2106 % generate a table with variables, constants, ...
2107 gen_state_table(Stream,Options,StateIds),
2108 gen_source_code_section(Stream,Options),
2109 % generate a table with the saved trace steps:
2110 (Len>1 -> gen_trace_table(Stream,StateIds) ; true),
2111 write_version_info(Stream,Options),
2112 (last(StateIds,Last),get_state_and_action(Last,LastId,_,_)
2113 -> format(Stream,' <script> visualise~w(~w); </script>~n',[LastId,Len])
2114 % show the visualisation of the last state by default
2115 ; true % trace is empty, there is no last item
2116 ),
2117 write_visb_template('visb_template_footer.html',Stream),
2118 clear_id_namespace_prefix.
2119
2120 % -----------------
2121
2122 :- use_module(library(system),[ datime/1]).
2123 :- use_module(probsrc(tools_strings),[number_codes_min_length/3]).
2124 :- use_module(probsrc(tools),[gen_relative_path/3]).
2125 :- use_module(probsrc(version),[version_str/1]).
2126 :- use_module(probsrc(specfile),[currently_opened_file/1, get_internal_representation/1]).
2127 write_version_info(_,Options) :-
2128 member(no_version_info,Options),!.
2129 write_version_info(Stream,Options) :-
2130 version_str(Str),datime(datime(Yr,Mon,Day,Hr,Min,_Sec)),
2131 number_codes_min_length(Min,2,MC),
2132 format(Stream,' <button type="button" class="collapsible-style">Info</button>~n',[]),
2133 format(Stream,'<div class="coll-content-vis visb-messages">~n',[]),
2134 format(Stream,'Generated on ~w/~w/~w at ~w:~s using <a href="https://prob.hhu.de/">ProB</a> version ~w~n',[Day,Mon,Yr,Hr,MC,Str]),
2135 (currently_opened_file(File)
2136 -> (File=package(Type) ->
2137 format(Stream,'<br>Main specification package: ~w~n',[Type])
2138 ; atom(File), get_relative_path(File,Options,Suffix) ->
2139 format(Stream,'<br>Main specification file: ~w',[Suffix]),
2140 format_file_info(Stream,File)
2141 ; format(Stream,'<br>Unknown main specification file: ~w~n',[File])
2142 )
2143 ; true),
2144 (b_machine_name(MainName)
2145 -> format(Stream,'<br>Main specification name: ~w~n',[MainName]) ; true),
2146 (visb_file_loaded(JSONFile,_,ModLocTime),
2147 JSONFile \= ''
2148 -> get_relative_path(JSONFile,Options,JSuffix),
2149 format(Stream,'<br>Main VisB JSON file: ~w',[JSuffix]),
2150 format_modified_info(Stream,ModLocTime),
2151 (get_non_empty_svg_file(SVGFile,ModLocTime2)
2152 -> get_relative_path(SVGFile,Options,SSuffix),
2153 format(Stream,'<br>VisB SVG file: ~w',[SSuffix]),
2154 format_modified_info(Stream,ModLocTime2)
2155 ; true
2156 )
2157 ; true).
2158
2159 get_non_empty_svg_file(SVGFile,ModLocTime2) :-
2160 visb_svg_file(RelFile,SVGFile,_,_,ModLocTime2),
2161 RelFile \= ''.
2162
2163 format_file_info(Stream,File) :-
2164 catch(file_property(File, modify_localtime, ModLocTime),
2165 E,
2166 (add_message(visb_visualiser,'Could not obtain modification time for file: ',E), fail)),
2167 !,
2168 format_modified_info(Stream,ModLocTime).
2169 format_file_info(Stream,_) :- nl(Stream).
2170
2171 format_modified_info(Stream,ModLocTime) :-
2172 format(Stream,' (modified on ',[]),
2173 format_datime(Stream,ModLocTime),
2174 format(Stream,')~n',[]).
2175
2176 format_datime(Stream,datime(Yr,Mon,Day,Hr,Min,_Sec)) :-
2177 number_codes_min_length(Min,2,MC),
2178 format(Stream,'~w/~w/~w at ~w:~s',[Day,Mon,Yr,Hr,MC]).
2179
2180 get_relative_path(File,Options,RelPath) :-
2181 member(html_file/HF,Options),
2182 absolute_file_name(File,AF,[]),
2183 absolute_file_name(HF,AHF,[]),
2184 !,
2185 gen_relative_path(AF,AHF,RelPath). % only print relative information
2186 get_relative_path(File,_,File).
2187
2188
2189 % -----------------
2190
2191 % gen a table with all the individual steps of the trace
2192 gen_trace_table(Stream,StateIds) :-
2193 length(StateIds,Len),
2194 %format(Stream,'~n<h3>Trace (length=~w)</h3>~n',[Len]),
2195 format(Stream,' <button type="button" class="collapsible-style">Trace (length=~w)</button>~n',[Len]),
2196 format(Stream,'<div class="coll-content-vis">~n',[]),
2197 (member(Obj,StateIds), get_state_and_action(Obj,_,_,DescStr), DescStr \= ''
2198 -> Opt=with_description ; Opt=no_description),
2199 gen_trace_table2(Stream,StateIds,Opt).
2200
2201 gen_trace_table2(Stream,StateIds,no_description) :-
2202 format(Stream,' <table> <tr> <th>Nr</th> <th>Event</th> <th>Target State ID</th> </tr>~n',[]),
2203 nth1(Nr,StateIds,Obj),
2204 get_state_and_action(Obj,StateId,ActionStr,_),
2205 (visited_state_corresponds_to_initialised_b_machine(StateId)
2206 -> format(Stream,'~n <tr id="row~w" onclick="visualise~w(~w)"><td>~w</td><td style="cursor:pointer">~w</td><td><button onclick="visualise~w(~w);">State ~w</button></td></tr>~n',
2207 [Nr,StateId,Nr,Nr,ActionStr,StateId,Nr,StateId])
2208 ; format(Stream,'~n <tr id="row~w"><td>~w</td><td style="cursor:not-allowed">~w</td><td>State ~w</td></tr>~n',
2209 [Nr,Nr,ActionStr,StateId])
2210 ),
2211 fail.
2212 gen_trace_table2(Stream,StateIds,with_description) :-
2213 format(Stream,' <table> <tr> <th>Nr</th> <th>Event</th> <th>Description</th> <th>Target State ID</th> </tr>~n',[]),
2214 nth1(Nr,StateIds,Obj),
2215 get_state_and_action(Obj,StateId,ActionStr,DescStr),
2216 html_escape(ActionStr,EAS),
2217 html_escape(DescStr,EDS),
2218 (visited_state_corresponds_to_initialised_b_machine(StateId)
2219 -> format(Stream,'~n <tr id="row~w" onclick="visualise~w(~w)"><td>~w</td><td style="cursor:pointer">~w</td><td>~w</td><td><button onclick="visualise~w(~w);">State ~w</button></td></tr>~n',
2220 [Nr,StateId,Nr,Nr,EAS,EDS,StateId,Nr,StateId])
2221 ; format(Stream,'~n <tr id="row~w"><td>~w</td><td style="cursor:not-allowed">~w</td><td>~w</td><td>State ~w</td></tr>~n',
2222 [Nr,Nr,EAS,EDS,StateId])
2223 ),
2224 fail.
2225 gen_trace_table2(Stream,_,_) :-
2226 format(Stream,' </table>~n </div>~n',[]).
2227
2228
2229 % utility to allow passing information about name of event/operation/action leading to state
2230 get_state_and_action(change_to_state_via_action(StateId,ActionStr,DescStr),StateId,ActionStr,DescStr) :- !.
2231 get_state_and_action(StateId,StateId,'','').
2232
2233 % -----------------
2234
2235 % inline provided svg file into html file:
2236 % second argument is either root or a particular state id for which the SVG file is to be created
2237 % the last argument is static_svg_inlined if all SVG objects were "inlined" into a single
2238 % SVG object (rather than via JavaScript functions to create the objects)
2239 copy_svg_file_and_gen_objects(Stream,_,static_svg_not_inlined) :- visb_svg_file(_,File,_,_,_), file_exists(File),
2240 !,
2241 safe_open_file(File,read,StreamIn,[encoding(utf8)]),
2242 copy_stream(StreamIn,Stream),
2243 close(StreamIn),
2244 (get_visb_contents_def(Contents,DefPos,static_svg_not_inlined)
2245 -> add_message(visb_visualiser,'Copying VISB_SVG_CONTENTS *after* SVG file: ',File,DefPos),
2246 format(Stream,'~w~n',[Contents])
2247 ; true
2248 ),
2249 gen_new_svg_objects(Stream).
2250 copy_svg_file_and_gen_objects(_,_,_) :-
2251 visb_svg_file(File,AFile,_,Pos,_),
2252 File \= '',
2253 add_error(visb_visualiser,'The specified VisB SVG file does not exist:',AFile,Pos),
2254 fail.
2255 copy_svg_file_and_gen_objects(Stream,SingleStateId,static_svg_inlined) :- % copy an empty SVG stub
2256 visb_file_loaded(_,_,_),!,
2257 write_default_svg_contents(Stream,inline_objects(SingleStateId)).
2258 copy_svg_file_and_gen_objects(_,_,static_svg_not_inlined). % no SVG required; we have no items or events: probably just want HTML export of variables,...
2259
2260 % get_code is faster than get_char or read_line for larger SVG files
2261 copy_stream(StreamIn,StreamOut) :-
2262 get_code(StreamIn, Code),
2263 (Code = -1 -> true
2264 ; put_code(StreamOut,Code),
2265 copy_stream(StreamIn,StreamOut)
2266 ).
2267
2268 % TODO: precompile and always assert as visb_special_definition:
2269 get_visb_contents_def(Contents,DefPos,InlineObjects) :-
2270 get_and_eval_special_definition('VISB_SVG_CONTENTS',_DefName,visb_contents,DefPos,ResValue,InlineObjects),
2271 b_value_to_string(ResValue,Contents).
2272
2273 % get a definition either from B DEFINITIONS section, or if not present from the VisB JSON special definition list
2274 get_and_eval_special_definition(Prefix,DefName,JSONBackup,DefPos,ResValue,InlineObjects) :-
2275 (b_sorted_b_definition_prefixed(expression,Prefix,DefName,DefPos),
2276 b_get_typed_definition(DefName,[variables],TBody)
2277 ;
2278 visb_special_definition(JSONBackup,DefName,_Type,TBody,_Class,DefPos)
2279 ),
2280 % TODO: warn if we use static SVG
2281 get_typed_static_definition_with_constants_state2(DefName,TBody,
2282 Body,DefPos,ConstantsState,InlineObjects,no_separation),
2283 evaluate_visb_formula(Body,DefName,'',ConstantsState,ResValue,DefPos).
2284
2285 write_default_svg_contents(Stream,InlineObjects) :-
2286 (visb_empty_svg_box_height_width(H,W,ViewBox) -> true ; H=400, W=400, ViewBox=''),
2287 format(Stream,'<svg xmlns=\"http://www.w3.org/2000/svg\"~n',[]),
2288 (ViewBox=''
2289 -> format(Stream,' width="~w" height="~w" viewBox="0 0 ~w ~w" >~n',[W,H,W,H])
2290 ; format(Stream,' width="~w" height="~w" viewBox="~w" >~n',[W,H,ViewBox])
2291 ),
2292 ( get_visb_contents_def(Contents,_,InlineObjects),
2293 format(Stream,'~w~n',[Contents]),
2294 fail
2295 ; true),
2296 (InlineObjects=inline_objects(StateID) -> inline_new_svg_objects(Stream,StateID) ; true),
2297 format(Stream,'</svg>~n',[]).
2298
2299 % get SVG file contents in case no SVG file is provided by user
2300 get_visb_default_svg_file_contents(Codes) :-
2301 with_open_stream_to_codes(
2302 write_default_svg_contents(Stream,inline_objects(root)),
2303 % allow inlining for groups and title children in ProB2-UI
2304 Stream,
2305 Codes, []).
2306
2307 % -----------------
2308
2309 % create a script to add all additional SVG objects
2310 gen_new_svg_objects(_) :- \+ visb_svg_object(_,_,_,_,_,_),!.
2311 gen_new_svg_objects(Stream) :-
2312 format(Stream, '<script>~n',[]),
2313 format(Stream, ' const svg = document.querySelector("svg");~n',[]),
2314 format(Stream, ' const svgns = "http://www.w3.org/2000/svg";~n',[]),
2315 (gen_new_svg_object(Stream,svg_root,_),fail ; true),
2316 format(Stream, '</script>~n',[]).
2317
2318 % generate JS script to create an individual new object
2319 gen_new_svg_object(Stream,ParentID,SVGID) :-
2320 visb_svg_object(SVGID,SVG_Class,AttrList,Children,_,_Pos),
2321 (ParentID=svg_root
2322 -> \+ visb_svg_child(SVGID,_) % only generate root svg objects that have no parents
2323 ; true),
2324 add_svg_id_prefix(SVGID,SVGID2),
2325 format(Stream,' if(document.getElementById("~w") == null) {~n',[SVGID2]),
2326 format(Stream,' var new___obj = document.createElementNS(svgns,"~w");~n',[SVG_Class]),
2327 format(Stream,' new___obj.setAttribute("~w","~w");~n',[id,SVGID2]),
2328 maplist(gen_new_svg_attr(Stream,SVGID2),AttrList),
2329 (ParentID \= svg_root
2330 -> format(Stream,' document.getElementById("~w").appendChild(new___obj);~n',[ParentID])
2331 ; format(Stream,' svg.appendChild(new___obj);~n',[])
2332 ),
2333 format(Stream,' }~n',[]),
2334 maplist(gen_new_svg_object(Stream,SVGID),Children). % we can now generate the children
2335
2336 gen_new_svg_attr(Stream,_SVGID,svg_attribute(text,Val)) :- !,
2337 format(Stream,' new___obj.textContent = "~w";~n',[Val]).
2338 gen_new_svg_attr(Stream,_SVGID,svg_attribute(Attr,Val)) :-
2339 format(Stream,' new___obj.setAttribute("~w","~w");~n',[Attr,Val]).
2340
2341 % instead of creating a script to create new SVG objects,
2342 % create an inlined textual XML representation of the objects
2343 % this can be used to obtain a static SVG file which can be modified in an editor
2344 % and then later used instead of the VISB_SVG_OBJECTS definitions
2345 inline_new_svg_objects(Stream,StateId) :-
2346 get_dynamic_svgid_attributes_for_state(StateId,DynUpdateList), % compute updates only once
2347 visb_svg_object(SVGID,_,_,_,_,_), % lookup static SVG object
2348 \+ visb_svg_child(SVGID,_), % children will be created in the scope of their parent
2349 inline_new_svg_object(Stream,StateId,DynUpdateList,0,unknown,SVGID),
2350 fail.
2351 inline_new_svg_objects(_,_).
2352
2353 inline_new_svg_object(Stream,StateId,DynUpdateList,IndentLevel,ParentPos,SVGID) :-
2354 (visb_svg_object(SVGID,SVG_Class,StaticAttrList,Children,_,Pos) -> true % lookup static SVG object
2355 ; add_warning(visb_visualiser,'Unknown SVG child object: ',SVGID,ParentPos),fail
2356 ),
2357 add_svg_id_prefix(SVGID,SVGID2), % for Jupyter
2358 indent_ws(Stream,IndentLevel),
2359 format(Stream,' <~w id="~w"',[SVG_Class,SVGID2]),
2360 (member(svgid_updates(SVGID,DynAttrList),DynUpdateList) % TODO: use avl_fetch
2361 -> override_attributes(StaticAttrList,DynAttrList,AttrList)
2362 ; AttrList=StaticAttrList),
2363 maplist(format_new_svg_attr(Stream,SVGID,TextContent),AttrList),
2364 (TextContent='' -> true ; true), % set Text variable to empty if unbound
2365 format(Stream,'>~w',[TextContent]),
2366 IL1 is IndentLevel+1,
2367 (Children=[] -> true
2368 ; nl(Stream),
2369 maplist(inline_new_svg_object(Stream,StateId,DynUpdateList,IL1,Pos),Children)),
2370 format(Stream,'</~w>~n',[SVG_Class]), % end marker
2371 fail.
2372 inline_new_svg_object(_,_,_,_,_,_).
2373
2374
2375 indent_ws(_,X) :- X<1,!.
2376 indent_ws(Stream,X) :- write(Stream,' '), X1 is X-1, indent_ws(Stream,X1).
2377
2378 % combinde svg_attribute/2 terms from two sorted lists, giving precedence to second list
2379 override_attributes([],L,R) :- !, R=L.
2380 override_attributes(L,[],R) :- !, R=L.
2381 override_attributes([svg_attribute(Attr1,Val1)|T1],[svg_attribute(Attr2,Val2)|T2],[svg_attribute(Attr3,Val3)|T3]) :-
2382 (Attr1=Attr2
2383 -> Attr3=Attr1, Val3=Val2, % dynamic value Val2 takes precedence
2384 override_attributes(T1,T2,T3)
2385 ; Attr1 @< Attr2 -> Attr3=Attr1, Val3=Val1, override_attributes(T1,[svg_attribute(Attr2,Val2)|T2],T3)
2386 ; Attr3=Attr2, Val3=Val2, override_attributes([svg_attribute(Attr1,Val1)|T1],T2,T3)
2387 ).
2388
2389 % get dynamic svg_attribute/2 list for a given state and SVG ID
2390 get_dynamic_svgid_attributes_for_state(root,List) :- !, List=[].
2391 get_dynamic_svgid_attributes_for_state(StateId,UpdateList) :-
2392 get_visb_attributes_for_state(StateId,List),
2393 sort(List,SList),
2394 group_set_attr(SList,'$$UNKNOWN$$',_,UpdateList).
2395
2396 group_set_attr([],_,[],[]).
2397 group_set_attr([set_attr(SvgID,Attr,Val)|T],SvgID,[svg_attribute(Attr,Val)|T1],T2) :- !,
2398 group_set_attr(T,SvgID,T1,T2).
2399 group_set_attr([set_attr(SvgID,Attr,Val)|T],_OldID,[],[svgid_updates(SvgID,L)|T2]) :- % a new SVGId is encountered
2400 group_set_attr([set_attr(SvgID,Attr,Val)|T],SvgID,L,T2).
2401
2402
2403 format_new_svg_attr(Stream,SVGID,Text,svg_attribute(Attr,Val)) :- % TODO: text content
2404 (Attr=text
2405 -> (Text=Val -> true ; add_warning(inline_new_svg_objects,'Multiple text attributes for: ',SVGID))
2406 ; number(Val) ->
2407 format(Stream,' ~w="~w"',[Attr,Val])
2408 ; escape_value_to_codes_for_js(Val,ECodes) ->
2409 format(Stream,' ~w="~s"',[Attr,ECodes])
2410 ; add_internal_error('Cannot escape: ',escape_value_to_codes_for_js(Val,_)),
2411 format(Stream,' ~w="~w"',[Attr,Val])
2412 ).
2413
2414
2415 :- dynamic id_namespace_prefix/1.
2416 % prefix that can be useful for Jupyter notebooks so that for each state we have a different namespace
2417 % can also be useful for exporting a trace into a single HTML
2418 % TODO: does not work with JSON and SVG files
2419
2420 :- use_module(probsrc(gensym),[gensym/2]).
2421 set_id_namespace_prefix_for_states(_,Options) :-
2422 member(id_namespace_prefix(Pre),Options),!,
2423 (Pre = auto
2424 -> gensym('visb',ID), % for Jupyter this relies on the fact the gensym is *not* reset when loading another spec
2425 atom_concat(ID,'.',Prefix)
2426 ; Prefix=Pre
2427 ), set_id_namespace_prefix(Prefix).
2428 set_id_namespace_prefix_for_states(_,_).
2429
2430 set_id_namespace_prefix(Prefix) :- clear_id_namespace_prefix,
2431 assert(id_namespace_prefix(Prefix)).
2432 clear_id_namespace_prefix :- retractall(id_namespace_prefix(_)).
2433
2434 % add a namespace prefix to an SVG ID
2435 add_svg_id_prefix(SvgID,Res) :- id_namespace_prefix(Prefix),!,
2436 % option where we prefix all Ids with a namespace for Jupyter to combine multiple SVGs in single HTML page
2437 atom_concat(Prefix,SvgID,Res).
2438 add_svg_id_prefix(SvgID,SvgID).
2439
2440 % only add for known objects
2441 opt_add_svg_id_prefix(SvgID,Res) :- id_namespace_prefix(Prefix),
2442 visb_svg_object(SvgID,_,_,_,_,_),!, % only add prefix for SVG objects we know about (that were created by VisB)
2443 % option where we prefix all Ids with a namespace for Jupyter to combine multiple SVGs in single HTML page
2444 atom_concat(Prefix,SvgID,Res).
2445 opt_add_svg_id_prefix(SvgID,SvgID).
2446
2447 % -----------------
2448
2449 :- dynamic js_generated_function/1.
2450
2451 % define a visualise JS function to set the attributes for the given StateId
2452 gen_visb_visualise_function(Stream,Options,Len,Obj) :-
2453 get_state_and_action(Obj,StateId,_ActionStr,_DescStr),
2454 \+ js_generated_function(StateId),!,
2455 assertz(js_generated_function(StateId)),
2456 visb_visualise_function_aux(Stream,Options,Len,StateId).
2457 gen_visb_visualise_function(_,_,_,_).
2458
2459 visb_visualise_function_aux(Stream,_,Len,StateId) :-
2460 format(Stream,' function visualise~w(stepNr) {~n',[StateId]),
2461 (Len>1 -> format(Stream,' setAttr("trace_meter","value",stepNr);~n',[]) ; true),
2462 format(Stream,' setAttr("visb_debug_messages","text","Step "+stepNr+"/~w, State ID: ~w");~n',[Len,StateId]),
2463 get_change_attribute_for_state(StateId,SvgID,SvgAttribute,Value),
2464 opt_add_svg_id_prefix(SvgID,SvgID2),
2465 (escape_value_to_codes_for_js(Value,ECodes)
2466 -> format(Stream,' setAttr("~w","~w","~s");~n',[SvgID2,SvgAttribute,ECodes])
2467 ; format(Stream,' setAttr("~w","~w","~w");~n',[SvgID2,SvgAttribute,Value])
2468 ),
2469 fail.
2470 visb_visualise_function_aux(Stream,Options,_,StateId) :-
2471 member(show_variables(VarList),Options),
2472 get_state_value_change(StateId,ID,ResValCodes),
2473 show_var_in_visb(VarList,ID),
2474 format(Stream,' setAttr("bVar_~w","text","~s");~n',[ID,ResValCodes]),
2475 fail.
2476 visb_visualise_function_aux(Stream,Options,_,StateId) :-
2477 member(show_events(OpList),Options),
2478 get_state_value_enabled_operation_status(StateId,OpID,Enabled,ResValCodes,TransStr),
2479 show_var_in_visb(OpList,OpID),
2480 format(Stream,' setAttr("bOperation_~w","text","~s");~n',[OpID,ResValCodes]),
2481 (Enabled=true -> BGCol=white ; BGCol='#f1f1f1'),
2482 format(Stream,' setAttr("row_bOperation_~w","bgcolor","~w");~n',[OpID,BGCol]),
2483 escape_value_to_codes_for_js(TransStr,ETS),
2484 format(Stream,' setAttr("name_bOperation_~w","text","~s");~n',[OpID,ETS]),
2485 % TO DO: highlight next event in trace, but then function needs one more parameter
2486 fail.
2487 visb_visualise_function_aux(Stream,_,Len,_) :- Len>1, % only then trace table is generated
2488 format(Stream,' highlightRow(stepNr);~n',[]),
2489 fail.
2490 visb_visualise_function_aux(Stream,_,_Len,_) :-
2491 format(Stream,' }~n',[]).
2492
2493 escape_value_to_codes_for_js(Atom,ECodes) :- atom(Atom),
2494 atom_codes(Atom,Codes), b_string_escape_codes(Codes,ECodes).
2495
2496
2497 :- use_module(probsrc(tools),[string_escape/2]).
2498 % gen a runAll script to run all events
2499 gen_runAll_script(Stream,StateIds) :-
2500 format(Stream,' async function runAll(delay) {~n',[]),
2501 length(StateIds,Len),
2502 nth1(Nr,StateIds,Obj),
2503 get_state_and_action(Obj,SId,ActionStr,DescStr), string_escape(ActionStr,EAS), string_escape(DescStr,EDS),
2504 format(Stream,' visualise~w(~w);~n',[SId,Nr]),
2505 format(Stream,' setAttr("visb_debug_messages","text","Step: ~w/~w, State ID: ~w, Event: ~w ~w");~n',[Nr,Len,SId,EAS,EDS]),
2506 format(Stream,' await sleep(delay);~n',[]),
2507 fail.
2508 gen_runAll_script(Stream,_) :-
2509 format(Stream,' }~n',[]).
2510
2511 % generate JS script to register hovers
2512 gen_registerHovers_scipt(Stream,Options) :- \+ visb_has_hovers(_),
2513 nonmember(debugging_hovers,Options),
2514 !, % no hover exists
2515 format(Stream,' <script> function registerHovers() {} </script>~n',[]).
2516 gen_registerHovers_scipt(Stream,Options) :-
2517 (member(debugging_hovers,Options) -> GenDebug=true ; GenDebug=false), % gen debugging hovers
2518 % Jquery is no longer required:
2519 %format(Stream,' <script src="https://ajax.googleapis.com/ajax/libs/jquery/3.6.0/jquery.min.js"></script>~n',[]),
2520 format(Stream,' <script>~n',[]),
2521 format(Stream,' function registerHovers() {~n',[]),
2522 format(Stream,' var obj;~n',[]),
2523 visb_has_hovers(SVGID), % only generate hover function if necessary; TODO: examine other IDs for GenDebug
2524 opt_add_svg_id_prefix(SVGID,SVGID2),
2525 format(Stream,' obj = document.getElementById("~w");~n',[SVGID2]),
2526 format(Stream,' obj.onmouseover = function(ev){~n',[]),
2527 (visb_hover(SVGID,ID,Attr,EnterVal,_),
2528 opt_add_svg_id_prefix(ID,ID2),
2529 (GenDebug=false -> true
2530 ; format(Stream,' setAttr("~w","~w","SVG ID: ~w")~n',[visb_debug_messages,text,SVGID2])),
2531 format(Stream,' setAttr("~w","~w","~w")~n',[ID2,Attr,EnterVal]), fail ;
2532 format(Stream,' };~n',[])
2533 ),
2534 format(Stream,' obj.onmouseout = function(){~n',[]),
2535 (visb_hover(SVGID,ID,Attr,_,LeaveVal),
2536 opt_add_svg_id_prefix(ID,ID2),
2537 (GenDebug=false -> true
2538 ; format(Stream,' setAttr("~w","~w","~w")~n',[visb_debug_messages,text,'...'])
2539 ),
2540 format(Stream,' setAttr("~w","~w","~w")~n',[ID2,Attr,LeaveVal]), fail ;
2541 format(Stream,' };~n',[])
2542 ),
2543 fail.
2544 gen_registerHovers_scipt(Stream,_) :-
2545 format(Stream,' }~n </script>~n',[]).
2546
2547
2548 % ----------------------------------
2549
2550 :- use_module(probsrc(translate),[set_unicode_mode/0, unset_unicode_mode/0]).
2551 :- use_module(probsrc(state_space), [get_action_trace_with_limit/2, get_state_id_trace/1]).
2552
2553 generate_visb_html_for_history_with_source(File) :-
2554 generate_visb_html_for_history(File,
2555 [show_constants(all),show_sets(all),show_variables(all),show_events(all),show_source]).
2556 generate_visb_html_for_history_with_vars(File) :-
2557 generate_visb_html_for_history(File,[show_constants(all),show_sets(all),show_variables(all),show_events(all)]).
2558 generate_visb_html_for_history(File) :-
2559 generate_visb_html_for_history(File,[]).
2560 generate_visb_html_for_history(File,Options) :-
2561 start_ms_timer(Timer),
2562 get_state_id_trace(T),
2563 T = [root|StateIds],
2564 set_unicode_mode,
2565 call_cleanup(get_action_trace_with_limit(120,Actions), % TODO: also get description of JSON traces
2566 unset_unicode_mode),
2567 reverse(Actions,FActions),
2568 combine_state_and_actions(StateIds,[root|StateIds],FActions,List),
2569 generate_visb_html(List,File,Options),
2570 stop_ms_walltimer_with_msg(Timer,'exporting history to VisB HTML file: ').
2571
2572 :- use_module(probsrc(specfile),[get_operation_description_for_transition/3]).
2573 combine_state_and_actions([],_,[],[]).
2574 combine_state_and_actions([StateId|TS],[PrevId|TP],[action(ActionStr,ATerm)|TA],
2575 [change_to_state_via_action(StateId,ActionStr,Desc)|TRes]) :-
2576 (get_operation_description_for_transition(PrevId,ATerm,D) -> Desc=D ; Desc=''),
2577 combine_state_and_actions(TS,TP,TA,TRes).
2578
2579 generate_visb_html_for_current_state(File) :-
2580 generate_visb_html_for_current_state(File,[show_variables(all)]).
2581 generate_visb_html_for_current_state(File,Options) :-
2582 start_ms_timer(Timer),
2583 current_state_id(ID),
2584 generate_visb_html([ID],File,Options),
2585 stop_ms_walltimer_with_msg(Timer,'exporting current state to VisB HTML file: ').
2586 generate_visb_html_codes_for_states(StateIds,Options,Codes) :-
2587 generate_visb_html_to_codes(StateIds,Options,Codes). % write to codes list
2588
2589 % ------------------------------
2590
2591 :- use_module(probsrc(specfile),[b_or_z_mode/0]).
2592 :- use_module(probsrc(bmachine), [b_get_machine_variables/1, b_get_machine_constants/1, b_top_level_operation/1]).
2593 :- use_module(probsrc(bsyntaxtree), [get_texpr_id/2]).
2594 :- use_module(extrasrc(bvisual2), [bv_top_level_set/2]).
2595 :- use_module(probsrc(specfile),[get_specification_description/2]).
2596 :- use_module(probsrc(tools_strings), [atom_tail_to_lower_case/2]).
2597
2598 show_typed_var_in_visb(all,_) :- !.
2599 show_typed_var_in_visb(VarList,b(identifier(ID),_,_)) :- !, show_var_in_visb(VarList,ID).
2600 show_var_in_visb(VarList,ID ) :- (VarList=all -> true ; member(ID,VarList) -> true).
2601
2602 % generate a table for the state (we could use bvisual2)
2603 gen_state_table(Stream,Options,_) :-
2604 b_or_z_mode,
2605 member(show_variables(VarList),Options),
2606 b_get_machine_variables(TypedVars),
2607 gen_state_table_aux(Stream,'Variables',TypedVars,VarList,[],'Value','bVar_'),fail.
2608 gen_state_table(Stream,Options,_) :-
2609 b_or_z_mode,
2610 member(show_variables(VarList),Options),
2611 b_get_machine_expressions(AExprs), AExprs \= [],
2612 gen_state_table_aux(Stream,'Expressions',AExprs,VarList,[],'Value','bVar_'),fail.
2613 gen_state_table(Stream,Options,StateIds) :-
2614 b_or_z_mode,
2615 member(show_constants(IDList),Options),
2616 b_get_machine_constants(TypedVars),
2617 last(StateIds,Last), % we assume there is only one constant valuation in the trace; TO DO: generalise
2618 get_state_and_action(Last,LastId,_,_),
2619 visited_expression(LastId,BState),
2620 expand_to_constants_and_variables(BState,ConstState,_),
2621 gen_state_table_aux(Stream,'Constants',TypedVars,IDList,ConstState,'Value','bConstant_'),fail.
2622 gen_state_table(Stream,Options,_) :-
2623 b_or_z_mode,
2624 member(show_sets(IDList),Options),
2625 findall(TSet,bv_top_level_set(TSet,_),TypedVars),
2626 findall(bind(Set,Val),(bv_top_level_set(TSet,Val),get_texpr_id(TSet,Set)),BState),
2627 gen_state_table_aux(Stream,'Sets',TypedVars,IDList,BState,'Value','bSet_'),fail.
2628 % TO DO: maybe show also top-level guards specfile_possible_trans_name or get_top_level_guard
2629 gen_state_table(Stream,Options,_StateIds) :-
2630 b_or_z_mode,
2631 member(show_events(IDList),Options),
2632 get_specification_description(operations,SN),
2633 atom_tail_to_lower_case(SN,SectionName),
2634 findall(b(identifier(OpName),subst,[]),b_top_level_operation(OpName),TypedVars),
2635 % TODO: op(Params,Results) instead of subst
2636 gen_state_table_aux(Stream,SectionName,TypedVars,IDList,[],'Enabled','bOperation_'),fail.
2637 gen_state_table(_Stream,_,_).
2638
2639
2640 gen_source_code_section(Stream,Options) :-
2641 member(show_source,Options), % we could also include original sources, rather than just internal rep.
2642 !,
2643 Section = 'Source',
2644 format(Stream,' <button type="button" class="collapsible collapsible-style">~w</button>~n',[Section]),
2645 format(Stream,'<div class="coll-content-hid">~n',[]),
2646 get_internal_representation(PP),
2647 format(Stream,'<pre>~s</pre>~n',[PP]),
2648 format(Stream,'</div>~n',[]).
2649 gen_source_code_section(_Stream,_).
2650
2651
2652 :- use_module(probsrc(bsyntaxtree),[get_texpr_description/2, get_texpr_type/2]).
2653 % creates a HTML table with header name Section and including one row per ID in TypedVars;
2654 % id of value for ID is prefixed with IDPrefix
2655 % VarListToShow is either all or a list of ids
2656 gen_state_table_aux(Stream,Section,TypedVars,VarListToShow,BState,ValueStr,IDPrefix) :-
2657 include(show_typed_var_in_visb(VarListToShow),TypedVars,SVars), % check which ids should be shown
2658 length(SVars,SLen), SLen>0,
2659 length(TypedVars,Len),
2660 (SLen=Len
2661 -> format(Stream,' <button type="button" class="collapsible collapsible-style">~w (~w)</button>~n',[Section,SLen])
2662 ; format(Stream,' <button type="button" class="collapsible collapsible-style">~w (~w/~w)</button>~n',
2663 [Section,SLen,Len])
2664 ),
2665 format(Stream,'<div class="coll-content-hid">~n',[]),
2666 format(Stream,' <table> <tr> <th>Nr</th> <th>Name</th> <th>~w</th> </tr>~n',[ValueStr]),
2667 ( nth1(Nr,SVars,IDorExprToShow),
2668 get_state_table_name_and_expr(IDorExprToShow,ID,TExpr),
2669 (get_state_value_codes_for_id(BState,ID,ValCodes)
2670 -> atom_codes(ValueAtom,ValCodes),
2671 html_escape(ValueAtom,EVA) % Value provided in BState; may be overriden in trace export
2672 ; EVA = '?'),
2673 get_table_hover_message(ID,TExpr,HoverMsg),
2674 format(Stream,'~n <tr id="row_~w~w" title="~w"> <td>~w</td> <td id="name_~w~w">~w</td> <td id="~w~w">~w</td>~n',
2675 [IDPrefix,ID, HoverMsg, Nr, IDPrefix,ID,ID, IDPrefix,ID,EVA]),
2676 fail
2677 ;
2678 format(Stream,' </table>~n </div>~n',[])
2679 ).
2680
2681 get_state_table_name_and_expr(bexpr(Kind,TExpr),Name,Expr) :- !, % we have special expression to show
2682 Name=Kind,Expr=TExpr.
2683 get_state_table_name_and_expr(TID,ID,TID) :- get_texpr_id(TID,ID). % normal case: variable name
2684
2685
2686 :- use_module(probsrc(bmachine),[b_get_machine_animation_expression/2]).
2687
2688 b_get_machine_expressions(List) :-
2689 findall(bexpr(AE_Name,AExpr),b_get_machine_animation_expression(AE_Name,AExpr),List). % 'ANIMATION_EXPRESSION'
2690
2691 :- use_module(probsrc(bmachine),[b_get_machine_operation_signature/2]).
2692 % get hover message for entries in variables/constants/... rows:
2693 get_table_hover_message(ID,TExpr,EscHoverMsg) :-
2694 get_texpr_type(TExpr,Type),
2695 (Type=subst,b_get_machine_operation_signature(ID,TS)
2696 -> ajoin(['Operation: ',TS],HoverMsg)
2697 ; pretty_type(Type,TS),
2698 (get_texpr_description(TExpr,Desc)
2699 -> ajoin(['Type: ',TS,'\nDesc: ',Desc],HoverMsg)
2700 ; ajoin(['Type: ',TS],HoverMsg)
2701 )
2702 ),
2703 html_escape(HoverMsg,EscHoverMsg).
2704
2705 % get the values that should be displayed in the variables table
2706 get_state_value_change(StateId,ID,ECodes) :-
2707 visited_expression(StateId,State), % we could refactor this and do it only once
2708 expand_to_constants_and_variables(State,_ConstState,VariableBState),
2709 ( get_state_value_codes_for_id(VariableBState,ID,ValCodes) % look up variable values
2710 ; b_get_machine_animation_expression(_,_) ->
2711 state_corresponds_to_fully_setup_b_machine(State,FullState),
2712 get_state_value_codes_for_anim_expr(FullState,ID,ValCodes) % evaluate animation expressions
2713 ),
2714 b_string_escape_codes(ValCodes,ECodes). % change " to \" for JavaScript
2715 %formatsilent('Value for ~w~nunescaped: "~s",~n escaped: "~s"~n',[ID,ValCodes,ECodes]).
2716
2717
2718 get_state_value_codes_for_id(BState,ID,ValCodes) :-
2719 member(bind(ID,Val),BState),
2720 translate_bvalue_to_codes(Val,ValCodes).
2721
2722 get_state_value_codes_for_anim_expr(BState,AE_Name,ValCodes) :-
2723 b_get_machine_animation_expression(AE_Name,AExpr),
2724 evaluate_visb_formula(AExpr,AE_Name,'',BState,ResValue,unknown),
2725 translate_bvalue_to_codes(ResValue,ValCodes).
2726
2727 :- use_module(probsrc(bmachine),[b_get_machine_operation_max/2]).
2728 :- use_module(probsrc(state_space),[time_out_for_node/3,max_reached_for_node/1]).
2729 :- use_module(probsrc(translate),[translate_event_with_src_and_target_id/5]).
2730 get_state_value_enabled_operation_status(StateId,OpName,Enabled,EnabledValue,TransStr) :-
2731 b_top_level_operation(OpName),
2732 findall(TransID, (transition(StateId,OpTerm,TransID,_NewStateId),
2733 match_operation(OpTerm,OpName)), TransList),
2734 length(TransList,Len),
2735 (Len>0
2736 -> Enabled=true,
2737 EnabledValue = "\x2705\", % green check mark, TRUE alternatives \x2705\ \x2713\ \x2714\
2738 (TransList=[TID], transition(StateId,OpTerm,TID,NewStateId),
2739 translate_event_with_src_and_target_id(OpTerm,StateId,NewStateId,200,TransStr)
2740 -> true
2741 ; ajoin([OpName,' (',Len,'\xd7\)'],TransStr) %
2742 )
2743 ; time_out_for_node(StateId,OpName,TypeOfTimeOut) ->
2744 Enabled=TypeOfTimeOut,
2745 EnabledValue = [8987], % four o'clock symbol
2746 TransStr = OpName
2747 %ajoin(['No transition found due to: ',TypeOfTimeOut],HoverMsg)
2748 ; get_preference(maxNrOfEnablingsPerOperation,0) ->
2749 Enabled=not_computed,
2750 EnabledValue = [10067], % red question mark
2751 TransStr = OpName
2752 %'No transitions were computed because MAX_OPERATIONS = 0' = HoverMsg
2753 ; b_get_machine_operation_max(OpName,0) ->
2754 Enabled=not_computed,
2755 EnabledValue = [10067], % red question mark
2756 TransStr = OpName
2757 %ajoin(['No transitions were computed because MAX_OPERATIONS_',OpName,' = 0'],HoverMsg)
2758 ; Enabled=false,
2759 EnabledValue = [9940], % stop sign, FALSE, alternatives \x10102\
2760 TransStr = OpName
2761 %ajoin(['Not enabled'],HoverMsg)
2762 ). % TO DO: show whether this is the next step in the trace
2763
2764 % --------------------------
2765
2766 % debugging features to inspect all created SVG objects
2767 tcltk_get_visb_objects(list([Header|AllObjects])) :-
2768 Header = list(['SVG-ID','svg_class','Attribute','Value']),
2769 findall(list([SvgID,SvgClass,Attr,Value]),
2770 (visb_svg_object(SvgID,SvgClass,AttrList,Childs,_Desc,_Pos),
2771 (member(svg_attribute(Attr,Value),AttrList) ;
2772 member(Value,Childs), Attr=children)
2773 ), AllObjects).
2774
2775 % debugging features to inspect all created SVG objects
2776 tcltk_get_visb_hovers(list([Header|AllObjects])) :-
2777 Header = list(['SVG-ID','ID','Attribute','EnterValue', 'ExitValue']),
2778 findall(list([SvgID,ID,Attr,EnterVal,ExitVal]),
2779 visb_hover(SvgID,ID,Attr,EnterVal,ExitVal), AllObjects).
2780
2781 % debugging features to inspect items
2782 tcltk_get_visb_items(Res) :-
2783 current_state_id(ID),
2784 tcltk_get_visb_items(ID,Res).
2785 tcltk_get_visb_items(_StateId,Res) :-
2786 \+ visb_file_is_loaded(_),!,
2787 Res = list(['No VisB JSON file loaded']).
2788 tcltk_get_visb_items(StateId,list([Header|AllItems])) :-
2789 Header = list(['SVG-ID','Attribute','Value']),
2790 get_preference(translation_limit_for_table_commands,Limit),
2791 findall(list([SvgID,SvgAttribute,Val]),
2792 get_change_attribute_for_state(StateId,SvgID,SvgAttribute,Val),
2793 Items),
2794 findall(list([DefID,'VisB Definition',DValS]),
2795 (get_expanded_bstate(StateId,ExpandedBState),
2796 reverse(ExpandedBState,RS),
2797 member(bind(DefID,DVal),RS),
2798 visb_definition(DefID,_,_,_,_,_),
2799 translate_bvalue_with_limit(DVal,Limit,DValS)),
2800 AllItems, Items).
2801
2802 :- use_module(probsrc(translate),[translate_event_with_limit/3]).
2803 tcltk_get_visb_events(Res) :-
2804 current_state_id(ID),
2805 tcltk_get_visb_events(ID,Res).
2806 tcltk_get_visb_events(_StateId,Res) :-
2807 \+ visb_file_is_loaded(_),!,
2808 Res = list(['No VisB JSON file loaded']).
2809 tcltk_get_visb_events(StateId,list([Header|AllItems])) :-
2810 Header = list(['SVG-ID','Event','Target']),
2811 get_preference(translation_limit_for_table_commands,Limit),
2812 findall(list([SvgID,EventStr,NewStateId]),
2813 (perform_visb_click_event(SvgID,[],StateId,_Event,OpTerm,NewStateId,Res),
2814 (Res=[] -> EventStr='disabled' ; translate_event_with_limit(OpTerm,Limit,EventStr))
2815 ),
2816 AllItems).
2817 % --------------------------
2818
2819 % for ProB2-UI
2820
2821 :- use_module(probsrc(translate),[translate_bexpression_with_limit/3]).
2822 get_visb_items(List) :-
2823 findall(visb_item(SvgID,Attr,TS,Desc,Pos),
2824 (visb_item(SvgID,Attr,TypedExpr,_Used,Desc,Pos,_),
2825 translate_bexpression_with_limit(TypedExpr,1000,TS)), List).
2826
2827 get_visb_attributes_for_state(StateId,List) :-
2828 % some external functions like ENABLED are evaluated in current state; it might be useful to set_current_state
2829 findall(set_attr(SvgID,SvgAttribute,Val),
2830 get_change_attribute_for_state(StateId,SvgID,SvgAttribute,Val),
2831 List).
2832
2833 % for ProB2-UI
2834 get_visb_click_events(List) :-
2835 findall(execute_event(SvgID,Event,Preds),
2836 get_visb_event(SvgID,Event,Preds), List).
2837 get_visb_event(SvgID,Event,Preds) :- visb_event(SvgID,Event,Preds,_,_File,_Pos).
2838 get_visb_event(SvgID,'',[]) :- % add a virtual empty event for SVG Ids with hovers but no events
2839 visb_has_hovers(SvgID),
2840 \+ visb_event(SvgID,_,_,_,_File,_Pos).
2841
2842
2843 :- use_module(probsrc(state_space), [extend_trace_by_transition_ids/1]).
2844 % perform a click on a VisB SVG ID in the animator
2845 tcltk_perform_visb_click_event(SvgID) :- current_state_id(StateId),
2846 (perform_visb_click_event(SvgID,[],StateId,TransitionIDs)
2847 -> formatsilent('Clicking on ~w in state ~w resulted in transition id sequence ~w~n',[SvgID,StateId,TransitionIDs]),
2848 extend_trace_by_transition_ids(TransitionIDs)
2849 ; add_error(visb_visualiser,'Cannot perform VisB click on: ',SvgID)
2850 ).
2851
2852 :- use_module(probsrc(b_state_model_check),[execute_operation_by_predicate_in_state_with_pos/6]).
2853 % computes the effect of clicking on an SvgID in StateId
2854 % it returns either empty list if the visb_event is not feasible or a list of transition ids
2855 % it fails if SvgID has no events associated with it
2856 perform_visb_click_event(SvgID,MetaInfos,StateId,ResTransitionIds) :-
2857 perform_visb_click_event(SvgID,MetaInfos,StateId,_,_,_,ResTransitionIds).
2858 perform_visb_click_event(SvgID,_MetaInfos,StateId,OpName,OpTerm,NewStateId,ResTransitionIds) :-
2859 get_expanded_bstate(StateId,ExpandedBState),
2860 set_error_context(checking_context('VisB:','performing click event')),
2861 set_context_state(StateId,perform_visb_click_event),
2862 get_svgid_with_events(SvgID,_),
2863 call_cleanup(perform_aux(SvgID,StateId,ExpandedBState,OpName,OpTerm,NewStateId,ResTransitionIds),
2864 (clear_context_state,clear_error_context)).
2865
2866 get_svgid_with_events(SvgID,FirstOpName) :- visb_event(SvgID,FirstOpName,_,_,_File,_Pos).
2867
2868
2869 :- use_module(probsrc(state_space),[transition/4]).
2870 perform_aux(SvgID,StateId,_ExpandedBState,OpName,OpTerm,NewStateId,ResTransitionIds) :-
2871 \+ b_or_z_mode,
2872 % just look up transition/4 entries in state space
2873 !, % TODO: maybe provide this possibility for B models, even if using explicit parameter values is more robust
2874 get_visb_event_operation(SvgID,OpName,_,_Pred,_Pos),
2875 if((transition(StateId,OpTerm,TransID,NewStateId),
2876 match_operation(OpTerm,OpName)),
2877 ResTransitionIds = [TransID],
2878 return_disabled(SvgID,StateId,OpName,OpTerm,NewStateId,ResTransitionIds)
2879 ).
2880 perform_aux(SvgID,StateId,ExpandedBState,OpName,OpTerm,NewStateId,ResTransitionIds) :-
2881 %state_space:portray_state_space,
2882 if(execute_visb_event_by_predicate(SvgID,StateId,ExpandedBState,OpName,OpTerm,NewStateId,TransId),
2883 ResTransitionIds = [TransId], % Later we may return a longer sequence of transitions
2884 return_disabled(SvgID,StateId,OpName,OpTerm,NewStateId,ResTransitionIds)).
2885
2886 return_disabled(SvgID,StateId,OpName,OpTerm,NewStateId,ResTransitionIds) :-
2887 OpTerm = disabled, NewStateId = StateId,
2888 get_svgid_with_events(SvgID,OpName),
2889 ResTransitionIds = []. % visb_event not enabled
2890
2891 :- use_module(probsrc(tools_strings),[match_atom/2]).
2892 :- use_module(probsrc(specfile),[get_operation_name/2]).
2893 match_operation(OpTerm,OpTerm) :- !.
2894 match_operation(OpTerm,OpName) :- atom(OpName),
2895 (get_operation_name(OpTerm,OpName)
2896 ; match_atom(OpName,OpTerm) % match an atom string with a compound term
2897 ),!.
2898
2899 execute_visb_event_by_predicate(SvgID,StateId,ExpandedBState,OpName,OpTerm,NewStateId,TransId) :-
2900 get_visb_event_operation(SvgID,OpName,_,Pred,Pos), % TO DO: include Metainfos if necessary
2901 exec_aux(SvgID,StateId,ExpandedBState,OpName,Pred,Pos,OpTerm,NewStateId,TransId).
2902
2903 :- use_module(probsrc(tcltk_interface),[compute_all_transitions_if_necessary/2]).
2904 :- use_module(library(random),[random_member/2]).
2905 :- use_module(extrasrc(mcts_game_play), [mcts_auto_play/4, mcts_auto_play_available/0]).
2906 exec_aux(_SvgID,StateId,ExpandedBState,OpName,Pred,Pos,OpTerm,NewStateId,TransId) :-
2907 b_is_operation_name(OpName),!,
2908 execute_operation_by_predicate_in_state_with_pos(ExpandedBState,OpName,Pred,OpTerm,NewState,Pos),
2909 patch_state(NewState,StateId,PatchedNewState),
2910 tcltk_interface:add_trans_id(StateId,OpTerm,PatchedNewState,NewStateId,TransId).
2911 %translate:print_bstate(PatchedNewState),nl.
2912 exec_aux(SvgID,StateId,_ExpandedBState,'MCTS_AUTO_PLAY',_Pred,Pos,OpTerm,NewStateId,TransId) :- !,
2913 mcts_auto_play_available,
2914 % TODO: allow to set SimRuns, TimeOut in Pred
2915 add_debug_message(visb_visualiser,'Performing MCTS_AUTO_PLAY for click on: ',SvgID,Pos),
2916 mcts_auto_play(StateId,OpTerm,TransId,NewStateId).
2917 exec_aux(_SvgID,StateId,_ExpandedBState,'RANDOM_ANIMATE',_Pred,_Pos,OpTerm,NewStateId,TransId) :- !,
2918 compute_all_transitions_if_necessary(StateId,false),
2919 findall(rtr(OpTerm,TransId,NewStateId),transition(StateId,OpTerm,TransId,NewStateId),List),
2920 random_member(rtr(OpTerm,TransId,NewStateId),List).
2921 % see tcltk_interface:tcltk_random_perform2 and allow Kind: fully_random, no_self_loops, heuristics, ...
2922 % split with ; ?
2923
2924 :- use_module(probsrc(bmachine), [b_is_variable/1,b_machine_has_constants/0]).
2925
2926 is_var_binding(bind(Var,_)) :- b_or_z_mode, b_is_variable(Var).
2927
2928
2929 % remove constants and VisB Definition entries from state:
2930 patch_state(NewState,StateId,PatchedState) :-
2931 get_constants_id_for_state_id(StateId,ConstId),!,
2932 PatchedState = const_and_vars(ConstId,VarsState),
2933 include(is_var_binding,NewState,VarsState).
2934 patch_state(NewState,StateId,VarsState) :-
2935 (b_machine_has_constants
2936 -> add_error(visb_visualiser,'Could not extract constants id for state:',StateId),
2937 VarsState=NewState
2938 ; include(is_var_binding,NewState,VarsState)).
2939
2940 % the next predicate gets all operations/events associated with SvgID in the order in which they were found
2941 % note that there is only one visb_event (the last one); all others are auxiliary
2942 get_visb_event_operation(SvgID,OpName,Preds,TypedPred,Pos) :- % check if there are more events registered:
2943 auxiliary_visb_event(SvgID,OpName,Preds,TypedPred,Pos).
2944 get_visb_event_operation(SvgID,OpName,Preds,TypedPred,Pos) :-
2945 visb_event(SvgID,OpName,Preds,TypedPred,_File,Pos).
2946
2947 % ---------------
2948
2949 get_visb_hovers(List) :-
2950 findall(hover(SvgID,ID,Attr,EnterVal,ExitVal),
2951 visb_hover(SvgID,ID,Attr,EnterVal,ExitVal), List).
2952
2953 get_visb_svg_objects(List) :-
2954 % TODO: remove objects inlined in get_visb_default_svg_file_contents
2955 findall(visb_svg_object(SvgID,SvgClass,AttrList),
2956 visb_svg_object(SvgID,SvgClass,AttrList,_Childs,_Desc,_Pos), List).
2957
2958 % ------------------
2959
2960 :- use_module(probsrc(bmachine),[b_absolute_file_name_relative_to_main_machine/2]).
2961 extended_static_check_default_visb_file :-
2962 (get_default_visb_file(VisBFile,Pos)
2963 % TODO: we could check if we have an visb_history(JSONFile,_,_) option
2964 -> extended_static_check_visb_file(VisBFile,Pos)
2965 ; true).
2966
2967 extended_static_check_visb_file('',_InclusionPos) :-
2968 load_visb_file('').
2969 extended_static_check_visb_file(VisBFile,InclusionPos) :-
2970 b_absolute_file_name_relative_to_main_machine(VisBFile,AFile),
2971 (file_exists(AFile)
2972 -> load_visb_file(AFile)
2973 ; add_warning(lint,'VISB_JSON_FILE does not exist: ',AFile,InclusionPos)
2974 ).