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