show_property - Shows the currently stored properties
show_property [-h] [[-c | -l | -i | -q] [-u | -t | -f]] | [-n property_number] | [-P property_name] | [-s] | [-m | -o output-file]
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)
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.
- -s Prints the number of stored properties.
- .
Last updated on 2010/05/19 15h:56