1 % (c) 2016-2019 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 is_table_command/6]).
17
18 :- use_module(module_information).
19 :- module_info(group,visualization).
20 :- module_info(description,'This module provides access and description to a variety of Prolog commands.').
21
22 :- use_module(error_manager).
23 :- use_module(debug).
24 :- use_module(tools,[ajoin/2]).
25 :- use_module(specfile,[animation_mode/1, animation_minor_mode/1,
26 b_mode/0, z_mode/0, b_or_z_mode/0, b_or_z_mode/1, eventb_mode/0,
27 csp_mode/0, csp_mode/1,
28 csp_with_bz_mode/0,
29 process_algebra_mode/0,
30 spec_file_has_been_successfully_loaded/0]).
31 :- use_module(state_space, [current_state_corresponds_to_fully_setup_b_machine/0, current_state_corresponds_to_setup_constants_b_machine/0]).
32
33 % dot command with no arguments
34 is_dot_command(Command) :- command_category(Command,dot), command_arguments(Command,[dotfile]).
35 call_dot_command(Command,File) :- call_dot_command(Command,File,[]).
36 call_dot_command(Command,File,OptionalArgs) :- %print(cmd(Command,File,OptionalArgs)),nl,
37 call_command(dot,Command,[dotfile],[File],OptionalArgs).
38
39 is_dot_command_for_expr(Command) :-
40 command_category(Command,dot), command_arguments(Command,[expression_atom,dotfile]).
41 call_dot_command_for_expr(Command,Expr,File) :-
42 call_dot_command_for_expr(Command,Expr,File,[]).
43 call_dot_command_for_expr(Command,Expr,File,OptionalArgs) :- % print(cmd(Command,Expr,File,OptionalArgs)),nl,
44 call_command(dot,Command,[expression_atom,dotfile],[Expr,File],OptionalArgs).
45
46 % dot commands with no or with extra arguments:
47 % find out which dot commands are available and what arguments and preferences they take:
48 is_dot_command(Command,Name,Description,NumberOfFormulaArgs,Preferences,AdditionalInfo) :-
49 command_description(Command,Name,Description), % move forward to ensure ordering of found commands is same as in file
50 (is_dot_command(Command),NumberOfFormulaArgs=0 ;
51 is_dot_command_for_expr(Command),NumberOfFormulaArgs=1),
52 get_command_preferences(Command, Preferences),
53 findall(Info, command_additional_info(Command, Info), AdditionalInfo).
54
55 :- use_module(library(lists)).
56 % table commands (return as last argument list of lists)
57 is_table_command(Command,Name,Description,NumberOfFormulaArgs,Preferences,AdditionalInfo) :-
58 command_category(Command,table),
59 command_arguments(Command,Args), last(Args,table_result),
60 length(Args,Len), NumberOfFormulaArgs is Len - 1,
61 command_description(Command,Name,Description),
62 get_command_preferences(Command, Preferences),
63 findall(Info, command_additional_info(Command, Info), AdditionalInfo).
64
65
66
67
68
69 % call a command described in this module
70 call_command(Category,Command,FormalArgs,ActualArgs,OptionalArgs) :-
71 command_category(Command,Category),
72 command_arguments(Command,FormalArgs), % to do: more flexible matching of args ?
73 !,
74 (command_unavailable(Command,Msg)
75 -> tools:ajoin(['Command ', Command, ' not available: '],Msg1),
76 add_error(meta_interface,Msg1,Msg),
77 fail
78 ; setup_optional_args(Command,OptionalArgs,OptArgValueList),
79 (command_call(Command,ActualArgs,OptArgValueList,Call)
80 -> debug_println(4,command_call(Call)),
81 call(Call)
82 ; command_call(Command,ArgsExpected,_,_),length(ArgsExpected,Exp),length(ActualArgs,Form) %, Exp \= Form
83 ->
84 tools:ajoin(['Command ', Command, ' expects ', Exp, ' arguments, but obtained ',Form,'!'],Msg1),
85 add_internal_error(Msg1,command_call(Command,ActualArgs,OptArgValueList,_)),
86 fail
87 ; add_internal_error('Cannot construct command call: ',command_call(Command,ActualArgs,OptArgValueList,_)),
88 fail
89 )
90 ).
91 call_command(Category,Command,_FormalArgs,_ActualArgs,_OptArgs) :- command_category(Command,Category),
92 !,
93 add_error(meta_interface,'Argument mis-match when calling command: ',Command),fail.
94 call_command(Category,Command,_,_,_) :-
95 add_error(meta_interface,'Unknown command: ',Category:Command),fail.
96
97
98 setup_optional_args(Command,OptionalArgs,OptArgValueList) :-
99 command_optional_arguments(Command,Names,_Types,DefaultValues),!,
100 setup_opt_args_aux(Names,DefaultValues,OptionalArgs,Command,OptArgValueList).
101 setup_optional_args(_,[],Res) :- !, Res=[].
102 setup_optional_args(Cmd,Opt,Res) :- add_internal_error('Illegal optional arguments: ',setup_optional_args(Cmd,Opt,Res)),
103 Res=[].
104
105 :- use_module(library(lists),[select/3]).
106
107 setup_opt_args_aux([],[],OptArgs,Command,Res) :-
108 (OptArgs = [] -> true ; add_internal_error('Too many optional arguments: ',Command:OptArgs)),
109 Res = [].
110 setup_opt_args_aux([Name|NT],[Default|DT],OptArgs,Command,Res) :-
111 (select('='(Name,Value),OptArgs,OA2)
112 -> Res = [Value|RT], setup_opt_args_aux(NT,DT,OA2,Command,RT)
113 ; Res = [Default|RT], setup_opt_args_aux(NT,DT,OptArgs,Command,RT)
114 ).
115
116
117 % TO DO: provide automatic conversion ? expression_atom -> expression_codes -> typed_expression ?
118
119 :- use_module(preferences,[virtual_preference_category/2]).
120 % get all preferences for a command
121 get_command_preferences(Command,Preferences) :-
122 findall(Pref, (command_preferences_category(Command,PrefCat),
123 virtual_preference_category(Pref,PrefCat)), Preferences).
124
125 % --------------------
126 % COMMAND DESCRIPTIONS
127 % --------------------
128
129 :- discontiguous command_description/3, command_call/4,
130 command_unavailable/2, command_arguments/2,
131 command_optional_arguments/4,
132 command_category/2, command_preferences_category/2,
133 command_additional_info/2.
134
135 :- use_module(b_machine_hierarchy,[write_dot_event_hierarchy_to_file/1,write_dot_hierarchy_to_file/1]).
136
137 command_description(machine_hierarchy,'Machine Hierarchy','Shows the machine hierarchy of a classical B model').
138 command_call(machine_hierarchy,[File],[],b_machine_hierarchy:write_dot_hierarchy_to_file(File)).
139 command_unavailable(machine_hierarchy,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
140 command_arguments(machine_hierarchy,[dotfile]).
141 command_category(machine_hierarchy,dot).
142
143
144 command_description(event_hierarchy,'Event Hierarchy','Shows the event hierarchy of an Event-B model').
145 command_call(event_hierarchy,[File],[],b_machine_hierarchy:write_dot_event_hierarchy_to_file(File)).
146 command_unavailable(event_hierarchy,'only available for Event-B models') :- \+ eventb_mode.
147 command_arguments(event_hierarchy,[dotfile]).
148 command_category(event_hierarchy,dot).
149 command_preferences_category(event_hierarchy,dot_event_hierarchy).
150
151
152 :- use_module(visualize_graph,[tcltk_print_states_for_dot/2]).
153 command_description(state_space,'State Space','Show state space').
154 command_call(state_space,[File],[ColourTransitions],visualize_graph:tcltk_print_states_for_dot(File,ColourTransitions)).
155 command_unavailable(state_space,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded.
156 command_arguments(state_space,[dotfile]).
157 command_optional_arguments(state_space,[colouring],[atom],[no_colour_for_transitions]).
158 command_category(state_space,dot).
159 command_preferences_category(state_space,dot_state_space).
160
161 command_description(state_space_sfdp,'State Space (Fast)','Show state space (fast)').
162 command_call(state_space_sfdp,[File],[ColourTransitions],visualize_graph:tcltk_print_states_for_dot_sfdp(File,ColourTransitions)).
163 command_unavailable(state_space_sfdp,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded.
164 command_arguments(state_space_sfdp,[dotfile]).
165 command_optional_arguments(state_space_sfdp,[colouring],[atom],[no_colour_for_transitions]).
166 command_category(state_space_sfdp,dot).
167 command_preferences_category(state_space_sfdp,dot_state_space). % TODO: maybe remove those that are fixed and have no effect
168 command_additional_info(state_space_sfdp,preferred_dot_type(sfdp)). % sfdp preferred
169
170 :- use_module(state_space_reduction,[write_transition_diagram_for_expr_to_dotfile/2,
171 write_signature_merge_to_dotfile/2]).
172
173
174 command_description(signature_merge,'Signature Merge','Show signature-merged reduced state space').
175 command_call(signature_merge,[File],[IgnoredEvents],state_space_reduction:write_signature_merge_to_dotfile(IgnoredEvents,File)).
176 command_unavailable(signature_merge,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded.
177 command_arguments(signature_merge,[dotfile]).
178 command_optional_arguments(signature_merge,[ignored_events],[list(operations)],[[]]).
179 command_category(signature_merge,dot).
180
181
182 :- use_module(reduce_graph_state_space,[print_dot_for_dfa_from_nfa/1]).
183 command_description(dfa_merge,'DFA Merge','Show state space as deterministic automaton (DFA)').
184 command_call(dfa_merge,[File],[],reduce_graph_state_space:print_dot_for_dfa_from_nfa(File)).
185 command_unavailable(dfa_merge,'only available when model successfully loaded') :- \+ spec_file_has_been_successfully_loaded.
186 command_arguments(dfa_merge,[dotfile]).
187 command_category(dfa_merge,dot).
188
189 :- use_module(state_space_reduction,[write_transition_diagram_for_expr_to_dotfile/2]).
190 command_description(transition_diagram,'State Space Expression Projection...','Project state space onto expression values and show transition diagram').
191 command_call(transition_diagram,[Expression,File],[],
192 state_space_reduction:write_transition_diagram_for_expr_to_dotfile(Expression,File)).
193 command_unavailable(transition_diagram,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
194 command_arguments(transition_diagram,[expression_atom,dotfile]). % also accepts expression_raw_ast
195 command_category(transition_diagram,dot).
196 command_preferences_category(transition_diagram,dot_projection).
197
198 :- use_module(probporsrc(dot_graphs_static_analysis), [tcltk_create_dependence_graph/1, tcltk_create_enable_graph/1]).
199 command_description(enable_graph,'Enable Graph','Show enabling graph of events').
200 command_call(enable_graph,[File],[],dot_graphs_static_analysis:tcltk_create_enable_graph(File)).
201 command_unavailable(enable_graph,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
202 command_arguments(enable_graph,[dotfile]).
203 command_category(enable_graph,dot).
204
205 :- use_module(graph_canon,[print_cstate_graph/1]).
206 command_description(state_as_graph,'Current State as Graph','Show values in current state as a graph').
207 command_call(state_as_graph,[File],[],graph_canon:print_cstate_graph(File)).
208 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.
209 command_arguments(state_as_graph,[dotfile]).
210 command_category(state_as_graph,dot).
211 % we could use tcltk_print_current_state_as_graph_for_dot
212
213 :- use_module(state_custom_dot_graph,[tcltk_generate_state_custom_dot_graph/1,state_custom_dot_graph_available/0]).
214
215 command_description(custom_graph,'Customized Current State as Graph','Show values in current state as a graph using CUSTOM_GRAPH_EDGES').
216 command_call(custom_graph,[File],[],state_custom_dot_graph:tcltk_generate_state_custom_dot_graph(File)).
217 command_unavailable(custom_graph,'only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine') :-
218 \+ state_custom_dot_graph_available.
219 command_unavailable(custom_graph,'only available for initialised B,Z or Event-B models') :-
220 state_custom_dot_graph_available,
221 \+ current_state_corresponds_to_fully_setup_b_machine.
222 command_arguments(custom_graph,[dotfile]). % also accepts expression_raw_ast
223 command_category(custom_graph,dot).
224
225 % from tcltk_interface.pl:
226 command_description(expr_as_graph,'(Relational) Expression as Graph...','Show (relational) expression value as a graph').
227 command_call(expr_as_graph,[Expression,File],[],user:tcltk_show_expression_as_dot(Expression,File)).
228 command_unavailable(expr_as_graph,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
229 command_arguments(expr_as_graph,[expression_atom,dotfile]). % also accepts expression_raw_ast
230 command_category(expr_as_graph,dot).
231
232
233 command_description(formula_tree,'Custom Predicate/Expression Formula Tree...','Show predicate/expressions and sub-formulas as a tree').
234 command_call(formula_tree,[Expression,File],[],user:generate_dot_from_formula(Expression,File)).
235 command_unavailable(formula_tree,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
236 command_arguments(formula_tree,[expression_atom,dotfile]). % is actually predicate_atom, also accepts expression_raw_ast
237 command_category(formula_tree,dot).
238 command_preferences_category(formula_tree,dot_formula_tree).
239
240 command_description(invariant,'Invariant Formula Tree','Show invariant as a formula tree').
241 command_call(invariant,[File],[],user:generate_dot_from_invariant(File)).
242 command_unavailable(invariant,'only available for initialised B,Z or Event-B models') :- \+ current_state_corresponds_to_fully_setup_b_machine.
243 command_arguments(invariant,[dotfile]).
244 command_category(invariant,dot).
245 command_preferences_category(invariant,dot_formula_tree).
246
247 command_description(properties,'Properties Formula Tree','Show properties as a formula tree').
248 command_call(properties,[File],[],user:generate_dot_from_properties(File)).
249 %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
250 command_unavailable(properties,'only available for B,Z or Event-B models after constant setup or initialisation') :- \+ current_state_corresponds_to_setup_constants_b_machine.
251 command_arguments(properties,[dotfile]).
252 command_category(properties,dot).
253 command_preferences_category(properties,dot_formula_tree).
254
255 command_description(assertions,'Assertions Formula Tree','Show assertions as a formula tree').
256 command_call(assertions,[File],[],user:generate_dot_from_assertions(File)).
257 %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
258 command_unavailable(assertions,'only available for B,Z or Event-B models after constant setup or initialisation') :- \+ current_state_corresponds_to_setup_constants_b_machine.
259 command_arguments(assertions,[dotfile]).
260 command_category(assertions,dot).
261 command_preferences_category(assertions,dot_formula_tree).
262
263 command_description(deadlock,'Deadlock Formula Tree','Show deadlocking status as a formula tree').
264 command_call(deadlock,[File],[],user:generate_dot_from_deadlock_po(File)).
265 command_unavailable(deadlock,'only available for initialised B,Z or Event-B models') :-
266 \+ current_state_corresponds_to_fully_setup_b_machine.
267 command_arguments(deadlock,[dotfile]).
268 command_category(deadlock,dot).
269 command_preferences_category(deadlock,dot_formula_tree).
270
271 :- use_module(bmachine,[b_get_machine_goal/1]).
272 command_description(goal,'Goal Formula Tree','Show GOAL as a formula tree').
273 command_call(goal,[File],[],user:generate_dot_from_goal(File)).
274 command_unavailable(goal,'only available for initialised B,Z or Event-B models with a GOAL DEFINITION') :-
275 (\+ b_or_z_mode ; \+ b_get_machine_goal(_)).
276 command_arguments(goal,[dotfile]).
277 command_category(goal,dot).
278 command_preferences_category(goal,dot_formula_tree).
279
280 command_description(dependence_graph,'Dependence Graph','Show dependence graph of events').
281 command_call(dependence_graph,[File],[],dot_graphs_static_analysis:tcltk_create_dependence_graph(File)).
282 command_unavailable(dependence_graph,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
283 command_arguments(dependence_graph,[dotfile]).
284 command_category(dependence_graph,dot).
285
286 command_description(variable_modification_graph,'Variable Read/Write Graph','Show variable modification by operations and reading in guards').
287 command_call(variable_modification_graph,[File],[],b_read_write_info:tcltk_dot_variable_modification_analysis(File)).
288 command_unavailable(variable_modification_graph,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
289 command_arguments(variable_modification_graph,[dotfile]).
290 command_category(variable_modification_graph,dot).
291 command_preferences_category(goal,dot_variable_modification).
292
293 :- use_module(visualize_graph,[tcltk_print_definitions_as_graph_for_dot/1]).
294 command_description(definitions,'Definitions Graph','Show dependence graph of DEFINITIONS').
295 command_call(definitions,[File],[],visualize_graph:tcltk_print_definitions_as_graph_for_dot(File)).
296 command_unavailable(definitions,'only available for B or Z models') :- (b_or_z_mode -> eventb_mode ; true).
297 command_arguments(definitions,[dotfile]).
298 command_category(definitions,dot).
299 command_preferences_category(definitions,dot_definitions).
300
301 :- use_module(visualize_graph,[tcltk_print_predicate_dependency_as_graph_for_dot/2]).
302 command_description(predicate_dependency,'Predicate Dependency Graph...','Show dependence graph of conjuncts of a predicate').
303 command_call(predicate_dependency,[Pred,File],[],visualize_graph:tcltk_print_predicate_dependency_as_graph_for_dot(Pred,File)).
304 command_unavailable(predicate_dependency,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
305 command_arguments(predicate_dependency,[expression_atom,dotfile]). % also accepts expression_raw_ast
306 command_category(predicate_dependency,dot).
307
308 command_description(last_error,'Last Error Formula Tree','Show last error source as a formula tree').
309 command_call(last_error,[File],[],user:generate_dot_from_last_span_predicate(File)).
310 command_unavailable(last_error,'only available when error occured') :- \+ user:can_generate_dot_from_last_state_error.
311 command_arguments(last_error,[dotfile]).
312 command_category(last_error,dot).
313
314
315 % TABLE COMMANDS:
316
317 % from tcltk_interface.pl:
318 command_description(expr_as_table,'Expression Table...','Show expression value as a table').
319 command_call(expr_as_table,[Expression,Result],[],user:tcltk_eval_as_table(Expression,Result)).
320 command_unavailable(expr_as_table,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
321 command_arguments(expr_as_table,[expression_atom,table_result]). % also accepts expression_raw_ast
322 command_category(expr_as_table,table).
323
324 command_description(quick_operation_coverage,'Operation Coverage','Show which operations are covered').
325 command_call(quick_operation_coverage,[Result],[],user:tcltk_operations_covered_info(Result,quick)).
326 %command_unavailable(quick_operation_coverage,'always available').
327 command_arguments(quick_operation_coverage,[table_result]). % also accepts expression_raw_ast
328 command_category(quick_operation_coverage,table).
329
330 command_description(precise_operation_coverage,'Operation Coverage and Feasibility','Show which feasible operations are covered').
331 command_call(precise_operation_coverage,[Result],[],user:tcltk_operations_covered_info(Result,precise)).
332 command_unavailable(precise_operation_coverage,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
333 command_arguments(precise_operation_coverage,[table_result]). % also accepts expression_raw_ast
334 command_category(precise_operation_coverage,table).
335
336 command_description(show_typing,'Show Typing','Show Types for Variables and Constants').
337 command_call(show_typing,[Result],[],meta_interface:show_typing_table(Result)).
338 command_unavailable(show_typing,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
339 command_arguments(show_typing,[table_result]). % also accepts expression_raw_ast
340 command_category(show_typing,table).
341 :- public show_typing_table/1.
342 show_typing_table(list([list(['Typing'])|LRes])) :- user:tcltk_show_typing_of_variables_and_constants(list(Res)),
343 maplist(wrap_into_list,Res,LRes).
344
345 command_description(variable_coverage,'Variable Coverage','Show Number of Distinct Covered Values for Variables').
346 command_call(variable_coverage,[Result],[],user:tcltk_compute_nr_covered_values_for_all_variables(Result)).
347 command_unavailable(variable_coverage,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
348 command_arguments(variable_coverage,[table_result]). % also accepts expression_raw_ast
349 command_category(variable_coverage,table).
350
351 command_description(minmax_table,'Min/Max Values','Show Min/Max Values for Constants and Variables').
352 command_call(minmax_table,[Result],[],meta_interface:minmax_table(Result)).
353 command_unavailable(minmax_table,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
354 command_arguments(minmax_table,[table_result]). % also accepts expression_raw_ast
355 command_category(minmax_table,table).
356 :- public minmax_table/1.
357 minmax_table(list([list(['Min/Max'])|LRes])) :- user:tcltk_compute_min_max(list(Res)),
358 maplist(wrap_into_list,Res,LRes).
359
360 wrap_into_list(list(L),R) :- !, R=list(L).
361 wrap_into_list([],R) :- !, R=list([]).
362 wrap_into_list([H|T],R) :- !, R=list([H|T]).
363 wrap_into_list(X,list([X])).
364
365 command_description(vacuous_invariants,'Vacuous Invariants','Show List of Vacuous Invariants (given current state space)').
366 command_call(vacuous_invariants,[Result],[],meta_interface:vacuous_invariants(Result)).
367 command_unavailable(vacuous_invariants,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
368 command_arguments(vacuous_invariants,[table_result]). % also accepts expression_raw_ast
369 command_category(vacuous_invariants,table).
370 :- public vacuous_invariants/1.
371 vacuous_invariants(list([list(['Vacuous Invariant'])|LRes])) :-
372 user:tcltk_get_vacuous_invariants(list(Res)),
373 maplist(wrap_into_list,Res,LRes).
374
375 command_description(vacuous_guards,'Vacuous Guards','Show List of Vacuous Guards (given current state space)').
376 command_call(vacuous_guards,[Result],[],meta_interface:vacuous_guards(Result)).
377 command_unavailable(vacuous_guards,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
378 command_arguments(vacuous_guards,[table_result]). % also accepts expression_raw_ast
379 command_category(vacuous_guards,table).
380 :- public vacuous_guards/1.
381 vacuous_guards(list([list(['Vacuous Invariant'])|LRes])) :-
382 user:tcltk_get_vacuous_guards(list(Res)),
383 maplist(wrap_into_list,Res,LRes).
384
385 command_description(mcdc_coverage,'MC/DC Operation Coverage','Show MC/DC Operation Coverage').
386 command_call(mcdc_coverage,[Result],[],user:tcltk_compute_mcdc_operation_coverage(Result)).
387 command_unavailable(mcdc_coverage,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
388 command_arguments(mcdc_coverage,[table_result]). % also accepts expression_raw_ast
389 command_category(mcdc_coverage,table).
390 command_preferences_category(mcdc_coverage,mc_dc_commands).
391
392 command_description(mcdc_inv_coverage,'MC/DC Invariant Coverage','Show MC/DC Invariant Coverage').
393 command_call(mcdc_inv_coverage,[Result],[],user:tcltk_compute_mcdc_invariant_coverage(Result)).
394 command_unavailable(mcdc_inv_coverage,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
395 command_arguments(mcdc_inv_coverage,[table_result]). % also accepts expression_raw_ast
396 command_category(mcdc_inv_coverage,table).
397 command_preferences_category(mcdc_inv_coverage,mc_dc_commands).
398
399 command_description(read_write_matrix,'Operation Read/Write Matrix','Show identifiers read and written by operations').
400 command_call(read_write_matrix,[Result],[],b_read_write_info:tcltk_read_write_matrix(Result)).
401 command_unavailable(read_write_matrix,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
402 command_arguments(read_write_matrix,[table_result]). % also accepts expression_raw_ast
403 command_category(read_write_matrix,table).
404
405 command_description(variable_read_write_matrix,'Variable Read/Write Matrix','Show for variables which operations read and write them').
406 command_call(variable_read_write_matrix,[Result],[],b_read_write_info:tcltk_variable_read_write_matrix(no_check,Result)).
407 command_unavailable(variable_read_write_matrix,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
408 command_arguments(variable_read_write_matrix,[table_result]). % also accepts expression_raw_ast
409 command_category(variable_read_write_matrix,table).
410
411 :- use_module(runtime_profiler,[runtime_profile_available/0, tcltk_get_profile_info/1]).
412 command_description(prob_profile_info,'ProB Profile Info','Show runtime information for operations').
413 command_call(prob_profile_info,[Result],[],runtime_profiler:tcltk_get_profile_info(Result)).
414 command_unavailable(prob_profile_info,'no profiling information available, recompile probcli with -Dprob_profile=true') :- \+ runtime_profile_available,!.
415 command_unavailable(prob_profile_info,'only available for B,Z or Event-B models') :- \+ b_or_z_mode.
416 command_arguments(prob_profile_info,[table_result]). % also accepts expression_raw_ast
417 command_category(prob_profile_info,table).
418