1 % Heinrich Heine Universitaet Duesseldorf
2 % (c) 2021-2026 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,
6 load_visb_definitions_from_list_of_facts/2,
7 load_visb_definitions_from_term/2,
8 load_visb_file_if_necessary/1,
9 visb_file_is_loaded/1, visb_file_is_loaded/3,
10 visb_current_state_can_be_visualised/0,
11 get_default_visb_file/2, extended_static_check_default_visb_file/0,
12 load_default_visb_file_if_necessary/0,
13 generate_visb_html_for_history/1, generate_visb_html_for_history/2,
14 generate_visb_html_for_history_with_vars/1,
15 generate_visb_html_for_history_with_source/1,
16 generate_visb_html_for_current_state/1, generate_visb_html_for_current_state/2,
17 generate_visb_html_codes_for_states/3,
18 generate_visb_html/3,
19 tcltk_get_visb_items/1, tcltk_get_visb_events/1,
20 tcltk_get_visb_objects/1, tcltk_get_visb_hovers/1,
21 get_visb_items/1, get_visb_attributes_for_state/2,
22 get_visb_click_events/1, get_visb_hovers/1,
23 perform_visb_click_event/4,
24 tcltk_perform_visb_click_event/1,
25 get_visb_default_svg_file_contents/1,
26 get_visb_svg_objects/1]).
27
28 :- use_module(probsrc(module_information),[module_info/2]).
29 :- module_info(group,visualization).
30 :- module_info(description,'This module provides VisB visualisation functionality.').
31
32 % special SVG object attributes treated by VisB
33 % title (creates hover tooltip; currently only works with objects created by VisB itself)
34 % id
35 % svg_class
36 % text
37 % hovers
38 % event, events
39 % predicate
40
41 :- meta_predicate process_repeat(-,-,-,2).
42
43 :- use_module(extrasrc(json_parser),[json_parse_file/3]).
44 :- use_module(library(lists)).
45
46 :- use_module(probsrc(error_manager)).
47 :- use_module(probsrc(preferences),[get_preference/2]).
48 :- use_module(probsrc(debug)).
49 :- use_module(probsrc(state_space), [visited_expression/2, visited_state_corresponds_to_initialised_b_machine/1,
50 get_constants_id_for_state_id/2, get_constants_state_id_for_id/2,
51 set_context_state/2, clear_context_state/0,
52 transition/3, transition/4, invariant_violated/1, invariant_not_yet_checked/1,
53 multiple_concrete_constants_exist/0, is_concrete_constants_state_id/1]).
54 :- use_module(probsrc(translate), [translate_bvalue_to_codes/2, translate_bvalue_to_codes_with_limit/3,
55 translate_bvalue_with_limit/3]).
56 :- use_module(probsrc(specfile),[eventb_mode/0, xtl_mode/0,
57 state_corresponds_to_initialised_b_machine/2,
58 state_corresponds_to_fully_setup_b_machine/2,
59 state_corresponds_to_set_up_constants_only/2,
60 expand_to_constants_and_variables/3,
61 extract_variables_from_state/2]).
62
63 :- use_module(probsrc(tools),[start_ms_timer/1,stop_ms_walltimer_with_msg/2, ajoin_with_sep/3]).
64 :- use_module(probsrc(tools_io),[safe_open_file/4, with_open_stream_to_codes/4]).
65 :- use_module(probsrc(bmachine), [b_machine_name/1, b_get_definition_name_with_pos/4, bmachine_is_precompiled/0,
66 pre_expand_typing_scope/2, determine_type_of_formula/2, determine_type_of_formula/3]).
67 :- use_module(probsrc(bsyntaxtree), [get_texpr_ids/2]).
68 :- use_module(probsrc(tools_lists),[include_maplist/3]).
69 :- use_module(probsrc(tools),[split_list/4, html_escape_codes/2]).
70 :- use_module(probsrc(tools_matching),[get_all_svg_attributes/1, is_svg_attribute/1, is_virtual_svg_attribute/1,
71 is_svg_attribute_with_fixed_values/2,
72 is_svg_number_attribute/2, is_svg_color_attribute/1]).
73
74 % --------------------------
75
76 % facts storing loaded JSON VisB file:
77 :- dynamic visb_file_loaded/3, visb_svg_file/5, visb_empty_svg_box_height_width/3,
78 visb_definition/6, visb_special_definition/6,
79 visb_item/7,
80 visb_event/6, visb_hover/6, visb_has_hovers/1, visb_has_visibility_hover/1,
81 visb_event_enable_list/5,
82 visb_svg_object/5, visb_svg_object_debug_info/2,
83 visb_svg_child/2, visb_svg_parent/2, % register parent/child relationships for groups, title, ...
84 visb_svg_child_of_object_from_svg_file/1. % true if parent of object is an SVG in an external file
85 :- dynamic auxiliary_visb_event/5.
86 % visb_svg_file(SVGFile, AbsolutePathSVGFile, JSONFileFromWhichWeImportSVG,PosTerm,ModLocTime)
87 % visb_item(SVGID,Attribute,TypedExpression,UsedIds,Description/Comment,StartPos,OtherMetaInfos)
88 % visb_event(SVGID,Event,PredicateList,TypedPredicate,File,Pos)
89 % visb_svg_object(SVGID,SVG_Class,AttrList,Description/Comment,Pos) ; AttrList contains svg_attribute(Attr,Val)
90
91 reset_visb :- debug_println(9,resetting_visb),
92 retractall(visb_file_loaded(_,_,_)),
93 retractall(visb_empty_svg_box_height_width(_,_,_)),
94 retractall(visb_svg_file(_,_,_,_,_)),
95 retractall(visb_definition(_,_,_,_,_,_)),
96 retractall(visb_special_definition(_,_,_,_,_,_)),
97 retractall(visb_item(_,_,_,_,_,_,_)),
98 retractall(visb_event(_,_,_,_,_,_)),
99 retractall(visb_hover(_,_,_,_,_,_)),
100 retractall(visb_has_hovers(_)),
101 retractall(visb_has_visibility_hover(_)),
102 retractall(visb_event_enable_list(_,_,_,_,_)),
103 retractall(auxiliary_visb_event(_,_,_,_,_)),
104 retractall(visb_svg_object(_,_,_,_,_)),
105 retractall(visb_svg_object_debug_info(_,_)),
106 retractall(visb_svg_child(_,_)),
107 retractall(visb_svg_child_of_object_from_svg_file(_)),
108 retractall(visb_svg_parent(_,_)),
109 reset_auto_attrs.
110
111 visb_file_is_loaded(JSONFile) :-
112 visb_file_is_loaded(JSONFile,_,true).
113 visb_file_is_loaded(JSONFile,SVGFile,AllowEmpty) :-
114 visb_file_loaded(JSONFile,_,_),
115 (visb_svg_file(_,SVGFile,_,_,_) -> true
116 ; visb_empty_svg_box_height_width(_,_,_) -> SVGFile = ''
117 ; user_has_defined_visb_objects -> SVGFile = ''
118 ; JSONFile='' ->
119 AllowEmpty=true,
120 add_warning(visb_visualiser,'No VISB_SVG_FILE or VISB_SVG_OBJECTS specified in DEFINITIONS',''),
121 % Note: warning also generated below No VisB JSON file is specified and no VISB_SVG_OBJECTS were created
122 SVGFile = ''
123 ; add_warning(visb_visualiser,'No SVG file or objects specified for VisB file:',JSONFile),
124 AllowEmpty=true,
125 SVGFile = ''
126 ).
127
128 no_svg_available :-
129 \+ user_has_defined_visb_objects,
130 no_svg_file_available,
131 \+ visb_empty_svg_box_height_width(_,_,_). % no SVG box provided
132
133 no_svg_file_available :- (visb_svg_file(_,SVGFile,_,_,_) -> SVGFile='' ; true).
134 %svg_file_available :- \+ no_svg_file_available.
135
136 :- use_module(probsrc(state_space),[current_state_id/1,
137 current_state_corresponds_to_setup_constants_b_machine/0]).
138 visb_current_state_can_be_visualised :-
139 %visb_file_is_loaded(_), % no longer checked; Tcl/Tk will automatically load VisB file if required
140 (b_or_z_mode -> current_state_corresponds_to_setup_constants_b_machine
141 ; \+ current_state_id(root)
142 ).
143
144 :- use_module(probsrc(eventhandling),[register_event_listener/3]).
145 :- register_event_listener(reset_specification,reset_visb,'Reset VisB information').
146 :- register_event_listener(reset_prob,reset_visb,'Reset VisB information').
147
148 %static_check_visb :- % now done when adding items and not storing multiple items
149 % visb_item(ID,Attr,F1,_,_,Pos1), visb_item(ID,Attr,F2,_,Pos2), F1 @< F2,
150 % add_warning(visb_visualiser,'Multiple formulas for SVG identifier and attribute:',ID/Attr,Pos1),
151 % add_message(visb_visualiser,'Location of second formula for:',ID/Attr,Pos2),
152 % fail.
153 % TO DO: some sanity checks on attributes and values
154 static_check_visb :-
155 no_svg_file_available,
156 ? visb_hover(SVGID,_ID,Attr,_Enter,_Exit,Pos),
157 \+ svg_id_exists(SVGID),
158 ajoin(['Hover for attribute ',Attr,' has unknown trigger-id (can lead to blank visualisation): '],Msg),
159 add_warning(visb_visualiser,Msg,SVGID,Pos),
160 fail.
161 static_check_visb :-
162 no_svg_file_available,
163 ? visb_hover(SVGID,ID,Attr,_Enter,_Exit,Pos), ID \= SVGID,
164 \+ svg_id_exists(ID),
165 ajoin(['Hover for attribute ',Attr,' has unknown id (can lead to blank visualisation): '],Msg),
166 add_warning(visb_visualiser,Msg,ID,Pos),
167 fail.
168 static_check_visb :-
169 visb_svg_file(SvgFile,_,_,Pos,_),
170 SvgFile \= '',
171 visb_empty_svg_box_height_width(H,W,ViewBox),
172 ajoin(['VISB_SVG_BOX (width=', W, ', height=', H, ', viewBox=', ViewBox,
173 ') cannot be applied to an existing SVG file (use VISB_SVG_CONTENTS for file or put info into SVG file): '],Msg),
174 add_warning(visb_visualiser,Msg,SvgFile,Pos),
175 fail.
176 static_check_visb.
177
178 svg_id_exists(SVGID) :- visb_svg_object(SVGID,_,_StaticAttrList,_,_ExitPos).
179 % --------------------------
180
181 :- use_module(probsrc(tools),[read_string_from_file/2]).
182
183 % store templates as facts, so that compiled version of probcli does not need to find files
184 :- dynamic visb_template_file_codes/2.
185
186 assert_from_template(Filename) :- %formatsilent('Loading ~w~n',[Filename]),
187 absolute_file_name(visbsrc(Filename), Absolute, []),
188 read_string_from_file(Absolute,String),
189 assertz(visb_template_file_codes(Filename,String)).
190
191 :- assert_from_template('visb_template_header.html').
192 :- assert_from_template('visb_template_svg_downloads.html').
193 :- assert_from_template('visb_template_replayTrace.html').
194 :- assert_from_template('visb_template_middle.html').
195 :- assert_from_template('visb_template_footer.html').
196
197 write_visb_template(HtmlFile,Stream) :-
198 visb_template_file_codes(HtmlFile,Codes),
199 format(Stream,'~s~n',[Codes]).
200
201
202 % --------------------------
203
204 :- use_module(probsrc(pref_definitions),[b_get_definition_string_from_spec/3]).
205 get_default_visb_file(Path, Pos) :- get_default_visb_file(Path, _, Pos).
206 get_default_visb_file(Path, Kind, Pos) :- bmachine_is_precompiled,
207 (b_get_definition_string_from_spec('VISB_JSON_FILE', Pos, Path)
208 -> Kind=json % user provided explicit path to VISB JSON file
209 ; b_get_definition_string_from_spec('VISB_DEFINITIONS_FILE', Pos, Path)
210 -> Kind=def % user provided explicit path to VISB DEFINITIONS file
211 % TODO: in future check that file extension is compatible
212 % advantage of VISB_DEFINITIONS_FILE == "File" over "File"
213 % 1) visualisation can be re-loaded without re-loading machine
214 % 2) can be used in TLA+ or similar
215 % 3) avoid clash if definitions file itself defines empty VISB_JSON_FILE
216 % 4) avoid problems with Atelier-B or other tools
217 ; get_default_visb_svg_file(_,Pos)
218 -> Kind=empty, Path='' % user provided SVG file path
219 ; user_has_defined_visb_objects_in_defs
220 -> Kind=empty, Path='' % user provided SVG object definitions
221 ).
222
223 user_has_defined_visb_objects :-
224 ? (visb_svg_object(_,_,_,_,_) -> true % created in JSON file
225 ; user_has_defined_visb_objects_in_defs).
226
227 user_has_defined_visb_objects_in_defs :-
228 b_sorted_b_definition_prefixed(expression,'VISB_SVG_OBJECTS',_,_).
229
230 % you should do b_absolute_file_name_relative_to_main_machine
231 get_default_visb_svg_file(Path, Pos) :-
232 b_get_definition_string_from_spec('VISB_SVG_FILE', Pos, Path).
233
234
235 % load default VISB_JSON_FILE if it is specified and not already loaded
236 load_default_visb_file_if_necessary :-
237 get_default_visb_file(File, Pos),!,
238 (load_visb_file_if_necessary(File) -> true
239 ; add_error(visb_visualiser,'Could not load VISB_JSON_FILE:',File,Pos)).
240 load_default_visb_file_if_necessary :-
241 (eventb_mode -> true ; add_message(visb_visualiser,'No VISB_JSON_FILE DEFINITION provided')).
242
243 % --------------------------
244 % Loading a JSON VisB file:
245
246
247 :- use_module(probsrc(tools), [get_filename_extension/2]).
248 :- use_module(probsrc(bmachine), [
249 b_load_additional_definitions_file/1,
250 b_load_additional_definitions_from_list_of_facts/1,
251 b_load_additional_definitions_from_term/1
252 ]).
253 load_visb_file(File) :-
254 temporary_set_preference(allow_arith_operators_on_reals,true,Old),
255 call_cleanup((load_visb_file1(File)),
256 reset_temporary_preference(allow_arith_operators_on_reals,Old)).
257 load_visb_file1(File) :-
258 get_filename_extension(File,def), % a .def B definition file
259 !,
260 add_message(visb_visualiser,'Loading VisB DEFINITIONS from B file: ',File),
261 b_load_additional_definitions_file(File),
262 load_visb_file2('',File).
263 load_visb_file1(File) :- load_visb_file2(File,File).
264
265 load_visb_definitions_from_list_of_facts(DefFilePath, ListOfFacts) :-
266 temporary_set_preference(allow_arith_operators_on_reals,true,Old),
267 call_cleanup(
268 (b_load_additional_definitions_from_list_of_facts(ListOfFacts),
269 load_visb_file2('', DefFilePath)),
270 reset_temporary_preference(allow_arith_operators_on_reals,Old)).
271
272 load_visb_definitions_from_term(DefFilePath, Machine) :-
273 temporary_set_preference(allow_arith_operators_on_reals,true,Old),
274 call_cleanup(
275 (b_load_additional_definitions_from_term(Machine),
276 load_visb_file2('', DefFilePath)),
277 reset_temporary_preference(allow_arith_operators_on_reals,Old)).
278
279 load_visb_file2(JsonFile,OrigFileName) :-
280 reset_visb,
281 load_visb_from_definitions(no_inlining,JsonFile), % TODO: pass InlineObjects?
282 start_ms_timer(T),
283 (JsonFile='' % No JSON file
284 -> (get_default_visb_svg_file(SvgFile,DefaultSVGPos)
285 -> (SvgFile='' -> AbsFile=SvgFile % just dummy empty string provided by user
286 ; b_absolute_file_name_relative_to_main_machine(SvgFile,AbsFile)
287 ),
288 add_visb_svg_file(SvgFile,AbsFile,'',DefaultSVGPos)
289 ; check_objects_created(JsonFile) % no JSON and SVG file; check we have created objects
290 )
291 ; add_visb_file(JsonFile,[]),
292 stop_ms_walltimer_with_msg(T,'loading VisB JSON file: ')
293 ),
294 static_check_visb,
295 (OrigFileName = ''
296 -> ModTime=0, ModLocTime=0 % We could get modification time of files with VISB_SVG_OBJECTS, ... DEFINITIONS
297 ; file_property(OrigFileName, modify_timestamp, ModTime),
298 file_property(OrigFileName, modify_localtime, ModLocTime)
299 ),
300 assertz(visb_file_loaded(OrigFileName,ModTime,ModLocTime)).
301
302 check_objects_created(File) :-
303 ? (visb_svg_object(_,_,_,_,_) -> true
304 ; add_warning(visb_visualiser,'No VisB JSON file is specified and no VISB_SVG_OBJECTS were created:',File)
305 ).
306
307 load_visb_from_definitions(InlineObjects,JsonFileContext) :-
308 start_ms_timer(T),
309 pre_expand_typing_scope([variables_and_additional_defs],ExpandedScope), % do this only once for all defs
310 get_svg_objects_from_definitions(InlineObjects,ExpandedScope,JsonFileContext),
311 (get_SVG_BOX_definition(InlineObjects) -> true ; true), % TODO: also pass scope
312 stop_ms_walltimer_with_msg(T,'extracting VisB infos from DEFINITIONS: ').
313
314 :- use_module(library(file_systems),[file_exists/1, file_property/3]).
315 %:- use_module(library(system),[now/1, datime/2]).
316 load_visb_file_if_necessary(File) :-
317 visb_file_loaded(File,ModTime1,_), % this file is already loaded
318 (File = '' -> true
319 ; file_exists(File),
320 file_property(File, modify_timestamp, ModTime2), % check if it has the same time stamp
321 debug_println(19,visb_json_already_loaded(File,ModTime1,ModTime2)),
322 ModTime1=ModTime2
323 ),
324 !.
325 load_visb_file_if_necessary(File) :- load_visb_file(File).
326
327
328 :- use_module(probsrc(bmachine),[set_additional_filename_as_parsing_default/3, reset_filename_parsing_default/2]).
329
330 add_visb_file(File,LoadedFiles) :- member(File,LoadedFiles),!,
331 add_error(visb_visualiser,'Circular inclusion of JSON files:',[File|LoadedFiles]).
332 add_visb_file(File,_) :- \+ file_exists(File),!,
333 add_error(visb_visualiser,'JSON file does not exist:',File), fail.
334 add_visb_file(File,LoadedFiles) :-
335 debug_format(19,'Loading JSON File: ~w~n',[File]),
336 set_additional_filename_as_parsing_default(File,NewNr,OldNr),
337 call_cleanup(add_visb_file2(File,LoadedFiles), reset_filename_parsing_default(NewNr,OldNr)).
338
339 add_visb_file2(File,LoadedFiles) :-
340 json_parse_file(File,json(List2),[position_infos(true),multiline_strings(true)]),
341 % tools_printing:trace_print(List2),nl,nl,
342 process_json(List2,File),
343 !,
344 (get_attr_with_pos(include,List2,JsonFileTerm,File,Pos)
345 -> check_json_string(JsonFileTerm,include,Pos,JsonFile),
346 absolute_file_name(JsonFile,AF,[relative_to(File)]),
347 formatsilent('Including JSON file: ~w~n',[JsonFile]),
348 add_visb_file(AF,[File|LoadedFiles])
349 ; true
350 ),
351 (LoadedFiles=[], % only check for main included file
352 ? get_attr_with_pos('model-name',List2,string(ModelName),File,MPos),
353 b_machine_name(Main), Main \= ModelName
354 -> ajoin(['VisB JSON file expects model-name ',ModelName,' instead of: '],MMsg),
355 add_warning(visb_visualiser,MMsg,Main,MPos)
356 ; true
357 ).
358 add_visb_file2(File,_) :-
359 add_error(visb_visualiser,'Unable to process JSON file:',File),
360 fail.
361
362 % process json content of a VisB file:
363 process_json(List,JSONFile) :- visb_svg_file(_,_,_,_,_),!, % we have already determined the SVG file
364 process_json2(List,JSONFile).
365 process_json(List,JSONFile) :-
366 ? get_attr_with_pos(svg_box,List,json(BoxList),JSONFile,Pos),
367 % json([=(width,400,3-3),=(height,400,3-3)])
368 ? (get_attr(svg,List,string(SvgFile)) -> SvgFile='' ; true), % check if svg attr empty or non-existant
369 force_get_attr_nr(height,BoxList,H,JSONFile),
370 force_get_attr_nr(width,BoxList,W,JSONFile),!,
371 (get_attr(viewBox,BoxList,string(VB)) -> ViewBox=VB ; ViewBox=''),
372 add_message(visb_visualiser,'Will create empty SVG image with specified dimensions: ',H:W,Pos),
373 assert_visb_empty_svg_box_height_width(H,W,ViewBox,Pos),
374 process_json2(List,JSONFile).
375 process_json(List,JSONFile) :-
376 ? get_attr_with_pos(svg,List,FileTerm,JSONFile,Pos),
377 check_json_string(FileTerm,svg,Pos,File),
378 (File = '' -> get_default_visb_svg_file(SvgFile, _)
379 ; get_default_visb_svg_file(SvgFile, DPos)
380 -> add_message(visb_visualiser,'Overriding svg file specified in JSON file: ',File,DPos)
381 ; SvgFile=File),
382 !,
383 absolute_file_name(SvgFile,AbsFile,[relative_to(JSONFile)]),
384 add_visb_svg_file(SvgFile,AbsFile,JSONFile,Pos),
385 process_json2(List,JSONFile).
386 process_json(List,JSONFile) :-
387 get_default_visb_svg_file(SvgFile, Pos), SvgFile \= '',
388 !,
389 absolute_file_name(SvgFile,AbsFile,[]), % relative to B machine??
390 add_visb_svg_file(SvgFile,AbsFile,JSONFile,Pos),
391 process_json2(List,JSONFile).
392 process_json(List,JSONFile) :-
393 process_json2(List,JSONFile),
394 (get_SVG_BOX_definition(no_inlining) -> true % TODO: pass (InlineObjects)
395 ; get_attr_with_pos(svg,List,_,JSONFile,Pos) -> % File is empty
396 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)
397 ; add_warning(visb_visualiser,'Creating empty SVG image. The JSON file contains no svg attribute (pointing to the SVG file): ',JSONFile)
398 ).
399
400 add_visb_svg_file(SvgFile,AbsFile,JSONFile,Pos) :-
401 (SvgFile='' -> add_message(visb_visualiser,'Empty VisB SVG file:',SvgFile,Pos)
402 ; file_exists(AbsFile)
403 -> debug_format(19,'SVG file = ~w (~w)~n',[SvgFile, AbsFile]),
404 file_property(AbsFile, modify_localtime, ModLocTime)
405 ; add_error(visb_visualiser,'The specified VisB SVG file does not exist:',SvgFile,Pos),
406 ModLocTime=unknown
407 ),
408 assertz(visb_svg_file(SvgFile,AbsFile,JSONFile,Pos,ModLocTime)).
409
410 process_json2(List,JSONFile) :-
411 process_json_definitions(List,JSONFile),
412 process_json_items(List,JSONFile),
413 process_json_events(List,JSONFile),
414 process_json_new_svg_objects(List,JSONFile).
415
416 :- use_module(probsrc(tools_strings),[ajoin/2]).
417 check_json_string(Term,_,_,Atom) :- Term = string(Atom), atom(Atom), !.
418 check_json_string(Term,Attr,Pos,_) :- !,
419 ajoin(['Illegal JSON attribute ',Attr,', expected a JSON string:'],Msg),
420 add_error(visb_visualiser,Msg,Term,Pos),fail.
421 % ----------------
422
423 % B definitions that can help write items, events more compactly
424 process_json_definitions(List,File) :-
425 ? get_attr(definitions,List,array(Defs)),!,
426 length(Defs,Len),
427 formatsilent('VisB Definitions: ~w~n',[Len]),
428 maplist(process_json_definition(File),Defs).
429 process_json_definitions(_,_File).
430
431 % VisB items which modify attributes of SVG objects
432 process_json_items(List,File) :-
433 ? get_attr(items,List,array(Items)),!,
434 length(Items,Len),
435 formatsilent('VisB Item declarations: ~w~n',[Len]),
436 maplist(process_visb_json_item(File),Items).
437 process_json_items(_,File) :- \+ visb_special_definition(visb_updates,_,_,_,_,_),!,
438 add_message(visb_visualiser,'The JSON file contains no items: ',File).
439 process_json_items(_,_).
440
441 % VisB events which react to clicks on SVG objects and display hovers
442 process_json_events(List,File) :-
443 get_attr(events,List,array(Items)),!,
444 length(Items,Len),
445 formatsilent('VisB Event declarations: ~w~n',[Len]),
446 maplist(process_json_event(File),Items).
447 process_json_events(_,_).
448
449 % VisB additional SVG objects added to SVG file
450 process_json_new_svg_objects(List,File) :-
451 ? get_attr(svg_objects,List,array(Items)),!,
452 length(Items,Len),
453 formatsilent('VisB additional svg_objects declarations: ~w~n',[Len]),
454 maplist(process_json_svg_object(File),Items).
455 process_json_new_svg_objects(List,File) :-
456 get_attr_with_pos(objects,List,array(Items),File,Pos),!,
457 add_warning(visb_visualiser,'Use "svg_objects" attribute instead of "objects" in: ',File,Pos),
458 maplist(process_json_svg_object(File),Items).
459 process_json_new_svg_objects(_,_).
460
461 :- use_module(probsrc(custom_explicit_sets),[try_expand_custom_set_with_catch/3,
462 is_custom_explicit_set/1, is_set_value/2]).
463 % evaluate all VISB_SVG_OBJECTS... DEFINITIONS and try and extract SVG objects
464 % this must be a set of records with at least id and svg_class field
465 get_svg_objects_from_definitions(InlineObjects,ExpandedScope,_) :-
466 ? find_and_eval_visb_DEFINITION('VISB_SVG_OBJECTS', visb_objects, SVG_ID, AttrList, Desc, DefName,
467 _DefPos, EvalPos, InlineObjects, allow_separation, ExpandedScope),
468 %formatsilent('Generating new SVG object ~w with attrs ~w~n',[SVG_ID,AttrList]),
469 add_visb_object_from_definition(visb_objects, SVG_ID, AttrList, Desc, DefName, EvalPos),
470 fail.
471 get_svg_objects_from_definitions(InlineObjects,ExpandedScope,_) :-
472 find_and_eval_visb_DEFINITION('VISB_SVG_EVENTS', visb_events, SVG_ID, AttrList, Desc, DefName,
473 _DefPos, EvalPos, InlineObjects, no_separation, ExpandedScope),
474 add_visb_object_from_definition(visb_events, SVG_ID, AttrList, Desc, DefName, EvalPos),
475 fail.
476 get_svg_objects_from_definitions(InlineObjects,ExpandedScope,_) :-
477 ? find_and_eval_visb_DEFINITION('VISB_SVG_HOVERS', visb_hovers, SVG_ID, AttrList, Desc, DefName,
478 _DefPos, EvalPos, InlineObjects, no_separation, ExpandedScope),
479 add_visb_hovers_from_definition(SVG_ID, AttrList, Desc, DefName, EvalPos),
480 fail.
481 get_svg_objects_from_definitions(_InlineObjects,ExpandedScope,JsonFileContext) :- % VISB_SVG_UPDATES
482 precompile_svg_object_updates(ExpandedScope,JsonFileContext).
483
484 % example definition VISB_SVG_HOVERS == rec(`id`:"myid", stroke:"black", stroke_exit:"gray");
485 % a hovers field inside VISB_SVG_OBJECTS can be something like:
486 % rec(.... hovers: (rec(class:"train-hover"),rec(trigger_id:"track_polyline",class:"train-hover")), ...)
487 % also used, e.g., as attribute in VISB_SVG_OBJECTS
488 add_visb_hovers_from_definition(SVG_ID,AttrList, Desc, DefName, DefPos) :-
489 select(svg_attribute(hovers,Hovers),AttrList,AttrList2),
490 !,
491 (AttrList2=[] -> true ; add_warning(visb_visualiser,'Unknown extra hover attributes:',AttrList2,DefPos)),
492 flex_member(Record,Hovers,DefName,DefPos),
493 (get_VISB_record_fields(Record,Fields) -> true
494 ; add_warning(visb_visualiser,'VisB hovers field value is not a record of SVG attributes: ',Record,DefPos),fail),
495 include_maplist(extract_attribute_from_record(DefPos),Fields,HoverAttrList),
496 add_visb_object_from_definition(visb_hovers, SVG_ID, HoverAttrList, Desc, DefName, DefPos).
497 add_visb_hovers_from_definition(SVG_ID,AttrList, Desc, DefName, DefPos) :-
498 add_visb_object_from_definition(visb_hovers, SVG_ID, AttrList, Desc, DefName, DefPos).
499
500
501 % add a VisB record object from a HOVER or OBJECT definition:
502 add_visb_object_from_definition(visb_objects,SVG_ID, AttrList, Desc, DefName, DefPos) :- !,
503 ? (select(svg_attribute(svg_class,SVG_Class),AttrList,AttrList2)
504 -> true % maybe we should call svg_class svg_shape and
505 % allow html_tag for children of foreignObject
506 ; add_warning(visb_visualiser,'SVG objects have no svg_class field: ',DefName,DefPos),
507 fail
508 ),
509 assert_visb_svg_object(SVG_ID,SVG_Class,AttrList2,Desc,DefName,DefPos).
510 add_visb_object_from_definition(visb_hovers,SVG_ID, AttrList, _Desc, _DefName, DefPos) :- !,
511 (select(svg_attribute(trigger_id,TriggerID),AttrList,AttrList2) -> true
512 ; select(svg_attribute('trigger-id',TriggerID),AttrList,AttrList2) -> true
513 ; TriggerID = SVG_ID, AttrList2=AttrList),
514 member(svg_attribute(Attr,EnterVal),AttrList2), % will backtrack for every SVG attribute
515 \+ get_exit_attribute_name(_,Attr), % it is not an exit attribute
516 get_exit_attribute_name(Attr,AttrExitName),
517 (member(svg_attribute(AttrExitName,ExitVal), AttrList2) -> true % user specified exit value explicitly
518 ; visb_svg_object(SVG_ID,_,StaticAttrList,_,ExitPos)
519 -> (member(svg_attribute(Attr,ExitVal),StaticAttrList) -> true % use value specified in VISB_SVG_OBJECTS
520 ; default_attribute_value(Attr,ExitVal)
521 -> add_message(visb_visualiser,'Assuming default hover exit value for attribute: ',Attr,DefPos)
522 ; Attr = 'svg_class'
523 -> add_warning(visb_visualiser,
524 'svg_class cannot be set in hover for: ',SVG_ID,ExitPos),
525 ExitVal=EnterVal
526 ; (Attr = hover ; Attr = hovers) ->
527 add_error(visb_visualiser,
528 'Only provide SVG attributes here; no need to wrap them in this attribute:',Attr,DefPos),fail
529 ; add_warning(visb_visualiser,
530 'No static (exit) value can be retrieved for hover for attribute (be sure to define a static value for this attribute in a VISB_SVG_OBJECT definition): ',Attr,ExitPos),
531 ExitVal=EnterVal
532 )
533 ; ajoin(['No VISB_SVG_OBJECT for id ',SVG_ID,' and no value for ',AttrExitName,
534 '; cannot retrieve hover exit value for attribute: '],Msg),
535 add_warning(visb_visualiser,Msg,Attr,DefPos),
536 fail %ExitVal=EnterVal
537 ),
538 assert_visb_hover(TriggerID,SVG_ID,Attr,EnterVal,ExitVal,DefPos).
539 add_visb_object_from_definition(visb_events,SVG_ID, AttrList, _Desc, DefName, DefPos) :- !,
540 ( select(svg_attribute(event,Event),AttrList,AttrList1) -> true
541 ; select(svg_attribute(events,Events),AttrList,AttrList1) -> % we have events attributes with multiple events
542 flex_member(EvVal,Events,DefName,DefPos),
543 extract_attr_value(event,EvVal,Event,DefPos)
544 ; AttrList = [_|_], % at least one other attribute than id; otherwise it may stem from separating VISB_SVG_OBJECTS
545 add_warning(visb_visualiser,'Missing event attribute in VisB definition: ',DefName,DefPos),
546 fail
547 ),
548 (select(svg_attribute(predicate,Pred),AttrList1,AttrList2) -> Preds=[Pred]
549 ; member(P,[preds,predicates]),
550 select(svg_attribute(P,Pred),AttrList1,AttrList2)
551 -> Preds=[Pred], add_warning(visb_visualiser,'Use predicate as attribute for VisB events instead of: ',P,DefPos)
552 ; Preds=[], AttrList2=AttrList1
553 ),
554 EnableItems=[],
555 maplist(process_remaining_attributes(DefName,DefPos),AttrList2),
556 % TODO extract from AttrList2: visb_enable_item(SvgID,Attr,EnabledValExpr,DisabledValExpr,PosAttr)
557 (error_manager:extract_file_number_and_name(DefPos,_,File) -> true ; File='?'),
558 PredPos = DefPos, %TODO: improve
559 add_visb_event(SVG_ID,Event,Preds,[],EnableItems,File,DefPos,PredPos,[]).
560 add_visb_object_from_definition(SpecialClass,_, _, _, _DefName, DefPos) :-
561 add_warning(visb_visualiser,'Unknown special class, cannot add VisB objects for definition: ',SpecialClass,DefPos).
562
563 % for hovers allow to explicitly specify exit value, in case the SVG object comes from an SVG file
564 get_exit_attribute_name(Attr,ExitAttr) :- atom_concat(Attr,'_exit',ExitAttr).
565
566 process_remaining_attributes(DefName,DefPos,svg_attribute(hover,_)) :- !,
567 add_warning(visb_visualiser,'Attribute hover not supported here (use separate VISB_SVG_HOVERS definition): ',DefName,DefPos).
568 process_remaining_attributes(DefName,DefPos,svg_attribute(hovers,_)) :- !,
569 add_warning(visb_visualiser,'Attribute hovers not supported here (use separate VISB_SVG_HOVERS definition): ',DefName,DefPos).
570 process_remaining_attributes(_,DefPos,Attr) :-
571 add_warning(visb_visualiser,'Unrecognised attribute in VISB_SVG_EVENTS definition: ',Attr,DefPos).
572
573
574 default_attribute_value(fill,black). % is remove for animate, ...
575 default_attribute_value(opacity,1).
576 default_attribute_value('stop-dasharray',none).
577 default_attribute_value('stop-opacity',1).
578 default_attribute_value('stroke-opacity',1).
579 default_attribute_value('stroke-width','1px').
580 default_attribute_value(stroke,none).
581 default_attribute_value(transform,none).
582 default_attribute_value(visibility,visible).
583
584 % is called in process_json when no SVG file specified
585 % VISB_SVG_BOX == rec(width:1000,height:1000,viewBox:"minx miny w h"),
586 get_SVG_BOX_definition(InlineObjects) :-
587 ? get_and_eval_special_definition('VISB_SVG_BOX','VISB_SVG_BOX',visb_box,DefPos,ResValue,InlineObjects),
588 (ResValue=(BH,BW) -> ViewBox=''
589 ; get_VISB_record_fields(ResValue,Fields),
590 ? select(field(height,BH),Fields,F1),
591 ? select(field(width,BW),F1,F2)
592 ? -> (select(field(viewBox,VBVal),F2,F3)
593 -> (VBVal=string(VB) -> ViewBox=VB
594 % Viewbox is "mx my w h" string, ie: minimum_x, minimum_y, width and height
595 ; VBVal = rec(VBFields)
596 -> (get_view_box_rec(VBFields,DefPos,ViewBox) -> true
597 ; ViewBox='',
598 add_warning(visb_visualiser,'VISB_SVG_BOX viewBox record has illegal fields (expected minx miny width height):',VBVal,DefPos))
599 ; add_warning(visb_visualiser,'VISB_SVG_BOX viewBox is not a string ("minx miny width height") or record:',VBVal,DefPos),
600 ViewBox=''
601 )
602 ; ViewBox='', F3=F2
603 ),
604 (F3=[] -> true
605 ; add_warning(visb_visualiser,'VISB_SVG_BOX unknown attributes (not height, width, viewBox): ',F2,DefPos))
606 ; add_error(visb_visualiser,'Ignoring VISB_SVG_BOX, must be record or pair of integers (height,width):',ResValue,DefPos)),
607 (get_number_from_bvalue(BH,H) -> true
608 ; add_error(visb_visualiser,'VISB_SVG_BOX Height is not a number:',ResValue,DefPos)),
609 (get_number_from_bvalue(BW,W) -> true
610 ; add_error(visb_visualiser,'VISB_SVG_BOX Width is not a number:',ResValue,DefPos)),
611 !,
612 assert_visb_empty_svg_box_height_width(H,W,ViewBox,DefPos).
613
614 get_view_box_rec([field(height,VH),field(minx,MXH),field(miny,MYH),field(width,VW)],DefPos,ViewBoxString) :-
615 (get_number_from_bvalue(VH,Height) -> true
616 ; add_error('VISB_SVG_BOX viewBox\'height is not a number:',VH,DefPos),fail),
617 (get_number_from_bvalue(VW,Width) -> true
618 ; add_error('VISB_SVG_BOX viewBox\'width is not a number:',VH,DefPos),fail),
619 (get_number_from_bvalue(MXH,MinX) -> true
620 ; add_error('VISB_SVG_BOX viewBox\'minx is not a number:',VH,DefPos),fail),
621 (get_number_from_bvalue(MYH,MinY) -> true
622 ; add_error('VISB_SVG_BOX viewBox\'miny is not a number:',VH,DefPos),fail),
623 ajoin([MinX,' ',MinY,' ', Width,' ',Height],ViewBoxString).
624
625
626 assert_visb_empty_svg_box_height_width(H,W,_ViewBox,Pos) :-
627 retract(visb_empty_svg_box_height_width(OldH,OldW,_)),
628 (OldH,OldW) \= (H,W),
629 add_message(visb_visualiser,'Overriding VisB SVG_BOX default dimensions: ',(OldH,OldW),Pos),
630 fail.
631 assert_visb_empty_svg_box_height_width(H,W,ViewBox,_Pos) :-
632 %add_message(visb_visualiser,'Setting VisB SVG_BOX default dimensions: ',(H,W,ViewBox),Pos),
633 assert(visb_empty_svg_box_height_width(H,W,ViewBox)).
634
635 :- use_module(probsrc(bsyntaxtree), [get_texpr_pos/2]).
636 :- use_module(probsrc(bmachine),[b_sorted_b_definition_prefixed/4, b_get_typed_definition/3]).
637 % find DEFINITION with given prefix in name, evaluate it and return SVG_ID and attribute list:
638 % AllowSep = allow_seperation means that the record fields can be separated into static objects and dynamic updates
639 % and only static ones will be retained (dynamic ones dealt with later)
640 find_and_eval_visb_DEFINITION(DEFPREFIX, Kind, SVG_ID, AttrList,Desc, DefName, DefPos,EvalPos,
641 InlineObjects,AllowSep,ExpandedScope) :-
642 ? ( b_sorted_b_definition_prefixed(expression,DEFPREFIX,DefName,DefPos),
643 ? if(b_get_typed_definition(DefName,ExpandedScope,Body),true,
644 (add_message(visb_visualiser,'Ignoring VisB DEFINITION due to errors: ',DefName),fail))
645 ; special_backup(DEFPREFIX,Kind),
646 % also look at stored definitions (e.g., from static/dynamic separation of VISB_SVG_OBJECTS)
647 visb_special_definition(Kind,DefName,_Type,Body,_Class,DefPos)
648 ),
649 set_error_context(visb_error_context(definition,DefName,'all_attributes',DefPos)),
650 ? call_cleanup((get_typed_static_definition_with_constants_state(DefName,Body,
651 ResBody,DefPos,ConstState,InlineObjects,AllowSep),
652 (get_texpr_pos(ResBody,Pos0) -> true ; Pos0=DefPos), % this could be a part of the full definition body
653 get_visb_DEFINITION_svg_object(Kind,DefName,ResBody,Pos0,ConstState,SVG_ID,AttrList,Desc,EvalPos)),
654 clear_error_context).
655
656 special_backup('VISB_SVG_HOVERS',visb_hovers).
657
658 % evaluate a typed body expressions evaluating to a record or set of records
659 % and translate into SVG attribute lists:
660 get_visb_static_svg_object_for_typed_expr(Kind,DefName,Body,DefPos,SVG_ID,AttrList,Desc,InnerPos) :-
661 AllowSep=no_separation,
662 Inline=no_inlining,
663 get_typed_static_definition_with_constants_state(DefName,Body,ResBody,DefPos,ConstState,Inline,AllowSep),
664 get_visb_DEFINITION_svg_object(Kind,DefName,ResBody,DefPos,ConstState,SVG_ID,AttrList,Desc,InnerPos).
665
666
667 flatten_couple(b(couple(A,B),_,_)) --> !,flatten_couple(A),flatten_couple(B).
668 % we could also flatten union(A,B), but at the risk of duplicate warnings when the same element occurs in A and B
669 flatten_couple(A) --> [A].
670
671 get_typed_static_definition_with_constants_state(DefName,Body,ResBody,DefPos,ConstantsState,InlineObjects,AllowSep) :-
672 flatten_couple(Body,TupleList,[]),
673 % the VISB_SVG_OBJECT definition may consist of a tuple (Obj1,Obj2,...) to allow grouping
674 (TupleList = [_,_|_]
675 -> add_debug_message(visb_visualiser,'Decomposed VisB definition body tuple:',DefName,DefPos)
676 ; true),
677 ? nth1(DefNr,TupleList,TupleBody),
678 (get_texpr_pos(TupleBody,TuplePos) -> true ; TuplePos=DefPos),
679 get_typed_static_definition_with_constants_state3(DefName,DefNr,TupleBody,ResBody,TuplePos,
680 ConstantsState,InlineObjects,AllowSep).
681 get_typed_static_definition_with_constants_state3(DefName,DefNr,Body,ResBody,DefPos,ConstantsState,InlineObjects,AllowSep) :-
682 determine_type_of_visb_formula(Body,TIds,Class),
683 debug_format(19,'Detected VisB DEFINITION ~w (~w)~n',[DefName,Class]),
684 (%Class=requires_variables, % now also useful if event field present
685 AllowSep=allow_separation, % allowed for VISB_SVG_OBJECTS
686 ? if(separate_into_static_and_dynamic_part(DefName,DefNr,Body,StaticBody,DynamicBody,EventBody,HoverBody),
687 true,
688 (get_texpr_type(Body,Type),
689 (contains_events_or_hovers_field(Type)
690 -> add_warning(visb_visualiser,'Static/Dynamic separation failed for (required for events or hovers): ',DefName,DefPos)
691 % VISB_SVG_OBJECT definition contains events/hovers and as such requires separation; which failed here
692 ; add_debug_message(visb_visualiser,'Static/Dynamic separation failed or not useful for: ',DefName,DefPos)
693 ),
694 fail)),
695 determine_type_of_visb_formula(StaticBody,SIds,SClass),
696 get_unique_initial_state_for_visb(SClass,DefName,DefPos,SIds,ConstantsState)
697 -> Separated=true, ResBody=StaticBody,
698 add_debug_message(visb_visualiser,'Automatically separated fields into static and dynamic: ',DefName,DefPos),
699 %write('STATIC: '),translate:print_bexpr(StaticBody),nl, write('DYNAMIC: '),translate:print_bexpr(DynamicBody),nl,
700 assert_visb_udpate_def_body(visb_updates,DefName,DynamicBody,DefPos),
701 add_visb_events_from_def_body(visb_events,DefName,EventBody,DefPos),
702 assert_visb_udpate_def_body(visb_hovers,DefName,HoverBody,DefPos) % needs to be asserted so that it can be evaluated after svg objects have been created to extract exit value
703 ; get_unique_initial_state_for_visb(Class,DefName,DefPos,TIds,ConstantsState)
704 -> ResBody=Body
705 ; ResBody=Body,
706 (Class=requires_constants ->
707 get_texpr_ids(TIds,Ids),
708 % we could check if values of Ids are identical in all constants solutions
709 (is_concrete_constants_state_id(_)
710 -> BMsg='multiple solutions for used constants exist: '
711 ; BMsg='but no constants were found or setup yet: '
712 ),
713 ajoin(['DEFINITION ',DefName, ' requires constants but ',BMsg],Msg),
714 (get_a_constants_state(ConstantsState,StateID,InlineObjects)
715 -> (member(CstID,Ids),
716 other_constant_value_exists_for(CstID,ConstantsState,StateID)
717 -> add_warning(visb_visualiser,Msg,CstID,DefPos)
718 ; ajoin(['DEFINITION ',DefName,
719 ' requires constants and all SETUP_CONSTANTS solutions have same value thus far: '],Msg2),
720 % constraint-based checks or execute by predicate could later create others !
721 add_message(visb_visualiser,Msg2,Ids,DefPos)
722 )
723 ; add_error(visb_visualiser,Msg,Ids,DefPos), ConstantsState=[]
724 )
725 ; ConstantsState=[]
726 )
727 ),
728 (Class=requires_variables, Separated=false
729 -> get_texpr_ids(TIds,AIds),
730 include(b_is_variable,AIds,VIds),
731 ajoin_with_sep(VIds,',',SVids),
732 (get_preference(visb_allow_variables_for_objects,false)
733 -> ajoin(['Ignoring DEFINITION which requires variables ',SVids,': '],WMsg),
734 add_warning(visb_visualiser,WMsg,DefName,DefPos),fail
735 ; ConstantsState=[]
736 -> add_warning(visb_visualiser,'Ignoring DEFINITION which requires variables, could not find unique initial state: ',DefName,DefPos),fail
737 ; ajoin(['DEFINITION requires variables ',SVids,
738 '; exporting history to HTML may not work correctly: '],WMsg),
739 add_message(visb_visualiser,WMsg,DefName,DefPos)
740 )
741 ; true).
742
743
744 :- use_module(probsrc(bsyntaxtree), [create_couple/2, create_couple/3]).
745 % separate/split/filter VISB_SVG_OBJECTS definitions into a static part and a dynamic part depending on variables
746 % (aka updates/items)
747 separate_into_static_and_dynamic_part(DefName,DefNr,Body,StaticBody,DynamicBody,EventBody,HoverBody) :-
748 ? separate_static_dyn_aux(DefName,DefNr,[],[],Body,StaticBody,DynamicBody,EventBody,HoverBody).
749
750
751 :- use_module(probsrc(state_space),[ time_out_for_node/3]).
752 :- use_module(probsrc(specfile),[ translate_operation_name/2]).
753 :- use_module(probsrc(bsyntaxtree),[replace_ids_by_exprs/4]).
754 rewrite_expression(let_expression(Ids,Exprs,Body),NewBody) :-
755 % currently we cannot process LET's here, expand them
756 replace_ids_by_exprs(Body,Ids,Exprs,NewBody). % see also expand_all_lets/2
757
758 separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,Path,b(Expr,_Type,_Info), Static,Dynamic,Event,Hover) :-
759 rewrite_expression(Expr,NewExpr),!,
760 separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,Path,NewExpr, Static,Dynamic,Event,Hover).
761 separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,Path,b(couple(A,B),_,_Info),
762 StaticCouple,DynamicCouple,EventCouple,HoverCouple) :- !,
763 separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,[0|Path],A,SA,DA,EA,HA),
764 separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,[1|Path],B,SB,DB,EB,HB),
765 create_couple(SA,SB,StaticCouple),
766 create_couple(DA,DB,DynamicCouple),
767 create_couple(EA,EB,EventCouple),
768 create_couple(HA,HB,HoverCouple).
769 separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,Path,TExpr,
770 b(StaticSetComp,set(ST),I),
771 b(DynamicSetComp,set(DT),I),
772 b(EventsSetComp,set(ET),I),
773 b(HoversSetComp,set(HT),I)) :-
774 ? bsyntaxtree:is_eventb_comprehension_set(TExpr,Ids,Pred,Expr),
775 (OuterQuantifiedIds = []
776 -> add_debug_message(visb_visualiser,'Top-level set comprehensions for VISB: ',Ids,TExpr)
777 ; add_message(visb_visualiser,'Nested set comprehensions for VISB: ',OuterQuantifiedIds,TExpr)
778 ),
779 !,
780 determine_type_of_visb_formula(b(exists(Ids,Pred),pred,[]),SIds,Class),
781 (get_unique_initial_state_for_visb(Class,DefName,Pred,SIds,_)
782 -> true % The predicate must be statically executable
783 ; time_out_for_node(root,O,_Type),
784 translate_operation_name(O,Op) ->
785 ajoin(['Due to TIME_OUT of ',Op,' the comprehension set domain cannot be evaluated: '],Msg),
786 add_warning(visb_visualiser,Msg,Pred,Pred),
787 % TODO: avoid other error messages that will occur after that
788 fail
789 ; add_message(visb_visualiser,'Cannot statically evaluate comprehension set domain: ',Pred,Pred),
790 % at the moment we require the domain to be computable statically for both static/dynamic attributes
791 fail
792 ),
793 append(OuterQuantifiedIds,Ids,NewOuterQuantifiedIds),
794 ? separate_static_dyn_aux(DefName,DefNr,NewOuterQuantifiedIds,Path,Expr,
795 StaticRec,DynamicRec,EventRec,HoverRec),
796 get_texpr_type(StaticRec,ST),
797 get_texpr_type(DynamicRec,DT),
798 get_texpr_type(EventRec,ET),
799 get_texpr_type(HoverRec,HT),
800 bsyntaxtree:get_texpr_info(TExpr,I),
801 b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,StaticRec,Pred, set(ST), StaticSetComp),
802 b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,DynamicRec,Pred,set(DT), DynamicSetComp),
803 b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,EventRec,Pred,set(ET), EventsSetComp),
804 b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,HoverRec,Pred,set(HT), HoversSetComp).
805 separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,Path,b(rec(Fields),_,Info),
806 b(rec(StaticFields),record(SFT),Info), % VISB_OBJECTS (static)
807 b(UpdateRecWithDynamicFields,record(DFT),Info), % VISB_UPDATES (dynamic)
808 b(rec(AllEventFields),record(EFT),Info), % VISB_EVENTS
809 b(rec(AllHoverFields),record(HFT),Info) % VISB_HOVERS
810 ) :- !,
811 split_list(is_visb_event_field,Fields,EventFields,ObjectAndHoverFields),
812 (select(field(hovers,HoverRec),ObjectAndHoverFields,ObjectFields)
813 -> HoverFields = [field(hovers,HoverRec)] % record deconstructed in add_visb_hovers_from_definition
814 ; ObjectFields=ObjectAndHoverFields, HoverFields = []),
815 % maplist(check_field_is_supported(Info),ObjectFields), % will lead to duplicate warning messages, check_visb_update_type e.g., will be called for dynamic updates
816 separate_fields(ObjectFields,StaticFields0,DynamicFields,DefName),
817 ? (member(field(svg_class,_SVG_Class),StaticFields0) -> true
818 ; member(field(svg_class,SVG_Class),DynamicFields)
819 -> add_warning(visb_visualiser,'SVG svg_class field is not static in: ',DefName,SVG_Class),
820 fail
821 ; add_warning(visb_visualiser,'No svg_class field in: ',DefName,Info),
822 fail
823 ),
824 ? (member(field(id,SVGID),StaticFields0)
825 -> (DynamicFields \= [] ; EventFields \= [] ; HoverFields \= [] % separation is useful for this record
826 ; Path \= [] % we are part of a couple; maybe other records have a dynamic,event or hover part; so proceed
827 ),
828 StaticFields = StaticFields0,
829 TStatic_SVGID = SVGID
830 ; member(field(id,SVGID),DynamicFields)
831 -> add_warning(visb_visualiser,'SVG id field is not static in: ',DefName,SVGID),
832 fail
833 ; OuterQuantifiedIds = []
834 -> gensym(svg_id,GenID),
835 ajoin(['Generated id ',GenID, ' for SVG object without id field in: '],Msg),
836 add_debug_message(visb_visualiser,Msg,DefName,Info),
837 SVGID = b(string(GenID),string,[]),
838 sort([field(id,SVGID) | StaticFields0],StaticFields)
839 ; % the record is quantified within a set comprehension; we need to compute the ID from OuterQuantifiedIds
840 % it has to be identical for VISB_SVG_OBJECTS and VISB_SVG_UPDATES
841 SVGID = b(ExtFunCall,string,[]),
842 convert_path_to_int(Path,IntPath),
843 PathExpr = b(integer(IntPath),integer,[]),
844 create_couple([b(string(DefName),string,[]),b(integer(DefNr),integer,[]),PathExpr|OuterQuantifiedIds],Tuple),
845 % add DefName and DefNr to avoid clash if other Definition has same quantified ids
846 ExtFunCall = external_function_call('SHA_HASH_HEX',[Tuple]),
847 add_debug_message(visb_visualiser,'Generated SHA_HASH_HEX call for id of SVG objects without id field in: ',DefName,Info),
848 sort([field(id,SVGID) | StaticFields0],StaticFields)
849 ),
850 maplist(get_field_type,StaticFields,SFT),
851 ( (select(field(visibility,VisibExpr),DynamicFields,RestDynamicFields)
852 ; member(field(visibility,VisibExpr),StaticFields0), % the visibility expression is static
853 RestDynamicFields = DynamicFields
854 ),
855 RestDynamicFields = [_|_],
856 \+ hovers_can_set_visibility(HoverFields),
857 (nonvar(TStatic_SVGID), TStatic_SVGID = b(string(Static_SVGID),_,_) % TODO: evaluate properly
858 -> \+ visb_has_visibility_hover(Static_SVGID) % TODO: check no other hover definition added later
859 ; true) % the ID is generated and cannot be accessed by other hovers which could make object visible
860 -> % create IF-THEN-ELSE to avoid evaluating fields when object not visible; also fixes WD issues
861 TRUE = b(boolean_true,boolean,[]),
862 sort([field(id,SVGID),field(visibility,TRUE)|RestDynamicFields],AllDynamicFields),
863 maplist(construct_dummy_value,RestDynamicFields,RestDummyFields),
864 sort([field(id,SVGID),field(visibility,b(boolean_false,boolean,[]))|RestDummyFields],AllDummyFields),
865 create_visibility_check(VisibExpr,VisibilityCond),
866 UpdateRecWithDynamicFields = if_then_else(VisibilityCond,
867 b(rec(AllDynamicFields),record(DFT),Info),
868 b(rec(AllDummyFields),record(DFT),Info)),
869 add_debug_message(visb_visualiser,'Refactoring VisB Record with visibility attribute: ',VisibilityCond)
870 % ,translate:print_bexpr(b(UpdateRecWithDynamicFields,any,[])),nl
871 ; sort([field(id,SVGID)|DynamicFields],AllDynamicFields), % TODO: use kernel_records
872 UpdateRecWithDynamicFields = rec(AllDynamicFields)
873 ),
874 maplist(get_field_type,AllDynamicFields,DFT),
875 sort([field(id,SVGID)|EventFields],AllEventFields), % ditto
876 maplist(get_field_type,AllEventFields,EFT),
877 sort([field(id,SVGID)|HoverFields],AllHoverFields), % ditto
878 maplist(get_field_type,AllHoverFields,HFT).
879 separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,_Path,TEXPR, _, _, _,_) :-
880 ajoin(['Uncovered expression for ',DefName,'-',DefNr,' ',OuterQuantifiedIds],Msg),
881 add_debug_message(visb_visualiser,Msg,TEXPR,TEXPR),fail.
882
883 hovers_can_set_visibility(HoverFields) :- member(field(hovers,Expr),HoverFields),
884 hover_expr_can_set_visibility(Expr).
885
886 hover_expr_can_set_visibility(b(E,_,_)) :- hovers_can_set_visib_aux(E).
887 hovers_can_set_visib_aux(couple(A,B)) :- !, (hover_expr_can_set_visibility(A) ; hover_expr_can_set_visibility(B)).
888 hovers_can_set_visib_aux(rec(Fields)) :- !, member(field(visibility,_),Fields).
889 hovers_can_set_visib_aux(set_extension(L)) :- !, member(E,L), hover_expr_can_set_visibility(E).
890 hovers_can_set_visib_aux(E) :- write(assume_hover_can_set_visibility(E)),nl.
891 % TODO: synchronise with flex_expand and check we cover all relevant cases like partial functions
892
893 :- use_module(probsrc(bsyntaxtree), [create_equality/3]).
894 create_visibility_check(VisibExpr,VisibilityCond) :- get_texpr_type(VisibExpr,string),!,
895 VISIBLE = b(string('visible'),string,[]),
896 create_equality(VisibExpr,VISIBLE,VisibilityCond).
897 create_visibility_check(VisibExpr,VisibilityCond) :-
898 TRUE = b(boolean_true,boolean,[]),
899 create_equality(VisibExpr,TRUE,VisibilityCond).
900
901 :- use_module(probsrc(typing_tools),[any_value_for_type/2]).
902 construct_dummy_value(field(Name,TExpr),field(Name,b(value(DummyValue),Type,[]))) :-
903 get_texpr_type(TExpr,Type),
904 any_value_for_type(Type,DummyValue). % object not visible: do not evaluate expression; just produce dummy value
905
906 % treat path of 0,1 as binary number, but add 1 at end to distinguish [0,0] and [0] or [1,0] and [1,0,0]
907 convert_path_to_int([],1).
908 convert_path_to_int([H|T],Res) :- convert_path_to_int(T,IT),
909 Res is IT*2+H.
910
911 % is the name of a field for events inside a VISB_SVG_OBJECT record
912 % example rec(..., event:"BOperation", predicate:"x=TRUE")
913 is_visb_event_field(field(Name,_)) :- is_visb_event_field_name(Name).
914 is_visb_event_field_name(event).
915 is_visb_event_field_name(events). % tuple or set of events inside VISB_SVG_OBJECTS
916 is_visb_event_field_name(predicate).
917 is_visb_event_field_name(predicates). % will generate warning
918 is_visb_event_field_name(preds). % will generate warning
919 % is the name of a field for hovers inside a VISB_SVG_OBJECT record
920 is_visb_hover_field_name(hovers).
921 is_visb_hover_field_name(items). % enable items
922 %is_visb_hover_field_name(optional). % not needed ?
923 %is_visb_hover_field_name(override). % not needed ?
924
925 % check if the type of a VISB_SVG_OBJECTS expression requires separation for hovers/events
926 contains_events_or_hovers_field(set(X)) :- contains_events_or_hovers_field(X).
927 contains_events_or_hovers_field(couple(A,B)) :-
928 (contains_events_or_hovers_field(A) -> true ; contains_events_or_hovers_field(B)).
929 contains_events_or_hovers_field(record(F)) :- member(field(Name,_),F),
930 (is_visb_event_field_name(Name) -> true ; is_visb_hover_field_name(Name)).
931
932 get_field_type(field(Name,Expr),field(Name,T)) :- get_texpr_type(Expr,T).
933
934 % separate fields from a SVG/VISB_SVG_OBJECT record into static part and dynamic update expressions
935 separate_fields([],[],[],_).
936 separate_fields([field(Field,Expr)|T],[field(Field,Expr)|TS],TD,DefName) :-
937 is_static_expr(Expr,Field,DefName),!,
938 separate_fields(T,TS,TD,DefName).
939 separate_fields([field(Field,Expr)|T],[field(Field,Default)|TS],[field(Field,Expr)|TD],DefName) :-
940 requires_static_default_value(Field,Default), !,
941 separate_fields(T,TS,TD,DefName).
942 separate_fields([H|T],TS,[H|TD],DefName) :-
943 separate_fields(T,TS,TD,DefName).
944
945 % fields which require a static default value; here to set up child SVG objects of title
946 % static default values could also be useful for hovers in general?
947 requires_static_default_value(title,b(string('-title-not-set-'),string,[])).
948
949 % virtual SVG attributes which are translated to children tags/objects
950 attribute_automatically_creates_children(title).
951
952 is_static_expr(Expr,Field,DefName) :-
953 determine_type_of_visb_formula(Expr,_TIds,Class), % TODO pass local variables from exists above
954 (Class=requires_nothing -> true
955 ; Class=requires_constants,
956 \+ multiple_concrete_constants_exist, % TODO: check if _TIds have multiple solutions
957 is_concrete_constants_state_id(_) -> true
958 ; ajoin(['Detected dynamic expression for field ',Field,' in ',DefName,': '],Msg),
959 add_debug_message(visb_visualiser,Msg,Expr,Expr),fail
960 ).
961
962 % --------
963
964
965 extract_attribute_from_record(DefPos,field(OrigName,Value),svg_attribute(Name,SVal)) :-
966 opt_rewrite_field_name(OrigName,Name),
967 extract_attribute_value(DefPos,Name,Value,SVal).
968 extract_attribute_from_record(DefPos,F,_) :-
969 add_error(bvisualiser,'Extract SVG attribute failed: ',F,DefPos),fail.
970
971 % extract a value for a particular field Name
972 extract_attribute_value(DefPos,Name,Value,SVal) :-
973 (deconstruct_singleton_set(Name,Value,Element)
974 -> Element \= '$optional_field_absent',
975 extract_attr_value(Name,Element,SVal,DefPos)
976 ; extract_attr_value(Name,Value,SVal,DefPos)
977 ).
978
979 :- use_module(probsrc(specfile), [classical_b_mode/0]).
980
981 % in TLA+ mode optional record fields have {TRUE|->VALUE} rather than VALUE
982 % this can also be useful in B to allow mixing different SVG records in a set
983 % for Alloy mode we may want to also support singleton sets as scalars
984 deconstruct_singleton_set(Name,Set,Res) :-
985 singleton_set(Set,El),
986 detect_partial_records_for_field(Name),
987 (El=(pred_true,El2)
988 -> Val=El2 % TLA2B encoding for optional fields that are present
989 ; Val=El), % Alloy
990 !,
991 Res = Val.
992 deconstruct_singleton_set(Name,[],Res) :-
993 detect_partial_records_for_field(Name),
994 Res = '$optional_field_absent'.
995
996 detect_partial_records_for_field(children) :- !, fail. % children field for groups is a set of ids
997 detect_partial_records_for_field(Name) :-
998 is_svg_number_attribute(Name),!. % sets never sensible as a numerical value
999 detect_partial_records_for_field(Name) :- is_id_or_text_attribute(Name),!. % ditto for ids
1000 detect_partial_records_for_field(Name) :- is_svg_color_attribute(Name),!. % ditto for colors
1001 detect_partial_records_for_field(_) :-
1002 ? \+ classical_b_mode. % TODO: check that we are in TLA or Alloy mode?
1003 % TODO: ensure ProB2 sets animation minor mode for TLA
1004
1005 :- use_module(probsrc(tools),[split_chars/3, safe_number_codes/2,safe_atom_codes/2]).
1006 :- use_module(extrasrc(external_functions_svg),[svg_points/4]).
1007 extract_attr_value(Name,Value,SVal,DefPos) :-
1008 is_svg_number_attribute(Name),!, % we could try and extract svg_class from attribute list above
1009 (get_number_from_bvalue(Value,NrVal)
1010 -> SVal=NrVal % convert to atom?
1011 ; b_value_to_string(Value,SVal),
1012 (is_special_svg_number_form(SVal) -> true
1013 ; atom_codes(SVal,CC),
1014 safe_number_codes(_NrVal,CC) -> true
1015 ; ajoin(['The value of the SVG attribute "',Name,
1016 '" is not a number: '],Msg),
1017 add_warning(visb_visualiser,Msg,SVal,DefPos)
1018 )
1019 ).
1020 extract_attr_value(children,Value,SVal,DefPos) :- !,
1021 (is_set_value(Value,extract_attr_value)
1022 -> (try_expand_custom_set_with_catch(Value,ExpandedSet,extract_attr_value),
1023 maplist(b_value_to_id_string,ExpandedSet,SVal) -> true
1024 ; add_warning(visb_visualiser,'The children attribute should be a finite set of identifiers: ',Value,DefPos),
1025 SVal=[]
1026 )
1027 ; add_warning(visb_visualiser,'The children attribute should be a set of identifiers: ',Value,DefPos),
1028 SVal=[]).
1029 extract_attr_value(points,Value,SVal,DefPos) :- % Class should be polygon or polyline
1030 % automatically translate sequences or sets of pairs of numbers to SVG string format
1031 (Value = [(Nr,_)|_] ; Value = avl_set(node((Nr,_),_,_,_,_))),
1032 is_number(Nr), % TODO: check typing
1033 svg_points(Value,Str,DefPos,no_wf_available),!,
1034 string(SVal)=Str.
1035 extract_attr_value(points,Value,SVal,_DefPos) :- Value = [],!, SVal = ''.
1036 extract_attr_value(visibility,Value,SVal,DefPos) :- !,
1037 % convert TRUE -> visible, FALSE -> hidden
1038 ( Value=pred_true -> TxtVal='visible'
1039 ; Value=pred_false -> TxtVal='hidden'
1040 ; b_value_to_text_string(Value,TxtVal),
1041 ? (member(TxtVal,[collapse,hidden,visible]) -> true
1042 ; add_warning(visb_visualiser,'Value of SVG attribute "visibility" must be collapse,hidden or visible and not: ',TxtVal,DefPos))
1043 ),
1044 SVal=TxtVal.
1045 extract_attr_value(Name,Value,_,DefPos) :-
1046 is_svg_color_attribute(Name),
1047 illegal_color(Value),
1048 ajoin(['Value of SVG attribute "',Name,
1049 '" is not a colour: ' ],Msg),
1050 add_warning(visb_visualiser,Msg,Value,DefPos),fail.
1051 extract_attr_value(Name,Value,SVal,_) :-
1052 ? is_id_or_text_attribute(Name),!,
1053 (is_text_attribute(Name)
1054 -> b_value_to_text_string(Value,SVal)
1055 ; b_value_to_id_string(Value,SVal)). % concatenates e.g. pairs of strings to string without ( |-> )
1056 extract_attr_value(Attr,RawValue,ResValue,_DefPos) :- raw_value_attribute(Attr),!, % keep value intact
1057 ResValue = RawValue.
1058 extract_attr_value(Name,Value,SVal,DefPos) :-
1059 b_value_to_string(Value,SVal),
1060 ? (is_svg_attribute_with_fixed_values(Name,List), \+ member(SVal,List)
1061 -> ajoin_with_sep(List,',',Opts),
1062 ajoin(['Value of SVG attribute "',Name,'" must be ',Opts,' and not: '],Msg),
1063 add_warning(visb_visualiser,Msg,SVal,DefPos)
1064 ; true).
1065
1066
1067
1068 is_number(int(_)).
1069 is_number(term(floating(_))).
1070
1071 % do not convert to string; these are treated separately
1072 raw_value_attribute(hovers).
1073 raw_value_attribute(events).
1074
1075 % now checked by check_attribute_type for updates, we could later check strings, currentcolor is allowed
1076 illegal_color(pred_false).
1077 illegal_color(pred_true).
1078 illegal_color([]).
1079 illegal_color(avl_set(_)).
1080 illegal_color([_|_]).
1081 illegal_color(closure(_,_,_)).
1082 illegal_color(term(floating(_))).
1083
1084 % evaluate a DEFINITION to a set of B records representing SVG objects
1085 % returns a possibly refined sub-position corresponding to generated SVG objects as last argument
1086 get_visb_DEFINITION_svg_object(SpecialClass,DefName,Body,_DefPos,ExpandedState,SVG_ID,AttrList,Desc,InnerPos) :-
1087 get_preference(visb_show_debug_infos,true),
1088 bsyntaxtree:is_eventb_comprehension_set(Body,Ids,Pred,Expr),
1089 % try and separate couple in Expr so that we have better position info for source of VISB_SVG_OBJECTS
1090 Body = b(_,Type,II),
1091 Expr = b(couple(_,_),_,_),
1092 !,
1093 couple_member(NewExpr,Expr), % evaluate each part of the couple in isolation, with better position info
1094 get_texpr_pos(NewExpr,InnerPos),
1095 b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,NewExpr,Pred, Type, NewBody),
1096 get_visb_DEF_svg_object_aux(SpecialClass,DefName,b(NewBody,Type,II),InnerPos,ExpandedState,SVG_ID,AttrList,Desc).
1097 get_visb_DEFINITION_svg_object(SpecialClass,DefName,Body,DefPos,ExpandedState,SVG_ID,AttrList,Desc,DefPos) :-
1098 ? get_visb_DEF_svg_object_aux(SpecialClass,DefName,Body,DefPos,ExpandedState,SVG_ID,AttrList,Desc).
1099
1100 couple_member(TExpr,b(couple(A,B),_,_)) :- !, (couple_member(TExpr,A) ; couple_member(TExpr,B)).
1101 couple_member(TExpr,TExpr).
1102
1103 get_visb_DEF_svg_object_aux(SpecialClass,DefName,Body,DefPos,ExpandedState,SVG_ID,AttrList,Desc) :-
1104 evaluate_visb_formula(Body,DefName,'',ExpandedState,ResValue,DefPos),
1105 flex_expand(ResValue,DefName,DefPos,Expanded,[]),
1106 (Expanded = [] -> add_message(visb_visualiser,'Empty set of SVG object records: ',DefName,DefPos)
1107 ; Expanded =[Record|_] ->
1108 (get_VISB_record_fields(Record,Fs)
1109 % TODO: as we now can have different type of records, check in flex_expand below
1110 ? -> (member(field(id,_),Fs)
1111 -> true
1112 ; add_message(visb_visualiser,'DEFINITION needs an `id` field if you want to use updates: ',DefName,DefPos)
1113 )
1114 ; ajoin(['DEFINITION ', DefName,' should evaluate to a set of records or tuples of records: '],Msg),
1115 add_warning(visb_visualiser,Msg,Record,DefPos)
1116 )
1117 ),
1118 ? member(Records,Expanded),
1119 get_VISB_record_fields(Records,Fields),
1120 ? (select(field(id,VID),Fields,F1)
1121 -> extract_attribute_value(DefPos,id,VID,SVG_ID)
1122 ; gensym(svg_id,SVG_ID), F1=Fields),
1123 (select(field(comment,CC),F1,F2), b_value_to_string(CC,Desc) -> true
1124 ; Desc = '', F2=F1),
1125 (SpecialClass=visb_updates, member(field(visibility,VV),F2),
1126 is_invisible(VV),
1127 \+ visb_has_visibility_hover(SVG_ID) % check for hover which may make object visible
1128 -> AttrList=[svg_attribute(visibility,'hidden')] % do not transmit updates
1129 ? ; include_maplist(extract_attribute_from_record(DefPos),F2,AttrList0),
1130 exclude(check_unsupported_special_visb_attribute(SpecialClass,DefPos),AttrList0,AttrList),
1131 ? (select(svg_attribute(svg_class,SVG_Class),AttrList,A2)
1132 -> maplist(check_attribute_is_supported(SVG_Class,DefPos),A2)
1133 ; true)
1134 ).
1135
1136 is_invisible(string(hidden)). % also treat collapse ?
1137 is_invisible(pred_false).
1138
1139 % expand nested tuples/sets to a single list of SVG records (possibly of different types)
1140 flex_expand(Value,DefName,Pos) --> {is_custom_explicit_set(Value)},!,
1141 {try_expand_custom_set_with_catch(Value,ExpandedSet,flex_expand),
1142 (is_custom_explicit_set(ExpandedSet)
1143 -> ajoin(['Could not expand set of SVG object records or tuples thereof for ',DefName,': '],Msg),
1144 add_warning(visb_visualiser,Msg,Value,Pos),
1145 fail
1146 ; true)},
1147 flex_expand(ExpandedSet,DefName,Pos).
1148 flex_expand([],_,_) --> !, [].
1149 flex_expand(L,_DefName,_Pos) --> {L =[(string(_),string(_))|_]}, !,
1150 [L]. % is probably a partial function {"id" |-> ,...}
1151 flex_expand([H|T],DefName,Pos) --> !, flex_expand(H,DefName,Pos), l_flex_expand(T,DefName,Pos).
1152 flex_expand((A,B),DefName,Pos) --> !, flex_expand(A,DefName,Pos), flex_expand(B,DefName,Pos).
1153 flex_expand(T,_,_) --> [T].
1154
1155 l_flex_expand([],_,_) --> !, [].
1156 l_flex_expand([H|T],DefName,Pos) --> !, flex_expand(H,DefName,Pos), l_flex_expand(T,DefName,Pos).
1157 l_flex_expand(T,_,_) --> [T].
1158
1159 flex_member(X,SetPairVal,DefName,Pos) :- flex_expand(SetPairVal,DefName,Pos,List,[]), member(X,List).
1160
1161
1162 % get the fields of a B value record
1163 % also transparently handles alternative representations, like a function from STRING to STRING
1164 get_VISB_record_fields(rec(Fields),Res) :- !, Res=Fields.
1165 get_VISB_record_fields(StringFunction,Fields) :-
1166 is_set_value(StringFunction,get_VISB_record_fields),
1167 try_expand_custom_set_with_catch(StringFunction,Expanded,get_VISB_record_fields),
1168 % TODO: check we have no duplicates
1169 maplist(convert_to_field,Expanded,Fields).
1170 % TODO: support records as generated by READ_XML:
1171 % rec(attributes:{("fill"|->"#90ee90"),("height"|->"360px"),("id"|->"background_rect"),("width"|->"600px"),("x"|->"1px"),("y"|->"2px")},element:"rect",meta:{("xmlLineNumber"|->"3")},pId:5,recId:6)
1172 % for <rect height="360px" x="1px" y="2px" id="background_rect" width="600px" fill="#90ee90"></rect>
1173
1174 convert_to_field((string(FieldName),Value),field(FieldName,Value)).
1175 % TODO: maybe handle enumerated set values as field names
1176
1177
1178 % already extract and type-check VISB_SVG_UPDATES definitions
1179 precompile_svg_object_updates(ExpandedScope,JsonFileContext) :-
1180 b_sorted_b_definition_prefixed(expression,'VISB_SVG_UPDATES',DefName,DefPos),
1181 b_get_typed_definition(DefName,ExpandedScope,TypedExpr),
1182 assert_visb_udpate_def_body(visb_updates,DefName,TypedExpr,DefPos),
1183 add_children_for_visb_update_def_body(TypedExpr,DefName,JsonFileContext),
1184 fail.
1185 precompile_svg_object_updates(_,_).
1186
1187 % assert VisB updates or hovers from B DEFINITION,
1188 % either from VISB_SVG_UPDATES or hovers or dynamic parts of VISB_SVG_OBJECTS:
1189 assert_visb_udpate_def_body(_Kind,DefName,TypedExpr,_DefPos) :-
1190 TypedExpr=b(rec([field(id,_)]),_,Info),!, % can happen when all fields are static
1191 add_debug_message(visb_visualiser,'Useless update/hover (just id field): ',DefName,Info).
1192 assert_visb_udpate_def_body(Kind,DefName,b(couple(A,B),_,_),DefPos) :- !,
1193 % separate couples into individual expressions; in case of WD errors we have more localised errors/problems
1194 assert_visb_udpate_def_body(Kind,DefName,A,DefPos),
1195 assert_visb_udpate_def_body(Kind,DefName,B,DefPos).
1196 assert_visb_udpate_def_body(Kind,DefName,TypedExpr,DefPos) :-
1197 get_texpr_type(TypedExpr,Type),
1198 determine_type_of_visb_formula(TypedExpr,_,FormulaClass),
1199 debug_format(19,'Detected ~w: ~w (~w)~n',[Kind,DefName,FormulaClass]),
1200 assertz(visb_special_definition(Kind,DefName,Type,TypedExpr,FormulaClass,DefPos)),
1201 check_visb_update_type(Kind,Type,DefName,unknown_svg_class,DefPos).
1202
1203 % check if we need to add virtual children for an VISB_SVG_UPDATES body:
1204 % (e.g., for title updates to SVG objects coming from an SVG file)
1205 add_children_for_visb_update_def_body(b(couple(A,B),_,_),DefName,JsonFile) :- !,
1206 (add_children_for_visb_update_def_body(A,DefName,JsonFile)
1207 ;
1208 add_children_for_visb_update_def_body(B,DefName,JsonFile)).
1209 add_children_for_visb_update_def_body(b(rec(Fields),_,_),DefName,JsonFile) :-
1210 select(field(id,TParentId),Fields,F2),!,
1211 is_static_expr(TParentId,id,DefName), % we need a static value to create children for it
1212 TParentId = b(_,_,Info),
1213 evaluate_static_visb_formula(TParentId,DefName,'',[],ResValue,Info),
1214 b_value_to_id_string(ResValue,ParentId),
1215 \+ svg_id_exists(ParentId),
1216 (\+ get_default_visb_svg_file(_,_), % cannot call no_svg_file_available yet
1217 JsonFile = '' % No JSON file to be loaded after, which could add SVG file or objects
1218 -> ajoin(['Unknown VISB_SVG_OBJECT with id ',ParentId,' in: '],Msg),
1219 add_warning(visb_visualiser,Msg,DefName,Info)
1220 ; select(field(title,TTitle),F2,_),
1221 (TTitle = b(string(Title),_,_) -> true ; Title = 'no-title-set'),
1222 get_texpr_pos(TTitle,Pos),
1223 add_virtual_title_object(Title,DefName,Pos,TitleID),
1224 assert_visb_svg_child(ParentId,Pos,TitleID),
1225 assert(visb_svg_child_of_object_from_svg_file(TitleID))
1226 ),
1227 fail.
1228 % TODO: set comprehensions like {x•x:Obj|rec(id=("obj",x), title=....)}
1229 % TODO: support sets and warn when ID is not statically known?
1230
1231 % assert VisB events or hovers from B DEFINITION, from part of VISB_SVG_OBJECTS:
1232 % supporting event: attribute and optional predicate attribute
1233 % Kind = visb_events %or visb_hovers
1234 add_visb_events_from_def_body(Kind,DefName,Body,DefPos) :-
1235 get_texpr_type(Body,Type),
1236 \+ empty_update_or_hover_type(Type), % at least one more field than just id field
1237 get_visb_static_svg_object_for_typed_expr(Kind,DefName,Body,DefPos,SVG_ID,AttrList,Desc,InnerPos),
1238 add_visb_object_from_definition(Kind, SVG_ID, AttrList, Desc, DefName, InnerPos),
1239 fail.
1240 add_visb_events_from_def_body(_,_,_,_).
1241
1242 empty_update_or_hover_type(record(Fields)) :- !, Fields \= [_,_|_]. % at least one more field than just id field
1243 empty_update_or_hover_type(set(X)) :- !, empty_update_or_hover_type(X).
1244 empty_update_or_hover_type(couple(A,B)) :- !, empty_update_or_hover_type(A), empty_update_or_hover_type(B).
1245
1246 get_svg_object_updates_from_definitions(ExpandedBState,SVG_ID,SvgAttribute,Value,Pos) :-
1247 ? visb_special_definition(visb_updates,DefName,_Type,BodyTypedExpr,_Class,DefPos),
1248 ? get_visb_DEFINITION_svg_object(visb_updates,DefName,BodyTypedExpr,DefPos,ExpandedBState,SVG_ID,AttrList,_Desc,Pos),
1249 ? member(svg_attribute(SvgAttribute,Value),AttrList).
1250
1251 % check types of VisB updates
1252 check_visb_update_type(Kind,Type,DefName,Class,DefPos) :-
1253 get_update_record_fields_type(Type,Fields),
1254 % other types are STRING +-> STRING, ...; this will be checked in get_visb_DEFINITION_svg_object
1255 (memberchk(field('svg_class',_),Fields)
1256 -> add_warning(visb_visualiser,'VisB updates should not set svg_class:',DefName,DefPos)
1257 ; true),
1258 ? member(field(Name,FieldType),Fields),
1259 (Name = trigger_id ->
1260 (Kind=visb_hovers -> true ;
1261 add_warning(visb_visualiser,'Attribute trigger_id can only be used for hovers:',DefName,DefPos)
1262 )
1263 ; check_attribute_type(FieldType,Name,DefName,Class,DefPos)
1264 ),
1265 fail.
1266 check_visb_update_type(_,_,_,_,_).
1267
1268 % get a fields type list from a type
1269 get_update_record_fields_type(set(X),Fields) :- !,
1270 get_update_record_fields_type(X,Fields).
1271 get_update_record_fields_type(record(Fields),R) :- !, R=Fields.
1272 get_update_record_fields_type(couple(A,B),Fields) :-
1273 (get_update_record_fields_type(A,Fields)
1274 ; get_update_record_fields_type(B,Fields)).
1275
1276 :- use_module(probsrc(translate), [pretty_type/2]).
1277 % check B type of a field for an SVG update or object
1278 check_attribute_type(Type,Name,DefName,Class,DefPos) :- alternative_spelling(Name,AName),!,
1279 check_attribute_type(Type,AName,DefName,Class,DefPos).
1280 check_attribute_type(Type,Name,DefName,Class,DefPos) :- Class \= unknown_svg_class,
1281 check_is_number_attribute(Name,Class,DefPos),!,
1282 illegal_number_type(Type),
1283 ajoin(['Type of field ',Name,' of ', DefName, ' is not a number: '],Msg),
1284 pretty_type(Type,TS),
1285 add_warning(visb_visualiser,Msg,TS,DefPos).
1286 check_attribute_type(Type,Name,DefName,_,DefPos) :-
1287 is_svg_color_attribute(Name),!,
1288 illegal_col_type(Type),
1289 ajoin(['Type of field ',Name,' of ', DefName, ' is not a color: '],Msg),
1290 pretty_type(Type,TS),
1291 add_warning(visb_visualiser,Msg,TS,DefPos).
1292 check_attribute_type(_Type,Name,_DefName,Class,DefPos) :-
1293 check_attribute_name_is_supported(Class,Name,DefPos).
1294
1295 illegal_nr_or_col_type(boolean).
1296 illegal_nr_or_col_type(set(_)).
1297 illegal_nr_or_col_type(seq(_)).
1298 illegal_nr_or_col_type(record(_)).
1299 illegal_nr_or_col_type(couple(A,B)) :- (illegal_nr_or_col_type(A) -> true ; illegal_nr_or_col_type(B)).
1300 % check if couple types can work by concatenating string representations
1301
1302 illegal_col_type(X) :- illegal_nr_or_col_type(X),!.
1303 illegal_col_type(real).
1304 % integer ? or can we map integers to colours using a color scheme like in DOT?
1305
1306 illegal_number_type(X) :- illegal_nr_or_col_type(X),!.
1307 %illegal_number_type(global(_)). % what if we use a global set with weird constants using back-quotes ?
1308
1309 % ----------------
1310
1311 % parse and load an individual JSON VisB item, e.g, :
1312 % { "name":"xscale",
1313 % "value" : "(100.0 / real(TrackElementNumber))"
1314 % }
1315
1316 process_json_definition(File,json(List)) :-
1317 (get_attr_true(ignore,List,File) -> true % ignore this definition
1318 ; process_json_def_lst(File,List)).
1319
1320 :- use_module(probsrc(bsyntaxtree), [get_texpr_type/2]).
1321 process_json_def_lst(File,List) :-
1322 force_del_attr_with_pos(name,List,string(ID),L1,File,NamePos),
1323 force_del_attr_with_pos(value,L1,string(Formula),L2,File,VPos),
1324 debug_format(19,' Processing definition for ~w with value-formula (lines ~w):~w~n',[ID,VPos,Formula]),
1325 !,
1326 set_gen_parse_errors(L2,VPos,GenParseErrors), % treat optional attribute
1327 process_json_definition(ID,NamePos,Formula,VPos,GenParseErrors).
1328 process_json_def_lst(File,List) :- get_pos_from_list(List,File,Pos),
1329 add_error(visb_visualiser,'Illegal VisB Definition:',List,Pos).
1330
1331 % we could also load a classical B Definition file and process its definitions like this:
1332 process_json_definition(ID,NamePos,Formula,VPos,GenParseErrors) :-
1333 atom_codes(Formula,FCodes),
1334 set_error_context(visb_error_context(definition,ID,'value',VPos)),
1335 (b_get_definition_name_with_pos(ID,_Arity,_DefType,_DPos)
1336 -> add_warning(visb_visualiser,'Ignoring VisB definition, DEFINITION of the same name already exists:',ID,NamePos)
1337 ; parse_expr(FCodes,TypedExpr,GenParseErrors)
1338 -> add_visb_json_definition(ID,TypedExpr,VPos)
1339 ; GenParseErrors=false -> formatsilent('Ignoring optional VisB definition for ~w due to error in B formula~n',[ID])
1340 ; add_error(visb_visualiser,'Cannot parse or typecheck VisB formula for definition',ID,VPos)
1341 ),
1342 clear_error_context.
1343
1344 add_visb_json_definition(ID,TypedExpr,VPos) :-
1345 get_texpr_type(TypedExpr,Type),
1346 determine_type_of_visb_formula(TypedExpr,TIds,Class), %write(type(ID,Class,TIds)),nl,
1347 (try_eval_static_def(Class,'static definition', ID,TypedExpr,TIds,StaticValue,VPos)
1348 -> get_texpr_type(TypedExpr,Type),StaticValueExpr = b(value(StaticValue),Type,[]),
1349 assert_visb_json_definition(ID,Type,StaticValueExpr,TIds,Class,VPos)
1350 ; assert_visb_json_definition(ID,Type,TypedExpr,TIds,Class,VPos)
1351 ).
1352
1353 % assert a VisB definition stemming from the JSON definitions section:
1354 assert_visb_json_definition(DefName,Type,TypedExpr,UsedTIds,Class,DefPos) :-
1355 ? (is_special_visb_def_name(DefName,SpecialClass) -> true ; SpecialClass = regular_def),
1356 assertz(visb_definition(DefName,Type,TypedExpr,Class,DefPos,SpecialClass)),
1357 (SpecialClass \= regular_def
1358 -> formatsilent('Detected special ~w definition ~w (~w)~n',[SpecialClass,DefName,Class]),
1359 add_special_json_definition(SpecialClass,DefName,Type,TypedExpr,UsedTIds,Class,DefPos)
1360 ; true
1361 ).
1362
1363 % register some special definitions, in which a set of objects/hovers/updates can be specified
1364 % by a single definition returning a set of records
1365 add_special_json_definition(visb_updates,DefName,Type,TypedExpr,_,Class,DefPos) :- !,
1366 check_visb_update_type(visb_updates,Type,DefName,Class,DefPos),
1367 assertz(visb_special_definition(visb_updates,DefName,Type,TypedExpr,Class,DefPos)). % will be evaluated later
1368 add_special_json_definition(visb_contents,DefName,Type,TypedExpr,_,Class,DefPos) :- !,
1369 assertz(visb_special_definition(visb_contents,DefName,Type,TypedExpr,Class,DefPos)).
1370 add_special_json_definition(visb_box,DefName,Type,TypedExpr,_,Class,DefPos) :- !,
1371 assertz(visb_special_definition(visb_box,DefName,Type,TypedExpr,Class,DefPos)).
1372 add_special_json_definition(visb_objects,DefName,_Type,TypedExpr,_UsedTIds,_Class,DefPos) :- !,
1373 AllowSep=allow_separation, % TODO: we re-determine the class and used ids below:
1374 get_typed_static_definition_with_constants_state(DefName,TypedExpr,ResBody,DefPos,CS,no_inlining,AllowSep),
1375 (get_visb_DEFINITION_svg_object(visb_objects,DefName,ResBody,DefPos,CS,SVG_ID,AttrList,Desc,InnerPos),
1376 %formatsilent('Adding ~w : ~w (from ~w)~n',[visb_objects,SVG_ID,DefName]),
1377 add_visb_object_from_definition(visb_objects, SVG_ID, AttrList, Desc, DefName, InnerPos),
1378 fail ; true).
1379 add_special_json_definition(SpecialClass,DefName,_Type,TypedExpr,UsedTIds,Class,DefPos) :-
1380 (get_unique_initial_state_for_visb(Class,DefName,DefPos,UsedTIds,ConstantsState) -> true
1381 ; ConstantsState=[]),
1382 get_static_visb_state(ConstantsState,FullState), % add static VisB Defs
1383 (Class=requires_variables,
1384 (get_preference(visb_allow_variables_for_objects,false) ; ConstantsState=[])
1385 -> add_warning(visb_visualiser,'Ignoring VisB definition which requires variables:',DefName,DefPos)
1386 ; get_visb_DEFINITION_svg_object(SpecialClass,DefName,TypedExpr,DefPos,FullState,SVG_ID,AttrList,Desc,InnerPos),
1387 %formatsilent('Adding ~w : ~w (from ~w)~n',[SpecialClass,SVG_ID,DefName]),
1388 add_visb_object_from_definition(SpecialClass, SVG_ID, AttrList, Desc, DefName, InnerPos)
1389 ; true).
1390
1391 is_special_visb_def_name(DefName,visb_updates) :- atom_concat('VISB_SVG_UPDATES',_,DefName).
1392 is_special_visb_def_name(DefName,visb_hovers) :- atom_concat('VISB_SVG_HOVERS',_,DefName).
1393 is_special_visb_def_name(DefName,visb_objects) :- atom_concat('VISB_SVG_OBJECTS',_,DefName).
1394 is_special_visb_def_name(DefName,visb_contents) :- atom_concat('VISB_SVG_CONTENTS',_,DefName).
1395 is_special_visb_def_name(DefName,visb_events) :- atom_concat('VISB_SVG_EVENTS',_,DefName).
1396 is_special_visb_def_name('VISB_SVG_BOX',visb_box).
1397 % TODO: maybe provide VISB_HTML_CONTENTS which appear after the SVG
1398
1399 % evaluate static VisB defs only once or evaluate expressions in svg_objects and loop bounds
1400 eval_static_def(Class,VisBKind,ID,TypedExpr,UsedTIds,StaticValue,VPos) :-
1401 get_unique_initial_state_for_visb(Class,ID,VPos,UsedTIds,ConstantsState),
1402 evaluate_static_visb_formula(TypedExpr,VisBKind,ID,ConstantsState,StaticValue,VPos).
1403
1404 % only evaluate statically if possible; no warnings/messages if not possible (just fail)
1405 try_eval_static_def(requires_variables,_VisBKind,_ID,_TypedExpr,_UsedTIds,_StaticValue,_VPos) :- !,
1406 fail. % do not try to evaluate statically; events will change the variable values anyway
1407 try_eval_static_def(Class,VisBKind,ID,TypedExpr,UsedTIds,StaticValue,VPos) :-
1408 % TODO: disable messages for multiple constants values; just fail
1409 eval_static_def(Class,VisBKind,ID,TypedExpr,UsedTIds,StaticValue,VPos).
1410
1411 % check if a unique constant value exists for a model
1412 get_unique_initial_state_for_visb(requires_nothing,_,_,_,State) :- !, State=[].
1413 get_unique_initial_state_for_visb(Class,DefName,DefPos,_,State) :-
1414 \+ multiple_concrete_constants_exist,
1415 is_concrete_constants_state_id(StateID),!,
1416 (Class=requires_variables
1417 -> get_preference(visb_allow_variables_for_objects,true),
1418 unique_initialisation_id_exists_from(StateID,DefName,DefPos,State)
1419 % Note: variable can still be modified by other events later, e.g., in ProB2-UI
1420 ; visited_expression(StateID,StateTerm),
1421 state_corresponds_to_set_up_constants_only(StateTerm,State)).
1422 get_unique_initial_state_for_visb(requires_constants,DefName,DefPos,Ids,State) :- Ids \= all,
1423 % try and see if all values for Ids are the same; TODO: also support requires_variables
1424 is_concrete_constants_state_id(StateID),!,
1425 visited_expression(StateID,StateTerm),
1426 state_corresponds_to_set_up_constants_only(StateTerm,State),
1427 (member(C,Ids), get_texpr_id(C,CstID),
1428 other_constant_value_exists_for(CstID,State,StateID)
1429 -> ajoin(['Multiple values for constant ',CstID, ' in context of: '],Msg),
1430 add_message(visb_visualiser,Msg,DefName,DefPos),fail
1431 ; true).
1432
1433 get_a_constants_state(State,StateID,inline_objects(SingleStateId)) :-
1434 get_constants_state_id_for_id(SingleStateId,StateID),!,
1435 visited_expression(StateID,StateTerm),
1436 state_corresponds_to_set_up_constants_only(StateTerm,State).
1437 get_a_constants_state(State,StateID,InlineObjects) :-
1438 check_inlining(InlineObjects),
1439 is_concrete_constants_state_id(StateID),!,
1440 visited_expression(StateID,StateTerm),
1441 state_corresponds_to_set_up_constants_only(StateTerm,State).
1442
1443 check_inlining(no_inlining) :- !.
1444 check_inlining(inline_objects(_SingleStateId)) :- !.
1445 check_inlining(X) :- add_internal_error('Invalid inlining value:',check_inlining(X)).
1446
1447 :- use_module(probsrc(store), [lookup_value_for_existing_id/3]).
1448 other_constant_value_exists_for(CstID,State,StateId) :-
1449 lookup_value_for_existing_id(CstID,State,Val1),
1450 is_concrete_constants_state_id(StateId2), StateId2 \= StateId,
1451 visited_expression(StateId2,StateTerm2),
1452 state_corresponds_to_set_up_constants_only(StateTerm2,State2),
1453 lookup_value_for_existing_id(CstID,State2,Val2),
1454 Val2 \= Val1.
1455
1456
1457 unique_initialisation_id_exists_from(FromStateId,DefName,DefPos,State) :-
1458 transition(FromStateId,_,StateID),!,
1459 (transition(FromStateId,_,StateID2),
1460 StateID2 \= StateID
1461 -> ajoin(['Multiple initialisations exists (state ids ',StateID,',',StateID2,') for: '],Msg),
1462 add_message(visb_visualiser,Msg,DefName,DefPos),fail
1463 ; true),
1464 visited_expression(StateID,StateTerm),
1465 state_corresponds_to_initialised_b_machine(StateTerm,State).
1466
1467 parse_expr_for_visb(Formula,JsonList,Pos,TypedExpr) :-
1468 set_gen_parse_errors(JsonList,Pos,GenParseErrors),
1469 parse_expr(Formula,TypedExpr,GenParseErrors).
1470
1471 set_gen_parse_errors(JSonList,Pos,GenParseErrors) :-
1472 (get_attr(optional,JSonList,_)
1473 -> GenParseErrors=false
1474 ; %get_pos_from_list(JSonList,File,Position),
1475 GenParseErrors=gen_parse_errors_for(Pos)).
1476
1477 % ----------------
1478
1479 % parse and load an individual JSON SVG object listed under svg_objects, e.g, :
1480 % {
1481 % "svg_class":"rect",
1482 % "id":"train_rect",
1483 % "x":"0",
1484 % "y":"0",
1485 % "comment":"..."
1486 % },
1487 process_json_svg_object(File,Json) :-
1488 process_repeat(0,Json,File,add_visb_json_svg_object).
1489
1490 add_visb_json_svg_object(File,json(List)) :- get_attr_true(ignore,List,File), !. % ignore this item
1491 add_visb_json_svg_object(File,json(List)) :-
1492 (force_del_attr_with_pos(svg_class,List,string(SVG_Class),L1,File,Pos1) -> true % shape: line, rect, ...
1493 ; infer_svg_class(List,SVG_Class,File,Pos1)
1494 -> add_message(visb_visualiser,'Inferred svg_class: ',SVG_Class,Pos1),L1=List),
1495 force_del_attr(id,L1,string(ID),L2,File),
1496 (del_attr(comment,L2,string(Desc),JsonList3) -> true ; Desc = '', JsonList3=L2),
1497 debug_format(19,' Creating new SVG object ~w with id:~w~n',[SVG_Class,ID]),
1498 add_debug_message(visb_visualiser,'New object: ',ID,Pos1),
1499 % TODO: we could pre-process all attributes not depending on %0, %1, ...
1500 maplist(get_svg_attr(SVG_Class,File),JsonList3,AttrList),
1501 %formatsilent('Adding SVG Object ~w with ID ~w (~w): ~w~n',[SVG_Class,ID,Desc,AttrList]),
1502 assert_visb_svg_object(ID,SVG_Class,AttrList,Desc,'JSON',Pos1),
1503 !.
1504 add_visb_json_svg_object(File,Json) :-
1505 !,
1506 get_pos_from_list(Json,File,Pos),
1507 add_error(visb_visualiser,'Illegal VisB additional SVG object:',Json,Pos).
1508
1509 infer_svg_class(List,line,File,Pos) :- get_attr_with_pos(x1,List,_,File,Pos),!.
1510 infer_svg_class(List,circle,File,Pos) :- get_attr_with_pos(r,List,_,File,Pos),!.
1511 infer_svg_class(List,rect,File,Pos) :- get_attr_with_pos(height,List,_,File,Pos),!.
1512 infer_svg_class(List,rect,File,Pos) :- get_attr_with_pos(width,List,_,File,Pos),!.
1513 infer_svg_class(List,ellipse,File,Pos) :- get_attr_with_pos(rx,List,_,File,Pos),!. % could also be rect
1514 infer_svg_class(List,text,File,Pos) :- get_attr_with_pos(text,List,_,File,Pos),!.
1515 infer_svg_class(List,g,File,Pos) :- get_attr_with_pos(children,List,_,File,Pos),!. % group + foreignObject have children
1516 infer_svg_class(List,use,File,Pos) :- get_attr_with_pos(href,List,_,File,Pos),!. % href can also be used with image, pattern, ...
1517
1518 % assert a new SVG object to be created upon SETUP_CONSTANTS/INITIALISATION:
1519 assert_visb_svg_object(ID,SVG_Class,_AttrList,_Desc,DefName,Pos1) :-
1520 visb_svg_object(ID,_,_,_,_Pos0),!,
1521 ajoin(['SVG object (from ',DefName,', svg_class=',SVG_Class,') with same id already created: '],Msg),
1522 add_warning(visb_visualiser,Msg,ID,Pos1).
1523 assert_visb_svg_object(_ID,_SVG_Class,AttrList,_Desc,_DefName,Pos1) :-
1524 \+ (AttrList=[] ; AttrList=[_|_]),!,
1525 add_error(visb_visualiser,'SVG objects attributes are not a list:',AttrList,Pos1).
1526 assert_visb_svg_object(ID,SVG_Class,AttrList,Desc,DefName,Pos1) :-
1527 check_svg_shape_class(ID,SVG_Class,Pos1),
1528 add_visb_debug_infos(ID,SVG_Class,AttrList,AttrList2,DefName,Pos1),
1529 sort(AttrList2,SAttrList),
1530 get_all_children(SAttrList,Children,RestAttrs,DefName,Pos1),
1531 (Children = [] -> true
1532 ? ; svg_shape_can_have_children(SVG_Class) -> true % g, foreignObject, HTML tags
1533 ; Children = [C1_ID|_], visb_svg_object(C1_ID,CAttr,_,_,_),
1534 attribute_automatically_creates_children(CAttr) % e.g., title object created for title attribute of ID
1535 -> true
1536 ; add_message(visb_visualiser,'Children attribute only useful for certain SVG classes such as groups (g) or foreignObject or when adding title objects (as tooltips): ',Children,Pos1)
1537 ),
1538 ? (select(svg_attribute(group_id,ParentGroupId),RestAttrs,RestAttrs2)
1539 -> assert_visb_svg_child(ParentGroupId,Pos1,ID) % register parent group id
1540 ; RestAttrs2=RestAttrs),
1541 compute_auto_attributes(RestAttrs,RestAttrs2,SVG_Class,NewRestAttrs),
1542 assertz(visb_svg_object(ID,SVG_Class,NewRestAttrs,Desc,Pos1)),
1543 maplist(assert_visb_svg_child(ID,Pos1),Children). % add all children
1544
1545 % adapt visb_svg_object to provide developer debug infos, e.g., in title hover messages
1546 add_visb_debug_infos(ID,SVG_Class,AttrList,NewAttrList,DefName,Pos) :- SVG_Class \= title,
1547 get_preference(visb_show_debug_infos,true),
1548 (select(svg_attribute(title,Title),AttrList,RestAttrs) -> true
1549 ; Title='', RestAttrs=AttrList),
1550 !,
1551 extract_span_description_with_opts(Pos,PosStr,
1552 [relative_file_name,compact_pos_info,
1553 inner_context_separator('\n in ','\n at ')]),
1554 %extract_definition_call_stack_desc(Pos,CS), already displayed in inner context
1555 ajoin(['-- VISB_DEBUG_INFO --\nid=',ID, '\nsvg_class=',SVG_Class, '\nsrc=',DefName,'\n', PosStr],DebugInfo),
1556 (Title='' -> NewTitle=DebugInfo ; ajoin([Title,'\n',DebugInfo],NewTitle)),
1557 %format('~nDEBUG::~n~w~n~w~n---~n',[ID,DebugInfo]),
1558 assert(visb_svg_object_debug_info(ID,DebugInfo)),
1559 NewAttrList = [svg_attribute(title,NewTitle)|RestAttrs].
1560 add_visb_debug_infos(_,_,AttrList,AttrList,_,_).
1561
1562 % compute the value of VisB auto attributes, e.g., automatically
1563 % doing a layout of objects in a grid
1564 % TODO: SVG/special_svg_number already supports auto but not for x,y coordinates?
1565 % TODO: try and determine width of object automatically; keep track of auto objects max height per row
1566 % TODO: support cx,cy
1567 compute_auto_attributes([],_,_,[]).
1568 compute_auto_attributes([svg_attribute(Attr,Val)|T],AllAttrs,SVG_Class,
1569 [svg_attribute(Attr,NewVal)|NT]) :-
1570 (Val=auto, compute_auto_attribute(Attr,AllAttrs,SVG_Class,NewVal)
1571 -> true
1572 ; NewVal=Val),
1573 compute_auto_attributes(T,AllAttrs,SVG_Class,NT).
1574
1575 :- dynamic next_auto_x/1, next_auto_y/2.
1576 next_auto_x(0).
1577 next_auto_y(0,10).
1578 reset_auto_attrs :- retractall(next_auto_x(_)),
1579 retractall(next_auto_y(_,_)),
1580 assertz(next_auto_x(0)),
1581 assertz(next_auto_y(0,10)).
1582
1583 get_x_auto_limit(Limit) :- visb_empty_svg_box_height_width(_H,W,_ViewBox),!,
1584 Limit = W. %TODO: inspect viewBox
1585 get_x_auto_limit(400).
1586
1587 compute_auto_attribute(id,_,_,GenID) :- !, gensym(svg_id,GenID).
1588 compute_auto_attribute(Attr,AllAttrs,SVG_Class,Val) :-
1589 auto_compute_x_coordinate(Attr,Kind),!,
1590 retract(next_auto_x(XV)),
1591 (get_width(SVG_Class,AllAttrs,Offset) -> true ; Offset=10),
1592 Padding = 2, % TODO: make customisable
1593 NewXV is XV+Offset+Padding,
1594 get_x_auto_limit(Lim),
1595 (NewXV > Lim
1596 -> NewVal=0, retract(next_auto_y(OldY,YOffset)),
1597 (get_height(SVG_Class,AllAttrs,Offset) -> true ; Offset = 10),
1598 NewY is OldY+YOffset,
1599 assert(next_auto_y(NewY,YOffset))
1600 ; NewVal=NewXV),
1601 assertz(next_auto_x(NewVal)),
1602 (Kind=left -> Val=XV ; Val is XV + Offset/2).
1603 compute_auto_attribute(Attr,AllAttrs,SVG_Class,Val) :- auto_compute_y_coordinate(Attr,Kind),
1604 next_auto_y(YV,_),
1605 (Kind = top -> Val = YV
1606 ; get_height(SVG_Class,AllAttrs,Height) -> Val is YV + Height/2
1607 ; Val is YV+5).
1608
1609 auto_compute_x_coordinate(x,left). % rect, ..
1610 auto_compute_x_coordinate(cx,center). % circle, ellipse
1611 auto_compute_y_coordinate(y,top). % rect, ..
1612 auto_compute_y_coordinate(cy,center). % circle, ellipse
1613
1614 get_width(rect,Attrs,Wid) :- member(svg_attribute(width,Wid),Attrs).
1615 get_width(circle,Attrs,Wid) :- member(svg_attribute(r,Radius),Attrs), Wid is 2*Radius.
1616 get_width(ellipse,Attrs,Wid) :- member(svg_attribute(rx,Radius),Attrs), Wid is 2*Radius.
1617 get_width(line,Attrs,Wid) :- member(svg_attribute(x1,X1),Attrs),
1618 member(svg_attribute(x2,X2),Attrs), Wid is abs(X2-X1).
1619
1620 get_height(rect,Attrs,Wid) :- member(svg_attribute(height,Wid),Attrs).
1621 get_height(circle,Attrs,Wid) :- member(svg_attribute(r,Radius),Attrs), Wid is 2*Radius.
1622 get_height(ellipse,Attrs,Wid) :- member(svg_attribute(ry,Radius),Attrs), Wid is 2*Radius.
1623 get_height(line,Attrs,Wid) :- member(svg_attribute(y1,X1),Attrs),
1624 member(svg_attribute(y2,X2),Attrs), Wid is abs(X2-X1).
1625
1626
1627 % register an SVG ID as child of a group
1628 assert_visb_svg_child(_ParentId,Pos,ChildID) :- visb_svg_child(ChildID,OldParent),!,
1629 ajoin(['SVG object already child of group ',OldParent,': '],Msg),
1630 add_warning(visb_visualiser,Msg,ChildID,Pos).
1631 assert_visb_svg_child(ParentId,Pos,ChildID) :- visb_svg_child(ParentId,ChildID),!, % TODO: full cycle detection
1632 ajoin(['SVG object already parent of group ',ParentId,' (cycle): '],Msg),
1633 add_warning(visb_visualiser,Msg,ChildID,Pos).
1634 assert_visb_svg_child(ParentId,_Pos,ChildID) :-
1635 assertz(visb_svg_child(ChildID,ParentId)),
1636 assertz(visb_svg_parent(ParentId,ChildID)).
1637
1638
1639
1640
1641 :- use_module(probsrc(gensym),[gensym/2]).
1642 % we need to translate a title attribute to a separate title object and add it as a child
1643 % see also post_process_visb_item which dispatches title updates to the child object
1644 get_all_children(SAttrList,Children,Rest,DefName,Pos) :-
1645 ? select(svg_attribute(title,Title),SAttrList,SList2),!,
1646 add_virtual_title_object(Title,DefName,Pos,TitleID),
1647 Children=[TitleID|TChilds],
1648 get_children_attribute(SList2,TChilds,Rest,Pos).
1649 get_all_children(SAttrList,Children,Rest,_,Pos) :-
1650 % get the children explicitly defined by the user:
1651 get_children_attribute(SAttrList,Children,Rest,Pos).
1652
1653 add_virtual_title_object(Title,DefName,Pos,TitleID) :-
1654 gensym(visb_title,TitleID),
1655 assert_visb_svg_object(TitleID,'title',[svg_attribute(text,Title)],'',DefName,Pos),
1656 add_debug_message(visb_visualiser,'Adding virtual title child object: ',TitleID,Pos).
1657
1658 get_children_attribute(SAttrList,Children,Rest,Pos) :-
1659 ? select(svg_attribute(children,C),SAttrList,R),!,
1660 (is_list(C) -> Children=C
1661 ; add_warning(visb_visualiser,'Children attribute should be a list (of SVG ids): ',C,Pos),
1662 Children=[]),
1663 Rest=R.
1664 get_children_attribute(SAttrList,[],SAttrList,_).
1665
1666
1667
1668 :- use_module(probsrc(tools_matching), [get_possible_fuzzy_matches_and_completions_msg/3,
1669 get_all_svg_classes/1, is_svg_shape_class/1,
1670 is_html_tag/1, is_html_attribute/1]).
1671
1672
1673 svg_shape_can_have_children(defs).
1674 svg_shape_can_have_children(foreignObject).
1675 svg_shape_can_have_children(g).
1676 svg_shape_can_have_children(pattern).
1677 svg_shape_can_have_children(X) :- is_html_tag(X).
1678
1679
1680 :- use_module(probsrc(tools_matching), [dotshape2svg_class/2]).
1681 % check whether svg_class value seems valid
1682 check_svg_shape_class(ID,Shape,Pos) :-
1683 (is_svg_shape_class(Shape) -> true
1684 ; is_html_tag(Shape) ->
1685 (visb_svg_child(ID,ParentId),
1686 visb_svg_object(ParentId,ParClass,_,_,_),
1687 (is_html_tag(ParClass) -> true ; ParClass=foreignObject)
1688 -> add_debug_message(visb_visualiser,'HTML tag used as svg_class in foreignObject child: ',Shape,Pos)
1689 ; ajoin(['SVG object ', ID, ' has HTML tag as svg_class (and should probably be a child of a foreignObject): '],Msg),
1690 add_message(visb_visualiser,Msg,Shape,Pos) % probably should be child of foreignObject
1691 )
1692 ; dotshape2svg_class(Shape,Class)
1693 -> ajoin(['SVG object ', ID, ' has unknown svg_class (did you mean ',Class,' ?): '],Msg),
1694 add_warning(visb_visualiser,Msg,Shape,Pos)
1695 ; get_all_svg_classes(Classes),
1696 get_possible_fuzzy_matches_and_completions_msg(Shape,Classes,FMsg)
1697 -> ajoin(['SVG object ', ID, ' has unknown svg_class (did you mean ',FMsg,' ?): '],Msg),
1698 add_warning(visb_visualiser,Msg,Shape,Pos)
1699 ; ajoin(['SVG object ', ID, ' has unknown svg_class: '],Msg),
1700 add_message(visb_visualiser,Msg,Shape,Pos)
1701 ).
1702
1703 % get SVG attribute for an svg_object:
1704 get_svg_attr(SVG_Class,File,'='(Attr,AttrVal,Pos),svg_attribute(Attr,Val)) :- !,
1705 construct_prob_pos_term(Pos,File,PosTerm),
1706 get_svg_static_attribute_value(Attr,SVG_Class,PosTerm,AttrVal,Val).
1707 get_svg_attr(_,File,Json,_) :-
1708 get_pos_from_list([Json],File,Position),
1709 add_error(visb_visualiser,'Illegal SVG object attribute',Json,Position),fail.
1710
1711 get_svg_static_attribute_value(Attr,SVG_Class,Pos,AttrVal,Nr) :-
1712 check_is_number_attribute(Attr,SVG_Class,Pos),
1713 \+ is_special_svg_number_form(AttrVal),
1714 !,
1715 (get_number_value(AttrVal,Nr,Attr,Pos) -> true
1716 ; add_error(visb_visualiser,'Illegal number value:',AttrVal,Pos), Nr=0).
1717 get_svg_static_attribute_value(_,_,_,string(Val),Res) :- !, Res=Val.
1718 % for children we get something like array([string(button1_1),string(button1_2)])
1719 get_svg_static_attribute_value(Attr,SVG_Class,Pos,array(List),ResList) :- !,
1720 maplist(get_svg_static_attribute_value(Attr,SVG_Class,Pos),List,ResList).
1721 get_svg_static_attribute_value(_Attr,_,Pos,Val,Val) :-
1722 add_warning(visb_visualiser,'Illegal SVG object attribute value: ',Val,Pos).
1723
1724
1725 % detect special SVG number forms, like 50%
1726 is_special_svg_number_form(string(Atom)) :-
1727 atom_codes(Atom,Codes),
1728 special_svg_number(Codes,[]).
1729
1730 :- use_module(probsrc(self_check)).
1731 :- assert_must_succeed(visb_visualiser:special_svg_number("10%",[])).
1732 :- assert_must_succeed(visb_visualiser:special_svg_number("10 %",[])).
1733 :- assert_must_succeed(visb_visualiser:special_svg_number(" 99em ",[])).
1734 :- assert_must_succeed(visb_visualiser:special_svg_number("1.0em",[])).
1735 :- assert_must_fail(visb_visualiser:special_svg_number("10",[])).
1736 :- assert_must_fail(visb_visualiser:special_svg_number("10+nrcols+%0",[])).
1737 special_svg_number --> " ",!, special_svg_number.
1738 special_svg_number --> [X], {digit(X)},!, special_svg_number2.
1739 special_svg_number --> "auto".
1740 special_svg_number2 --> [X], {digit(X)},!, special_svg_number2.
1741 special_svg_number2 --> ".",!, special_svg_number2. % TODO: only allow one dot; + accept e notation?
1742 special_svg_number2 --> optws,!, svg_unit,!, optws.
1743
1744 % using info from https://oreillymedia.github.io/Using_SVG/guide/units.html
1745 svg_unit --> "%".
1746 svg_unit --> "ch".
1747 svg_unit --> "cm".
1748 svg_unit --> "em".
1749 svg_unit --> "ex".
1750 svg_unit --> "in".
1751 svg_unit --> "mm".
1752 svg_unit --> "pc".
1753 svg_unit --> "pt".
1754 svg_unit --> "px".
1755 svg_unit --> "deg". % angle units
1756 svg_unit --> "grad".
1757 svg_unit --> "rad".
1758 svg_unit --> "turn".
1759 svg_unit --> "rem". % root em
1760 svg_unit --> "vh". % viewport height unit (1%)
1761 svg_unit --> "vw". % viewport width unit (1%)
1762 svg_unit --> "vmin". % min ov vh, vw
1763 svg_unit --> "vmax". % max ov vh, vw
1764
1765
1766 optws --> " ",!,optws.
1767 optws --> [].
1768
1769 digit(X) :- X >= 48, X =< 57.
1770
1771 is_svg_number_attribute(Attr) :- is_svg_number_attribute(Attr,_).
1772
1773
1774 :- use_module(probsrc(tools_matching), [dot2svg_attribute/2, is_dot_attribute/1]).
1775 % some checks to see whether the attribute is supported by the given SVG class
1776
1777 check_attribute_is_supported(SVG_Class,DefPos,svg_attribute(Name,_V)) :- !,
1778 (nonvar(SVG_Class), check_is_number_attribute(Name,SVG_Class,DefPos) -> true
1779 % TODO: check color and other attributes, see also check_attribute_type
1780 ; check_attribute_name_is_supported(SVG_Class,Name,DefPos)).
1781 check_attribute_is_supported(S,DefPos,F) :-
1782 add_internal_error('Illegal call:',check_attribute_is_supported(S,DefPos,F)).
1783
1784 % if these special attributes occur here, something went wrong, e.g.,
1785 % when separating static/dynamic parts
1786 check_unsupported_special_visb_attribute(visb_objects,_,_) :- !,fail. % here we can process everything
1787 check_unsupported_special_visb_attribute(SpecialClass,DefPos,svg_attribute(Name,_)) :-
1788 special_visb_attribute_not_allowed_in_dynamic_objects(Name,SpecialClass,Kind),
1789 ajoin(['The VisB special attribute ',Name,' cannot be used here (',SpecialClass,' use separate ',Kind,' definition): '],Msg),
1790 add_warning(visb_visualiser,Msg,Name,DefPos).
1791
1792 special_visb_attribute_not_allowed_in_dynamic_objects(hover,SC,'VISB_SVG_HOVERS') :- SC \= visb_hovers.
1793 special_visb_attribute_not_allowed_in_dynamic_objects(hovers,SC,'VISB_SVG_HOVERS') :- SC \= visb_hovers.
1794 special_visb_attribute_not_allowed_in_dynamic_objects(event,SC,'VISB_SVG_EVENTS') :- SC \= visb_events.
1795 special_visb_attribute_not_allowed_in_dynamic_objects(events,SC,'VISB_SVG_EVENTS') :- SC \= visb_events.
1796 special_visb_attribute_not_allowed_in_dynamic_objects(predicate,SC,'VISB_SVG_EVENTS') :- SC \= visb_events.
1797 special_visb_attribute_not_allowed_in_dynamic_objects(predicates,SC,'VISB_SVG_EVENTS') :- SC \= visb_events.
1798 special_visb_attribute_not_allowed_in_dynamic_objects(preds,SC,'VISB_SVG_EVENTS') :- SC \= visb_events.
1799
1800
1801 check_attribute_name_is_supported(SVG_Class,Name,DefPos) :-
1802 nonvar(SVG_Class),
1803 is_html_tag(SVG_Class),
1804 \+ is_svg_shape_class(SVG_Class), % script and title can be both SVG and HTML
1805 !,
1806 (is_html_attribute(Name)
1807 -> true % TODO: we could check whether attribute appropriate for Tag
1808 ; is_virtual_svg_attribute(Name) -> true % Virtual VisB attribute like children, text, ...
1809 ; ajoin(['Unknown HTML attribute used inside HTML tag ',SVG_Class,': '],Msg),
1810 add_message(visb_visualiser,Msg,Name,DefPos)
1811 ).
1812 check_attribute_name_is_supported(_SVG_Class,Name,DefPos) :-
1813 ? \+ is_svg_attribute(Name),
1814 !,
1815 (dot2svg_attribute(Name,GraphVizTranslName)
1816 -> ajoin(['Unknown SVG attribute (maybe you want to use ',GraphVizTranslName,' ?): '],Msg),
1817 add_warning(visb_visualiser,Msg,Name,DefPos)
1818 ; get_all_svg_attributes(Attrs),
1819 (get_possible_fuzzy_matches_and_completions_msg(Name,Attrs,FMsg)
1820 -> ajoin(['Unknown SVG attribute (did you mean ',FMsg,' ?): '],Msg),
1821 add_warning(visb_visualiser,Msg,Name,DefPos) % create warning, as it is likely we have made an error
1822 ; is_dot_attribute(Name)
1823 -> add_warning(visb_visualiser,'This Dot/Graphviz attribute is not a valid SVG attribute: ',Name,DefPos)
1824 ; add_message(visb_visualiser,'Unknown SVG attribute: ',Name,DefPos)
1825 )
1826 ).
1827 check_attribute_name_is_supported(_,_,_).
1828
1829 % succeed if attribute is a number attribute and perform a check the attribute is supported by the class
1830 check_is_number_attribute(Attr,Class,Pos) :-
1831 is_svg_number_attribute(Attr,ClassList),
1832 (nonvar(Class), nonmember(Class,ClassList)
1833 -> (equivalent_attribute(Attr,List2,NewAttr), member(Class,List2)
1834 -> ajoin(['The number attribute ',Attr,' is not supported for SVG class ',Class,', use: '],Msg),
1835 add_warning(visb_visualiser,Msg,NewAttr,Pos)
1836 ; ajoin(['The number attribute ',Attr,' is not supported for this SVG class: '],Msg),
1837 add_warning(visb_visualiser,Msg,Class,Pos)
1838 )
1839 ; true
1840 ).
1841
1842 % optionally rewrite record field to alternative spelling
1843 opt_rewrite_field_name(Name,Res) :-
1844 (alternative_spelling(Name,Alt) -> Res=Alt ; Res=Name).
1845
1846 % these alternatives are useful e.g. in TLA+ without backquote:
1847 alternative_spelling(colour,'color').
1848 alternative_spelling(fill_opacity,'fill-opacity').
1849 alternative_spelling(fill_rule,'fill-rule').
1850 alternative_spelling(font_family,'font-family').
1851 alternative_spelling(font_size,'font-size').
1852 alternative_spelling(font_style,'font-style').
1853 alternative_spelling(font_variant,'font-variant').
1854 alternative_spelling(font_weight,'font-weight').
1855 alternative_spelling(marker_end,'marker-end').
1856 alternative_spelling(marker_start,'marker-start').
1857 alternative_spelling(stroke_opacity,'stroke-opacity').
1858 alternative_spelling(stroke_dasharray,'stroke-dasharray').
1859 %alternative_spelling('stroke-dash-array','stroke-dasharray').
1860 alternative_spelling(stroke_linecap,'stroke-linecap').
1861 alternative_spelling(stroke_linejoin,'stroke-linejoin').
1862 alternative_spelling(stroke_width,'stroke-width').
1863
1864
1865
1866 % used to suggest fixing unsupported attributes in SVG objects:
1867 equivalent_attribute(cx,[rect],x).
1868 equivalent_attribute(cy,[rect],y).
1869 equivalent_attribute(x,[circle,ellipse],cx).
1870 equivalent_attribute(x,[line],x1).
1871 equivalent_attribute(y,[circle,ellipse],cy).
1872 equivalent_attribute(y,[line],y1).
1873 equivalent_attribute(r,[rect],rx). % ry also exists
1874 equivalent_attribute(rx,[circle],r).
1875 equivalent_attribute(width,[circle],r).
1876 equivalent_attribute(width,[ellipse],rx).
1877 equivalent_attribute(height,[ellipse],ry).
1878
1879
1880
1881
1882 % ----------------
1883
1884 % parse and load an individual JSON VisB item, e.g, :
1885 % {
1886 % "id":"train_info_text",
1887 % "attr":"x",
1888 % "value":"real(train_rear_end)*100.0/real(TrackElementNumber+1)",
1889 % "comment":"move info field above train"
1890 % },
1891 process_visb_json_item(File,Json) :-
1892 process_repeat(0,Json,File,add_visb_json_item).
1893
1894 add_visb_json_item(File,json(List)) :-
1895 get_attr_true(ignore,List,File), % ignore this item
1896 !.
1897 add_visb_json_item(File,json(List)) :-
1898 del_attr_with_pos(id,List,string(ID),L1,File,PosStartOfItem),
1899 !,
1900 process_visb_json_item_id(File,L1,ID,PosStartOfItem).
1901 add_visb_json_item(File,Json) :-
1902 !,
1903 get_pos_from_list(Json,File,Pos),
1904 add_error(visb_visualiser,'VisB Item has no id attribute:',Json,Pos).
1905
1906 process_visb_json_item_id(File,L1,ID,PosStartOfItem) :-
1907 ? del_attr(attr,L1,string(Attr),L2), % VisB has attr and value infos
1908 force_del_attr_with_pos(value,L2,string(Formula),L3,File,PosFormula),
1909 !,
1910 ? (del_attr(comment,L3,string(Desc),L4) -> true ; Desc = '',L4=L3),
1911 debug_format(19,' Processing id:~w attr:~w : value:~w desc:~w~n',[ID,Attr,Formula,Desc]),
1912 actually_add_visb_json_item(ID,Attr,Formula,Desc,L4,PosStartOfItem,PosFormula,File).
1913 process_visb_json_item_id(File,L1,ID,PosStartOfItem) :-
1914 get_attr(SomeSVGAttr,L1,_V),
1915 ? is_svg_attribute(SomeSVGAttr),
1916 debug_format(19,'Detected new style VisB JSON declaration with id:~w and SVG attr:~w~n',[ID,SomeSVGAttr]),
1917 !,
1918 % object is in new format with multiple attributes "x":"0" rather than "attr":"x", "value":"0"
1919 (del_attr(comment,L1,string(Desc),L2) -> true ; Desc = '',L2=L1),
1920 ? (non_det_del_attr_with_pos(SVGATTR,L2,string(Formula),L3,File,PosFormula),
1921 is_visb_item_svg_attribute(PosFormula,SVGATTR,Formula),
1922 debug_format(19,' -> Processing new style id:~w attr:~w : value:~w desc:~n',[ID,SVGATTR,Formula,Desc]),
1923 actually_add_visb_json_item(ID,SVGATTR,Formula,Desc,L3,PosStartOfItem,PosFormula,File),
1924 fail
1925 ;
1926 true).
1927 process_visb_json_item_id(_File,_JsonList,ID,PosStartOfItem) :-
1928 !,
1929 add_error(visb_visualiser,'Illegal VisB Item without attr and value fields:',ID,PosStartOfItem).
1930
1931 is_visb_item_svg_attribute(Pos,Attr,Val) :-
1932 Attr \= override, % so we ignore a possible override attribute
1933 ? (is_svg_attribute(Attr) -> true
1934 ; add_warning(visb_visualiser,'Ignoring unknown attribute: ',Attr=Val,Pos),
1935 fail
1936 ).
1937
1938 :- use_module(probsrc(tools_strings),[safe_name/2]).
1939 actually_add_visb_json_item(ID,Attr,Formula,Desc,JsonList,PosStartOfItem,PosFormula,File) :-
1940 set_error_context(visb_error_context(item,ID,Attr,PosFormula)),
1941 atom_codes(Formula,FormulaC),
1942 (parse_expr_for_visb(FormulaC,JsonList,PosFormula,TypedExpr)
1943 % TO DO: if optional attribute present: avoid generating errors in b_parse_machine_expression_from_codes
1944 -> assert_visb_item(ID,Attr,TypedExpr,Desc,PosStartOfItem,JsonList,File)
1945 ; get_attr_with_pos(optional,JsonList,_,File,Pos)
1946 -> formatsilent('Ignoring optional VisB item for ~w (lines ~w) due to error in B formula~n',[ID,Pos])
1947 ; ajoin(['Cannot parse or typecheck VisB formula for ',ID,' and attribute ',Attr,':'],Msg),
1948 add_error(visb_visualiser,Msg,Formula,PosFormula)
1949 ), clear_error_context.
1950
1951
1952 :- use_module(probsrc(bsyntaxtree), [find_identifier_uses/3]).
1953 % assert a VISB item (aka VISB_SVG_UPDATE)
1954 assert_visb_item(ID,Attr,_TypedExpr,_Desc,PosStartOfItem,_,_) :-
1955 visb_item(ID,Attr,_,_,_,Pos2,Meta2),
1956 !,
1957 get_file_name_msg(PosStartOfItem,From1,File1),
1958 (member(override,Meta2)
1959 -> ajoin(['Overriding VisB item',From1,File1,' for same SVG ID ',ID,' and attribute '],Msg),
1960 add_debug_message(visb_visualiser,Msg,Attr,Pos2)
1961 ; ajoin(['Overriding VisB item',From1,File1,' for same SVG ID ',ID,
1962 '. Add an \"override\" attribute to remove this warning. Overriden attribute '],Msg),
1963 add_warning(visb_visualiser,Msg,Attr,Pos2),
1964 % error_context already includes attribute and ID
1965 add_message(visb_visualiser,'Overriding this stored formula for ',ID,PosStartOfItem) % provide detailed info
1966 ).
1967 assert_visb_item(ID,Attr,_TypedExpr,_Desc,PosStartOfItem,_JsonList,_File) :-
1968 illegal_attribute_for_visb_item(ID,Attr),!,
1969 add_warning(visb_visualiser,'This attribute cannot be modified in a VisB item: ',Attr,PosStartOfItem).
1970 assert_visb_item(ID,Attr,TypedExpr,Desc,PosStartOfItem,JsonList,File) :-
1971 (get_attr_true(override,JsonList,File) -> Meta = [override] ; Meta=[]),
1972 % determine_type_of_visb_formula(TypedExpr,_,Class) now does take definitions into account; TODO: save info
1973 find_identifier_uses(TypedExpr,[],UsedIds),
1974 assertz(visb_item(ID,Attr,TypedExpr,UsedIds,Desc,PosStartOfItem,Meta)).
1975
1976 illegal_attribute_for_visb_item(_,children).
1977 illegal_attribute_for_visb_item(_,group_id).
1978 illegal_attribute_for_visb_item(_,id).
1979 illegal_attribute_for_visb_item(_,svg_class).
1980
1981
1982 get_file_name_msg(Pos1,' from ',File1) :- extract_tail_file_name(Pos1,File1),!.
1983 get_file_name_msg(_,'',''). % no file info
1984
1985 % ----
1986
1987 get_attr_true(Attr,JsonList,File) :-
1988 get_attr_with_pos(Attr,JsonList,TRUE,File,Pos),
1989 (json_true_value(TRUE) -> true
1990 ; json_false_value(TRUE) -> fail
1991 ; ajoin(['Value for attribute ',Attr,' is not true or false: '],Msg),
1992 add_warning(visb_visualiser,Msg,TRUE,Pos)
1993 ).
1994
1995 json_true_value(@(true)).
1996 json_true_value(string(true)).
1997 json_true_value(number(1)).
1998
1999 json_false_value(@(false)).
2000 json_false_value(string(false)).
2001 json_false_value(number(0)).
2002
2003 % ----------------
2004 % FOR-LOOP / REPEAT processing
2005
2006 %process_repeat(RepCounter, Json, FinalCall to be executed repeatedly for each instance with File and Json, File)
2007 % RepCounter tells us which of %0, %1, ... should be replaced next
2008
2009 process_repeat(RepCount,json(JsonList),File,FinalCall) :-
2010 ? non_det_del_attr_with_pos(FOR_REP,JsonList,Value,RestJsonList,File,ForRepPos),
2011 % find first for or repeat and process it
2012 (FOR_REP=for ; FOR_REP=repeat),
2013 !,
2014 process_first_repeat(FOR_REP,Value,ForRepPos,RepCount,json(RestJsonList),File,FinalCall).
2015 process_repeat(_RepCount,Json,File,FinalCall) :-
2016 % we have processed all for/repeat loops: now perform the final call on the transformed codes
2017 call(FinalCall,File,Json).
2018
2019 process_first_repeat(for,json(ForList),ForPos,RepCount,JsonData,File,FinalCall) :-
2020 !, % we have a for loop like "for": {"from":1, "to":4}
2021 force_get_attr_nr(from,ForList,From,File),
2022 force_get_attr_nr(to,ForList,To,File),
2023 (get_attr_with_pos(step,ForList,StepAttrVal,File,StepPos),
2024 get_number_value(StepAttrVal,Step,step,StepPos)
2025 -> true % there is an explicit step attribute
2026 ; Step=1),
2027 debug_format(19,' -> Iterating %~w from ~w to ~w with step ~w~n',[RepCount,From,To,Step]),
2028 R1 is RepCount+1,
2029 number_codes(RepCount,Pat),
2030 check_between(From,To,Step,ForPos), % check whether step value makes sense
2031 ? ( between(From,To,Step,IterElem),
2032 number_codes(IterElem,IterElemC), % we will replace the text %Pat by the text of the number IterElem
2033 replace_in_json(Pat,IterElemC,JsonData,ReplacedJsonData), % replace within other for/repeat loops, but also other attributes
2034 process_repeat(R1,ReplacedJsonData,File,FinalCall), % now process next loop or finish
2035 fail
2036 ; true).
2037 process_first_repeat(repeat,array(RepList),RepPos,RepCount,JsonData,File,FinalCall) :-
2038 !, % we have a repetition like "repeat": ["tr1","tr2"] or "repeat": [ ["1","2"] , ...]
2039 (RepList=[array(L1)|_], length(L1,Len)
2040 -> NewRepCount is RepCount+Len, % we have a multi-repeat with list of values to be replaced
2041 LastRepCount is NewRepCount-1,
2042 debug_format(19,' -> Iterating repeat (%~w,...,%~w) over ~w~n',[RepCount,LastRepCount,RepList]),
2043 check_all_same_length_json(RepList,Len,RepPos)
2044 ; NewRepCount is RepCount+1, % next replacement starts at $(RepCount+1)
2045 debug_format(19,' -> Iterating repeat (%~w) over ~w~n',[RepCount,RepList])
2046 ),
2047 ? ( member(IterElem,RepList),
2048 multi_replace_in_json(IterElem,RepCount,JsonData,ReplacedJsonData), % replace within other for/repeat loops, but also other attributes
2049 process_repeat(NewRepCount,ReplacedJsonData,File,FinalCall), % now process next loop or finish
2050 fail
2051 ; true).
2052
2053 check_all_same_length_json(List,ExpectedLen,Pos) :-
2054 nth1(Nr,List,Json),
2055 (Json=array(SubList),length(SubList,Len) -> Len \= ExpectedLen ; Len='not a list'),
2056 !,
2057 ajoin(['The element number ',Nr,' of the repeat list has not the expected length of ',ExpectedLen,', length is: '],Msg),
2058 add_warning(visb_visualiser,Msg,Len,Pos).
2059 check_all_same_length_json(_,_,_).
2060
2061 json_value_to_codes(@(Literal), C) :- atom(Literal), !, atom_codes(Literal, C).
2062 json_value_to_codes(number(Number), C) :- number(Number), !, number_codes(Number, C).
2063 json_value_to_codes(string(String), C) :- atom(String), !, atom_codes(String, C).
2064 json_value_to_codes(Json, _) :- !, add_error(json_value_to_codes,'Cannot convert json term to codes:', Json), fail.
2065
2066 % replace (possibly) multiple patterns at once
2067 multi_replace_in_json(array([]),_RepCount,JsonIn,JsonOut) :- !, JsonOut=JsonIn.
2068 multi_replace_in_json(array([IterElem|TIT]),RepCount,JsonIn,JsonOut) :-
2069 !,
2070 number_codes(RepCount,Pat),
2071 json_value_to_codes(IterElem,IterElemC),
2072 %format('Replacing in JSON: ~s -> ~s~n',[Pat,IterElemC]),
2073 replace_in_json(Pat,IterElemC,JsonIn,Json),
2074 R1 is RepCount+1,
2075 multi_replace_in_json(array(TIT),R1,Json,JsonOut).
2076 multi_replace_in_json(IterElem,RepCount,JsonIn,JsonOut) :- % a value, not a list
2077 !,
2078 number_codes(RepCount,Pat),
2079 json_value_to_codes(IterElem,IterElemC),
2080 %format('Replacing in JSON: ~s -> ~s~n',[Pat,IterElemC]),
2081 replace_in_json(Pat,IterElemC,JsonIn,JsonOut).
2082
2083 check_between(_,_,Step,ForPos) :- Step =< 0, !,
2084 add_error(visb_visualiser,'The step of a for loop must be positive:',Step,ForPos),fail.
2085 check_between(From,To,Step,ForPos) :- Iters is (To-From)/Step,
2086 Iters > 100000,!,
2087 add_error(visb_visualiser,'Very large for loop:',Iters,ForPos),fail.
2088 check_between(_,_,_,_).
2089
2090
2091 % ----------------
2092
2093 % parse and load VisB events
2094 % A VisB Event looks like:
2095 % {
2096 % "id": "button",
2097 % "event": "toggle_button",
2098 % "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
2099 % { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
2100 % }
2101 process_json_event(File,Json) :-
2102 process_repeat(0,Json,File,add_visb_json_event).
2103
2104 add_visb_json_event(File,json(List)) :- get_attr_true(ignore,List,File), !. % ignore this item
2105 add_visb_json_event(File,json(List)) :-
2106 get_pos_from_list(List,File,Pos),
2107 force_del_attr(id,List,string(ID),L0,File), % for items it could make sense to not specify an id
2108 ? (del_attr(event,L0,string(Event),L1) -> true ; Event='', L1=L0),
2109 (del_attr_with_pos(predicates,L1,array(Preds),L2,File,PredPos) -> true
2110 ; del_attr_with_pos(preds,L1,array(Preds),L2,File,PredPos) -> true
2111 ; Preds=[], L2=L1, PredPos=unknown),
2112 ? (del_attr(hovers,L2,array(Hovers),L3) -> true ; Hovers=[],L3=L2),
2113 (del_attr(items,L3,array(EI),L4)
2114 -> (empty_b_event(Event)
2115 -> EnableItems=[],
2116 add_warning(visb_visualiser,'Ignoring enable items; you need to provide an event name:',ID,Pos)
2117 ; EnableItems=EI)
2118 ; EnableItems=[],L4=L3),
2119 debug_format(19,' Processing id:~w event:~w preds:~w enable:~w hovers:~w~n',[ID,Event,Preds,EnableItems,Hovers]),
2120 !,
2121 actually_add_visb_json_event(ID,Event,Preds,Hovers,EnableItems,L4,File,Pos,PredPos).
2122 add_visb_json_event(File,Json) :-
2123 !,
2124 get_pos_from_list(Json,File,Pos),
2125 add_error(visb_visualiser,'Illegal VisB Event:',Json,Pos).
2126
2127 actually_add_visb_json_event(ID,Event,JsonPreds,JsonHovers,JsonEnableItems,JsonList,File,Pos,PredPos) :-
2128 check_additional_args(JsonList,File),
2129 maplist(process_json_pred,JsonPreds,Preds),
2130 maplist(process_json_enabling_item(ID,Event,File),JsonEnableItems,EnableItems),
2131 maplist(process_json_hover(ID,File),JsonHovers,Hovers),
2132 add_visb_event(ID,Event,Preds,Hovers,EnableItems,File,Pos,PredPos,JsonList).
2133
2134 :- use_module(probsrc(tools_strings), [atom_prefix/2]).
2135 :- use_module(probsrc(bmachine), [b_is_operation_name/1]).
2136 add_visb_event(ID,Event,Preds,Hovers,EnableItems,File,Pos,PredPos,JsonList) :-
2137 (retract(visb_event(ID,OldEvent,OldPreds,OldTypedPred,OldFile,OldPos))
2138 -> (get_attr_true(override,JsonList,File)
2139 -> ajoin(['Overriding VisB event from file ',OldFile,' for ID: '],Msg),
2140 add_debug_message(visb_visualiser,Msg,ID,Pos),
2141 retractall(visb_hover(ID,_,_,_,_,_))
2142 ; (OldFile=File
2143 -> ajoin(['No override attribute: adding VisB event ',Event,
2144 ' (first event ',OldEvent,') for ID: '],Msg)
2145 ; ajoin(['No override attribute: adding VisB event ',Event,
2146 ' (first event ',OldEvent,' in file ',OldFile,') for ID: '],Msg)
2147 ),
2148 add_debug_message(visb_visualiser,Msg,ID,Pos),
2149 assertz(auxiliary_visb_event(ID,OldEvent,OldPreds,OldTypedPred,OldPos))
2150 ),
2151 assert_visb_event(ID,Event,Preds,Hovers,EnableItems,File,Pos,PredPos)
2152 % ProB2-UI cannot currently support multiple events associated with the same id
2153 % TODO: merge visb_events if we have no override attribute
2154 ? ; (xtl_mode ; b_is_operation_name_or_external_subst(Event)) ->
2155 assert_visb_event(ID,Event,Preds,Hovers,EnableItems,File,Pos,PredPos)
2156 ; (empty_b_event(Event) ; \+ b_or_z_mode)
2157 -> % for empty event we just want hovers
2158 (Preds = [] -> true
2159 ; add_warning(visb_visualiser,'Ignoring preds for VisB event for SVG ID: ',ID,Pos)
2160 ),
2161 assert_visb_event(ID,Event,[],Hovers,EnableItems,File,Pos,PredPos)
2162 ; get_attr_with_pos(optional,JsonList,_,File,Pos) ->
2163 formatsilent('Ignoring optional VisB event for ~w (lines ~w) due to unknown B operation ~w~n',[ID,Pos,Event])
2164 ; detect_op_call_with_paras(Event,OpName) ->
2165 add_warning(visb_visualiser,'Ignoring parameters provided in event; use predicate attribute to specify parameters: ',Event,Pos),
2166 assert_visb_event(ID,OpName,Preds,Hovers,EnableItems,File,Pos,PredPos)
2167 ; atom(Event), atom_prefix('{',Event) ->
2168 ajoin(['Unknown B operation ', Event, ' in VisB for SVG ID (be sure to use events attribute for multiple events): '],Msg),
2169 add_warning(visb_visualiser,Msg,ID,Pos)
2170 ; ajoin(['Unknown B operation ', Event, ' in VisB for SVG ID: '],Msg),
2171 add_warning(visb_visualiser,Msg,ID,Pos)
2172 ).
2173
2174 b_is_operation_name_or_external_subst(OpName) :- b_is_operation_name(OpName).
2175 b_is_operation_name_or_external_subst(Special) :- special_operation(Special).
2176
2177 % maybe we should provide those via the external substitution interface:
2178 % these are all schedulers which choose among existing enabled operations in some manner
2179 special_operation('MCTS_AUTO_PLAY').
2180 special_operation('RANDOM_ANIMATE').
2181 special_operation('RANDOM_ANIMATE_UNTIL_LTL').
2182 % maybe other special names like random_animate with nr of steps, LTL until, ...
2183 special_operation_enabled('MCTS_AUTO_PLAY',_,_,_) :- mcts_auto_play_available.
2184 special_operation_enabled('RANDOM_ANIMATE',_,_,_). % TODO: check if a transition exists
2185 special_operation_enabled('RANDOM_ANIMATE_UNTIL_LTL',_,_,_).
2186
2187 % detect operation call with parameters
2188 detect_op_call_with_paras(Event,OpName) :- atom(Event),
2189 atom_codes(Event,Codes), parse_op_call_name(OpC,Codes,_),!,
2190 atom_codes(OpName,OpC),
2191 b_is_operation_name(OpName).
2192
2193 parse_op_call_name([X|T]) --> alpha(X), parse_op_call_name2(T).
2194 parse_op_call_name2([]) --> "(".
2195 parse_op_call_name2([H|T]) --> alphadigit(H), parse_op_call_name2(T).
2196
2197 alpha(X) --> [X],{X>=97, X=<122}.
2198 alphadigit(X) --> [X], ({X>=97,X=<122} ; {X>=65, X=<90} ; {X=95} ; {X>=48, X=<57}).
2199
2200 empty_b_event('').
2201
2202 assert_visb_event(ID,Event,Preds,Hovers,EnableItems,File,Pos,PredPos) :-
2203 construct_pre_post_predicate(ID,Event,Preds,TypedPred,PredPos),
2204 assertz(visb_event(ID,Event,Preds,TypedPred,File,Pos)),
2205 % process hovers
2206 ? (member(HoverElement,Hovers),
2207 (HoverElement=visb_hover(HoverID,Attr,EnterVal,ExitVal) -> true ; add_error(visb_visualiser,'Illegal hover term:',HoverElement),fail),
2208 assert_visb_hover(ID,HoverID,Attr,EnterVal,ExitVal,Pos),fail
2209 ; true),
2210 % now process any additional items with disabled and enabled values
2211 assert_visb_enabling_item_list(Event,TypedPred,EnableItems,File,Pos).
2212
2213 process_json_pred(string(P),R) :- !, R=P.
2214 process_json_pred(Json,_) :- !, add_error(visb_visualiser,'Illegal json term for predicate:',Json), fail.
2215
2216 process_json_hover(OriginID,File,json(Hover),visb_hover(ID,Attr,EnterVal,LeaveVal)) :-
2217 force_del_attr(attr,Hover,string(Attr),H2,File),
2218 force_del_attr_with_pos(enter,H2,EV,H3,File,EnterPos),
2219 force_del_attr_with_pos(leave,H3,LV,H4,File,ExitPos),
2220 (is_svg_number_attribute(Attr) % we evaluate number attributes
2221 -> get_number_value(EV,EnterVal,Attr,EnterPos),
2222 get_number_value(LV,LeaveVal,Attr,ExitPos)
2223 ; string(EnterVal)=EV, string(LeaveVal)=LV % return string as is; TODO: also evaluate other attributes
2224 ),
2225 (get_attr(id,H4,string(ID)) -> true ; ID=OriginID).
2226
2227
2228 assert_visb_hover(TriggerID,SVG_ID,Attr,EnterVal,ExitVal,Pos) :-
2229 assert(visb_hover(TriggerID,SVG_ID,Attr,EnterVal,ExitVal,Pos)),
2230 (visb_has_hovers(TriggerID) -> true ; assert(visb_has_hovers(TriggerID))),
2231 (visb_has_visibility_hover(SVG_ID) -> true
2232 ; Attr=visibility -> assert(visb_has_visibility_hover(TriggerID)) % object can be made visible by hover
2233 ; true),
2234 debug_format(19,'Adding hover for ~w : ~w.~w -> ~w <- ~w~n',[TriggerID,SVG_ID,Attr,EnterVal,ExitVal]).
2235
2236
2237 % process items in event which get translated to enabling/disabling predicates
2238 % "items":[ {"attr":"stroke-width","enabled":"10", "disabled":"1"} ]
2239 process_json_enabling_item(ID,Event,File,json(JsonList),
2240 visb_enable_item(SvgID,Attr,EnabledValExpr,DisabledValExpr,PosAttr)) :-
2241 force_del_attr_with_pos(attr,JsonList,string(Attr),L2,File,PosAttr),
2242 force_del_attr_with_pos('enabled',L2,string(EnVal),L3,File,EPos),
2243 force_del_attr_with_pos('disabled',L3,string(DisVal),L4,File,DPos),
2244 (del_attr(id,L4,string(SvgID),L5) -> true ; SvgID=ID, L4=L5),
2245 atom_codes(EnVal,EC),
2246 parse_expr_for_visb(EC,L5,EPos,EnabledValExpr),
2247 atom_codes(DisVal,DC),
2248 parse_expr_for_visb(DC,L5,DPos,DisabledValExpr),
2249 (debug_mode(off) -> true
2250 ; translate_bexpression_with_limit(EnabledValExpr,30,EVS),
2251 translate_bexpression_with_limit(DisabledValExpr,30,DVS),
2252 formatsilent('Enabling item for event ~w and SVG ID ~w and attribute ~w : ~w <-> ~w~n',[Event,SvgID,Attr,EVS,DVS])
2253 ).
2254
2255 assert_visb_enabling_item_list(Event,TypedPred,EnableList,File,Pos) :-
2256 maplist(check_enabling_item(Event),EnableList),
2257 (EnableList \= []
2258 -> (debug_mode(off)
2259 -> true
2260 ; format('Associating enabling/disabling list with event ~w and predicate: ',[Event]), translate:print_bexpr(TypedPred),nl),
2261 assert(visb_event_enable_list(Event,TypedPred,EnableList,File,Pos))
2262 ; true).
2263
2264 check_enabling_item(Event,visb_enable_item(SvgID,Attr,_,_,PosAttr)) :-
2265 (visb_item(SvgID,Attr,_,_,_Desc,DuplicatePos,_)
2266 -> (extract_span_description(DuplicatePos,DuplPos) -> true; DuplPos=DuplicatePos),
2267 ajoin(['VisB conflict for SVG ID ',SvgID,' and attribute ',Attr,
2268 '. Conflict between VisB item (',DuplPos,') and VisB enable/disable entry for event: '],Msg),
2269 add_warning(visb_visualiser,Msg,Event,PosAttr)
2270 ; true).
2271
2272 valid_additional_attributes(comment).
2273 valid_additional_attributes(description).
2274 valid_additional_attributes(optional).
2275 valid_additional_attributes(override).
2276
2277 % check if there are additional unprocessed args and generate a warning
2278 check_additional_args(JsonList,File) :-
2279 get_attr_with_pos(Attr,JsonList,_,File,Pos),
2280 \+ valid_additional_attributes(Attr),
2281 add_warning(visb_visualiser,'Ignoring unknown JSON field: ',Attr,Pos),
2282 fail.
2283 check_additional_args(_,_).
2284
2285 :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2]).
2286 % construct a pre-post typed predicate for a VisB Event
2287 construct_pre_post_predicate(SvgID,OpName,Preds,TypedPred,Pos) :-
2288 set_error_context(visb_error_context(event,SvgID,OpName,Pos)),
2289 maplist(construct_pre_post_pred(OpName,Pos),Preds,TL),
2290 clear_error_context,
2291 conjunct_predicates(TL,TypedPred).
2292
2293 :- use_module(probsrc(bmachine), [b_parse_machine_operation_pre_post_predicate/5]).
2294 construct_pre_post_pred(OpName,Pos,PredStr,TypedPred) :- empty_b_event(OpName),!,
2295 add_error(visb_visualiser,'Cannot parse VisB event predicate without event name:',PredStr,Pos),
2296 TypedPred = b(truth,pred,[]).
2297 construct_pre_post_pred(OpName,Pos,String,TypedExpr) :- special_operation(OpName),!,
2298 % we have a special operation; allow to provide an expression with options/parameters
2299 atom_codes(String,Codes),
2300 GenParseErrors=gen_parse_errors_for(Pos),
2301 parse_expr(Codes,TypedExpr,GenParseErrors). % TODO: should we require a predicate instead, and provide arg names?
2302 construct_pre_post_pred(OpName,Pos,String,TypedPred) :-
2303 atom_codes(String,Codes), replace_special_patterns(Codes,RCodes,Pos), %format("Replaced : ~S~n",[RCodes]),
2304 get_visb_extra_scope([identifier(VisBExtraScope)]),
2305 visb_click_meta_b_type(MetaRecType),
2306 ExtraScope = [identifier([b(identifier('VISB_CLICK_META_INFOS'),MetaRecType,[visb_generated])|VisBExtraScope])],
2307 (b_parse_machine_operation_pre_post_predicate(RCodes,ExtraScope,TypedPred,OpName,gen_parse_errors_for(Pos))
2308 -> true
2309 ; add_error(visb_visualiser,'Error for VisB event predicate:',String,Pos),
2310 TypedPred = b(truth,pred,[])
2311 ).
2312
2313 % replace special patterns by dummy values to avoid error messages in ProB2-UI
2314 replace_special_patterns([],[],_Pos) :- !.
2315 replace_special_patterns([37|T],Res,Pos) :- !, % percentage sign %
2316 replace_aux(T,Res,Pos).
2317 replace_special_patterns([H|T],[H|RT],Pos) :- !, replace_special_patterns(T,RT,Pos).
2318
2319 replace_aux(Input,Res,Pos) :-
2320 replace_pat(PAT,Replacement),
2321 append(PAT,T,Input),
2322 !,
2323 atom_codes(PatAtom,PAT),
2324 ajoin(['The %',PatAtom,' pattern is obsolete. Please use VISB_CLICK_META_INFOS\'',PatAtom,' instead.'],Msg),
2325 add_warning(visb_visualiser,Msg,'',Pos),
2326 append(Replacement,ResT,Res),
2327 replace_special_patterns(T,ResT,Pos).
2328 replace_aux(Input,[37|Res],Pos) :- !, replace_special_patterns(Input,Res,Pos).
2329
2330 replace_pat("shiftKey","VISB_CLICK_META_INFOS'shiftKey").
2331 replace_pat("metaKey","VISB_CLICK_META_INFOS'metaKey").
2332 replace_pat("pageX","VISB_CLICK_META_INFOS'pageX").
2333 replace_pat("pageY","VISB_CLICK_META_INFOS'pageY").
2334
2335
2336
2337 % small utils:
2338 % ----------------
2339
2340 % a variation of between/3 with a step argument
2341 between(From,To,_,_) :- From > To, !,fail.
2342 between(From,_,_,From).
2343 ?between(From,To,Step,Elem) :- F1 is From+Step, between(F1,To,Step,Elem).
2344
2345 :- use_module(probsrc(tools_strings),[is_simple_classical_b_identifier_codes/1]).
2346 :- use_module(probsrc(preferences), [reset_temporary_preference/2,temporary_set_preference/3]).
2347 parse_expr(ExprCodes,TypedExpr,_GenParseErrors) :-
2348 is_simple_classical_b_identifier_codes(ExprCodes),
2349 atom_codes(DefID,ExprCodes),
2350 visb_definition(DefID,Type,_DefFormula,Class,_VPos,_),
2351 !,
2352 TypedExpr = b(identifier(DefID),Type,[type_of_formula(Class)]).
2353 parse_expr(ExprCodes,TypedExpr,GenParseErrors) :-
2354 temporary_set_preference(allow_arith_operators_on_reals,true,CHNG),
2355 get_visb_extra_scope(ExtraScope),
2356 % formatsilent('Parsing: ~s (extra ids: ~w)~n',[ExprCodes,ExtraScope]), start_ms_timer(T1),
2357 call_cleanup(bmachine:b_parse_machine_expression_from_codes_with_prob_ids(ExprCodes,ExtraScope,TypedExpr,
2358 GenParseErrors),
2359 reset_temporary_preference(allow_arith_operators_on_reals,CHNG)).
2360 %stop_ms_walltimer_with_msg(T1,'parsing: ').
2361 % TODO: we could share a machine parameter M like in prob2_interface
2362 % so that b_type_expression_for_full_b_machine will load machine only once
2363 % cf b_type_open_predicate_for_full_b_machine
2364
2365 determine_type_of_visb_formula(b(_,_,[type_of_formula(Class)]),all,Res) :- !,
2366 Res = Class. % generated by VisB, TODO: store UsedTIds in type_of_formula(.)
2367 determine_type_of_visb_formula(TypedExpr,TIds,Class) :-
2368 determine_type_of_formula_with_visb_defs(TypedExpr,TIds,Class).
2369
2370 %check for used_ids inside TypedExpr an see what type of visb_definition are used
2371 determine_type_of_formula_with_visb_defs(TypedExpr,TIds,ResClass) :-
2372 determine_type_of_formula(TypedExpr,TIds,Class1), % compute class w/o knowledge of VisB definitions
2373 ? (class_more_general_than(Class2,Class1),
2374 ? required_by_visb_def(TIds,Class2) -> Class=Class2
2375 ; Class=Class1),
2376 (Class=requires_variables -> ResClass=Class
2377 ; expression_requires_state(TypedExpr) -> ResClass = requires_variables
2378 ; ResClass=Class).
2379
2380 :- use_module(probsrc(bsyntaxtree),[map_over_bexpr/2]).
2381 :- use_module(probsrc(external_functions),[external_function_requires_state/1]).
2382 expression_requires_state(TypedExpr) :-
2383 (map_over_bexpr(sub_expression_requires_state,TypedExpr) -> true ; fail).
2384 % TODO: should we also check is_not_declarative/1 ? e.g., for RANDOM or CHANGED
2385 sub_expression_requires_state(external_pred_call(P,_)) :- external_function_requires_state(P).
2386 sub_expression_requires_state(external_function_call(P,_)) :- external_function_requires_state(P).
2387
2388
2389 class_more_general_than(requires_variables,requires_nothing).
2390 class_more_general_than(requires_variables,requires_constants).
2391 class_more_general_than(requires_constants,requires_nothing).
2392
2393 required_by_visb_def(TIds,Class) :-
2394 ? member(TID,TIds), get_texpr_id(TID,ID),visb_definition(ID,_,_,Class,_,_).
2395
2396
2397 get_visb_extra_scope([identifier(ExtraIDs)]) :-
2398 get_visb_extra_identifiers(ExtraIDs).
2399 get_visb_extra_identifiers(ExtraIDs) :-
2400 findall(b(identifier(ID),Type,[visb_generated]),visb_definition(ID,Type,_,_,_,_),ExtraIDs).
2401
2402 % replace a pattern code prefixed by % by another code list
2403 replace_in_json(Pattern,RepStr,string(Val),string(NewVal)) :- !, replace_atom(Pattern,RepStr,Val,NewVal).
2404 replace_in_json(Pattern,RepStr,array(Vals),array(NewVals)) :- !, maplist(replace_in_json(Pattern,RepStr),Vals,NewVals).
2405 replace_in_json(Pattern,RepStr,json(Vals),json(NewVals)) :- !, maplist(replace_in_json_pair(Pattern,RepStr),Vals,NewVals).
2406 replace_in_json(_,_,Val,Val). % number/literal (no replacement necessary)
2407
2408 replace_in_json_pair(Pattern,RepStr,'='(KIn,VIn,Pos),'='(KOut,VOut,Pos)) :-
2409 replace_atom(Pattern,RepStr,KIn,KOut),
2410 replace_in_json(Pattern,RepStr,VIn,VOut).
2411
2412 replace_atom(Pattern,RepStr,Val,NewVal) :-
2413 atom_codes(Val,Codes),
2414 replace_pat(Pattern,RepStr,NewCodes,Codes,[]),
2415 atom_codes(NewVal,NewCodes). % TO DO: keep as codes for efficiency
2416
2417 :- assert_must_succeed((visb_visualiser: replace_pat("0","_1_",Res,"ab%0cd",[]), Res == "ab_1_cd")).
2418 :- assert_must_succeed((visb_visualiser: replace_pat("0","",Res,"ab%0%0cd%0",[]), Res == "abcd")).
2419 % dcg utility to replace %Pat by NewStr constructing Res
2420 replace_pat(Pat,NewStr,Res) --> "%", Pat, !, {append(NewStr,TR,Res)}, replace_pat(Pat,NewStr,TR).
2421 replace_pat(Pat,RepStr,[H|T]) --> [H],!, replace_pat(Pat,RepStr,T).
2422 replace_pat(_,_,[]) --> [].
2423
2424
2425 % small JSON utils:
2426 % ----------------
2427
2428 ?get_attr(Attr,List,Val) :- member('='(Attr,Val,_),List).
2429 get_attr_with_pos(Attr,List,Val,File,Pos) :-
2430 El = '='(Attr,Val,_),
2431 ? member(El,List),
2432 get_pos_from_list([El],File,Pos).
2433
2434 ?del_attr(Attr,List,Val,Rest) :- select('='(Attr,Val,_Pos),List,Rest).
2435 %del_attr_with_pos(Attr,List,Val,Rest,Pos) :- select('='(Attr,Val,Pos),List,Rest).
2436 ?del_attr_with_pos(Attr,List,Val,Rest,File,PosTerm) :- select('='(Attr,Val,From-To),List,Rest),!,
2437 PosTerm = src_position_with_filename_and_ec(From,1,To,1,File).
2438 ?non_det_del_attr_with_pos(Attr,List,Val,Rest,File,PosTerm) :- select('='(Attr,Val,From-To),List,Rest),
2439 PosTerm = src_position_with_filename_and_ec(From,1,To,1,File).
2440
2441 force_del_attr(Attr,List,Val,Rest,File) :- force_del_attr_with_pos(Attr,List,Val,Rest,File,_).
2442
2443 ?force_del_attr_with_pos(Attr,List,Val,Rest,File,PosTerm) :- select('='(Attr,Val,From-To),List,Rest),!,
2444 %TODO: we would ideally want to extract the exact column position of Val, for this we need to extend the JSON parser first
2445 PosTerm = src_position_with_filename_and_ec(From,1,To,1,File).
2446 force_del_attr_with_pos(Attr,List,_,_,File,_) :- get_pos_from_list(List,File,Pos),!,
2447 add_error(visb_visualiser,'The JSON object has no attribute:',Attr,Pos),fail.
2448
2449 construct_prob_pos_term(From-To,File,PosTerm) :- !,
2450 PosTerm = src_position_with_filename_and_ec(From,1,To,1,File).
2451 construct_prob_pos_term(Pos,_,Pos).
2452
2453 force_get_attr_nr(Attr,List,Nr,File) :-
2454 force_del_attr_with_pos(Attr,List,AttrVal,_,File,Pos),!,
2455 get_number_value(AttrVal,Nr,Attr,Pos).
2456
2457 get_number_value(AttrVal,Nr,Attr,Pos) :-
2458 (AttrVal = number(Nr) -> true
2459 ; AttrVal = string(StrAttrVal),
2460 atom_codes(StrAttrVal,AttrValC),
2461 parse_expr(AttrValC,TypedExpr,gen_parse_errors_for(Pos)),
2462 determine_type_of_visb_formula(TypedExpr,UsedTIds,Class)
2463 % Class = requires_nothing, requires_constants, requires_variables
2464 ->
2465 (Class = requires_variables
2466 -> ajoin(['The JSON formula for the attribute"',Attr,
2467 '" must not depend on variables:'],Msg),
2468 add_error(visb_visualiser,Msg,StrAttrVal,Pos),fail
2469 ; Class = requires_constants,
2470 \+ is_concrete_constants_state_id(_)
2471 -> ajoin(['The JSON formula for the attribute"',Attr,
2472 '" depends on constants which have not been set up (via SETUP_CONSTANTS):'],Msg),
2473 add_error(visb_visualiser,Msg,StrAttrVal,Pos),fail
2474 ; Class = requires_constants,
2475 multiple_concrete_constants_exist,
2476 ajoin(['The JSON formula for the attribute"',Attr,
2477 '" depends on constants and multiple solutions for SETUP_CONSTANTS exist:'],Msg),
2478 add_warning(visb_visualiser,Msg,StrAttrVal,Pos),fail
2479 ; get_texpr_type(TypedExpr,Type),
2480 is_number_type(Type)
2481 -> eval_static_def(Class,'VisB attribute',Attr,TypedExpr,UsedTIds,ResVal,Pos),
2482 get_number_from_bvalue(ResVal,Nr)
2483 ; get_texpr_type(TypedExpr,Type),
2484 % it could produce a string which is a number; we could try and convert to a number
2485 ajoin(['The type ',Type,' of the JSON value formula for the attribute "',Attr,
2486 '" is not a number:'],Msg),
2487 add_error(visb_visualiser,Msg,StrAttrVal,Pos),fail
2488 )
2489 ; ajoin(['The JSON value for the attribute "',Attr,'" cannot be parsed as a number:'],Msg),
2490 add_error(visb_visualiser,Msg,AttrVal,Pos),fail).
2491
2492 is_number_type(integer).
2493 is_number_type(real).
2494 :- use_module(probsrc(kernel_reals),[is_real/2]).
2495 :- use_module(probsrc(custom_explicit_sets),[singleton_set/2]).
2496 get_number_from_bvalue(int(Nr),Res) :- !, Res=Nr.
2497 get_number_from_bvalue(Term,Res) :- is_real(Term,Nr),!,Res=Nr.
2498
2499 get_pos_from_list(json(List),File,Pos) :- !, get_pos_from_list(List,File,Pos).
2500 get_pos_from_list([H|T],File,RPos) :-
2501 H='='(_,_,From-_),
2502 last([H|T],
2503 '='(_,_,_-To)),
2504 !,
2505 RPos=src_position_with_filename_and_ec(From,1,To,1,File).
2506 get_pos_from_list(_,File,File). % should we provide another term?
2507
2508 % ----------------------------------
2509
2510 :- use_module(probsrc(b_global_sets),[add_prob_deferred_set_elements_to_store/3]).
2511 :- use_module(probsrc(tools),[b_string_escape_codes/2]).
2512
2513 % computing updates to SVG for a given StateId:
2514 % predicate to obtain required setAttribute changes to visualise StateId
2515 % looks up visb_item facts but also evaluates VISB_SVG_UPDATE definitions
2516 get_change_attribute_for_state(StateId,SvgID,SvgAttribute,Value) :-
2517 set_error_context(checking_context('VisB:','computing attributes for state')),
2518 get_expanded_bstate(StateId,ExpandedBState),
2519 set_context_state(StateId,get_change_attribute_for_state), % also sets it for external functions
2520 % TODO: also set history so that get_current_history in external_functions is more reliable
2521 ? call_cleanup(get_change_aux(StateId,ExpandedBState,SvgID,SvgAttribute,Value),
2522 (clear_context_state,clear_error_context)).
2523
2524 get_change_aux(StateId,ExpandedBState,SvgID,SvgAttribute,Value) :-
2525 ? get_aux2(StateId,ExpandedBState,SvgID0,SvgAttribute0,Value0,DefPos),
2526 post_process_visb_item(SvgID0,SvgAttribute0,Value0,DefPos,SvgID,SvgAttribute,Value).
2527 get_aux2(StateId,ExpandedBState,SvgID,SvgAttribute,Value,DefPos) :-
2528 % first get updates from DEFINITIONS which usually return sets of records
2529 ? get_svg_object_updates_from_definitions(ExpandedBState,SvgID,SvgAttribute,Value,DefPos),
2530 debug_format(19,' VISB_SVG_UPDATE ~w:~w = ~w (in state ~w)~n',[SvgID,SvgAttribute,Value,StateId]).
2531 get_aux2(StateId,ExpandedBState,SvgID,SvgAttribute,Value,Pos) :-
2532 % TODO: check if visibility item exists, and if value is false: do not compute the rest
2533 ? get_visb_item_formula(SvgID,SvgAttribute,Formula,Pos,ExpandedBState),
2534 % TODO: if UsedIds=[] only set attribute once, if it requires_only_constants : ditto
2535 evaluate_visb_formula(Formula,'VisB item',SvgID,ExpandedBState,FValue,Pos),
2536 %b_value_to_string(FValue,Value),
2537 extract_attr_value(SvgAttribute,FValue,Value,Pos),
2538 debug_format(19,' VisB item ~w:~w = ~w (in state ~w)~n',[SvgID,SvgAttribute,Value,StateId]).
2539
2540 % post-process certain items, like title to adapt the value and id:
2541 % SVG does not support a title attribute; we need a title child and set its text attribute
2542 post_process_visb_item(SvgID,title,Value,Pos,NewID,text,NewValue) :-
2543 (visb_svg_object_debug_info(SvgID,DebugInfo) -> ajoin([Value,'\n',DebugInfo],NewValue) ; NewValue=Value),
2544 ? (visb_svg_parent(SvgID,TitleID),
2545 visb_svg_object(TitleID,title,_,_,_)
2546 -> NewID=TitleID,
2547 debug_format(9,'Redirecting title update for ~w to child object ~w~n',[SvgID,TitleID])
2548 ; visb_svg_object(SvgID,_SVG_Class,_RestAttrs,_Desc,_Pos1)
2549 -> % this is an object we created
2550 add_warning(visb_visualiser,'Could not find title child object, be sure to define a static title attribute for SVG object: ',SvgID,Pos),
2551 fail
2552 ; add_warning(visb_visualiser,'SVG does not natively support title attributes: ',SvgID,Pos),
2553 fail
2554 ),!.
2555 post_process_visb_item(SvgID,Attr,Value,_,SvgID,Attr,Value).
2556
2557 % ------------------
2558
2559 % convert B value to Json String
2560 b_value_to_string(string(SValue),Res) :- !, Res=SValue. % What about quoting,...?
2561 b_value_to_string(FValue,Res) :-
2562 translate_bvalue_to_codes(FValue,ValCodes),
2563 atom_codes(Res,ValCodes).
2564
2565 % attributes for which we convert pairs to the concatenation of strings
2566 is_id_or_text_attribute(id).
2567 is_id_or_text_attribute('group_id'). % works much like a parent_id; also can be used to attach animate to e.g. a rect
2568 is_id_or_text_attribute('trigger_id').
2569 is_id_or_text_attribute('trigger-id').
2570 is_id_or_text_attribute(A) :- is_text_attribute(A).
2571 % children
2572 is_text_attribute('text').
2573 is_text_attribute('transform').
2574 is_text_attribute('event'). % for VISB_SVG_EVENTS
2575 is_text_attribute('predicate'). % for VISB_SVG_EVENTS
2576 is_text_attribute('svg_class').
2577
2578
2579 b_value_to_id_string(Val,String) :- b_val_to_id_string_aux(Val,add_underscore,String).
2580 b_value_to_text_string(Val,String) :- b_val_to_id_string_aux(Val,no_underscore,String).
2581
2582 % a special string conversion which e.g., allows to use things like ("ab",2) as id which gets translated to ab2
2583 % also useful for text attributes
2584 b_val_to_id_string_aux(string(SValue),_,Res) :- !, Res=SValue.
2585 b_val_to_id_string_aux((A,B),Add,Res) :- !,
2586 b_val_to_id_string_aux(A,Add,VA), b_val_to_id_string_aux(B,Add,VB),
2587 (Add=add_underscore
2588 -> atom_concat('_',VB,VB1) % introduce separator; in case we have things like numbers so that (12,3) /= (1,23)
2589 ; VB1=VB % for fields like predicate, transform, ... we do not want additional underscores
2590 ),
2591 atom_concat(VA,VB1,Res).
2592 b_val_to_id_string_aux(Set,Add,Res) :- singleton_set(Set,El),!, b_val_to_id_string_aux(El,Add,Res).
2593 % TODO: maybe convert sequence of values using conc
2594 b_val_to_id_string_aux(FValue,_,Res) :-
2595 translate_bvalue_to_codes(FValue,ValCodes),
2596 atom_codes(Res,ValCodes).
2597
2598 % get either a regular VisB item or an item associated with a VisB event and its enabled status
2599 get_visb_item_formula(SvgID,SvgAttribute,Formula,Pos,_ExpandedBState) :-
2600 ? visb_item(SvgID,SvgAttribute,Formula,_UsedIds,_Desc,Pos,_). % regular VisB item
2601 get_visb_item_formula(SvgID,SvgAttribute,Formula,Pos,ExpandedBState) :- % item within VisB event
2602 visb_event_enable_list(OpName,TypedPred,EnableList,_,ItemPos),
2603 debug_format(19,'Checking enabledness of VisB event ~w~n',[OpName]),
2604 (check_enabled(OpName,TypedPred,ExpandedBState,ItemPos)
2605 -> Formula=EnabledValExpr
2606 ; Formula=DisabledValExpr
2607 ),
2608 member(visb_enable_item(SvgID,SvgAttribute,EnabledValExpr,DisabledValExpr,Pos), EnableList).
2609
2610 check_enabled(OpName,Pred,ExpandedBState,Pos) :-
2611 special_operation(OpName),!,
2612 special_operation_enabled(OpName,Pred,ExpandedBState,Pos).
2613 check_enabled(OpName,Pred,ExpandedBState,Pos) :-
2614 b_is_operation_name(OpName),
2615 % TODO: see if we can use GUARD without execution
2616 % TODO: not yet working for XTL mode
2617 execute_operation_by_predicate_in_state_with_pos(ExpandedBState,OpName,Pred,_OpTerm,_NewState,Pos,_).
2618
2619
2620 get_expanded_bstate(StateId,ExpandedBState) :-
2621 \+ b_or_z_mode,!,
2622 StateId \= root,
2623 % in XTL mode we need to access the state via external functions like STATE_PROPERTY
2624 get_static_visb_state([],ExpandedBState).
2625 get_expanded_bstate(StateId,ExpandedBState) :-
2626 visited_expression(StateId,State),
2627 state_corresponds_to_initialised_b_machine(State,BState),
2628 debug_format(19,'Adding VisB definitions to state: ~w~n',[StateId]),
2629 add_prob_deferred_set_elements_to_store(BState,BState2,visible), % add prob_ids
2630 findall(visb_definition(DefID,Type,DefFormula,Class,VPos,Special),
2631 visb_definition(DefID,Type,DefFormula,Class,VPos,Special),DefList),
2632 eval_defs(DefList,BState2,ExpandedBState).
2633
2634
2635 :- use_module(probsrc(b_interpreter), [ b_compute_expression_nowf/7,b_compute_explicit_epression_no_wf/7]).
2636
2637 evaluate_static_visb_formula(Formula,Kind,Nr,InState,ResValue,Pos) :-
2638 get_static_visb_state(InState,StaticState),
2639 evaluate_visb_formula(Formula,Kind,Nr,StaticState,ResValue,Pos).
2640
2641 evaluate_visb_formula(Formula,Kind,Nr,BState2,ResValue,Pos) :-
2642 % add_message(visb,'Evaluating: ',Kind:Nr,Pos), debug:nl_time, %set_prolog_flag(profiling,on), print_profile,
2643 ? (b_compute_explicit_epression_no_wf(Formula,[],BState2,ResValue,Kind,Nr,Pos) -> true
2644 ; add_error(visb_visualiser,'Evaluation of VisB formula failed:',Formula,Pos),
2645 fail).
2646
2647 % evaluate VisB definitions in order one by one, adding values to state
2648 eval_defs([],State,State).
2649 eval_defs([visb_definition(ID,_,TypedExpr,_Class,VPos,Special)|T],State0,State2) :-
2650 (Special \= regular_def
2651 -> State1=State0 % ignore special defs; they are processed separately
2652 ; b_compute_expression_nowf(TypedExpr,[],State0,ResValue,'VisB definition',ID,VPos),
2653 State1 = [bind(ID,ResValue)|State0], % store value for later definitions and VisB items
2654 (debug_mode(off) -> true
2655 ; translate_bvalue_to_codes_with_limit(ResValue,2000,RC),
2656 formatsilent(' VisB definition ~w == ~s~n',[ID,RC]))
2657 ),
2658 eval_defs(T,State1,State2).
2659
2660 % check if we have a static value for a VisB definition:
2661 visb_def_static_value(DefID,Value) :-
2662 ? visb_definition(DefID,_,b(value(Value),_,_),Class,_,SpecialClass),
2663 SpecialClass = regular_def,
2664 (Class = requires_nothing ; Class = requires_constants). % probably we do not need to check this, as we have value/1
2665
2666 get_static_visb_state(InState,FullState) :-
2667 findall(bind(DefID,Value),visb_def_static_value(DefID,Value),FullState,InState).
2668 % TO DO: get state with deferred_set_elements,...
2669
2670 % ----------------------------------
2671
2672 % generate a stand-alone HTML file with a visualisation for all states in the list
2673
2674 generate_visb_html(StateIds,File,Options) :-
2675 safe_open_file(File,write,Stream,[encoding(utf8)]),
2676 generate_html_to_stream(StateIds,Stream,[html_file/File|Options]),
2677 close(Stream).
2678
2679 generate_visb_html_to_codes(StateIds,Options,Codes) :-
2680 with_open_stream_to_codes(
2681 generate_html_to_stream(StateIds,Stream,Options),
2682 Stream,Codes,[]).
2683
2684
2685 % generate an HTML file to visualise the given StateId
2686 generate_html_to_stream(StateIds,Stream,Options) :-
2687 set_id_namespace_prefix_for_states(StateIds,Options),
2688 write_visb_template('visb_template_header.html',Stream),
2689 (member(show_svg_downloads,Options) -> write_visb_template('visb_template_svg_downloads.html',Stream) ; true),
2690 format(Stream,' <script>~n',[]),
2691 retractall(js_generated_function(_)),
2692 length(StateIds,Len),
2693 format(Stream,' const differences = [~n',[]),
2694 maplist(gen_visb_visualise_function(Stream,Options,Len,StateIds),StateIds),
2695 write_visb_template('visb_template_replayTrace.html',Stream),
2696 format(Stream,' </script>~n~n',[]),
2697 gen_registerHovers_scipt(Stream,Options),
2698 write_visb_template('visb_template_middle.html',Stream),
2699 (no_svg_available
2700 -> format(Stream,' <button type="button" class="collapsible-style">No SVG Visualisation Available</button>~n',[])
2701 ; % generate SVG section
2702 (member(no_header,Options) -> true
2703 ; format(Stream,' <button type="button" class="collapsible collapsible-style active">SVG Visualisation</button>~n',[])
2704 ),
2705 format(Stream,' <div style="position: relative;">~n',[]), % container for SVG download buttons
2706 format(Stream,' <div text-align="left" id="visb_svg_outer_container" class="svg-outer-container">~n',[]),
2707 format(Stream,' <div id="visb_svg_inner_container" class="svg-inner-container">~n',[]),
2708 %format(Stream,' <fieldset> <legend>Visualisation:</legend>~n',[]), % comment in to draw a border
2709 (StateIds = [SingleStateId] -> GenForState=SingleStateId ; GenForState=root),
2710 copy_svg_file_and_gen_objects(Stream,GenForState,_SVGinlined),
2711 % TO DO: avoid creating JS code below if _SVGinlined
2712 %format(Stream,' </fieldset>~n',[]),
2713 format(Stream,' </div>~n',[]), % inner container
2714 format(Stream,' </div>~n',[]), % outer container
2715 format(Stream,' <button id="btnResetScale" class="visualisation-button" onclick="resetScale()">Reset View</button>~n',[]),
2716 (member(show_svg_downloads,Options) ->
2717 format(Stream,' <button onclick="downloadSVG()">Save SVG (Current State)</button>~n',[]),
2718 format(Stream,' <button onclick="downloadAllSVGs()">Save all SVGs</button>~n',[])
2719 ; true),
2720 format(Stream,' </div>~n',[]) % container for SVG download buttons
2721 ),
2722 (Len>1, memberchk(show_sequence_chart,Options) % don't export PlantUML for list of state IDs (sequence chart depends on trace)
2723 -> (create_temp_puml_files(Len,Files),
2724 uml_generator:write_uml_sequence_chart_all_states(Files), % generate .puml files
2725 tools_commands:gen_plantuml_output(Files,svg,[]) % generate .svg files
2726 -> format(Stream,' <button type="button" class="collapsible collapsible-style active">Sequence Chart Visualisation</button>~n',[]),
2727 format(Stream,' <div class="seq-chart-container">~n',[]),
2728 reverse(Files,RFiles),
2729 write_temp_puml_outputs(1,RFiles,Stream), % write SVG contents to HTML
2730 format(Stream,' </div>~n',[])
2731 ; add_warning(visb_visualiser,'HTML export: did not write the Sequence Diagram Visualisation due to an error in the PlantUML call.'),
2732 format(Stream,' <button type="button" class="collapsible-style">No Sequence Chart Visualisation Available</button>~n',[])
2733 )
2734 ; true),
2735 (Len>1
2736 -> %format(Stream,'~n<h3>Run Trace</h3>~n',[]),
2737 format(Stream,' <button type="button" class="collapsible-style">Replay Trace</button>~n',[]),
2738 format(Stream,' <div class="coll-content-vis">~n',[]),
2739 format(Stream,' <button id="btnPrev" onclick="backStep()" title="Go back one step">« Back</button>~n',[]),
2740 format(Stream,' <button id="btnNext" onclick="forwardStep()" title="Go forward one step">Forward »</button>~n',[]),
2741 format(Stream,' <button onclick="runAll(10)" title="Fast replay of entire trace">Run Trace (10 ms delay)</button>~n',[]),
2742 format(Stream,' <button onclick="runAll(500)" title="Slow replay of entire trace">Run Trace (500 ms delay)</button>~n',[]),
2743 format(Stream,' <button onclick="runAll(parseInt(delayInput.value))" title="Custom replay of entire trace">Run Trace with Delay (ms):</button>~n',[]),
2744 format(Stream,' <input id="delayInput" type="number" value="1000" min="0" step="100" onkeydown="if(event.key===\'Enter\') runAll(parseInt(this.value))">~n',[]),
2745 % We could decide to provide an option/preference for generating the visb_debug_messages field:
2746 % (check that ProB2-UI also generates this text field)
2747 format(Stream,' <br><label id="visb_debug_messages" class="visb-messages"> </label>~n',[]),
2748 format(Stream,' </div>~n',[]),
2749 format(Stream,' <progress id="trace_meter" min="0" max="~w" value="0"></progress>~n',[Len]) % progress of trace replay; note <meter> element also works
2750 ; true
2751 ),
2752 % generate a table with variables, constants, ...
2753 gen_state_table(Stream,Options,StateIds),
2754 gen_source_code_section(Stream,Options),
2755 % generate a table with the saved trace steps:
2756 (Len>1 -> gen_trace_table(Stream,StateIds) ; true),
2757 write_version_info(Stream,Options),
2758 (last(StateIds,_)
2759 -> format(Stream,' <script> replayStep(~w); </script>~n',[Len])
2760 % show the visualisation of the last state by default
2761 ; true % trace is empty, there is no last item
2762 ),
2763 write_visb_template('visb_template_footer.html',Stream),
2764 clear_id_namespace_prefix.
2765
2766 create_temp_puml_files(Len,[]) :- Len<1, !.
2767 create_temp_puml_files(Len,[Path|T]) :-
2768 system_call:get_temporary_filename('for_html.puml',Path),
2769 NewLen is Len-1,
2770 create_temp_puml_files(NewLen,T).
2771
2772 :- use_module(probsrc(tools_io),[write_file_to_stream/2]).
2773 write_temp_puml_outputs(_,[],_).
2774 write_temp_puml_outputs(Nr,[File|T],Stream) :-
2775 tools:split_filename(File,FileRoot,_Ext),
2776 ajoin([FileRoot,'.svg'],SvgFile),
2777 format(Stream,' <div id="seq_chart_~w" style="display:none">~n',[Nr]), % container for seq. charts
2778 write_file_to_stream(SvgFile,Stream),
2779 format(Stream,' </div>~n',[]), % container for seq. charts
2780 NNr is Nr+1,
2781 write_temp_puml_outputs(NNr,T,Stream).
2782
2783 % -----------------
2784
2785 :- use_module(library(system),[ datime/1]).
2786 :- use_module(probsrc(tools_strings),[number_codes_min_length/3, format_modified_info/2]).
2787 :- use_module(probsrc(tools),[gen_relative_path/3]).
2788 :- use_module(probsrc(version),[version_str/1]).
2789 :- use_module(probsrc(specfile),[currently_opened_file/1, get_internal_representation/1]).
2790 write_version_info(_,Options) :-
2791 member(no_version_info,Options),!.
2792 write_version_info(Stream,Options) :-
2793 version_str(Str),datime(datime(Yr,Mon,Day,Hr,Min,_Sec)),
2794 number_codes_min_length(Min,2,MC),
2795 format(Stream,' <button type="button" class="collapsible-style" title="Information about ProB and model">Info</button>~n',[]),
2796 format(Stream,'<div class="coll-content-vis visb-messages">~n',[]),
2797 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]),
2798 (currently_opened_file(File)
2799 -> (File=package(Type) ->
2800 format(Stream,'<br>Main specification package: ~w~n',[Type])
2801 ; atom(File), get_relative_path(File,Options,Suffix) ->
2802 format(Stream,'<br>Main specification file: ~w',[Suffix]),
2803 format_file_info(Stream,File)
2804 ; format(Stream,'<br>Unknown main specification file: ~w~n',[File])
2805 )
2806 ; true),
2807 (b_machine_name(MainName)
2808 -> format(Stream,'<br>Main specification name: ~w~n',[MainName]) ; true),
2809 (visb_file_loaded(JSONFile,_,ModLocTime),
2810 JSONFile \= ''
2811 -> get_relative_path(JSONFile,Options,JSuffix),
2812 format(Stream,'<br>Main VisB JSON file: ~w',[JSuffix]),
2813 format_modified_info(Stream,ModLocTime),
2814 (get_non_empty_svg_file(SVGFile,ModLocTime2)
2815 -> get_relative_path(SVGFile,Options,SSuffix),
2816 format(Stream,'<br>VisB SVG file: ~w',[SSuffix]),
2817 format_modified_info(Stream,ModLocTime2)
2818 ; true
2819 )
2820 ; true).
2821
2822 get_non_empty_svg_file(SVGFile,ModLocTime2) :-
2823 visb_svg_file(RelFile,SVGFile,_,_,ModLocTime2),
2824 RelFile \= ''.
2825
2826 format_file_info(Stream,File) :-
2827 catch(file_property(File, modify_localtime, ModLocTime),
2828 E,
2829 (add_message(visb_visualiser,'Could not obtain modification time for file: ',E), fail)),
2830 !,
2831 format_modified_info(Stream,ModLocTime).
2832 format_file_info(Stream,_) :- nl(Stream).
2833
2834
2835 get_relative_path(File,Options,RelPath) :-
2836 ? member(html_file/HF,Options),
2837 absolute_file_name(File,AF,[]),
2838 absolute_file_name(HF,AHF,[]),
2839 !,
2840 gen_relative_path(AF,AHF,RelPath). % only print relative information
2841 get_relative_path(File,_,File).
2842
2843
2844 % -----------------
2845
2846 % gen a table with all the individual steps of the trace
2847 gen_trace_table(Stream,StateIds) :-
2848 length(StateIds,Len),
2849 %format(Stream,'~n<h3>Trace (length=~w)</h3>~n',[Len]),
2850 format(Stream,' <button type="button" class="collapsible collapsible-style active">Trace (length=~w)</button>~n',[Len]),
2851 format(Stream,'<div class="coll-content-vis">~n',[]),
2852 ? (member(Obj,StateIds), get_state_and_action(Obj,_,_,DescStr), DescStr \= ''
2853 -> Opt=with_description ; Opt=no_description),
2854 gen_trace_table2(Stream,StateIds,Opt).
2855
2856 gen_trace_table2(Stream,StateIds,no_description) :-
2857 format(Stream,' <table> <tr> <th>Nr</th> <th>Event</th> <th>Target State ID</th> </tr>~n',[]),
2858 ? nth1(Nr,StateIds,Obj),
2859 get_state_and_action(Obj,StateId,ActionStr,_),
2860 ((visited_state_corresponds_to_initialised_b_machine(StateId) ; xtl_mode) % allow onclick to all rows in xtl_mode
2861 -> (invariant_violated(StateId) -> BtnStyle='style="background-color:rgb(255,179,179);border-radius:6px" ' ; BtnStyle=''),
2862 format(Stream,'~n <tr id="row~w" onclick="replayStep(~w)"><td>~w</td><td style="cursor:pointer">~w</td><td><button ~wonclick="replayStep(~w);">State ~w</button></td></tr>~n',
2863 [Nr,Nr,Nr,ActionStr,BtnStyle,Nr,StateId])
2864 ; format(Stream,'~n <tr id="row~w"><td>~w</td><td style="cursor:not-allowed">~w</td><td>State ~w</td></tr>~n',
2865 [Nr,Nr,ActionStr,StateId])
2866 ),
2867 fail.
2868 gen_trace_table2(Stream,StateIds,with_description) :-
2869 format(Stream,' <table> <tr> <th>Nr</th> <th>Event</th> <th>Description</th> <th>Target State ID</th> </tr>~n',[]),
2870 ? nth1(Nr,StateIds,Obj),
2871 get_state_and_action(Obj,StateId,ActionStr,DescStr),
2872 atom_codes(ActionStr,ActionCodes),html_escape_codes(ActionCodes,EAS),
2873 atom_codes(DescStr,DescCodes),html_escape_codes(DescCodes,EDS),
2874 ((visited_state_corresponds_to_initialised_b_machine(StateId) ; xtl_mode) % allow onclick to all rows in xtl_mode
2875 -> (invariant_violated(StateId) -> BtnStyle='style="background-color:rgb(255,179,179);border-radius:6px" ' ; BtnStyle=''),
2876 format(Stream,'~n <tr id="row~w" onclick="replayStep(~w)"><td>~w</td><td style="cursor:pointer">~s</td><td>~s</td><td><button ~wonclick="replayStep(~w);">State ~w</button></td></tr>~n',
2877 [Nr,Nr,Nr,EAS,EDS,BtnStyle, Nr,StateId])
2878 ; 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',
2879 [Nr,Nr,EAS,EDS,StateId])
2880 ),
2881 fail.
2882 gen_trace_table2(Stream,_,_) :-
2883 format(Stream,' </table>~n </div>~n',[]).
2884
2885
2886 % utility to allow passing information about name of event/operation/action leading to state
2887 get_state_and_action(change_to_state_via_action(StateId,ActionStr,DescStr),StateId,ActionStr,DescStr) :- !.
2888 get_state_and_action(StateId,StateId,'','').
2889
2890 % -----------------
2891
2892 % inline provided svg file into html file:
2893 % second argument is either root or a particular state id for which the SVG file is to be created
2894 % the last argument is static_svg_inlined if all SVG objects were "inlined" into a single
2895 % SVG object (rather than via JavaScript functions to create the objects)
2896 copy_svg_file_and_gen_objects(Stream,_,static_svg_not_inlined) :- visb_svg_file(_,File,_,_,_), file_exists(File),
2897 !,
2898 write_file_to_stream(File,Stream),
2899 ( get_visb_contents_def(Contents,DefName,DefPos,static_svg_not_inlined),
2900 ajoin(['Copying ',DefName,' *after* SVG file: '],Msg),
2901 add_message(visb_visualiser,Msg,File,DefPos),
2902 format(Stream,'~w~n',[Contents]),
2903 fail
2904 ; true
2905 ),
2906 gen_new_svg_objects(Stream).
2907 copy_svg_file_and_gen_objects(_,_,_) :-
2908 visb_svg_file(File,AFile,_,Pos,_),
2909 File \= '',
2910 add_error(visb_visualiser,'The specified VisB SVG file does not exist:',AFile,Pos),
2911 fail.
2912 copy_svg_file_and_gen_objects(Stream,SingleStateId,static_svg_inlined) :- % copy an empty SVG stub
2913 visb_file_loaded(_,_,_),!,
2914 write_default_svg_contents(Stream,inline_objects(SingleStateId)).
2915 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,...
2916
2917 % TODO: precompile and always assert as visb_special_definition (we could also evaluate it; could use template strings):
2918 get_visb_contents_def(Contents,DefName,DefPos,InlineObjects) :-
2919 ? get_and_eval_special_definition('VISB_SVG_CONTENTS',DefName,visb_contents,DefPos,ResValue,InlineObjects),
2920 b_value_to_string(ResValue,Contents).
2921 get_visb_contents_def(Contents,default_svg_contents,unknown,_InlineObjects) :-
2922 % default content, for VISB_CLICK_META_INFOS'jsVars
2923 Contents = '<script>let visb_vars = {};</script>'.
2924
2925 % get a definition either from B DEFINITIONS section, or if not present from the VisB JSON special definition list
2926 get_and_eval_special_definition(Prefix,DefName,JSONBackup,DefPos,ResValue,InlineObjects) :-
2927 (b_sorted_b_definition_prefixed(expression,Prefix,DefName,DefPos),
2928 ? b_get_typed_definition(DefName,[variables_and_additional_defs],TBody)
2929 ;
2930 visb_special_definition(JSONBackup,DefName,_Type,TBody,_Class,DefPos)
2931 ),
2932 % TODO: warn if we use static SVG
2933 ? get_typed_static_definition_with_constants_state(DefName,TBody,
2934 Body,DefPos,ConstantsState,InlineObjects,no_separation),
2935 evaluate_visb_formula(Body,DefName,'',ConstantsState,ResValue,DefPos).
2936
2937 write_default_svg_contents(Stream,InlineObjects) :-
2938 (visb_empty_svg_box_height_width(H,W,ViewBox) -> true ; H=400, W=400, ViewBox=''),
2939 format(Stream,'<svg xmlns=\"http://www.w3.org/2000/svg\"~n',[]),
2940 (ViewBox=''
2941 -> format(Stream,' width="~w" height="~w" viewBox="0 0 ~w ~w" >~n',[W,H,W,H])
2942 ; format(Stream,' width="~w" height="~w" viewBox="~w" >~n',[W,H,ViewBox])
2943 ),
2944 ? ( get_visb_contents_def(Contents,_,_,InlineObjects),
2945 format(Stream,'~w~n',[Contents]),
2946 fail
2947 ; true),
2948 (InlineObjects=inline_objects(StateID) -> inline_new_svg_objects(Stream,StateID) ; true),
2949 format(Stream,'</svg>~n',[]).
2950
2951 % get SVG file contents in case no SVG file is provided by user
2952 get_visb_default_svg_file_contents(Codes) :-
2953 with_open_stream_to_codes(
2954 write_default_svg_contents(Stream,inline_objects(root)),
2955 % allow inlining for groups and title children in ProB2-UI
2956 Stream,
2957 Codes, []).
2958
2959 % -----------------
2960
2961 % create a script to add all additional SVG objects
2962 gen_new_svg_objects(_) :- \+ visb_svg_object(_,_,_,_,_),!.
2963 gen_new_svg_objects(Stream) :-
2964 format(Stream, '<script>~n',[]),
2965 format(Stream, ' const svg = document.querySelector("svg");~n',[]),
2966 format(Stream, ' const svgns = "http://www.w3.org/2000/svg";~n',[]),
2967 (gen_new_svg_object(Stream,svg_root,_),fail ; true),
2968 format(Stream, '</script>~n',[]).
2969
2970 % generate JS script to create an individual new object
2971 gen_new_svg_object(Stream,ParentID,SVGID) :-
2972 visb_svg_object(SVGID,SVG_Class,AttrList,_,_Pos),
2973 (ParentID=svg_root
2974 -> (visb_svg_child(SVGID,RealParentID) % only generate root svg objects that have no parents
2975 -> visb_svg_child_of_object_from_svg_file(SVGID) % unless the parent will not be created here in this loop
2976 ; RealParentID=ParentID
2977 )
2978 ; RealParentID=ParentID),
2979 add_svg_id_prefix(SVGID,SVGID2),
2980 format(Stream,' if(document.getElementById("~w") == null) {~n',[SVGID2]),
2981 format(Stream,' var new___obj = document.createElementNS(svgns,"~w");~n',[SVG_Class]),
2982 format(Stream,' new___obj.setAttribute("~w","~w");~n',[id,SVGID2]),
2983 maplist(gen_new_svg_attr(Stream,SVGID2),AttrList),
2984 (RealParentID \= svg_root
2985 -> format(Stream,' document.getElementById("~w").appendChild(new___obj);~n',[RealParentID])
2986 ; format(Stream,' svg.appendChild(new___obj);~n',[])
2987 ),
2988 format(Stream,' }~n',[]),
2989 (visb_svg_parent(SVGID,ChildID), % we can now generate the children
2990 gen_new_svg_object(Stream,SVGID,ChildID),
2991 fail
2992 ; true).
2993
2994 gen_new_svg_attr(Stream,_SVGID,svg_attribute(text,Val)) :- !,
2995 format(Stream,' new___obj.textContent = "~w";~n',[Val]).
2996 gen_new_svg_attr(Stream,_SVGID,svg_attribute(Attr,Val)) :-
2997 format(Stream,' new___obj.setAttribute("~w","~w");~n',[Attr,Val]).
2998
2999 % instead of creating a script to create new SVG objects,
3000 % create an inlined textual XML representation of the objects
3001 % this can be used to obtain a static SVG file which can be modified in an editor
3002 % and then later used instead of the VISB_SVG_OBJECTS definitions
3003 inline_new_svg_objects(Stream,StateId) :-
3004 get_dynamic_svgid_attributes_for_state(StateId,DynUpdateList), % compute updates only once
3005 ? visb_svg_object(SVGID,_,_,_,_), % lookup static SVG object
3006 \+ visb_svg_child(SVGID,_), % children will be created in the scope of their parent
3007 inline_new_svg_object(Stream,StateId,DynUpdateList,0,unknown,SVGID),
3008 fail.
3009 inline_new_svg_objects(_,_).
3010
3011 inline_new_svg_object(Stream,StateId,DynUpdateList,IndentLevel,ParentPos,SVGID) :-
3012 (visb_svg_object(SVGID,SVG_Class,StaticAttrList,_,Pos) -> true % lookup static SVG object
3013 ; add_warning(visb_visualiser,'Unknown SVG child object: ',SVGID,ParentPos),fail
3014 ),
3015 add_svg_id_prefix(SVGID,SVGID2), % for Jupyter
3016 indent_ws(Stream,IndentLevel),
3017 format(Stream,' <~w id="~w"',[SVG_Class,SVGID2]),
3018 (member(svgid_updates(SVGID,DynAttrList),DynUpdateList) % TODO: use avl_fetch
3019 -> override_attributes(StaticAttrList,DynAttrList,AttrList)
3020 ; AttrList=StaticAttrList),
3021 maplist(format_new_svg_attr(Stream,SVGID,Pos,TextContent),AttrList),
3022 (TextContent=''
3023 -> EscapedTextContent="" % set Text variable to empty if unbound
3024 ; do_not_escape_text_for_class(SVG_Class) -> atom_codes(TextContent,EscapedTextContent)
3025 ; atom_codes(TextContent,TCC), html_escape_codes(TCC,EscapedTextContent)),
3026 format(Stream,'>~s',[EscapedTextContent]), % Note: this text is not inside quotes, we need HTML escape
3027 IL1 is IndentLevel+1,
3028 ? ( visb_svg_parent(SVGID,Child),
3029 nl(Stream),
3030 inline_new_svg_object(Stream,StateId,DynUpdateList,IL1,Pos,Child),
3031 fail
3032 ; true),
3033 format(Stream,'</~w>~n',[SVG_Class]), % end marker
3034 fail.
3035 inline_new_svg_object(_,_,_,_,_,_).
3036
3037 % for foreignObjects the text may contain HTML tags which should not be escaped:
3038 do_not_escape_text_for_class(foreignObject).
3039 do_not_escape_text_for_class(script). % otherwise " quotes will be escaped to "
3040
3041 indent_ws(_,X) :- X<1,!.
3042 indent_ws(Stream,X) :- write(Stream,' '), X1 is X-1, indent_ws(Stream,X1).
3043
3044 % combinde svg_attribute/2 terms from two sorted lists, giving precedence to second list
3045 override_attributes([],L,R) :- !, R=L.
3046 override_attributes(L,[],R) :- !, R=L.
3047 override_attributes([svg_attribute(Attr1,Val1)|T1],[svg_attribute(Attr2,Val2)|T2],[svg_attribute(Attr3,Val3)|T3]) :-
3048 (Attr1=Attr2
3049 -> Attr3=Attr1, Val3=Val2, % dynamic value Val2 takes precedence
3050 override_attributes(T1,T2,T3)
3051 ; Attr1 @< Attr2 -> Attr3=Attr1, Val3=Val1, override_attributes(T1,[svg_attribute(Attr2,Val2)|T2],T3)
3052 ; Attr3=Attr2, Val3=Val2, override_attributes([svg_attribute(Attr1,Val1)|T1],T2,T3)
3053 ).
3054
3055 % get dynamic svg_attribute/2 list for a given state and SVG ID
3056 get_dynamic_svgid_attributes_for_state(root,List) :- !, List=[].
3057 get_dynamic_svgid_attributes_for_state(StateId,UpdateList) :-
3058 get_visb_attributes_for_state(StateId,List),
3059 sort(List,SList),
3060 group_set_attr(SList,'$$UNKNOWN$$',_,UpdateList).
3061
3062 group_set_attr([],_,[],[]).
3063 group_set_attr([set_attr(SvgID,Attr,Val)|T],SvgID,[svg_attribute(Attr,Val)|T1],T2) :- !,
3064 group_set_attr(T,SvgID,T1,T2).
3065 group_set_attr([set_attr(SvgID,Attr,Val)|T],_OldID,[],[svgid_updates(SvgID,L)|T2]) :- % a new SVGId is encountered
3066 group_set_attr([set_attr(SvgID,Attr,Val)|T],SvgID,L,T2).
3067
3068 % print svg attribute and extract text attribute
3069 format_new_svg_attr(Stream,SVGID,Pos,TextContent,svg_attribute(Attr,Val)) :- % TODO: text content
3070 (Attr=text
3071 -> (TextContent=Val -> true % TextContent is initially a variable and can be unified once
3072 ; add_warning(inline_new_svg_objects,'Multiple text attributes for: ',SVGID,Pos),
3073 add_debug_message(inline_new_svg_objects,' * Using text 1: ',TextContent),
3074 add_debug_message(inline_new_svg_objects,' * Ignoring text 2: ',Val)
3075 )
3076 ; number(Val) ->
3077 format(Stream,' ~w="~w"',[Attr,Val])
3078 ; escape_value_to_codes_for_js(Val,ECodes) ->
3079 format(Stream,' ~w="~s"',[Attr,ECodes])
3080 ; compound(Val), functor(Val,F,N) ->
3081 ajoin(['Cannot escape ',Attr,' *compound* ',F,'/',N,' value for ', SVGID,': '],Msg),
3082 add_error(visb_visualiser,Msg,Val,Pos),
3083 format(Stream,' ~w="~w"',[Attr,Val])
3084 ; ajoin(['Cannot escape ',Attr,' value for ', SVGID,': '],Msg),
3085 add_error(visb_visualiser,Msg,Val,Pos),
3086 format(Stream,' ~w="~w"',[Attr,Val])
3087 ).
3088
3089
3090 :- dynamic id_namespace_prefix/1.
3091 % prefix that can be useful for Jupyter notebooks so that for each state we have a different namespace
3092 % can also be useful for exporting a trace into a single HTML
3093 % TODO: does not work with JSON and SVG files
3094
3095 :- use_module(probsrc(gensym),[gensym/2]).
3096 set_id_namespace_prefix_for_states(_,Options) :-
3097 member(id_namespace_prefix(Pre),Options),!,
3098 (Pre = auto
3099 -> gensym('visb',ID), % for Jupyter this relies on the fact the gensym is *not* reset when loading another spec
3100 atom_concat(ID,'.',Prefix)
3101 ; Prefix=Pre
3102 ), set_id_namespace_prefix(Prefix).
3103 set_id_namespace_prefix_for_states(_,_).
3104
3105 set_id_namespace_prefix(Prefix) :- clear_id_namespace_prefix,
3106 assert(id_namespace_prefix(Prefix)).
3107 clear_id_namespace_prefix :- retractall(id_namespace_prefix(_)).
3108
3109 % add a namespace prefix to an SVG ID
3110 add_svg_id_prefix(SvgID,Res) :- id_namespace_prefix(Prefix),!,
3111 % option where we prefix all Ids with a namespace for Jupyter to combine multiple SVGs in single HTML page
3112 atom_concat(Prefix,SvgID,Res).
3113 add_svg_id_prefix(SvgID,SvgID).
3114
3115 % only add for known objects
3116 opt_add_svg_id_prefix(SvgID,Res) :- id_namespace_prefix(Prefix),
3117 visb_svg_object(SvgID,_,_,_,_),!, % only add prefix for SVG objects we know about (that were created by VisB)
3118 % option where we prefix all Ids with a namespace for Jupyter to combine multiple SVGs in single HTML page
3119 atom_concat(Prefix,SvgID,Res).
3120 opt_add_svg_id_prefix(SvgID,SvgID).
3121
3122 % -----------------
3123
3124 :- dynamic js_generated_function/1.
3125 :- dynamic last_attribute_values/3.
3126
3127 % define a visualise JS function to set the attributes for the given StateId
3128 gen_visb_visualise_function(Stream,Options,Len,StateIds,Obj) :-
3129 get_state_and_action(Obj,StateId,ActionStr,DescStr),
3130 ? nth1(Nr,StateIds,Obj),
3131 \+ js_generated_function(Nr), !,
3132 assertz(js_generated_function(Nr)),
3133 (Nr > 1 ->
3134 PrevNr is Nr-1, nth1(PrevNr,StateIds,PrevObj), get_state_and_action(PrevObj,PrevStateId,_,_)
3135 ; PrevStateId = -1),
3136 visb_visualise_function_aux(Stream,Options,Len,StateId,PrevStateId,Nr,ActionStr,DescStr),
3137 (Nr == Len ->
3138 retractall(last_attribute_values(_,_,_)),
3139 format(Stream,' ]~n',[])
3140 ; true).
3141 gen_visb_visualise_function(_,_,_,_,_).
3142
3143 :- use_module(extrasrc(bvisual2), [bv_get_top_level/1,bv_get_value_unlimited/3]).
3144 :- use_module(probsrc(tools),[string_escape/2]).
3145 visb_visualise_function_aux(Stream,_,Len,StateId,_,Nr,ActionStr,DescStr) :-
3146 format(Stream,' [~n',[]),
3147 (Len>1 -> format(Stream,' {id: "trace_meter", attr: "value", val: "~w"},~n',[Nr]) ; true),
3148 (escape_value_to_codes_for_js(ActionStr,EAS), escape_value_to_codes_for_js(DescStr,EDS) ->
3149 % was only string_escape before; however, this turns e.g. |-> into ↦ which we don't want (we are in JS part here)
3150 format(Stream,' {id: "visb_debug_messages", attr: "text", val: "Step ~w/~w, State ID: ~w, Event: ~s ~s"},~n',[Nr,Len,StateId,EAS,EDS])
3151 ; string_escape(ActionStr,SEAS), string_escape(DescStr,SEDS), % fallback
3152 format(Stream,' {id: "visb_debug_messages", attr: "text", val: "Step ~w/~w, State ID: ~w, Event: ~w ~w"},~n',[Nr,Len,StateId,SEAS,SEDS])
3153 ),
3154 ? get_change_attribute_for_state(StateId,SvgID,SvgAttribute,Value),
3155 \+ last_attribute_values(SvgID,SvgAttribute,Value),
3156 retractall(last_attribute_values(SvgID,SvgAttribute,_)),
3157 assertz(last_attribute_values(SvgID,SvgAttribute,Value)),
3158 opt_add_svg_id_prefix(SvgID,SvgID2),
3159 (escape_value_to_codes_for_js(Value,ECodes)
3160 -> format(Stream,' {id: "~w", attr: "~w", val: "~s"},~n',[SvgID2,SvgAttribute,ECodes])
3161 ; format(Stream,' {id: "~w", attr: "~w", val: "~w"},~n',[SvgID2,SvgAttribute,Value])
3162 ),
3163 fail.
3164 visb_visualise_function_aux(Stream,Options,Len,StateId,PrevStateId,_,_,_) :-
3165 b_or_z_mode,
3166 member(show_variables(VarList),Options),
3167
3168 visited_expression(StateId,State),
3169 (visited_expression(PrevStateId,PrevState) -> true ; PrevState=root),
3170
3171 show_var_in_visb(VarList,ID),
3172 ? get_state_value_change(StateId,State,ID,Options,ResValCodes),
3173
3174 % current value:
3175 ajoin(['bVar_',ID],SvgID),
3176 change_svg_attribute_differences_aux(Stream,SvgID,'text',ResValCodes),
3177
3178 Len > 1, % don't add previous value and change markers for state-only HTML
3179 (state_corresponds_to_fully_setup_b_machine(PrevState,_), % don't show prev values before initialisation
3180 ? get_state_value_change(PrevStateId,PrevState,ID,Options,PrevResValCodes)
3181 -> true
3182 ; PrevResValCodes = "?"),
3183
3184 % mark row if value has changed in the last step
3185 ajoin(['row_bVar_',ID],SvgRowID),
3186 (ResValCodes = PrevResValCodes -> RowColor = white; RowColor = '#fffacd'),
3187 change_svg_attribute_differences_aux(Stream,SvgRowID,'bgcolor',RowColor),
3188
3189 % previous value:
3190 ajoin(['bVarPrev_',ID],SvgPrevID),
3191 change_svg_attribute_differences_aux(Stream,SvgPrevID,'text',PrevResValCodes),
3192
3193 fail.
3194 visb_visualise_function_aux(Stream,_Options,Len,StateId,PrevStateId,_,_,_) :-
3195 xtl_mode,
3196
3197 bv_get_top_level(IDs),
3198 member(ID,IDs),
3199 (bv_get_value_unlimited(ID,StateId,v(Val))
3200 -> atom_codes(Val,ResValCodes)
3201 ; ResValCodes = ""),
3202
3203 % current value:
3204 ajoin(['bVar_',ID],SvgID),
3205 change_svg_attribute_differences_aux(Stream,SvgID,'text',ResValCodes),
3206
3207 Len > 1, % don't add previous value and change markers for state-only HTML
3208 (PrevStateId \= root,
3209 bv_get_value_unlimited(ID,PrevStateId,v(PrevVal))
3210 -> atom_codes(PrevVal,PrevResValCodes)
3211 ; PrevResValCodes = ""),
3212
3213 % mark row if value has changed in the last step
3214 ajoin(['row_bVar_',ID],SvgRowID),
3215 (ResValCodes = PrevResValCodes -> RowColor = white; RowColor = '#fffacd'),
3216 change_svg_attribute_differences_aux(Stream,SvgRowID,'bgcolor',RowColor),
3217
3218 % previous value:
3219 ajoin(['bVarPrev_',ID],SvgPrevID),
3220 change_svg_attribute_differences_aux(Stream,SvgPrevID,'text',PrevResValCodes),
3221
3222 fail.
3223 visb_visualise_function_aux(Stream,Options,_,StateId,_,_,_,_) :-
3224 member(show_events(OpList),Options),
3225 get_state_value_enabled_operation_status(StateId,OpID,Enabled,ResValCodes,TransStr),
3226 show_var_in_visb(OpList,OpID),
3227 ajoin(['bOperation_',OpID],SvgID),
3228 \+ last_attribute_values(SvgID,'text',ResValCodes),
3229 retractall(last_attribute_values(SvgID,'text',_)),
3230 assertz(last_attribute_values(SvgID,'text',ResValCodes)),
3231 format(Stream,' {id: "~w", attr: "text", val: "~s"},~n',[SvgID,ResValCodes]),
3232 (Enabled=true -> BGCol=white ; BGCol='#f1f1f1'),
3233 format(Stream,' {id: "row_~w", attr: "bgcolor", val: "~s"},~n',[SvgID,BGCol]),
3234 escape_value_to_codes_for_js(TransStr,ETS),
3235 format(Stream,' {id: "name_~w", attr: "text", val: "~s"},~n',[SvgID,ETS]),
3236 % TO DO: highlight next event in trace, but then function needs one more parameter
3237 fail.
3238 visb_visualise_function_aux(Stream,Options,Len,_,_,Nr,_,_) :-
3239 (Len>1, member(show_sequence_chart,Options)
3240 -> format(Stream,' {id: "seq_chart_~w", attr: "style", val: "display:block"},~n',[Nr]),
3241 (Nr>1
3242 -> PNr is Nr-1, format(Stream,' {id: "seq_chart_~w", attr: "style", val: "display:none"},~n',[PNr])
3243 ; gen_seq_charts_setup(Stream,Len))), % all sequence charts except the first should be invisible
3244 fail.
3245 visb_visualise_function_aux(Stream,_,Len,_,_,Nr,_,_) :-
3246 Nr == Len ->
3247 format(Stream,' ]~n',[])
3248 ; format(Stream,' ],~n',[]).
3249
3250 gen_seq_charts_setup(_,Len) :- Len<2, !.
3251 gen_seq_charts_setup(Stream,Len) :-
3252 format(Stream,' {id: "seq_chart_~w", attr: "style", val: "display:none"},~n',[Len]),
3253 NLen is Len-1,
3254 gen_seq_charts_setup(Stream,NLen).
3255
3256 escape_value_to_codes_for_js(Atom,ECodes) :- atom(Atom),
3257 atom_codes(Atom,Codes), b_string_escape_codes(Codes,ECodes).
3258
3259 change_svg_attribute_differences_aux(Stream,ID,Attr,ValueCodes) :-
3260 (last_attribute_values(ID,Attr,ValueCodes)
3261 -> true
3262 ; retractall(last_attribute_values(ID,Attr,_)),
3263 assertz(last_attribute_values(ID,Attr,ValueCodes)),
3264 format(Stream,' {id: "~w", attr: "~w", val: "~s"},~n',[ID,Attr,ValueCodes])
3265 ).
3266
3267
3268
3269 % generate JS script to register hovers
3270 ?gen_registerHovers_scipt(Stream,Options) :- \+ visb_has_hovers(_),
3271 nonmember(debugging_hovers,Options),
3272 !, % no hover exists
3273 format(Stream,' <script> function registerHovers() {} </script>~n',[]).
3274 gen_registerHovers_scipt(Stream,Options) :-
3275 (member(debugging_hovers,Options) -> GenDebug=true ; GenDebug=false), % gen debugging hovers
3276 % Jquery is no longer required:
3277 %format(Stream,' <script src="https://ajax.googleapis.com/ajax/libs/jquery/3.6.0/jquery.min.js"></script>~n',[]),
3278 format(Stream,' <script>~n',[]),
3279 format(Stream,' function registerHovers() {~n',[]),
3280 format(Stream,' var obj;~n',[]),
3281 ? visb_has_hovers(SVGID), % only generate hover function if necessary; TODO: examine other IDs for GenDebug
3282 opt_add_svg_id_prefix(SVGID,SVGID2),
3283 format(Stream,' obj = document.getElementById("~w");~n',[SVGID2]),
3284 format(Stream,' obj.onmouseover = function(ev){~n',[]),
3285 ? (visb_hover(SVGID,ID,Attr,EnterVal,_,_),
3286 opt_add_svg_id_prefix(ID,ID2),
3287 (GenDebug=false -> true
3288 ; format(Stream,' setAttr("~w","~w","SVG ID: ~w")~n',[visb_debug_messages,text,SVGID2])),
3289 format(Stream,' setAttr("~w","~w","~w")~n',[ID2,Attr,EnterVal]), fail ;
3290 format(Stream,' };~n',[])
3291 ),
3292 format(Stream,' obj.onmouseout = function(){~n',[]),
3293 ? (visb_hover(SVGID,ID,Attr,_,LeaveVal,_),
3294 opt_add_svg_id_prefix(ID,ID2),
3295 (GenDebug=false -> true
3296 ; format(Stream,' setAttr("~w","~w","~w")~n',[visb_debug_messages,text,'...'])
3297 ),
3298 format(Stream,' setAttr("~w","~w","~w")~n',[ID2,Attr,LeaveVal]), fail ;
3299 format(Stream,' };~n',[])
3300 ),
3301 fail.
3302 gen_registerHovers_scipt(Stream,_) :-
3303 format(Stream,' }~n </script>~n',[]).
3304
3305
3306 % ----------------------------------
3307
3308 :- use_module(probsrc(translate),[set_unicode_mode/0, unset_unicode_mode/0]).
3309 :- use_module(probsrc(state_space), [get_action_trace_with_limit/2, get_state_id_trace/1]).
3310
3311 generate_visb_html_for_history_with_source(File) :-
3312 generate_visb_html_for_history(File,
3313 [show_constants(all),show_sets(all),show_variables(all),show_events(all),show_invariants,show_source]).
3314 generate_visb_html_for_history_with_vars(File) :-
3315 generate_visb_html_for_history(File,[show_constants(all),show_sets(all),show_variables(all),show_events(all)]).
3316 generate_visb_html_for_history(File) :-
3317 generate_visb_html_for_history(File,[]).
3318 generate_visb_html_for_history(File,Options) :-
3319 start_ms_timer(Timer),
3320 get_state_id_trace(T),
3321 T = [root|StateIds],
3322 set_unicode_mode,
3323 call_cleanup(get_action_trace_with_limit(120,Actions), % TODO: also get description of JSON traces
3324 unset_unicode_mode),
3325 reverse(Actions,FActions),
3326 combine_state_and_actions(StateIds,[root|StateIds],FActions,List),
3327 generate_visb_html(List,File,Options),
3328 stop_ms_walltimer_with_msg(Timer,'exporting history to VisB HTML file: ').
3329
3330 :- use_module(probsrc(specfile),[get_operation_description_for_transition/4]).
3331 combine_state_and_actions([],_,[],[]).
3332 combine_state_and_actions([StateId|TS],[PrevId|TP],[action(ActionStr,ATerm)|TA],
3333 [change_to_state_via_action(StateId,ActionStr,Desc)|TRes]) :-
3334 (get_operation_description_for_transition(PrevId,ATerm,StateId,D) -> Desc=D ; Desc=''),
3335 combine_state_and_actions(TS,TP,TA,TRes).
3336
3337 generate_visb_html_for_current_state(File) :-
3338 generate_visb_html_for_current_state(File,[show_variables(all)]).
3339 generate_visb_html_for_current_state(File,Options) :-
3340 start_ms_timer(Timer),
3341 current_state_id(ID),
3342 generate_visb_html([ID],File,Options),
3343 stop_ms_walltimer_with_msg(Timer,'exporting current state to VisB HTML file: ').
3344 generate_visb_html_codes_for_states(StateIds,Options,Codes) :-
3345 generate_visb_html_to_codes(StateIds,Options,Codes). % write to codes list
3346
3347 % ------------------------------
3348
3349 :- use_module(probsrc(specfile),[b_or_z_mode/0]).
3350 :- use_module(probsrc(bmachine), [b_get_machine_variables/1, b_get_machine_constants/1, b_top_level_operation/1]).
3351 :- use_module(probsrc(bsyntaxtree), [get_texpr_id/2]).
3352 :- use_module(extrasrc(bvisual2), [bv_top_level_set/2]).
3353 :- use_module(probsrc(specfile),[get_specification_description/2]).
3354 :- use_module(probsrc(tools_strings), [atom_tail_to_lower_case/2]).
3355
3356 show_typed_var_in_visb(all,_) :- !.
3357 show_typed_var_in_visb(VarList,b(identifier(ID),_,_)) :- !, show_var_in_visb(VarList,ID).
3358 show_var_in_visb(VarList,ID ) :- (VarList=all -> true ; member(ID,VarList) -> true).
3359
3360 % generate a table for the state (we could use bvisual2)
3361 gen_state_table(Stream,Options,StateIds) :-
3362 b_or_z_mode,
3363 member(show_variables(VarList),Options),
3364 b_get_machine_variables(TypedVars),
3365 % is this useful if Len > 1, but StateIds are not from a trace? (see also below for formulas)
3366 (length(StateIds,Len), Len > 1 -> NOptions = [show_prev_value|Options] ; NOptions = Options),
3367 gen_state_table_aux(Stream,NOptions,'Variables',TypedVars,VarList,[],'Value','bVar_'),fail.
3368 gen_state_table(Stream,Options,StateIds) :-
3369 b_or_z_mode,
3370 member(show_variables(VarList),Options),
3371 b_get_machine_expressions(AExprs,Options), AExprs \= [],
3372 (length(StateIds,Len), Len > 1 -> NOptions = [show_prev_value|Options] ; NOptions = Options),
3373 gen_state_table_aux(Stream,NOptions,'Formulas',AExprs,VarList,[],'Value','bVar_'),fail.
3374 gen_state_table(Stream,Options,StateIds) :-
3375 b_or_z_mode,
3376 ? member(show_constants(IDList),Options),
3377 b_get_machine_constants(TypedVars),
3378 last(StateIds,Last), % we assume there is only one constant valuation in the trace; TO DO: generalise
3379 get_state_and_action(Last,LastId,_,_),
3380 visited_expression(LastId,BState),
3381 expand_to_constants_and_variables(BState,ConstState,_),
3382 gen_state_table_aux(Stream,Options,'Constants',TypedVars,IDList,ConstState,'Value','bConstant_'),fail.
3383 gen_state_table(Stream,Options,_) :-
3384 b_or_z_mode,
3385 ? member(show_sets(IDList),Options),
3386 findall(TSet,bv_top_level_set(TSet,_),TypedVars),
3387 findall(bind(Set,Val),(bv_top_level_set(TSet,Val),get_texpr_id(TSet,Set)),BState),
3388 gen_state_table_aux(Stream,Options,'Sets',TypedVars,IDList,BState,'Value','bSet_'),fail.
3389 % TO DO: maybe show also top-level guards specfile_possible_trans_name or get_top_level_guard
3390 gen_state_table(Stream,Options,_StateIds) :-
3391 b_or_z_mode,
3392 member(show_events(IDList),Options),
3393 get_specification_description(operations,SN),
3394 atom_tail_to_lower_case(SN,SectionName),
3395 findall(b(identifier(OpName),subst,[]),b_top_level_operation(OpName),TypedVars),
3396 % TODO: op(Params,Results) instead of subst
3397 gen_state_table_aux(Stream,Options,SectionName,TypedVars,IDList,[],'Enabled','bOperation_'),fail.
3398 gen_state_table(Stream,Options,StateIds) :-
3399 xtl_mode,
3400 (length(StateIds,Len), Len > 1 -> NOptions = [show_prev_value|Options] ; NOptions = Options),
3401 bv_get_top_level(IDs),
3402 findall(b(identifier(ID),string,[]), member(ID,IDs), Props),
3403 gen_state_table_aux(Stream,NOptions,'Properties',Props,IDs,[],'Value','bVar_'), fail.
3404 gen_state_table(_Stream,_,_).
3405
3406
3407 gen_source_code_section(Stream,Options) :-
3408 member(show_source,Options), % we could also include original sources, rather than just internal rep.
3409 !,
3410 Section = 'Source',
3411 format(Stream,' <button type="button" class="collapsible collapsible-style" title="Inspect source code of internal representation of ProB of model">~w</button>~n',[Section]),
3412 format(Stream,'<div class="coll-content-hid">~n',[]),
3413 get_internal_representation(PP),
3414 format(Stream,'<pre>~s</pre>~n',[PP]),
3415 format(Stream,'</div>~n',[]).
3416 gen_source_code_section(_Stream,_).
3417
3418
3419 :- use_module(probsrc(bsyntaxtree),[get_texpr_description/2, get_texpr_type/2]).
3420 % creates a HTML table with header name Section and including one row per ID in TypedVars;
3421 % id of value for ID is prefixed with IDPrefix
3422 % VarListToShow is either all or a list of ids
3423 gen_state_table_aux(Stream,Options,Section,TypedVars,VarListToShow,BState,ValueStr,IDPrefix) :-
3424 include(show_typed_var_in_visb(VarListToShow),TypedVars,SVars), % check which ids should be shown
3425 length(SVars,SLen), SLen>0,
3426 length(TypedVars,Len),
3427 (SLen=Len
3428 -> format(Stream,' <button type="button" class="collapsible collapsible-style">~w (~w)</button>~n',[Section,SLen])
3429 ; format(Stream,' <button type="button" class="collapsible collapsible-style">~w (~w/~w)</button>~n',
3430 [Section,SLen,Len])
3431 ),
3432 format(Stream,'<div class="coll-content-hid">~n',[]),
3433 ? (member(show_prev_value,Options) % add extra column for previous value of variables (and animation expressions)
3434 -> format(Stream,' <table> <tr> <th>Nr</th> <th>Name</th> <th>Value</th> <th>Previous Value</th> </tr>~n',[])
3435 ; format(Stream,' <table> <tr> <th>Nr</th> <th>Name</th> <th>~w</th> </tr>~n',[ValueStr])),
3436 ? ( nth1(Nr,SVars,IDorExprToShow),
3437 get_state_table_name_and_expr(IDorExprToShow,ID,LongID,TExpr),
3438 ? (get_state_value_codes_for_id(BState,ID,Options,_,ValCodes)
3439 -> html_escape_codes(ValCodes,EVC) % Value provided in BState; may be overriden in trace export
3440 ; EVC = "?"),
3441 get_table_hover_message_codes(ID,TExpr,HoverMsgC),
3442 ? (member(show_prev_value,Options) % add previous value of variables (and animation expressions)
3443 -> % for variables the values are added later in JS
3444 % do we want to show the previous value in the state only HTML?
3445 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',
3446 [IDPrefix,ID, HoverMsgC, Nr, IDPrefix,ID,LongID, IDPrefix,ID, ID ])
3447 ;
3448 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',
3449 [IDPrefix,ID, HoverMsgC, Nr, IDPrefix,ID,LongID, IDPrefix,ID,EVC])),
3450 fail
3451 ;
3452 format(Stream,' </table>~n </div>~n',[])
3453 ).
3454
3455 %get_state_table_name_and_expr(bexpr(Kind,TExpr),Name,LongName,Expr) :- !, % we have special expression to show
3456 % Name=Kind,LongName=Kind,Expr=TExpr.
3457 get_state_table_name_and_expr(bexpr(Kind,TExpr),ID,LongName,Expr) :- !, % we have special expression to show
3458 ID=Kind, % ID for SVG updates, ...
3459 translate_bexpression_with_limit(TExpr,200,TS),
3460 ajoin([Kind,' == ',TS],LongName),
3461 Expr=TExpr.
3462 get_state_table_name_and_expr(TID,ID,ID,TID) :- get_texpr_id(TID,ID). % normal case: variable name
3463
3464
3465 :- use_module(probsrc(bmachine),[b_get_machine_animation_expression/2, b_get_operation_variant/3,
3466 b_nth1_non_ignored_invariant/3]).
3467
3468 visb_machine_animation_expression(variant,AEName,Variant,_) :-
3469 b_get_operation_variant(Name,ConvOrAnt,Variant),
3470 ajoin(['Variant for ',Name, ' (',ConvOrAnt,')'],AEName).
3471 visb_machine_animation_expression(animation_expression,Name,TExpr,_) :-
3472 b_get_machine_animation_expression(Name,TExpr).
3473 visb_machine_animation_expression(invariant,Name,TPred,Options) :-
3474 member(show_invariants,Options),
3475 b_nth1_non_ignored_invariant(Nr,TPred,_),
3476 ajoin(['INVARIANT-',Nr],Name).
3477 % TODO: we should also adapt get_state_value_change to return true when invariant_violated is false for the state
3478 % we could also only include this section when there is an invariant violation in the trace?
3479
3480 b_get_machine_expressions(List,Options) :-
3481 findall(bexpr(AE_Name,AExpr),visb_machine_animation_expression(_,AE_Name,AExpr,Options),List).
3482 % 'ANIMATION_EXPRESSION' or invariants or variants
3483
3484 :- use_module(probsrc(bmachine),[b_get_machine_operation_signature/2]).
3485 % get hover message for entries in variables/constants/... rows:
3486 get_table_hover_message_codes(ID,TExpr,EscHoverMsg) :-
3487 get_texpr_type(TExpr,Type),
3488 (Type=subst,b_get_machine_operation_signature(ID,TS)
3489 -> ajoin(['Operation: ',TS],HoverMsg)
3490 ; pretty_type(Type,TS),
3491 (get_texpr_description(TExpr,Desc)
3492 -> ajoin(['Type: ',TS,'\nDesc: ',Desc],HoverMsg)
3493 ; ajoin(['Type: ',TS],HoverMsg)
3494 )
3495 ),
3496 atom_codes(HoverMsg,HoverCodes),
3497 html_escape_codes(HoverCodes,EscHoverMsg).
3498
3499 % get the values that should be displayed in the variables table
3500 get_state_value_change(StateId,State,ID,Options,ECodes) :-
3501 extract_variables_from_state(State,VariableBState),
3502 ? ( get_state_value_codes_for_id(VariableBState,ID,Options,Val,ValCodes) % look up variable values
3503 ; visb_machine_animation_expression(_,_,_,Options) ->
3504 state_corresponds_to_fully_setup_b_machine(State,FullState),
3505 get_state_value_codes_for_anim_expr(StateId,FullState,ID,Options,Val,ValCodes) % evaluate animation expressions
3506 ),
3507 escape_if_necessary(Val,ValCodes,ECodes). % change " to \" for JavaScript
3508 % formatsilent('Value for ~w~nunescaped: "~s",~n escaped: "~s"~n',[ID,ValCodes,ECodes]).
3509
3510 % avoid unnecessary escaping traversals:
3511 escape_if_necessary([],ValCodes,Res) :- !, Res=ValCodes.
3512 escape_if_necessary(int(_),ValCodes,Res) :- !, Res=ValCodes.
3513 escape_if_necessary(pred_true,ValCodes,Res) :- !, Res=ValCodes.
3514 escape_if_necessary(pred_false,ValCodes,Res) :- !, Res=ValCodes.
3515 escape_if_necessary(_,ValCodes,ECodes) :- b_string_escape_codes(ValCodes,ECodes).
3516
3517
3518 get_state_value_codes_for_id(BState,ID,Options,Val,ValCodes) :-
3519 ? member(bind(ID,Val),BState),
3520 translate_values_for_state_table(Val,Options,ValCodes).
3521
3522 % translate a value for display in state table (not yet escaped)
3523 translate_values_for_state_table(Val,Options,ValCodes) :-
3524 (member(limit_for_values(Nr),Options)
3525 -> translate_bvalue_to_codes_with_limit(Val,Nr,ValCodes)
3526 ; get_preference(expand_avl_upto,Max), Max<0
3527 -> translate_bvalue_to_codes(Val,ValCodes) % unlimited
3528 ; translate_bvalue_to_codes_with_limit(Val,10000,ValCodes)
3529 ).
3530
3531 :- use_module(probsrc(bsyntaxtree), [safe_create_texpr/3]).
3532 get_state_value_codes_for_anim_expr(StateId,BState,AE_Name,Options,ResValue,ValCodes) :-
3533 visb_machine_animation_expression(Kind,AE_Name,AExpr,Options),
3534 (Kind=invariant
3535 -> ((invariant_not_yet_checked(StateId) ; invariant_violated(StateId))
3536 -> (safe_create_texpr(convert_bool(AExpr),boolean,TExpr),
3537 evaluate_visb_formula(TExpr,AE_Name,'',BState,ResValue,unknown)
3538 -> translate_pred_val(ResValue,ValCodes)
3539 ; ResValue=pred_unknown, ValCodes = "?" % WD error?
3540 )
3541 ; ResValue=pred_true, translate_pred_val(pred_true,ValCodes) % no need to evaluate invariant
3542 )
3543 ; evaluate_visb_formula(AExpr,AE_Name,'',BState,ResValue,unknown),
3544 translate_values_for_state_table(ResValue,Options,ValCodes)
3545 ).
3546 translate_pred_val(pred_true,[8868]). % see translate:unicode_translation(truth,X).
3547 translate_pred_val(pred_false,[8869]). % see translate:unicode_translation(falsity,X).
3548
3549 :- use_module(probsrc(bmachine),[b_get_machine_operation_max/2]).
3550 :- use_module(probsrc(state_space),[time_out_for_node/3,max_reached_for_node/1]).
3551 :- use_module(probsrc(translate),[translate_event_with_src_and_target_id/5]).
3552 get_state_value_enabled_operation_status(StateId,OpName,Enabled,EnabledValue,TransStr) :-
3553 b_top_level_operation(OpName),
3554 findall(TransID, (transition(StateId,OpTerm,TransID,_NewStateId),
3555 match_operation(OpTerm,OpName)), TransList),
3556 length(TransList,Len),
3557 (Len>0
3558 -> Enabled=true,
3559 EnabledValue = "\x2705\", % green check mark, TRUE alternatives \x2705\ \x2713\ \x2714\
3560 (TransList=[TID], transition(StateId,OpTerm,TID,NewStateId),
3561 translate_event_with_src_and_target_id(OpTerm,StateId,NewStateId,200,TransStr)
3562 -> true
3563 ; ajoin([OpName,' (',Len,'\xd7\)'],TransStr) %
3564 )
3565 ; time_out_for_node(StateId,OpName,TypeOfTimeOut) ->
3566 Enabled=TypeOfTimeOut,
3567 EnabledValue = [8987], % four o'clock symbol
3568 TransStr = OpName
3569 %ajoin(['No transition found due to: ',TypeOfTimeOut],HoverMsg)
3570 ; get_preference(maxNrOfEnablingsPerOperation,0) ->
3571 Enabled=not_computed,
3572 EnabledValue = [10067], % red question mark
3573 TransStr = OpName
3574 %'No transitions were computed because MAX_OPERATIONS = 0' = HoverMsg
3575 ; b_get_machine_operation_max(OpName,0) ->
3576 Enabled=not_computed,
3577 EnabledValue = [10067], % red question mark
3578 TransStr = OpName
3579 %ajoin(['No transitions were computed because MAX_OPERATIONS_',OpName,' = 0'],HoverMsg)
3580 ; Enabled=false,
3581 EnabledValue = [9940], % stop sign, FALSE, alternatives \x10102\
3582 TransStr = OpName
3583 %ajoin(['Not enabled'],HoverMsg)
3584 ). % TO DO: show whether this is the next step in the trace
3585
3586 % --------------------------
3587
3588 % debugging features to inspect all created SVG objects
3589 tcltk_get_visb_objects(list([Header|AllObjects])) :-
3590 Header = list(['SVG-ID','svg_class','Attribute','Value']),
3591 findall(list([SvgID,SvgClass,Attr,Value]),
3592 (visb_svg_obj_with_parent(SvgID,SvgClass,AttrList,true),
3593 (member(svg_attribute(Attr,Value),AttrList) ;
3594 visb_svg_parent(SvgID,Value), Attr=children)
3595 ), Childs),
3596 findall(list([SvgID,SvgClass,Attr,Value]),
3597 (visb_svg_obj_with_parent(SvgID,SvgClass,AttrList,false),
3598 member(svg_attribute(Attr,Value),AttrList)
3599 ),AllObjects, Childs).
3600
3601 % debugging features to inspect all created SVG objects
3602 tcltk_get_visb_hovers(list([Header|AllObjects])) :-
3603 Header = list(['SVG-ID','ID','Attribute','EnterValue', 'ExitValue']),
3604 findall(list([SvgID,ID,Attr,EnterVal,ExitVal]),
3605 visb_hover(SvgID,ID,Attr,EnterVal,ExitVal,_Pos), AllObjects).
3606
3607 % debugging features to inspect items
3608 tcltk_get_visb_items(Res) :-
3609 current_state_id(ID),
3610 tcltk_get_visb_items(ID,Res).
3611 tcltk_get_visb_items(_StateId,Res) :-
3612 \+ visb_file_is_loaded(_),!,
3613 Res = list(['No VisB JSON file loaded']).
3614 tcltk_get_visb_items(StateId,list([Header|AllItems])) :-
3615 Header = list(['SVG-ID','Attribute','Value']),
3616 get_preference(translation_limit_for_table_commands,Limit),
3617 findall(list([SvgID,SvgAttribute,Val]),
3618 get_change_attribute_for_state(StateId,SvgID,SvgAttribute,Val),
3619 Items),
3620 findall(list([DefID,'VisB Definition',DValS]),
3621 (get_expanded_bstate(StateId,ExpandedBState),
3622 reverse(ExpandedBState,RS),
3623 member(bind(DefID,DVal),RS),
3624 visb_definition(DefID,_,_,_,_,_),
3625 translate_bvalue_with_limit(DVal,Limit,DValS)),
3626 AllItems, Items).
3627
3628 :- use_module(probsrc(translate),[translate_event_with_limit/3]).
3629 tcltk_get_visb_events(Res) :-
3630 current_state_id(ID),
3631 tcltk_get_visb_events(ID,Res).
3632 tcltk_get_visb_events(_StateId,Res) :-
3633 \+ visb_file_is_loaded(_),!,
3634 Res = list(['No VisB JSON file loaded']).
3635 tcltk_get_visb_events(StateId,list([Header|AllItems])) :-
3636 Header = list(['SVG-ID','Event','Target']),
3637 get_preference(translation_limit_for_table_commands,Limit),
3638 findall(list([SvgID,EventStr,NewStateId]),
3639 (perform_visb_click_event(SvgID,[],StateId,_Event,OpTerm,NewStateId,Res),
3640 (Res=[] -> EventStr='disabled' ; translate_event_with_limit(OpTerm,Limit,EventStr))
3641 ),
3642 AllItems).
3643 % --------------------------
3644
3645 % for ProB2-UI
3646
3647 :- use_module(probsrc(translate),[translate_bexpression_with_limit/3]).
3648 get_visb_items(List) :-
3649 findall(visb_item(SvgID,Attr,TS,Desc,Pos),
3650 (visb_item(SvgID,Attr,TypedExpr,_Used,Desc,Pos,_),
3651 translate_bexpression_with_limit(TypedExpr,1000,TS)), List).
3652
3653 get_visb_attributes_for_state(StateId,List) :-
3654 % some external functions like ENABLED are evaluated in current state; it might be useful to set_current_state
3655 (visb_file_is_loaded(_) -> true
3656 ; add_warning(visb_visualiser,'No VisB visualisation loaded, cannot get attributes for state: ',StateId)),
3657 findall(set_attr(SvgID,SvgAttribute,Val),
3658 get_change_attribute_for_state(StateId,SvgID,SvgAttribute,Val),
3659 List).
3660
3661 % for ProB2-UI
3662 get_visb_click_events(List) :-
3663 findall(execute_event(SvgID,Event,Preds),
3664 get_visb_event(SvgID,Event,Preds), List).
3665 get_visb_event(SvgID,Event,Preds) :- visb_event(SvgID,Event,Preds,_,_File,_Pos).
3666 get_visb_event(SvgID,'',[]) :- % add a virtual empty event for SVG Ids with hovers but no events
3667 visb_has_hovers(SvgID),
3668 \+ visb_event(SvgID,_,_,_,_File,_Pos).
3669
3670
3671 :- use_module(probsrc(state_space), [extend_trace_by_transition_ids/1]).
3672 % perform a click on a VisB SVG ID in the animator
3673 tcltk_perform_visb_click_event(SvgID) :- current_state_id(StateId),
3674 (perform_visb_click_event(SvgID,[],StateId,TransitionIDs)
3675 -> formatsilent('Clicking on ~w in state ~w resulted in transition id sequence ~w~n',[SvgID,StateId,TransitionIDs]),
3676 extend_trace_by_transition_ids(TransitionIDs)
3677 ; add_error(visb_visualiser,'Cannot perform VisB click on: ',SvgID)
3678 ).
3679
3680 % computes the effect of clicking on an SvgID in StateId
3681 % it returns either empty list if the visb_event is not feasible or a list of transition ids
3682 % it fails if SvgID has no events associated with it
3683 perform_visb_click_event(SvgID,MetaInfos,StateId,ResTransitionIds) :-
3684 perform_visb_click_event(SvgID,MetaInfos,StateId,_,_,_,ResTransitionIds).
3685 perform_visb_click_event(SvgID,MetaInfos,StateId,OpName,OpTerm,NewStateId,ResTransitionIds) :-
3686 get_expanded_bstate(StateId,ExpandedBState),
3687 set_error_context(checking_context('VisB:','performing click event')),
3688 set_context_state(StateId,perform_visb_click_event),
3689 get_svgid_with_events(SvgID,_),
3690 call_cleanup(perform_aux(SvgID,StateId,ExpandedBState,OpName,OpTerm,NewStateId,ResTransitionIds,MetaInfos),
3691 (clear_context_state,clear_error_context)).
3692
3693 get_svgid_with_events(SvgID,FirstOpName) :- visb_event(SvgID,FirstOpName,_,_,_File,_Pos).
3694
3695
3696 :- use_module(probsrc(tools),[safe_read_term_from_atom/2]).
3697 :- use_module(probsrc(state_space),[transition/4]).
3698 perform_aux(SvgID,StateId,_ExpandedBState,OpName,OpTerm,NewStateId,ResTransitionIds,_MetaInfos) :-
3699 \+ b_or_z_mode,
3700 % just look up transition/4 entries in state space
3701 % TODO: maybe provide this possibility for B models, even if using explicit parameter values is more robust
3702 get_visb_event_operation(SvgID,OpName,Preds,_Pred,Pos),
3703 safe_read_term_from_atom(OpName,OpTerm0),
3704 (xtl_mode -> check_xtl_direct_transition_candidate(OpTerm0,Preds,Pos), OpTerm=OpTerm0 ; true), !,
3705 % for XTL: use exec by pred for arity 0, otherwise try to find transition term in state space
3706 if((transition(StateId,OpTerm,TransID,NewStateId),
3707 match_operation(OpTerm,OpName)), % match is relevant if \+xtl_mode
3708 ResTransitionIds = [TransID],
3709 return_disabled(SvgID,StateId,OpName,OpTerm,NewStateId,ResTransitionIds)
3710 ).
3711 perform_aux(SvgID,StateId,ExpandedBState,OpName,OpTerm,NewStateId,ResTransitionIds,MetaInfos) :-
3712 %state_space:portray_state_space,
3713 if(execute_visb_event_by_predicate(SvgID,StateId,ExpandedBState,OpName,OpTerm,NewStateId,TransIds,MetaInfos),
3714 ResTransitionIds = TransIds,
3715 return_disabled(SvgID,StateId,OpName,OpTerm,NewStateId,ResTransitionIds)).
3716
3717 check_xtl_direct_transition_candidate(OpTerm,Preds,Pos) :-
3718 nonvar(OpTerm), % upper case event names are interpreted as Prolog variables -> use exec by pred (or FIXME)
3719 functor(OpTerm,_,Ar), Ar>0, % use exec by pred for arity 0, otherwise try to find transition term in state space
3720 (Preds \= []
3721 -> add_warning(visb_visualiser,'Ignoring predicates for VisB XTL event with explicit transition term (use predicate to provide parameter values): ',OpTerm,Pos)
3722 ; true).
3723
3724 return_disabled(SvgID,StateId,OpName,OpTerm,NewStateId,ResTransitionIds) :-
3725 OpTerm = disabled, NewStateId = StateId,
3726 get_svgid_with_events(SvgID,OpName),
3727 ResTransitionIds = []. % visb_event not enabled
3728
3729 :- use_module(probsrc(tools_strings),[match_atom/2]).
3730 :- use_module(probsrc(specfile),[get_operation_name/2]).
3731 match_operation(OpTerm,OpTerm) :- !.
3732 match_operation(OpTerm,OpName) :- atom(OpName),
3733 (get_operation_name(OpTerm,OpName)
3734 ; match_atom(OpName,OpTerm) % match an atom string with a compound term
3735 ),!.
3736
3737 execute_visb_event_by_predicate(SvgID,StateId,ExpandedBState,OpName,OpTerm,NewStateId,TransIds,MetaInfos) :-
3738 get_visb_event_operation(SvgID,OpName,_,Pred,Pos),
3739 build_visb_click_meta_object(MetaInfos,BMetaInfos),
3740 bsyntaxtree:replace_id_by_expr(Pred,'VISB_CLICK_META_INFOS',BMetaInfos,NPred),
3741 exec_aux(SvgID,StateId,ExpandedBState,OpName,NPred,Pos,OpTerm,NewStateId,TransIds).
3742
3743 build_visb_click_meta_object(MetaInfos,BMetaInfos) :-
3744 (member(alt_key,MetaInfos) -> AltKey = pred_true ; AltKey = pred_false),
3745 (member(ctrl_key,MetaInfos) -> CtrlKey = pred_true ; CtrlKey = pred_false),
3746 (member(meta_key,MetaInfos) -> MetaKey = pred_true ; MetaKey = pred_false),
3747 (member(pageX(PageX),MetaInfos) -> true ; PageX = 0), % fallback
3748 (member(pageY(PageY),MetaInfos) -> true ; PageY = 0), % fallback
3749 (member(shift_key,MetaInfos) -> ShiftKey = pred_true ; ShiftKey = pred_false),
3750 findall(','(string(Var),string(VarValue)), member(js_var(Var,VarValue), MetaInfos), JSVars),
3751
3752 visb_click_meta_b_type(BType),
3753 BMetaInfos = b(value(rec([
3754 field(altKey,AltKey),
3755 field(ctrlKey,CtrlKey),
3756 field(jsVars,JSVars),
3757 field(metaKey,MetaKey),
3758 field(pageX,int(PageX)),
3759 field(pageY,int(PageY)),
3760 field(shiftKey,ShiftKey)
3761 ])),BType,[visb_generated]).
3762
3763 visb_click_meta_b_type(record([
3764 field(altKey,boolean),
3765 field(ctrlKey,boolean),
3766 field(jsVars,set(couple(string,string))),
3767 field(metaKey,boolean),
3768 field(pageX,integer),
3769 field(pageY,integer),
3770 field(shiftKey,boolean)
3771 ])).
3772
3773 :- use_module(probsrc(tcltk_interface),[compute_all_transitions_if_necessary/2]).
3774 :- use_module(library(random),[random_member/2]).
3775 :- use_module(extrasrc(mcts_game_play), [mcts_auto_play/4, mcts_auto_play_available/0]).
3776 :- use_module(probsrc(tools_timeout), [time_out_with_factor_call/3]).
3777 exec_aux(SvgID,StateId,ExpandedBState,OpName,Pred,Pos,OpTerm,NewStateId,[TransId]) :-
3778 (b_or_z_mode -> b_is_operation_name(OpName) ; true), !, % note: ignores special definitions below if not B mode
3779 time_out_with_factor_call(
3780 exec_op_by_pred_aux(StateId,ExpandedBState,OpName,Pred,OpTerm,NewState,Pos,TransInfo),
3781 5, % min_max_time_out(10,100,15000)
3782 (ajoin(['TIME-OUT for VisB click on SVG ID ', SvgID,' while executing operation by predicate: '],Msg),
3783 add_warning(visb_visualiser,Msg,OpName,Pos),fail)),
3784 patch_state(NewState,StateId,PatchedNewState),
3785 % add transition to state space:
3786 tcltk_interface:add_trans_id_infos(StateId,OpTerm,PatchedNewState,NewStateId,TransId,TransInfo).
3787 %translate:print_bstate(PatchedNewState),nl.
3788 exec_aux(SvgID,StateId,_ExpandedBState,'MCTS_AUTO_PLAY',_Pred,Pos,OpTerm,NewStateId,[TransId]) :- !,
3789 mcts_auto_play_available,
3790 % TODO: allow to set SimRuns, TimeOut in Pred
3791 add_debug_message(visb_visualiser,'Performing MCTS_AUTO_PLAY for click on: ',SvgID,Pos),
3792 mcts_auto_play(StateId,OpTerm,TransId,NewStateId).
3793 exec_aux(_SvgID,StateId,_ExpandedBState,'RANDOM_ANIMATE',_Pred,_Pos,OpTerm,NewStateId,[TransId]) :- !,
3794 compute_all_transitions_if_necessary(StateId,false),
3795 findall(rtr(OpTerm,TransId,NewStateId),transition(StateId,OpTerm,TransId,NewStateId),List),
3796 random_member(rtr(OpTerm,TransId,NewStateId),List).
3797 % see tcltk_interface:tcltk_random_perform2 and allow Kind: fully_random, no_self_loops, heuristics, ...
3798 % split with ; ?
3799 exec_aux(SvgID,StateId,ExpandedBState,'RANDOM_ANIMATE_UNTIL_LTL',LTLExpr,Pos,OpTerm,NewStateId,TransIds) :- !,
3800 OpTerm = 'RANDOM_ANIMATE_UNTIL_LTL',
3801 (get_texpr_type(LTLExpr,string),
3802 evaluate_visb_formula(LTLExpr,'RANDOM_ANIMATE_UNTIL_LTL',SvgID,ExpandedBState,Value,Pos),
3803 Value = string(LTLFormula)
3804 -> tcltk_interface:tcltk_animate_until(LTLFormula,StateId,1000,ltl_state_property,_Steps,_Res,NewStateId,TransIds)
3805 ; add_error(visb_visualiser,'Argument to RANDOM_ANIMATE_UNTIL_LTL must provide LTL formula as string:',StateId)
3806 ).
3807
3808 :- use_module(probsrc(b_state_model_check),[execute_operation_by_predicate_in_state_with_pos/7,
3809 xtl_execute_operation_by_predicate_in_state/8]).
3810 exec_op_by_pred_aux(StateId,ExpandedBState,OpName,Pred,OpTerm,NewState,Pos,TransInfo) :- xtl_mode,!,
3811 visited_expression(StateId,RawState),
3812 xtl_execute_operation_by_predicate_in_state(ExpandedBState,RawState,OpName,Pred,OpTerm,NewState,Pos,TransInfo).
3813 exec_op_by_pred_aux(_StateId,ExpandedBState,OpName,Pred,OpTerm,NewState,Pos,TransInfo) :-
3814 execute_operation_by_predicate_in_state_with_pos(ExpandedBState,OpName,Pred,OpTerm,NewState,Pos,TransInfo).
3815
3816 :- use_module(probsrc(bmachine), [b_is_variable/1,b_machine_has_constants/0]).
3817
3818 is_var_binding(bind(Var,_)) :- b_or_z_mode, b_is_variable(Var).
3819
3820
3821 % remove constants and VisB Definition entries from state:
3822 patch_state(NewState,_StateId,PatchedState) :-
3823 \+ b_or_z_mode, !, PatchedState=NewState. % XTL state is raw state
3824 patch_state(NewState,StateId,PatchedState) :-
3825 get_constants_id_for_state_id(StateId,ConstId),!,
3826 PatchedState = const_and_vars(ConstId,VarsState),
3827 include(is_var_binding,NewState,VarsState).
3828 patch_state(NewState,StateId,VarsState) :-
3829 (b_machine_has_constants
3830 -> add_error(visb_visualiser,'Could not extract constants id for state:',StateId),
3831 VarsState=NewState
3832 ; include(is_var_binding,NewState,VarsState)).
3833
3834 % the next predicate gets all operations/events associated with SvgID in the order in which they were found
3835 % note that there is only one visb_event (the last one); all others are auxiliary
3836 get_visb_event_operation(SvgID,OpName,Preds,TypedPred,Pos) :- % check if there are more events registered:
3837 auxiliary_visb_event(SvgID,OpName,Preds,TypedPred,Pos).
3838 get_visb_event_operation(SvgID,OpName,Preds,TypedPred,Pos) :-
3839 visb_event(SvgID,OpName,Preds,TypedPred,_File,Pos).
3840
3841 % ---------------
3842
3843 get_visb_hovers(List) :-
3844 findall(hover(SvgID,ID,Attr,EnterVal,ExitVal),
3845 visb_hover(SvgID,ID,Attr,EnterVal,ExitVal,_), List).
3846
3847 get_visb_svg_objects(List) :-
3848 % TODO: remove objects inlined in get_visb_default_svg_file_contents
3849 topological_sort_svg_objects(SvgIDs),
3850 findall(visb_svg_object(SvgID,SvgClass,AttrList),
3851 (member(SvgID,SvgIDs),
3852 visb_svg_obj_with_parent(SvgID,SvgClass,AttrList,_)), List).
3853
3854 visb_svg_obj_with_parent(SvgID,SvgClass,AttrList,IsChild) :-
3855 visb_svg_object(SvgID,SvgClass,List,_Desc,_Pos),
3856 (visb_svg_child(SvgID,ParentId)
3857 -> IsChild=true, AttrList = [svg_attribute(parentId,ParentId)|List] % add parentId attribute for ProB2-UI
3858 ; IsChild=false, AttrList = List).
3859
3860
3861 :- use_module(probsrc(tools),[top_sort/3]).
3862 :- use_module(library(ugraphs),[vertices_edges_to_ugraph/3]).
3863 topological_sort_svg_objects(SortedSVGObjects) :-
3864 findall(SvgID,visb_svg_object(SvgID,_,_,_,_),Vertices),
3865 findall(V-W,visb_svg_parent(V,W),Edges),
3866 vertices_edges_to_ugraph(Vertices,Edges,Graph),
3867 (top_sort(Graph,SortedSVGObjects,UnsortedNr)
3868 -> (UnsortedNr = 0 -> true
3869 ; add_warning(visb_visualiser,'Cycle in SVG_OBJECTS parent/child graph, unsorted objects: ',UnsortedNr)
3870 )
3871 ; SortedSVGObjects=Vertices,
3872 add_error(visb_visualiser,'Topological sorting of SVG_OBJECTS failed: ',Vertices)
3873 ).
3874
3875 % ------------------
3876
3877 :- use_module(probsrc(bmachine),[b_absolute_file_name_relative_to_main_machine/2]).
3878 extended_static_check_default_visb_file :-
3879 (get_default_visb_file(VisBFile,Pos)
3880 % TODO: we could check if we have an visb_history(JSONFile,_,_) option
3881 -> extended_static_check_visb_file(VisBFile,Pos)
3882 ; true).
3883
3884 extended_static_check_visb_file('',_InclusionPos) :- !,
3885 load_visb_file('').
3886 extended_static_check_visb_file(VisBFile,InclusionPos) :-
3887 b_absolute_file_name_relative_to_main_machine(VisBFile,AFile),
3888 (file_exists(AFile)
3889 -> load_visb_file(AFile)
3890 ; add_warning(lint,'VISB_JSON_FILE does not exist: ',AFile,InclusionPos)
3891 ).
3892
3893 % ---------------------------
3894
3895 % portray all VisB items in DEFINITION B syntax
3896 get_visb_ids(SIds) :-
3897 findall(Id,visb_id(Id),Ids),
3898 sort(Ids,SIds).
3899
3900 visb_id(ID) :- visb_svg_object(ID,_,_,_,_). % see svg_id_exists
3901 visb_id(ID) :- visb_item(ID,_,_,_,_,_,_), \+ visb_svg_object(ID,_,_,_,_).
3902 visb_id(ID) :- visb_event(ID,_,_,_,_,_), \+ visb_svg_object(ID,_,_,_,_).
3903 visb_id(ID) :- visb_hover(ID,_,_,_,_,_), \+ visb_svg_object(ID,_,_,_,_).
3904
3905 :- public portray_visb/0.
3906 portray_visb:-
3907 get_visb_ids(SIds), nth1(Nr,SIds,ID),
3908 %visb_svg_object(ID,SVG_Class,NewRestAttrs,Desc,Pos1),
3909 findall(field(Attr,b(value(StaticVal),any,[])),
3910 (visb_svg_object(ID,SVG_Class,StaticAttrs,Desc,_Pos1),
3911 ( Attr=svg_class,StaticVal=string(SVG_Class)
3912 ; Attr=comment,StaticVal=string(Desc)
3913 ; member(svg_attribute(Attr,StaticVal),StaticAttrs))
3914 ),
3915 StaticValues),
3916 findall(field(Attr,TypedExpr),
3917 visb_item(ID,Attr,TypedExpr,_UsedIds,_Desc,_PosStartOfItem,_Meta), % meta can contain override
3918 Updates,StaticValues),
3919 % TODO: incorporate events and hovers
3920 UpdateRec = b(rec(Fields),any,[]),
3921 gen_string(ID,IDS),
3922 Fields = [field(id,IDS) | Updates],
3923 (StaticValues=[] -> format('~nVISB_SVG_UPDATES~w == ',[Nr]) ; format('~nVISB_SVG_OBJECTS~w == ',[Nr])),
3924 translate:print_bexpr(UpdateRec), write(';'), nl,
3925 fail.
3926 portray_visb.
3927 gen_string(ID,b(string(ID),string,[])).
3928 % use_module(visbsrc(visb_visualiser)), visb_visualiser:portray_visb.