1 % (c) 2016-2026 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_plantuml_command/1, is_plantuml_command/6,
18 call_plantuml_command/2, call_plantuml_command/3,
19 is_plantuml_command_for_expr/1,
20 call_plantuml_command_for_expr/3, call_plantuml_command_for_expr/4,
21 is_table_command/6, is_table_command/1, is_table_command_for_expr/1,
22 write_table_to_csv_file/2, write_table_to_csv_file/3, write_table_to_text_file/2]).
23
24 :- use_module(probsrc(module_information)).
25 :- module_info(group,visualization).
26 :- module_info(description,'This module provides access and description to a variety of Prolog commands.').
27
28 % the table command can be called from probcli via -csv
29 % e.g., probcli M.mch -csv wd_pos user_output
30
31 :- use_module(probsrc(error_manager)).
32 :- use_module(probsrc(debug)).
33 :- use_module(probsrc(tools_strings),[ajoin/2]).
34 :- use_module(probsrc(preferences),[get_preference/2, get_computed_preference/2]).
35 :- use_module(probsrc(specfile),[
36 b_or_z_mode/0,
37 eventb_mode/0,
38 csp_mode/0,
39 %csp_with_bz_mode/0,
40 spec_file_has_been_successfully_loaded/0]).
41 :- use_module(probsrc(state_space), [current_state_corresponds_to_fully_setup_b_machine/0, current_state_corresponds_to_setup_constants_b_machine/0]).
42
43 :- use_module(probsrc(bmachine),[b_machine_has_constants_or_properties/0, b_machine_has_assertions/0,
44 b_machine_has_constants/0, b_machine_has_variables/0,
45 b_machine_has_operations/0]).
46
47 % dot command with no arguments
48 is_dot_command(Command) :- command_category(Command,dot), command_arguments(Command,[dotfile]).
49 call_dot_command(Command,File) :- call_dot_command(Command,File,[]).
50 call_dot_command(Command,File,OptionalArgs) :- %print(cmd(Command,File,OptionalArgs)),nl,
51 call_command(dot,Command,[dotfile],[File],OptionalArgs).
52
53 % dot command with expr argument
54 is_dot_command_for_expr(Command) :-
55 command_category(Command,dot), command_arguments(Command,[expression_atom,dotfile]).
56 call_dot_command_for_expr(Command,Expr,File) :-
57 call_dot_command_for_expr(Command,Expr,File,[]).
58 call_dot_command_for_expr(Command,Expr,File,OptionalArgs) :- % print(cmd(Command,Expr,File,OptionalArgs)),nl,
59 call_command(dot,Command,[expression_atom,dotfile],[Expr,File],OptionalArgs).
60
61 % plantuml command with no arguments
62 is_plantuml_command(Command) :- command_category(Command,plantuml), command_arguments(Command,[plantumlfile]).
63 call_plantuml_command(Command,File) :- call_plantuml_command(Command,File,[]).
64 call_plantuml_command(Command,File,OptionalArgs) :-
65 plantuml_filename_extension_can_be_converted(File,Ext,UmlFile),
66 !, % we can convert a plantuml file to this format
67 call_plantuml_command(Command,UmlFile,OptionalArgs),
68 gen_plantuml_output([UmlFile],Ext,File).
69 call_plantuml_command(Command,File,OptionalArgs) :-
70 split_filename(File,FileRoot,Ext),
71 (Ext \= puml
72 -> add_warning(get_puml_output,'Unsupported file extension for PlantUML output, create .puml file: ',Ext),
73 ajoin([FileRoot,'.puml'],PumlFile)
74 ; PumlFile = File),
75 call_command(plantuml,Command,[plantumlfile],[PumlFile],OptionalArgs).
76
77 % plantuml command with expr argument
78 is_plantuml_command_for_expr(Command) :-
79 command_category(Command,plantuml), command_arguments(Command,[expression_atom,plantumlfile]).
80 call_plantuml_command_for_expr(Command,Expr,File) :-
81 plantuml_filename_extension_can_be_converted(File,Ext,UmlFile),
82 !, % we can convert a plantuml file to this format
83 call_plantuml_command_for_expr(Command,Expr,File,[]),
84 gen_plantuml_output([UmlFile],Ext,File).
85 call_plantuml_command_for_expr(Command,Expr,File,OptionalArgs) :-
86 call_command(plantuml,Command,[expression_atom,plantumlfile],[Expr,File],OptionalArgs).
87
88
89 :- use_module(probsrc(tools_commands),[gen_dot_output/4, gen_plantuml_output/3, valid_dot_output_format/1, valid_plantuml_output_format/1]).
90 :- use_module(probsrc(tools),[split_filename/3]).
91 :- use_module(probsrc(tools_strings),[ajoin/2]).
92
93 % call dot_command and dot engine if necessary
94 call_dot_command_with_engine(Command,File,OptionalArgs,DotEngine) :-
95 dot_filename_extension_can_be_converted(File,Ext,DotFile),
96 !, % we can convert a dot file to this format
97 call_dot_command(Command,DotFile,OptionalArgs),
98 % DotEngine = default, sfdp, circo, ...
99 gen_dot_output(DotFile,DotEngine,Ext,File).
100 call_dot_command_with_engine(Command,File,OptionalArgs,_) :-
101 call_dot_command(Command,File,OptionalArgs).
102
103 % call dot_command and dot engine if necessary
104 call_dot_command_with_engine_for_expr(Command,Expr,File,OptionalArgs,DotEngine) :-
105 dot_filename_extension_can_be_converted(File,Ext,DotFile),
106 !, % we can convert a dot file to this format
107 call_dot_command_for_expr(Command,Expr,DotFile,OptionalArgs),
108 gen_dot_output(DotFile,DotEngine,Ext,File).
109 call_dot_command_with_engine_for_expr(Command,Expr,File,OptionalArgs,_) :-
110 call_dot_command_for_expr(Command,Expr,File,OptionalArgs).
111
112 dot_filename_extension_can_be_converted(File,Ext,DotFile) :-
113 split_filename(File,FileRoot,Ext), Ext \= dot,
114 valid_dot_output_format(Ext),!, % we can convert a dot file to this format
115 ajoin([FileRoot,'.dot'],DotFile). % TODO: we could generate a temp file in /tmp
116
117 plantuml_filename_extension_can_be_converted(File,Ext,DotFile) :-
118 split_filename(File,FileRoot,Ext), Ext \= puml,
119 valid_plantuml_output_format(Ext),!, % we can convert a plantuml file to this format
120 ajoin([FileRoot,'.puml'],DotFile). % TODO: we could generate a temp file in /tmp
121
122 % TODO: maybe automatically call dot -Tpdf <F.dot >F.pdf for pdf, svg or similar file endings
123
124 % dot commands with no or with extra arguments:
125 % find out which dot commands are available and what arguments and preferences they take:
126 is_dot_command(Command,Name,Description,NumberOfFormulaArgs,Preferences,AdditionalInfo) :-
127 command_description(Command,Name,Description), % move forward to ensure ordering of found commands is same as in file
128 (is_dot_command(Command),NumberOfFormulaArgs=0 ;
129 is_dot_command_for_expr(Command),NumberOfFormulaArgs=1),
130 get_command_preferences(Command, Preferences),
131 findall(Info, command_additional_info(Command, Info), AdditionalInfo).
132
133 % find out which plantuml commands are available and what arguments and preferences they take:
134 is_plantuml_command(Command,Name,Description,NumberOfFormulaArgs,Preferences,AdditionalInfo) :-
135 command_description(Command,Name,Description), % move forward to ensure ordering of found commands is same as in file
136 (is_plantuml_command(Command),NumberOfFormulaArgs=0 ;
137 is_plantuml_command_for_expr(Command),NumberOfFormulaArgs=1),
138 get_command_preferences(Command, Preferences),
139 findall(Info, command_additional_info(Command, Info), AdditionalInfo).
140
141 :- use_module(library(lists)).
142 % table commands (return as last argument list of lists)
143 is_table_command(Command,Name,Description,NumberOfFormulaArgs,Preferences,AdditionalInfo) :-
144 command_category(Command,table),
145 command_arguments(Command,Args), last(Args,table_result),
146 length(Args,Len), NumberOfFormulaArgs is Len - 1,
147 command_description(Command,Name,Description),
148 get_command_preferences(Command, Preferences),
149 findall(Info, command_additional_info(Command, Info), AdditionalInfo).
150
151 is_table_command(Command) :-
152 is_table_command(Command,_,_,0,_,_).
153 is_table_command_for_expr(Command) :-
154 command_category(Command,table), command_arguments(Command,[expression_atom,table_result]).
155
156
157 % ---------------------------------------
158
159 :- use_module(probsrc(tools_io),[safe_intelligent_open_file/3]).
160 % write result of a table command to a CSV file, user_output prints to console w/o CSV seperators
161
162
163 write_table_to_csv_file(CSVFile,Table) :-
164 write_table_to_csv_file(CSVFile,[],Table).
165
166 write_table_to_text_file(TextFile,Table) :-
167 write_table_to_csv_file(TextFile,[text_output],Table).
168
169 write_table_to_csv_file(CSVFile,Opts,Table) :-
170 (CSVFile=user_output ;
171 member(text_output,Opts)),
172 !, % use textual output on user_output
173 Options = [csv_separator(' '),no_quoting|Opts],
174 safe_intelligent_open_file(CSVFile,write,Stream),
175 call_cleanup(write_table_to_csv_stream(Stream,Options,Table), close(Stream)).
176 write_table_to_csv_file(CSVFile,Options,Table) :-
177 safe_intelligent_open_file(CSVFile,write,Stream),
178 call_cleanup(write_table_to_csv_stream(Stream,Options,Table), close(Stream)).
179
180
181 % write result of a table command to a CSV stream
182 write_table_to_csv_stream(Stream,Options,list(L)) :- !,
183 write_table_to_csv_stream(Stream,Options,L).
184 write_table_to_csv_stream(_Stream,_,[]) :- !.
185 write_table_to_csv_stream(Stream,Options,[H|T]) :- !, write_row(H,Options,Stream), nl(Stream),
186 write_table_to_csv_stream(Stream,Options,T).
187 write_table_to_csv_stream(Stream,Options,Other) :- write(Stream,Other),nl(Stream),
188 add_internal_error('Table is not a list: ',write_table_to_csv_stream(Stream,Options,Other)).
189
190 write_row([],_,_) :- !.
191 write_row(list(L),Options,Stream) :- !, write_row(L,Options,Stream).
192 write_row([H],Options,Stream) :- !, write_value(H,Options,Stream).
193 write_row([H|T],Options,Stream) :- !, write_value(H,Options,Stream), write_sep(Options,Stream),
194 write_row(T,Options,Stream).
195 write_row(Other,Options,Stream) :- write(Stream,Other),nl(Stream),
196 add_internal_error('Table row is not a list: ',write_table_to_csv_stream(Stream,Options,Other)).
197
198 ?write_sep(Options,Stream) :- member(csv_separator(Sep),Options), !, write(Stream,Sep).
199 write_sep(_,Stream) :- write(Stream,',').
200
201 write_value(Nr,_,Stream) :- number(Nr), !, write(Stream,Nr).
202 ?write_value(Val,Options,Stream) :- member(no_quoting,Options), !, write(Stream,Val).
203 write_value(Atom,_,Stream) :- atom(Atom), atom_codes(Atom,AC),!,
204 csv_escape_codes(AC,EC),
205 format(Stream,'"~s"',[EC]). % quote for CSV
206 write_value(Other,_,Stream) :- format(Stream,'"~w"',[Other]).
207
208 csv_escape_codes([],[]).
209 csv_escape_codes([0'" | T],R) :- !,
210 R=[0'", 0'" |ET], % quotes in a CSV record must be preceded by another quote
211 csv_escape_codes(T,ET).
212 csv_escape_codes([H|T],[H|ET]) :- csv_escape_codes(T,ET).
213
214 % ---------------------------------------
215
216 % call a command described in this module
217 call_command(Category,Command,FormalArgs,ActualArgs,OptionalArgs) :-
218 command_category(Command,Category),
219 command_arguments(Command,FormalArgs), % to do: more flexible matching of args ?
220 !,
221 (command_unavailable(Command,Msg)
222 -> ajoin(['Command ', Command, ' not available: '],Msg1),
223 add_error(meta_interface,Msg1,Msg),
224 fail
225 ; setup_optional_args(Command,OptionalArgs,OptArgValueList),
226 (command_call(Command,ActualArgs,OptArgValueList,Call)
227 -> debug_println(4,command_call(Call)),
228 ? call(Call)
229 ; command_call(Command,ArgsExpected,_,_),length(ArgsExpected,Exp),length(ActualArgs,Form) %, Exp \= Form
230 ->
231 ajoin(['Command ', Command, ' expects ', Exp, ' arguments, but obtained ',Form,'!'],Msg1),
232 add_internal_error(Msg1,command_call(Command,ActualArgs,OptArgValueList,_)),
233 fail
234 ; add_internal_error('Cannot construct command call: ',command_call(Command,ActualArgs,OptArgValueList,_)),
235 fail
236 )
237 ).
238 call_command(Category,Command,FormalArgs,_ActualArgs,_OptArgs) :- command_category(Command,Category),
239 !,
240 add_error(meta_interface,'Argument mis-match when calling command: ',Command:FormalArgs),fail.
241 call_command(Category,Command,_,_,_) :- command_category(Command,_OtherCategory),!,
242 add_error(meta_interface,'Command belongs to other category: ',Category:Command),fail.
243 call_command(Category,Command,_,_,_) :-
244 add_error(meta_interface,'Unknown command: ',Category:Command),fail.
245
246
247 setup_optional_args(Command,OptionalArgs,OptArgValueList) :-
248 command_optional_arguments(Command,Names,_Types,DefaultValues),!,
249 setup_opt_args_aux(Names,DefaultValues,OptionalArgs,Command,OptArgValueList).
250 setup_optional_args(_,[],Res) :- !, Res=[].
251 setup_optional_args(Cmd,Opt,Res) :- add_internal_error('Illegal optional arguments: ',setup_optional_args(Cmd,Opt,Res)),
252 Res=[].
253
254 :- use_module(library(lists),[select/3]).
255
256 setup_opt_args_aux([],[],OptArgs,Command,Res) :-
257 (OptArgs = [] -> true ; add_internal_error('Too many optional arguments: ',Command:OptArgs)),
258 Res = [].
259 setup_opt_args_aux([Name|NT],[Default|DT],OptArgs,Command,Res) :-
260 (select('='(Name,Value),OptArgs,OA2)
261 -> Res = [Value|RT], setup_opt_args_aux(NT,DT,OA2,Command,RT)
262 ; Res = [Default|RT], setup_opt_args_aux(NT,DT,OptArgs,Command,RT)
263 ).
264
265
266 % TO DO: provide automatic conversion ? expression_atom -> expression_codes -> typed_expression ?
267
268 :- use_module(probsrc(preferences),[virtual_preference_category/2]).
269 % get all preferences for a command
270 get_command_preferences(Command,Preferences) :-
271 findall(Pref, (command_preferences_category(Command,PrefCat),
272 virtual_preference_category(Pref,PrefCat)), Preferences).
273
274 % --------------------
275 % COMMAND DESCRIPTIONS
276 % --------------------
277
278 :- discontiguous command_description/3, command_call/4,
279 command_unavailable/2, command_arguments/2,
280 command_optional_arguments/4,
281 command_category/2, command_preferences_category/2,
282 command_additional_info/2.
283
284 :- use_module(probsrc(b_machine_hierarchy),[write_dot_event_hierarchy_to_file/1,write_dot_variable_hierarchy_to_file/1,
285 write_dot_hierarchy_to_file/1]).
286
287 command_description(machine_hierarchy,'Machine Hierarchy','Shows the machine hierarchy of a classical B model').
288 command_call(machine_hierarchy,[File],[],b_machine_hierarchy:write_dot_hierarchy_to_file(File)).
289 command_unavailable(machine_hierarchy,Txt) :- command_unavailable(b_mode,Txt).
290 command_arguments(machine_hierarchy,[dotfile]).
291 command_category(machine_hierarchy,dot).
292 command_preferences_category(machine_hierarchy,dot_machine_hierarchy).
293 command_additional_info(machine_hierarchy,group(machine_info)).
294
295 command_description(operations,'Operation Call Graph','Shows the call graph of a classical B model').
296 command_call(operations,[File],[],b_machine_hierarchy:write_dot_op_hierarchy_to_file(File)).
297 command_unavailable(operations,'only available for B or Z models with OPERATIONS') :-
298 (\+ (b_or_z_mode,b_machine_has_operations) ; eventb_mode).
299 command_arguments(operations,[dotfile]).
300 command_category(operations,dot).
301 command_preferences_category(operations,dot_graph_generator).
302 command_additional_info(operations,group(machine_info)).
303
304 command_description(event_hierarchy,'Event Hierarchy','Shows the event hierarchy of an Event-B model').
305 command_call(event_hierarchy,[File],[],b_machine_hierarchy:write_dot_event_hierarchy_to_file(File)).
306 command_unavailable(event_hierarchy,'only available for Event-B models with events') :-
307 \+ (eventb_mode, b_machine_has_operations).
308 command_arguments(event_hierarchy,[dotfile]).
309 command_category(event_hierarchy,dot).
310 command_preferences_category(event_hierarchy,dot_event_hierarchy).
311 command_additional_info(event_hierarchy,group(machine_info)).
312
313 command_description(variable_hierarchy,'Variable Refinement Hierarchy','Shows variables within the refinement hierarchy of an Event-B model').
314 command_call(variable_hierarchy,[File],[],b_machine_hierarchy:write_dot_variable_hierarchy_to_file(File)).
315 command_unavailable(variable_hierarchy,'only available for Event-B models with variables') :-
316 \+ (eventb_mode, b_machine_has_variables).
317 command_arguments(variable_hierarchy,[dotfile]).
318 command_category(variable_hierarchy,dot).
319 command_preferences_category(variable_hierarchy,dot_variable_hierarchy).
320 command_additional_info(variable_hierarchy,group(machine_info)).
321
322
323 :- use_module(dotsrc(visualize_graph),[tcltk_print_states_for_dot/2]).
324 command_description(state_space,'State Space','Show state space').
325 command_call(state_space,[File],[ColourTransitions],visualize_graph:tcltk_print_states_for_dot(File,ColourTransitions)).
326 command_unavailable(state_space,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded.
327 command_arguments(state_space,[dotfile]).
328 command_optional_arguments(state_space,[colouring],[atom],[no_colour_for_transitions]).
329 command_category(state_space,dot).
330 command_preferences_category(state_space,dot_state_space).
331 command_additional_info(state_space,group(state_space_visualisation)).
332
333 command_description(state_space_sfdp,'State Space (Fast)','Show state space (faster layout with less information and more overlaps)').
334 command_call(state_space_sfdp,[File],[ColourTransitions],visualize_graph:tcltk_print_states_for_dot_sfdp(File,ColourTransitions)).
335 command_unavailable(state_space_sfdp,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded.
336 command_arguments(state_space_sfdp,[dotfile]).
337 command_optional_arguments(state_space_sfdp,[colouring],[atom],[no_colour_for_transitions]).
338 command_category(state_space_sfdp,dot).
339 command_preferences_category(state_space_sfdp,dot_state_space). % TODO: maybe remove those that are fixed and have no effect
340 command_additional_info(state_space_sfdp,preferred_dot_type(sfdp)). % sfdp preferred
341 command_additional_info(state_space_sfdp,extra_arguments(['-Goverlap=scale'])). % other option is prism
342 command_additional_info(state_space_sfdp,group(state_space_visualisation)).
343
344 :- use_module(dotsrc(visualize_graph),[tcltk_print_current_state_for_dot/1]).
345 command_description(current_state,'Current State in State Space','Show current state and successors in state space').
346 command_call(current_state,[File],[],visualize_graph:tcltk_print_current_state_for_dot(File)).
347 command_unavailable(current_state,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded.
348 command_arguments(current_state,[dotfile]).
349 command_category(current_state,dot).
350 command_preferences_category(current_state,dot_state_space).
351 command_additional_info(current_state,group(state_space_visualisation)).
352
353 :- use_module(dotsrc(visualize_graph),[tcltk_print_history_to_current_state_for_dot/1]).
354 command_description(history,'Path to Current State','Show a path leading to current state').
355 % in ProB2-UI the Tcl/Tk history is not the ProB2 history !!!
356 command_call(history,[File],[],visualize_graph:tcltk_print_history_to_current_state_for_dot(File)).
357 command_unavailable(history,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded.
358 command_arguments(history,[dotfile]).
359 command_category(history,dot).
360 command_preferences_category(history,dot_state_space).
361 command_additional_info(history,group(trace_visualisation)).
362
363 %:- use_module(dotsrc(visualize_graph),[tcltk_print_history_to_current_state_with_neighbors_for_dot/1]).
364 %command_description(history_with_neighbours,'History of States (with Neighbours for last State)','Show history with neighbours leading to current state').
365 %command_call(history_with_neighbours,[File],[],visualize_graph:tcltk_print_history_to_current_state_with_neighbors_for_dot(File)).
366 %command_unavailable(history_with_neighbours,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded.
367 %command_arguments(history_with_neighbours,[dotfile]).
368 %command_category(history_with_neighbours,dot).
369 %command_preferences_category(history_with_neighbours,dot_state_space).
370
371 :- use_module(dotsrc(state_space_reduction),[write_transition_diagram_for_expr_to_dotfile/2,
372 write_signature_merge_to_dotfile/2]).
373 command_description(signature_merge,'Signature Merge','Show signature-merged reduced state space (i.e., merge states which have same set of enabled events/operations)').
374 command_call(signature_merge,[File],[IgnoredEvents],state_space_reduction:write_signature_merge_to_dotfile(IgnoredEvents,File)).
375 command_unavailable(signature_merge,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded.
376 command_arguments(signature_merge,[dotfile]).
377 command_optional_arguments(signature_merge,[ignored_events],[list(operations)],[[]]).
378 command_category(signature_merge,dot).
379 command_preferences_category(signature_merge,dot_graph_generator).
380 command_additional_info(signature_merge,group(state_space_visualisation)).
381
382
383 :- use_module(dotsrc(reduce_graph_state_space),[print_dot_for_dfa_from_nfa/1]).
384 command_description(dfa_merge,'DFA Merge','Show state space as deterministic automaton (DFA)').
385 command_call(dfa_merge,[File],[],reduce_graph_state_space:print_dot_for_dfa_from_nfa(File)).
386 command_unavailable(dfa_merge,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded.
387 command_arguments(dfa_merge,[dotfile]).
388 command_category(dfa_merge,dot).
389 command_additional_info(dfa_merge,group(state_space_visualisation)).
390
391 :- use_module(dotsrc(state_space_reduction),[write_transition_diagram_for_expr_to_dotfile/2]).
392 command_description(transition_diagram,'State Space Expression Projection...','Project state space onto expression values and show transition diagram').
393 command_call(transition_diagram,[Expression,File],[],
394 state_space_reduction:write_transition_diagram_for_expr_to_dotfile(Expression,File)).
395 command_unavailable(transition_diagram,Txt) :- command_unavailable(b_mode,Txt).
396 command_arguments(transition_diagram,[expression_atom,dotfile]). % also accepts expression_raw_ast
397 command_category(transition_diagram,dot).
398 command_preferences_category(transition_diagram,dot_projection).
399 command_additional_info(transition_diagram,group(state_space_visualisation)).
400
401 :- use_module(probporsrc(dot_graphs_static_analysis), [tcltk_create_dependence_graph/1, tcltk_create_enable_graph/1]).
402 command_description(enable_graph,'Event Enable Graph','Show enabling graph of events (i.e., which event/operation can enable/disable which other event)').
403 command_call(enable_graph,[File],[],dot_graphs_static_analysis:tcltk_create_enable_graph(File)).
404 command_unavailable(enable_graph,Txt) :- command_unavailable(operations_events,Txt).
405 command_arguments(enable_graph,[dotfile]).
406 command_category(enable_graph,dot).
407 command_preferences_category(enable_graph,dot_enable_graph).
408 command_additional_info(enable_graph,group(data_flow_info)).
409
410 :- use_module(dotsrc(state_as_dot_graph),[print_cstate_graph/1]).
411 command_description(state_as_graph,'Current State as Graph','Show values of variables in current state as one graph').
412 command_call(state_as_graph,[File],[],state_as_dot_graph:print_cstate_graph(File)).
413 %command_call(state_as_graph,[File],[],visualize_graph:tcltk_print_current_state_as_graph_for_dot(File)).
414 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.
415 command_arguments(state_as_graph,[dotfile]).
416 command_category(state_as_graph,dot).
417 command_preferences_category(state_as_graph,state_as_graph).
418 % we could use tcltk_print_current_state_as_graph_for_dot
419 command_additional_info(state_as_graph,group(state_visualisation)).
420
421 :- use_module(dotsrc(state_custom_dot_graph),
422 [tcltk_generate_state_custom_dot_graph/1,state_custom_dot_graph_available/0]).
423
424 command_description(custom_graph,'Customized Current State as Graph','Show values in current state as a graph using CUSTOM_GRAPH definition').
425 command_call(custom_graph,[File],[],state_custom_dot_graph:tcltk_generate_state_custom_dot_graph(File)).
426 command_unavailable(custom_graph,'only available when CUSTOM_GRAPH or CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine') :-
427 ? \+ state_custom_dot_graph_available.
428 command_unavailable(custom_graph,'only available for initialised B,Z or Event-B models') :-
429 ? state_custom_dot_graph_available,
430 \+ current_state_corresponds_to_fully_setup_b_machine.
431 command_arguments(custom_graph,[dotfile]). % also accepts expression_raw_ast
432 command_category(custom_graph,dot).
433 command_preferences_category(custom_graph,dot_graph_generator).
434 command_additional_info(custom_graph,group(state_visualisation)).
435
436 :- use_module(rulesdslsrc(rule_validation), [generate_dependency_graph/1]).
437 :- use_module(probsrc(specfile), [animation_minor_mode/1]).
438 command_description(rule_dependency_graph,'Rule Dependency Graph','Show dependencies of rules and computations of a rules machine').
439 command_call(rule_dependency_graph,[File],[],generate_dependency_graph(File)).
440 command_unavailable(rule_dependency_graph,'only available for rules machines (.rmch)') :-
441 \+ animation_minor_mode(rules_dsl).
442 command_unavailable(rule_dependency_graph,'only available for initialised rules machine') :-
443 animation_minor_mode(rules_dsl),
444 \+ current_state_corresponds_to_fully_setup_b_machine.
445 command_arguments(rule_dependency_graph,[dotfile]).
446 command_category(rule_dependency_graph,dot).
447 command_preferences_category(rule_dependency_graph,rule_dependency_graph).
448 command_preferences_category(rule_dependency_graph,dot_graph_generator).
449 command_additional_info(rule_dependency_graph,group(state_visualisation)).
450
451 :- use_module(seqproversrc(sequent_prover_exports), [export_proof_for_current_state/2]).
452 command_description(proof_tree_graph,'Proof Tree','Show sequent prover trace as proof tree.').
453 command_call(proof_tree_graph,[File],[],export_proof_for_current_state(dot,File)).
454 command_unavailable(proof_tree_graph,'only available in sequent prover mode (for .pl PO files)') :-
455 \+ animation_minor_mode(sequent_prover).
456 command_arguments(proof_tree_graph,[dotfile]).
457 command_category(proof_tree_graph,dot).
458 command_preferences_category(proof_tree_graph,dot_graph_generator).
459 command_additional_info(proof_tree_graph,group(trace_visualisation)).
460
461 % from tcltk_interface.pl:
462 command_description(expr_as_graph,'(Relational) Expression as Graph...','Show (relational) expression value as a graph').
463 command_call(expr_as_graph,[Expression,File],[],tcltk_interface:tcltk_show_expression_as_dot(Expression,File)).
464 command_unavailable(expr_as_graph,Txt) :- command_unavailable(b_mode,Txt).
465 command_arguments(expr_as_graph,[expression_atom,dotfile]). % also accepts expression_raw_ast
466 command_category(expr_as_graph,dot).
467 command_preferences_category(expr_as_graph,state_as_graph).
468 command_additional_info(expr_as_graph,group(formula_visualisation)).
469
470
471 command_description(formula_tree,'Custom Predicate/Expression Formula Tree...','Show predicate/expressions and sub-formulas as a tree').
472 command_call(formula_tree,[Expression,File],[],tcltk_interface:generate_dot_from_formula(Expression,File)).
473 command_unavailable(formula_tree,Txt) :- command_unavailable(b_mode,Txt).
474 command_arguments(formula_tree,[expression_atom,dotfile]). % is actually predicate_atom, also accepts expression_raw_ast
475 command_category(formula_tree,dot).
476 command_preferences_category(formula_tree,dot_formula_tree).
477 command_additional_info(formula_tree,group(formula_visualisation)).
478
479 command_description(invariant,'Invariant Formula Tree','Show invariant as a formula tree').
480 command_call(invariant,[File],[],tcltk_interface:generate_dot_from_invariant(File)).
481 command_unavailable(invariant,'only available for initialised B,Z or Event-B models') :- \+ current_state_corresponds_to_fully_setup_b_machine.
482 command_arguments(invariant,[dotfile]).
483 command_category(invariant,dot).
484 command_preferences_category(invariant,dot_formula_tree).
485 command_additional_info(invariant,group(formula_visualisation)).
486
487 command_description(properties,'Properties Formula Tree','Show properties/axioms as a formula tree').
488 command_call(properties,[File],[],tcltk_interface:generate_dot_from_properties(File)).
489 %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
490 command_unavailable(properties,'only available for B,Z or Event-B models with PROPERTIES after constant setup or initialisation') :-
491 \+ (current_state_corresponds_to_setup_constants_b_machine,b_machine_has_constants_or_properties).
492 command_arguments(properties,[dotfile]).
493 command_category(properties,dot).
494 command_preferences_category(properties,dot_formula_tree).
495 command_additional_info(properties,group(formula_visualisation)).
496
497 command_description(assertions,'Assertions Formula Tree','Show assertions/theorems as a formula tree').
498 command_call(assertions,[File],[],tcltk_interface:generate_dot_from_assertions(File)).
499 %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
500 command_unavailable(assertions,'only available for B,Z or Event-B models with ASSERTIONS after constant setup or initialisation') :-
501 \+ (current_state_corresponds_to_setup_constants_b_machine, b_machine_has_assertions).
502 command_arguments(assertions,[dotfile]).
503 command_category(assertions,dot).
504 command_preferences_category(assertions,dot_formula_tree).
505 command_additional_info(assertions,group(formula_visualisation)).
506
507 command_description(deadlock,'Deadlock Formula Tree','Show deadlocking status (i.e., guards of all operations/events) in current state as a formula tree').
508 command_call(deadlock,[File],[],tcltk_interface:generate_dot_from_deadlock_po(File)).
509 command_unavailable(deadlock,'only available for initialised B,Z or Event-B models with OPERATIONS') :-
510 \+ (current_state_corresponds_to_fully_setup_b_machine, b_machine_has_operations).
511 command_arguments(deadlock,[dotfile]).
512 command_category(deadlock,dot).
513 command_preferences_category(deadlock,dot_formula_tree).
514 command_additional_info(deadlock,group(formula_visualisation)).
515
516 :- use_module(probsrc(bmachine),[b_get_machine_goal/1]).
517 command_description(goal,'Goal Formula Tree','Show GOAL as a formula tree').
518 command_call(goal,[File],[],tcltk_interface:generate_dot_from_goal(File)).
519 command_unavailable(goal,'only available for initialised B,Z or Event-B models with a GOAL DEFINITION') :-
520 (\+ b_or_z_mode ; \+ b_get_machine_goal(_)).
521 command_arguments(goal,[dotfile]).
522 command_category(goal,dot).
523 command_preferences_category(goal,dot_formula_tree).
524 command_additional_info(goal,group(formula_visualisation)).
525
526 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
527 command_call(dependence_graph,[File],[],dot_graphs_static_analysis:tcltk_create_dependence_graph(File)).
528 command_unavailable(dependence_graph,Txt) :- command_unavailable(operations_events,Txt).
529 command_arguments(dependence_graph,[dotfile]).
530 command_category(dependence_graph,dot).
531 command_preferences_category(dependence_graph,dot_enable_graph).
532 command_additional_info(dependence_graph,group(data_flow_info)).
533
534 command_description(variable_modification_graph,'Variable Read/Write Graph','Show variable modification by operations and reading in guards').
535 command_call(variable_modification_graph,[File],[],b_read_write_info:tcltk_dot_variable_modification_analysis(File)).
536 command_unavailable(variable_modification_graph,Txt) :- command_unavailable(variables,Txt).
537 command_arguments(variable_modification_graph,[dotfile]).
538 command_category(variable_modification_graph,dot).
539 command_preferences_category(variable_modification_graph,dot_variable_modification).
540 command_additional_info(variable_modification_graph,group(data_flow_info)).
541
542 :- use_module(dotsrc(visualize_graph),[tcltk_print_definitions_as_graph_for_dot/1]).
543 command_description(definitions,'Definitions Graph','Show dependency graph of DEFINITIONS').
544 command_call(definitions,[File],[],visualize_graph:tcltk_print_definitions_as_graph_for_dot(File)).
545 command_unavailable(definitions,'only available for B or Z models') :- (b_or_z_mode -> eventb_mode ; true).
546 command_arguments(definitions,[dotfile]).
547 command_category(definitions,dot).
548 command_preferences_category(definitions,dot_definitions).
549 command_additional_info(definitions,group(debug_info)).
550
551 :- use_module(dotsrc(visualize_graph),[tcltk_print_predicate_dependency_as_graph_for_dot/2]).
552 command_description(predicate_dependency,'Predicate Dependency Graph...','Show dependency graph of conjuncts of a predicate').
553 command_call(predicate_dependency,[Pred,File],[],visualize_graph:tcltk_print_predicate_dependency_as_graph_for_dot(Pred,File)).
554 command_unavailable(predicate_dependency,Txt) :- command_unavailable(b_mode,Txt).
555 command_arguments(predicate_dependency,[expression_atom,dotfile]). % also accepts expression_raw_ast
556 command_category(predicate_dependency,dot).
557 command_additional_info(predicate_dependency,group(debug_info)).
558
559 command_description(last_error,'Last State Error Formula Tree','Try and visualise last state error source as a formula tree').
560 command_call(last_error,[File],[],tcltk_interface:generate_dot_from_last_span_predicate(File)).
561 command_unavailable(last_error,'only available when (state) error occured') :-
562 \+ tcltk_interface:can_generate_dot_from_last_state_error.
563 command_arguments(last_error,[dotfile]).
564 command_category(last_error,dot).
565 command_additional_info(last_error,group(formula_visualisation)).
566
567 command_description(last_mcts_tree,'MCTS Game Tree','Show two levels of last MCTS (Monte Carlo Tree Search) game tree').
568 command_call(last_mcts_tree,[File],[],mcts_game_play:tcltk_gen_last_mcts_tree(2,File)).
569 command_unavailable(last_mcts_tree,'only available when GAME_OVER, ... definitions generated') :- \+ mcts_game_play:mcts_auto_play_available.
570 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.
571 command_arguments(last_mcts_tree,[dotfile]).
572 command_category(last_mcts_tree,dot).
573 command_additional_info(last_mcts_tree,group(formula_visualisation)).
574
575 %command_description(constants_profile_graph,'ProB Constants Profile Graph','Show constants computed by equations and order of computation').
576 %command_call(constants_profile_graph,[File],[],runtime_profiler:tcltk_dot_constants_profile_info(File)).
577 %command_unavailable(constants_profile_graph,Txt) :- command_unavailable(prob_constants_profile_info,Txt).
578 %command_arguments(constants_profile_graph,[dotfile]).
579 %command_category(constants_profile_graph,dot).
580 %%command_preferences_category(constants_profile_graph,...).
581 %command_additional_info(constants_profile_graph,group(debug_info)).
582
583 % -----------------------------------------
584
585 % PLANTUML COMMANDS:
586
587 :- use_module(dotsrc(uml_generator),[write_uml_sequence_chart/1]).
588 command_description(uml_sequence_chart,'UML Sequence Chart','Visualise the current trace as a UML sequence chart.').
589 command_call(uml_sequence_chart,[File],[],write_uml_sequence_chart(File)).
590 command_unavailable(uml_sequence_chart,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded.
591 %command_unavailable(uml_sequence_chart,'only available when SEQUENCE_CHART definitions are defined in the DEFINITIONS of a B machine') :-
592 % \+ bmachine:b_definition_prefixed(expression,'SEQUENCE_CHART',_,_,_). % no such def exists
593 command_arguments(uml_sequence_chart,[plantumlfile]).
594 command_category(uml_sequence_chart,plantuml).
595 command_additional_info(uml_sequence_chart,group(trace_visualisation)).
596
597 % -----------------------------------------
598
599 % TABLE COMMANDS:
600
601
602 command_description(machine_statistics,'Machine Statistics','Show statistics for main machine/specification').
603 command_call(machine_statistics,[Result],[],meta_interface:meta_get_machine_stats(Result)).
604 command_unavailable(machine_statistics,Txt) :- command_unavailable(b_mode,Txt).
605 command_arguments(machine_statistics,[table_result]).
606 command_category(machine_statistics,table).
607 command_additional_info(machine_statistics,group(machine_info)).
608
609 :- use_module(probsrc(bmachine),[b_machine_statistics/2]).
610 :- public meta_get_machine_stats/1.
611 meta_get_machine_stats(list([list(['Key','Nr'])|L])) :- findall(list([Key,Nr]),b_machine_statistics(Key,Nr),L).
612
613 command_description(expr_as_table,'Expression Table...','Show expression value as a table').
614 command_call(expr_as_table,[Expression,Result],[],tcltk_interface:tcltk_eval_as_table(Expression,Result)).
615 command_unavailable(expr_as_table,Txt) :- command_unavailable(b_mode,Txt).
616 command_arguments(expr_as_table,[expression_atom,table_result]). % also accepts expression_raw_ast
617 command_category(expr_as_table,table).
618 command_additional_info(expr_as_table,group(formula_visualisation)).
619
620 :- use_module(probsrc(tcltk_interface),[tcltk_operations_covered_info/3]).
621
622 command_description(quick_operation_coverage,'Operation Coverage','Show which operations are covered in current state space').
623 command_call(quick_operation_coverage,[Result],[],tcltk_interface:tcltk_operations_covered_info(Result,_,quick)).
624 command_unavailable(quick_operation_coverage,'only available for B,Z, Event-B with OPERATIONS, or CSP models') :-
625 \+ (b_or_z_mode, b_machine_has_operations), \+ csp_mode.
626 command_arguments(quick_operation_coverage,[table_result]). % also accepts expression_raw_ast
627 command_category(quick_operation_coverage,table).
628 command_additional_info(quick_operation_coverage,group(coverage_info)).
629
630 command_description(precise_operation_coverage,'Operation Coverage and Feasibility','Show which feasible operations are covered (possible means operation is in principle feasible given invariant)').
631 command_call(precise_operation_coverage,[Result],[],tcltk_interface:tcltk_operations_covered_info(Result,_,precise)).
632 command_unavailable(precise_operation_coverage,Txt) :- command_unavailable(operations_events,Txt).
633 command_arguments(precise_operation_coverage,[table_result]). % also accepts expression_raw_ast
634 command_category(precise_operation_coverage,table).
635 command_additional_info(precise_operation_coverage,group(coverage_info)).
636
637 % not really useful for ProB2: already in Statistics View when more details shown:
638 %command_description(operation_coverage_stats,'Operation Coverage Statistics','Show operation coverage statistics').
639 %command_call(operation_coverage_stats,[Result],[],meta_interface:get_operation_coverage_stats(Result)).
640 %command_arguments(operation_coverage_stats,[table_result]).
641 %command_category(operation_coverage_stats,table).
642 %:- use_module(extrasrc(coverage_statistics),[tcltk_compute_coverage/1]).
643 %get_operation_coverage_stats(list([list(['Info'])|LRes])) :-
644 % tcltk_compute_coverage(list(Res)),
645 % maplist(wrap_into_list,Res,LRes).
646
647
648 command_description(show_typing,'Show Typing','Show types for variables and constants').
649 command_call(show_typing,[Result],[],meta_interface:show_typing_table(Result)).
650 command_unavailable(show_typing,Txt) :- command_unavailable(b_mode,Txt).
651 command_arguments(show_typing,[table_result]). % also accepts expression_raw_ast
652 command_category(show_typing,table).
653 :- public show_typing_table/1.
654 show_typing_table(list([list(['Typing'])|LRes])) :- tcltk_interface:tcltk_show_typing_of_variables_and_constants(list(Res)),
655 maplist(wrap_into_list,Res,LRes).
656 command_additional_info(show_typing,group(machine_info)).
657
658 command_description(variable_coverage,'Variable Coverage','Show number of distinct covered values for variables in current state space').
659 command_call(variable_coverage,[Result],[],state_space_reduction:tcltk_compute_nr_covered_values_for_all_variables(Result)).
660 command_unavailable(variable_coverage,Txt) :- command_unavailable(variables,Txt).
661 command_arguments(variable_coverage,[table_result]). % also accepts expression_raw_ast
662 command_category(variable_coverage,table).
663 command_additional_info(variable_coverage,group(coverage_info)).
664
665 command_description(constants_coverage,'Constant Coverage','Show number of distinct covered values for constants in current state space').
666 command_call(constants_coverage,[Result],[],state_space_reduction:tcltk_compute_nr_covered_values_for_all_constants(Result)).
667 command_unavailable(constants_coverage,Txt) :- command_unavailable(constants,Txt).
668 command_arguments(constants_coverage,[table_result]).
669 command_category(constants_coverage,table).
670 command_additional_info(constants_coverage,group(coverage_info)).
671
672 % analyze_constants
673 command_description(constants_analysis,'Constant Analysis','Show size (B and Prolog term size) and other infos about constants').
674 command_call(constants_analysis,[Result],[],coverage_statistics:tcltk_analyse_constants(Result)).
675 command_unavailable(constants_analysis,Txt) :- command_unavailable(constants,Txt).
676 command_arguments(constants_analysis,[table_result]).
677 command_category(constants_analysis,table).
678 command_additional_info(constants_analysis,group(debug_info)).
679
680 command_description(expression_coverage,'Expression Coverage...','Evaluate expression over current state space and compute distinct values and their number of occurence').
681 command_call(expression_coverage,[Expr,Result],[],meta_interface:expression_coverage(Expr,Result)).
682 command_unavailable(expression_coverage,Txt) :- command_unavailable(b_mode,Txt).
683 command_arguments(expression_coverage,[expression_atom,table_result]).
684 command_category(expression_coverage,table).
685 command_additional_info(expression_coverage,group(coverage_info)).
686
687 :- public expression_coverage/2.
688 :- use_module(dotsrc(state_space_reduction),[compute_covered_values_for_expression/4]).
689 expression_coverage(ExprToEvaluate,list(LRes)) :-
690 compute_covered_values_for_expression(ExprToEvaluate,_MaxTypeCard,_TotalNrOfValuesFound,list(Res)),
691 maplist(wrap_into_list,Res,LRes).
692
693 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').
694 command_call(minmax_table,[Result],[],meta_interface:minmax_table(Result)).
695 command_unavailable(minmax_table,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded.
696 command_arguments(minmax_table,[table_result]).
697 command_category(minmax_table,table).
698 command_additional_info(minmax_table,group(coverage_info)).
699 :- use_module(extrasrc(coverage_statistics),[tcltk_compute_min_max/1]).
700 :- public minmax_table/1.
701 minmax_table(R) :- tcltk_compute_min_max(R).
702
703 command_description(inv_coverage,'Invariant Analysis','Analyse the truth value of individual invariants in current state space').
704 command_call(inv_coverage,[Result],[],mcdc_coverage:tcltk_get_invariant_coverage(Result)).
705 command_unavailable(inv_coverage,Txt) :- command_unavailable(b_mode,Txt).
706 command_arguments(inv_coverage,[table_result]).
707 command_category(inv_coverage,table).
708 command_additional_info(inv_coverage,group(coverage_info)).
709
710 command_description(vacuous_invariants,'Vacuous Invariants','Show list of vacuous invariants (i.e., implications or disjunctions wich are useless, given current explicit state space)').
711 command_call(vacuous_invariants,[Result],[],meta_interface:vacuous_invariants(Result)).
712 command_unavailable(vacuous_invariants,Txt) :- command_unavailable(b_mode,Txt).
713 command_arguments(vacuous_invariants,[table_result]).
714 command_category(vacuous_invariants,table).
715 :- public vacuous_invariants/1.
716 vacuous_invariants(Res) :-
717 tcltk_interface:tcltk_get_vacuous_invariants_table(Res).
718 command_additional_info(vacuous_invariants,group(coverage_info)).
719
720 command_description(specialized_invariants,'Specialized Invariants','Show list of invariants (specialized using proof information for each operation; used by ProB for faster model checking)').
721 command_call(specialized_invariants,[Result],[],meta_interface:specialized_invariants(Result)).
722 command_unavailable(specialized_invariants,Txt) :- command_unavailable(b_mode,Txt).
723 command_arguments(specialized_invariants,[table_result]).
724 command_category(specialized_invariants,table).
725 command_additional_info(specialized_invariants,group(debug_info)).
726 :- public specialized_invariants/1.
727 specialized_invariants(list([list(['Operation','Unproven','Predicate'])|LRes])) :-
728 bmachine:tcltk_get_specialized_invariants_for_ops(list(Res)),
729 maplist(wrap_into_list,Res,LRes).
730
731 wrap_into_list(list(L),R) :- !, R=list(L).
732 wrap_into_list([],R) :- !, R=list([]).
733 wrap_into_list([H|T],R) :- !, R=list([H|T]).
734 wrap_into_list(X,list([X])).
735
736 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)').
737 command_call(vacuous_guards,[Result],[],meta_interface:vacuous_guards(Result)).
738 command_unavailable(vacuous_guards,Txt) :- command_unavailable(operations_events,Txt).
739 command_arguments(vacuous_guards,[table_result]).
740 command_category(vacuous_guards,table).
741 command_additional_info(vacuous_guards,group(coverage_info)).
742 :- public vacuous_guards/1.
743 vacuous_guards(list([list(['Vacuous Guards'])|LRes])) :-
744 tcltk_interface:tcltk_get_vacuous_guards(list(Res)),
745 maplist(wrap_into_list,Res,LRes).
746
747 :- use_module(extrasrc(mcdc_coverage),[tcltk_get_invariant_coverage/1,
748 tcltk_compute_mcdc_operation_coverage/1,
749 tcltk_compute_mcdc_invariant_coverage/1]).
750
751
752
753
754 command_description(read_write_matrix,'Operation Read/Write Matrix','Show identifiers read and written by operations').
755 command_call(read_write_matrix,[Result],[],b_read_write_info:tcltk_read_write_matrix(Result)).
756 command_unavailable(read_write_matrix,Txt) :- command_unavailable(operations_events,Txt).
757 command_arguments(read_write_matrix,[table_result]).
758 command_category(read_write_matrix,table).
759 command_additional_info(read_write_matrix,group(machine_info)).
760
761 command_description(variable_read_write_matrix,'Variable Read/Write Matrix','Show for variables which operations read and write them').
762 command_call(variable_read_write_matrix,[Result],[],b_read_write_info:tcltk_variable_read_write_matrix(no_check,Result)).
763 command_unavailable(variable_read_write_matrix,Txt) :- command_unavailable(variables,Txt).
764 command_arguments(variable_read_write_matrix,[table_result]).
765 command_category(variable_read_write_matrix,table).
766 command_additional_info(variable_read_write_matrix,group(machine_info)).
767
768
769
770 command_description(wd_pos,'WD POs','Show Well-Definedness Proof Obligations').
771 command_call(wd_pos,[Result],[],well_def_analyser:tcltk_get_machine_wd_pos(only_goal,Result,_,_)).
772 command_unavailable(wd_pos,Txt) :- command_unavailable(b_mode,Txt).
773 command_arguments(wd_pos,[table_result]).
774 command_category(wd_pos,table).
775 command_preferences_category(wd_pos,wd_commands). % e.g., TABLE_COLUMN_LIMIT preference
776 command_additional_info(wd_pos,group(wd_info)).
777
778 command_description(wd_pos_and_hyps,'WD POs and Hyps','Show Well-Definedness Proof Obligations and Hypotheses necessary for successful proof (for discharged POs)').
779 command_call(wd_pos_and_hyps,[Result],[],well_def_analyser:tcltk_get_machine_wd_pos(goal_and_hyps,Result,_,_)).
780 command_unavailable(wd_pos_and_hyps,Txt) :- command_unavailable(b_mode,Txt).
781 command_arguments(wd_pos_and_hyps,[table_result]).
782 command_category(wd_pos_and_hyps,table).
783 command_preferences_category(wd_pos_and_hyps,wd_commands).
784 command_additional_info(wd_pos_and_hyps,group(wd_info)).
785
786 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)').
787 command_call(det_check_constants,[Result],[],b_state_model_check:tcltk_cbc_constants_det_check(Result)).
788 command_unavailable(det_check_constants,Txt) :- command_unavailable(constants,Txt).
789 command_arguments(det_check_constants,[table_result]).
790 command_category(det_check_constants,table).
791 command_preferences_category(det_check_constants,cbc_commands).
792 command_additional_info(det_check_constants,group(debug_info)).
793
794 command_description(unsat_core_properties,'Unsat Core of Properties/Axioms','Analyse a minimal unsatisfiable core of the PROPERTIES/Axioms').
795 command_call(unsat_core_properties,[Result],[],unsat_cores:unsat_core_properties_table(Result)).
796 command_unavailable(unsat_core_properties,'only available for B,Z or Event-B models with CONSTANTS or PROPERTIES') :-
797 \+ (b_or_z_mode, b_machine_has_constants_or_properties).
798 command_arguments(unsat_core_properties,[table_result]).
799 command_category(unsat_core_properties,table).
800 command_preferences_category(unsat_core_properties,table_commands).
801 command_additional_info(unsat_core_properties,group(debug_info)).
802
803 command_description(visb_attributes,'VisB Items','Show VisB items which set SVG attributes based on current state').
804 command_call(visb_attributes,[Result],[],visb_visualiser:tcltk_get_visb_items(Result)).
805 command_unavailable(visb_attributes,'only available after a VisB file was loaded') :-
806 \+ visb_visualiser:visb_file_is_loaded(_).
807 command_arguments(visb_attributes,[table_result]).
808 command_category(visb_attributes,table).
809 command_preferences_category(visb_attributes,table_commands).
810 command_additional_info(visb_attributes,group(visb_info)).
811
812 command_description(visb_events,'VisB Events','Show VisB click events that are available in current state').
813 command_call(visb_events,[Result],[],visb_visualiser:tcltk_get_visb_events(Result)).
814 command_unavailable(visb_events,'only available after a VisB file was loaded') :-
815 \+ visb_visualiser:visb_file_is_loaded(_).
816 command_arguments(visb_events,[table_result]).
817 command_category(visb_events,table).
818 command_preferences_category(visb_events,table_commands).
819 command_additional_info(visb_events,group(visb_info)).
820
821 command_description(visb_objects,'VisB Objects','Show VisB SVG objects which were created in addition to the SVG file').
822 command_call(visb_objects,[Result],[],visb_visualiser:tcltk_get_visb_objects(Result)).
823 command_unavailable(visb_objects,'only available after a VisB file was loaded') :-
824 \+ visb_visualiser:visb_file_is_loaded(_).
825 command_arguments(visb_objects,[table_result]).
826 command_category(visb_objects,table).
827 command_preferences_category(visb_objects,table_commands).
828 command_additional_info(visb_objects,group(visb_info)).
829
830 command_description(visb_hovers,'VisB Hovers','Show VisB hovers with enter and exit values').
831 command_call(visb_hovers,[Result],[],visb_visualiser:tcltk_get_visb_hovers(Result)).
832 command_unavailable(visb_hovers,'only available after a VisB file was loaded') :-
833 \+ visb_visualiser:visb_file_is_loaded(_).
834 command_arguments(visb_hovers,[table_result]).
835 command_category(visb_hovers,table).
836 command_preferences_category(visb_hovers,table_commands).
837 command_additional_info(visb_hovers,group(visb_info)).
838
839 command_description(find_value,'Find Value...','Find value inside variables and constants').
840 command_call(find_value,[Expression,Result],[],tcltk_interface:tcltk_find_value_as_table(Expression,[prefix],Result)).
841 command_unavailable(find_value,Txt) :- command_unavailable(b_mode,Txt).
842 command_arguments(find_value,[expression_atom,table_result]). % also accepts expression_raw_ast
843 command_category(find_value,table).
844 command_additional_info(find_value,group(debug_info)).
845
846 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)').
847 command_call(id_value_formula_tree,[ID,File],[],tcltk_interface:tcltk_show_identifier_value_as_dot_tree(ID,File)).
848 command_unavailable(id_value_formula_tree,Txt) :- command_unavailable(b_mode,Txt).
849 command_arguments(id_value_formula_tree,[expression_atom,dotfile]). % is actually predicate_atom, also accepts expression_raw_ast
850 command_category(id_value_formula_tree,dot).
851 command_preferences_category(id_value_formula_tree,dot_formula_tree).
852 command_additional_info(id_value_formula_tree,group(formula_visualisation)).
853
854
855 command_description(mcdc_coverage,'MC/DC Operation Coverage','Show MC/DC operation coverage').
856 command_call(mcdc_coverage,[Result],[],mcdc_coverage:tcltk_compute_mcdc_operation_coverage(Result)).
857 command_unavailable(mcdc_coverage,Txt) :- command_unavailable(operations_events,Txt).
858 command_arguments(mcdc_coverage,[table_result]).
859 command_category(mcdc_coverage,table).
860 command_preferences_category(mcdc_coverage,mc_dc_commands).
861 command_additional_info(mcdc_coverage,group(coverage_info)).
862
863 command_description(mcdc_inv_coverage,'MC/DC Invariant Coverage','Show MC/DC invariant coverage').
864 command_call(mcdc_inv_coverage,[Result],[],mcdc_coverage:tcltk_compute_mcdc_invariant_coverage(Result)).
865 command_unavailable(mcdc_inv_coverage,Txt) :- command_unavailable(b_mode,Txt).
866 command_arguments(mcdc_inv_coverage,[table_result]).
867 command_category(mcdc_inv_coverage,table).
868 command_preferences_category(mcdc_inv_coverage,mc_dc_commands).
869 command_additional_info(mcdc_inv_coverage,group(coverage_info)).
870
871 :- use_module(probsrc(runtime_profiler),[runtime_profile_available/0, tcltk_get_profile_info/2,constants_profiling_on/0,
872 tcltk_get_operations_profile_info/1, tcltk_get_constants_profile_info/1]).
873 command_description(prob_profile_info,'ProB Profile Info','Show runtime information for operations and invariants (in ms)').
874 command_call(prob_profile_info,[Result],[],runtime_profiler:tcltk_get_operations_profile_info(Result)).
875 command_unavailable(prob_profile_info,'no profiling information available, set PROFILING_INFO preference to TRUE') :-
876 \+ runtime_profile_available,!. % and possibly remove -Dprob_profile=false flag
877 command_unavailable(prob_profile_info,Txt) :-
878 get_preference(prob_source_profiling_on,false), % with prob_source_profiling we also profile ProB2-UI calls
879 command_unavailable(b_mode,Txt).
880 command_arguments(prob_profile_info,[table_result]). % also accepts expression_raw_ast
881 command_category(prob_profile_info,table).
882 command_additional_info(prob_profile_info,group(debug_info)).
883
884 command_description(prob_constants_profile_info,'ProB Constants Profile Info','Show runtime information for calculation of constants by equations in PROPERTIES (in ms)').
885 command_call(prob_constants_profile_info,[Result],[],runtime_profiler:tcltk_get_constants_profile_info(Result)).
886 command_unavailable(prob_constants_profile_info,
887 'no profiling information available, set PROFILING_INFO and PERFORMANCE_INFO preference to TRUE') :-
888 \+ runtime_profile_available,!.
889 command_unavailable(prob_constants_profile_info,Txt) :- command_unavailable(b_mode,Txt).
890 command_arguments(prob_constants_profile_info,[table_result]).
891 command_category(prob_constants_profile_info,table).
892 command_additional_info(prob_constants_profile_info,group(debug_info)).
893
894 command_description(prob_external_fun_profile_info,
895 'ProB External Functions Profile Info','Show runtime information for external function calls (in ms)').
896 command_call(prob_external_fun_profile_info,[Result],[],runtime_profiler:tcltk_get_profile_info(external_functions,Result)).
897 command_unavailable(prob_external_fun_profile_info,
898 'no profiling information available, set PROFILING_INFO preference to TRUE') :-
899 \+ runtime_profile_available,!. % and possibly remove -Dprob_profile=false flag
900 command_unavailable(prob_external_fun_profile_info,Txt) :- command_unavailable(b_mode,Txt).
901 command_arguments(prob_external_fun_profile_info,[table_result]).
902 command_category(prob_external_fun_profile_info,table).
903 command_additional_info(prob_external_fun_profile_info,group(debug_info)).
904
905 command_description(prob_cache_info,'ProB Persistent Cache Profile Info',
906 'Show runtime information for on disk caching of constants and operation calls (in ms)').
907 command_call(prob_cache_info,[Result],[],
908 runtime_profiler:tcltk_get_multiple_profile_infos(cache,Result)).
909 command_unavailable(prob_cache_info,'persistent cache not activated; provide -cache DIRECTORY at startup') :-
910 \+ value_persistance:cache_is_activated,!.
911 command_unavailable(prob_cache_info,'no profiling information available, set PROFILING_INFO preference to TRUE') :-
912 \+ runtime_profile_available,!. % and possibly remove -Dprob_profile=false flag
913 command_unavailable(prob_cache_info,Txt) :- command_unavailable(b_mode,Txt).
914 command_arguments(prob_cache_info,[table_result]).
915 command_category(prob_cache_info,table).
916 command_additional_info(prob_cache_info,group(debug_info)).
917
918 :- use_module(extrasrc(b_operation_cache),[tcltk_op_cache_stats/1]).
919 command_description(prob_opcache_info,'ProB Operation Caching Info','Show information for in memory operation caching, useful for model checking (see OPERATION_REUSE preference)').
920 command_call(prob_opcache_info,[Result],[],b_operation_cache:tcltk_op_cache_stats(Result)).
921 command_unavailable(prob_opcache_info,'only available when OPERATION_REUSE is TRUE or full.') :-
922 get_preference(operation_reuse_setting,false).
923 command_unavailable(prob_opcache_info,Txt) :- command_unavailable(b_mode,Txt).
924 command_arguments(prob_opcache_info,[table_result]).
925 command_category(prob_opcache_info,table).
926 command_additional_info(prob_opcache_info,group(debug_info)).
927
928
929 command_description(prob_memo_profile,'ProB Memoization Info','Show information for memoized constants').
930 command_call(prob_memo_profile,[Result],[],memoization:tcltk_get_memo_profile_table(Result)).
931 command_unavailable(prob_memo_profile,Txt) :- command_unavailable(b_mode,Txt).
932 command_arguments(prob_memo_profile,[table_result]).
933 command_category(prob_memo_profile,table).
934 command_additional_info(prob_memo_profile,group(debug_info)).
935
936 :- use_module(probsrc(bmachine_static_checks),[find_constant_expressions_in_operations/1]).
937 command_description(constant_expr_analysis,'Constant Expressions in Operations','Detect potentially expensive constant expressions in operations (and could be unnecessarily computed multiple times)').
938 command_call(constant_expr_analysis,[Result],[],bmachine_static_checks:find_constant_expressions_in_operations(Result)).
939 command_unavailable(constant_expr_analysis,Txt) :- command_unavailable(b_mode,Txt).
940 command_arguments(constant_expr_analysis,[table_result]).
941 command_category(constant_expr_analysis,table).
942 command_additional_info(constant_expr_analysis,group(debug_info)).
943
944
945 % a few typical reasons why commands are not available:
946 command_unavailable(constants,'only available for B,Z or Event-B models with CONSTANTS') :-
947 \+ (b_or_z_mode, b_machine_has_constants).
948 command_unavailable(variables,'only available for B,Z or Event-B models with VARIABLES') :-
949 \+ (b_or_z_mode, b_machine_has_variables).
950 command_unavailable(operations_events,'only available for B,Z or Event-B models with OPERATIONS/events') :-
951 \+ (b_or_z_mode, b_machine_has_operations).
952 command_unavailable(b_mode,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.