1		% Heinrich Heine Universitaet Duesseldorf
2		% (c) 2021-2026 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(visb_html_export,[generate_visb_html_for_history/1, generate_visb_html_for_history/2,
6		generate_visb_html_for_history_with_vars/1,
7		generate_visb_html_for_history_with_source/1,
8		generate_visb_html_for_current_state/1, generate_visb_html_for_current_state/2,
9		generate_visb_html_codes_for_states/3,
10		generate_visb_html/3,
11		get_visb_default_svg_file_contents/1]).
12
13		:- use_module(probsrc(module_information),[module_info/2]).
14		:- module_info(group,visualization).
15		:- module_info(description,'This module provides the VisB HTML export.').
16
17		:- use_module(library(lists)).
18		:- use_module(library(codesio),[write_to_codes/2]).
19		:- use_module(library(file_systems), [file_exists/1, file_property/3, delete_file/1]).
20		:- use_module(library(system), [datime/1]).
21		:- use_module(probsrc(error_manager)).
22		:- use_module(probsrc(preferences), [get_preference/2]).
23		:- use_module(probsrc(debug)).
24		:- use_module(probsrc(state_space), [visited_expression/2,
25		visited_state_corresponds_to_initialised_b_machine/1,
26		transition/4, invariant_violated/1, invariant_not_yet_checked/1,
27		current_state_id/1, time_out_for_node/3,
28		get_action_trace_with_limit/2, get_state_id_trace/1]).
29		:- use_module(probsrc(translate), [translate_bvalue_to_codes/2,
30		translate_bvalue_to_codes_with_limit/3,
31		translate_bexpression_with_limit/3, pretty_type/2,
32		set_unicode_mode/0, unset_unicode_mode/0,
33		translate_event_with_src_and_target_id/5]).
34		:- use_module(probsrc(specfile), [xtl_mode/0, b_or_z_mode/0,
35		state_corresponds_to_fully_setup_b_machine/2,
36		expand_to_constants_and_variables/3,
37		extract_variables_from_state/2, currently_opened_file/1,
38		get_internal_representation/1,
39		get_operation_description_for_transition/4,
40		get_specification_description/2]).
41		:- use_module(probsrc(tools), [start_ms_timer/1, stop_ms_walltimer_with_msg/2,
42		html_escape_codes/2, read_string_from_file/2,
43		b_string_escape_codes/2, gen_relative_path/3, string_escape/2]).
44		:- use_module(probsrc(tools_io), [safe_open_file/4, with_open_stream_to_codes/4,
45		write_file_to_stream/2]).
46		:- use_module(probsrc(tools_strings), [ajoin/2, number_codes_min_length/3, format_modified_info/2,
47		atom_tail_to_lower_case/2]).
48		:- use_module(probsrc(bmachine), [b_machine_name/1,
49		b_get_machine_variables/1, b_get_machine_constants/1,
50		b_top_level_operation/1, b_get_machine_animation_expression/2,
51		b_get_operation_variant/3, b_nth1_non_ignored_invariant/3,
52		b_get_machine_operation_signature/2, b_get_machine_operation_max/2]).
53		:- use_module(probsrc(bsyntaxtree), [get_texpr_type/2, get_texpr_id/2,
54		get_texpr_description/2, safe_create_texpr/3]).
55		:- use_module(probsrc(gensym), [gensym/2]).
56		:- use_module(probsrc(version), [version_str/1]).
57		:- use_module(extrasrc(bvisual2), [bv_get_top_level/1, bv_get_value_unlimited/3, bv_top_level_set/2]).
58		:- use_module(extrasrc(meta_interface),[command_description/3, command_category/2, command_unavailable/2,
59		call_command/5, call_dot_command/2]).
60		:- use_module(probsrc(tcltk_interface),[tcltk_forward/0, tcltk_fast_backtrack/0]).
61		:- use_module(visb_visualiser, [get_change_attribute_for_state/4, get_visb_attributes_for_state/2,
62		get_and_eval_special_definition/6, evaluate_visb_formula/6,
63		b_value_to_string/2, add_visb_lint_message/3,
64		no_svg_available/0, match_operation/2,
65		visb_file_loaded/4, visb_svg_file/5, visb_empty_svg_box_height_width/3,
66		visb_svg_object/5, visb_svg_child/2, visb_svg_parent/2,
67		visb_svg_child_of_object_from_svg_file/1,
68		visb_has_hovers/1, visb_hover/6]).
69
70		% Note: errors and warnings are still reported with source visb_visualiser
71
72		% --------------------------
73
74		% store templates as facts, so that compiled version of probcli does not need to find files
75		:- dynamic visb_template_file_codes/2.
76
77		assert_from_template(Filename) :- %formatsilent('Loading ~w~n',[Filename]),
78		absolute_file_name(visbsrc(Filename), Absolute, []),
79		read_string_from_file(Absolute,String),
80		assertz(visb_template_file_codes(Filename,String)).
81
82		:- assert_from_template('visb_template_header.html').
83		:- assert_from_template('visb_template_svg_downloads.html').
84		:- assert_from_template('visb_template_replayTrace.html').
85		:- assert_from_template('visb_template_middle.html').
86		:- assert_from_template('visb_template_footer.html').
87
88		write_visb_template(HtmlFile,Stream) :-
89		visb_template_file_codes(HtmlFile,Codes),
90		format(Stream,'~s~n',[Codes]).
91
92
93		% ----------------------------------
94
95		% generate a stand-alone HTML file with a visualisation for all states in the list
96
97		generate_visb_html(StateIds,File,Options) :-
98		safe_open_file(File,write,Stream,[encoding(utf8)]),
99		call_cleanup(generate_html_to_stream(StateIds,Stream,[html_file/File|Options]),
100		close(Stream)).
101
102		generate_visb_html_to_codes(StateIds,Options,Codes) :-
103		with_open_stream_to_codes(
104		generate_html_to_stream(StateIds,Stream,Options),
105		Stream,Codes,[]).
106
107
108		% generate an HTML file to visualise the given StateId
109		generate_html_to_stream(StateIds,Stream,Options) :-
110		set_id_namespace_prefix_for_states(StateIds,Options),
111		write_visb_template('visb_template_header.html',Stream),
112		(member(show_svg_downloads,Options) -> write_visb_template('visb_template_svg_downloads.html',Stream) ; true),
113		format(Stream,' <script>~n',[]),
114		retractall(js_generated_function(_)),
115		retractall(last_attribute_values(_,_,_)), % in case a previous export was aborted
116		length(StateIds,Len),
117		format(Stream,' const differences = [~n',[]),
118		maplist(gen_visb_visualise_function(Stream,Options,Len,StateIds),StateIds),
119		write_visb_template('visb_template_replayTrace.html',Stream),
120		format(Stream,' </script>~n~n',[]),
121		gen_registerHovers_script(Stream,Options),
122		write_visb_template('visb_template_middle.html',Stream),
123		(no_svg_available
124		-> format(Stream,' <button type="button" class="collapsible-style">No SVG Visualisation Available</button>~n',[])
125		; % generate SVG section
126		(member(no_header,Options) -> true
127		; format(Stream,' <button type="button" class="collapsible collapsible-style active">SVG Visualisation</button>~n',[])
128		),
129		format(Stream,' <div style="position: relative;">~n',[]), % container for SVG download buttons
130		format(Stream,' <div text-align="left" id="visb_svg_outer_container" class="svg-outer-container">~n',[]),
131		format(Stream,' <div id="visb_svg_inner_container" class="svg-inner-container">~n',[]),
132		%format(Stream,' <fieldset> <legend>Visualisation:</legend>~n',[]), % comment in to draw a border
133		(StateIds = [SingleState] -> get_state_and_action(SingleState,GenForState,_,_) % can be change_to_state_via_action/3
134		; GenForState=root),
135		copy_svg_file_and_gen_objects(Stream,GenForState,_SVGinlined),
136		% TO DO: avoid creating JS code below if _SVGinlined
137		%format(Stream,' </fieldset>~n',[]),
138		format(Stream,' </div>~n',[]), % inner container
139		format(Stream,' </div>~n',[]), % outer container
140		format(Stream,' <button id="btnResetScale" class="visualisation-button" onclick="resetScale()">Reset View</button>~n',[]),
141		(member(show_svg_downloads,Options) ->
142		format(Stream,' <button onclick="downloadSVG()">Save SVG (Current State)</button>~n',[]),
143		format(Stream,' <button onclick="downloadAllSVGs()">Save all SVGs</button>~n',[])
144		; true),
145		format(Stream,' </div>~n',[]) % container for SVG download buttons
146		),
147		(Len>1, memberchk(show_sequence_chart,Options) % don't export PlantUML for list of state IDs (sequence chart depends on trace)
148		-> (create_temp_puml_files(Len,Files),
149		uml_generator:write_uml_sequence_chart_all_states(Files), % generate .puml files
150		tools_commands:gen_plantuml_output(Files,svg,[]) % generate .svg files
151		-> format(Stream,' <button type="button" class="collapsible collapsible-style active">Sequence Chart Visualisation</button>~n',[]),
152		format(Stream,' <div class="seq-chart-container">~n',[]),
153		reverse(Files,RFiles),
154		write_temp_puml_outputs(1,RFiles,Stream), % write SVG contents to HTML
155		format(Stream,' </div>~n',[])
156		; add_warning(visb_visualiser,'HTML export: did not write the Sequence Diagram Visualisation due to an error in the PlantUML call.'),
157		format(Stream,' <button type="button" class="collapsible-style">No Sequence Chart Visualisation Available</button>~n',[])
158		)
159		; true),
160		(Len>1
161		-> generate_graph_table_visualisations(Len,Options,Stream),
162		%format(Stream,'~n<h3>Run Trace</h3>~n',[]),
163		format(Stream,' <button type="button" class="collapsible-style">Replay Trace</button>~n',[]),
164		format(Stream,' <div class="coll-content-vis">~n',[]),
165		format(Stream,' <button id="btnPrev" onclick="backStep()" title="Go back one step">« Back</button>~n',[]),
166		format(Stream,' <button id="btnNext" onclick="forwardStep()" title="Go forward one step">Forward »</button>~n',[]),
167		format(Stream,' <button onclick="runAll(10)" title="Fast replay of entire trace">Run Trace (10 ms delay)</button>~n',[]),
168		format(Stream,' <button onclick="runAll(500)" title="Slow replay of entire trace">Run Trace (500 ms delay)</button>~n',[]),
169		format(Stream,' <button onclick="runAll(parseInt(delayInput.value))" title="Custom replay of entire trace">Run Trace with Delay (ms):</button>~n',[]),
170		format(Stream,' <input id="delayInput" type="number" value="1000" min="0" step="100" onkeydown="if(event.key===\'Enter\') runAll(parseInt(this.value))">~n',[]),
171		format(Stream,' <label class="visb-messages" style="float:right">~n',[]),
172		format(Stream,' <input type="checkbox" id="checkbox_focus_svg"> Focus changes in SVG~n',[]),
173		format(Stream,' </label>~n',[]),
174		% We could decide to provide an option/preference for generating the visb_debug_messages field:
175		% (check that ProB2-UI also generates this text field)
176		format(Stream,' <br><label id="visb_debug_messages" class="visb-messages"> </label>~n',[]),
177		format(Stream,' </div>~n',[]),
178		format(Stream,' <progress id="trace_meter" min="0" max="~w" value="0"></progress>~n',[Len]) % progress of trace replay; note <meter> element also works
179		; true
180		),
181		% generate a table with variables, constants, ...
182		gen_state_table(Stream,Options,StateIds),
183		gen_source_code_section(Stream,Options),
184		% generate a table with the saved trace steps:
185		(Len>1 -> gen_trace_table(Stream,StateIds) ; true),
186		write_version_info(Stream,Options),
187		(last(StateIds,_)
188		-> format(Stream,' <script> replayStep(~w,false); </script>~n',[Len])
189		% show the visualisation of the last state by default (without focussing affected elements)
190		; true % trace is empty, there is no last item
191		),
192		write_visb_template('visb_template_footer.html',Stream),
193		clear_id_namespace_prefix.
194
195		create_temp_puml_files(Len,[]) :- Len<1, !.
196		create_temp_puml_files(Len,[Path|T]) :-
197		system_call:get_temporary_filename('for_html.puml',Path),
198		NewLen is Len-1,
199		create_temp_puml_files(NewLen,T).
200
201
202		write_temp_puml_outputs(_,[],_).
203		write_temp_puml_outputs(Nr,[File|T],Stream) :-
204		tools:split_filename(File,FileRoot,_Ext),
205		ajoin([FileRoot,'.svg'],SvgFile),
206		format(Stream,' <div id="seq_chart_~w" style="display:none">~n',[Nr]), % container for seq. charts
207		write_file_to_stream(SvgFile,Stream),
208		format(Stream,' </div>~n',[]), % container for seq. charts
209		delete_temp_file(File), delete_temp_file(SvgFile),
210		NNr is Nr+1,
211		write_temp_puml_outputs(NNr,T,Stream).
212
213		% -----------------
214		% GRAPHVIZ / TABLE SECTIONS
215
216		generate_graph_table_visualisations(Len,Options,Stream) :-
217		member(gen_graph_table(Cmd),Options),
218		command_category(Cmd,Cat), (Cat=dot ; Cat=table),
219		command_description(Cmd,CmdName,CmdDesc),
220		(\+ command_unavailable(Cmd,_) % TODO: only for current history, not for list of state ids
221		-> html_text_codes(CmdDesc,ECmdDesc), html_text_codes(CmdName,ECmdName),
222		format(Stream,' <button type="button" class="collapsible collapsible-style active" title="~s">~s</button>~n',[ECmdDesc,ECmdName]),
223		format(Stream,' <div class="coll-content-vis">~n',[]),
224		tcltk_fast_backtrack,
225		(tcltk_forward
226		-> (Cat=dot -> write_dot_graphs(Cmd,1,Len,Stream) ;
227		Cat=table -> write_table_vis(Cmd,1,Len,Stream))
228		; true),
229		format(Stream,' </div>~n',[])
230		; format(Stream,' <button type="button" class="collapsible-style">No ~w Available</button>~n',[CmdName])),
231		fail.
232		generate_graph_table_visualisations(_,_,_).
233
234		% write the graph for the current state Nr and then move forward until state Len of the history is reached
235		% (i.e., the state the animator was in before the export, also when there is a forward history)
236		write_dot_graphs(Cmd,Nr,Len,Stream) :-
237		write_dot_graph(Cmd,Nr,Stream),
238		NNr is Nr+1,
239		(Nr<Len, tcltk_forward -> write_dot_graphs(Cmd,NNr,Len,Stream) ; true).
240
241		write_dot_graph(Cmd,Nr,Stream) :-
242		\+ state_space:current_state_corresponds_to_initialised_b_machine, !,
243		format(Stream,' <div id="~w_~w" style="display:none">No Graph Visualisation Available</div>~n',[Cmd,Nr]).
244		write_dot_graph(Cmd,Nr,Stream) :-
245		system_call:get_temporary_filename('for_html.dot',DotFile),
246		system_call:get_temporary_filename('for_html.svg',File),
247		call_dot_command(Cmd,DotFile),
248		tools_commands:gen_dot_output(DotFile,dot,svg,File),
249		tools:split_filename(File,FileRoot,_Ext),
250		ajoin([FileRoot,'.svg'],SvgFile),
251		format(Stream,' <div id="~w_~w" style="display:none">~n',[Cmd,Nr]),
252		write_file_to_stream(SvgFile,Stream),
253		format(Stream,' </div>~n',[]),
254		delete_temp_file(DotFile), delete_temp_file(File), delete_temp_file(SvgFile).
255
256		delete_temp_file(File) :-
257		(file_exists(File)
258		-> catch(delete_file(File),E,add_debug_message(visb_visualiser,'Could not delete temporary file: ',E:File))
259		; true).
260
261		write_table_vis(Cmd,Nr,Len,Stream) :-
262		write_table_vis_for_state(Cmd,Nr,Stream),
263		NNr is Nr+1,
264		(Nr<Len, tcltk_forward -> write_table_vis(Cmd,NNr,Len,Stream) ; true).
265
266		write_table_vis_for_state(Cmd,Nr,Stream) :-
267		\+ state_space:current_state_corresponds_to_initialised_b_machine, !,
268		format(Stream,' <div id="~w_~w" style="display:none">No Table Available</div>~n',[Cmd,Nr]).
269		write_table_vis_for_state(Cmd,Nr,Stream) :-
270		call_command(table,Cmd,_,[TableResult],[]),
271		format(Stream,' <div id="~w_~w" style="display:none">~n',[Cmd,Nr]),
272		format(Stream,' <table>~n',[]),
273		TableResult = list([list(Keys)|Elements]),
274		% Keys:
275		format(Stream,' <tr>',[]),
276		write_html_table_elements(th,Keys,Stream),
277		format(Stream,' </tr>',[]),
278		% Elements:
279		write_html_table(Elements,Stream),
280		format(Stream,' </table>~n',[]),
281		format(Stream,' </div>~n',[]).
282
283		write_html_table([],_).
284		write_html_table([list(Elements)|T],Stream) :-
285		format(Stream,' <tr>',[]),
286		write_html_table_elements(td,Elements,Stream),
287		format(Stream,' </tr>',[]),
288		write_html_table(T,Stream).
289
290		write_html_table_elements(_,[],_).
291		write_html_table_elements(Tag,[Element|T],Stream) :-
292		format(Stream,' <~w>',[Tag]), format_html_text(Stream,Element), format(Stream,'</~w>~n',[Tag]),
293		write_html_table_elements(Tag,T,Stream).
294
295		% -----------------
296
297		write_version_info(_,Options) :-
298		member(no_version_info,Options),!.
299		write_version_info(Stream,Options) :-
300		version_str(Str),datime(datime(Yr,Mon,Day,Hr,Min,_Sec)),
301		number_codes_min_length(Min,2,MC),
302		format(Stream,' <button type="button" class="collapsible-style" title="Information about ProB and model">Info</button>~n',[]),
303		format(Stream,'<div class="coll-content-vis visb-messages">~n',[]),
304		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]),
305		(currently_opened_file(File)
306		-> (File=package(Type) ->
307		format(Stream,'<br>Main specification package: ',[]), format_html_text(Stream,Type), nl(Stream)
308		; atom(File), get_relative_path(File,Options,Suffix) ->
309		format(Stream,'<br>Main specification file: ',[]), format_html_text(Stream,Suffix),
310		format_file_info(Stream,File)
311		; format(Stream,'<br>Unknown main specification file: ',[]), format_html_text(Stream,File), nl(Stream)
312		)
313		; true),
314		(b_machine_name(MainName)
315		-> format(Stream,'<br>Main specification name: ',[]), format_html_text(Stream,MainName), nl(Stream)
316		; true),
317		(visb_file_loaded(JSONFile,_,ModLocTime,_),
318		JSONFile \= ''
319		-> get_relative_path(JSONFile,Options,JSuffix),
320		format(Stream,'<br>Main VisB JSON file: ',[]), format_html_text(Stream,JSuffix),
321		format_modified_info(Stream,ModLocTime),
322		(get_non_empty_svg_file(SVGFile,ModLocTime2)
323		-> get_relative_path(SVGFile,Options,SSuffix),
324		format(Stream,'<br>VisB SVG file: ',[]), format_html_text(Stream,SSuffix),
325		format_modified_info(Stream,ModLocTime2)
326		; true
327		)
328		; true).
329
330		get_non_empty_svg_file(SVGFile,ModLocTime2) :-
331		visb_svg_file(RelFile,SVGFile,_,_,ModLocTime2),
332		RelFile \= ''.
333
334		format_file_info(Stream,File) :-
335		catch(file_property(File, modify_localtime, ModLocTime),
336		E,
337		(add_visb_lint_message('Could not obtain modification time for file',E,unknown), fail)),
338		!,
339		format_modified_info(Stream,ModLocTime).
340		format_file_info(Stream,_) :- nl(Stream).
341
342
343		get_relative_path(File,Options,RelPath) :-
344		member(html_file/HF,Options),
345		absolute_file_name(File,AF,[]),
346		absolute_file_name(HF,AHF,[]),
347		!,
348		gen_relative_path(AF,AHF,RelPath). % only print relative information
349		get_relative_path(File,_,File).
350
351
352		% -----------------
353
354		% gen a table with all the individual steps of the trace
355		gen_trace_table(Stream,StateIds) :-
356		length(StateIds,Len),
357		%format(Stream,'~n<h3>Trace (length=~w)</h3>~n',[Len]),
358		format(Stream,' <button type="button" class="collapsible collapsible-style active">Trace (length=~w)</button>~n',[Len]),
359		format(Stream,'<div class="coll-content-vis">~n',[]),
360		(member(Obj,StateIds), get_state_and_action(Obj,_,_,DescStr), DescStr \= ''
361		-> Opt=with_description ; Opt=no_description),
362		gen_trace_table2(Stream,StateIds,Opt).
363
364		gen_trace_table2(Stream,StateIds,no_description) :-
365		format(Stream,' <table> <tr> <th>Nr</th> <th>Event</th> <th>Target State ID</th> </tr>~n',[]),
366		nth1(Nr,StateIds,Obj),
367		get_state_and_action(Obj,StateId,ActionStr,_),
368		atom_codes(ActionStr,ActionCodes),html_escape_codes(ActionCodes,EAS),
369		((visited_state_corresponds_to_initialised_b_machine(StateId) ; xtl_mode) % allow onclick to all rows in xtl_mode
370		-> (invariant_violated(StateId) -> BtnStyle='style="background-color:rgb(255,179,179);border-radius:6px" ' ; BtnStyle=''),
371		format(Stream,'~n <tr id="row~w" onclick="replayStep(~w)"><td>~w</td><td style="cursor:pointer">~s</td><td><button ~wonclick="replayStep(~w);">State ~w</button></td></tr>~n',
372		[Nr,Nr,Nr,EAS,BtnStyle,Nr,StateId])
373		; format(Stream,'~n <tr id="row~w"><td>~w</td><td style="cursor:not-allowed">~s</td><td>State ~w</td></tr>~n',
374		[Nr,Nr,EAS,StateId])
375		),
376		fail.
377		gen_trace_table2(Stream,StateIds,with_description) :-
378		format(Stream,' <table> <tr> <th>Nr</th> <th>Event</th> <th>Description</th> <th>Target State ID</th> </tr>~n',[]),
379		nth1(Nr,StateIds,Obj),
380		get_state_and_action(Obj,StateId,ActionStr,DescStr),
381		atom_codes(ActionStr,ActionCodes),html_escape_codes(ActionCodes,EAS),
382		atom_codes(DescStr,DescCodes),html_escape_codes(DescCodes,EDS),
383		((visited_state_corresponds_to_initialised_b_machine(StateId) ; xtl_mode) % allow onclick to all rows in xtl_mode
384		-> (invariant_violated(StateId) -> BtnStyle='style="background-color:rgb(255,179,179);border-radius:6px" ' ; BtnStyle=''),
385		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',
386		[Nr,Nr,Nr,EAS,EDS,BtnStyle, Nr,StateId])
387		; 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',
388		[Nr,Nr,EAS,EDS,StateId])
389		),
390		fail.
391		gen_trace_table2(Stream,_,_) :-
392		format(Stream,' </table>~n </div>~n',[]).
393
394
395		% utility to allow passing information about name of event/operation/action leading to state
396		get_state_and_action(change_to_state_via_action(StateId,ActionStr,DescStr),StateId,ActionStr,DescStr) :- !.
397		get_state_and_action(StateId,StateId,'','').
398
399		% -----------------
400
401		% inline provided svg file into html file:
402		% second argument is either root or a particular state id for which the SVG file is to be created
403		% the last argument is static_svg_inlined if all SVG objects were "inlined" into a single
404		% SVG object (rather than via JavaScript functions to create the objects)
405		copy_svg_file_and_gen_objects(Stream,_,static_svg_not_inlined) :- visb_svg_file(_,File,_,_,_), file_exists(File),
406		!,
407		write_file_to_stream(File,Stream),
408		( get_visb_contents_def(Contents,DefName,DefPos,static_svg_not_inlined),
409		(DefName = default_svg_contents -> true % no need to inform user about our own default contents
410		; ajoin(['Copying ',DefName,' *after* SVG file: '],Msg),
411		add_message(visb_visualiser,Msg,File,DefPos)),
412		format(Stream,'~w~n',[Contents]),
413		fail
414		; true
415		),
416		gen_new_svg_objects(Stream).
417		copy_svg_file_and_gen_objects(_,_,_) :-
418		visb_svg_file(File,AFile,_,Pos,_),
419		File \= '',
420		add_error(visb_visualiser,'The specified VisB SVG file does not exist:',AFile,Pos),
421		fail.
422		copy_svg_file_and_gen_objects(Stream,SingleStateId,static_svg_inlined) :- % copy an empty SVG stub
423		visb_file_loaded(_,_,_,_),!,
424		write_default_svg_contents(Stream,inline_objects(SingleStateId)).
425		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,...
426
427		% TODO: precompile and always assert as visb_special_definition (we could also evaluate it; could use template strings):
428		get_visb_contents_def(Contents,DefName,DefPos,InlineObjects) :-
429		get_and_eval_special_definition('VISB_SVG_CONTENTS',DefName,visb_contents,DefPos,ResValue,InlineObjects),
430		b_value_to_string(ResValue,Contents).
431		get_visb_contents_def(Contents,default_svg_contents,unknown,_InlineObjects) :-
432		% default content, for VISB_CLICK_META_INFOS'jsVars
433		Contents = '<script>let visb_vars = {};</script>'.
434
435		write_default_svg_contents(Stream,InlineObjects) :-
436		(visb_empty_svg_box_height_width(H,W,ViewBox) -> true ; H=400, W=400, ViewBox=''),
437		format(Stream,'<svg xmlns=\"http://www.w3.org/2000/svg\"~n',[]),
438		(ViewBox=''
439		-> format(Stream,' width="~w" height="~w" viewBox="0 0 ~w ~w" >~n',[W,H,W,H])
440		; format(Stream,' width="~w" height="~w" viewBox="~w" >~n',[W,H,ViewBox])
441		),
442		( get_visb_contents_def(Contents,_,_,InlineObjects),
443		format(Stream,'~w~n',[Contents]),
444		fail
445		; true),
446		(InlineObjects=inline_objects(StateID) -> inline_new_svg_objects(Stream,StateID) ; true),
447		format(Stream,'</svg>~n',[]).
448
449		% get SVG file contents in case no SVG file is provided by user
450		get_visb_default_svg_file_contents(Codes) :-
451		with_open_stream_to_codes(
452		write_default_svg_contents(Stream,inline_objects(root)),
453		% allow inlining for groups and title children in ProB2-UI
454		Stream,
455		Codes, []).
456
457		% -----------------
458
459		% create a script to add all additional SVG objects
460		gen_new_svg_objects(_) :- \+ visb_svg_object(_,_,_,_,_),!.
461		gen_new_svg_objects(Stream) :-
462		format(Stream, '<script>~n{ // block scope: the footer script also declares a global const svg~n',[]),
463		format(Stream, ' const svg = document.querySelector("svg");~n',[]),
464		format(Stream, ' const svgns = "http://www.w3.org/2000/svg";~n',[]),
465		(gen_new_svg_object(Stream,svg_root,_),fail ; true),
466		format(Stream, '}~n</script>~n',[]).
467
468		% generate JS script to create an individual new object
469		gen_new_svg_object(Stream,ParentID,SVGID) :-
470		visb_svg_object(SVGID,SVG_Class,AttrList,_,_Pos),
471		(ParentID=svg_root
472		-> (visb_svg_child(SVGID,RealParentID) % only generate root svg objects that have no parents
473		-> visb_svg_child_of_object_from_svg_file(SVGID) % unless the parent will not be created here in this loop
474		; RealParentID=ParentID
475		)
476		; RealParentID=ParentID),
477		add_svg_id_prefix(SVGID,SVGID2),
478		format(Stream,' if(document.getElementById("',[]), format_js_string(Stream,SVGID2),
479		format(Stream,'") == null) {~n',[]),
480		format(Stream,' var new___obj = document.createElementNS(svgns,"',[]), format_js_string(Stream,SVG_Class),
481		format(Stream,'");~n',[]),
482		gen_new_svg_attr(Stream,SVGID2,svg_attribute(id,SVGID2)),
483		maplist(gen_new_svg_attr(Stream,SVGID2),AttrList),
484		(RealParentID \= svg_root
485		-> opt_add_svg_id_prefix(RealParentID,RealParentID2), % parent may come from SVG file and have no prefix
486		format(Stream,' document.getElementById("',[]), format_js_string(Stream,RealParentID2),
487		format(Stream,'").appendChild(new___obj);~n',[])
488		; format(Stream,' svg.appendChild(new___obj);~n',[])
489		),
490		format(Stream,' }~n',[]),
491		(visb_svg_parent(SVGID,ChildID), % we can now generate the children
492		gen_new_svg_object(Stream,SVGID,ChildID),
493		fail
494		; true).
495
496		gen_new_svg_attr(Stream,_SVGID,svg_attribute(text,Val)) :- !,
497		format(Stream,' new___obj.textContent = "',[]), format_js_string(Stream,Val),
498		format(Stream,'";~n',[]).
499		gen_new_svg_attr(Stream,_SVGID,svg_attribute(Attr,Val)) :-
500		format(Stream,' new___obj.setAttribute("',[]), format_js_string(Stream,Attr),
501		format(Stream,'","',[]), format_js_string(Stream,Val),
502		format(Stream,'");~n',[]).
503
504		% instead of creating a script to create new SVG objects,
505		% create an inlined textual XML representation of the objects
506		% this can be used to obtain a static SVG file which can be modified in an editor
507		% and then later used instead of the VISB_SVG_OBJECTS definitions
508		inline_new_svg_objects(Stream,StateId) :-
509		get_dynamic_svgid_attributes_for_state(StateId,DynUpdateList), % compute updates only once
510		visb_svg_object(SVGID,_,_,_,_), % lookup static SVG object
511		\+ visb_svg_child(SVGID,_), % children will be created in the scope of their parent
512		inline_new_svg_object(Stream,StateId,DynUpdateList,0,unknown,SVGID),
513		fail.
514		inline_new_svg_objects(_,_).
515
516		inline_new_svg_object(Stream,StateId,DynUpdateList,IndentLevel,ParentPos,SVGID) :-
517		(visb_svg_object(SVGID,SVG_Class,StaticAttrList,_,Pos) -> true % lookup static SVG object
518		; add_warning(visb_visualiser,'Unknown SVG child object: ',SVGID,ParentPos),fail
519		),
520		add_svg_id_prefix(SVGID,SVGID2), % for Jupyter
521		indent_ws(Stream,IndentLevel),
522		atom_codes(SVGID2,IDCodes), xml_escape_codes(IDCodes,EIDCodes),
523		format(Stream,' <~w id="~s"',[SVG_Class,EIDCodes]),
524		(member(svgid_updates(SVGID,DynAttrList),DynUpdateList) % TODO: use avl_fetch
525		-> override_attributes(StaticAttrList,DynAttrList,AttrList)
526		; AttrList=StaticAttrList),
527		maplist(format_new_svg_attr(Stream,SVGID,Pos,TextContent),AttrList),
528		(TextContent=''
529		-> EscapedTextContent="" % set Text variable to empty if unbound
530		; do_not_escape_text_for_class(SVG_Class) -> atom_codes(TextContent,EscapedTextContent)
531		; atom_codes(TextContent,TCC), xml_escape_codes(TCC,EscapedTextContent)),
532		format(Stream,'>~s',[EscapedTextContent]), % Note: this text is not inside quotes, we need HTML escape
533		IL1 is IndentLevel+1,
534		( visb_svg_parent(SVGID,Child),
535		nl(Stream),
536		inline_new_svg_object(Stream,StateId,DynUpdateList,IL1,Pos,Child),
537		fail
538		; true),
539		format(Stream,'</~w>~n',[SVG_Class]), % end marker
540		fail.
541		inline_new_svg_object(_,_,_,_,_,_).
542
543		% for foreignObjects the text may contain HTML tags which should not be escaped:
544		do_not_escape_text_for_class(foreignObject).
545		do_not_escape_text_for_class(script). % otherwise " quotes will be escaped to "
546
547		indent_ws(_,X) :- X<1,!.
548		indent_ws(Stream,X) :- write(Stream,' '), X1 is X-1, indent_ws(Stream,X1).
549
550		% combinde svg_attribute/2 terms from two sorted lists, giving precedence to second list
551		override_attributes([],L,R) :- !, R=L.
552		override_attributes(L,[],R) :- !, R=L.
553		override_attributes([svg_attribute(Attr1,Val1)|T1],[svg_attribute(Attr2,Val2)|T2],[svg_attribute(Attr3,Val3)|T3]) :-
554		(Attr1=Attr2
555		-> Attr3=Attr1, Val3=Val2, % dynamic value Val2 takes precedence
556		override_attributes(T1,T2,T3)
557		; Attr1 @< Attr2 -> Attr3=Attr1, Val3=Val1, override_attributes(T1,[svg_attribute(Attr2,Val2)|T2],T3)
558		; Attr3=Attr2, Val3=Val2, override_attributes([svg_attribute(Attr1,Val1)|T1],T2,T3)
559		).
560
561		% get dynamic svg_attribute/2 list for a given state and SVG ID
562		get_dynamic_svgid_attributes_for_state(root,List) :- !, List=[].
563		get_dynamic_svgid_attributes_for_state(StateId,UpdateList) :-
564		get_visb_attributes_for_state(StateId,List),
565		sort(List,SList),
566		group_set_attr(SList,'$$UNKNOWN$$',_,UpdateList).
567
568		group_set_attr([],_,[],[]).
569		group_set_attr([set_attr(SvgID,Attr,Val)|T],SvgID,[svg_attribute(Attr,Val)|T1],T2) :- !,
570		group_set_attr(T,SvgID,T1,T2).
571		group_set_attr([set_attr(SvgID,Attr,Val)|T],_OldID,[],[svgid_updates(SvgID,L)|T2]) :- % a new SVGId is encountered
572		group_set_attr([set_attr(SvgID,Attr,Val)|T],SvgID,L,T2).
573
574		% print svg attribute and extract text attribute
575		format_new_svg_attr(Stream,SVGID,Pos,TextContent,svg_attribute(Attr,Val)) :- % TODO: text content
576		(Attr=text
577		-> (TextContent=Val -> true % TextContent is initially a variable and can be unified once
578		; add_warning(inline_new_svg_objects,'Multiple text attributes for: ',SVGID,Pos),
579		add_debug_message(inline_new_svg_objects,' * Using text 1: ',TextContent),
580		add_debug_message(inline_new_svg_objects,' * Ignoring text 2: ',Val)
581		)
582		; number(Val) ->
583		format(Stream,' ~w="~w"',[Attr,Val])
584		; atom(Val) ->
585		atom_codes(Val,Codes), xml_escape_codes(Codes,ECodes), % we are inside an XML attribute, not JavaScript
586		format(Stream,' ~w="~s"',[Attr,ECodes])
587		; compound(Val), functor(Val,F,N) ->
588		ajoin(['Cannot escape ',Attr,' *compound* ',F,'/',N,' value for ', SVGID,': '],Msg),
589		add_error(visb_visualiser,Msg,Val,Pos),
590		format(Stream,' ~w="~w"',[Attr,Val])
591		; ajoin(['Cannot escape ',Attr,' value for ', SVGID,': '],Msg),
592		add_error(visb_visualiser,Msg,Val,Pos),
593		format(Stream,' ~w="~w"',[Attr,Val])
594		).
595
596
597		:- dynamic id_namespace_prefix/1.
598		% prefix that can be useful for Jupyter notebooks so that for each state we have a different namespace
599		% can also be useful for exporting a trace into a single HTML
600		% TODO: does not work with JSON and SVG files
601
602
603		set_id_namespace_prefix_for_states(_,Options) :-
604		member(id_namespace_prefix(Pre),Options),!,
605		(Pre = auto
606		-> gensym('visb',ID), % for Jupyter this relies on the fact the gensym is *not* reset when loading another spec
607		atom_concat(ID,'.',Prefix)
608		; Prefix=Pre
609		), set_id_namespace_prefix(Prefix).
610		set_id_namespace_prefix_for_states(_,_).
611
612		set_id_namespace_prefix(Prefix) :- clear_id_namespace_prefix,
613		assert(id_namespace_prefix(Prefix)).
614		clear_id_namespace_prefix :- retractall(id_namespace_prefix(_)).
615
616		% add a namespace prefix to an SVG ID
617		add_svg_id_prefix(SvgID,Res) :- id_namespace_prefix(Prefix),!,
618		% option where we prefix all Ids with a namespace for Jupyter to combine multiple SVGs in single HTML page
619		atom_concat(Prefix,SvgID,Res).
620		add_svg_id_prefix(SvgID,SvgID).
621
622		% only add for known objects
623		opt_add_svg_id_prefix(SvgID,Res) :- id_namespace_prefix(Prefix),
624		visb_svg_object(SvgID,_,_,_,_),!, % only add prefix for SVG objects we know about (that were created by VisB)
625		% option where we prefix all Ids with a namespace for Jupyter to combine multiple SVGs in single HTML page
626		atom_concat(Prefix,SvgID,Res).
627		opt_add_svg_id_prefix(SvgID,SvgID).
628
629		% -----------------
630
631		:- dynamic js_generated_function/1.
632		:- dynamic last_attribute_values/3.
633
634		% define a visualise JS function to set the attributes for the given StateId
635		gen_visb_visualise_function(Stream,Options,Len,StateIds,Obj) :-
636		get_state_and_action(Obj,StateId,ActionStr,DescStr),
637		nth1(Nr,StateIds,Obj),
638		\+ js_generated_function(Nr), !,
639		assertz(js_generated_function(Nr)),
640		(Nr > 1 ->
641		PrevNr is Nr-1, nth1(PrevNr,StateIds,PrevObj), get_state_and_action(PrevObj,PrevStateId,_,_)
642		; PrevStateId = -1),
643		visb_visualise_function_aux(Stream,Options,Len,StateId,PrevStateId,Nr,ActionStr,DescStr),
644		(Nr == Len ->
645		retractall(last_attribute_values(_,_,_)),
646		format(Stream,' ]~n',[])
647		; true).
648		gen_visb_visualise_function(_,_,_,_,_).
649
650
651		visb_visualise_function_aux(Stream,_,Len,StateId,_,Nr,ActionStr,DescStr) :-
652		format(Stream,' [~n',[]),
653		(Len>1 -> format(Stream,' {id: "trace_meter", attr: "value", val: "~w"},~n',[Nr]) ; true),
654		(escape_value_to_codes_for_js(ActionStr,EAS), escape_value_to_codes_for_js(DescStr,EDS) ->
655		% was only string_escape before; however, this turns e.g. |-> into ↦ which we don't want (we are in JS part here)
656		format(Stream,' {id: "visb_debug_messages", attr: "text", val: "Step ~w/~w, State ID: ~w, Event: ~s ~s"},~n',[Nr,Len,StateId,EAS,EDS])
657		; string_escape(ActionStr,SEAS), string_escape(DescStr,SEDS), % fallback
658		format(Stream,' {id: "visb_debug_messages", attr: "text", val: "Step ~w/~w, State ID: ~w, Event: ~w ~w"},~n',[Nr,Len,StateId,SEAS,SEDS])
659		),
660		get_change_attribute_for_state(StateId,SvgID,SvgAttribute,Value),
661		\+ last_attribute_values(SvgID,SvgAttribute,Value),
662		retractall(last_attribute_values(SvgID,SvgAttribute,_)),
663		assertz(last_attribute_values(SvgID,SvgAttribute,Value)),
664		opt_add_svg_id_prefix(SvgID,SvgID2),
665		(escape_value_to_codes_for_js(Value,ECodes)
666		-> format(Stream,' {id: "~w", attr: "~w", val: "~s"},~n',[SvgID2,SvgAttribute,ECodes])
667		; format(Stream,' {id: "~w", attr: "~w", val: "',[SvgID2,SvgAttribute]),
668		format_js_string(Stream,Value), format(Stream,'"},~n',[])
669		),
670		fail.
671		visb_visualise_function_aux(Stream,Options,Len,StateId,PrevStateId,_,_,_) :-
672		b_or_z_mode,
673		member(show_variables(VarList),Options),
674
675		visited_expression(StateId,State),
676		(visited_expression(PrevStateId,PrevState) -> true ; PrevState=root),
677
678		show_var_in_visb(VarList,ID),
679		get_state_value_change(StateId,State,ID,Options,ResValCodes),
680
681		% current value:
682		ajoin(['bVar_',ID],SvgID),
683		change_svg_attribute_differences_aux(Stream,SvgID,'text',ResValCodes),
684
685		Len > 1, % don't add previous value and change markers for state-only HTML
686		(state_corresponds_to_fully_setup_b_machine(PrevState,_), % don't show prev values before initialisation
687		get_state_value_change(PrevStateId,PrevState,ID,Options,PrevResValCodes)
688		-> true
689		; PrevResValCodes = "?"),
690
691		% mark row if value has changed in the last step
692		ajoin(['row_bVar_',ID],SvgRowID),
693		(ResValCodes = PrevResValCodes -> RowColor = white; RowColor = '#fffacd'),
694		change_svg_attribute_differences_aux(Stream,SvgRowID,'bgcolor',RowColor),
695
696		% previous value:
697		ajoin(['bVarPrev_',ID],SvgPrevID),
698		change_svg_attribute_differences_aux(Stream,SvgPrevID,'text',PrevResValCodes),
699
700		fail.
701		visb_visualise_function_aux(Stream,_Options,Len,StateId,PrevStateId,_,_,_) :-
702		xtl_mode,
703
704		bv_get_top_level(IDs),
705		member(ID,IDs),
706		(bv_get_value_unlimited(ID,StateId,v(Val))
707		-> atom_codes(Val,ValCodes), js_escape_codes(ValCodes,ResValCodes)
708		; ResValCodes = ""),
709
710		% current value:
711		ajoin(['bVar_',ID],SvgID),
712		change_svg_attribute_differences_aux(Stream,SvgID,'text',ResValCodes),
713
714		Len > 1, % don't add previous value and change markers for state-only HTML
715		(PrevStateId \= root,
716		bv_get_value_unlimited(ID,PrevStateId,v(PrevVal))
717		-> atom_codes(PrevVal,PrevValCodes), js_escape_codes(PrevValCodes,PrevResValCodes)
718		; PrevResValCodes = ""),
719
720		% mark row if value has changed in the last step
721		ajoin(['row_bVar_',ID],SvgRowID),
722		(ResValCodes = PrevResValCodes -> RowColor = white; RowColor = '#fffacd'),
723		change_svg_attribute_differences_aux(Stream,SvgRowID,'bgcolor',RowColor),
724
725		% previous value:
726		ajoin(['bVarPrev_',ID],SvgPrevID),
727		change_svg_attribute_differences_aux(Stream,SvgPrevID,'text',PrevResValCodes),
728
729		fail.
730		visb_visualise_function_aux(Stream,Options,_,StateId,_,_,_,_) :-
731		member(show_events(OpList),Options),
732		get_state_value_enabled_operation_status(StateId,OpID,Enabled,ResValCodes,TransStr),
733		show_var_in_visb(OpList,OpID),
734		ajoin(['bOperation_',OpID],SvgID),
735		change_svg_attribute_differences_aux(Stream,SvgID,'text',ResValCodes),
736		(Enabled=true -> BGCol=white ; BGCol='#f1f1f1'),
737		ajoin(['row_',SvgID],SvgRowID),
738		change_svg_attribute_differences_aux(Stream,SvgRowID,'bgcolor',BGCol),
739		% the transition string (with parameters) can change even if the status text remains the same:
740		escape_value_to_codes_for_js(TransStr,ETS),
741		ajoin(['name_',SvgID],SvgNameID),
742		change_svg_attribute_differences_aux(Stream,SvgNameID,'text',ETS),
743		% TO DO: highlight next event in trace, but then function needs one more parameter
744		fail.
745		visb_visualise_function_aux(Stream,Options,Len,_,_,Nr,_,_) :-
746		(Len>1, member(show_sequence_chart,Options)
747		-> format(Stream,' {id: "seq_chart_~w", attr: "style", val: "display:block"},~n',[Nr]),
748		(Nr>1
749		-> PNr is Nr-1, format(Stream,' {id: "seq_chart_~w", attr: "style", val: "display:none"},~n',[PNr])
750		; gen_graph_setup(Stream,seq_chart,Len))), % all sequence charts except the first should be invisible
751		fail.
752		visb_visualise_function_aux(Stream,Options,Len,_,_,Nr,_,_) :-
753		member(gen_graph_table(Cmd),Options),
754		(Len>1
755		-> format(Stream,' {id: "~w_~w", attr: "style", val: "display:block"},~n',[Cmd,Nr]),
756		(Nr>1
757		-> PNr is Nr-1, format(Stream,' {id: "~w_~w", attr: "style", val: "display:none"},~n',[Cmd,PNr])
758		; gen_graph_setup(Stream,Cmd,Len))),
759		fail.
760		visb_visualise_function_aux(Stream,_,Len,_,_,Nr,_,_) :-
761		Nr == Len ->
762		format(Stream,' ]~n',[])
763		; format(Stream,' ],~n',[]).
764
765		gen_graph_setup(_,_,Len) :- Len<2, !.
766		gen_graph_setup(Stream,Cmd,Len) :-
767		format(Stream,' {id: "~w_~w", attr: "style", val: "display:none"},~n',[Cmd,Len]),
768		NLen is Len-1,
769		gen_graph_setup(Stream,Cmd,NLen).
770
771		escape_value_to_codes_for_js(Atom,ECodes) :- atom(Atom),
772		atom_codes(Atom,Codes), js_escape_codes(Codes,ECodes).
773
774		% escape codes for use inside a "..." JavaScript string literal within an HTML <script> element;
775		% < is escaped as \u003c so that a value cannot end the script with </script> or start a comment <!--
776		js_escape_codes(Codes,ECodes) :-
777		b_string_escape_codes(Codes,Codes2), escape_lt_for_js(Codes2,ECodes).
778		escape_lt_for_js([],[]).
779		escape_lt_for_js([0'<|T],[0'\\,0'u,0'0,0'0,0'3,0'c|ET]) :- !, escape_lt_for_js(T,ET).
780		escape_lt_for_js([H|T],[H|ET]) :- escape_lt_for_js(T,ET).
781
782		% write any value as escaped contents of a "..." JavaScript string literal
783		format_js_string(Stream,Val) :- number(Val),!, write(Stream,Val).
784		format_js_string(Stream,Val) :-
785		(atom(Val) -> atom_codes(Val,Codes) ; write_to_codes(Val,Codes)),
786		js_escape_codes(Codes,ECodes),
787		format(Stream,'~s',[ECodes]).
788
789		% escape codes for use inside a "..." XML/HTML attribute value or as XML text;
790		% unlike html_escape_codes we do not generate HTML entities like ä which are not valid in SVG files
791		xml_escape_codes([],[]).
792		xml_escape_codes([C|T],Res) :-
793		(xml_escape_code(C,EC) -> append(EC,ET,Res) ; Res=[C|ET]),
794		xml_escape_codes(T,ET).
795		xml_escape_code(0'&,"&").
796		xml_escape_code(0'<,"<").
797		xml_escape_code(0'>,">").
798		xml_escape_code(0'",""").
799
800		% write any value as escaped HTML text
801		format_html_text(Stream,Val) :-
802		html_text_codes(Val,ECodes),
803		format(Stream,'~s',[ECodes]).
804
805		html_text_codes(Val,ECodes) :-
806		(atom(Val) -> atom_codes(Val,Codes) ; write_to_codes(Val,Codes)),
807		html_escape_codes(Codes,ECodes).
808
809		change_svg_attribute_differences_aux(Stream,ID,Attr,ValueCodes) :-
810		(last_attribute_values(ID,Attr,ValueCodes)
811		-> true
812		; retractall(last_attribute_values(ID,Attr,_)),
813		assertz(last_attribute_values(ID,Attr,ValueCodes)),
814		format(Stream,' {id: "~w", attr: "~w", val: "~s"},~n',[ID,Attr,ValueCodes])
815		).
816
817
818		% generate JS script to register hovers
819		gen_registerHovers_script(Stream,Options) :- \+ visb_has_hovers(_),
820		nonmember(debugging_hovers,Options),
821		!, % no hover exists
822		format(Stream,' <script> function registerHovers() {} </script>~n',[]).
823		gen_registerHovers_script(Stream,Options) :-
824		(member(debugging_hovers,Options) -> GenDebug=true ; GenDebug=false), % gen debugging hovers
825		% Jquery is no longer required:
826		%format(Stream,' <script src="https://ajax.googleapis.com/ajax/libs/jquery/3.6.0/jquery.min.js"></script>~n',[]),
827		format(Stream,' <script>~n',[]),
828		format(Stream,' function registerHovers() {~n',[]),
829		format(Stream,' var obj;~n',[]),
830		visb_has_hovers(SVGID), % only generate hover function if necessary; TODO: examine other IDs for GenDebug
831		opt_add_svg_id_prefix(SVGID,SVGID2),
832		format(Stream,' obj = document.getElementById("',[]), format_js_string(Stream,SVGID2),
833		format(Stream,'");~n',[]),
834		format(Stream,' if (obj != null) {~n',[]), % do not abort registerHovers if the SVG object does not exist
835		format(Stream,' obj.onmouseover = function(ev){~n',[]),
836		(visb_hover(SVGID,ID,Attr,EnterVal,_,_),
837		opt_add_svg_id_prefix(ID,ID2),
838		(GenDebug=false -> true
839		; ajoin(['SVG ID: ',SVGID2],DebugMsg),
840		gen_js_set_attr(Stream,visb_debug_messages,text,DebugMsg)),
841		gen_js_set_attr(Stream,ID2,Attr,EnterVal), fail ;
842		format(Stream,' };~n',[])
843		),
844		format(Stream,' obj.onmouseout = function(){~n',[]),
845		(visb_hover(SVGID,ID,Attr,_,LeaveVal,_),
846		opt_add_svg_id_prefix(ID,ID2),
847		(GenDebug=false -> true
848		; gen_js_set_attr(Stream,visb_debug_messages,text,'...')
849		),
850		gen_js_set_attr(Stream,ID2,Attr,LeaveVal), fail ;
851		format(Stream,' };~n',[])
852		),
853		format(Stream,' }~n',[]),
854		fail.
855		gen_registerHovers_script(Stream,_) :-
856		format(Stream,' }~n </script>~n',[]).
857
858		gen_js_set_attr(Stream,ID,Attr,Val) :-
859		format(Stream,' setAttr("',[]), format_js_string(Stream,ID),
860		format(Stream,'","',[]), format_js_string(Stream,Attr),
861		format(Stream,'","',[]), format_js_string(Stream,Val),
862		format(Stream,'")~n',[]).
863
864
865		% ----------------------------------
866
867
868		generate_visb_html_for_history_with_source(File) :-
869		generate_visb_html_for_history(File,
870		[show_constants(all),show_sets(all),show_variables(all),show_events(all),show_invariants,show_source]).
871		generate_visb_html_for_history_with_vars(File) :-
872		generate_visb_html_for_history(File,[show_constants(all),show_sets(all),show_variables(all),show_events(all)]).
873		generate_visb_html_for_history(File) :-
874		generate_visb_html_for_history(File,[]).
875		generate_visb_html_for_history(File,Options) :-
876		start_ms_timer(Timer),
877		get_state_id_trace(T),
878		T = [root|StateIds],
879		set_unicode_mode,
880		call_cleanup(get_action_trace_with_limit(120,Actions), % TODO: also get description of JSON traces
881		unset_unicode_mode),
882		reverse(Actions,FActions),
883		combine_state_and_actions(StateIds,[root|StateIds],FActions,List),
884		generate_visb_html(List,File,Options),
885		stop_ms_walltimer_with_msg(Timer,'exporting history to VisB HTML file: ').
886
887
888		combine_state_and_actions([],_,[],[]).
889		combine_state_and_actions([StateId|TS],[PrevId|TP],[action(ActionStr,ATerm)|TA],
890		[change_to_state_via_action(StateId,ActionStr,Desc)|TRes]) :-
891		(get_operation_description_for_transition(PrevId,ATerm,StateId,D) -> Desc=D ; Desc=''),
892		combine_state_and_actions(TS,TP,TA,TRes).
893
894		generate_visb_html_for_current_state(File) :-
895		generate_visb_html_for_current_state(File,[show_variables(all)]).
896		generate_visb_html_for_current_state(File,Options) :-
897		start_ms_timer(Timer),
898		current_state_id(ID),
899		generate_visb_html([ID],File,Options),
900		stop_ms_walltimer_with_msg(Timer,'exporting current state to VisB HTML file: ').
901		generate_visb_html_codes_for_states(StateIds,Options,Codes) :-
902		generate_visb_html_to_codes(StateIds,Options,Codes). % write to codes list
903
904		% ------------------------------
905
906
907		show_typed_var_in_visb(all,_) :- !.
908		show_typed_var_in_visb(VarList,b(identifier(ID),_,_)) :- !, show_var_in_visb(VarList,ID).
909		show_var_in_visb(VarList,ID ) :- (VarList=all -> true ; member(ID,VarList) -> true).
910
911		% generate a table for the state (we could use bvisual2)
912		gen_state_table(Stream,Options,StateIds) :-
913		b_or_z_mode,
914		member(show_variables(VarList),Options),
915		b_get_machine_variables(TypedVars),
916		% is this useful if Len > 1, but StateIds are not from a trace? (see also below for formulas)
917		(length(StateIds,Len), Len > 1 -> NOptions = [show_prev_value|Options] ; NOptions = Options),
918		gen_state_table_aux(Stream,NOptions,'Variables',TypedVars,VarList,[],'Value','bVar_'),fail.
919		gen_state_table(Stream,Options,StateIds) :-
920		b_or_z_mode,
921		member(show_variables(VarList),Options),
922		b_get_machine_expressions(AExprs,Options), AExprs \= [],
923		(length(StateIds,Len), Len > 1 -> NOptions = [show_prev_value|Options] ; NOptions = Options),
924		gen_state_table_aux(Stream,NOptions,'Formulas',AExprs,VarList,[],'Value','bVar_'),fail.
925		gen_state_table(Stream,Options,StateIds) :-
926		b_or_z_mode,
927		member(show_constants(IDList),Options),
928		b_get_machine_constants(TypedVars),
929		last(StateIds,Last), % we assume there is only one constant valuation in the trace; TO DO: generalise
930		get_state_and_action(Last,LastId,_,_),
931		visited_expression(LastId,BState),
932		expand_to_constants_and_variables(BState,ConstState,_),
933		gen_state_table_aux(Stream,Options,'Constants',TypedVars,IDList,ConstState,'Value','bConstant_'),fail.
934		gen_state_table(Stream,Options,_) :-
935		b_or_z_mode,
936		member(show_sets(IDList),Options),
937		findall(TSet,bv_top_level_set(TSet,_),TypedVars),
938		findall(bind(Set,Val),(bv_top_level_set(TSet,Val),get_texpr_id(TSet,Set)),BState),
939		gen_state_table_aux(Stream,Options,'Sets',TypedVars,IDList,BState,'Value','bSet_'),fail.
940		% TO DO: maybe show also top-level guards specfile_possible_trans_name or get_top_level_guard
941		gen_state_table(Stream,Options,_StateIds) :-
942		b_or_z_mode,
943		member(show_events(IDList),Options),
944		get_specification_description(operations,SN),
945		atom_tail_to_lower_case(SN,SectionName),
946		findall(b(identifier(OpName),subst,[]),b_top_level_operation(OpName),TypedVars),
947		% TODO: op(Params,Results) instead of subst
948		gen_state_table_aux(Stream,Options,SectionName,TypedVars,IDList,[],'Enabled','bOperation_'),fail.
949		gen_state_table(Stream,Options,StateIds) :-
950		xtl_mode,
951		(length(StateIds,Len), Len > 1 -> NOptions = [show_prev_value|Options] ; NOptions = Options),
952		bv_get_top_level(IDs),
953		findall(b(identifier(ID),string,[]), member(ID,IDs), Props),
954		gen_state_table_aux(Stream,NOptions,'Properties',Props,IDs,[],'Value','bVar_'), fail.
955		gen_state_table(_Stream,_,_).
956
957
958		gen_source_code_section(Stream,Options) :-
959		member(show_source,Options), % we could also include original sources, rather than just internal rep.
960		!,
961		Section = 'Source',
962		format(Stream,' <button type="button" class="collapsible collapsible-style" title="Inspect source code of internal representation of ProB of model">~w</button>~n',[Section]),
963		format(Stream,'<div class="coll-content-hid">~n',[]),
964		get_internal_representation(PP),
965		html_escape_codes(PP,EPP),
966		format(Stream,'<pre>~s</pre>~n',[EPP]),
967		format(Stream,'</div>~n',[]).
968		gen_source_code_section(_Stream,_).
969
970
971		% creates a HTML table with header name Section and including one row per ID in TypedVars;
972		% id of value for ID is prefixed with IDPrefix
973		% VarListToShow is either all or a list of ids
974		gen_state_table_aux(Stream,Options,Section,TypedVars,VarListToShow,BState,ValueStr,IDPrefix) :-
975		include(show_typed_var_in_visb(VarListToShow),TypedVars,SVars), % check which ids should be shown
976		length(SVars,SLen), SLen>0,
977		length(TypedVars,Len),
978		(SLen=Len
979		-> format(Stream,' <button type="button" class="collapsible collapsible-style">~w (~w)</button>~n',[Section,SLen])
980		; format(Stream,' <button type="button" class="collapsible collapsible-style">~w (~w/~w)</button>~n',
981		[Section,SLen,Len])
982		),
983		format(Stream,'<div class="coll-content-hid">~n',[]),
984		(member(show_prev_value,Options) % add extra column for previous value of variables (and animation expressions)
985		-> format(Stream,' <table> <tr> <th>Nr</th> <th>Name</th> <th>Value</th> <th>Previous Value</th> </tr>~n',[])
986		; format(Stream,' <table> <tr> <th>Nr</th> <th>Name</th> <th>~w</th> </tr>~n',[ValueStr])),
987		( nth1(Nr,SVars,IDorExprToShow),
988		get_state_table_name_and_expr(IDorExprToShow,ID,LongID,TExpr),
989		(get_state_value_codes_for_id(BState,ID,Options,_,ValCodes)
990		-> html_escape_codes(ValCodes,EVC) % Value provided in BState; may be overriden in trace export
991		; EVC = "?"),
992		html_text_codes(LongID,ELongID), % LongID can contain a pretty-printed expression
993		get_table_hover_message_codes(ID,TExpr,HoverMsgC),
994		(member(show_prev_value,Options) % add previous value of variables (and animation expressions)
995		-> % for variables the values are added later in JS
996		% do we want to show the previous value in the state only HTML?
997		format(Stream,'~n <tr id="row_~w~w" title="~s"> <td>~w</td> <td id="name_~w~w">~s</td> <td id="~w~w">?</td> <td id="bVarPrev_~w">?</td> </tr>~n',
998		[IDPrefix,ID, HoverMsgC, Nr, IDPrefix,ID,ELongID, IDPrefix,ID, ID ])
999		;
1000		format(Stream,'~n <tr id="row_~w~w" title="~s"> <td>~w</td> <td id="name_~w~w">~s</td> <td id="~w~w">~s</td> </tr>~n',
1001		[IDPrefix,ID, HoverMsgC, Nr, IDPrefix,ID,ELongID, IDPrefix,ID,EVC])),
1002		fail
1003		;
1004		format(Stream,' </table>~n </div>~n',[])
1005		).
1006
1007		%get_state_table_name_and_expr(bexpr(Kind,TExpr),Name,LongName,Expr) :- !, % we have special expression to show
1008		% Name=Kind,LongName=Kind,Expr=TExpr.
1009		get_state_table_name_and_expr(bexpr(Kind,TExpr),ID,LongName,Expr) :- !, % we have special expression to show
1010		ID=Kind, % ID for SVG updates, ...
1011		translate_bexpression_with_limit(TExpr,200,TS),
1012		ajoin([Kind,' == ',TS],LongName),
1013		Expr=TExpr.
1014		get_state_table_name_and_expr(TID,ID,ID,TID) :- get_texpr_id(TID,ID). % normal case: variable name
1015
1016
1017		visb_machine_animation_expression(variant,AEName,Variant,_) :-
1018		b_get_operation_variant(Name,ConvOrAnt,Variant),
1019		ajoin(['Variant for ',Name, ' (',ConvOrAnt,')'],AEName).
1020		visb_machine_animation_expression(animation_expression,Name,TExpr,_) :-
1021		b_get_machine_animation_expression(Name,TExpr).
1022		visb_machine_animation_expression(invariant,Name,TPred,Options) :-
1023		member(show_invariants,Options),
1024		b_nth1_non_ignored_invariant(Nr,TPred,_),
1025		ajoin(['INVARIANT-',Nr],Name).
1026		% TODO: we should also adapt get_state_value_change to return true when invariant_violated is false for the state
1027		% we could also only include this section when there is an invariant violation in the trace?
1028
1029		b_get_machine_expressions(List,Options) :-
1030		findall(bexpr(AE_Name,AExpr),visb_machine_animation_expression(_,AE_Name,AExpr,Options),List).
1031		% 'ANIMATION_EXPRESSION' or invariants or variants
1032
1033
1034		% get hover message for entries in variables/constants/... rows:
1035		get_table_hover_message_codes(ID,TExpr,EscHoverMsg) :-
1036		get_texpr_type(TExpr,Type),
1037		(Type=subst,b_get_machine_operation_signature(ID,TS)
1038		-> ajoin(['Operation: ',TS],HoverMsg)
1039		; pretty_type(Type,TS),
1040		(get_texpr_description(TExpr,Desc)
1041		-> ajoin(['Type: ',TS,'\nDesc: ',Desc],HoverMsg)
1042		; ajoin(['Type: ',TS],HoverMsg)
1043		)
1044		),
1045		atom_codes(HoverMsg,HoverCodes),
1046		html_escape_codes(HoverCodes,EscHoverMsg).
1047
1048		% get the values that should be displayed in the variables table
1049		get_state_value_change(StateId,State,ID,Options,ECodes) :-
1050		extract_variables_from_state(State,VariableBState),
1051		( get_state_value_codes_for_id(VariableBState,ID,Options,Val,ValCodes) % look up variable values
1052		; visb_machine_animation_expression(_,_,_,Options) ->
1053		state_corresponds_to_fully_setup_b_machine(State,FullState),
1054		get_state_value_codes_for_anim_expr(StateId,FullState,ID,Options,Val,ValCodes) % evaluate animation expressions
1055		),
1056		escape_if_necessary(Val,ValCodes,ECodes). % change " to \" for JavaScript
1057		% formatsilent('Value for ~w~nunescaped: "~s",~n escaped: "~s"~n',[ID,ValCodes,ECodes]).
1058
1059		% avoid unnecessary escaping traversals:
1060		escape_if_necessary([],ValCodes,Res) :- !, Res=ValCodes.
1061		escape_if_necessary(int(_),ValCodes,Res) :- !, Res=ValCodes.
1062		escape_if_necessary(pred_true,ValCodes,Res) :- !, Res=ValCodes.
1063		escape_if_necessary(pred_false,ValCodes,Res) :- !, Res=ValCodes.
1064		escape_if_necessary(_,ValCodes,ECodes) :- js_escape_codes(ValCodes,ECodes).
1065
1066
1067		get_state_value_codes_for_id(BState,ID,Options,Val,ValCodes) :-
1068		member(bind(ID,Val),BState),
1069		translate_values_for_state_table(Val,Options,ValCodes).
1070
1071		% translate a value for display in state table (not yet escaped)
1072		translate_values_for_state_table(Val,Options,ValCodes) :-
1073		(member(limit_for_values(Nr),Options)
1074		-> translate_bvalue_to_codes_with_limit(Val,Nr,ValCodes)
1075		; get_preference(expand_avl_upto,Max), Max<0
1076		-> translate_bvalue_to_codes(Val,ValCodes) % unlimited
1077		; translate_bvalue_to_codes_with_limit(Val,10000,ValCodes)
1078		).
1079
1080
1081		get_state_value_codes_for_anim_expr(StateId,BState,AE_Name,Options,ResValue,ValCodes) :-
1082		visb_machine_animation_expression(Kind,AE_Name,AExpr,Options),
1083		(Kind=invariant
1084		-> ((invariant_not_yet_checked(StateId) ; invariant_violated(StateId))
1085		-> (safe_create_texpr(convert_bool(AExpr),boolean,TExpr),
1086		evaluate_visb_formula(TExpr,AE_Name,'',BState,ResValue,unknown)
1087		-> translate_pred_val(ResValue,ValCodes)
1088		; ResValue=pred_unknown, ValCodes = "?" % WD error?
1089		)
1090		; ResValue=pred_true, translate_pred_val(pred_true,ValCodes) % no need to evaluate invariant
1091		)
1092		; evaluate_visb_formula(AExpr,AE_Name,'',BState,ResValue,unknown),
1093		translate_values_for_state_table(ResValue,Options,ValCodes)
1094		).
1095		translate_pred_val(pred_true,[8868]). % see translate:unicode_translation(truth,X).
1096		translate_pred_val(pred_false,[8869]). % see translate:unicode_translation(falsity,X).
1097
1098
1099		get_state_value_enabled_operation_status(StateId,OpName,Enabled,EnabledValue,TransStr) :-
1100		b_top_level_operation(OpName),
1101		findall(TransID, (transition(StateId,OpTerm,TransID,_NewStateId),
1102		match_operation(OpTerm,OpName)), TransList),
1103		length(TransList,Len),
1104		(Len>0
1105		-> Enabled=true,
1106		EnabledValue = "\x2705\", % green check mark, TRUE alternatives \x2705\ \x2713\ \x2714\
1107		(TransList=[TID], transition(StateId,OpTerm,TID,NewStateId),
1108		translate_event_with_src_and_target_id(OpTerm,StateId,NewStateId,200,TransStr)
1109		-> true
1110		; ajoin([OpName,' (',Len,'\xd7\)'],TransStr) %
1111		)
1112		; time_out_for_node(StateId,OpName,TypeOfTimeOut) ->
1113		Enabled=TypeOfTimeOut,
1114		EnabledValue = [8987], % four o'clock symbol
1115		TransStr = OpName
1116		%ajoin(['No transition found due to: ',TypeOfTimeOut],HoverMsg)
1117		; get_preference(maxNrOfEnablingsPerOperation,0) ->
1118		Enabled=not_computed,
1119		EnabledValue = [10067], % red question mark
1120		TransStr = OpName
1121		%'No transitions were computed because MAX_OPERATIONS = 0' = HoverMsg
1122		; b_get_machine_operation_max(OpName,0) ->
1123		Enabled=not_computed,
1124		EnabledValue = [10067], % red question mark
1125		TransStr = OpName
1126		%ajoin(['No transitions were computed because MAX_OPERATIONS_',OpName,' = 0'],HoverMsg)
1127		; Enabled=false,
1128		EnabledValue = [9940], % stop sign, FALSE, alternatives \x10102\
1129		TransStr = OpName
1130		%ajoin(['Not enabled'],HoverMsg)
1131		). % TO DO: show whether this is the next step in the trace