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