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