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 |