1 | % (c) 2016-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(meta_interface,[command_description/3, command_call/4, | |
6 | command_unavailable/2, | |
7 | command_arguments/2, command_optional_arguments/4, | |
8 | command_category/2, | |
9 | command_preferences_category/2, | |
10 | command_additional_info/2, | |
11 | get_command_preferences/2, | |
12 | call_command/5, | |
13 | is_dot_command/1, is_dot_command/6, | |
14 | call_dot_command/2, call_dot_command/3, | |
15 | is_dot_command_for_expr/1, call_dot_command_for_expr/3, call_dot_command_for_expr/4, | |
16 | call_dot_command_with_engine/4, call_dot_command_with_engine_for_expr/5, | |
17 | is_table_command/6, is_table_command/1, is_table_command_for_expr/1, | |
18 | write_table_to_csv_file/2, write_table_to_csv_file/3, write_table_to_text_file/2]). | |
19 | ||
20 | :- use_module(probsrc(module_information)). | |
21 | :- module_info(group,visualization). | |
22 | :- module_info(description,'This module provides access and description to a variety of Prolog commands.'). | |
23 | ||
24 | :- use_module(probsrc(error_manager)). | |
25 | :- use_module(probsrc(debug)). | |
26 | :- use_module(probsrc(tools_strings),[ajoin/2]). | |
27 | :- use_module(probsrc(preferences),[get_preference/2]). | |
28 | :- use_module(probsrc(specfile),[ | |
29 | b_or_z_mode/0, | |
30 | eventb_mode/0, | |
31 | csp_mode/0, | |
32 | %csp_with_bz_mode/0, | |
33 | spec_file_has_been_successfully_loaded/0]). | |
34 | :- use_module(probsrc(state_space), [current_state_corresponds_to_fully_setup_b_machine/0, current_state_corresponds_to_setup_constants_b_machine/0]). | |
35 | ||
36 | :- use_module(probsrc(bmachine),[b_machine_has_constants_or_properties/0, b_machine_has_assertions/0, | |
37 | b_machine_has_constants/0, b_machine_has_variables/0, | |
38 | b_machine_has_operations/0]). | |
39 | ||
40 | % dot command with no arguments | |
41 | is_dot_command(Command) :- command_category(Command,dot), command_arguments(Command,[dotfile]). | |
42 | call_dot_command(Command,File) :- call_dot_command(Command,File,[]). | |
43 | call_dot_command(Command,File,OptionalArgs) :- %print(cmd(Command,File,OptionalArgs)),nl, | |
44 | call_command(dot,Command,[dotfile],[File],OptionalArgs). | |
45 | ||
46 | is_dot_command_for_expr(Command) :- | |
47 | command_category(Command,dot), command_arguments(Command,[expression_atom,dotfile]). | |
48 | call_dot_command_for_expr(Command,Expr,File) :- | |
49 | call_dot_command_for_expr(Command,Expr,File,[]). | |
50 | call_dot_command_for_expr(Command,Expr,File,OptionalArgs) :- % print(cmd(Command,Expr,File,OptionalArgs)),nl, | |
51 | call_command(dot,Command,[expression_atom,dotfile],[Expr,File],OptionalArgs). | |
52 | ||
53 | ||
54 | :- use_module(probsrc(tools_commands),[gen_dot_output/4, valid_dot_output_format/1]). | |
55 | :- use_module(probsrc(tools),[split_filename/3]). | |
56 | :- use_module(probsrc(tools_strings),[ajoin/2]). | |
57 | ||
58 | % call dot_command and dot engine if necessary | |
59 | call_dot_command_with_engine(Command,File,OptionalArgs,DotEngine) :- | |
60 | filename_extension_can_be_converted(File,Ext,DotFile), | |
61 | !, % we can convert a dot file to this format | |
62 | call_dot_command(Command,DotFile,OptionalArgs), | |
63 | % DotEngine = default, sfdp, circo, ... | |
64 | gen_dot_output(DotFile,DotEngine,Ext,File). | |
65 | call_dot_command_with_engine(Command,File,OptionalArgs,_) :- | |
66 | call_dot_command(Command,File,OptionalArgs). | |
67 | ||
68 | % call dot_command and dot engine if necessary | |
69 | call_dot_command_with_engine_for_expr(Command,Expr,File,OptionalArgs,DotEngine) :- | |
70 | filename_extension_can_be_converted(File,Ext,DotFile), | |
71 | !, % we can convert a dot file to this format | |
72 | call_dot_command_for_expr(Command,Expr,DotFile,OptionalArgs), | |
73 | gen_dot_output(DotFile,DotEngine,Ext,File). | |
74 | call_dot_command_with_engine_for_expr(Command,Expr,File,OptionalArgs,_) :- | |
75 | call_dot_command_for_expr(Command,Expr,File,OptionalArgs). | |
76 | ||
77 | filename_extension_can_be_converted(File,Ext,DotFile) :- | |
78 | split_filename(File,FileRoot,Ext), Ext \= dot, | |
79 | valid_dot_output_format(Ext),!, % we can convert a dot file to this format | |
80 | ajoin([FileRoot,'.dot'],DotFile). % TODO: we could generate a temp file in /tmp | |
81 | ||
82 | % TODO: maybe automatically call dot -Tpdf <F.dot >F.pdf for pdf, svg or similar file endings | |
83 | ||
84 | % dot commands with no or with extra arguments: | |
85 | % find out which dot commands are available and what arguments and preferences they take: | |
86 | is_dot_command(Command,Name,Description,NumberOfFormulaArgs,Preferences,AdditionalInfo) :- | |
87 | command_description(Command,Name,Description), % move forward to ensure ordering of found commands is same as in file | |
88 | (is_dot_command(Command),NumberOfFormulaArgs=0 ; | |
89 | is_dot_command_for_expr(Command),NumberOfFormulaArgs=1), | |
90 | get_command_preferences(Command, Preferences), | |
91 | findall(Info, command_additional_info(Command, Info), AdditionalInfo). | |
92 | ||
93 | :- use_module(library(lists)). | |
94 | % table commands (return as last argument list of lists) | |
95 | is_table_command(Command,Name,Description,NumberOfFormulaArgs,Preferences,AdditionalInfo) :- | |
96 | command_category(Command,table), | |
97 | command_arguments(Command,Args), last(Args,table_result), | |
98 | length(Args,Len), NumberOfFormulaArgs is Len - 1, | |
99 | command_description(Command,Name,Description), | |
100 | get_command_preferences(Command, Preferences), | |
101 | findall(Info, command_additional_info(Command, Info), AdditionalInfo). | |
102 | ||
103 | is_table_command(Command) :- | |
104 | is_table_command(Command,_,_,0,_,_). | |
105 | is_table_command_for_expr(Command) :- | |
106 | command_category(Command,table), command_arguments(Command,[expression_atom,table_result]). | |
107 | ||
108 | % --------------------------------------- | |
109 | ||
110 | :- use_module(probsrc(tools_io),[safe_intelligent_open_file/3]). | |
111 | % write result of a table command to a CSV file, user_output prints to console w/o CSV seperators | |
112 | ||
113 | ||
114 | write_table_to_csv_file(CSVFile,Table) :- | |
115 | write_table_to_csv_file(CSVFile,[],Table). | |
116 | ||
117 | write_table_to_text_file(TextFile,Table) :- | |
118 | write_table_to_csv_file(TextFile,[text_output],Table). | |
119 | ||
120 | write_table_to_csv_file(CSVFile,Opts,Table) :- | |
121 | (CSVFile=user_output ; | |
122 | member(text_output,Opts)), | |
123 | !, % use textual output on user_output | |
124 | Options = [csv_separator(' '),no_quoting|Opts], | |
125 | safe_intelligent_open_file(CSVFile,write,Stream), | |
126 | call_cleanup(write_table_to_csv_stream(Stream,Options,Table), close(Stream)). | |
127 | write_table_to_csv_file(CSVFile,Options,Table) :- | |
128 | safe_intelligent_open_file(CSVFile,write,Stream), | |
129 | call_cleanup(write_table_to_csv_stream(Stream,Options,Table), close(Stream)). | |
130 | ||
131 | ||
132 | % write result of a table command to a CSV stream | |
133 | write_table_to_csv_stream(Stream,Options,list(L)) :- !, | |
134 | write_table_to_csv_stream(Stream,Options,L). | |
135 | write_table_to_csv_stream(_Stream,_,[]) :- !. | |
136 | write_table_to_csv_stream(Stream,Options,[H|T]) :- !, write_row(H,Options,Stream), nl(Stream), | |
137 | write_table_to_csv_stream(Stream,Options,T). | |
138 | write_table_to_csv_stream(Stream,Options,Other) :- write(Stream,Other),nl(Stream), | |
139 | add_internal_error('Table is not a list: ',write_table_to_csv_stream(Stream,Options,Other)). | |
140 | ||
141 | write_row([],_,_) :- !. | |
142 | write_row(list(L),Options,Stream) :- !, write_row(L,Options,Stream). | |
143 | write_row([H],Options,Stream) :- !, write_value(H,Options,Stream). | |
144 | write_row([H|T],Options,Stream) :- !, write_value(H,Options,Stream), write_sep(Options,Stream), | |
145 | write_row(T,Options,Stream). | |
146 | write_row(Other,Options,Stream) :- write(Stream,Other),nl(Stream), | |
147 | add_internal_error('Table row is not a list: ',write_table_to_csv_stream(Stream,Options,Other)). | |
148 | ||
149 | write_sep(Options,Stream) :- member(csv_separator(Sep),Options), !, write(Stream,Sep). | |
150 | write_sep(_,Stream) :- write(Stream,','). | |
151 | ||
152 | write_value(Nr,_,Stream) :- number(Nr), !, write(Stream,Nr). | |
153 | write_value(Val,Options,Stream) :- member(no_quoting,Options), !, write(Stream,Val). | |
154 | write_value(Atom,_,Stream) :- atom(Atom), atom_codes(Atom,AC),!, | |
155 | csv_escape_codes(AC,EC), | |
156 | format(Stream,'"~s"',[EC]). % quote for CSV | |
157 | write_value(Other,_,Stream) :- format(Stream,'"~w"',[Other]). | |
158 | ||
159 | csv_escape_codes([],[]). | |
160 | csv_escape_codes([0'" | T],R) :- !, | |
161 | R=[0'", 0'" |ET], % quotes in a CSV record must be preceded by another quote | |
162 | csv_escape_codes(T,ET). | |
163 | csv_escape_codes([H|T],[H|ET]) :- csv_escape_codes(T,ET). | |
164 | ||
165 | % --------------------------------------- | |
166 | ||
167 | % call a command described in this module | |
168 | call_command(Category,Command,FormalArgs,ActualArgs,OptionalArgs) :- | |
169 | command_category(Command,Category), | |
170 | command_arguments(Command,FormalArgs), % to do: more flexible matching of args ? | |
171 | !, | |
172 | (command_unavailable(Command,Msg) | |
173 | -> ajoin(['Command ', Command, ' not available: '],Msg1), | |
174 | add_error(meta_interface,Msg1,Msg), | |
175 | fail | |
176 | ; setup_optional_args(Command,OptionalArgs,OptArgValueList), | |
177 | (command_call(Command,ActualArgs,OptArgValueList,Call) | |
178 | -> debug_println(4,command_call(Call)), | |
179 | call(Call) | |
180 | ; command_call(Command,ArgsExpected,_,_),length(ArgsExpected,Exp),length(ActualArgs,Form) %, Exp \= Form | |
181 | -> | |
182 | ajoin(['Command ', Command, ' expects ', Exp, ' arguments, but obtained ',Form,'!'],Msg1), | |
183 | add_internal_error(Msg1,command_call(Command,ActualArgs,OptArgValueList,_)), | |
184 | fail | |
185 | ; add_internal_error('Cannot construct command call: ',command_call(Command,ActualArgs,OptArgValueList,_)), | |
186 | fail | |
187 | ) | |
188 | ). | |
189 | call_command(Category,Command,FormalArgs,_ActualArgs,_OptArgs) :- command_category(Command,Category), | |
190 | !, | |
191 | add_error(meta_interface,'Argument mis-match when calling command: ',Command:FormalArgs),fail. | |
192 | call_command(Category,Command,_,_,_) :- command_category(Command,_OtherCategory),!, | |
193 | add_error(meta_interface,'Command belongs to other category: ',Category:Command),fail. | |
194 | call_command(Category,Command,_,_,_) :- | |
195 | add_error(meta_interface,'Unknown command: ',Category:Command),fail. | |
196 | ||
197 | ||
198 | setup_optional_args(Command,OptionalArgs,OptArgValueList) :- | |
199 | command_optional_arguments(Command,Names,_Types,DefaultValues),!, | |
200 | setup_opt_args_aux(Names,DefaultValues,OptionalArgs,Command,OptArgValueList). | |
201 | setup_optional_args(_,[],Res) :- !, Res=[]. | |
202 | setup_optional_args(Cmd,Opt,Res) :- add_internal_error('Illegal optional arguments: ',setup_optional_args(Cmd,Opt,Res)), | |
203 | Res=[]. | |
204 | ||
205 | :- use_module(library(lists),[select/3]). | |
206 | ||
207 | setup_opt_args_aux([],[],OptArgs,Command,Res) :- | |
208 | (OptArgs = [] -> true ; add_internal_error('Too many optional arguments: ',Command:OptArgs)), | |
209 | Res = []. | |
210 | setup_opt_args_aux([Name|NT],[Default|DT],OptArgs,Command,Res) :- | |
211 | (select('='(Name,Value),OptArgs,OA2) | |
212 | -> Res = [Value|RT], setup_opt_args_aux(NT,DT,OA2,Command,RT) | |
213 | ; Res = [Default|RT], setup_opt_args_aux(NT,DT,OptArgs,Command,RT) | |
214 | ). | |
215 | ||
216 | ||
217 | % TO DO: provide automatic conversion ? expression_atom -> expression_codes -> typed_expression ? | |
218 | ||
219 | :- use_module(probsrc(preferences),[virtual_preference_category/2]). | |
220 | % get all preferences for a command | |
221 | get_command_preferences(Command,Preferences) :- | |
222 | findall(Pref, (command_preferences_category(Command,PrefCat), | |
223 | virtual_preference_category(Pref,PrefCat)), Preferences). | |
224 | ||
225 | % -------------------- | |
226 | % COMMAND DESCRIPTIONS | |
227 | % -------------------- | |
228 | ||
229 | :- discontiguous command_description/3, command_call/4, | |
230 | command_unavailable/2, command_arguments/2, | |
231 | command_optional_arguments/4, | |
232 | command_category/2, command_preferences_category/2, | |
233 | command_additional_info/2. | |
234 | ||
235 | :- use_module(probsrc(b_machine_hierarchy),[write_dot_event_hierarchy_to_file/1,write_dot_variable_hierarchy_to_file/1, | |
236 | write_dot_hierarchy_to_file/1]). | |
237 | ||
238 | command_description(machine_hierarchy,'Machine Hierarchy','Shows the machine hierarchy of a classical B model'). | |
239 | command_call(machine_hierarchy,[File],[],b_machine_hierarchy:write_dot_hierarchy_to_file(File)). | |
240 | command_unavailable(machine_hierarchy,Txt) :- command_unavailable(b_mode,Txt). | |
241 | command_arguments(machine_hierarchy,[dotfile]). | |
242 | command_category(machine_hierarchy,dot). | |
243 | command_preferences_category(machine_hierarchy,dot_machine_hierarchy). | |
244 | ||
245 | command_description(operations,'Operation Call Graph','Shows the call graph of a classical B model'). | |
246 | command_call(operations,[File],[],b_machine_hierarchy:write_dot_op_hierarchy_to_file(File)). | |
247 | command_unavailable(operations,'only available for B or Z models with OPERATIONS') :- | |
248 | (\+ (b_or_z_mode,b_machine_has_operations) ; eventb_mode). | |
249 | command_arguments(operations,[dotfile]). | |
250 | command_category(operations,dot). | |
251 | command_preferences_category(operations,dot_graph_generator). | |
252 | ||
253 | command_description(event_hierarchy,'Event Hierarchy','Shows the event hierarchy of an Event-B model'). | |
254 | command_call(event_hierarchy,[File],[],b_machine_hierarchy:write_dot_event_hierarchy_to_file(File)). | |
255 | command_unavailable(event_hierarchy,'only available for Event-B models with events') :- | |
256 | \+ (eventb_mode, b_machine_has_operations). | |
257 | command_arguments(event_hierarchy,[dotfile]). | |
258 | command_category(event_hierarchy,dot). | |
259 | command_preferences_category(event_hierarchy,dot_event_hierarchy). | |
260 | ||
261 | command_description(variable_hierarchy,'Variable Refinement Hierarchy','Shows variables within the refinement hierarchy of an Event-B model'). | |
262 | command_call(variable_hierarchy,[File],[],b_machine_hierarchy:write_dot_variable_hierarchy_to_file(File)). | |
263 | command_unavailable(variable_hierarchy,'only available for Event-B models with variables') :- | |
264 | \+ (eventb_mode, b_machine_has_variables). | |
265 | command_arguments(variable_hierarchy,[dotfile]). | |
266 | command_category(variable_hierarchy,dot). | |
267 | command_preferences_category(variable_hierarchy,dot_variable_hierarchy). | |
268 | ||
269 | ||
270 | :- use_module(dotsrc(visualize_graph),[tcltk_print_states_for_dot/2]). | |
271 | command_description(state_space,'State Space','Show state space'). | |
272 | command_call(state_space,[File],[ColourTransitions],visualize_graph:tcltk_print_states_for_dot(File,ColourTransitions)). | |
273 | command_unavailable(state_space,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded. | |
274 | command_arguments(state_space,[dotfile]). | |
275 | command_optional_arguments(state_space,[colouring],[atom],[no_colour_for_transitions]). | |
276 | command_category(state_space,dot). | |
277 | command_preferences_category(state_space,dot_state_space). | |
278 | ||
279 | command_description(state_space_sfdp,'State Space (Fast)','Show state space (faster layout with less information and more overlaps)'). | |
280 | command_call(state_space_sfdp,[File],[ColourTransitions],visualize_graph:tcltk_print_states_for_dot_sfdp(File,ColourTransitions)). | |
281 | command_unavailable(state_space_sfdp,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded. | |
282 | command_arguments(state_space_sfdp,[dotfile]). | |
283 | command_optional_arguments(state_space_sfdp,[colouring],[atom],[no_colour_for_transitions]). | |
284 | command_category(state_space_sfdp,dot). | |
285 | command_preferences_category(state_space_sfdp,dot_state_space). % TODO: maybe remove those that are fixed and have no effect | |
286 | command_additional_info(state_space_sfdp,preferred_dot_type(sfdp)). % sfdp preferred | |
287 | ||
288 | :- use_module(dotsrc(visualize_graph),[tcltk_print_current_state_for_dot/1]). | |
289 | command_description(current_state,'Current State in State Space','Show current state and successors in state space'). | |
290 | command_call(current_state,[File],[],visualize_graph:tcltk_print_current_state_for_dot(File)). | |
291 | command_unavailable(current_state,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded. | |
292 | command_arguments(current_state,[dotfile]). | |
293 | command_category(current_state,dot). | |
294 | command_preferences_category(current_state,dot_state_space). | |
295 | ||
296 | :- use_module(dotsrc(visualize_graph),[tcltk_print_history_to_current_state_for_dot/1]). | |
297 | command_description(history,'Path to Current State','Show a path leading to current state'). | |
298 | % in ProB2-UI the Tcl/Tk history is not the ProB2 history !!! | |
299 | command_call(history,[File],[],visualize_graph:tcltk_print_history_to_current_state_for_dot(File)). | |
300 | command_unavailable(history,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded. | |
301 | command_arguments(history,[dotfile]). | |
302 | command_category(history,dot). | |
303 | command_preferences_category(history,dot_state_space). | |
304 | ||
305 | %:- use_module(dotsrc(visualize_graph),[tcltk_print_history_to_current_state_with_neighbors_for_dot/1]). | |
306 | %command_description(history_with_neighbours,'History of States (with Neighbours for last State)','Show history with neighbours leading to current state'). | |
307 | %command_call(history_with_neighbours,[File],[],visualize_graph:tcltk_print_history_to_current_state_with_neighbors_for_dot(File)). | |
308 | %command_unavailable(history_with_neighbours,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded. | |
309 | %command_arguments(history_with_neighbours,[dotfile]). | |
310 | %command_category(history_with_neighbours,dot). | |
311 | %command_preferences_category(history_with_neighbours,dot_state_space). | |
312 | ||
313 | :- use_module(dotsrc(state_space_reduction),[write_transition_diagram_for_expr_to_dotfile/2, | |
314 | write_signature_merge_to_dotfile/2]). | |
315 | command_description(signature_merge,'Signature Merge','Show signature-merged reduced state space (i.e., merge states which have same set of enabled events/operations)'). | |
316 | command_call(signature_merge,[File],[IgnoredEvents],state_space_reduction:write_signature_merge_to_dotfile(IgnoredEvents,File)). | |
317 | command_unavailable(signature_merge,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded. | |
318 | command_arguments(signature_merge,[dotfile]). | |
319 | command_optional_arguments(signature_merge,[ignored_events],[list(operations)],[[]]). | |
320 | command_category(signature_merge,dot). | |
321 | command_preferences_category(signature_merge,dot_graph_generator). | |
322 | ||
323 | ||
324 | :- use_module(dotsrc(reduce_graph_state_space),[print_dot_for_dfa_from_nfa/1]). | |
325 | command_description(dfa_merge,'DFA Merge','Show state space as deterministic automaton (DFA)'). | |
326 | command_call(dfa_merge,[File],[],reduce_graph_state_space:print_dot_for_dfa_from_nfa(File)). | |
327 | command_unavailable(dfa_merge,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded. | |
328 | command_arguments(dfa_merge,[dotfile]). | |
329 | command_category(dfa_merge,dot). | |
330 | ||
331 | :- use_module(dotsrc(state_space_reduction),[write_transition_diagram_for_expr_to_dotfile/2]). | |
332 | command_description(transition_diagram,'State Space Expression Projection...','Project state space onto expression values and show transition diagram'). | |
333 | command_call(transition_diagram,[Expression,File],[], | |
334 | state_space_reduction:write_transition_diagram_for_expr_to_dotfile(Expression,File)). | |
335 | command_unavailable(transition_diagram,Txt) :- command_unavailable(b_mode,Txt). | |
336 | command_arguments(transition_diagram,[expression_atom,dotfile]). % also accepts expression_raw_ast | |
337 | command_category(transition_diagram,dot). | |
338 | command_preferences_category(transition_diagram,dot_projection). | |
339 | ||
340 | :- use_module(probporsrc(dot_graphs_static_analysis), [tcltk_create_dependence_graph/1, tcltk_create_enable_graph/1]). | |
341 | command_description(enable_graph,'Event Enable Graph','Show enabling graph of events (i.e., which event/operation can enable/disable which other event)'). | |
342 | command_call(enable_graph,[File],[],dot_graphs_static_analysis:tcltk_create_enable_graph(File)). | |
343 | command_unavailable(enable_graph,Txt) :- command_unavailable(operations_events,Txt). | |
344 | command_arguments(enable_graph,[dotfile]). | |
345 | command_category(enable_graph,dot). | |
346 | command_preferences_category(enable_graph,dot_enable_graph). | |
347 | ||
348 | :- use_module(dotsrc(state_as_dot_graph),[print_cstate_graph/1]). | |
349 | command_description(state_as_graph,'Current State as Graph','Show values of variables in current state as one graph'). | |
350 | command_call(state_as_graph,[File],[],state_as_dot_graph:print_cstate_graph(File)). | |
351 | %command_call(state_as_graph,[File],[],visualize_graph:tcltk_print_current_state_as_graph_for_dot(File)). | |
352 | command_unavailable(state_as_graph,'only available for B,Z or Event-B models after constant setup or initialisation') :- \+ current_state_corresponds_to_setup_constants_b_machine. | |
353 | command_arguments(state_as_graph,[dotfile]). | |
354 | command_category(state_as_graph,dot). | |
355 | command_preferences_category(state_as_graph,state_as_graph). | |
356 | % we could use tcltk_print_current_state_as_graph_for_dot | |
357 | ||
358 | :- use_module(dotsrc(state_custom_dot_graph), | |
359 | [tcltk_generate_state_custom_dot_graph/1,state_custom_dot_graph_available/0]). | |
360 | ||
361 | command_description(custom_graph,'Customized Current State as Graph','Show values in current state as a graph using CUSTOM_GRAPH_EDGES efinition'). | |
362 | command_call(custom_graph,[File],[],state_custom_dot_graph:tcltk_generate_state_custom_dot_graph(File)). | |
363 | command_unavailable(custom_graph,'only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine') :- | |
364 | \+ state_custom_dot_graph_available. | |
365 | command_unavailable(custom_graph,'only available for initialised B,Z or Event-B models') :- | |
366 | state_custom_dot_graph_available, | |
367 | \+ current_state_corresponds_to_fully_setup_b_machine. | |
368 | command_arguments(custom_graph,[dotfile]). % also accepts expression_raw_ast | |
369 | command_category(custom_graph,dot). | |
370 | command_preferences_category(custom_graph,dot_graph_generator). | |
371 | ||
372 | % from tcltk_interface.pl: | |
373 | command_description(expr_as_graph,'(Relational) Expression as Graph...','Show (relational) expression value as a graph'). | |
374 | command_call(expr_as_graph,[Expression,File],[],tcltk_interface:tcltk_show_expression_as_dot(Expression,File)). | |
375 | command_unavailable(expr_as_graph,Txt) :- command_unavailable(b_mode,Txt). | |
376 | command_arguments(expr_as_graph,[expression_atom,dotfile]). % also accepts expression_raw_ast | |
377 | command_category(expr_as_graph,dot). | |
378 | command_preferences_category(expr_as_graph,state_as_graph). | |
379 | ||
380 | ||
381 | command_description(formula_tree,'Custom Predicate/Expression Formula Tree...','Show predicate/expressions and sub-formulas as a tree'). | |
382 | command_call(formula_tree,[Expression,File],[],tcltk_interface:generate_dot_from_formula(Expression,File)). | |
383 | command_unavailable(formula_tree,Txt) :- command_unavailable(b_mode,Txt). | |
384 | command_arguments(formula_tree,[expression_atom,dotfile]). % is actually predicate_atom, also accepts expression_raw_ast | |
385 | command_category(formula_tree,dot). | |
386 | command_preferences_category(formula_tree,dot_formula_tree). | |
387 | ||
388 | command_description(invariant,'Invariant Formula Tree','Show invariant as a formula tree'). | |
389 | command_call(invariant,[File],[],tcltk_interface:generate_dot_from_invariant(File)). | |
390 | command_unavailable(invariant,'only available for initialised B,Z or Event-B models') :- \+ current_state_corresponds_to_fully_setup_b_machine. | |
391 | command_arguments(invariant,[dotfile]). | |
392 | command_category(invariant,dot). | |
393 | command_preferences_category(invariant,dot_formula_tree). | |
394 | ||
395 | command_description(properties,'Properties Formula Tree','Show properties/axioms as a formula tree'). | |
396 | command_call(properties,[File],[],tcltk_interface:generate_dot_from_properties(File)). | |
397 | %command_unavailable(properties,'only available for initialised B,Z or Event-B models') :- \+ b_or_z_mode. % for non-initialised machines an existential quantifier is added | |
398 | command_unavailable(properties,'only available for B,Z or Event-B models with PROPERTIES after constant setup or initialisation') :- | |
399 | \+ (current_state_corresponds_to_setup_constants_b_machine,b_machine_has_constants_or_properties). | |
400 | command_arguments(properties,[dotfile]). | |
401 | command_category(properties,dot). | |
402 | command_preferences_category(properties,dot_formula_tree). | |
403 | ||
404 | command_description(assertions,'Assertions Formula Tree','Show assertions/theorems as a formula tree'). | |
405 | command_call(assertions,[File],[],tcltk_interface:generate_dot_from_assertions(File)). | |
406 | %command_unavailable(assertions,'only available for initialised B,Z or Event-B models') :- \+ b_or_z_mode. % for non-initialised machines an existential quantifier is added | |
407 | command_unavailable(assertions,'only available for B,Z or Event-B models with ASSERTIONS after constant setup or initialisation') :- | |
408 | \+ (current_state_corresponds_to_setup_constants_b_machine, b_machine_has_assertions). | |
409 | command_arguments(assertions,[dotfile]). | |
410 | command_category(assertions,dot). | |
411 | command_preferences_category(assertions,dot_formula_tree). | |
412 | ||
413 | command_description(deadlock,'Deadlock Formula Tree','Show deadlocking status (i.e., guards of all operations/events) in current state as a formula tree'). | |
414 | command_call(deadlock,[File],[],tcltk_interface:generate_dot_from_deadlock_po(File)). | |
415 | command_unavailable(deadlock,'only available for initialised B,Z or Event-B models with OPERATIONS') :- | |
416 | \+ (current_state_corresponds_to_fully_setup_b_machine, b_machine_has_operations). | |
417 | command_arguments(deadlock,[dotfile]). | |
418 | command_category(deadlock,dot). | |
419 | command_preferences_category(deadlock,dot_formula_tree). | |
420 | ||
421 | :- use_module(probsrc(bmachine),[b_get_machine_goal/1]). | |
422 | command_description(goal,'Goal Formula Tree','Show GOAL as a formula tree'). | |
423 | command_call(goal,[File],[],tcltk_interface:generate_dot_from_goal(File)). | |
424 | command_unavailable(goal,'only available for initialised B,Z or Event-B models with a GOAL DEFINITION') :- | |
425 | (\+ b_or_z_mode ; \+ b_get_machine_goal(_)). | |
426 | command_arguments(goal,[dotfile]). | |
427 | command_category(goal,dot). | |
428 | command_preferences_category(goal,dot_formula_tree). | |
429 | ||
430 | command_description(dependence_graph,'Event Dependence Graph','Show dependency graph of events (i.e., which events are not commutative)'). % difference to enable graph : not whether we have enabling/disabling but influence on effect | |
431 | command_call(dependence_graph,[File],[],dot_graphs_static_analysis:tcltk_create_dependence_graph(File)). | |
432 | command_unavailable(dependence_graph,Txt) :- command_unavailable(operations_events,Txt). | |
433 | command_arguments(dependence_graph,[dotfile]). | |
434 | command_category(dependence_graph,dot). | |
435 | command_preferences_category(dependence_graph,dot_enable_graph). | |
436 | ||
437 | command_description(variable_modification_graph,'Variable Read/Write Graph','Show variable modification by operations and reading in guards'). | |
438 | command_call(variable_modification_graph,[File],[],b_read_write_info:tcltk_dot_variable_modification_analysis(File)). | |
439 | command_unavailable(variable_modification_graph,Txt) :- command_unavailable(variables,Txt). | |
440 | command_arguments(variable_modification_graph,[dotfile]). | |
441 | command_category(variable_modification_graph,dot). | |
442 | command_preferences_category(variable_modification_graph,dot_variable_modification). | |
443 | ||
444 | :- use_module(dotsrc(visualize_graph),[tcltk_print_definitions_as_graph_for_dot/1]). | |
445 | command_description(definitions,'Definitions Graph','Show dependency graph of DEFINITIONS'). | |
446 | command_call(definitions,[File],[],visualize_graph:tcltk_print_definitions_as_graph_for_dot(File)). | |
447 | command_unavailable(definitions,'only available for B or Z models') :- (b_or_z_mode -> eventb_mode ; true). | |
448 | command_arguments(definitions,[dotfile]). | |
449 | command_category(definitions,dot). | |
450 | command_preferences_category(definitions,dot_definitions). | |
451 | ||
452 | :- use_module(dotsrc(visualize_graph),[tcltk_print_predicate_dependency_as_graph_for_dot/2]). | |
453 | command_description(predicate_dependency,'Predicate Dependency Graph...','Show dependency graph of conjuncts of a predicate'). | |
454 | command_call(predicate_dependency,[Pred,File],[],visualize_graph:tcltk_print_predicate_dependency_as_graph_for_dot(Pred,File)). | |
455 | command_unavailable(predicate_dependency,Txt) :- command_unavailable(b_mode,Txt). | |
456 | command_arguments(predicate_dependency,[expression_atom,dotfile]). % also accepts expression_raw_ast | |
457 | command_category(predicate_dependency,dot). | |
458 | ||
459 | command_description(last_error,'Last State Error Formula Tree','Try and visualise last state error source as a formula tree'). | |
460 | command_call(last_error,[File],[],tcltk_interface:generate_dot_from_last_span_predicate(File)). | |
461 | command_unavailable(last_error,'only available when (state) error occured') :- | |
462 | \+ tcltk_interface:can_generate_dot_from_last_state_error. | |
463 | command_arguments(last_error,[dotfile]). | |
464 | command_category(last_error,dot). | |
465 | ||
466 | command_description(last_mcts_tree,'MCTS Game Tree','Show two levels of last MCTS (Monte Carlo Tree Search) game tree'). | |
467 | command_call(last_mcts_tree,[File],[],mcts_game_play:tcltk_gen_last_mcts_tree(2,File)). | |
468 | command_unavailable(last_mcts_tree,'only available when GAME_OVER, ... definitions generated') :- \+ mcts_game_play:mcts_auto_play_available. | |
469 | command_unavailable(last_mcts_tree,'only available after a game move has been computed by MCTS') :- mcts_game_play:mcts_auto_play_available, \+ mcts_game_play:mcts_tree_available. | |
470 | command_arguments(last_mcts_tree,[dotfile]). | |
471 | command_category(last_mcts_tree,dot). | |
472 | ||
473 | ||
474 | % ----------------------------------------- | |
475 | ||
476 | % TABLE COMMANDS: | |
477 | ||
478 | ||
479 | command_description(machine_statistics,'Machine Statistics','Show statistics for main machine/specification'). | |
480 | command_call(machine_statistics,[Result],[],meta_interface:meta_get_machine_stats(Result)). | |
481 | command_unavailable(machine_statistics,Txt) :- command_unavailable(b_mode,Txt). | |
482 | command_arguments(machine_statistics,[table_result]). | |
483 | command_category(machine_statistics,table). | |
484 | ||
485 | :- use_module(probsrc(bmachine),[b_machine_statistics/2]). | |
486 | :- public meta_get_machine_stats/1. | |
487 | meta_get_machine_stats(list([list(['Key','Nr'])|L])) :- findall(list([Key,Nr]),b_machine_statistics(Key,Nr),L). | |
488 | ||
489 | command_description(expr_as_table,'Expression Table...','Show expression value as a table'). | |
490 | command_call(expr_as_table,[Expression,Result],[],tcltk_interface:tcltk_eval_as_table(Expression,Result)). | |
491 | command_unavailable(expr_as_table,Txt) :- command_unavailable(b_mode,Txt). | |
492 | command_arguments(expr_as_table,[expression_atom,table_result]). % also accepts expression_raw_ast | |
493 | command_category(expr_as_table,table). | |
494 | ||
495 | :- use_module(probsrc(tcltk_interface),[tcltk_operations_covered_info/3]). | |
496 | ||
497 | command_description(quick_operation_coverage,'Operation Coverage','Show which operations are covered in current state space'). | |
498 | command_call(quick_operation_coverage,[Result],[],tcltk_interface:tcltk_operations_covered_info(Result,_,quick)). | |
499 | command_unavailable(quick_operation_coverage,'only available for B,Z, Event-B with OPERATIONS, or CSP models') :- | |
500 | \+ (b_or_z_mode, b_machine_has_operations), \+ csp_mode. | |
501 | command_arguments(quick_operation_coverage,[table_result]). % also accepts expression_raw_ast | |
502 | command_category(quick_operation_coverage,table). | |
503 | ||
504 | command_description(precise_operation_coverage,'Operation Coverage and Feasibility','Show which feasible operations are covered (possible means operation is in principle feasible given invariant)'). | |
505 | command_call(precise_operation_coverage,[Result],[],tcltk_interface:tcltk_operations_covered_info(Result,_,precise)). | |
506 | command_unavailable(precise_operation_coverage,Txt) :- command_unavailable(operations_events,Txt). | |
507 | command_arguments(precise_operation_coverage,[table_result]). % also accepts expression_raw_ast | |
508 | command_category(precise_operation_coverage,table). | |
509 | ||
510 | % not really useful for ProB2: already in Statistics View when more details shown: | |
511 | %command_description(operation_coverage_stats,'Operation Coverage Statistics','Show operation coverage statistics'). | |
512 | %command_call(operation_coverage_stats,[Result],[],meta_interface:get_operation_coverage_stats(Result)). | |
513 | %command_arguments(operation_coverage_stats,[table_result]). | |
514 | %command_category(operation_coverage_stats,table). | |
515 | %:- use_module(extrasrc(coverage_statistics),[tcltk_compute_coverage/1]). | |
516 | %get_operation_coverage_stats(list([list(['Info'])|LRes])) :- | |
517 | % tcltk_compute_coverage(list(Res)), | |
518 | % maplist(wrap_into_list,Res,LRes). | |
519 | ||
520 | ||
521 | command_description(show_typing,'Show Typing','Show types for variables and constants'). | |
522 | command_call(show_typing,[Result],[],meta_interface:show_typing_table(Result)). | |
523 | command_unavailable(show_typing,Txt) :- command_unavailable(b_mode,Txt). | |
524 | command_arguments(show_typing,[table_result]). % also accepts expression_raw_ast | |
525 | command_category(show_typing,table). | |
526 | :- public show_typing_table/1. | |
527 | show_typing_table(list([list(['Typing'])|LRes])) :- tcltk_interface:tcltk_show_typing_of_variables_and_constants(list(Res)), | |
528 | maplist(wrap_into_list,Res,LRes). | |
529 | ||
530 | command_description(variable_coverage,'Variable Coverage','Show number of distinct covered values for variables in current state space'). | |
531 | command_call(variable_coverage,[Result],[],state_space_reduction:tcltk_compute_nr_covered_values_for_all_variables(Result)). | |
532 | command_unavailable(variable_coverage,Txt) :- command_unavailable(variables,Txt). | |
533 | command_arguments(variable_coverage,[table_result]). % also accepts expression_raw_ast | |
534 | command_category(variable_coverage,table). | |
535 | ||
536 | command_description(constants_coverage,'Constant Coverage','Show number of distinct covered values for constants in current state space'). | |
537 | command_call(constants_coverage,[Result],[],state_space_reduction:tcltk_compute_nr_covered_values_for_all_constants(Result)). | |
538 | command_unavailable(constants_coverage,Txt) :- command_unavailable(constants,Txt). | |
539 | command_arguments(constants_coverage,[table_result]). | |
540 | command_category(constants_coverage,table). | |
541 | ||
542 | % analyze_constants | |
543 | command_description(constants_analysis,'Constant Analysis','Show size (B and Prolog term size) and other infos about constants'). | |
544 | command_call(constants_analysis,[Result],[],coverage_statistics:tcltk_analyse_constants(Result)). | |
545 | command_unavailable(constants_analysis,Txt) :- command_unavailable(constants,Txt). | |
546 | command_arguments(constants_analysis,[table_result]). | |
547 | command_category(constants_analysis,table). | |
548 | ||
549 | command_description(expression_coverage,'Expression Coverage...','Evaluate expression over current state space and compute distinct values and their number of occurence'). | |
550 | command_call(expression_coverage,[Expr,Result],[],meta_interface:expression_coverage(Expr,Result)). | |
551 | command_unavailable(expression_coverage,Txt) :- command_unavailable(b_mode,Txt). | |
552 | command_arguments(expression_coverage,[expression_atom,table_result]). | |
553 | command_category(expression_coverage,table). | |
554 | ||
555 | :- public expression_coverage/2. | |
556 | :- use_module(dotsrc(state_space_reduction),[compute_covered_values_for_expression/4]). | |
557 | expression_coverage(ExprToEvaluate,list(LRes)) :- | |
558 | compute_covered_values_for_expression(ExprToEvaluate,_MaxTypeCard,_TotalNrOfValuesFound,list(Res)), | |
559 | maplist(wrap_into_list,Res,LRes). | |
560 | ||
561 | command_description(minmax_table,'Min/Max Values','Show minimum/maximum values for constants and variables in current state space; useful to analyse state explosion problems'). | |
562 | command_call(minmax_table,[Result],[],meta_interface:minmax_table(Result)). | |
563 | command_unavailable(minmax_table,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded. | |
564 | command_arguments(minmax_table,[table_result]). | |
565 | command_category(minmax_table,table). | |
566 | :- use_module(extrasrc(coverage_statistics),[tcltk_compute_min_max/1]). | |
567 | :- public minmax_table/1. | |
568 | minmax_table(R) :- tcltk_compute_min_max(R). | |
569 | ||
570 | command_description(inv_coverage,'Invariant Analysis','Analyse the truth value of individual invariants in current state space'). | |
571 | command_call(inv_coverage,[Result],[],mcdc_coverage:tcltk_get_invariant_coverage(Result)). | |
572 | command_unavailable(inv_coverage,Txt) :- command_unavailable(b_mode,Txt). | |
573 | command_arguments(inv_coverage,[table_result]). | |
574 | command_category(inv_coverage,table). | |
575 | ||
576 | command_description(vacuous_invariants,'Vacuous Invariants','Show list of vacuous invariants (implications or disjunctions wich are useless, given current explicit state space)'). | |
577 | command_call(vacuous_invariants,[Result],[],meta_interface:vacuous_invariants(Result)). | |
578 | command_unavailable(vacuous_invariants,Txt) :- command_unavailable(b_mode,Txt). | |
579 | command_arguments(vacuous_invariants,[table_result]). | |
580 | command_category(vacuous_invariants,table). | |
581 | :- public vacuous_invariants/1. | |
582 | vacuous_invariants(Res) :- | |
583 | tcltk_interface:tcltk_get_vacuous_invariants_table(Res). | |
584 | ||
585 | command_description(specialized_invariants,'Specialized Invariants','Show list of invariants (specialized using proof information for each operation; used by ProB for faster model checking)'). | |
586 | command_call(specialized_invariants,[Result],[],meta_interface:specialized_invariants(Result)). | |
587 | command_unavailable(specialized_invariants,Txt) :- command_unavailable(b_mode,Txt). | |
588 | command_arguments(specialized_invariants,[table_result]). | |
589 | command_category(specialized_invariants,table). | |
590 | :- public specialized_invariants/1. | |
591 | specialized_invariants(list([list(['Operation','Unproven','Predicate'])|LRes])) :- | |
592 | bmachine:tcltk_get_specialized_invariants_for_ops(list(Res)), | |
593 | maplist(wrap_into_list,Res,LRes). | |
594 | ||
595 | wrap_into_list(list(L),R) :- !, R=list(L). | |
596 | wrap_into_list([],R) :- !, R=list([]). | |
597 | wrap_into_list([H|T],R) :- !, R=list([H|T]). | |
598 | wrap_into_list(X,list([X])). | |
599 | ||
600 | command_description(vacuous_guards,'Vacuous Guards','Show list of vacuous Guards (i.e., guards which cannot be individually false and are thus useless, given current explicit state space)'). | |
601 | command_call(vacuous_guards,[Result],[],meta_interface:vacuous_guards(Result)). | |
602 | command_unavailable(vacuous_guards,Txt) :- command_unavailable(operations_events,Txt). | |
603 | command_arguments(vacuous_guards,[table_result]). | |
604 | command_category(vacuous_guards,table). | |
605 | :- public vacuous_guards/1. | |
606 | vacuous_guards(list([list(['Vacuous Guards'])|LRes])) :- | |
607 | tcltk_interface:tcltk_get_vacuous_guards(list(Res)), | |
608 | maplist(wrap_into_list,Res,LRes). | |
609 | ||
610 | :- use_module(extrasrc(mcdc_coverage),[tcltk_get_invariant_coverage/1, | |
611 | tcltk_compute_mcdc_operation_coverage/1, | |
612 | tcltk_compute_mcdc_invariant_coverage/1]). | |
613 | ||
614 | ||
615 | ||
616 | ||
617 | command_description(read_write_matrix,'Operation Read/Write Matrix','Show identifiers read and written by operations'). | |
618 | command_call(read_write_matrix,[Result],[],b_read_write_info:tcltk_read_write_matrix(Result)). | |
619 | command_unavailable(read_write_matrix,Txt) :- command_unavailable(operations_events,Txt). | |
620 | command_arguments(read_write_matrix,[table_result]). | |
621 | command_category(read_write_matrix,table). | |
622 | ||
623 | command_description(variable_read_write_matrix,'Variable Read/Write Matrix','Show for variables which operations read and write them'). | |
624 | command_call(variable_read_write_matrix,[Result],[],b_read_write_info:tcltk_variable_read_write_matrix(no_check,Result)). | |
625 | command_unavailable(variable_read_write_matrix,Txt) :- command_unavailable(variables,Txt). | |
626 | command_arguments(variable_read_write_matrix,[table_result]). | |
627 | command_category(variable_read_write_matrix,table). | |
628 | ||
629 | ||
630 | ||
631 | command_description(wd_pos,'WD POs','Show Well-Definedness Proof Obligations'). | |
632 | command_call(wd_pos,[Result],[],well_def_analyser:tcltk_get_machine_wd_pos(only_goal,Result,_,_)). | |
633 | command_unavailable(wd_pos,Txt) :- command_unavailable(b_mode,Txt). | |
634 | command_arguments(wd_pos,[table_result]). | |
635 | command_category(wd_pos,table). | |
636 | command_preferences_category(wd_pos,wd_commands). | |
637 | ||
638 | command_description(wd_pos_and_hyps,'WD POs and Hyps','Show Well-Definedness Proof Obligations and Hypotheses necessary for successful proof (for discharged POs)'). | |
639 | command_call(wd_pos_and_hyps,[Result],[],well_def_analyser:tcltk_get_machine_wd_pos(goal_and_hyps,Result,_,_)). | |
640 | command_unavailable(wd_pos_and_hyps,Txt) :- command_unavailable(b_mode,Txt). | |
641 | command_arguments(wd_pos_and_hyps,[table_result]). | |
642 | command_category(wd_pos_and_hyps,table). | |
643 | command_preferences_category(wd_pos_and_hyps,wd_commands). | |
644 | ||
645 | command_description(det_check_constants,'Compute Forced Constants','Analyse which values of CONSTANTS are forced and optionally compute an explanation (i.e., core of PROPERTIES which imply the value)'). | |
646 | command_call(det_check_constants,[Result],[],b_state_model_check:tcltk_cbc_constants_det_check(Result)). | |
647 | command_unavailable(det_check_constants,Txt) :- command_unavailable(constants,Txt). | |
648 | command_arguments(det_check_constants,[table_result]). | |
649 | command_category(det_check_constants,table). | |
650 | command_preferences_category(det_check_constants,cbc_commands). | |
651 | ||
652 | command_description(unsat_core_properties,'Unsat Core of Properties/Axioms','Analyse a minimal unsatisfiable core of the PROPERTIES/Axioms'). | |
653 | command_call(unsat_core_properties,[Result],[],unsat_cores:unsat_core_properties_table(Result)). | |
654 | command_unavailable(unsat_core_properties,'only available for B,Z or Event-B models with CONSTANTS or PROPERTIES') :- | |
655 | \+ (b_or_z_mode, b_machine_has_constants_or_properties). | |
656 | command_arguments(unsat_core_properties,[table_result]). | |
657 | command_category(unsat_core_properties,table). | |
658 | command_preferences_category(unsat_core_properties,table_commands). | |
659 | ||
660 | command_description(visb_attributes,'VisB Items','Show VisB items which set SVG attributes based on current state'). | |
661 | command_call(visb_attributes,[Result],[],visb_visualiser:tcltk_get_visb_items(Result)). | |
662 | command_unavailable(visb_attributes,'only available after a VisB file was loaded') :- | |
663 | \+ visb_visualiser:visb_file_is_loaded(_). | |
664 | command_arguments(visb_attributes,[table_result]). | |
665 | command_category(visb_attributes,table). | |
666 | command_preferences_category(visb_attributes,table_commands). | |
667 | ||
668 | command_description(visb_events,'VisB Events','Show VisB click events that are available in current state'). | |
669 | command_call(visb_events,[Result],[],visb_visualiser:tcltk_get_visb_events(Result)). | |
670 | command_unavailable(visb_events,'only available after a VisB file was loaded') :- | |
671 | \+ visb_visualiser:visb_file_is_loaded(_). | |
672 | command_arguments(visb_events,[table_result]). | |
673 | command_category(visb_events,table). | |
674 | command_preferences_category(visb_events,table_commands). | |
675 | ||
676 | command_description(visb_objects,'VisB Objects','Show VisB SVG objects which were created in addition to the SVG file'). | |
677 | command_call(visb_objects,[Result],[],visb_visualiser:tcltk_get_visb_objects(Result)). | |
678 | command_unavailable(visb_objects,'only available after a VisB file was loaded') :- | |
679 | \+ visb_visualiser:visb_file_is_loaded(_). | |
680 | command_arguments(visb_objects,[table_result]). | |
681 | command_category(visb_objects,table). | |
682 | command_preferences_category(visb_objects,table_commands). | |
683 | ||
684 | command_description(visb_hovers,'VisB Hovers','Show VisB hovers with enter and exit values'). | |
685 | command_call(visb_hovers,[Result],[],visb_visualiser:tcltk_get_visb_hovers(Result)). | |
686 | command_unavailable(visb_hovers,'only available after a VisB file was loaded') :- | |
687 | \+ visb_visualiser:visb_file_is_loaded(_). | |
688 | command_arguments(visb_hovers,[table_result]). | |
689 | command_category(visb_hovers,table). | |
690 | command_preferences_category(visb_hovers,table_commands). | |
691 | ||
692 | command_description(find_value,'Find Value...','Find value inside variables and constants'). | |
693 | command_call(find_value,[Expression,Result],[],tcltk_interface:tcltk_find_value_as_table(Expression,[prefix],Result)). | |
694 | command_unavailable(find_value,Txt) :- command_unavailable(b_mode,Txt). | |
695 | command_arguments(find_value,[expression_atom,table_result]). % also accepts expression_raw_ast | |
696 | command_category(find_value,table). | |
697 | ||
698 | command_description(id_value_formula_tree,'Value of Identifier as Formula Tree...','Show value of an identifier as a formula tree (mainly useful for symbolic values)'). | |
699 | command_call(id_value_formula_tree,[ID,File],[],tcltk_interface:tcltk_show_identifier_value_as_dot_tree(ID,File)). | |
700 | command_unavailable(id_value_formula_tree,Txt) :- command_unavailable(b_mode,Txt). | |
701 | command_arguments(id_value_formula_tree,[expression_atom,dotfile]). % is actually predicate_atom, also accepts expression_raw_ast | |
702 | command_category(id_value_formula_tree,dot). | |
703 | command_preferences_category(id_value_formula_tree,dot_formula_tree). | |
704 | ||
705 | ||
706 | command_description(mcdc_coverage,'MC/DC Operation Coverage','Show MC/DC operation coverage'). | |
707 | command_call(mcdc_coverage,[Result],[],mcdc_coverage:tcltk_compute_mcdc_operation_coverage(Result)). | |
708 | command_unavailable(mcdc_coverage,Txt) :- command_unavailable(operations_events,Txt). | |
709 | command_arguments(mcdc_coverage,[table_result]). | |
710 | command_category(mcdc_coverage,table). | |
711 | command_preferences_category(mcdc_coverage,mc_dc_commands). | |
712 | ||
713 | command_description(mcdc_inv_coverage,'MC/DC Invariant Coverage','Show MC/DC invariant coverage'). | |
714 | command_call(mcdc_inv_coverage,[Result],[],mcdc_coverage:tcltk_compute_mcdc_invariant_coverage(Result)). | |
715 | command_unavailable(mcdc_inv_coverage,Txt) :- command_unavailable(b_mode,Txt). | |
716 | command_arguments(mcdc_inv_coverage,[table_result]). | |
717 | command_category(mcdc_inv_coverage,table). | |
718 | command_preferences_category(mcdc_inv_coverage,mc_dc_commands). | |
719 | ||
720 | :- use_module(probsrc(runtime_profiler),[runtime_profile_available/0, tcltk_get_profile_info/1]). | |
721 | command_description(prob_profile_info,'ProB Profile Info','Show runtime information for operations'). | |
722 | command_call(prob_profile_info,[Result],[],runtime_profiler:tcltk_get_profile_info(Result)). | |
723 | command_unavailable(prob_profile_info,'no profiling information available, recompile probcli with -Dprob_profile=true') :- \+ runtime_profile_available,!. | |
724 | command_unavailable(prob_profile_info,Txt) :- command_unavailable(b_mode,Txt). | |
725 | command_arguments(prob_profile_info,[table_result]). % also accepts expression_raw_ast | |
726 | command_category(prob_profile_info,table). | |
727 | ||
728 | ||
729 | :- use_module(extrasrc(b_operation_cache),[tcltk_op_cache_stats/1]). | |
730 | command_description(prob_opcache_info,'ProB Operation Caching Info','Show information for operation caching (see OPERATION_REUSE preference)'). | |
731 | command_call(prob_opcache_info,[Result],[],b_operation_cache:tcltk_op_cache_stats(Result)). | |
732 | command_unavailable(prob_opcache_info,'only available when OPERATION_REUSE is TRUE or full.') :- | |
733 | get_preference(try_operation_reuse,false). | |
734 | command_unavailable(prob_opcache_info,Txt) :- command_unavailable(b_mode,Txt). | |
735 | command_arguments(prob_opcache_info,[table_result]). | |
736 | command_category(prob_opcache_info,table). | |
737 | ||
738 | ||
739 | command_description(prob_memo_profile,'ProB Memoization Info','Show information for memoized constants'). | |
740 | command_call(prob_memo_profile,[Result],[],memoization:tcltk_get_memo_profile_table(Result)). | |
741 | command_unavailable(prob_memo_profile,Txt) :- command_unavailable(b_mode,Txt). | |
742 | command_arguments(prob_memo_profile,[table_result]). | |
743 | command_category(prob_memo_profile,table). | |
744 | ||
745 | ||
746 | % a few typical reasons why commands are not available: | |
747 | command_unavailable(constants,'only available for B,Z or Event-B models with CONSTANTS') :- | |
748 | \+ (b_or_z_mode, b_machine_has_constants). | |
749 | command_unavailable(variables,'only available for B,Z or Event-B models with VARIABLES') :- | |
750 | \+ (b_or_z_mode, b_machine_has_variables). | |
751 | command_unavailable(operations_events,'only available for B,Z or Event-B models with OPERATIONS/events') :- | |
752 | \+ (b_or_z_mode, b_machine_has_operations). | |
753 | command_unavailable(b_mode,'only available for B,Z or Event-B models') :- \+ b_or_z_mode. |