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

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/prop/Prop.h"
#include "nusmv/core/wff/ExprMgr.h"
#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/utils/OStream.h"

Go to the source code of this file.

Defines
#define	LTL_STRUCTCHECKLTLSPEC(self)   ((Ltl_StructCheckLtlSpec_ptr) self)
#define	LTL_STRUCTCHECKLTLSPEC_CHECK_INSTANCE(self)
Typedefs
typedef node_ptr(*	Ltl_StructCheckLtlSpec_ltl2smv )(NuSMVEnv_ptr, unsigned int, node_ptr)
typedef node_ptr(*	Ltl_StructCheckLtlSpec_oreg2smv )(NuSMVEnv_ptr, unsigned int, node_ptr)
typedef struct Ltl_StructCheckLtlSpec_TAG *	Ltl_StructCheckLtlSpec_ptr
Functions
Expr_ptr	Ltl_apply_input_vars_rewriting (Expr_ptr spec, SymbTable_ptr st, SymbLayer_ptr layer, FlatHierarchy_ptr outfh)
void	Ltl_CheckLtlSpec (NuSMVEnv_ptr env, Prop_ptr prop)
	The main routine to perform LTL model checking.
void	Ltl_spec_to_hierarchy (NuSMVEnv_ptr env, Expr_ptr spec, node_ptr context, node_ptr(*what2smv)(NuSMVEnv_ptr env, unsigned int id, node_ptr expr), SymbLayer_ptr layer, FlatHierarchy_ptr outfh)
	Takes a formula (with context) and constructs the flat hierarchy from it.
void	print_ltlspec (OStream_ptr, Prop_ptr, Prop_PrintFmt)

---

Define Documentation

#define LTL_STRUCTCHECKLTLSPEC

(

self

)

((Ltl_StructCheckLtlSpec_ptr) self)

Todo:

Missing synopsis

Todo:

Missing description

#define LTL_STRUCTCHECKLTLSPEC_CHECK_INSTANCE

(

self

)

Value:

(nusmv_assert(LTL_STRUCTCHECKLTLSPEC(self) != \
          LTL_STRUCTCHECKLTLSPEC(NULL)))

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef node_ptr(* Ltl_StructCheckLtlSpec_ltl2smv)(NuSMVEnv_ptr, unsigned int, node_ptr)

typedef node_ptr(* Ltl_StructCheckLtlSpec_oreg2smv)(NuSMVEnv_ptr, unsigned int, node_ptr)

Todo:

Missing synopsis

Todo:

Missing description

typedef struct Ltl_StructCheckLtlSpec_TAG* Ltl_StructCheckLtlSpec_ptr

---

Function Documentation

Expr_ptr Ltl_apply_input_vars_rewriting	(	Expr_ptr	spec,
		SymbTable_ptr	st,
		SymbLayer_ptr	layer,
		FlatHierarchy_ptr	outfh
	)

Todo:

Missing synopsis

Todo:

Missing description

void Ltl_CheckLtlSpec	(	NuSMVEnv_ptr	env,
		Prop_ptr	prop
	)

The main routine to perform LTL model checking.

The main routine to perform LTL model checking. It first takes the LTL formula, prints it in a file. It calls the LTL2SMV translator on it an reads in the generated tableau. The tableau is instantiated, compiled and then conjoined with the original model (both the set of fairness conditions and the transition relation are affected by this operation, for this reason we save the current model, and after the verification of the property we restore the original one).

If already set (The Scalar and the Bdd ones, the FSMs used for verification are taken from within the property. Otherwise, global FSMs are set within the property and then used for verification.

void Ltl_spec_to_hierarchy	(	NuSMVEnv_ptr	env,
		Expr_ptr	spec,
		node_ptr	context,
		node_ptr(*)(NuSMVEnv_ptr env, unsigned int id, node_ptr expr)	what2smv,
		SymbLayer_ptr	layer,
		FlatHierarchy_ptr	outfh
	)

Takes a formula (with context) and constructs the flat hierarchy from it.

Description []

SideEffects [layer and outfh are expected to get changed]

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

layer and outfh are expected to get changed

void print_ltlspec	(	OStream_ptr	,
		Prop_ptr	,
		Prop_PrintFmt
	)

Print the LTL specification.