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, visb_state_can_be_visualised/1,
11		get_default_visb_file/2, extended_static_check_default_visb_file/0,
12		load_default_visb_file_if_necessary/0,
13		tcltk_get_visb_items/1, tcltk_get_visb_events/1,
14		tcltk_get_visb_objects/1, tcltk_get_visb_hovers/1,
15		get_visb_items/1, get_visb_attributes_for_state/2,
16		get_visb_click_events/1, get_visb_hovers/1,
17		perform_visb_click_event/4,
18		tcltk_perform_visb_click_event/1,
19		get_visb_svg_objects/1,
20		% used by visb_html_export:
21		get_change_attribute_for_state/4, get_and_eval_special_definition/6,
22		evaluate_visb_formula/6, b_value_to_string/2, add_visb_lint_message/3,
23		no_svg_available/0, match_operation/2,
24		visb_file_loaded/4, visb_svg_file/5, visb_empty_svg_box_height_width/3,
25		visb_svg_object/5, visb_svg_child/2, visb_svg_parent/2,
26		visb_svg_child_of_object_from_svg_file/1,
27		visb_has_hovers/1, visb_hover/6]).
28
29		:- use_module(probsrc(module_information),[module_info/2]).
30		:- module_info(group,visualization).
31		:- module_info(description,'This module provides VisB visualisation functionality.').
32
33		% special SVG object attributes treated by VisB
34		% title (creates hover tooltip; currently only works with objects created by VisB itself)
35		% id
36		% svg_class
37		% text
38		% hovers
39		% event, events
40		% predicate
41
42		:- meta_predicate process_repeat(-,-,-,2).
43
44		:- use_module(extrasrc(json_parser), [json_parse_file/3]).
45		:- use_module(library(lists)).
46		:- use_module(probsrc(error_manager)).
47		:- use_module(probsrc(preferences), [get_preference/2, reset_temporary_preference/2,
48		temporary_set_preference/3]).
49		:- use_module(probsrc(debug)).
50		:- use_module(probsrc(state_space), [visited_expression/2, get_constants_id_for_state_id/2,
51		get_constants_state_id_for_id/2, set_context_state/2,
52		clear_context_state/0, transition/3, transition/4,
53		multiple_concrete_constants_exist/0,
54		root_sufficiently_explored/0,
55		is_concrete_constants_state_id/1, current_state_id/1,
56		current_state_corresponds_to_setup_constants_b_machine/0,
57		visited_state_corresponds_to_setup_constants_b_machine/1,
58		time_out_for_node/3, max_reached_for_node/1]).
59		:- use_module(probsrc(translate), [translate_bvalue_to_codes/2,
60		translate_bvalue_to_codes_with_limit/3,
61		translate_bvalue_with_limit/3, pretty_type/2]).
62		:- use_module(probsrc(specfile), [eventb_mode/0, xtl_mode/0,
63		state_corresponds_to_initialised_b_machine/2,
64		state_corresponds_to_set_up_constants_only/2,
65		translate_operation_name/2, classical_b_mode/0, b_or_z_mode/0,
66		csp_with_bz_mode/0]).
67		:- use_module(probsrc(tools), [start_ms_timer/1, stop_ms_walltimer_with_msg/2, ajoin_with_sep/3,
68		split_list/4, get_filename_extension/2, split_chars/3,
69		safe_number_codes/2, safe_atom_codes/2]).
70		:- use_module(probsrc(bmachine), [b_machine_name/1, b_get_definition_name_with_pos/4,
71		bmachine_is_precompiled/0, pre_expand_typing_scope/2,
72		determine_type_of_formula/2, determine_type_of_formula/3,
73		b_load_additional_definitions_file/1,
74		b_load_additional_definitions_from_list_of_facts/1,
75		b_load_additional_definitions_from_term/1,
76		set_additional_filename_as_parsing_default/3,
77		reset_filename_parsing_default/2,
78		b_sorted_b_definition_prefixed/4, b_get_typed_definition/3,
79		b_is_operation_name/1,
80		b_parse_machine_operation_pre_post_predicate/5]).
81		:- use_module(probsrc(bsyntaxtree), [get_texpr_ids/2, get_texpr_pos/2, create_couple/2,
82		create_couple/3, replace_ids_by_exprs/4, create_equality/3,
83		get_texpr_type/2, find_identifier_uses/3,
84		conjunct_predicates/2, map_over_bexpr/2, get_texpr_id/2]).
85		:- use_module(probsrc(tools_lists), [include_maplist/3]).
86		:- use_module(probsrc(tools_matching), [get_all_svg_attributes/1, is_svg_attribute/1,
87		is_virtual_svg_attribute/1, is_svg_number_attribute/2,
88		is_svg_color_attribute/1, svg_attribute_default_value/2,
89		get_possible_fuzzy_matches_and_completions_msg/3,
90		get_all_svg_classes/1, is_svg_shape_class/1, is_html_tag/1,
91		is_html_attribute/1, dotshape2svg_class/2,
92		fix_svg_attribute/2, is_dot_attribute/1]).
93		:- use_module(visb_json_utils, [get_attr/3, get_attr_with_pos/5,
94		del_attr/4, del_attr_with_pos/6, non_det_del_attr_with_pos/6,
95		force_del_attr/5, force_del_attr_with_pos/6,
96		get_attr_true/3, is_optional_json_item/1, is_optional_json_item/3,
97		check_json_string/4,
98		get_pos_from_list/3, construct_prob_pos_term/3,
99		replace_in_json/4, multi_replace_in_json/4,
100		check_all_same_length_json/3]).
101		:- use_module(visb_static_check, [static_check_dynamic_update_def_body/1,
102		static_check_attribute_value_expression/2,
103		check_svg_attribute_value/3]).
104		:- use_module(probsrc(eventhandling), [register_event_listener/3]).
105		:- use_module(probsrc(pref_definitions), [b_get_definition_string_from_spec/3]).
106		:- use_module(library(file_systems), [file_exists/1, file_property/3]).
107		:- use_module(probsrc(tools_strings), [ajoin/2, safe_name/2, atom_prefix/2,
108		is_simple_classical_b_identifier_codes/1]).
109		:- use_module(probsrc(custom_explicit_sets), [try_expand_custom_set_with_catch/3,
110		is_custom_explicit_set/1, is_set_value/2,
111		singleton_set/2]).
112		:- use_module(probsrc(typing_tools), [any_value_for_type/2]).
113		:- use_module(extrasrc(external_functions_svg), [svg_points/4]).
114		:- use_module(probsrc(store), [lookup_value_for_existing_id/3]).
115		:- use_module(probsrc(gensym), [gensym/2]).
116		:- use_module(probsrc(self_check)).
117		:- use_module(probsrc(external_functions), [external_function_requires_state/1]).
118		:- use_module(probsrc(kernel_reals), [is_real/2]).
119		:- use_module(probsrc(b_global_sets), [add_prob_deferred_set_elements_to_store/3]).
120		:- use_module(probsrc(b_interpreter), [b_compute_expression_nowf/7,
121		b_compute_explicit_epression_no_wf/7]).
122
123
124		% --------------------------
125
126		% facts storing loaded JSON VisB file:
127		:- dynamic visb_file_loaded/4, visb_svg_file/5, visb_empty_svg_box_height_width/3,
128		visb_definition/6, visb_special_definition/6,
129		visb_item/7,
130		visb_event/7, visb_hover/6, visb_has_hovers/1, visb_has_visibility_hover/1,
131		visb_event_enable_list/5,
132		visb_svg_object/5, visb_svg_object_debug_info/2,
133		visb_svg_child/2, visb_svg_parent/2, % register parent/child relationships for groups, title, ...
134		visb_svg_child_of_object_from_svg_file/1. % true if parent of object is an SVG in an external file
135		:- dynamic auxiliary_visb_event/6.
136		% visb_svg_file(SVGFile, AbsolutePathSVGFile, JSONFileFromWhichWeImportSVG,PosTerm,ModLocTime)
137		% visb_item(SVGID,Attribute,TypedExpression,UsedIds,Description/Comment,StartPos,OtherMetaInfos)
138		% visb_event(SVGID,Event,PredicateList,ExecutionKind,TypedPredicate,File,Pos) ; ExecutionKind: default, first, random or heuristic
139		% visb_svg_object(SVGID,SVG_Class,AttrList,Description/Comment,Pos) ; AttrList contains svg_attribute(Attr,Val)
140
141		reset_visb :- debug_println(9,resetting_visb),
142		retractall(visb_file_loaded(_,_,_,_)),
143		retractall(visb_empty_svg_box_height_width(_,_,_)),
144		retractall(visb_svg_file(_,_,_,_,_)),
145		retractall(visb_definition(_,_,_,_,_,_)),
146		retractall(visb_special_definition(_,_,_,_,_,_)),
147		retractall(visb_item(_,_,_,_,_,_,_)),
148		retractall(visb_event(_,_,_,_,_,_,_)),
149		retractall(visb_hover(_,_,_,_,_,_)),
150		retractall(visb_has_hovers(_)),
151		retractall(visb_has_visibility_hover(_)),
152		retractall(visb_event_enable_list(_,_,_,_,_)),
153		retractall(auxiliary_visb_event(_,_,_,_,_,_)),
154		retractall(visb_svg_object(_,_,_,_,_)),
155		retractall(visb_svg_object_debug_info(_,_)),
156		retractall(visb_svg_child(_,_)),
157		retractall(visb_svg_child_of_object_from_svg_file(_)),
158		retractall(visb_svg_parent(_,_)),
159		reset_auto_attrs.
160
161		visb_file_is_loaded(JSONFile) :-
162		visb_file_is_loaded(JSONFile,_,true).
163		visb_file_is_loaded(JSONFile,SVGFile,AllowEmpty) :-
164		visb_file_loaded(JSONFile,_,_,_),
165		(visb_svg_file(_,SVGFile,_,_,_) -> true
166		; visb_empty_svg_box_height_width(_,_,_) -> SVGFile = ''
167		; user_has_defined_visb_objects -> SVGFile = ''
168		; JSONFile='' ->
169		AllowEmpty=true,
170		add_warning(visb_visualiser,'No VISB_SVG_FILE or VISB_SVG_OBJECTS specified in DEFINITIONS',''),
171		% Note: warning also generated below No VisB JSON file is specified and no VISB_SVG_OBJECTS were created
172		SVGFile = ''
173		; add_warning(visb_visualiser,'No SVG file or objects specified for VisB file:',JSONFile),
174		AllowEmpty=true,
175		SVGFile = ''
176		).
177
178		no_svg_available :-
179		\+ user_has_defined_visb_objects,
180		no_svg_file_available,
181		\+ visb_empty_svg_box_height_width(_,_,_). % no SVG box provided
182
183		no_svg_file_available :- (visb_svg_file(_,SVGFile,_,_,_) -> SVGFile='' ; true).
184		%svg_file_available :- \+ no_svg_file_available.
185
186		visb_state_can_be_visualised(ID) :-
187		(b_or_z_mode -> visited_state_corresponds_to_setup_constants_b_machine(ID)
188		; ID \= root
189		).
190		visb_current_state_can_be_visualised :-
191		%visb_file_is_loaded(_), % no longer checked; Tcl/Tk will automatically load VisB file if required
192		current_state_id(ID), visb_state_can_be_visualised(ID).
193
194
195		:- register_event_listener(reset_specification,reset_visb,'Reset VisB information').
196		:- register_event_listener(reset_prob,reset_visb,'Reset VisB information').
197
198		%static_check_visb :- % now done when adding items and not storing multiple items
199		% visb_item(ID,Attr,F1,_,_,Pos1), visb_item(ID,Attr,F2,_,Pos2), F1 @< F2,
200		% add_warning(visb_visualiser,'Multiple formulas for SVG identifier and attribute:',ID/Attr,Pos1),
201		% add_message(visb_visualiser,'Location of second formula for:',ID/Attr,Pos2),
202		% fail.
203		% TO DO: some sanity checks on attributes and values
204		static_check_visb :-
205		no_svg_file_available,
206	?	visb_hover(SVGID,_ID,Attr,_Enter,_Exit,Pos),
207		\+ svg_id_exists(SVGID),
208		ajoin(['Hover for attribute ',Attr,' has unknown trigger-id (can lead to blank visualisation): '],Msg),
209		add_warning(visb_visualiser,Msg,SVGID,Pos),
210		fail.
211		static_check_visb :-
212		no_svg_file_available,
213	?	visb_hover(SVGID,ID,Attr,_Enter,_Exit,Pos), ID \= SVGID,
214		\+ svg_id_exists(ID),
215		ajoin(['Hover for attribute ',Attr,' has unknown id (can lead to blank visualisation): '],Msg),
216		add_warning(visb_visualiser,Msg,ID,Pos),
217		fail.
218		static_check_visb :-
219		visb_svg_file(SvgFile,_,_,Pos,_),
220		SvgFile \= '',
221		visb_empty_svg_box_height_width(H,W,ViewBox),
222		ajoin(['VISB_SVG_BOX (width=', W, ', height=', H, ', viewBox=', ViewBox,
223		') cannot be applied to an existing SVG file (use VISB_SVG_CONTENTS for file or put info into SVG file): '],Msg),
224		add_warning(visb_visualiser,Msg,SvgFile,Pos),
225		fail.
226		static_check_visb.
227
228		svg_id_exists(SVGID) :- visb_svg_object(SVGID,_,_StaticAttrList,_,_ExitPos).
229		svg_id_has_class(SVGID,Class) :- visb_svg_object(SVGID,Class,_StaticAttrList,_,_ExitPos).
230		% --------------------------
231
232
233		get_default_visb_file(Path, Pos) :- get_default_visb_file(Path, _, Pos).
234		get_default_visb_file(Path, Kind, Pos) :- bmachine_is_precompiled,
235		(b_get_definition_string_from_spec('VISB_JSON_FILE', Pos, Path)
236		-> Kind=json % user provided explicit path to VISB JSON file
237		; b_get_definition_string_from_spec('VISB_DEFINITIONS_FILE', Pos, Path)
238		-> Kind=def % user provided explicit path to VISB DEFINITIONS file
239		% TODO: in future check that file extension is compatible
240		% advantage of VISB_DEFINITIONS_FILE == "File" over "File"
241		% 1) visualisation can be re-loaded without re-loading machine
242		% 2) can be used in TLA+ or similar
243		% 3) avoid clash if definitions file itself defines empty VISB_JSON_FILE
244		% 4) avoid problems with Atelier-B or other tools
245		; get_default_visb_svg_file(_,Pos)
246		-> Kind=empty, Path='' % user provided SVG file path
247		; user_has_defined_visb_objects_in_defs
248		-> Kind=empty, Path='' % user provided SVG object definitions
249		).
250
251		user_has_defined_visb_objects :-
252	?	(visb_svg_object(_,_,_,_,_) -> true % created in JSON file
253		; user_has_defined_visb_objects_in_defs).
254
255		user_has_defined_visb_objects_in_defs :-
256		b_sorted_b_definition_prefixed(expression,'VISB_SVG_OBJECTS',_,_).
257
258		% you should use default_visb_svg_abs_file to obtain the absolute path
259		get_default_visb_svg_file(Path, Pos) :-
260		b_get_definition_string_from_spec('VISB_SVG_FILE', Pos, Path).
261
262		% the VISB_SVG_FILE is relative to the main B machine, also when a JSON file is used
263		default_visb_svg_abs_file('',AbsFile) :- !, AbsFile=''. % just dummy empty string provided by user
264		default_visb_svg_abs_file(SvgFile,AbsFile) :-
265		b_absolute_file_name_relative_to_main_machine(SvgFile,AbsFile).
266
267
268		% load default VISB_JSON_FILE if it is specified and not already loaded
269		load_default_visb_file_if_necessary :-
270		get_default_visb_file(File, Pos),!,
271		(load_visb_file_if_necessary(File) -> true
272		; add_error(visb_visualiser,'Could not load VISB_JSON_FILE:',File,Pos)).
273		load_default_visb_file_if_necessary :-
274		(eventb_mode -> true ; add_message(visb_visualiser,'No VISB_JSON_FILE DEFINITION provided')).
275
276		% --------------------------
277		% Loading a JSON VisB file:
278
279
280		load_visb_file(File) :-
281		temporary_set_preference(allow_arith_operators_on_reals,true,Old),
282		call_cleanup((load_visb_file1(File)),
283		reset_temporary_preference(allow_arith_operators_on_reals,Old)).
284		load_visb_file1(File) :-
285		get_filename_extension(File,def), % a .def B definition file
286		!,
287		add_message(visb_visualiser,'Loading VisB DEFINITIONS from B file: ',File),
288		b_load_additional_definitions_file(File),
289		load_visb_file2('',File).
290		load_visb_file1(File) :- load_visb_file2(File,File).
291
292		load_visb_definitions_from_list_of_facts(DefFilePath, ListOfFacts) :-
293		temporary_set_preference(allow_arith_operators_on_reals,true,Old),
294		call_cleanup(
295		(b_load_additional_definitions_from_list_of_facts(ListOfFacts),
296		load_visb_file2('', DefFilePath)),
297		reset_temporary_preference(allow_arith_operators_on_reals,Old)).
298
299		load_visb_definitions_from_term(DefFilePath, Machine) :-
300		temporary_set_preference(allow_arith_operators_on_reals,true,Old),
301		call_cleanup(
302		(b_load_additional_definitions_from_term(Machine),
303		load_visb_file2('', DefFilePath)),
304		reset_temporary_preference(allow_arith_operators_on_reals,Old)).
305
306		load_visb_file2(JsonFile,OrigFileName) :-
307		reset_visb,
308		load_visb_from_definitions(no_inlining,JsonFile), % TODO: pass InlineObjects?
309		start_ms_timer(T),
310		(JsonFile='' % No JSON file
311		-> (get_default_visb_svg_file(SvgFile,DefaultSVGPos)
312		-> default_visb_svg_abs_file(SvgFile,AbsFile),
313		add_visb_svg_file(SvgFile,AbsFile,'',DefaultSVGPos)
314		; check_objects_created(JsonFile) % no JSON and SVG file; check we have created objects
315		)
316		; add_visb_file(JsonFile,[]),
317		stop_ms_walltimer_with_msg(T,'loading VisB JSON file: ')
318		),
319		static_check_visb,
320		(OrigFileName = ''
321		-> ModTime=0, ModLocTime=0 % We could get modification time of files with VISB_SVG_OBJECTS, ... DEFINITIONS
322		; file_property(OrigFileName, modify_timestamp, ModTime),
323		file_property(OrigFileName, modify_localtime, ModLocTime)
324		),
325		constants_status(CS),
326		assertz(visb_file_loaded(OrigFileName,ModTime,ModLocTime,CS)).
327
328		% mainly useful for CSP||B where concrete_constants not directly available upon loading machine
329		% TODO: we could compute the number of constant values available and store this (e.g., when MAX_INITIALISATIONS is 0)
330		constants_status(X) :- root_sufficiently_explored,!, X=available.
331		constants_status(not_available).
332
333		check_objects_created(File) :-
334	?	(visb_svg_object(_,_,_,_,_) -> true
335		; add_warning(visb_visualiser,'No VisB JSON file is specified and no VISB_SVG_OBJECTS were created:',File)
336		).
337
338		load_visb_from_definitions(InlineObjects,JsonFileContext) :-
339		start_ms_timer(T),
340		pre_expand_typing_scope([variables_and_additional_defs],ExpandedScope), % do this only once for all defs
341		get_svg_objects_from_definitions(InlineObjects,ExpandedScope,JsonFileContext),
342		(get_SVG_BOX_definition(InlineObjects) -> true ; true), % TODO: also pass scope
343		stop_ms_walltimer_with_msg(T,'extracting VisB infos from DEFINITIONS: ').
344
345
346		%:- use_module(library(system),[now/1, datime/2]).
347		load_visb_file_if_necessary(File) :-
348		visb_file_loaded(File,ModTime1,_,ConstantsStatus), % this file is already loaded
349		constants_status(ConstantsStatus), % if constants status has changed we need to re-load visualisation
350		(File = '' -> true
351		; file_exists(File),
352		file_property(File, modify_timestamp, ModTime2), % check if it has the same time stamp
353		debug_println(19,visb_json_already_loaded(File,ModTime1,ModTime2)),
354		ModTime1=ModTime2
355		),
356		!.
357		load_visb_file_if_necessary(File) :- constants_status(not_available),!,
358		add_message(visb_visualiser,'Not loading VisB file no constants set up yet: ',File).
359		load_visb_file_if_necessary(File) :- load_visb_file(File).
360
361
362		add_visb_file(File,LoadedFiles) :- member(File,LoadedFiles),!,
363		add_error(visb_visualiser,'Circular inclusion of JSON files:',[File|LoadedFiles]).
364		add_visb_file(File,_) :- \+ file_exists(File),!,
365		add_error(visb_visualiser,'JSON file does not exist:',File), fail.
366		add_visb_file(File,LoadedFiles) :-
367		debug_format(19,'Loading JSON File: ~w~n',[File]),
368		set_additional_filename_as_parsing_default(File,NewNr,OldNr),
369		call_cleanup(add_visb_file2(File,LoadedFiles), reset_filename_parsing_default(NewNr,OldNr)).
370
371		add_visb_file2(File,LoadedFiles) :-
372		json_parse_file(File,json(List2),[position_infos(true),multiline_strings(true)]),
373		% tools_printing:trace_print(List2),nl,nl,
374		process_json(List2,File),
375		!,
376		(get_attr_with_pos(include,List2,JsonFileTerm,File,Pos)
377		-> check_json_string(JsonFileTerm,include,Pos,JsonFile),
378		absolute_file_name(JsonFile,AF,[relative_to(File)]),
379		formatsilent('Including JSON file: ~w~n',[JsonFile]),
380		absolute_file_name(File,AbsFile), % File may be relative; we compare absolute paths to detect cycles
381		add_visb_file(AF,[AbsFile|LoadedFiles])
382		; true
383		),
384		(LoadedFiles=[], % only check for main included file
385	?	get_attr_with_pos('model-name',List2,string(ModelName),File,MPos),
386		b_machine_name(Main), Main \= ModelName
387		-> ajoin(['VisB JSON file expects model-name ',ModelName,' instead of: '],MMsg),
388		add_warning(visb_visualiser,MMsg,Main,MPos)
389		; true
390		).
391		add_visb_file2(File,_) :-
392		add_error(visb_visualiser,'Unable to process JSON file:',File),
393		fail.
394
395		% process json content of a VisB file:
396		process_json(List,JSONFile) :- visb_svg_file(_,_,_,_,_),!, % we have already determined the SVG file
397		process_json2(List,JSONFile).
398		process_json(List,JSONFile) :-
399	?	get_attr_with_pos(svg_box,List,json(BoxList),JSONFile,Pos),
400		% json([=(width,400,3-3),=(height,400,3-3)])
401	?	(get_attr(svg,List,string(SvgFile)) -> SvgFile='' ; true), % check if svg attr empty or non-existant
402		force_get_attr_nr(height,BoxList,H,JSONFile),
403		force_get_attr_nr(width,BoxList,W,JSONFile),!,
404		(get_attr(viewBox,BoxList,string(VB)) -> ViewBox=VB ; ViewBox=''),
405		add_message(visb_visualiser,'Will create empty SVG image with specified dimensions: ',H:W,Pos),
406		assert_visb_empty_svg_box_height_width(H,W,ViewBox,Pos),
407		process_json2(List,JSONFile).
408		process_json(List,JSONFile) :-
409	?	get_attr_with_pos(svg,List,FileTerm,JSONFile,Pos),
410		check_json_string(FileTerm,svg,Pos,File),
411		(File = '' -> get_default_visb_svg_file(SvgFile, _),
412		default_visb_svg_abs_file(SvgFile,AbsFile) % VISB_SVG_FILE is relative to the B machine
413		; get_default_visb_svg_file(SvgFile, DPos)
414		-> add_message(visb_visualiser,'Overriding svg file specified in JSON file: ',File,DPos),
415		default_visb_svg_abs_file(SvgFile,AbsFile)
416		; SvgFile=File,
417		absolute_file_name(SvgFile,AbsFile,[relative_to(JSONFile)])),
418		!,
419		add_visb_svg_file(SvgFile,AbsFile,JSONFile,Pos),
420		process_json2(List,JSONFile).
421		process_json(List,JSONFile) :-
422		get_default_visb_svg_file(SvgFile, Pos), SvgFile \= '',
423		!,
424		default_visb_svg_abs_file(SvgFile,AbsFile),
425		add_visb_svg_file(SvgFile,AbsFile,JSONFile,Pos),
426		process_json2(List,JSONFile).
427		process_json(List,JSONFile) :-
428		process_json2(List,JSONFile),
429		(get_SVG_BOX_definition(no_inlining) -> true % TODO: pass (InlineObjects)
430		; get_attr_with_pos(svg,List,_,JSONFile,Pos) -> % File is empty
431		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)
432		; add_warning(visb_visualiser,'Creating empty SVG image. The JSON file contains no svg attribute (pointing to the SVG file): ',JSONFile)
433		).
434
435		add_visb_svg_file(SvgFile,AbsFile,JSONFile,Pos) :-
436		(SvgFile='' -> add_message(visb_visualiser,'Empty VisB SVG file:',SvgFile,Pos),
437		ModLocTime=unknown
438		; file_exists(AbsFile)
439		-> debug_format(19,'SVG file = ~w (~w)~n',[SvgFile, AbsFile]),
440		file_property(AbsFile, modify_localtime, ModLocTime)
441		; add_error(visb_visualiser,'The specified VisB SVG file does not exist:',SvgFile,Pos),
442		ModLocTime=unknown
443		),
444		assertz(visb_svg_file(SvgFile,AbsFile,JSONFile,Pos,ModLocTime)).
445
446		process_json2(List,JSONFile) :-
447		process_json_definitions(List,JSONFile),
448		process_json_items(List,JSONFile),
449		process_json_events(List,JSONFile),
450		process_json_new_svg_objects(List,JSONFile).
451
452
453		% ----------------
454
455		% B definitions that can help write items, events more compactly
456		process_json_definitions(List,File) :-
457	?	get_attr(definitions,List,array(Defs)),!,
458		length(Defs,Len),
459		formatsilent('VisB Definitions: ~w~n',[Len]),
460		maplist(process_json_definition(File),Defs).
461		process_json_definitions(_,_File).
462
463		% VisB items which modify attributes of SVG objects
464		process_json_items(List,File) :-
465	?	get_attr(items,List,array(Items)),!,
466		length(Items,Len),
467		formatsilent('VisB Item declarations: ~w~n',[Len]),
468		maplist(process_visb_json_item(File),Items).
469		process_json_items(_,File) :- \+ visb_special_definition(visb_updates,_,_,_,_,_),!,
470		add_message(visb_visualiser,'The JSON file contains no items: ',File).
471		process_json_items(_,_).
472
473		% VisB events which react to clicks on SVG objects and display hovers
474		process_json_events(List,File) :-
475		get_attr(events,List,array(Items)),!,
476		length(Items,Len),
477		formatsilent('VisB Event declarations: ~w~n',[Len]),
478		maplist(process_json_event(File),Items).
479		process_json_events(_,_).
480
481		% VisB additional SVG objects added to SVG file
482		process_json_new_svg_objects(List,File) :-
483	?	get_attr(svg_objects,List,array(Items)),!,
484		length(Items,Len),
485		formatsilent('VisB additional svg_objects declarations: ~w~n',[Len]),
486		maplist(process_json_svg_object(File),Items).
487		process_json_new_svg_objects(List,File) :-
488		get_attr_with_pos(objects,List,array(Items),File,Pos),!,
489		add_warning(visb_visualiser,'Use "svg_objects" attribute instead of "objects" in: ',File,Pos),
490		maplist(process_json_svg_object(File),Items).
491		process_json_new_svg_objects(_,_).
492
493
494		% evaluate all VISB_SVG_OBJECTS... DEFINITIONS and try and extract SVG objects
495		% this must be a set of records with at least id and svg_class field
496		get_svg_objects_from_definitions(InlineObjects,ExpandedScope,_) :-
497	?	find_and_eval_visb_DEFINITION('VISB_SVG_OBJECTS', visb_objects, SVG_ID, AttrList, Desc, DefName,
498		_DefPos, EvalPos, InlineObjects, allow_separation, ExpandedScope),
499		%formatsilent('Generating new SVG object ~w with attrs ~w~n',[SVG_ID,AttrList]),
500		add_visb_object_from_definition(visb_objects, SVG_ID, AttrList, Desc, DefName, EvalPos),
501		fail.
502		get_svg_objects_from_definitions(InlineObjects,ExpandedScope,_) :-
503		find_and_eval_visb_DEFINITION('VISB_SVG_EVENTS', visb_events, SVG_ID, AttrList, Desc, DefName,
504		_DefPos, EvalPos, InlineObjects, no_separation, ExpandedScope),
505		% attributes: event or events, predicate
506		add_visb_object_from_definition(visb_events, SVG_ID, AttrList, Desc, DefName, EvalPos),
507		fail.
508		get_svg_objects_from_definitions(InlineObjects,ExpandedScope,_) :-
509	?	find_and_eval_visb_DEFINITION('VISB_SVG_HOVERS', visb_hovers, SVG_ID, AttrList, Desc, DefName,
510		_DefPos, EvalPos, InlineObjects, no_separation, ExpandedScope),
511		% attributes: id, trigger_id (optional), other SVG attributes
512	?	add_visb_hovers_from_definition(SVG_ID, AttrList, Desc, DefName, EvalPos),
513		fail.
514		get_svg_objects_from_definitions(_InlineObjects,ExpandedScope,JsonFileContext) :- % VISB_SVG_UPDATES
515		precompile_svg_object_updates(ExpandedScope,JsonFileContext).
516
517		% example definition VISB_SVG_HOVERS == rec(`id`:"myid", stroke:"black", stroke_exit:"gray");
518		% a hovers field inside VISB_SVG_OBJECTS can be something like:
519		% rec(.... hovers: (rec(class:"train-hover"),rec(trigger_id:"track_polyline",class:"train-hover")), ...)
520		% also used, e.g., as attribute in VISB_SVG_OBJECTS
521		add_visb_hovers_from_definition(SVG_ID,AttrList, Desc, DefName, DefPos) :-
522		select(svg_attribute(hovers,Hovers),AttrList,AttrList2),
523		!,
524		(AttrList2=[] -> true ; add_warning(visb_visualiser,'Unknown extra hover attributes:',AttrList2,DefPos)),
525		flex_member(Record,Hovers,DefName,DefPos),
526		(get_VISB_record_fields(Record,Fields) -> true
527		; add_warning(visb_visualiser,'VisB hovers field value is not a record of SVG attributes: ',Record,DefPos),fail),
528		include_maplist(extract_attribute_from_record(DefPos),Fields,HoverAttrList),
529		add_visb_object_from_definition(visb_hovers, SVG_ID, HoverAttrList, Desc, DefName, DefPos).
530		add_visb_hovers_from_definition(SVG_ID,AttrList, Desc, DefName, DefPos) :-
531	?	add_visb_object_from_definition(visb_hovers, SVG_ID, AttrList, Desc, DefName, DefPos).
532
533
534		% add a VisB record object from a HOVER or OBJECT definition:
535		add_visb_object_from_definition(visb_objects,SVG_ID, AttrList, Desc, DefName, DefPos) :- !,
536	?	(select(svg_attribute(svg_class,SVG_Class),AttrList,AttrList2)
537		-> true % maybe we should call svg_class svg_shape and
538		% allow html_tag for children of foreignObject
539		; add_warning(visb_visualiser,'SVG objects have no svg_class field: ',DefName,DefPos),
540		fail
541		),
542		assert_visb_svg_object(SVG_ID,SVG_Class,AttrList2,Desc,DefName,DefPos).
543		add_visb_object_from_definition(visb_hovers,SVG_ID, AttrList, _Desc, _DefName, DefPos) :- !,
544	?	(select(svg_attribute(trigger_id,TriggerID),AttrList,AttrList2) -> true
545		; select(svg_attribute('trigger-id',TriggerID),AttrList,AttrList2) -> true
546		; TriggerID = SVG_ID, AttrList2=AttrList),
547	?	member(svg_attribute(Attr,EnterVal),AttrList2), % will backtrack for every SVG attribute
548		\+ get_exit_attribute_name(_,Attr), % it is not an exit attribute
549		get_exit_attribute_name(Attr,AttrExitName),
550		(member(svg_attribute(AttrExitName,ExitVal), AttrList2) -> true % user specified exit value explicitly
551		; visb_svg_object(SVG_ID,_,StaticAttrList,_,ExitPos)
552		-> (member(svg_attribute(Attr,ExitVal),StaticAttrList) -> true % use value specified in VISB_SVG_OBJECTS
553		; default_attribute_value(Attr,ExitVal)
554		-> add_message(visb_visualiser,'Assuming default hover exit value for attribute: ',Attr,DefPos)
555		; Attr = 'svg_class'
556		-> add_warning(visb_visualiser,
557		'svg_class cannot be set in hover for: ',SVG_ID,ExitPos),
558		ExitVal=EnterVal
559		; (Attr = hover ; Attr = hovers) ->
560		add_error(visb_visualiser,
561		'Only provide SVG attributes here; no need to wrap them in this attribute:',Attr,DefPos),fail
562		; add_warning(visb_visualiser,
563		'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),
564		ExitVal=EnterVal
565		)
566		; ajoin(['No VISB_SVG_OBJECT for id ',SVG_ID,' and no value for ',AttrExitName,
567		'; cannot retrieve hover exit value for attribute: '],Msg),
568		add_warning(visb_visualiser,Msg,Attr,DefPos),
569		fail %ExitVal=EnterVal
570		),
571		assert_visb_hover(TriggerID,SVG_ID,Attr,EnterVal,ExitVal,DefPos).
572		add_visb_object_from_definition(visb_events,SVG_ID, AttrList, _Desc, DefName, DefPos) :- !,
573		( select(svg_attribute(event,Event),AttrList,AttrList1) -> true
574		; select(svg_attribute(events,Events),AttrList,AttrList1) -> % we have events attributes with multiple events
575		flex_member(EvVal,Events,DefName,DefPos),
576		extract_attr_value(event,EvVal,Event,DefPos)
577		; AttrList = [_|_], % at least one other attribute than id; otherwise it may stem from separating VISB_SVG_OBJECTS
578		add_warning(visb_visualiser,'Missing event attribute in VisB definition: ',DefName,DefPos),
579		fail
580		),
581		(select(svg_attribute(predicate,Pred),AttrList1,AttrList2) -> Preds=[Pred]
582		; member(P,[preds,predicates]),
583		select(svg_attribute(P,Pred),AttrList1,AttrList2)
584		-> Preds=[Pred], add_warning(visb_visualiser,'Use predicate as attribute for VisB events instead of: ',P,DefPos)
585		; Preds=[], AttrList2=AttrList1
586		),
587		(select(svg_attribute(execution_kind,EKind),AttrList2,AttrList3)
588		-> check_execution_kind(EKind,SVG_ID,DefPos,ExecKind)
589		; default_execution_kind(ExecKind), AttrList3=AttrList2
590		),
591		EnableItems=[],
592		maplist(warn_remaining_attributes(DefName,DefPos),AttrList3),
593		% TODO extract from AttrList2: visb_enable_item(SvgID,Attr,EnabledValExpr,DisabledValExpr,PosAttr)
594		(error_manager:extract_file_number_and_name(DefPos,_,File) -> true ; File='?'),
595		PredPos = DefPos, %TODO: improve
596		add_visb_event(SVG_ID,Event,Preds,ExecKind,[],EnableItems,File,DefPos,PredPos,[]).
597		add_visb_object_from_definition(SpecialClass,_, _, _, _DefName, DefPos) :-
598		add_warning(visb_visualiser,'Unknown special class, cannot add VisB objects for definition: ',SpecialClass,DefPos).
599
600		% for hovers allow to explicitly specify exit value, in case the SVG object comes from an SVG file
601		get_exit_attribute_name(Attr,ExitAttr) :- atom_concat(Attr,'_exit',ExitAttr).
602
603		warn_remaining_attributes(DefName,DefPos,svg_attribute(hover,_)) :- !,
604		add_warning(visb_visualiser,'Attribute hover not supported here (use separate VISB_SVG_HOVERS definition): ',DefName,DefPos).
605		warn_remaining_attributes(DefName,DefPos,svg_attribute(hovers,_)) :- !,
606		add_warning(visb_visualiser,'Attribute hovers not supported here (use separate VISB_SVG_HOVERS definition): ',DefName,DefPos).
607		warn_remaining_attributes(_,DefPos,Attr) :-
608		add_warning(visb_visualiser,'Unrecognised attribute in VISB_SVG_EVENTS definition: ',Attr,DefPos).
609
610
611		default_attribute_value(fill,black). % is remove for animate, ...
612		default_attribute_value(opacity,1).
613		default_attribute_value('stop-dasharray',none).
614		default_attribute_value('stop-opacity',1).
615		default_attribute_value('stroke-opacity',1).
616		default_attribute_value('stroke-width','1px').
617		default_attribute_value(stroke,none).
618		default_attribute_value(transform,none).
619		default_attribute_value(visibility,visible).
620
621		% is called in process_json when no SVG file specified
622		% VISB_SVG_BOX == rec(width:1000,height:1000,viewBox:"minx miny w h"),
623		get_SVG_BOX_definition(InlineObjects) :-
624	?	get_and_eval_special_definition('VISB_SVG_BOX','VISB_SVG_BOX',visb_box,DefPos,ResValue,InlineObjects),
625		(ResValue=(BH,BW) -> ViewBox=''
626		; get_VISB_record_fields(ResValue,Fields),
627	?	select(field(height,BH),Fields,F1),
628	?	select(field(width,BW),F1,F2)
629	?	-> (select(field(viewBox,VBVal),F2,F3)
630		-> (VBVal=string(VB) -> ViewBox=VB
631		% Viewbox is "mx my w h" string, ie: minimum_x, minimum_y, width and height
632		; VBVal = rec(VBFields)
633		-> (VBFields = [field(height,_),field(minx,_),field(miny,_),field(width,_)]
634		-> (get_view_box_rec(VBFields,DefPos,ViewBox) -> true ; ViewBox='') % error already reported
635		; ViewBox='',
636		add_warning(visb_visualiser,'VISB_SVG_BOX viewBox record has illegal fields (expected minx miny width height):',VBVal,DefPos))
637		; add_warning(visb_visualiser,'VISB_SVG_BOX viewBox is not a string ("minx miny width height") or record:',VBVal,DefPos),
638		ViewBox=''
639		)
640		; ViewBox='', F3=F2
641		),
642		(F3=[] -> true
643		; add_warning(visb_visualiser,'VISB_SVG_BOX unknown attributes (not height, width, viewBox): ',F3,DefPos))
644		; add_error(visb_visualiser,'Ignoring VISB_SVG_BOX, must be record or pair of integers (height,width):',ResValue,DefPos),
645		fail),
646		(get_number_from_bvalue(BH,H) -> true
647		; add_error(visb_visualiser,'Ignoring VISB_SVG_BOX, height is not a number:',ResValue,DefPos), fail),
648		(get_number_from_bvalue(BW,W) -> true
649		; add_error(visb_visualiser,'Ignoring VISB_SVG_BOX, width is not a number:',ResValue,DefPos), fail),
650		!,
651		assert_visb_empty_svg_box_height_width(H,W,ViewBox,DefPos).
652
653		get_view_box_rec([field(height,VH),field(minx,MXH),field(miny,MYH),field(width,VW)],DefPos,ViewBoxString) :-
654		(get_number_from_bvalue(VH,Height) -> true
655		; add_error(visb_visualiser,'VISB_SVG_BOX viewBox\'height is not a number:',VH,DefPos),fail),
656		(get_number_from_bvalue(VW,Width) -> true
657		; add_error(visb_visualiser,'VISB_SVG_BOX viewBox\'width is not a number:',VW,DefPos),fail),
658		(get_number_from_bvalue(MXH,MinX) -> true
659		; add_error(visb_visualiser,'VISB_SVG_BOX viewBox\'minx is not a number:',MXH,DefPos),fail),
660		(get_number_from_bvalue(MYH,MinY) -> true
661		; add_error(visb_visualiser,'VISB_SVG_BOX viewBox\'miny is not a number:',MYH,DefPos),fail),
662		ajoin([MinX,' ',MinY,' ', Width,' ',Height],ViewBoxString).
663
664
665		assert_visb_empty_svg_box_height_width(H,W,_ViewBox,Pos) :-
666		retract(visb_empty_svg_box_height_width(OldH,OldW,_)),
667		(OldH,OldW) \= (H,W),
668		add_message(visb_visualiser,'Overriding VisB SVG_BOX default dimensions: ',(OldH,OldW),Pos),
669		fail.
670		assert_visb_empty_svg_box_height_width(H,W,ViewBox,_Pos) :-
671		%add_message(visb_visualiser,'Setting VisB SVG_BOX default dimensions: ',(H,W,ViewBox),Pos),
672		assert(visb_empty_svg_box_height_width(H,W,ViewBox)).
673
674
675		% find DEFINITION with given prefix in name, evaluate it and return SVG_ID and attribute list:
676		% AllowSep = allow_seperation means that the record fields can be separated into static objects and dynamic updates
677		% and only static ones will be retained (dynamic ones dealt with later)
678		find_and_eval_visb_DEFINITION(DEFPREFIX, Kind, SVG_ID, AttrList,Desc, DefName, DefPos,EvalPos,
679		InlineObjects,AllowSep,ExpandedScope) :-
680	?	( b_sorted_b_definition_prefixed(expression,DEFPREFIX,DefName,DefPos),
681	?	if(b_get_typed_definition(DefName,ExpandedScope,Body),true,
682		(add_visb_lint_message('Ignoring VisB DEFINITION due to errors',DefName,DefPos),fail))
683		; special_backup(DEFPREFIX,Kind),
684		% also look at stored definitions (e.g., from static/dynamic separation of VISB_SVG_OBJECTS)
685		visb_special_definition(Kind,DefName,_Type,Body,_Class,DefPos)
686		),
687		set_error_context(visb_error_context(definition,DefName,'all_attributes',DefPos)),
688	?	call_cleanup((get_typed_static_definition_with_constants_state(DefName,Body,
689		ResBody,DefPos,ConstState,InlineObjects,AllowSep),
690		(get_texpr_pos(ResBody,Pos0) -> true ; Pos0=DefPos), % this could be a part of the full definition body
691		get_visb_DEFINITION_svg_object(Kind,DefName,ResBody,Pos0,ConstState,SVG_ID,AttrList,Desc,EvalPos)),
692		clear_error_context).
693
694		special_backup('VISB_SVG_HOVERS',visb_hovers).
695
696		% evaluate a typed body expressions evaluating to a record or set of records
697		% and translate into SVG attribute lists:
698		get_visb_static_svg_object_for_typed_expr(Kind,DefName,Body,DefPos,SVG_ID,AttrList,Desc,InnerPos) :-
699		AllowSep=no_separation,
700		Inline=no_inlining,
701		get_typed_static_definition_with_constants_state(DefName,Body,ResBody,DefPos,ConstState,Inline,AllowSep),
702		get_visb_DEFINITION_svg_object(Kind,DefName,ResBody,DefPos,ConstState,SVG_ID,AttrList,Desc,InnerPos).
703
704
705		flatten_couple(b(couple(A,B),_,_)) --> !,flatten_couple(A),flatten_couple(B).
706		% we could also flatten union(A,B), but at the risk of duplicate warnings when the same element occurs in A and B
707		flatten_couple(A) --> [A].
708
709		get_typed_static_definition_with_constants_state(DefName,Body,ResBody,DefPos,ConstantsState,InlineObjects,AllowSep) :-
710		flatten_couple(Body,TupleList,[]),
711		% the VISB_SVG_OBJECT definition may consist of a tuple (Obj1,Obj2,...) to allow grouping
712		(TupleList = [_,_|_]
713		-> add_debug_message(visb_visualiser,'Decomposed VisB definition body tuple:',DefName,DefPos)
714		; true),
715	?	nth1(DefNr,TupleList,TupleBody),
716		(get_texpr_pos(TupleBody,TuplePos) -> true ; TuplePos=DefPos),
717		get_typed_static_definition_with_constants_state3(DefName,DefNr,TupleBody,ResBody,TuplePos,
718		ConstantsState,InlineObjects,AllowSep).
719		get_typed_static_definition_with_constants_state3(DefName,DefNr,Body,ResBody,DefPos,ConstantsState,InlineObjects,AllowSep) :-
720		determine_type_of_visb_formula(Body,TIds,Class),
721		debug_format(19,'Detected VisB DEFINITION ~w (~w)~n',[DefName,Class]),
722		(%Class=requires_variables, % now also useful if event field present
723		AllowSep=allow_separation, % allowed for VISB_SVG_OBJECTS
724	?	if(separate_into_static_and_dynamic_part(DefName,DefNr,Body,StaticBody,DynamicBody,EventBody,HoverBody),
725		true,
726		(get_texpr_type(Body,Type),
727		(contains_events_or_hovers_field(Type)
728		-> add_warning(visb_visualiser,'Static/Dynamic separation failed for (required for events or hovers): ',DefName,DefPos)
729		% VISB_SVG_OBJECT definition contains events/hovers and as such requires separation; which failed here
730		; add_debug_message(visb_visualiser,'Static/Dynamic separation failed or not useful for: ',DefName,DefPos)
731		),
732		fail)),
733		determine_type_of_visb_formula(StaticBody,SIds,SClass),
734		get_unique_initial_state_for_visb(SClass,DefName,DefPos,SIds,ConstantsState)
735		-> Separated=true, ResBody=StaticBody,
736		add_debug_message(visb_visualiser,'Automatically separated fields into static and dynamic: ',DefName,DefPos),
737		%write('STATIC: '),translate:print_bexpr(StaticBody),nl, write('DYNAMIC: '),translate:print_bexpr(DynamicBody),nl,
738		assert_visb_udpate_def_body(visb_updates,DefName,DynamicBody,DefPos),
739		add_visb_events_from_def_body(visb_events,DefName,EventBody,DefPos),
740		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
741		; get_unique_initial_state_for_visb(Class,DefName,DefPos,TIds,ConstantsState)
742		-> ResBody=Body
743		; ResBody=Body,
744		(Class=requires_constants ->
745		get_texpr_ids(TIds,Ids),
746		% we could check if values of Ids are identical in all constants solutions
747		(is_concrete_constants_state_id(_)
748		-> BMsg='multiple solutions for used constants exist: '
749		; \+ root_sufficiently_explored
750		-> BMsg='no constants were setup yet: '
751		% two cases below should not happen; but happen on Linux with CSP||B models
752		; state_space:logical_transition_from_root(RID),
753		state_space:packed_visited_expression(RID,RSt),
754		functor(RSt,RFun,RArity)
755		-> ajoin(['no constants were found, but logical successor ',RFun,'/',RArity,
756		' with id ', RID,' of root exists: '],BMsg)
757		; BMsg='no constants were found: '
758		),
759		ajoin(['DEFINITION ',DefName, ' requires constants but ',BMsg],Msg),
760		(get_a_constants_state(ConstantsState,StateID,InlineObjects)
761		-> (member(CstID,Ids),
762		other_constant_value_exists_for(CstID,ConstantsState,StateID)
763		-> add_warning(visb_visualiser,Msg,CstID,DefPos)
764		; ajoin(['DEFINITION ',DefName,
765		' requires constants and all SETUP_CONSTANTS solutions have same value thus far: '],Msg2),
766		% constraint-based checks or execute by predicate could later create others !
767		add_message(visb_visualiser,Msg2,Ids,DefPos)
768		)
769		; add_error(visb_visualiser,Msg,Ids,DefPos),
770		fail % avoid other subsequent errors when evaluating with ConstantsState=[]
771		)
772		; ConstantsState=[]
773		)
774		),
775		(Class=requires_variables, Separated=false
776		-> get_texpr_ids(TIds,AIds),
777		include(b_is_variable,AIds,VIds),
778		ajoin_with_sep(VIds,',',SVids),
779		(get_preference(visb_allow_variables_for_objects,false)
780		-> ajoin(['Ignoring DEFINITION which requires variables ',SVids,': '],WMsg),
781		add_warning(visb_visualiser,WMsg,DefName,DefPos),fail
782		; ConstantsState=[]
783		-> add_warning(visb_visualiser,'Ignoring DEFINITION which requires variables, could not find unique initial state: ',DefName,DefPos),fail
784		; ajoin(['DEFINITION requires variables ',SVids,
785		'; exporting history to HTML may not work correctly'],WMsg),
786		add_visb_lint_message(WMsg,DefName,DefPos)
787		)
788		; true).
789
790
791		% separate/split/filter VISB_SVG_OBJECTS definitions into a static part and a dynamic part depending on variables
792		% (aka updates/items)
793		separate_into_static_and_dynamic_part(DefName,DefNr,Body,StaticBody,DynamicBody,EventBody,HoverBody) :-
794	?	separate_static_dyn_aux(DefName,DefNr,[],[],Body,StaticBody,DynamicBody,EventBody,HoverBody).
795
796
797		rewrite_expression(let_expression(Ids,Exprs,Body),NewBody) :-
798		% currently we cannot process LET's here, expand them
799		replace_ids_by_exprs(Body,Ids,Exprs,NewBody). % see also expand_all_lets/2
800
801		separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,Path,b(Expr,_Type,_Info), Static,Dynamic,Event,Hover) :-
802		rewrite_expression(Expr,NewExpr),!,
803		separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,Path,NewExpr, Static,Dynamic,Event,Hover).
804		separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,Path,b(couple(A,B),_,_Info),
805		StaticCouple,DynamicCouple,EventCouple,HoverCouple) :- !,
806		separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,[0|Path],A,SA,DA,EA,HA),
807		separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,[1|Path],B,SB,DB,EB,HB),
808		create_couple(SA,SB,StaticCouple),
809		create_couple(DA,DB,DynamicCouple),
810		create_couple(EA,EB,EventCouple),
811		create_couple(HA,HB,HoverCouple).
812		separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,Path,TExpr,
813		b(StaticSetComp,set(ST),I),
814		b(DynamicSetComp,set(DT),I),
815		b(EventsSetComp,set(ET),I),
816		b(HoversSetComp,set(HT),I)) :-
817	?	bsyntaxtree:is_eventb_comprehension_set(TExpr,Ids,Pred,Expr),
818		(OuterQuantifiedIds = []
819		-> add_debug_message(visb_visualiser,'Top-level set comprehensions for VISB: ',Ids,TExpr)
820		; add_message(visb_visualiser,'Nested set comprehensions for VISB: ',OuterQuantifiedIds,TExpr)
821		),
822		!,
823		determine_type_of_visb_formula(b(exists(Ids,Pred),pred,[]),SIds,Class),
824		(get_unique_initial_state_for_visb(Class,DefName,Pred,SIds,_)
825		-> true % The predicate must be statically executable
826		; time_out_for_node(root,O,_Type),
827		translate_operation_name(O,Op) ->
828		ajoin(['Due to TIME_OUT of ',Op,' the comprehension set domain cannot be evaluated: '],Msg),
829		add_warning(visb_visualiser,Msg,Pred,Pred),
830		% TODO: avoid other error messages that will occur after that
831		fail
832		; (root_sufficiently_explored -> RMsg = '' ; RMsg = ' because constants were not set up yet'),
833		(multiple_concrete_constants_exist -> MMsg = ',multiple SETUP_CONSTANTS exist' ; MMsg = ''),
834		ajoin(['Cannot evaluate comprehension set domain (',Class,MMsg,')',RMsg],LMsg),
835		add_visb_lint_message(LMsg,Pred,Pred),
836		% at the moment we require the domain to be computable statically for both static/dynamic attributes
837		fail
838		),
839		append(OuterQuantifiedIds,Ids,NewOuterQuantifiedIds),
840	?	separate_static_dyn_aux(DefName,DefNr,NewOuterQuantifiedIds,Path,Expr,
841		StaticRec,DynamicRec,EventRec,HoverRec),
842		get_texpr_type(StaticRec,ST),
843		get_texpr_type(DynamicRec,DT),
844		get_texpr_type(EventRec,ET),
845		get_texpr_type(HoverRec,HT),
846		bsyntaxtree:get_texpr_info(TExpr,I),
847		b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,StaticRec,Pred, set(ST), StaticSetComp),
848		b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,DynamicRec,Pred,set(DT), DynamicSetComp),
849		b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,EventRec,Pred,set(ET), EventsSetComp),
850		b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,HoverRec,Pred,set(HT), HoversSetComp).
851		separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,Path,b(rec(Fields),_,Info),
852		b(rec(StaticFields),record(SFT),Info), % VISB_OBJECTS (static)
853		b(UpdateRecWithDynamicFields,record(DFT),Info), % VISB_UPDATES (dynamic)
854		b(rec(AllEventFields),record(EFT),Info), % VISB_EVENTS
855		b(rec(AllHoverFields),record(HFT),Info) % VISB_HOVERS
856		) :- !,
857		split_list(is_visb_event_field,Fields,EventFields,ObjectAndHoverFields),
858		(select(field(hovers,HoverRec),ObjectAndHoverFields,ObjectFields)
859		-> HoverFields = [field(hovers,HoverRec)] % record deconstructed in add_visb_hovers_from_definition
860		; ObjectFields=ObjectAndHoverFields, HoverFields = []),
861		% 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
862		separate_fields(ObjectFields,StaticFields0,DynamicFields,DefName),
863	?	(member(field(svg_class,_SVG_Class),StaticFields0) -> true
864		; member(field(svg_class,SVG_Class),DynamicFields)
865		-> add_warning(visb_visualiser,'SVG svg_class field is not static in: ',DefName,SVG_Class),
866		fail
867		; add_warning(visb_visualiser,'No svg_class field in: ',DefName,Info),
868		fail
869		),
870	?	(member(field(id,SVGID),StaticFields0)
871		-> (DynamicFields \= [] ; EventFields \= [] ; HoverFields \= [] % separation is useful for this record
872		; Path \= [] % we are part of a couple; maybe other records have a dynamic,event or hover part; so proceed
873		),
874		StaticFields = StaticFields0,
875		TStatic_SVGID = SVGID
876		; member(field(id,SVGID),DynamicFields)
877		-> add_warning(visb_visualiser,'SVG id field is not static in: ',DefName,SVGID),
878		fail
879		; OuterQuantifiedIds = []
880		-> gensym(svg_id,GenID),
881		ajoin(['Generated id ',GenID, ' for SVG object without id field in: '],Msg),
882		add_debug_message(visb_visualiser,Msg,DefName,Info),
883		SVGID = b(string(GenID),string,[]),
884		sort([field(id,SVGID) | StaticFields0],StaticFields)
885		; % the record is quantified within a set comprehension; we need to compute the ID from OuterQuantifiedIds
886		% it has to be identical for VISB_SVG_OBJECTS and VISB_SVG_UPDATES
887		SVGID = b(ExtFunCall,string,[]),
888		convert_path_to_int(Path,IntPath),
889		PathExpr = b(integer(IntPath),integer,[]),
890		create_couple([b(string(DefName),string,[]),b(integer(DefNr),integer,[]),PathExpr|OuterQuantifiedIds],Tuple),
891		% add DefName and DefNr to avoid clash if other Definition has same quantified ids
892		ExtFunCall = external_function_call('SHA_HASH_HEX',[Tuple]),
893		ajoin(['Generated call to compute id for SVG object without id field in ',DefName,': '],Msg),
894		add_debug_message(visb_visualiser,Msg,SVGID,Info),
895		sort([field(id,SVGID) | StaticFields0],StaticFields)
896		),
897		maplist(get_field_type,StaticFields,SFT),
898		( (select(field(visibility,VisibExpr),DynamicFields,RestDynamicFields)
899		; member(field(visibility,VisibExpr),StaticFields0), % the visibility expression is static
900		RestDynamicFields = DynamicFields
901		),
902		RestDynamicFields = [_|_],
903		\+ hovers_can_set_visibility(HoverFields),
904		(nonvar(TStatic_SVGID), TStatic_SVGID = b(string(Static_SVGID),_,_) % TODO: evaluate properly
905		-> \+ visb_has_visibility_hover(Static_SVGID) % TODO: check no other hover definition added later
906		; true) % the ID is generated and cannot be accessed by other hovers which could make object visible
907		-> % create IF-THEN-ELSE to avoid evaluating fields when object not visible; also fixes WD issues
908		TRUE = b(boolean_true,boolean,[]),
909		sort([field(id,SVGID),field(visibility,TRUE)|RestDynamicFields],AllDynamicFields),
910		maplist(construct_dummy_value,RestDynamicFields,RestDummyFields),
911		sort([field(id,SVGID),field(visibility,b(boolean_false,boolean,[]))|RestDummyFields],AllDummyFields),
912		create_visibility_check(VisibExpr,VisibilityCond),
913		UpdateRecWithDynamicFields = if_then_else(VisibilityCond,
914		b(rec(AllDynamicFields),record(DFT),Info),
915		b(rec(AllDummyFields),record(DFT),Info)),
916		add_debug_message(visb_visualiser,'Refactoring VisB Record with visibility attribute: ',VisibilityCond)
917		% ,translate:print_bexpr(b(UpdateRecWithDynamicFields,any,[])),nl
918		; sort([field(id,SVGID)|DynamicFields],AllDynamicFields), % TODO: use kernel_records
919		UpdateRecWithDynamicFields = rec(AllDynamicFields)
920		),
921		maplist(get_field_type,AllDynamicFields,DFT),
922		sort([field(id,SVGID)|EventFields],AllEventFields), % ditto
923		maplist(get_field_type,AllEventFields,EFT),
924		sort([field(id,SVGID)|HoverFields],AllHoverFields), % ditto
925		maplist(get_field_type,AllHoverFields,HFT).
926		separate_static_dyn_aux(DefName,DefNr,OuterQuantifiedIds,_Path,TEXPR, _, _, _,_) :-
927		ajoin(['Uncovered expression for ',DefName,'-',DefNr,' ',OuterQuantifiedIds],Msg),
928		add_debug_message(visb_visualiser,Msg,TEXPR,TEXPR),fail.
929
930		hovers_can_set_visibility(HoverFields) :- member(field(hovers,Expr),HoverFields),
931		hover_expr_can_set_visibility(Expr).
932
933		hover_expr_can_set_visibility(b(E,_,_)) :- hovers_can_set_visib_aux(E).
934		hovers_can_set_visib_aux(couple(A,B)) :- !, (hover_expr_can_set_visibility(A) ; hover_expr_can_set_visibility(B)).
935		hovers_can_set_visib_aux(rec(Fields)) :- !, member(field(visibility,_),Fields).
936		hovers_can_set_visib_aux(set_extension(L)) :- !, member(E,L), hover_expr_can_set_visibility(E).
937		hovers_can_set_visib_aux(E) :- debug_format(19,'Assuming hover can set visibility: ~w~n',[E]).
938		% TODO: synchronise with flex_expand and check we cover all relevant cases like partial functions
939
940
941		create_visibility_check(VisibExpr,VisibilityCond) :- get_texpr_type(VisibExpr,string),!,
942		static_check_attribute_value_expression(visibility,VisibExpr),
943		VISIBLE = b(string('visible'),string,[]),
944		create_equality(VisibExpr,VISIBLE,VisibilityCond).
945		create_visibility_check(VisibExpr,VisibilityCond) :- get_texpr_type(VisibExpr,boolean),!,
946		TRUE = b(boolean_true,boolean,[]),
947		create_equality(VisibExpr,TRUE,VisibilityCond).
948		create_visibility_check(VisibExpr,b(truth,pred,[])) :-
949		add_warning(visb_visualiser,'The attribute visibility is not of type STRING or BOOL: ',VisibExpr,VisibExpr).
950
951
952		construct_dummy_value(field(Name,TExpr),field(Name,b(value(DummyValue),Type,[]))) :-
953		get_texpr_type(TExpr,Type),
954		get_default_or_dummy_value(Type,Name,DummyValue). % object not visible: do not evaluate expression; use dummy value
955
956		get_default_or_dummy_value(string,Name,DummyValue) :-
957		svg_attribute_default_value(Name,Default),!,
958		DummyValue=string(Default).
959		get_default_or_dummy_value(Type,_Name,DummyValue) :- any_value_for_type(Type,DummyValue).
960
961
962		% 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]
963		convert_path_to_int([],1).
964		convert_path_to_int([H|T],Res) :- convert_path_to_int(T,IT),
965		Res is IT*2+H.
966
967		% is the name of a field for events inside a VISB_SVG_OBJECT record
968		% example rec(..., event:"BOperation", predicate:"x=TRUE")
969		is_visb_event_field(field(Name,_)) :- is_visb_event_field_name(Name).
970		is_visb_event_field_name(event).
971		is_visb_event_field_name(events). % tuple or set of events inside VISB_SVG_OBJECTS
972		is_visb_event_field_name(predicate).
973		is_visb_event_field_name(predicates). % will generate warning
974		is_visb_event_field_name(preds). % will generate warning
975		is_visb_event_field_name(execution_kind).
976		% is the name of a field for hovers inside a VISB_SVG_OBJECT record
977		is_visb_hover_field_name(hovers).
978		is_visb_hover_field_name(items). % enable items
979		%is_visb_hover_field_name(optional). % not needed ?
980		%is_visb_hover_field_name(override). % not needed ?
981
982		% check if the type of a VISB_SVG_OBJECTS expression requires separation for hovers/events
983		contains_events_or_hovers_field(set(X)) :- contains_events_or_hovers_field(X).
984		contains_events_or_hovers_field(couple(A,B)) :-
985		(contains_events_or_hovers_field(A) -> true ; contains_events_or_hovers_field(B)).
986	?	contains_events_or_hovers_field(record(F)) :- member(field(Name,_),F),
987		(is_visb_event_field_name(Name) -> true ; is_visb_hover_field_name(Name)).
988
989		get_field_type(field(Name,Expr),field(Name,T)) :- get_texpr_type(Expr,T).
990
991		% separate fields from a SVG/VISB_SVG_OBJECT record into static part and dynamic update expressions
992		separate_fields([],[],[],_).
993		separate_fields([field(Field,Expr)|T],[field(Field,Expr)|TS],TD,DefName) :-
994		is_static_expr(Expr,Field,DefName),!,
995		separate_fields(T,TS,TD,DefName).
996		separate_fields([field(Field,Expr)|T],[field(Field,Default)|TS],[field(Field,Expr)|TD],DefName) :-
997		requires_static_default_value(Field,Default), !,
998		separate_fields(T,TS,TD,DefName).
999		separate_fields([H|T],TS,[H|TD],DefName) :-
1000		separate_fields(T,TS,TD,DefName).
1001
1002		% fields which require a static default value; here to set up child SVG objects of title
1003		% static default values could also be useful for hovers in general?
1004		requires_static_default_value(title,b(string('-title-not-set-'),string,[])).
1005
1006		% virtual SVG attributes which are translated to children tags/objects
1007		attribute_automatically_creates_children(title).
1008
1009		is_static_expr(Expr,Field,DefName) :-
1010		determine_type_of_visb_formula(Expr,_TIds,Class), % TODO pass local variables from exists above
1011		(Class=requires_nothing -> true
1012		; Class=requires_constants,
1013		\+ multiple_concrete_constants_exist, % TODO: check if _TIds have multiple solutions
1014		is_concrete_constants_state_id(_) -> true
1015		; ajoin(['Detected dynamic expression for field ',Field,' in ',DefName,': '],Msg),
1016		add_debug_message(visb_visualiser,Msg,Expr,Expr),fail
1017		).
1018
1019		% --------
1020
1021
1022		extract_attribute_from_record(_,field(OrigName,Value),_) :-
1023		opt_rewrite_field_name(OrigName,Name),
1024		deconstruct_singleton_set(Name,Value,'$optional_field_absent'),
1025		!, fail. % optional field (e.g., in TLA+) not present; no error
1026		extract_attribute_from_record(DefPos,field(OrigName,Value),svg_attribute(Name,SVal)) :-
1027		opt_rewrite_field_name(OrigName,Name),
1028		extract_attribute_value(DefPos,Name,Value,SVal).
1029		extract_attribute_from_record(DefPos,F,_) :-
1030		add_error(visb_visualiser,'Extract SVG attribute failed: ',F,DefPos),fail.
1031
1032		% extract a value for a particular field Name
1033		extract_attribute_value(DefPos,Name,Value,SVal) :-
1034		(deconstruct_singleton_set(Name,Value,Element)
1035		-> Element \= '$optional_field_absent',
1036		extract_attr_value(Name,Element,SVal,DefPos)
1037		; extract_attr_value(Name,Value,SVal,DefPos)
1038		).
1039
1040
1041		% in TLA+ mode optional record fields have {TRUE|->VALUE} rather than VALUE
1042		% this can also be useful in B to allow mixing different SVG records in a set
1043		% for Alloy mode we may want to also support singleton sets as scalars
1044		deconstruct_singleton_set(Name,Set,Res) :-
1045		singleton_set(Set,El),
1046		detect_partial_records_for_field(Name),
1047		(El=(pred_true,El2)
1048		-> Val=El2 % TLA2B encoding for optional fields that are present
1049		; Val=El), % Alloy
1050		!,
1051		Res = Val.
1052		deconstruct_singleton_set(Name,[],Res) :-
1053		detect_partial_records_for_field(Name),
1054		Res = '$optional_field_absent'.
1055
1056		detect_partial_records_for_field(points) :- !, fail. % can be set of points
1057		detect_partial_records_for_field(children) :- !, fail. % children field for groups is a set of ids
1058		detect_partial_records_for_field(Name) :-
1059		is_svg_number_attribute(Name),!. % sets never sensible as a numerical value
1060		detect_partial_records_for_field(Name) :- is_id_or_text_attribute(Name),!. % ditto for ids
1061		detect_partial_records_for_field(Name) :- is_svg_color_attribute(Name),!. % ditto for colors
1062		detect_partial_records_for_field(_) :-
1063		\+ classical_b_mode. % TODO: check that we are in TLA or Alloy mode?
1064		% TODO: ensure ProB2 sets animation minor mode for TLA
1065
1066
1067		extract_attr_value(Name,Value,SVal,DefPos) :-
1068		is_svg_number_attribute(Name),!, % we could try and extract svg_class from attribute list above
1069		(get_number_from_bvalue(Value,NrVal)
1070		-> SVal=NrVal % convert to atom?
1071		; b_value_to_string(Value,SVal),
1072		(is_special_svg_number_form(SVal) -> true
1073		; atom_codes(SVal,CC),
1074		safe_number_codes(_NrVal,CC) -> true
1075		; ajoin(['The value of the SVG attribute "',Name,
1076		'" is not a number: '],Msg),
1077		add_warning(visb_visualiser,Msg,SVal,DefPos)
1078		)
1079		).
1080		extract_attr_value(children,Value,SVal,DefPos) :- !,
1081		(is_set_value(Value,extract_attr_value)
1082		-> (try_expand_custom_set_with_catch(Value,ExpandedSet,extract_attr_value),
1083		maplist(b_value_to_id_string,ExpandedSet,SVal) -> true
1084		; add_warning(visb_visualiser,'The children attribute should be a finite set of identifiers: ',Value,DefPos),
1085		SVal=[]
1086		)
1087		; add_warning(visb_visualiser,'The children attribute should be a set of identifiers: ',Value,DefPos),
1088		SVal=[]).
1089		extract_attr_value(points,Value,SVal,DefPos) :- % Class should be polygon or polyline
1090		% automatically translate sequences or sets of pairs of numbers to SVG string format
1091		(Value = [(Nr,_)|_] ; Value = avl_set(node((Nr,_),_,_,_,_))),
1092		is_number(Nr), % TODO: check typing
1093		svg_points(Value,Str,DefPos,no_wf_available),!,
1094		string(SVal)=Str.
1095		extract_attr_value(points,Value,SVal,_DefPos) :- Value = [],!, SVal = ''.
1096		extract_attr_value(visibility,Value,SVal,DefPos) :- !,
1097		% convert TRUE -> visible, FALSE -> hidden
1098		( Value=pred_true -> TxtVal='visible'
1099		; Value=pred_false -> TxtVal='hidden'
1100		; b_value_to_string(Value,TxtVal),
1101	?	(member(TxtVal,[collapse,hidden,visible]) -> true
1102		; add_warning(visb_visualiser,'Value of SVG attribute "visibility" must be collapse,hidden or visible and not: ',TxtVal,DefPos))
1103		),
1104		SVal=TxtVal.
1105		extract_attr_value(Name,Value,_,DefPos) :-
1106		check_svg_attribute_value(Name,Value,DefPos),fail.
1107		extract_attr_value(Name,Value,SVal,_) :-
1108	?	is_id_or_text_attribute(Name),!,
1109		(Name=text -> b_value_to_string(Value,SVal) % a pure text field; you probably want to see the B value
1110		; is_text_attribute(Name) % something like transform, predicate, event; here maybe automatic concat can be useful
1111		-> b_value_to_attr_string(Value,SVal)
1112		; b_value_to_id_string(Value,SVal)). % concatenates e.g. pairs of strings to string without ( |-> )
1113		extract_attr_value(Attr,RawValue,ResValue,_DefPos) :- raw_value_attribute(Attr),!, % keep value intact
1114		ResValue = RawValue.
1115		extract_attr_value(_Name,Value,SVal,_DefPos) :-
1116		b_value_to_string(Value,SVal).
1117
1118		% visb_visualiser:extract_attr_value(text,avl_set(node((fd(1,'Kunden'),int(0)),true,0,empty,empty)),S,unknown).
1119
1120		is_number(int(_)).
1121		is_number(term(floating(_))).
1122
1123		% do not convert to string; these are treated separately
1124		raw_value_attribute(hovers).
1125		raw_value_attribute(events).
1126
1127
1128		% evaluate a DEFINITION to a set of B records representing SVG objects
1129		% returns a possibly refined sub-position corresponding to generated SVG objects as last argument
1130		get_visb_DEFINITION_svg_object(SpecialClass,DefName,Body,_DefPos,ExpandedState,SVG_ID,AttrList,Desc,InnerPos) :-
1131		get_preference(visb_show_debug_infos,true),
1132		bsyntaxtree:is_eventb_comprehension_set(Body,Ids,Pred,Expr),
1133		% try and separate couple in Expr so that we have better position info for source of VISB_SVG_OBJECTS
1134		Body = b(_,Type,II),
1135		Expr = b(couple(_,_),_,_),
1136		!,
1137		couple_member(NewExpr,Expr), % evaluate each part of the couple in isolation, with better position info
1138		get_texpr_pos(NewExpr,InnerPos),
1139		b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,NewExpr,Pred, Type, NewBody),
1140		get_visb_DEF_svg_object_aux(SpecialClass,DefName,b(NewBody,Type,II),InnerPos,ExpandedState,SVG_ID,AttrList,Desc).
1141		get_visb_DEFINITION_svg_object(SpecialClass,DefName,Body,DefPos,ExpandedState,SVG_ID,AttrList,Desc,DefPos) :-
1142	?	get_visb_DEF_svg_object_aux(SpecialClass,DefName,Body,DefPos,ExpandedState,SVG_ID,AttrList,Desc).
1143
1144		couple_member(TExpr,b(couple(A,B),_,_)) :- !, (couple_member(TExpr,A) ; couple_member(TExpr,B)).
1145		couple_member(TExpr,TExpr).
1146
1147		get_visb_DEF_svg_object_aux(SpecialClass,DefName,Body,DefPos,ExpandedState,SVG_ID,AttrList,Desc) :-
1148		evaluate_visb_formula(Body,DefName,'',ExpandedState,ResValue,DefPos),
1149		flex_expand(ResValue,DefName,DefPos,Expanded,[]),
1150		(Expanded = [] -> add_message(visb_visualiser,'Empty set of SVG object records: ',DefName,DefPos)
1151		; Expanded =[Record|_] ->
1152		(get_VISB_record_fields(Record,Fs)
1153		% TODO: as we now can have different type of records, check in flex_expand below
1154	?	-> (member(field(id,_),Fs)
1155		-> true
1156		; add_message(visb_visualiser,'DEFINITION needs an `id` field if you want to use updates: ',DefName,DefPos)
1157		)
1158		; ajoin(['DEFINITION ', DefName,' should evaluate to a set of records or tuples of records: '],Msg),
1159		add_warning(visb_visualiser,Msg,Record,DefPos)
1160		)
1161		),
1162	?	member(Records,Expanded),
1163		get_VISB_record_fields(Records,Fields),
1164	?	(select(field(id,VID),Fields,F1)
1165		-> extract_attribute_value(DefPos,id,VID,SVG_ID)
1166		; gensym(svg_id,SVG_ID), F1=Fields),
1167		(select(field(comment,CC),F1,F2), b_value_to_string(CC,Desc) -> true
1168		; Desc = '', F2=F1),
1169	?	(SpecialClass=visb_updates, member(field(visibility,VV),F2),
1170		is_invisible(VV),
1171		\+ visb_has_visibility_hover(SVG_ID) % check for hover which may make object visible
1172		-> AttrList=[svg_attribute(visibility,'hidden')] % do not transmit updates
1173		; include_maplist(extract_attribute_from_record(DefPos),F2,AttrList0),
1174		exclude(check_unsupported_special_visb_attribute(SpecialClass,DefPos),AttrList0,AttrList),
1175	?	(select(svg_attribute(svg_class,SVG_Class),AttrList,A2)
1176		-> maplist(check_attribute_is_supported(SVG_Class,DefPos),A2)
1177		; true)
1178		).
1179
1180		is_invisible(string(hidden)). % also treat collapse ?
1181		is_invisible(pred_false).
1182
1183		% expand nested tuples/sets to a single list of SVG records (possibly of different types)
1184		flex_expand(Value,DefName,Pos) --> {is_custom_explicit_set(Value)},!,
1185		{try_expand_custom_set_with_catch(Value,ExpandedSet,flex_expand),
1186		(is_custom_explicit_set(ExpandedSet)
1187		-> ajoin(['Could not expand set of SVG object records or tuples thereof for ',DefName,': '],Msg),
1188		add_warning(visb_visualiser,Msg,Value,Pos),
1189		fail
1190		; true)},
1191		flex_expand(ExpandedSet,DefName,Pos).
1192		flex_expand([],_,_) --> !, [].
1193		flex_expand(L,_DefName,_Pos) --> {L =[(string(_),string(_))|_]}, !,
1194		[L]. % is probably a partial function {"id" |-> ,...}
1195		flex_expand([H|T],DefName,Pos) --> !, flex_expand(H,DefName,Pos), l_flex_expand(T,DefName,Pos).
1196		flex_expand((A,B),DefName,Pos) --> !, flex_expand(A,DefName,Pos), flex_expand(B,DefName,Pos).
1197		flex_expand(T,_,_) --> [T].
1198
1199		l_flex_expand([],_,_) --> !, [].
1200		l_flex_expand([H|T],DefName,Pos) --> !, flex_expand(H,DefName,Pos), l_flex_expand(T,DefName,Pos).
1201		l_flex_expand(T,_,_) --> [T].
1202
1203		flex_member(X,SetPairVal,DefName,Pos) :- flex_expand(SetPairVal,DefName,Pos,List,[]), member(X,List).
1204
1205
1206		% get the fields of a B value record
1207		% also transparently handles alternative representations, like a function from STRING to STRING
1208		get_VISB_record_fields(rec(Fields),Res) :- !, Res=Fields.
1209		get_VISB_record_fields(StringFunction,Fields) :-
1210		is_set_value(StringFunction,get_VISB_record_fields),
1211		try_expand_custom_set_with_catch(StringFunction,Expanded,get_VISB_record_fields),
1212		% TODO: check we have no duplicates
1213		maplist(convert_to_field,Expanded,Fields).
1214		% TODO: support records as generated by READ_XML:
1215		% rec(attributes:{("fill"|->"#90ee90"),("height"|->"360px"),("id"|->"background_rect"),("width"|->"600px"),("x"|->"1px"),("y"|->"2px")},element:"rect",meta:{("xmlLineNumber"|->"3")},pId:5,recId:6)
1216		% for <rect height="360px" x="1px" y="2px" id="background_rect" width="600px" fill="#90ee90"></rect>
1217
1218		convert_to_field((string(FieldName),Value),field(FieldName,Value)).
1219		% TODO: maybe handle enumerated set values as field names
1220
1221
1222		% already extract and type-check VISB_SVG_UPDATES definitions
1223		precompile_svg_object_updates(ExpandedScope,JsonFileContext) :-
1224		b_sorted_b_definition_prefixed(expression,'VISB_SVG_UPDATES',DefName,DefPos),
1225	?	b_get_typed_definition(DefName,ExpandedScope,TypedExpr),
1226		assert_visb_udpate_def_body(visb_updates,DefName,TypedExpr,DefPos),
1227		add_children_for_visb_update_def_body(TypedExpr,DefName,JsonFileContext),
1228		fail.
1229		precompile_svg_object_updates(_,_).
1230
1231		% assert VisB updates or hovers from B DEFINITION,
1232		% either from VISB_SVG_UPDATES or hovers or dynamic parts of VISB_SVG_OBJECTS:
1233		assert_visb_udpate_def_body(_Kind,DefName,TypedExpr,_DefPos) :-
1234		TypedExpr=b(rec([field(id,_)]),_,Info),!, % can happen when all fields are static
1235		add_debug_message(visb_visualiser,'Useless update/hover (just id field): ',DefName,Info).
1236		assert_visb_udpate_def_body(Kind,DefName,b(couple(A,B),_,_),DefPos) :- !,
1237		% separate couples into individual expressions; in case of WD errors we have more localised errors/problems
1238		assert_visb_udpate_def_body(Kind,DefName,A,DefPos),
1239		assert_visb_udpate_def_body(Kind,DefName,B,DefPos).
1240		assert_visb_udpate_def_body(Kind,DefName,TypedExpr,DefPos) :-
1241		get_texpr_type(TypedExpr,Type),
1242		determine_type_of_visb_formula(TypedExpr,_,FormulaClass),
1243		debug_format(19,'Detected ~w: ~w (~w)~n',[Kind,DefName,FormulaClass]),
1244		assertz(visb_special_definition(Kind,DefName,Type,TypedExpr,FormulaClass,DefPos)),
1245		check_visb_update_type(Kind,Type,DefName,unknown_svg_class,DefPos),
1246		static_check_dynamic_update_def_body(TypedExpr).
1247
1248
1249		% check if we need to add virtual children for an VISB_SVG_UPDATES body:
1250		% (e.g., for title updates to SVG objects coming from an SVG file)
1251		add_children_for_visb_update_def_body(b(couple(A,B),_,_),DefName,JsonFile) :- !,
1252		(add_children_for_visb_update_def_body(A,DefName,JsonFile)
1253		;
1254		add_children_for_visb_update_def_body(B,DefName,JsonFile)).
1255		add_children_for_visb_update_def_body(b(rec(Fields),_,_),DefName,JsonFile) :-
1256	?	select(field(id,TParentId),Fields,F2),!,
1257		is_static_expr(TParentId,id,DefName), % we need a static value to create children for it
1258		TParentId = b(_,_,Info),
1259		determine_type_of_visb_formula(TParentId,TIds,Class),
1260		eval_static_def(Class,DefName,'',TParentId,TIds,ResValue,Info), % evaluate in constants state if necessary
1261		b_value_to_id_string(ResValue,ParentId),
1262		\+ svg_id_exists(ParentId),
1263		(\+ get_default_visb_svg_file(_,_), % cannot call no_svg_file_available yet
1264		JsonFile = '', % No JSON file to be loaded after, which could add SVG file or objects
1265		\+ special_definition_exists('VISB_SVG_CONTENTS')
1266		-> ajoin(['Unknown VISB_SVG_OBJECT with id ',ParentId,' in: '],Msg),
1267		add_warning(visb_visualiser,Msg,DefName,Info)
1268	?	; select(field(title,TTitle),F2,_),
1269		(TTitle = b(string(Title),_,_) -> true ; Title = 'no-title-set'),
1270		get_texpr_pos(TTitle,Pos),
1271		add_virtual_title_object(Title,DefName,Pos,TitleID),
1272		assert_visb_svg_child(ParentId,Pos,TitleID),
1273		assert(visb_svg_child_of_object_from_svg_file(TitleID))
1274		),
1275		fail.
1276		% TODO: set comprehensions like {x•x:Obj|rec(id=("obj",x), title=....)}
1277		% TODO: support sets and warn when ID is not statically known?
1278
1279		% assert VisB events or hovers from B DEFINITION, from part of VISB_SVG_OBJECTS:
1280		% supporting event: attribute and optional predicate attribute
1281		% Kind = visb_events %or visb_hovers
1282		add_visb_events_from_def_body(Kind,DefName,Body,DefPos) :-
1283		get_texpr_type(Body,Type),
1284		\+ empty_update_or_hover_type(Type), % at least one more field than just id field
1285		get_visb_static_svg_object_for_typed_expr(Kind,DefName,Body,DefPos,SVG_ID,AttrList,Desc,InnerPos),
1286		add_visb_object_from_definition(Kind, SVG_ID, AttrList, Desc, DefName, InnerPos),
1287		fail.
1288		add_visb_events_from_def_body(_,_,_,_).
1289
1290		empty_update_or_hover_type(record(Fields)) :- !, Fields \= [_,_|_]. % at least one more field than just id field
1291		empty_update_or_hover_type(set(X)) :- !, empty_update_or_hover_type(X).
1292		empty_update_or_hover_type(couple(A,B)) :- !, empty_update_or_hover_type(A), empty_update_or_hover_type(B).
1293
1294		get_svg_object_updates_from_definitions(ExpandedBState,SVG_ID,SvgAttribute,Value,Pos) :-
1295	?	visb_special_definition(visb_updates,DefName,_Type,BodyTypedExpr,_Class,DefPos),
1296	?	get_visb_DEFINITION_svg_object(visb_updates,DefName,BodyTypedExpr,DefPos,ExpandedBState,SVG_ID,AttrList,_Desc,Pos),
1297	?	member(svg_attribute(SvgAttribute,Value),AttrList).
1298
1299		% check types of VisB updates
1300		check_visb_update_type(Kind,Type,DefName,Class,DefPos) :-
1301		get_update_record_fields_type(Type,Fields),
1302		% other types are STRING +-> STRING, ...; this will be checked in get_visb_DEFINITION_svg_object
1303		(memberchk(field('svg_class',_),Fields)
1304		-> add_warning(visb_visualiser,'VisB updates should not set svg_class:',DefName,DefPos)
1305		; true),
1306	?	member(field(Name,FieldType),Fields),
1307		(Name = trigger_id ->
1308		(Kind=visb_hovers -> true ;
1309		add_warning(visb_visualiser,'Attribute trigger_id can only be used for hovers:',DefName,DefPos)
1310		)
1311		; check_attribute_type_and_name(FieldType,Name,DefName,Class,DefPos)
1312		),
1313		fail.
1314		check_visb_update_type(_,_,_,_,_).
1315
1316		% get a fields type list from a type
1317		get_update_record_fields_type(set(X),Fields) :- !,
1318		get_update_record_fields_type(X,Fields).
1319		get_update_record_fields_type(record(Fields),R) :- !, R=Fields.
1320		get_update_record_fields_type(couple(A,B),Fields) :-
1321		(get_update_record_fields_type(A,Fields)
1322		; get_update_record_fields_type(B,Fields)).
1323
1324
1325		% check B type of a field for an SVG update or object
1326		check_attribute_type_only(Type,Name,DefName,Class,DefPos) :- alternative_spelling(Name,AName),!,
1327		check_attribute_type_only(Type,AName,DefName,Class,DefPos).
1328		check_attribute_type_only(Type,Name,DefName,Class,DefPos) :- Class \= unknown_svg_class,
1329		check_is_number_attribute(Name,Class,DefPos),!,
1330		(illegal_number_type(Type)
1331		-> ajoin(['Type of field ',Name,' of ', DefName, ' is not a number: '],Msg),
1332		pretty_type(Type,TS),
1333		add_warning(visb_visualiser,Msg,TS,DefPos)
1334		; true).
1335		check_attribute_type_only(Type,Name,DefName,_,DefPos) :-
1336		is_svg_color_attribute(Name),!,
1337		(illegal_col_type(Type)
1338		-> ajoin(['Type of field ',Name,' of ', DefName, ' is not a color: '],Msg),
1339		pretty_type(Type,TS),
1340		add_warning(visb_visualiser,Msg,TS,DefPos)
1341		; true).
1342		check_attribute_type_only(_Type,_Name,_DefName,_Class,_DefPos).
1343
1344		check_attribute_type(BType,AttrName,ID,Pos) :-
1345		(svg_id_has_class(ID,Class) -> true ; true),
1346		check_attribute_type_only(BType,AttrName,ID,Class,Pos).
1347		check_attribute_type_and_name(Type,AttrName,DefName,Class,DefPos) :-
1348		check_attribute_type_only(Type,AttrName,DefName,Class,DefPos),
1349		check_attribute_name_is_supported(Class,AttrName,DefPos).
1350
1351		illegal_nr_or_col_type(boolean).
1352		illegal_nr_or_col_type(set(_)).
1353		illegal_nr_or_col_type(seq(_)).
1354		illegal_nr_or_col_type(record(_)).
1355		illegal_nr_or_col_type(couple(A,B)) :- (illegal_nr_or_col_type(A) -> true ; illegal_nr_or_col_type(B)).
1356		% check if couple types can work by concatenating string representations
1357
1358		illegal_col_type(X) :- illegal_nr_or_col_type(X),!.
1359		illegal_col_type(real).
1360		% integer ? or can we map integers to colours using a color scheme like in DOT?
1361
1362		illegal_number_type(X) :- illegal_nr_or_col_type(X),!.
1363		%illegal_number_type(global(_)). % what if we use a global set with weird constants using back-quotes ?
1364
1365		% ----------------
1366
1367		% parse and load an individual JSON VisB item, e.g, :
1368		% { "name":"xscale",
1369		% "value" : "(100.0 / real(TrackElementNumber))"
1370		% }
1371
1372		process_json_definition(File,json(List)) :-
1373		(get_attr_true(ignore,List,File) -> true % ignore this definition
1374		; process_json_def_lst(File,List)).
1375
1376
1377		process_json_def_lst(File,List) :-
1378		force_del_attr_with_pos(name,List,string(ID),L1,File,NamePos),
1379		force_del_attr_with_pos(value,L1,string(Formula),L2,File,VPos),
1380		debug_format(19,' Processing definition for ~w with value-formula (lines ~w):~w~n',[ID,VPos,Formula]),
1381		!,
1382		set_gen_parse_errors(L2,VPos,GenParseErrors), % treat optional attribute
1383		process_json_definition(ID,NamePos,Formula,VPos,GenParseErrors).
1384		process_json_def_lst(File,List) :- get_pos_from_list(List,File,Pos),
1385		add_error(visb_visualiser,'Illegal VisB Definition:',List,Pos).
1386
1387		% we could also load a classical B Definition file and process its definitions like this:
1388		process_json_definition(ID,NamePos,Formula,VPos,GenParseErrors) :-
1389		atom_codes(Formula,FCodes),
1390		set_error_context(visb_error_context(definition,ID,'value',VPos)),
1391		(b_get_definition_name_with_pos(ID,_Arity,_DefType,_DPos)
1392		-> add_warning(visb_visualiser,'Ignoring VisB definition, DEFINITION of the same name already exists:',ID,NamePos)
1393		; parse_expr(FCodes,TypedExpr,GenParseErrors)
1394		-> add_visb_json_definition(ID,TypedExpr,VPos)
1395		; GenParseErrors=false -> formatsilent('Ignoring optional VisB definition for ~w due to error in B formula~n',[ID])
1396		; add_error(visb_visualiser,'Cannot parse or typecheck VisB formula for definition',ID,VPos)
1397		),
1398		clear_error_context.
1399
1400		add_visb_json_definition(ID,TypedExpr,VPos) :-
1401		get_texpr_type(TypedExpr,Type),
1402		determine_type_of_visb_formula(TypedExpr,TIds,Class), %write(type(ID,Class,TIds)),nl,
1403		(try_eval_static_def(Class,'static definition', ID,TypedExpr,TIds,StaticValue,VPos)
1404		-> get_texpr_type(TypedExpr,Type),StaticValueExpr = b(value(StaticValue),Type,[]),
1405		assert_visb_json_definition(ID,Type,StaticValueExpr,TIds,Class,VPos)
1406		; assert_visb_json_definition(ID,Type,TypedExpr,TIds,Class,VPos)
1407		).
1408
1409		% assert a VisB definition stemming from the JSON definitions section:
1410		assert_visb_json_definition(DefName,Type,TypedExpr,UsedTIds,Class,DefPos) :-
1411	?	(is_special_visb_def_name(DefName,SpecialClass) -> true ; SpecialClass = regular_def),
1412		assertz(visb_definition(DefName,Type,TypedExpr,Class,DefPos,SpecialClass)),
1413		(SpecialClass \= regular_def
1414		-> formatsilent('Detected special ~w definition ~w (~w)~n',[SpecialClass,DefName,Class]),
1415		add_special_json_definition(SpecialClass,DefName,Type,TypedExpr,UsedTIds,Class,DefPos)
1416		; true
1417		).
1418
1419		% register some special definitions, in which a set of objects/hovers/updates can be specified
1420		% by a single definition returning a set of records
1421		add_special_json_definition(visb_updates,DefName,Type,TypedExpr,_,Class,DefPos) :- !,
1422		check_visb_update_type(visb_updates,Type,DefName,Class,DefPos),
1423		assertz(visb_special_definition(visb_updates,DefName,Type,TypedExpr,Class,DefPos)). % will be evaluated later
1424		add_special_json_definition(visb_contents,DefName,Type,TypedExpr,_,Class,DefPos) :- !,
1425		assertz(visb_special_definition(visb_contents,DefName,Type,TypedExpr,Class,DefPos)).
1426		add_special_json_definition(visb_box,DefName,Type,TypedExpr,_,Class,DefPos) :- !,
1427		assertz(visb_special_definition(visb_box,DefName,Type,TypedExpr,Class,DefPos)).
1428		add_special_json_definition(visb_objects,DefName,_Type,TypedExpr,_UsedTIds,_Class,DefPos) :- !,
1429		AllowSep=allow_separation, % TODO: we re-determine the class and used ids below:
1430		get_typed_static_definition_with_constants_state(DefName,TypedExpr,ResBody,DefPos,CS,no_inlining,AllowSep),
1431		(get_visb_DEFINITION_svg_object(visb_objects,DefName,ResBody,DefPos,CS,SVG_ID,AttrList,Desc,InnerPos),
1432		%formatsilent('Adding ~w : ~w (from ~w)~n',[visb_objects,SVG_ID,DefName]),
1433		add_visb_object_from_definition(visb_objects, SVG_ID, AttrList, Desc, DefName, InnerPos),
1434		fail ; true).
1435		add_special_json_definition(SpecialClass,DefName,_Type,TypedExpr,UsedTIds,Class,DefPos) :-
1436		(get_unique_initial_state_for_visb(Class,DefName,DefPos,UsedTIds,ConstantsState) -> true
1437		; ConstantsState=[]),
1438		get_static_visb_state(ConstantsState,FullState), % add static VisB Defs
1439		(Class=requires_variables,
1440		(get_preference(visb_allow_variables_for_objects,false) ; ConstantsState=[])
1441		-> add_warning(visb_visualiser,'Ignoring VisB definition which requires variables:',DefName,DefPos)
1442		; (get_visb_DEFINITION_svg_object(SpecialClass,DefName,TypedExpr,DefPos,FullState,SVG_ID,AttrList,Desc,InnerPos),
1443		%formatsilent('Adding ~w : ~w (from ~w)~n',[SpecialClass,SVG_ID,DefName]),
1444		add_visb_object_from_definition(SpecialClass, SVG_ID, AttrList, Desc, DefName, InnerPos),
1445		fail % backtrack to add all objects and all hover attributes
1446		; true)
1447		).
1448
1449		is_special_visb_def_name(DefName,visb_updates) :- atom_concat('VISB_SVG_UPDATES',_,DefName).
1450		is_special_visb_def_name(DefName,visb_hovers) :- atom_concat('VISB_SVG_HOVERS',_,DefName).
1451		is_special_visb_def_name(DefName,visb_objects) :- atom_concat('VISB_SVG_OBJECTS',_,DefName).
1452		is_special_visb_def_name(DefName,visb_contents) :- atom_concat('VISB_SVG_CONTENTS',_,DefName).
1453		is_special_visb_def_name(DefName,visb_events) :- atom_concat('VISB_SVG_EVENTS',_,DefName).
1454		is_special_visb_def_name('VISB_SVG_BOX',visb_box).
1455		% TODO: maybe provide VISB_HTML_CONTENTS which appear after the SVG
1456
1457		% evaluate static VisB defs only once or evaluate expressions in svg_objects and loop bounds
1458		eval_static_def(Class,VisBKind,ID,TypedExpr,UsedTIds,StaticValue,VPos) :-
1459		get_unique_initial_state_for_visb(Class,ID,VPos,UsedTIds,ConstantsState),
1460		evaluate_static_visb_formula(TypedExpr,VisBKind,ID,ConstantsState,StaticValue,VPos).
1461
1462		% only evaluate statically if possible; no warnings/messages if not possible (just fail)
1463		try_eval_static_def(requires_variables,_VisBKind,_ID,_TypedExpr,_UsedTIds,_StaticValue,_VPos) :- !,
1464		fail. % do not try to evaluate statically; events will change the variable values anyway
1465		try_eval_static_def(Class,VisBKind,ID,TypedExpr,UsedTIds,StaticValue,VPos) :-
1466		% TODO: disable messages for multiple constants values; just fail
1467		eval_static_def(Class,VisBKind,ID,TypedExpr,UsedTIds,StaticValue,VPos).
1468
1469		% check if a unique constant value exists for a model
1470		get_unique_initial_state_for_visb(requires_nothing,_,_,_,State) :- !, State=[].
1471		get_unique_initial_state_for_visb(Class,DefName,DefPos,_,State) :-
1472		\+ multiple_concrete_constants_exist,
1473		is_concrete_constants_state_id(StateID),!,
1474		(Class=requires_variables
1475		-> get_preference(visb_allow_variables_for_objects,true),
1476		unique_initialisation_id_exists_from(StateID,DefName,DefPos,State)
1477		% Note: variable can still be modified by other events later, e.g., in ProB2-UI
1478		; visited_expression(StateID,StateTerm),
1479		state_corresponds_to_set_up_constants_only(StateTerm,State)).
1480		get_unique_initial_state_for_visb(requires_constants,DefName,DefPos,Ids,State) :- Ids \= all,
1481		% try and see if all values for Ids are the same; TODO: also support requires_variables
1482		is_concrete_constants_state_id(StateID),!,
1483		visited_expression(StateID,StateTerm),
1484		state_corresponds_to_set_up_constants_only(StateTerm,State),
1485		(member(C,Ids), get_texpr_id(C,CstID),
1486		other_constant_value_exists_for(CstID,State,StateID)
1487		-> ajoin(['Multiple values for constant ',CstID, ' in context of'],Msg),
1488		add_visb_lint_message(Msg,DefName,DefPos),fail
1489		; true).
1490
1491
1492		get_a_constants_state(State,StateID,inline_objects(SingleStateId)) :-
1493		get_constants_state_id_for_id(SingleStateId,StateID),!,
1494		visited_expression(StateID,StateTerm),
1495		state_corresponds_to_set_up_constants_only(StateTerm,State).
1496		get_a_constants_state(State,StateID,InlineObjects) :-
1497		check_inlining(InlineObjects),
1498		is_concrete_constants_state_id(StateID),!,
1499		visited_expression(StateID,StateTerm),
1500		state_corresponds_to_set_up_constants_only(StateTerm,State).
1501
1502		check_inlining(no_inlining) :- !.
1503		check_inlining(inline_objects(_SingleStateId)) :- !.
1504		check_inlining(X) :- add_internal_error('Invalid inlining value:',check_inlining(X)).
1505
1506
1507		other_constant_value_exists_for(CstID,State,StateId) :-
1508		lookup_value_for_existing_id(CstID,State,Val1),
1509		is_concrete_constants_state_id(StateId2), StateId2 \= StateId,
1510		visited_expression(StateId2,StateTerm2),
1511		state_corresponds_to_set_up_constants_only(StateTerm2,State2),
1512		lookup_value_for_existing_id(CstID,State2,Val2),
1513		Val2 \= Val1.
1514
1515
1516		unique_initialisation_id_exists_from(FromStateId,DefName,DefPos,State) :-
1517		transition(FromStateId,_,StateID),!,
1518		(transition(FromStateId,_,StateID2),
1519		StateID2 \= StateID
1520		-> ajoin(['Multiple initialisations exists (state ids ',StateID,',',StateID2,') for'],Msg),
1521		add_visb_lint_message(Msg,DefName,DefPos),fail
1522		; true),
1523		visited_expression(StateID,StateTerm),
1524		state_corresponds_to_initialised_b_machine(StateTerm,State).
1525
1526		parse_expr_for_visb(Formula,JsonList,Pos,TypedExpr) :-
1527		set_gen_parse_errors(JsonList,Pos,GenParseErrors),
1528		parse_expr(Formula,TypedExpr,GenParseErrors).
1529
1530		set_gen_parse_errors(JSonList,Pos,GenParseErrors) :-
1531		(is_optional_json_item(JSonList)
1532		-> GenParseErrors=false
1533		; %get_pos_from_list(JSonList,File,Position),
1534		GenParseErrors=gen_parse_errors_for(Pos)).
1535
1536		% ----------------
1537
1538		% parse and load an individual JSON SVG object listed under svg_objects, e.g, :
1539		% {
1540		% "svg_class":"rect",
1541		% "id":"train_rect",
1542		% "x":"0",
1543		% "y":"0",
1544		% "comment":"..."
1545		% },
1546		process_json_svg_object(File,Json) :-
1547		process_repeat(0,Json,File,add_visb_json_svg_object).
1548
1549		add_visb_json_svg_object(File,json(List)) :- get_attr_true(ignore,List,File), !. % ignore this item
1550		add_visb_json_svg_object(File,json(List)) :-
1551		(del_attr_with_pos(svg_class,List,string(SVG_Class),L1,File,Pos1) -> true % shape: line, rect, ...
1552		; infer_svg_class(List,SVG_Class,File,Pos1)
1553		-> add_visb_lint_message('Inferred svg_class',SVG_Class,Pos1),L1=List
1554		; force_del_attr_with_pos(svg_class,List,string(SVG_Class),L1,File,Pos1) % generates error message
1555		),
1556		force_del_attr(id,L1,string(ID),L2,File),
1557		(del_attr(comment,L2,string(Desc),JsonList3) -> true ; Desc = '', JsonList3=L2),
1558		debug_format(19,' Creating new SVG object ~w with id:~w~n',[SVG_Class,ID]),
1559		add_debug_message(visb_visualiser,'New object: ',ID,Pos1),
1560		% TODO: we could pre-process all attributes not depending on %0, %1, ...
1561		maplist(get_svg_attr(ID,SVG_Class,File),JsonList3,AttrList),
1562		%formatsilent('Adding SVG Object ~w with ID ~w (~w): ~w~n',[SVG_Class,ID,Desc,AttrList]),
1563		assert_visb_svg_object(ID,SVG_Class,AttrList,Desc,'JSON',Pos1),
1564		!.
1565		add_visb_json_svg_object(File,Json) :-
1566		!,
1567		get_pos_from_list(Json,File,Pos),
1568		add_error(visb_visualiser,'Illegal VisB additional SVG object:',Json,Pos).
1569
1570		infer_svg_class(List,line,File,Pos) :- get_attr_with_pos(x1,List,_,File,Pos),!.
1571		infer_svg_class(List,circle,File,Pos) :- get_attr_with_pos(r,List,_,File,Pos),!.
1572		infer_svg_class(List,rect,File,Pos) :- get_attr_with_pos(height,List,_,File,Pos),!.
1573		infer_svg_class(List,rect,File,Pos) :- get_attr_with_pos(width,List,_,File,Pos),!.
1574		infer_svg_class(List,ellipse,File,Pos) :- get_attr_with_pos(rx,List,_,File,Pos),!. % could also be rect
1575		infer_svg_class(List,text,File,Pos) :- get_attr_with_pos(text,List,_,File,Pos),!.
1576		infer_svg_class(List,g,File,Pos) :- get_attr_with_pos(children,List,_,File,Pos),!. % group + foreignObject have children
1577		infer_svg_class(List,use,File,Pos) :- get_attr_with_pos(href,List,_,File,Pos),!. % href can also be used with image, pattern, ...
1578
1579		% assert a new SVG object to be created upon SETUP_CONSTANTS/INITIALISATION:
1580		assert_visb_svg_object(ID,SVG_Class,_AttrList,_Desc,DefName,Pos1) :-
1581		visb_svg_object(ID,_,_,_,_Pos0),!,
1582		ajoin(['SVG object (from ',DefName,', svg_class=',SVG_Class,') with same id already created: '],Msg),
1583		add_warning(visb_visualiser,Msg,ID,Pos1).
1584		assert_visb_svg_object(_ID,_SVG_Class,AttrList,_Desc,_DefName,Pos1) :-
1585		\+ (AttrList=[] ; AttrList=[_|_]),!,
1586		add_error(visb_visualiser,'SVG objects attributes are not a list:',AttrList,Pos1).
1587		assert_visb_svg_object(ID,SVG_Class,AttrList,Desc,DefName,Pos1) :-
1588		add_visb_debug_infos(ID,SVG_Class,AttrList,AttrList2,DefName,Pos1),
1589		sort(AttrList2,SAttrList),
1590		get_all_children(SAttrList,Children,RestAttrs,DefName,Pos1),
1591		(Children = [] -> true
1592	?	; svg_shape_can_have_children(SVG_Class) -> true % g, foreignObject, symbol, HTML tags
1593		; Children = [C1_ID|_], visb_svg_object(C1_ID,CAttr,_,_,_),
1594		attribute_automatically_creates_children(CAttr) % e.g., title object created for title attribute of ID
1595		-> true
1596		; add_visb_lint_message('Children attribute only useful for certain SVG classes such as groups (g) or foreignObject or when adding title objects (as tooltips)',Children,Pos1)
1597		),
1598	?	(select(svg_attribute(group_id,ParentGroupId),RestAttrs,RestAttrs2)
1599		-> assert_visb_svg_child(ParentGroupId,Pos1,ID) % register parent group id
1600		; RestAttrs2=RestAttrs),
1601		check_svg_shape_class(ID,SVG_Class,Pos1), % after registering group_id, so that the parent is known
1602		compute_auto_attributes(RestAttrs2,RestAttrs2,SVG_Class,NewRestAttrs),
1603		assertz(visb_svg_object(ID,SVG_Class,NewRestAttrs,Desc,Pos1)),
1604		maplist(assert_visb_svg_child(ID,Pos1),Children). % add all children
1605
1606		% adapt visb_svg_object to provide developer debug infos, e.g., in title hover messages
1607		add_visb_debug_infos(ID,SVG_Class,AttrList,NewAttrList,DefName,Pos) :- SVG_Class \= title,
1608		get_preference(visb_show_debug_infos,true),
1609		(select(svg_attribute(title,Title),AttrList,RestAttrs) -> true
1610		; Title='', RestAttrs=AttrList),
1611		!,
1612		extract_span_description_with_opts(Pos,PosStr,
1613		[relative_file_name,compact_pos_info,
1614		inner_context_separator('\n in ','\n at ')]),
1615		%extract_definition_call_stack_desc(Pos,CS), already displayed in inner context
1616		ajoin(['-- VISB_DEBUG_INFO --\nid=',ID, '\nsvg_class=',SVG_Class, '\nsrc=',DefName,'\n', PosStr],DebugInfo),
1617		(Title='' -> NewTitle=DebugInfo ; ajoin([Title,'\n',DebugInfo],NewTitle)),
1618		%format('~nDEBUG::~n~w~n~w~n---~n',[ID,DebugInfo]),
1619		assert(visb_svg_object_debug_info(ID,DebugInfo)),
1620		NewAttrList = [svg_attribute(title,NewTitle)|RestAttrs].
1621		add_visb_debug_infos(_,_,AttrList,AttrList,_,_).
1622
1623		% compute the value of VisB auto attributes, e.g., automatically
1624		% doing a layout of objects in a grid
1625		% TODO: SVG/special_svg_number already supports auto but not for x,y coordinates?
1626		% TODO: try and determine width of object automatically; keep track of auto objects max height per row
1627		% TODO: support cx,cy
1628		compute_auto_attributes([],_,_,[]).
1629		compute_auto_attributes([svg_attribute(Attr,Val)|T],AllAttrs,SVG_Class,
1630		[svg_attribute(Attr,NewVal)|NT]) :-
1631		(Val=auto, compute_auto_attribute(Attr,AllAttrs,SVG_Class,NewVal)
1632		-> true
1633		; NewVal=Val),
1634		compute_auto_attributes(T,AllAttrs,SVG_Class,NT).
1635
1636		:- dynamic next_auto_x/1, next_auto_y/2.
1637		next_auto_x(0).
1638		next_auto_y(0,0). % y coordinate and height of the current row of automatically placed objects
1639		reset_auto_attrs :- retractall(next_auto_x(_)),
1640		retractall(next_auto_y(_,_)),
1641		assertz(next_auto_x(0)),
1642		assertz(next_auto_y(0,0)).
1643
1644		get_x_auto_limit(Limit) :- visb_empty_svg_box_height_width(_H,W,_ViewBox),!,
1645		Limit = W. %TODO: inspect viewBox
1646		get_x_auto_limit(400).
1647
1648		compute_auto_attribute(id,_,_,GenID) :- !, gensym(svg_id,GenID).
1649		% Note: x/cx is computed before y/cy (attributes are sorted), so that y/cy uses the row chosen here
1650		compute_auto_attribute(Attr,AllAttrs,SVG_Class,Val) :-
1651		auto_compute_x_coordinate(Attr,Kind),!,
1652		(get_width(SVG_Class,AllAttrs,Width) -> true ; Width=10),
1653		(get_height(SVG_Class,AllAttrs,Height) -> true ; Height=10),
1654		Padding = 2, % TODO: make customisable
1655		get_x_auto_limit(Lim),
1656		retract(next_auto_x(XV)),
1657		retract(next_auto_y(Y,RowHeight)),
1658		(XV > 0, XV+Width > Lim % object does not fit into the current row: start a new row
1659		-> X=0, NewY is Y+RowHeight, NewRowHeight is Height+Padding
1660		; X=XV, NewY=Y, NewRowHeight is max(RowHeight,Height+Padding)),
1661		NewXV is X+Width+Padding,
1662		assertz(next_auto_x(NewXV)),
1663		assertz(next_auto_y(NewY,NewRowHeight)),
1664		(Kind=left -> Val=X ; Val is X + Width/2).
1665		compute_auto_attribute(Attr,AllAttrs,SVG_Class,Val) :- auto_compute_y_coordinate(Attr,Kind),
1666		next_auto_y(YV,_),
1667		(Kind = top -> Val = YV
1668		; get_height(SVG_Class,AllAttrs,Height) -> Val is YV + Height/2
1669		; Val is YV+5).
1670
1671		auto_compute_x_coordinate(x,left). % rect, ..
1672		auto_compute_x_coordinate(cx,center). % circle, ellipse
1673		auto_compute_y_coordinate(y,top). % rect, ..
1674		auto_compute_y_coordinate(cy,center). % circle, ellipse
1675
1676		get_width(rect,Attrs,Wid) :- get_number_attr(width,Attrs,Wid).
1677		get_width(circle,Attrs,Wid) :- get_number_attr(r,Attrs,Radius), Wid is 2*Radius.
1678		get_width(ellipse,Attrs,Wid) :- get_number_attr(rx,Attrs,Radius), Wid is 2*Radius.
1679		get_width(line,Attrs,Wid) :- get_number_attr(x1,Attrs,X1),
1680		get_number_attr(x2,Attrs,X2), Wid is abs(X2-X1).
1681
1682		get_height(rect,Attrs,Wid) :- get_number_attr(height,Attrs,Wid).
1683		get_height(circle,Attrs,Wid) :- get_number_attr(r,Attrs,Radius), Wid is 2*Radius.
1684		get_height(ellipse,Attrs,Wid) :- get_number_attr(ry,Attrs,Radius), Wid is 2*Radius.
1685		get_height(line,Attrs,Wid) :- get_number_attr(y1,Attrs,X1),
1686		get_number_attr(y2,Attrs,X2), Wid is abs(X2-X1).
1687
1688		% get the value of an attribute as a number; fails for values such as 50% or auto
1689		get_number_attr(Attr,Attrs,Nr) :- member(svg_attribute(Attr,Val),Attrs),
1690		(number(Val) -> Nr=Val
1691		; atom(Val), atom_codes(Val,Codes), catch(number_codes(Nr,Codes),_,fail)).
1692
1693
1694		% register an SVG ID as child of a group
1695		assert_visb_svg_child(_ParentId,Pos,ChildID) :- visb_svg_child(ChildID,OldParent),!,
1696		ajoin(['SVG object already child of group ',OldParent,': '],Msg),
1697		add_warning(visb_visualiser,Msg,ChildID,Pos).
1698		assert_visb_svg_child(ParentId,Pos,ChildID) :- visb_svg_child(ParentId,ChildID),!, % TODO: full cycle detection
1699		ajoin(['SVG object already parent of group ',ParentId,' (cycle): '],Msg),
1700		add_warning(visb_visualiser,Msg,ChildID,Pos).
1701		assert_visb_svg_child(ParentId,_Pos,ChildID) :-
1702		assertz(visb_svg_child(ChildID,ParentId)),
1703		assertz(visb_svg_parent(ParentId,ChildID)).
1704
1705
1706		% we need to translate a title attribute to a separate title object and add it as a child
1707		% see also post_process_visb_item which dispatches title updates to the child object
1708		get_all_children(SAttrList,Children,Rest,DefName,Pos) :-
1709	?	select(svg_attribute(title,Title),SAttrList,SList2),!,
1710		add_virtual_title_object(Title,DefName,Pos,TitleID),
1711		Children=[TitleID|TChilds],
1712		get_children_attribute(SList2,TChilds,Rest,Pos).
1713		get_all_children(SAttrList,Children,Rest,_,Pos) :-
1714		% get the children explicitly defined by the user:
1715		get_children_attribute(SAttrList,Children,Rest,Pos).
1716
1717		add_virtual_title_object(Title,DefName,Pos,TitleID) :-
1718		gensym(visb_title,TitleID),
1719		assert_visb_svg_object(TitleID,'title',[svg_attribute(text,Title)],'',DefName,Pos),
1720		add_debug_message(visb_visualiser,'Adding virtual title child object: ',TitleID,Pos).
1721
1722		get_children_attribute(SAttrList,Children,Rest,Pos) :-
1723	?	select(svg_attribute(children,C),SAttrList,R),!,
1724		(is_list(C) -> Children=C
1725		; add_warning(visb_visualiser,'Children attribute should be a list (of SVG ids): ',C,Pos),
1726		Children=[]),
1727		Rest=R.
1728		get_children_attribute(SAttrList,[],SAttrList,_).
1729
1730
1731		svg_shape_can_have_children(defs).
1732		svg_shape_can_have_children(foreignObject).
1733		svg_shape_can_have_children(g).
1734		svg_shape_can_have_children(pattern).
1735		svg_shape_can_have_children(symbol).
1736		svg_shape_can_have_children(X) :- is_html_tag(X).
1737
1738
1739		% check whether svg_class value seems valid
1740		check_svg_shape_class(ID,Shape,Pos) :-
1741		(is_svg_shape_class(Shape) -> true
1742		; is_html_tag(Shape) ->
1743		(visb_svg_child(ID,ParentId),
1744		visb_svg_object(ParentId,ParClass,_,_,_),
1745		(is_html_tag(ParClass) -> true ; ParClass=foreignObject)
1746		-> add_debug_message(visb_visualiser,'HTML tag used as svg_class in foreignObject child: ',Shape,Pos)
1747		; ajoin(['SVG object ', ID, ' has HTML tag as svg_class (and should probably be a child of a foreignObject)'],Msg),
1748		add_visb_lint_message(Msg,Shape,Pos) % probably should be child of foreignObject
1749		)
1750		; dotshape2svg_class(Shape,Class)
1751		-> ajoin(['SVG object ', ID, ' has unknown svg_class (did you mean ',Class,' ?): '],Msg),
1752		add_warning(visb_visualiser,Msg,Shape,Pos)
1753		; get_all_svg_classes(Classes),
1754		get_possible_fuzzy_matches_and_completions_msg(Shape,Classes,FMsg)
1755		-> ajoin(['SVG object ', ID, ' has unknown svg_class (did you mean ',FMsg,' ?): '],Msg),
1756		add_warning(visb_visualiser,Msg,Shape,Pos)
1757		; ajoin(['SVG object ', ID, ' has unknown svg_class'],Msg),
1758		add_visb_lint_message(Msg,Shape,Pos)
1759		).
1760
1761		% get SVG attribute for a JSON svg_object:
1762		get_svg_attr(ID,SVG_Class,File,'='(Attr,AttrVal,Pos),svg_attribute(Attr,Val)) :- !,
1763		construct_prob_pos_term(Pos,File,PosTerm),
1764		get_svg_static_attribute_value(Attr,ID,SVG_Class,PosTerm,AttrVal,Val),
1765		check_attribute_name_is_supported(SVG_Class,Attr,PosTerm).
1766		get_svg_attr(_,_,File,Json,_) :-
1767		get_pos_from_list([Json],File,Position),
1768		add_error(visb_visualiser,'Illegal SVG object attribute',Json,Position),fail.
1769
1770		get_svg_static_attribute_value(Attr,ID,SVG_Class,Pos,AttrVal,Nr) :-
1771		check_is_number_attribute(Attr,SVG_Class,Pos),
1772		\+ is_special_svg_number_form(AttrVal),
1773		!,
1774		(get_number_value(AttrVal,Nr,Attr,Pos) -> true
1775		; ajoin(['Illegal number value for attribute ',Attr, ' of svg_object ',ID,':'],Msg),
1776		add_error(visb_visualiser,Msg,AttrVal,Pos), Nr=0).
1777		get_svg_static_attribute_value(_,_,_,_,string(Val),Res) :- !, Res=Val.
1778		% for children we get something like array([string(button1_1),string(button1_2)])
1779		get_svg_static_attribute_value(Attr,ID,SVG_Class,Pos,array(List),ResList) :- !,
1780		maplist(get_svg_static_attribute_value(Attr,ID,SVG_Class,Pos),List,ResList).
1781		get_svg_static_attribute_value(Attr,ID,_,Pos,Val,Val) :-
1782		ajoin(['Illegal value for attribute ',Attr, ' of svg_object ',ID,':'],Msg),
1783		add_warning(visb_visualiser,Msg,Val,Pos).
1784
1785
1786		% detect special SVG number forms, like 50%
1787		is_special_svg_number_form(string(Atom)) :-
1788		atom_codes(Atom,Codes),
1789		special_svg_number(Codes,[]).
1790
1791
1792		:- assert_must_succeed(visb_visualiser:special_svg_number("10%",[])).
1793		:- assert_must_succeed(visb_visualiser:special_svg_number("10 %",[])).
1794		:- assert_must_succeed(visb_visualiser:special_svg_number(" 99em ",[])).
1795		:- assert_must_succeed(visb_visualiser:special_svg_number("1.0em",[])).
1796		:- assert_must_fail(visb_visualiser:special_svg_number("10",[])).
1797		:- assert_must_fail(visb_visualiser:special_svg_number("10+nrcols+%0",[])).
1798		special_svg_number --> " ",!, special_svg_number.
1799		special_svg_number --> [X], {digit(X)},!, special_svg_number2.
1800		special_svg_number --> "auto".
1801		special_svg_number2 --> [X], {digit(X)},!, special_svg_number2.
1802		special_svg_number2 --> ".",!, special_svg_number2. % TODO: only allow one dot; + accept e notation?
1803	?	special_svg_number2 --> optws,!, svg_unit,!, optws.
1804
1805		% using info from https://oreillymedia.github.io/Using_SVG/guide/units.html
1806		svg_unit --> "%".
1807		svg_unit --> "ch".
1808		svg_unit --> "cm".
1809		svg_unit --> "em".
1810		svg_unit --> "ex".
1811		svg_unit --> "in".
1812		svg_unit --> "mm".
1813		svg_unit --> "pc".
1814		svg_unit --> "pt".
1815		svg_unit --> "px".
1816		svg_unit --> "deg". % angle units
1817		svg_unit --> "grad".
1818		svg_unit --> "rad".
1819		svg_unit --> "turn".
1820		svg_unit --> "rem". % root em
1821		svg_unit --> "vh". % viewport height unit (1%)
1822		svg_unit --> "vw". % viewport width unit (1%)
1823		svg_unit --> "vmin". % min ov vh, vw
1824		svg_unit --> "vmax". % max ov vh, vw
1825
1826
1827		optws --> " ",!,optws.
1828		optws --> [].
1829
1830		digit(X) :- X >= 48, X =< 57.
1831
1832		is_svg_number_attribute(Attr) :- is_svg_number_attribute(Attr,_).
1833
1834
1835		% some checks to see whether the attribute is supported by the given SVG class
1836
1837		check_attribute_is_supported(SVG_Class,DefPos,svg_attribute(Name,_V)) :- !,
1838		(nonvar(SVG_Class), check_is_number_attribute(Name,SVG_Class,DefPos) -> true
1839		% TODO: check color and other attributes, see also check_attribute_type
1840		; check_attribute_name_is_supported(SVG_Class,Name,DefPos)).
1841		check_attribute_is_supported(S,DefPos,F) :-
1842		add_internal_error('Illegal call:',check_attribute_is_supported(S,DefPos,F)).
1843
1844		% if these special attributes occur here, something went wrong, e.g.,
1845		% when separating static/dynamic parts
1846		check_unsupported_special_visb_attribute(visb_objects,_,_) :- !,fail. % here we can process everything
1847		check_unsupported_special_visb_attribute(SpecialClass,DefPos,svg_attribute(Name,_)) :-
1848		special_visb_attribute_not_allowed_in_dynamic_objects(Name,SpecialClass,Kind),
1849		ajoin(['The VisB special attribute ',Name,' cannot be used here (',SpecialClass,' use separate ',Kind,' definition): '],Msg),
1850		add_warning(visb_visualiser,Msg,Name,DefPos).
1851
1852		special_visb_attribute_not_allowed_in_dynamic_objects(hover,SC,'VISB_SVG_HOVERS') :- SC \= visb_hovers.
1853		special_visb_attribute_not_allowed_in_dynamic_objects(hovers,SC,'VISB_SVG_HOVERS') :- SC \= visb_hovers.
1854		special_visb_attribute_not_allowed_in_dynamic_objects(event,SC,'VISB_SVG_EVENTS') :- SC \= visb_events.
1855		special_visb_attribute_not_allowed_in_dynamic_objects(events,SC,'VISB_SVG_EVENTS') :- SC \= visb_events.
1856		special_visb_attribute_not_allowed_in_dynamic_objects(predicate,SC,'VISB_SVG_EVENTS') :- SC \= visb_events.
1857		special_visb_attribute_not_allowed_in_dynamic_objects(predicates,SC,'VISB_SVG_EVENTS') :- SC \= visb_events.
1858		special_visb_attribute_not_allowed_in_dynamic_objects(preds,SC,'VISB_SVG_EVENTS') :- SC \= visb_events.
1859		special_visb_attribute_not_allowed_in_dynamic_objects(execution_kind,SC,'VISB_SVG_EVENTS') :- SC \= visb_events.
1860
1861
1862		check_attribute_name_is_supported(SVG_Class,Name,DefPos) :-
1863		nonvar(SVG_Class),
1864		is_html_tag(SVG_Class),
1865		\+ is_svg_shape_class(SVG_Class), % script and title can be both SVG and HTML
1866		!,
1867		(is_html_attribute(Name)
1868		-> true % TODO: we could check whether attribute appropriate for Tag
1869		; is_virtual_svg_attribute(Name) -> true % Virtual VisB attribute like children, text, ...
1870		; ajoin(['Unknown HTML attribute used inside HTML tag ',SVG_Class],Msg),
1871		add_visb_lint_message(Msg,Name,DefPos)
1872		).
1873		check_attribute_name_is_supported(_SVG_Class,Name,DefPos) :-
1874		check_attribute_name_is_supported(Name,DefPos).
1875
1876		check_attribute_name_is_supported(Name,DefPos) :-
1877	?	\+ is_svg_attribute(Name),
1878		!,
1879		(fix_svg_attribute(Name,GraphVizTranslName)
1880		-> ajoin(['Unknown SVG attribute (maybe you want to use ',GraphVizTranslName,' ?): '],Msg),
1881		add_warning(visb_visualiser,Msg,Name,DefPos)
1882		; get_all_svg_attributes(Attrs),
1883		(get_possible_fuzzy_matches_and_completions_msg(Name,Attrs,FMsg)
1884		-> ajoin(['Unknown SVG attribute (did you mean ',FMsg,' ?): '],Msg),
1885		add_warning(visb_visualiser,Msg,Name,DefPos) % create warning, as it is likely we have made an error
1886		; is_dot_attribute(Name)
1887		-> add_warning(visb_visualiser,'This Dot/Graphviz attribute is not a valid SVG attribute: ',Name,DefPos)
1888		; get_preference(visb_strict_checking,false)
1889		-> add_visb_lint_message('Unknown SVG attribute',Name,DefPos)
1890		; add_warning(visb_visualiser,'Unknown SVG attribute (set VISB_LINT to FALSE to avoid warning): ',Name,DefPos)
1891		)
1892		).
1893		check_attribute_name_is_supported(_,_).
1894
1895		% add message or warning, depending on VISB_LINT setting
1896		add_visb_lint_message(Msg,Obj,Pos) :- get_preference(visb_strict_checking,false), !,
1897		ajoin([Msg,': '],Msg2),
1898		add_message(visb_visualiser,Msg2,Obj,Pos).
1899		add_visb_lint_message(Msg,Obj,Pos) :-
1900		ajoin([Msg,' (set VISB_LINT to FALSE to avoid warning): '],Msg2),
1901		add_warning(visb_visualiser,Msg2,Obj,Pos).
1902
1903
1904		% succeed if attribute is a number attribute and perform a check the attribute is supported by the class
1905		check_is_number_attribute(Attr,Class,Pos) :-
1906		is_svg_number_attribute(Attr,ClassList),
1907		(nonvar(Class), nonmember(Class,ClassList)
1908		-> (equivalent_attribute(Attr,List2,NewAttr), member(Class,List2)
1909		-> ajoin(['The number attribute ',Attr,' is not supported for SVG class ',Class,', use: '],Msg),
1910		add_warning(visb_visualiser,Msg,NewAttr,Pos)
1911		; ajoin(['The number attribute ',Attr,' is not supported for this SVG class: '],Msg),
1912		add_warning(visb_visualiser,Msg,Class,Pos)
1913		)
1914		; true
1915		).
1916
1917		% optionally rewrite record field to alternative spelling
1918		opt_rewrite_field_name(Name,Res) :-
1919		(alternative_spelling(Name,Alt) -> Res=Alt ; Res=Name).
1920
1921		% these alternatives are useful e.g. in TLA+ without backquote:
1922		alternative_spelling(colour,'color').
1923		alternative_spelling(fill_opacity,'fill-opacity').
1924		alternative_spelling(fill_rule,'fill-rule').
1925		alternative_spelling(font_family,'font-family').
1926		alternative_spelling(font_size,'font-size').
1927		alternative_spelling(font_style,'font-style').
1928		alternative_spelling(font_variant,'font-variant').
1929		alternative_spelling(font_weight,'font-weight').
1930		alternative_spelling(marker_end,'marker-end').
1931		alternative_spelling(marker_start,'marker-start').
1932		alternative_spelling(stroke_opacity,'stroke-opacity').
1933		alternative_spelling(stroke_dasharray,'stroke-dasharray').
1934		alternative_spelling(stroke_linecap,'stroke-linecap').
1935		alternative_spelling(stroke_linejoin,'stroke-linejoin').
1936		alternative_spelling(stroke_width,'stroke-width').
1937
1938
1939		% used to suggest fixing unsupported attributes in SVG objects:
1940		equivalent_attribute(cx,[rect],x).
1941		equivalent_attribute(cy,[rect],y).
1942		equivalent_attribute(x,[circle,ellipse],cx).
1943		equivalent_attribute(x,[line],x1).
1944		equivalent_attribute(y,[circle,ellipse],cy).
1945		equivalent_attribute(y,[line],y1).
1946		equivalent_attribute(r,[rect],rx). % ry also exists
1947		equivalent_attribute(rx,[circle],r).
1948		equivalent_attribute(width,[circle],r).
1949		equivalent_attribute(width,[ellipse],rx).
1950		equivalent_attribute(height,[ellipse],ry).
1951
1952
1953		% ----------------
1954
1955		% parse and load an individual JSON VisB item, e.g, :
1956		% {
1957		% "id":"train_info_text",
1958		% "attr":"x",
1959		% "value":"real(train_rear_end)*100.0/real(TrackElementNumber+1)",
1960		% "comment":"move info field above train"
1961		% },
1962		process_visb_json_item(File,Json) :-
1963		process_repeat(0,Json,File,add_visb_json_item).
1964
1965		add_visb_json_item(File,json(List)) :-
1966		get_attr_true(ignore,List,File), % ignore this item
1967		!.
1968		add_visb_json_item(File,json(List)) :-
1969		del_attr_with_pos(id,List,string(ID),L1,File,PosStartOfItem),
1970		!,
1971		process_visb_json_item_id(File,L1,ID,PosStartOfItem).
1972		add_visb_json_item(File,Json) :-
1973		!,
1974		get_pos_from_list(Json,File,Pos),
1975		add_error(visb_visualiser,'VisB Item has no id attribute:',Json,Pos).
1976
1977		process_visb_json_item_id(File,L1,ID,PosStartOfItem) :-
1978		del_attr_with_pos(attr,L1,string(Attr),L2,File,AttrPos), % VisB has attr and value infos
1979		force_del_attr_with_pos(value,L2,string(Formula),L3,File,PosFormula),
1980		!,
1981	?	(del_attr(comment,L3,string(Desc),L4) -> true ; Desc = '',L4=L3),
1982		debug_format(19,' Processing id:~w attr:~w : value:~w desc:~w~n',[ID,Attr,Formula,Desc]),
1983		actually_add_visb_json_item(ID,Attr,AttrPos,Formula,Desc,L4,PosStartOfItem,PosFormula,File).
1984		process_visb_json_item_id(File,L1,ID,PosStartOfItem) :-
1985		get_attr_with_pos(SomeSVGAttr,L1,_V,File,_),
1986	?	is_svg_attribute(SomeSVGAttr),
1987		debug_format(19,'Detected new style VisB JSON declaration with id:~w and SVG attr:~w~n',[ID,SomeSVGAttr]),
1988		!,
1989		% object is in new format with multiple attributes "x":"0" rather than "attr":"x", "value":"0"
1990		(del_attr(comment,L1,string(Desc),L2) -> true ; Desc = '',L2=L1),
1991	?	(non_det_del_attr_with_pos(SVGATTR,L2,string(Formula),L3,File,PosFormula),
1992		is_visb_item_svg_attribute(PosFormula,SVGATTR,Formula),
1993		debug_format(19,' -> Processing new style id:~w attr:~w : value:~w desc:~w~n',[ID,SVGATTR,Formula,Desc]),
1994		actually_add_visb_json_item(ID,SVGATTR,PosFormula,Formula,Desc,L3,PosStartOfItem,PosFormula,File),
1995		fail
1996		;
1997		true).
1998		process_visb_json_item_id(_File,_JsonList,ID,PosStartOfItem) :-
1999		!,
2000		add_error(visb_visualiser,'Illegal VisB Item without attr and value fields:',ID,PosStartOfItem).
2001
2002		is_visb_item_svg_attribute(Pos,Attr,Val) :-
2003		Attr \= override, % so we ignore a possible override attribute
2004	?	(is_svg_attribute(Attr) -> true
2005		; add_warning(visb_visualiser,'Ignoring unknown attribute: ',Attr=Val,Pos),
2006		fail
2007		).
2008
2009
2010		actually_add_visb_json_item(ID,Attr,AttrPos,Formula,Desc,JsonList,PosStartOfItem,PosFormula,File) :-
2011		set_error_context(visb_error_context(item,ID,Attr,PosFormula)),
2012		check_attribute_name_is_supported(Attr,AttrPos),
2013		atom_codes(Formula,FormulaC),
2014		(parse_expr_for_visb(FormulaC,JsonList,PosFormula,TypedExpr)
2015		% TO DO: if optional attribute present: avoid generating errors in b_parse_machine_expression_from_codes
2016		-> get_texpr_type(TypedExpr,BType),
2017		check_attribute_type(BType,Attr,ID,PosFormula),
2018		assert_visb_item(ID,Attr,TypedExpr,Desc,PosStartOfItem,JsonList,File)
2019		; is_optional_json_item(JsonList,File,Pos)
2020		-> formatsilent('Ignoring optional VisB item for ~w (lines ~w) due to error in B formula~n',[ID,Pos])
2021		; ajoin(['Cannot parse or typecheck VisB formula for ',ID,' and attribute ',Attr,':'],Msg),
2022		add_error(visb_visualiser,Msg,Formula,PosFormula)
2023		), clear_error_context.
2024
2025
2026		% assert a VISB item (aka VISB_SVG_UPDATE)
2027		assert_visb_item(ID,Attr,_TypedExpr,_Desc,PosStartOfItem,_,_) :-
2028		visb_item(ID,Attr,_,_,_,Pos2,Meta2),
2029		!,
2030		get_file_name_msg(PosStartOfItem,From1,File1),
2031		(member(override,Meta2)
2032		-> ajoin(['Overriding VisB item',From1,File1,' for same SVG ID ',ID,' and attribute '],Msg),
2033		add_debug_message(visb_visualiser,Msg,Attr,Pos2)
2034		; ajoin(['Overriding VisB item',From1,File1,' for same SVG ID ',ID,
2035		'. Add an \"override\" attribute to remove this warning. Overriden attribute '],Msg),
2036		add_warning(visb_visualiser,Msg,Attr,Pos2),
2037		% error_context already includes attribute and ID
2038		add_message(visb_visualiser,'Overriding this stored formula for ',ID,PosStartOfItem) % provide detailed info
2039		).
2040		assert_visb_item(ID,Attr,_TypedExpr,_Desc,PosStartOfItem,_JsonList,_File) :-
2041		illegal_attribute_for_visb_item(ID,Attr),!,
2042		add_warning(visb_visualiser,'This attribute cannot be modified in a VisB item: ',Attr,PosStartOfItem).
2043		assert_visb_item(ID,Attr,TypedExpr,Desc,PosStartOfItem,JsonList,File) :-
2044		(get_attr_true(override,JsonList,File) -> Meta = [override] ; Meta=[]),
2045		% determine_type_of_visb_formula(TypedExpr,_,Class) now does take definitions into account; TODO: save info
2046		find_identifier_uses(TypedExpr,[],UsedIds),
2047		assertz(visb_item(ID,Attr,TypedExpr,UsedIds,Desc,PosStartOfItem,Meta)).
2048
2049		illegal_attribute_for_visb_item(_,children).
2050		illegal_attribute_for_visb_item(_,group_id).
2051		illegal_attribute_for_visb_item(_,id).
2052		illegal_attribute_for_visb_item(_,svg_class).
2053
2054
2055		get_file_name_msg(Pos1,' from ',File1) :- extract_tail_file_name(Pos1,File1),!.
2056		get_file_name_msg(_,'',''). % no file info
2057
2058		% ----------------
2059		% FOR-LOOP / REPEAT processing
2060
2061		%process_repeat(RepCounter, Json, FinalCall to be executed repeatedly for each instance with File and Json, File)
2062		% RepCounter tells us which of %0, %1, ... should be replaced next
2063
2064		process_repeat(RepCount,json(JsonList),File,FinalCall) :-
2065	?	non_det_del_attr_with_pos(FOR_REP,JsonList,Value,RestJsonList,File,ForRepPos),
2066		% find first for or repeat and process it
2067		(FOR_REP=for ; FOR_REP=repeat),
2068		!,
2069		process_first_repeat(FOR_REP,Value,ForRepPos,RepCount,json(RestJsonList),File,FinalCall).
2070		process_repeat(_RepCount,Json,File,FinalCall) :-
2071		% we have processed all for/repeat loops: now perform the final call on the transformed codes
2072		call(FinalCall,File,Json).
2073
2074		process_first_repeat(for,json(ForList),ForPos,RepCount,JsonData,File,FinalCall) :-
2075		!, % we have a for loop like "for": {"from":1, "to":4}
2076		force_get_attr_nr(from,ForList,From,File),
2077		force_get_attr_nr(to,ForList,To,File),
2078		(get_attr_with_pos(step,ForList,StepAttrVal,File,StepPos),
2079		get_number_value(StepAttrVal,Step,step,StepPos)
2080		-> true % there is an explicit step attribute
2081		; Step=1),
2082		debug_format(19,' -> Iterating %~w from ~w to ~w with step ~w~n',[RepCount,From,To,Step]),
2083		R1 is RepCount+1,
2084		number_codes(RepCount,Pat),
2085		check_between(From,To,Step,ForPos), % check whether step value makes sense
2086	?	( between(From,To,Step,IterElem),
2087		number_codes(IterElem,IterElemC), % we will replace the text %Pat by the text of the number IterElem
2088		replace_in_json(Pat,IterElemC,JsonData,ReplacedJsonData), % replace within other for/repeat loops, but also other attributes
2089		process_repeat(R1,ReplacedJsonData,File,FinalCall), % now process next loop or finish
2090		fail
2091		; true).
2092		process_first_repeat(repeat,array(RepList),RepPos,RepCount,JsonData,File,FinalCall) :-
2093		!, % we have a repetition like "repeat": ["tr1","tr2"] or "repeat": [ ["1","2"] , ...]
2094		(RepList=[array(L1)|_], length(L1,Len)
2095		-> NewRepCount is RepCount+Len, % we have a multi-repeat with list of values to be replaced
2096		LastRepCount is NewRepCount-1,
2097		debug_format(19,' -> Iterating repeat (%~w,...,%~w) over ~w~n',[RepCount,LastRepCount,RepList]),
2098		check_all_same_length_json(RepList,Len,RepPos)
2099		; NewRepCount is RepCount+1, % next replacement starts at $(RepCount+1)
2100		debug_format(19,' -> Iterating repeat (%~w) over ~w~n',[RepCount,RepList])
2101		),
2102	?	( member(IterElem,RepList),
2103		multi_replace_in_json(IterElem,RepCount,JsonData,ReplacedJsonData), % replace within other for/repeat loops, but also other attributes
2104		process_repeat(NewRepCount,ReplacedJsonData,File,FinalCall), % now process next loop or finish
2105		fail
2106		; true).
2107
2108		check_between(_,_,Step,ForPos) :- Step =< 0, !,
2109		add_error(visb_visualiser,'The step of a for loop must be positive:',Step,ForPos),fail.
2110		check_between(From,To,Step,ForPos) :- Iters is (To-From)/Step,
2111		Iters > 100000,!,
2112		add_error(visb_visualiser,'Very large for loop:',Iters,ForPos),fail.
2113		check_between(_,_,_,_).
2114
2115
2116		% ----------------
2117
2118		% parse and load VisB events
2119		% A VisB Event looks like:
2120		% {
2121		% "id": "button",
2122		% "event": "toggle_button",
2123		% "execution_kind": "random", (optional: default, first, random or heuristic)
2124		% "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
2125		% { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
2126		% }
2127		process_json_event(File,Json) :-
2128		process_repeat(0,Json,File,add_visb_json_event).
2129
2130		add_visb_json_event(File,json(List)) :- get_attr_true(ignore,List,File), !. % ignore this item
2131		add_visb_json_event(File,json(List)) :-
2132		get_pos_from_list(List,File,Pos),
2133		force_del_attr(id,List,string(ID),L0,File), % for items it could make sense to not specify an id
2134		(del_attr_with_pos(event,L0,EvTerm,L1,File,EvPos)
2135		-> (check_json_string(EvTerm,event,EvPos,Event) -> true ; Event='') % TODO: accept multiple events
2136		; Event='', L1=L0),
2137		(del_attr_with_pos(predicates,L1,array(Preds),L2,File,PredPos) -> true
2138		; del_attr_with_pos(preds,L1,array(Preds),L2,File,PredPos) -> true
2139		; Preds=[], L2=L1, PredPos=unknown),
2140		(del_attr(execution_kind,L2,EKindTerm,L2b)
2141		-> (check_json_string(EKindTerm,execution_kind,Pos,EKind)
2142		-> check_execution_kind(EKind,ID,Pos,ExecKind)
2143		; default_execution_kind(ExecKind))
2144		; default_execution_kind(ExecKind), L2b=L2),
2145	?	(del_attr(hovers,L2b,array(Hovers),L3) -> true ; Hovers=[],L3=L2b),
2146		(del_attr(items,L3,array(EI),L4)
2147		-> (empty_b_event(Event)
2148		-> EnableItems=[],
2149		add_warning(visb_visualiser,'Ignoring enable items; you need to provide an event name:',ID,Pos)
2150		; EnableItems=EI)
2151		; EnableItems=[],L4=L3),
2152		debug_format(19,' Processing id:~w event:~w preds:~w kind:~w enable:~w hovers:~w~n',[ID,Event,Preds,ExecKind,EnableItems,Hovers]),
2153		!,
2154		actually_add_visb_json_event(ID,Event,Preds,ExecKind,Hovers,EnableItems,L4,File,Pos,PredPos).
2155		add_visb_json_event(File,Json) :-
2156		!,
2157		get_pos_from_list(Json,File,Pos),
2158		add_error(visb_visualiser,'Illegal VisB Event:',Json,Pos).
2159
2160		actually_add_visb_json_event(ID,Event,JsonPreds,ExecKind,JsonHovers,JsonEnableItems,JsonList,File,Pos,PredPos) :-
2161		check_additional_args(JsonList,File),
2162		maplist(process_json_pred,JsonPreds,Preds),
2163		maplist(process_json_enabling_item(ID,Event,File),JsonEnableItems,EnableItems),
2164		maplist(process_json_hover(ID,File),JsonHovers,Hovers),
2165		add_visb_event(ID,Event,Preds,ExecKind,Hovers,EnableItems,File,Pos,PredPos,JsonList).
2166
2167		% the execution kind determines which transition is executed when a VisB event is clicked
2168		% default means that the preference visb_default_execution_kind is used (looked up when the event is executed)
2169		execution_kind(default).
2170		execution_kind(first).
2171		execution_kind(random).
2172		execution_kind(heuristic).
2173		default_execution_kind(default).
2174
2175		check_execution_kind(Kind,_,_,Res) :- execution_kind(Kind), !, Res=Kind.
2176		check_execution_kind(Kind,ID,Pos,Res) :-
2177		default_execution_kind(Res),
2178		ajoin(['Unknown execution_kind ',Kind,' (must be default, first, random or heuristic) using ',Res,' for VisB event of SVG ID: '],Msg),
2179		add_warning(visb_visualiser,Msg,ID,Pos).
2180
2181		% get the execution kind to be used when executing a VisB event
2182		get_actual_execution_kind(default,Kind) :- !, get_preference(visb_default_execution_kind,Kind).
2183		get_actual_execution_kind(Kind,Kind).
2184
2185
2186		add_visb_event(ID,Event,Preds,ExecKind,Hovers,EnableItems,File,Pos,PredPos,JsonList) :-
2187		(retract(visb_event(ID,OldEvent,OldPreds,OldExecKind,OldTypedPred,OldFile,OldPos))
2188		-> (get_attr_true(override,JsonList,File)
2189		-> ajoin(['Overriding VisB event from file ',OldFile,' for ID: '],Msg),
2190		add_debug_message(visb_visualiser,Msg,ID,Pos),
2191		retractall(visb_hover(ID,_,_,_,_,_))
2192		; (OldFile=File
2193		-> ajoin(['No override attribute: adding VisB event ',Event,
2194		' (first event ',OldEvent,') for ID: '],Msg)
2195		; ajoin(['No override attribute: adding VisB event ',Event,
2196		' (first event ',OldEvent,' in file ',OldFile,') for ID: '],Msg)
2197		),
2198		add_debug_message(visb_visualiser,Msg,ID,Pos),
2199		assertz(auxiliary_visb_event(ID,OldEvent,OldPreds,OldExecKind,OldTypedPred,OldPos))
2200		),
2201		assert_visb_event(ID,Event,Preds,ExecKind,Hovers,EnableItems,File,Pos,PredPos)
2202		% ProB2-UI cannot currently support multiple events associated with the same id
2203		% TODO: merge visb_events if we have no override attribute
2204	?	; (xtl_mode ; b_is_operation_name_or_external_subst(Event)) ->
2205		assert_visb_event(ID,Event,Preds,ExecKind,Hovers,EnableItems,File,Pos,PredPos)
2206		; (empty_b_event(Event) ; \+ b_or_z_mode)
2207		-> % for empty event we just want hovers
2208		(Preds = [] -> true
2209		; add_warning(visb_visualiser,'Ignoring preds for VisB event for SVG ID: ',ID,Pos)
2210		),
2211		assert_visb_event(ID,Event,[],ExecKind,Hovers,EnableItems,File,Pos,PredPos)
2212		; is_optional_json_item(JsonList,File,Pos) ->
2213		formatsilent('Ignoring optional VisB event for ~w (lines ~w) due to unknown B operation ~w~n',[ID,Pos,Event])
2214		; detect_op_call_with_paras(Event,OpName) -> % check if we have a name with parameters inside
2215		add_warning(visb_visualiser,'Ignoring parameters provided in event; use the "predicate" attribute to specify parameters: ',Event,Pos),
2216		assert_visb_event(ID,OpName,Preds,ExecKind,Hovers,EnableItems,File,Pos,PredPos)
2217		; atom(Event), atom_prefix('{',Event) ->
2218		ajoin(['Unknown B operation ', Event, ' as VisB event for SVG ID (be sure to use the "events" attribute for multiple events): '],Msg),
2219		add_warning(visb_visualiser,Msg,ID,Pos)
2220		; ajoin(['Unknown B operation ', Event, ' as VisB event for SVG ID: '],Msg),
2221		add_warning(visb_visualiser,Msg,ID,Pos)
2222		).
2223
2224		b_is_operation_name_or_external_subst(OpName) :- b_is_operation_name(OpName).
2225		b_is_operation_name_or_external_subst(Special) :- special_operation(Special).
2226
2227		% maybe we should provide those via the external substitution interface:
2228		% these are all schedulers which choose among existing enabled operations in some manner
2229		special_operation('MCTS_AUTO_PLAY').
2230		special_operation('RANDOM_ANIMATE').
2231		special_operation('RANDOM_ANIMATE_UNTIL_LTL').
2232		special_operation(F) :- external_fun_as_special_operation(F).
2233		external_fun_as_special_operation('STORE_VALUE').
2234		external_fun_as_special_operation('SET_PREF').
2235		% maybe other special names like random_animate with nr of steps, LTL until, ...
2236		special_operation_enabled('MCTS_AUTO_PLAY',_,_,_) :- mcts_auto_play_available.
2237		special_operation_enabled('RANDOM_ANIMATE',_,_,_). % TODO: check if a transition exists
2238		special_operation_enabled('RANDOM_ANIMATE_UNTIL_LTL',_,_,_).
2239		special_operation_enabled(F,_,_,_) :- external_fun_as_special_operation(F).
2240
2241		% detect simple operation call with parameters
2242		detect_op_call_with_paras(Event,OpName) :- atom(Event),
2243		atom_codes(Event,Codes), parse_op_call_name(OpC,Codes,_),!,
2244		atom_codes(OpName,OpC),
2245		b_is_operation_name_or_external_subst(OpName).
2246
2247		parse_op_call_name([X|T]) --> alpha(X), parse_op_call_name2(T).
2248		parse_op_call_name2([]) --> "(".
2249		parse_op_call_name2([H|T]) --> alphadigit(H), parse_op_call_name2(T).
2250
2251		alpha(X) --> [X],({X>=97, X=<122} ; {X>=65, X=<90}).
2252		alphadigit(X) --> [X], ({X>=97,X=<122} ; {X>=65, X=<90} ; {X=95} ; {X>=48, X=<57}).
2253
2254		empty_b_event('').
2255
2256		assert_visb_event(ID,Event,Preds,ExecKind,Hovers,EnableItems,File,Pos,PredPos) :-
2257		construct_pre_post_predicate(ID,Event,Preds,TypedPred,PredPos),
2258		assertz(visb_event(ID,Event,Preds,ExecKind,TypedPred,File,Pos)),
2259		% process hovers
2260	?	(member(HoverElement,Hovers),
2261		(HoverElement=visb_hover(HoverID,Attr,EnterVal,ExitVal) -> true ; add_error(visb_visualiser,'Illegal hover term:',HoverElement),fail),
2262		assert_visb_hover(ID,HoverID,Attr,EnterVal,ExitVal,Pos),fail
2263		; true),
2264		% now process any additional items with disabled and enabled values
2265		assert_visb_enabling_item_list(Event,TypedPred,EnableItems,File,Pos).
2266
2267		process_json_pred(string(P),R) :- !, R=P.
2268		process_json_pred(Json,_) :- !, add_error(visb_visualiser,'Illegal json term for predicate:',Json), fail.
2269
2270		process_json_hover(OriginID,File,json(Hover),visb_hover(ID,Attr,EnterVal,LeaveVal)) :-
2271		force_del_attr(attr,Hover,string(Attr),H2,File),
2272		force_del_attr_with_pos(enter,H2,EV,H3,File,EnterPos),
2273		force_del_attr_with_pos(leave,H3,LV,H4,File,ExitPos),
2274		(is_svg_number_attribute(Attr) % we evaluate number attributes
2275		-> get_number_value(EV,EnterVal,Attr,EnterPos),
2276		get_number_value(LV,LeaveVal,Attr,ExitPos)
2277		; string(EnterVal)=EV, string(LeaveVal)=LV % return string as is; TODO: also evaluate other attributes
2278		),
2279		(get_attr(id,H4,string(ID)) -> true ; ID=OriginID).
2280
2281
2282		assert_visb_hover(TriggerID,SVG_ID,Attr,EnterVal,ExitVal,Pos) :-
2283		assert(visb_hover(TriggerID,SVG_ID,Attr,EnterVal,ExitVal,Pos)),
2284		(visb_has_hovers(TriggerID) -> true ; assert(visb_has_hovers(TriggerID))),
2285		(visb_has_visibility_hover(SVG_ID) -> true
2286		; Attr=visibility -> assert(visb_has_visibility_hover(SVG_ID)) % object SVG_ID can be made visible by hover
2287		; true),
2288		debug_format(19,'Adding hover for ~w : ~w.~w -> ~w <- ~w~n',[TriggerID,SVG_ID,Attr,EnterVal,ExitVal]).
2289
2290
2291		% process items in event which get translated to enabling/disabling predicates
2292		% "items":[ {"attr":"stroke-width","enabled":"10", "disabled":"1"} ]
2293		process_json_enabling_item(ID,Event,File,json(JsonList),
2294		visb_enable_item(SvgID,Attr,EnabledValExpr,DisabledValExpr,PosAttr)) :-
2295		force_del_attr_with_pos(attr,JsonList,string(Attr),L2,File,PosAttr),
2296		force_del_attr_with_pos('enabled',L2,string(EnVal),L3,File,EPos),
2297		force_del_attr_with_pos('disabled',L3,string(DisVal),L4,File,DPos),
2298		(del_attr(id,L4,string(SvgID),L5) -> true ; SvgID=ID, L4=L5),
2299		atom_codes(EnVal,EC),
2300		parse_expr_for_visb(EC,L5,EPos,EnabledValExpr),
2301		atom_codes(DisVal,DC),
2302		parse_expr_for_visb(DC,L5,DPos,DisabledValExpr),
2303		(debug_mode(off) -> true
2304		; translate_bexpression_with_limit(EnabledValExpr,30,EVS),
2305		translate_bexpression_with_limit(DisabledValExpr,30,DVS),
2306		formatsilent('Enabling item for event ~w and SVG ID ~w and attribute ~w : ~w <-> ~w~n',[Event,SvgID,Attr,EVS,DVS])
2307		).
2308
2309		assert_visb_enabling_item_list(Event,TypedPred,EnableList,File,Pos) :-
2310		maplist(check_enabling_item(Event),EnableList),
2311		(EnableList \= []
2312		-> (debug_mode(off)
2313		-> true
2314		; format('Associating enabling/disabling list with event ~w and predicate: ',[Event]), translate:print_bexpr(TypedPred),nl),
2315		assert(visb_event_enable_list(Event,TypedPred,EnableList,File,Pos))
2316		; true).
2317
2318		check_enabling_item(Event,visb_enable_item(SvgID,Attr,_,_,PosAttr)) :-
2319		(visb_item(SvgID,Attr,_,_,_Desc,DuplicatePos,_)
2320		-> (extract_span_description(DuplicatePos,DuplPos) -> true; DuplPos=DuplicatePos),
2321		ajoin(['VisB conflict for SVG ID ',SvgID,' and attribute ',Attr,
2322		'. Conflict between VisB item (',DuplPos,') and VisB enable/disable entry for event: '],Msg),
2323		add_warning(visb_visualiser,Msg,Event,PosAttr)
2324		; true).
2325
2326		valid_additional_attributes(comment).
2327		valid_additional_attributes(description).
2328		valid_additional_attributes(optional).
2329		valid_additional_attributes(override).
2330
2331		% check if there are additional unprocessed args and generate a warning
2332		check_additional_args(JsonList,File) :-
2333		get_attr_with_pos(Attr,JsonList,_,File,Pos),
2334		\+ valid_additional_attributes(Attr),
2335		add_warning(visb_visualiser,'Ignoring unknown JSON field: ',Attr,Pos),
2336		fail.
2337		check_additional_args(_,_).
2338
2339
2340		% construct a pre-post typed predicate for a VisB Event
2341		construct_pre_post_predicate(SvgID,OpName,Preds,TypedPred,Pos) :-
2342		set_error_context(visb_error_context(event,SvgID,OpName,Pos)),
2343		maplist(construct_pre_post_pred(OpName,Pos),Preds,TL),
2344		clear_error_context,
2345		conjunct_predicates(TL,TypedPred).
2346
2347
2348		construct_pre_post_pred(OpName,Pos,PredStr,TypedPred) :- empty_b_event(OpName),!,
2349		add_error(visb_visualiser,'Cannot parse VisB event predicate without event name:',PredStr,Pos),
2350		TypedPred = b(truth,pred,[]).
2351		construct_pre_post_pred(OpName,Pos,String,TypedExpr) :- special_operation(OpName),!,
2352		% we have a special operation; allow to provide an expression with options/parameters
2353		construct_pre_post_for_special(Pos,String,TypedExpr).
2354		construct_pre_post_pred(OpName,Pos,String,TypedPred) :-
2355		atom_codes(String,Codes), replace_special_patterns(Codes,RCodes,Pos), %format("Replaced : ~S~n",[RCodes]),
2356		get_visb_extra_scope([identifier(VisBExtraScope)]),
2357		visb_click_meta_b_type(MetaRecType),
2358		ExtraScope = [identifier([b(identifier('VISB_CLICK_META_INFOS'),MetaRecType,[visb_generated])|VisBExtraScope])],
2359		(b_parse_machine_operation_pre_post_predicate(RCodes,ExtraScope,TypedPred,OpName,gen_parse_errors_for(Pos))
2360		-> true
2361		; add_error(visb_visualiser,'Error for VisB event predicate:',String,Pos),
2362		TypedPred = b(truth,pred,[])
2363		).
2364
2365		construct_pre_post_for_special(Pos,Pred,TypedExpr) :- member(Pred,[btrue,bfalse]), !,
2366		add_warning(visb_visualiser,'Special operations require an expression specifying the parameter values, not a predicate: ',Pred,Pos),
2367		TypedExpr = b(integer(0),integer,[]).
2368		construct_pre_post_for_special(Pos,String,TypedExpr) :-
2369		atom_codes(String,Codes),
2370		GenParseErrors=gen_parse_errors_for(Pos),
2371		parse_expr(Codes,TypedExpr,GenParseErrors). % TODO: should we require a predicate instead, and provide arg names?
2372
2373		% replace special patterns by dummy values to avoid error messages in ProB2-UI
2374		replace_special_patterns([],[],_Pos) :- !.
2375		replace_special_patterns([37|T],Res,Pos) :- !, % percentage sign %
2376		replace_aux(T,Res,Pos).
2377		replace_special_patterns([H|T],[H|RT],Pos) :- !, replace_special_patterns(T,RT,Pos).
2378
2379		replace_aux(Input,Res,Pos) :-
2380		replace_pat(PAT,Replacement),
2381		append(PAT,T,Input),
2382		!,
2383		atom_codes(PatAtom,PAT),
2384		ajoin(['The %',PatAtom,' pattern is obsolete. Please use VISB_CLICK_META_INFOS\'',PatAtom,' instead.'],Msg),
2385		add_warning(visb_visualiser,Msg,'',Pos),
2386		append(Replacement,ResT,Res),
2387		replace_special_patterns(T,ResT,Pos).
2388		replace_aux(Input,[37|Res],Pos) :- !, replace_special_patterns(Input,Res,Pos).
2389
2390		replace_pat("shiftKey","VISB_CLICK_META_INFOS'shiftKey").
2391		replace_pat("metaKey","VISB_CLICK_META_INFOS'metaKey").
2392		replace_pat("pageX","VISB_CLICK_META_INFOS'pageX").
2393		replace_pat("pageY","VISB_CLICK_META_INFOS'pageY").
2394
2395
2396		% small utils:
2397		% ----------------
2398
2399		% a variation of between/3 with a step argument
2400		between(From,To,_,_) :- From > To, !,fail.
2401		between(From,_,_,From).
2402	?	between(From,To,Step,Elem) :- F1 is From+Step, between(F1,To,Step,Elem).
2403
2404
2405		parse_expr(ExprCodes,TypedExpr,_GenParseErrors) :-
2406		is_simple_classical_b_identifier_codes(ExprCodes),
2407		atom_codes(DefID,ExprCodes),
2408		visb_definition(DefID,Type,_DefFormula,Class,_VPos,_),
2409		!,
2410		TypedExpr = b(identifier(DefID),Type,[type_of_formula(Class)]).
2411		parse_expr(ExprCodes,TypedExpr,GenParseErrors) :-
2412		temporary_set_preference(allow_arith_operators_on_reals,true,CHNG),
2413		get_visb_extra_scope(ExtraScope),
2414		% formatsilent('Parsing: ~s (extra ids: ~w)~n',[ExprCodes,ExtraScope]), start_ms_timer(T1),
2415		call_cleanup(bmachine:b_parse_machine_expression_from_codes_with_prob_ids(ExprCodes,ExtraScope,TypedExpr,
2416		GenParseErrors),
2417		reset_temporary_preference(allow_arith_operators_on_reals,CHNG)).
2418		%stop_ms_walltimer_with_msg(T1,'parsing: ').
2419		% TODO: we could share a machine parameter M like in prob2_interface
2420		% so that b_type_expression_for_full_b_machine will load machine only once
2421		% cf b_type_open_predicate_for_full_b_machine
2422
2423		determine_type_of_visb_formula(b(_,_,[type_of_formula(Class)]),all,Res) :- !,
2424		Res = Class. % generated by VisB, TODO: store UsedTIds in type_of_formula(.)
2425		determine_type_of_visb_formula(TypedExpr,TIds,Class) :-
2426		determine_type_of_formula_with_visb_defs(TypedExpr,TIds,Class).
2427
2428		%check for used_ids inside TypedExpr an see what type of visb_definition are used
2429		determine_type_of_formula_with_visb_defs(TypedExpr,TIds,ResClass) :-
2430		determine_type_of_formula(TypedExpr,TIds,Class1), % compute class w/o knowledge of VisB definitions
2431	?	(class_more_general_than(Class2,Class1),
2432	?	required_by_visb_def(TIds,Class2) -> Class=Class2
2433		; Class=Class1),
2434		(Class=requires_variables -> ResClass=Class
2435		; expression_requires_state(TypedExpr) -> ResClass = requires_variables
2436		; ResClass=Class).
2437
2438
2439		expression_requires_state(TypedExpr) :-
2440		(map_over_bexpr(sub_expression_requires_state,TypedExpr) -> true ; fail).
2441		% TODO: should we also check is_not_declarative/1 ? e.g., for RANDOM or CHANGED
2442		sub_expression_requires_state(external_pred_call(P,_)) :- external_function_requires_state(P).
2443		sub_expression_requires_state(external_function_call(P,_)) :- external_function_requires_state(P).
2444
2445
2446		class_more_general_than(requires_variables,requires_nothing).
2447		class_more_general_than(requires_variables,requires_constants).
2448		class_more_general_than(requires_constants,requires_nothing).
2449
2450		required_by_visb_def(TIds,Class) :-
2451	?	member(TID,TIds), get_texpr_id(TID,ID),visb_definition(ID,_,_,Class,_,_).
2452
2453
2454		get_visb_extra_scope([identifier(ExtraIDs)]) :-
2455		get_visb_extra_identifiers(ExtraIDs).
2456		get_visb_extra_identifiers(ExtraIDs) :-
2457		findall(b(identifier(ID),Type,[visb_generated]),visb_definition(ID,Type,_,_,_,_),ExtraIDs).
2458
2459
2460		force_get_attr_nr(Attr,List,Nr,File) :-
2461		force_del_attr_with_pos(Attr,List,AttrVal,_,File,Pos),!,
2462		get_number_value(AttrVal,Nr,Attr,Pos).
2463
2464		get_number_value(AttrVal,Nr,Attr,Pos) :-
2465		(AttrVal = number(Nr) -> true
2466		; AttrVal = string(StrAttrVal),
2467		atom_codes(StrAttrVal,AttrValC),
2468		parse_expr(AttrValC,TypedExpr,gen_parse_errors_for(Pos)),
2469		determine_type_of_visb_formula(TypedExpr,UsedTIds,Class)
2470		% Class = requires_nothing, requires_constants, requires_variables
2471		->
2472		(Class = requires_variables
2473		-> ajoin(['The JSON formula for the attribute"',Attr,
2474		'" must not depend on variables:'],Msg),
2475		add_error(visb_visualiser,Msg,StrAttrVal,Pos),fail
2476		; Class = requires_constants,
2477		\+ is_concrete_constants_state_id(_)
2478		-> ajoin(['The JSON formula for the attribute"',Attr,
2479		'" depends on constants which have not been set up (via SETUP_CONSTANTS):'],Msg),
2480		add_error(visb_visualiser,Msg,StrAttrVal,Pos),fail
2481		; get_texpr_type(TypedExpr,Type),
2482		is_number_type(Type)
2483		-> (eval_static_def(Class,'VisB attribute',Attr,TypedExpr,UsedTIds,ResVal,Pos)
2484		-> get_number_from_bvalue(ResVal,Nr)
2485		; Class = requires_constants,
2486		multiple_concrete_constants_exist
2487		-> ajoin(['The JSON formula for the attribute"',Attr,
2488		'" depends on constants and multiple solutions for SETUP_CONSTANTS exist:'],Msg),
2489		add_warning(visb_visualiser,Msg,StrAttrVal,Pos),fail
2490		)
2491		; get_texpr_type(TypedExpr,Type),
2492		% it could produce a string which is a number; we could try and convert to a number
2493		ajoin(['The type ',Type,' of the JSON value formula for the attribute "',Attr,
2494		'" is not a number:'],Msg),
2495		add_error(visb_visualiser,Msg,StrAttrVal,Pos),fail
2496		)
2497		; ajoin(['The JSON value for the attribute "',Attr,'" cannot be parsed as a number:'],Msg),
2498		add_error(visb_visualiser,Msg,AttrVal,Pos),fail).
2499
2500		is_number_type(integer).
2501		is_number_type(real).
2502
2503
2504		get_number_from_bvalue(int(Nr),Res) :- !, Res=Nr.
2505		get_number_from_bvalue(Term,Res) :- is_real(Term,Nr),!,Res=Nr.
2506
2507		% ----------------------------------
2508
2509
2510		% computing updates to SVG for a given StateId:
2511		% predicate to obtain required setAttribute changes to visualise StateId
2512		% looks up visb_item facts but also evaluates VISB_SVG_UPDATE definitions
2513		get_change_attribute_for_state(StateId,SvgID,SvgAttribute,Value) :-
2514		visb_state_can_be_visualised(StateId),
2515		set_error_context(checking_context('VisB:','computing attributes for state')),
2516		set_context_state(StateId,get_change_attribute_for_state), % also sets it for external functions
2517		% TODO: also set history so that get_current_history in external_functions is more reliable
2518	?	call_cleanup((get_expanded_bstate(StateId,ExpandedBState), % inside call_cleanup: contexts cleared if it fails
2519		get_change_aux(StateId,ExpandedBState,SvgID,SvgAttribute,Value)),
2520		(clear_context_state,clear_error_context)).
2521
2522		get_change_aux(StateId,ExpandedBState,SvgID,SvgAttribute,Value) :-
2523	?	get_aux2(StateId,ExpandedBState,SvgID0,SvgAttribute0,Value0,DefPos),
2524		post_process_visb_item(SvgID0,SvgAttribute0,Value0,DefPos,SvgID,SvgAttribute,Value).
2525		get_aux2(StateId,ExpandedBState,SvgID,SvgAttribute,Value,DefPos) :-
2526		% first get updates from DEFINITIONS which usually return sets of records
2527	?	get_svg_object_updates_from_definitions(ExpandedBState,SvgID,SvgAttribute,Value,DefPos),
2528		debug_format(19,' VISB_SVG_UPDATE ~w:~w = ~w (in state ~w)~n',[SvgID,SvgAttribute,Value,StateId]).
2529		get_aux2(StateId,ExpandedBState,SvgID,SvgAttribute,Value,Pos) :-
2530		% TODO: check if visibility item exists, and if value is false: do not compute the rest
2531	?	get_visb_item_formula(SvgID,SvgAttribute,Formula,Pos,ExpandedBState),
2532		% TODO: if UsedIds=[] only set attribute once, if it requires_only_constants : ditto
2533		evaluate_visb_formula(Formula,'VisB item',SvgID,ExpandedBState,FValue,Pos),
2534		%b_value_to_string(FValue,Value),
2535		extract_attr_value(SvgAttribute,FValue,Value,Pos),
2536		debug_format(19,' VisB item ~w:~w = ~w (in state ~w)~n',[SvgID,SvgAttribute,Value,StateId]).
2537
2538		% post-process certain items, like title to adapt the value and id:
2539		% SVG does not support a title attribute; we need a title child and set its text attribute
2540		post_process_visb_item(SvgID,title,Value,Pos,NewID,text,NewValue) :-
2541		(visb_svg_object_debug_info(SvgID,DebugInfo) -> ajoin([Value,'\n',DebugInfo],NewValue) ; NewValue=Value),
2542	?	(visb_svg_parent(SvgID,TitleID),
2543		visb_svg_object(TitleID,title,_,_,_)
2544		-> NewID=TitleID,
2545		debug_format(9,'Redirecting title update for ~w to child object ~w~n',[SvgID,TitleID])
2546		; visb_svg_object(SvgID,_SVG_Class,_RestAttrs,_Desc,_Pos1)
2547		-> % this is an object we created
2548		add_warning(visb_visualiser,'Could not find title child object, be sure to define a static title attribute for SVG object: ',SvgID,Pos),
2549		fail
2550		; add_warning(visb_visualiser,'SVG does not natively support title attributes: ',SvgID,Pos),
2551		fail
2552		),!.
2553		post_process_visb_item(SvgID,Attr,Value,_,SvgID,Attr,Value).
2554
2555		% ------------------
2556
2557		% convert B value to Json String
2558		b_value_to_string(string(SValue),Res) :- !, Res=SValue. % What about quoting,...?
2559		b_value_to_string(FValue,Res) :-
2560		translate_bvalue_to_codes(FValue,ValCodes),
2561		atom_codes(Res,ValCodes).
2562
2563		% attributes for which we convert pairs to the concatenation of strings
2564		is_id_or_text_attribute(id).
2565		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
2566		is_id_or_text_attribute('trigger_id').
2567		is_id_or_text_attribute('trigger-id').
2568		is_id_or_text_attribute(A) :- is_text_attribute(A).
2569		% children
2570		is_text_attribute('text').
2571		is_text_attribute('transform').
2572		is_text_attribute('event'). % for VISB_SVG_EVENTS
2573		is_text_attribute('predicate'). % for VISB_SVG_EVENTS
2574		is_text_attribute('svg_class').
2575
2576
2577		b_value_to_id_string(Val,String) :- b_val_to_id_string_aux(Val,add_underscore,String).
2578		b_value_to_attr_string(Val,String) :- b_val_to_id_string_aux(Val,no_underscore,String).
2579
2580		% a special string conversion which e.g., allows to use things like ("ab",2) as id which gets translated to ab2
2581		% also useful for text attributes
2582		b_val_to_id_string_aux(string(SValue),_,Res) :- !, Res=SValue.
2583		b_val_to_id_string_aux((A,B),Add,Res) :- !,
2584		b_val_to_id_string_aux(A,Add,VA), b_val_to_id_string_aux(B,Add,VB),
2585		(Add=add_underscore
2586		-> atom_concat('_',VB,VB1) % introduce separator; in case we have things like numbers so that (12,3) /= (1,23)
2587		; VB1=VB % for fields like predicate, transform, ... we do not want additional underscores
2588		),
2589		atom_concat(VA,VB1,Res).
2590		b_val_to_id_string_aux(Set,Add,Res) :- singleton_set(Set,El),!, b_val_to_id_string_aux(El,Add,Res).
2591		% TODO: maybe convert sequence of values using conc
2592		b_val_to_id_string_aux(FValue,_,Res) :- b_value_to_string(FValue,Res).
2593
2594
2595
2596		% get either a regular VisB item or an item associated with a VisB event and its enabled status
2597		get_visb_item_formula(SvgID,SvgAttribute,Formula,Pos,_ExpandedBState) :-
2598	?	visb_item(SvgID,SvgAttribute,Formula,_UsedIds,_Desc,Pos,_). % regular VisB item
2599		get_visb_item_formula(SvgID,SvgAttribute,Formula,Pos,ExpandedBState) :- % item within VisB event
2600		visb_event_enable_list(OpName,TypedPred,EnableList,_,ItemPos),
2601		debug_format(19,'Checking enabledness of VisB event ~w~n',[OpName]),
2602		(check_enabled(OpName,TypedPred,ExpandedBState,ItemPos)
2603		-> Formula=EnabledValExpr
2604		; Formula=DisabledValExpr
2605		),
2606		member(visb_enable_item(SvgID,SvgAttribute,EnabledValExpr,DisabledValExpr,Pos), EnableList).
2607
2608		check_enabled(OpName,Pred,ExpandedBState,Pos) :-
2609		special_operation(OpName),!,
2610		special_operation_enabled(OpName,Pred,ExpandedBState,Pos).
2611		check_enabled(OpName,Pred,ExpandedBState,Pos) :-
2612		b_is_operation_name(OpName),
2613		% TODO: see if we can use GUARD without execution
2614		% TODO: not yet working for XTL mode
2615		execute_operation_by_predicate_in_state_with_pos(ExpandedBState,OpName,Pred,_OpTerm,_NewState,Pos,_).
2616
2617
2618		get_expanded_bstate(StateId,ExpandedBState) :-
2619		\+ b_or_z_mode,!,
2620		StateId \= root,
2621		% in XTL mode we need to access the state via external functions like STATE_PROPERTY
2622		get_static_visb_state([],ExpandedBState).
2623		get_expanded_bstate(StateId,ExpandedBState) :-
2624		visited_expression(StateId,State),
2625		state_corresponds_to_initialised_b_machine(State,BState),
2626		debug_format(19,'Adding VisB definitions to state: ~w~n',[StateId]),
2627		add_prob_deferred_set_elements_to_store(BState,BState2,visible), % add prob_ids
2628		findall(visb_definition(DefID,Type,DefFormula,Class,VPos,Special),
2629		visb_definition(DefID,Type,DefFormula,Class,VPos,Special),DefList),
2630		eval_defs(DefList,BState2,ExpandedBState).
2631
2632
2633		evaluate_static_visb_formula(Formula,Kind,Nr,InState,ResValue,Pos) :-
2634		get_static_visb_state(InState,StaticState),
2635		evaluate_visb_formula(Formula,Kind,Nr,StaticState,ResValue,Pos).
2636
2637		evaluate_visb_formula(Formula,Kind,Nr,BState2,ResValue,Pos) :-
2638		% add_message(visb,'Evaluating: ',Kind:Nr,Pos), debug:nl_time, %set_prolog_flag(profiling,on), print_profile,
2639	?	(b_compute_explicit_epression_no_wf(Formula,[],BState2,ResValue,Kind,Nr,Pos) -> true
2640		; add_error(visb_visualiser,'Evaluation of VisB formula failed:',Formula,Pos),
2641		fail).
2642
2643		% evaluate VisB definitions in order one by one, adding values to state
2644		eval_defs([],State,State).
2645		eval_defs([visb_definition(ID,_,TypedExpr,_Class,VPos,Special)|T],State0,State2) :-
2646		(Special \= regular_def
2647		-> State1=State0 % ignore special defs; they are processed separately
2648		; b_compute_expression_nowf(TypedExpr,[],State0,ResValue,'VisB definition',ID,VPos),
2649		State1 = [bind(ID,ResValue)|State0], % store value for later definitions and VisB items
2650		(debug_level_inactive_for(19)-> true
2651		; translate_bvalue_to_codes_with_limit(ResValue,2000,RC),
2652		formatsilent(' VisB definition ~w == ~s~n',[ID,RC]))
2653		),
2654		eval_defs(T,State1,State2).
2655
2656		% check if we have a static value for a VisB definition:
2657		visb_def_static_value(DefID,Value) :-
2658	?	visb_definition(DefID,_,b(value(Value),_,_),Class,_,SpecialClass),
2659		SpecialClass = regular_def,
2660		(Class = requires_nothing ; Class = requires_constants). % probably we do not need to check this, as we have value/1
2661
2662		get_static_visb_state(InState,FullState) :-
2663		findall(bind(DefID,Value),visb_def_static_value(DefID,Value),FullState,InState).
2664		% TO DO: get state with deferred_set_elements,...
2665
2666		% get a definition either from B DEFINITIONS section, or if not present from the VisB JSON special definition list
2667		get_and_eval_special_definition(Prefix,DefName,JSONBackup,DefPos,ResValue,InlineObjects) :-
2668		(b_sorted_b_definition_prefixed(expression,Prefix,DefName,DefPos),
2669	?	b_get_typed_definition(DefName,[variables_and_additional_defs],TBody)
2670		;
2671		visb_special_definition(JSONBackup,DefName,_Type,TBody,_Class,DefPos)
2672		),
2673		% TODO: warn if we use static SVG
2674	?	get_typed_static_definition_with_constants_state(DefName,TBody,
2675		Body,DefPos,ConstantsState,InlineObjects,no_separation),
2676		evaluate_visb_formula(Body,DefName,'',ConstantsState,ResValue,DefPos).
2677
2678		% check if we have a DEFINITION with the indicated prefix
2679		special_definition_exists(Prefix) :-
2680		b_sorted_b_definition_prefixed(expression,Prefix,_DefName,_DefPos).
2681
2682		% --------------------------
2683
2684		% debugging features to inspect all created SVG objects
2685		tcltk_get_visb_objects(list([Header|AllObjects])) :-
2686		Header = list(['SVG-ID','svg_class','Attribute','Value']),
2687		findall(list([SvgID,SvgClass,Attr,Value]),
2688		(visb_svg_obj_with_parent(SvgID,SvgClass,AttrList,true),
2689		(member(svg_attribute(Attr,Value),AttrList) ;
2690		visb_svg_parent(SvgID,Value), Attr=children)
2691		), Childs),
2692		findall(list([SvgID,SvgClass,Attr,Value]),
2693		(visb_svg_obj_with_parent(SvgID,SvgClass,AttrList,false),
2694		member(svg_attribute(Attr,Value),AttrList)
2695		),AllObjects, Childs).
2696
2697		% debugging features to inspect all created SVG objects
2698		tcltk_get_visb_hovers(list([Header|AllObjects])) :-
2699		Header = list(['SVG-ID','ID','Attribute','EnterValue', 'ExitValue']),
2700		findall(list([SvgID,ID,Attr,EnterVal,ExitVal]),
2701		visb_hover(SvgID,ID,Attr,EnterVal,ExitVal,_Pos), AllObjects).
2702
2703		% debugging features to inspect items
2704		tcltk_get_visb_items(Res) :-
2705		current_state_id(ID),
2706		tcltk_get_visb_items(ID,Res).
2707		tcltk_get_visb_items(_StateId,Res) :-
2708		\+ visb_file_is_loaded(_),!,
2709		Res = list(['No VisB JSON file loaded']).
2710		tcltk_get_visb_items(StateId,list([Header|AllItems])) :-
2711		Header = list(['SVG-ID','Attribute','Value']),
2712		get_preference(translation_limit_for_table_commands,Limit),
2713		findall(list([SvgID,SvgAttribute,Val]),
2714		get_change_attribute_for_state(StateId,SvgID,SvgAttribute,Val),
2715		Items),
2716		findall(list([DefID,'VisB Definition',DValS]),
2717		(get_expanded_bstate(StateId,ExpandedBState),
2718		reverse(ExpandedBState,RS),
2719		member(bind(DefID,DVal),RS),
2720		visb_definition(DefID,_,_,_,_,_),
2721		translate_bvalue_with_limit(DVal,Limit,DValS)),
2722		AllItems, Items).
2723
2724		:- use_module(probsrc(translate),[translate_event_with_limit/3]).
2725		tcltk_get_visb_events(Res) :-
2726		current_state_id(ID),
2727		tcltk_get_visb_events(ID,Res).
2728		tcltk_get_visb_events(_StateId,Res) :-
2729		\+ visb_file_is_loaded(_),!,
2730		Res = list(['No VisB JSON file loaded']).
2731		tcltk_get_visb_events(StateId,list([Header|AllItems])) :-
2732		Header = list(['SVG-ID','Event','Target']),
2733		get_preference(translation_limit_for_table_commands,Limit),
2734		findall(list([SvgID,EventStr,NewStateId]),
2735		(perform_visb_click_event(SvgID,[],StateId,_Event,OpTerm,NewStateId,Res),
2736		(Res=[] -> EventStr='disabled' ; translate_event_with_limit(OpTerm,Limit,EventStr))
2737		),
2738		AllItems).
2739		% --------------------------
2740
2741		% for ProB2-UI
2742
2743		:- use_module(probsrc(translate),[translate_bexpression_with_limit/3]).
2744		get_visb_items(List) :-
2745		findall(visb_item(SvgID,Attr,TS,Desc,Pos),
2746		(visb_item(SvgID,Attr,TypedExpr,_Used,Desc,Pos,_),
2747		translate_bexpression_with_limit(TypedExpr,1000,TS)), List).
2748
2749		get_visb_attributes_for_state(StateId,List) :-
2750		% some external functions like ENABLED are evaluated in current state; it might be useful to set_current_state
2751		(visb_file_is_loaded(_) -> true
2752		; add_warning(visb_visualiser,'No VisB visualisation loaded, cannot get attributes for state: ',StateId)),
2753		findall(set_attr(SvgID,SvgAttribute,Val),
2754		get_change_attribute_for_state(StateId,SvgID,SvgAttribute,Val),
2755		List).
2756
2757		% for ProB2-UI
2758		get_visb_click_events(List) :-
2759		findall(execute_event(SvgID,Event,Preds),
2760		get_visb_event(SvgID,Event,Preds), List).
2761		get_visb_event(SvgID,Event,Preds) :- visb_event(SvgID,Event,Preds,_,_,_File,_Pos).
2762		get_visb_event(SvgID,'',[]) :- % add a virtual empty event for SVG Ids with hovers but no events
2763		visb_has_hovers(SvgID),
2764		\+ visb_event(SvgID,_,_,_,_,_File,_Pos).
2765
2766
2767		:- use_module(probsrc(state_space), [extend_trace_by_transition_ids/1]).
2768		% perform a click on a VisB SVG ID in the animator
2769		tcltk_perform_visb_click_event(SvgID) :- current_state_id(StateId),
2770		(perform_visb_click_event(SvgID,[],StateId,TransitionIDs)
2771		-> formatsilent('Clicking on ~w in state ~w resulted in transition id sequence ~w~n',[SvgID,StateId,TransitionIDs]),
2772		extend_trace_by_transition_ids(TransitionIDs)
2773		; add_error(visb_visualiser,'Cannot perform VisB click on: ',SvgID)
2774		).
2775
2776		% computes the effect of clicking on an SvgID in StateId
2777		% it returns either empty list if the visb_event is not feasible or a list of transition ids
2778		% it fails if SvgID has no events associated with it
2779		perform_visb_click_event(SvgID,MetaInfos,StateId,ResTransitionIds) :-
2780		perform_visb_click_event(SvgID,MetaInfos,StateId,_,_,_,ResTransitionIds).
2781		perform_visb_click_event(SvgID,MetaInfos,StateId,OpName,OpTerm,NewStateId,ResTransitionIds) :-
2782		get_svgid_with_events(SvgID,_), % check before setting contexts, which would otherwise not be cleared
2783		set_error_context(checking_context('VisB:','performing click event')),
2784		set_context_state(StateId,perform_visb_click_event),
2785		call_cleanup((get_expanded_bstate(StateId,ExpandedBState),
2786		perform_aux(SvgID,StateId,ExpandedBState,OpName,OpTerm,NewStateId,ResTransitionIds,MetaInfos)),
2787		(clear_context_state,clear_error_context)).
2788
2789		get_svgid_with_events(SvgID,FirstOpName) :- visb_event(SvgID,FirstOpName,_,_,_,_File,_Pos).
2790
2791
2792		:- use_module(probsrc(tools),[safe_read_term_from_atom/2]).
2793		:- use_module(probsrc(state_space),[transition/4]).
2794		perform_aux(SvgID,StateId,_ExpandedBState,OpName,OpTerm,NewStateId,ResTransitionIds,_MetaInfos) :-
2795		\+ b_or_z_mode,
2796		% just look up transition/4 entries in state space
2797		% TODO: maybe provide this possibility for B models, even if using explicit parameter values is more robust
2798		get_visb_event_operation(SvgID,OpName,Preds,_ExecKind,_Pred,Pos),
2799		safe_read_term_from_atom(OpName,OpTerm0),
2800		(xtl_mode -> check_xtl_direct_transition_candidate(OpTerm0,Preds,Pos), OpTerm=OpTerm0 ; true), !,
2801		% for XTL: use exec by pred for arity 0, otherwise try to find transition term in state space
2802		if((transition(StateId,OpTerm,TransID,NewStateId),
2803		match_operation(OpTerm,OpName)), % match is relevant if \+xtl_mode
2804		ResTransitionIds = [TransID],
2805		return_disabled(SvgID,StateId,OpName,OpTerm,NewStateId,ResTransitionIds)
2806		).
2807		perform_aux(SvgID,StateId,ExpandedBState,OpName,OpTerm,NewStateId,ResTransitionIds,MetaInfos) :-
2808		%state_space:portray_state_space,
2809		if(execute_visb_event_by_predicate(SvgID,StateId,ExpandedBState,OpName,OpTerm,NewStateId,TransIds,MetaInfos),
2810		ResTransitionIds = TransIds,
2811		return_disabled(SvgID,StateId,OpName,OpTerm,NewStateId,ResTransitionIds)).
2812
2813		check_xtl_direct_transition_candidate(OpTerm,Preds,Pos) :-
2814		nonvar(OpTerm), % upper case event names are interpreted as Prolog variables -> use exec by pred (or FIXME)
2815		functor(OpTerm,_,Ar), Ar>0, % use exec by pred for arity 0, otherwise try to find transition term in state space
2816		(Preds \= []
2817		-> add_warning(visb_visualiser,'Ignoring predicates for VisB XTL event with explicit transition term (use predicate to provide parameter values): ',OpTerm,Pos)
2818		; true).
2819
2820		return_disabled(SvgID,StateId,OpName,OpTerm,NewStateId,ResTransitionIds) :-
2821		OpTerm = disabled, NewStateId = StateId,
2822		get_svgid_with_events(SvgID,OpName),
2823		ResTransitionIds = []. % visb_event not enabled
2824
2825		:- use_module(probsrc(tools_strings),[match_atom/2]).
2826		:- use_module(probsrc(specfile),[get_operation_name/2]).
2827		match_operation(OpTerm,OpTerm) :- !.
2828		match_operation(OpTerm,OpName) :- atom(OpName),
2829		(get_operation_name(OpTerm,OpName)
2830		; match_atom(OpName,OpTerm) % match an atom string with a compound term
2831		),!.
2832
2833		execute_visb_event_by_predicate(SvgID,StateId,ExpandedBState,OpName,OpTerm,NewStateId,TransIds,MetaInfos) :-
2834		get_visb_event_operation(SvgID,OpName,_,EventExecKind,Pred,Pos),
2835		get_actual_execution_kind(EventExecKind,ExecKind),
2836		build_visb_click_meta_object(MetaInfos,BMetaInfos),
2837		bsyntaxtree:replace_id_by_expr(Pred,'VISB_CLICK_META_INFOS',BMetaInfos,NPred),
2838		exec_aux(SvgID,StateId,ExpandedBState,OpName,ExecKind,NPred,Pos,OpTerm,NewStateId,TransIds).
2839
2840		build_visb_click_meta_object(MetaInfos,BMetaInfos) :-
2841		(member(alt_key,MetaInfos) -> AltKey = pred_true ; AltKey = pred_false),
2842		(member(ctrl_key,MetaInfos) -> CtrlKey = pred_true ; CtrlKey = pred_false),
2843		(member(meta_key,MetaInfos) -> MetaKey = pred_true ; MetaKey = pred_false),
2844		(member(pageX(PageX),MetaInfos) -> true ; PageX = 0), % fallback
2845		(member(pageY(PageY),MetaInfos) -> true ; PageY = 0), % fallback
2846		(member(shift_key,MetaInfos) -> ShiftKey = pred_true ; ShiftKey = pred_false),
2847		findall(','(string(Var),string(VarValue)), member(js_var(Var,VarValue), MetaInfos), JSVars),
2848
2849		visb_click_meta_b_type(BType),
2850		BMetaInfos = b(value(rec([
2851		field(altKey,AltKey),
2852		field(ctrlKey,CtrlKey),
2853		field(jsVars,JSVars),
2854		field(metaKey,MetaKey),
2855		field(pageX,int(PageX)),
2856		field(pageY,int(PageY)),
2857		field(shiftKey,ShiftKey)
2858		])),BType,[visb_generated]).
2859
2860		visb_click_meta_b_type(record([
2861		field(altKey,boolean),
2862		field(ctrlKey,boolean),
2863		field(jsVars,set(couple(string,string))),
2864		field(metaKey,boolean),
2865		field(pageX,integer),
2866		field(pageY,integer),
2867		field(shiftKey,boolean)
2868		])).
2869
2870		:- use_module(probsrc(tcltk_interface),[compute_all_transitions_if_necessary/2]).
2871		:- use_module(library(random),[random_member/2]).
2872		:- use_module(extrasrc(mcts_game_play), [mcts_auto_play/4, mcts_auto_play_available/0]).
2873		:- use_module(probsrc(tools_timeout), [time_out_with_factor_call/3]).
2874		:- use_module(probsrc(external_functions),[call_external_function/7]).
2875		:- use_module(probsrc(bsyntaxtree), [is_truth/1]).
2876		:- use_module(probsrc(specfile), [get_specific_max_operations_for_operation/2]).
2877		exec_aux(SvgID,StateId,_ExpandedBState,OpName,ExecKind,Pred,_Pos,OpTerm,NewStateId,[TransId]) :-
2878		choose_among_transitions_kind(ExecKind),
2879		is_truth(Pred),
2880		b_is_operation_name(OpName),
2881		\+ get_specific_max_operations_for_operation(OpName,0), % otherwise execute by predicate should be done
2882		% TODO: check max_reached_or_timeout_for_node?
2883		% TODO: further execution kinds like tcltk_random_perform2: explore_open, min_out_degree
2884		!,
2885		write(random_click_for(SvgID,StateId,OpName,ExecKind)),nl,
2886		compute_all_transitions_if_necessary(StateId,false),
2887		findall(rtr(OpTerm,TransId,NewStateId),
2888		(transition(StateId,OpTerm,TransId,NewStateId),
2889		match_operation(OpTerm,OpName)),
2890		List),
2891		choose_transition(ExecKind,List,rtr(OpTerm,TransId,NewStateId)).
2892		exec_aux(SvgID,StateId,ExpandedBState,OpName,_,Pred,Pos,OpTerm,NewStateId,[TransId]) :-
2893		(csp_with_bz_mode -> fail % execute by predicate does not work properly yet with csp_and_b states
2894		; b_or_z_mode -> b_is_operation_name(OpName)
2895		; true), !, % note: ignores special definitions below if not B mode
2896		time_out_with_factor_call(
2897		exec_op_by_pred_aux(StateId,ExpandedBState,OpName,Pred,OpTerm,NewState,Pos,TransInfo),
2898		5, % min_max_time_out(10,100,15000)
2899		(ajoin(['TIME-OUT for VisB click on SVG ID ', SvgID,' while executing operation by predicate: '],Msg),
2900		add_warning(visb_visualiser,Msg,OpName,Pos),fail)),
2901		patch_state(NewState,StateId,PatchedNewState),
2902		% add transition to state space:
2903		tcltk_interface:add_trans_id_infos(StateId,OpTerm,PatchedNewState,NewStateId,TransId,TransInfo).
2904		%translate:print_bstate(PatchedNewState),nl.
2905		exec_aux(SvgID,StateId,_ExpandedBState,'MCTS_AUTO_PLAY',_,_Pred,Pos,OpTerm,NewStateId,[TransId]) :- !,
2906		mcts_auto_play_available,
2907		% TODO: allow to set SimRuns, TimeOut in Pred
2908		add_debug_message(visb_visualiser,'Performing MCTS_AUTO_PLAY for click on: ',SvgID,Pos),
2909		mcts_auto_play(StateId,OpTerm,TransId,NewStateId).
2910		% TODO: more general call via call_external_substitution(FunName,Args,InState,OutState,Info,WF)
2911		exec_aux(_SvgID,StateId,_ExpandedBState,'RANDOM_ANIMATE',_,_Pred,_Pos,OpTerm,NewStateId,[TransId]) :- !,
2912		compute_all_transitions_if_necessary(StateId,false),
2913		findall(rtr(OpTerm,TransId,NewStateId),transition(StateId,OpTerm,TransId,NewStateId),List),
2914		random_member(rtr(OpTerm,TransId,NewStateId),List).
2915		% see tcltk_interface:tcltk_random_perform2 and allow Kind: fully_random, no_self_loops, heuristics, ...
2916		% split with ; ?
2917		exec_aux(SvgID,StateId,ExpandedBState,'RANDOM_ANIMATE_UNTIL_LTL',_,LTLExpr,Pos,OpTerm,NewStateId,TransIds) :- !,
2918		OpTerm = 'RANDOM_ANIMATE_UNTIL_LTL',
2919		(get_texpr_type(LTLExpr,string),
2920		evaluate_visb_formula(LTLExpr,'RANDOM_ANIMATE_UNTIL_LTL',SvgID,ExpandedBState,Value,Pos),
2921		Value = string(LTLFormula)
2922		-> tcltk_interface:tcltk_animate_until(LTLFormula,StateId,1000,ltl_state_property,_Steps,_Res,NewStateId,TransIds)
2923		; add_error(visb_visualiser,'Argument to RANDOM_ANIMATE_UNTIL_LTL must provide LTL formula as string:',StateId),
2924		fail
2925		).
2926		exec_aux(SvgID,StateId,ExpandedBState,ExternalFun,_,ArgEXPR,Pos,OpTerm,NewStateId,TransIds) :-
2927		external_fun_as_special_operation(ExternalFun),!,
2928		NewStateId=StateId, TransIds=[],
2929		evaluate_visb_formula(ArgEXPR,ExternalFun,1,ExpandedBState,ArgValue,Pos),
2930		convert_arg_value_to_list(ArgEXPR,ArgValue,UnEvalArgs,EvaluatedArgs),
2931		OpTerm =.. [ExternalFun|EvaluatedArgs],
2932		debug_format(9,'VisB event for ~w: calling external function ~w with ~w~n',[SvgID,ExternalFun,EvaluatedArgs]),
2933		% Note: we ignore the return value
2934		call_external_function(ExternalFun,UnEvalArgs,EvaluatedArgs,_Value,any,Pos,no_wf_available).
2935
2936		:- use_module(probsrc(state_space_exploration_modes),[heuristic_function_active/0,
2937		compute_heuristic_function_for_state_id/2]).
2938		% execution kinds which choose among the transitions already computed for the operation
2939		choose_among_transitions_kind(random).
2940		choose_among_transitions_kind(heuristic).
2941
2942		choose_transition(heuristic,List,Choice) :- heuristic_function_active,
2943		findall(H-RTR,(member(RTR,List), RTR=rtr(_,_,Dest),
2944		compute_heuristic_function_for_state_id(Dest,int(H))),HList),
2945		keysort(HList,[MinH-_|_]),!,
2946		findall(RTR,member(MinH-RTR,HList),MinList), % choose randomly among those with minimal heuristic value
2947		random_member(Choice,MinList).
2948		choose_transition(_,List,Choice) :- random_member(Choice,List).
2949
2950		% convert single argument expression to list; better would be to use a predicate with argument names
2951		convert_arg_value_to_list(b(couple(A,B),_,_),(VA,VB),[A|T],[VA|VT]) :- !, convert_arg_value_to_list(B,VB,T,VT).
2952		convert_arg_value_to_list(Arg,Val,[Arg],[Val]).
2953
2954		:- use_module(probsrc(b_state_model_check),[execute_operation_by_predicate_in_state_with_pos/7,
2955		xtl_execute_operation_by_predicate_in_state/8]).
2956		exec_op_by_pred_aux(StateId,ExpandedBState,OpName,Pred,OpTerm,NewState,Pos,TransInfo) :- xtl_mode,!,
2957		visited_expression(StateId,RawState),
2958		xtl_execute_operation_by_predicate_in_state(ExpandedBState,RawState,OpName,Pred,OpTerm,NewState,Pos,TransInfo).
2959		exec_op_by_pred_aux(_StateId,ExpandedBState,OpName,Pred,OpTerm,NewState,Pos,TransInfo) :-
2960		execute_operation_by_predicate_in_state_with_pos(ExpandedBState,OpName,Pred,OpTerm,NewState,Pos,TransInfo).
2961
2962		:- use_module(probsrc(bmachine), [b_is_variable/1,b_machine_has_constants/0]).
2963
2964		is_var_binding(bind(Var,_)) :- b_or_z_mode, b_is_variable(Var).
2965
2966
2967		% remove constants and VisB Definition entries from state:
2968		patch_state(NewState,_StateId,PatchedState) :-
2969		\+ b_or_z_mode, !, PatchedState=NewState. % XTL state is raw state
2970		patch_state(NewState,StateId,PatchedState) :-
2971		get_constants_id_for_state_id(StateId,ConstId),!,
2972		PatchedState = const_and_vars(ConstId,VarsState),
2973		include(is_var_binding,NewState,VarsState).
2974		patch_state(NewState,StateId,VarsState) :-
2975		(b_machine_has_constants
2976		-> add_error(visb_visualiser,'Could not extract constants id for state:',StateId),
2977		VarsState=NewState
2978		; include(is_var_binding,NewState,VarsState)).
2979
2980		% the next predicate gets all operations/events associated with SvgID in the order in which they were found
2981		% note that there is only one visb_event (the last one); all others are auxiliary
2982		get_visb_event_operation(SvgID,OpName,Preds,ExecKind,TypedPred,Pos) :- % check if there are more events registered:
2983		auxiliary_visb_event(SvgID,OpName,Preds,ExecKind,TypedPred,Pos).
2984		get_visb_event_operation(SvgID,OpName,Preds,ExecKind,TypedPred,Pos) :-
2985		visb_event(SvgID,OpName,Preds,ExecKind,TypedPred,_File,Pos).
2986
2987		% ---------------
2988
2989		get_visb_hovers(List) :-
2990		findall(hover(SvgID,ID,Attr,EnterVal,ExitVal),
2991		visb_hover(SvgID,ID,Attr,EnterVal,ExitVal,_), List).
2992
2993		get_visb_svg_objects(List) :-
2994		% TODO: remove objects inlined in get_visb_default_svg_file_contents
2995		topological_sort_svg_objects(SvgIDs),
2996		findall(visb_svg_object(SvgID,SvgClass,AttrList),
2997		(member(SvgID,SvgIDs),
2998		visb_svg_obj_with_parent(SvgID,SvgClass,AttrList,_)), List).
2999
3000		visb_svg_obj_with_parent(SvgID,SvgClass,AttrList,IsChild) :-
3001		visb_svg_object(SvgID,SvgClass,List,_Desc,_Pos),
3002		(visb_svg_child(SvgID,ParentId)
3003		-> IsChild=true, AttrList = [svg_attribute(parentId,ParentId)|List] % add parentId attribute for ProB2-UI
3004		; IsChild=false, AttrList = List).
3005
3006
3007		:- use_module(probsrc(tools),[top_sort/3]).
3008		:- use_module(library(ugraphs),[vertices_edges_to_ugraph/3]).
3009		topological_sort_svg_objects(SortedSVGObjects) :-
3010		findall(SvgID,visb_svg_object(SvgID,_,_,_,_),Vertices),
3011		findall(V-W,visb_svg_parent(V,W),Edges),
3012		vertices_edges_to_ugraph(Vertices,Edges,Graph),
3013		(top_sort(Graph,SortedSVGObjects,UnsortedNr)
3014		-> (UnsortedNr = 0 -> true
3015		; add_warning(visb_visualiser,'Cycle in SVG_OBJECTS parent/child graph, unsorted objects: ',UnsortedNr)
3016		)
3017		; SortedSVGObjects=Vertices,
3018		add_error(visb_visualiser,'Topological sorting of SVG_OBJECTS failed: ',Vertices)
3019		).
3020
3021		% ------------------
3022
3023		:- use_module(probsrc(bmachine),[b_absolute_file_name_relative_to_main_machine/2]).
3024		extended_static_check_default_visb_file :-
3025		(get_default_visb_file(VisBFile,Pos)
3026		% TODO: we could check if we have an visb_history(JSONFile,_,_) option
3027		-> extended_static_check_visb_file(VisBFile,Pos)
3028		; true).
3029
3030		extended_static_check_visb_file('',_InclusionPos) :- !,
3031		load_visb_file('').
3032		extended_static_check_visb_file(VisBFile,InclusionPos) :-
3033		b_absolute_file_name_relative_to_main_machine(VisBFile,AFile),
3034		(file_exists(AFile)
3035		-> load_visb_file(AFile)
3036		; add_warning(lint,'VISB_JSON_FILE does not exist: ',AFile,InclusionPos)
3037		).
3038
3039		% ---------------------------
3040
3041		% portray all VisB items in DEFINITION B syntax
3042		get_visb_ids(SIds) :-
3043		findall(Id,visb_id(Id),Ids),
3044		sort(Ids,SIds).
3045
3046		visb_id(ID) :- visb_svg_object(ID,_,_,_,_). % see svg_id_exists
3047		visb_id(ID) :- visb_item(ID,_,_,_,_,_,_), \+ visb_svg_object(ID,_,_,_,_).
3048		visb_id(ID) :- visb_event(ID,_,_,_,_,_,_), \+ visb_svg_object(ID,_,_,_,_).
3049		visb_id(ID) :- visb_hover(ID,_,_,_,_,_), \+ visb_svg_object(ID,_,_,_,_).
3050
3051		:- public portray_visb/0.
3052		portray_visb:-
3053		get_visb_ids(SIds), nth1(Nr,SIds,ID),
3054		%visb_svg_object(ID,SVG_Class,NewRestAttrs,Desc,Pos1),
3055		findall(field(Attr,b(value(StaticVal),any,[])),
3056		(visb_svg_object(ID,SVG_Class,StaticAttrs,Desc,_Pos1),
3057		( Attr=svg_class,StaticVal=string(SVG_Class)
3058		; Attr=comment,StaticVal=string(Desc)
3059		; member(svg_attribute(Attr,StaticVal),StaticAttrs))
3060		),
3061		StaticValues),
3062		findall(field(Attr,TypedExpr),
3063		visb_item(ID,Attr,TypedExpr,_UsedIds,_Desc,_PosStartOfItem,_Meta), % meta can contain override
3064		Updates,StaticValues),
3065		% TODO: incorporate events and hovers
3066		UpdateRec = b(rec(Fields),any,[]),
3067		gen_string(ID,IDS),
3068		Fields = [field(id,IDS) | Updates],
3069		(StaticValues=[] -> format('~nVISB_SVG_UPDATES~w == ',[Nr]) ; format('~nVISB_SVG_OBJECTS~w == ',[Nr])),
3070		translate:print_bexpr(UpdateRec), write(';'), nl,
3071		fail.
3072		portray_visb.
3073		gen_string(ID,b(string(ID),string,[])).
3074		% use_module(visbsrc(visb_visualiser)), visb_visualiser:portray_visb.