#include "nusmv/shell/cmd/cmd.h"
#include "nusmv/shell/prop/propCmd.h"
#include "nusmv/core/compile/compile.h"
#include "nusmv/core/prop/Prop.h"
#include "nusmv/core/prop/PropDb.h"
#include "nusmv/core/prop/propPkg.h"
#include "nusmv/core/utils/OStream.h"
#include "nusmv/core/utils/StreamMgr.h"
#include "nusmv/core/utils/ErrorMgr.h"
#include "nusmv/core/node/printers/MasterPrinter.h"
#include "nusmv/core/parser/parser.h"
#include "nusmv/core/enc/enc.h"
#include "nusmv/core/mc/mc.h"
#include "nusmv/core/prop/propProp.h"
#include "nusmv/core/utils/error.h"
Defines | |
#define | COMMAND_CONVERT_PROPERTY_TO_INVAR_NAME "convert_property_to_invar" |
Functions | |
int | CommandAddProperty (NuSMVEnv_ptr env, int argc, char **argv) |
int | CommandCheckProperty (NuSMVEnv_ptr env, int argc, char **argv) |
int | CommandConvertPropertyToInvar (NuSMVEnv_ptr env, int argc, char **argv) |
int | CommandShowProperty (NuSMVEnv_ptr env, int argc, char **argv) |
Shell interface for the prop package. | |
void | PropPkg_init_cmd (NuSMVEnv_ptr env) |
Module header file for prop shell commands. | |
void | PropPkg_quit_cmd (NuSMVEnv_ptr env) |
Quit the prop package for commands. | |
Variables | |
cmp_struct_ptr | cmps |
#define COMMAND_CONVERT_PROPERTY_TO_INVAR_NAME "convert_property_to_invar" |
int CommandAddProperty | ( | NuSMVEnv_ptr | env, | |
int | argc, | |||
char ** | argv | |||
) |
Command arguments: [-h] [(-c | -l | -i | -q | -s) -p "formula [IN context]"] [-n "name"]
Adds a property in the list of properties. It is possible to insert LTL, CTL, INVAR, PSL and quantitative (COMPUTE) properties. Every newly inserted property is initialized to unchecked. A type option must be given to properly execute the command.
Command options:
-c
-l
-i
-s
-q
-p "formula [IN context]"
formula
specified on the command-line. context
is the module instance name which the variables in formula
must be evaluated in. -n name
int CommandCheckProperty | ( | NuSMVEnv_ptr | env, | |
int | argc, | |||
char ** | argv | |||
) |
Command arguments: [-h] [-n number | -P "name"] | [(-c | -l | -i | -s | -q ) [-p "formula [IN context]"]]
Checks the specified property taken from the property list, or adds the new specified property and checks it.
Command options:
-h
-c
-l
-i
-s
-q
-n number
number
in the property list if it exists. -P name
named
in the property list if it exists. -p "formula [IN context]"
formula
specified on the command-line. context
is the module instance name which the variables in formula
must be evaluated in. If no property has been specified via -n
or -p
or -P
, then all the properties (of a given type) in the property list will be evaluated.
int CommandConvertPropertyToInvar | ( | NuSMVEnv_ptr | env, | |
int | argc, | |||
char ** | argv | |||
) |
Command arguments: [-n number | -P \"name\" | -p \"formula\"]
int CommandShowProperty | ( | NuSMVEnv_ptr | env, | |
int | argc, | |||
char ** | argv | |||
) |
Shell interface for the prop package.
Command arguments: [-h] [[-c | -l | -i | -q] [-u | -t | -f]] | [-n property_number] | [-P property_name] | [-s] [-m | -o output-file] [-F format]
Shows the properties currently stored in the list of properties. This list is initialized with the properties (CTL, LTL, INVAR, COMPUTE) present in the input file, if any; then all of the properties added by the user with the relative check
or add_property<> commands are appended to this list. For every property, the following informations are displayed:
-
the identifier of the property (a progressive number);
-
the property formula;
-
the type (CTL, LTL, INVAR, COMPUTE) <il>the status of the formula (Unchecked, True, False) or the result of the quantitative expression, if any (it can be infinite);
-
if the formula has been found to be false, the number of the corresponding counterexample trace.
By default, all the properties currently stored in the list of properties are shown. Specifying the suitable options, properties with a certain status (Unchecked, True, False) and/or of a certain type (e.g. CTL, LTL), or with a given identifier, it is possible to let the system show a restricted set of properties. It is allowed to insert only one option per status and one option per type.
Command options:
-c
- Prints only CTL properties.
-l
- Prints only LTL properties.
-i
- Prints only INVAR properties.
-q
- Prints only quantitative (COMPUTE) properties.
-u
- Prints only unchecked properties.
-t
- Prints only those properties found to be true.
-f
- Prints only those properties found to be false.
-n property-number
- Prints out the property numbered
property-number
.
-P property-name
- Prints out the property named
property-name
.
-m
- Pipes the output through the program specified by the
PAGER
shell variable if defined, else through the UNIX
"more" command.
-o output-file
- Writes the output generated by the command to
output-file<>.
-F format
print with given format. Use -F help to see available formats.
-s Prints the number of stored properties.
<>.
- See also:
- add_property check_ctlspec check_ltlspec check_invar compute
void PropPkg_init_cmd | ( | NuSMVEnv_ptr | env | ) |
Module header file for prop shell commands.
AutomaticEnd
void PropPkg_quit_cmd | ( | NuSMVEnv_ptr | env | ) |
Quit the prop package for commands.
This must be called independently from the package initialization function
cmp_struct_ptr cmps |