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 | ). |