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