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