NuSMV/code/nusmv/shell/ltl/ltlCmd.c File Reference

#include "nusmv/shell/cmd/cmd.h"
#include "nusmv/shell/ltl/ltlCmd.h"
#include "nusmv/core/utils/StreamMgr.h"
#include "nusmv/core/utils/ErrorMgr.h"
#include "nusmv/core/utils/error.h"
#include "nusmv/core/prop/Prop.h"
#include "nusmv/core/prop/propPkg.h"
#include "nusmv/core/prop/PropDb.h"
#include "nusmv/core/mc/mc.h"
#include "nusmv/core/enc/enc.h"
#include "nusmv/core/compile/compile.h"

Functions
int	CommandCheckLtlSpec (NuSMVEnv_ptr env, int argc, char **argv)
void	Ltl_Init (NuSMVEnv_ptr env)
	Module header for shell commands.
Variables
cmp_struct_ptr	cmps
	Shell commands to deal with the LTL model checking.

---

Function Documentation

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

Command:

check_ltlspec: Performs LTL model checking

Command arguments: [-h] [-m | -o output-file] [-n number | -p "ltl-expr [IN context]" | -P \"name\"]

Performs model checking of LTL formulas. LTL model checking is reduced to CTL model checking as described in the paper by [CGH97].

A ltl-expr to be checked can be specified at command line using option -p. Alternatively, option -n can be used for checking a particular formula in the property database. If neither -n nor -p are used, all the LTLSPEC formulas in the database are checked.

Command options:

-m

Pipes the output generated by the command in processing LTLSPECs to the program specified by the PAGER shell variable if defined, else through the Unix command "more".

-o output-file

Writes the output generated by the command in processing LTLSPECs to the file output-file.

-p "ltl-expr [IN context]"

An LTL formula to be checked. context is the module instance name which the variables in ltl_expr must be evaluated in.

-n number

Checks the LTL property with index number in the property database.

-P name

Checks the LTL property named name in the property database.

void Ltl_Init

(

NuSMVEnv_ptr

env

)

Module header for shell commands.

Author:

Michele Dorigatti

Todo:

: Missing description

AutomaticStart

Initializes the ltl package. Initializes the ltl package.

None

---

Variable Documentation

cmp_struct_ptr cmps

Shell commands to deal with the LTL model checking.

Author:

Marco Roveri Shell commands to deal with the LTL model checking.