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