NuSMV/code/nusmv/shell/prop/propCmd.c File Reference

#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 Documentation

#define COMMAND_CONVERT_PROPERTY_TO_INVAR_NAME   "convert_property_to_invar"

Todo:

Missing synopsis

Todo:

Missing description

---

Function Documentation

int CommandAddProperty	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

add_property: Adds a property to the list of properties

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

Adds a CTL property.

-l

Adds an LTL property.

-i

Adds an INVAR property.

-s

Adds a PSL property.

-q

Adds a quantitative (COMPUTE) property.

-p "formula [IN context]"

Adds the formula specified on the command-line.
context is the module instance name which the variables in formula must be evaluated in.

-n name

Names the added property as "name"

See also:

show_property

int CommandCheckProperty	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

check_property: Checks a property into the current list of properties, or a newly specified property

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

Prints the help.

-c

Checks all the CTL properties not already checked

-l

Checks all the LTL properties not already checked

-i

Checks all the INVAR properties not already checked

-s

Checks all the PSL properties not already checked

-q

Checks all the COMPUTE properties not already checked

-n number

Checks the property with id number in the property list if it exists.

-P name

Checks the property named named in the property list if it exists.

-p "formula [IN context]"

Checks the 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.

See also:

check_property

int CommandConvertPropertyToInvar	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

convert_property_to_invar:

Command arguments: [-n number | -P \"name\" | -p \"formula\"]

int CommandShowProperty	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Shell interface for the prop package.

Author:

Marco Roveri This file contains the interface of the prop package with the interactive shell.

Command:

show_property: Shows the currently stored properties

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

---

Variable Documentation

cmp_struct_ptr cmps