NuSMV/code/nusmv/core/ltl/ltl2smv/ltl2smv.h File Reference

#include "nusmv/core/node/node.h"

Go to the source code of this file.

Data Structures
struct	Ltl2SmvPrefixes
	A function to run ltl2smv routine. More...
Defines
#define	LTL_MODULE_BASE_NAME   "ltl_spec_"
Functions
node_ptr	ltl2smv (NuSMVEnv_ptr env, unsigned int uniqueId, node_ptr in_ltl_expr)
	The routine converting an LTL formula to am SMV Module.
node_ptr	ltl2smv_core (NuSMVEnv_ptr env, unsigned int uniqueId, node_ptr in_ltl_expr, boolean single_justice, const Ltl2SmvPrefixes *prefixes)
	The main routine converting an LTL formula to am SMV Module.
node_ptr	ltl2smv_single_justice (NuSMVEnv_ptr env, unsigned int uniqueId, node_ptr in_ltl_expr)
	The routine converting an LTL formula to am SMV Module.

---

Define Documentation

#define LTL_MODULE_BASE_NAME   "ltl_spec_"

MAcro********************************************************************

Synopsis [This macro is a string represeting the prefix of the name of modules generated by ltl2smv procedure]

Description []

SeeAlso [ltl2smv]

Todo:

Missing synopsis

Todo:

Missing description

---

Function Documentation

node_ptr ltl2smv	(	NuSMVEnv_ptr	env,
		unsigned int	uniqueId,
		node_ptr	in_ltl_expr
	)

The routine converting an LTL formula to am SMV Module.

The parameters are: uniqueId - is a positive integer number, which is converted to string representation and then used as a part of the generated SMV models name. (_LTL_uniqueId_SPECF_N_) in_ltl_expr - the input LTL Formula in the form of node_ptr. The expression should be flattened, rewritten wrt input variables, negated, i.e. be ready for conversion without any additional transformations

The function also performs memory-sharing on the input expression, since the returned module may be smaller if the memory of expression is shared. So DO NOT modify the output expressions.

But the invoker can modify the declarations and module itself (but not their expressions). See generate_smv_module for more info.

The return value is the created SMV module in the form of node_ptr.

The computed module may contain more than one justice condition.

See also:

ltl2smv_core

node_ptr ltl2smv_core	(	NuSMVEnv_ptr	env,
		unsigned int	uniqueId,
		node_ptr	in_ltl_expr,
		boolean	single_justice,
		const Ltl2SmvPrefixes *	prefixes
	)

The main routine converting an LTL formula to am SMV Module.

The parameters are: uniqueId - is a positive integer number, which is converted to string representation and then used as a part of the generated SMV models name. (_LTL_uniqueId_SPECF_N_) in_ltl_expr - the input LTL Formula in the form of node_ptr. The expression should be flattened, rewritten wrt input variables, negated, i.e. be ready for conversion without any additional transformations single_justice - is a boolean that when true, it builds a monitor such that there is a single fairness condition instead of possibly many.

The function also performs memory-sharing on the input expression, since the returned module may be smaller if the memory of expression is shared. So DO NOT modify the output expressions.

But the invoker can modify the declarations and module itself (but not their expressions). See generate_smv_module for more info.

The return value is the created SMV module in the form of node_ptr.

node_ptr ltl2smv_single_justice	(	NuSMVEnv_ptr	env,
		unsigned int	uniqueId,
		node_ptr	in_ltl_expr
	)

The routine converting an LTL formula to am SMV Module.

The parameters are: uniqueId - is a positive integer number, which is converted to string representation and then used as a part of the generated SMV models name. (_LTL_uniqueId_SPECF_N_) in_ltl_expr - the input LTL Formula in the form of node_ptr. The expression should be flattened, rewritten wrt input variables, negated, i.e. be ready for conversion without any additional transformations

The function also performs memory-sharing on the input expression, since the returned module may be smaller if the memory of expression is shared. So DO NOT modify the output expressions.

But the invoker can modify the declarations and module itself (but not their expressions). See generate_smv_module for more info.

The return value is the created SMV module in the form of node_ptr.

The computed module will contain less than one justice condition.