NuSMV/code/nusmv/core/prop/Prop_private.h File Reference

#include "nusmv/core/prop/Prop.h"
#include "nusmv/core/utils/EnvObject.h"
#include "nusmv/core/utils/EnvObject_private.h"
#include "nusmv/core/utils/utils.h"

Go to the source code of this file.

Data Structures
struct	Prop
	Definition of the public accessor for class Prop. More...
Typedefs
typedef Prop_ptr(*	Prop_convert_to_invar_method )(Prop_ptr)
typedef Expr_ptr(*	Prop_get_expr_method )(const Prop_ptr)
	Private and protected interface of class 'Prop'.
typedef const char (	Prop_get_type_as_string_method )(const Prop_ptr)
typedef void(*	Prop_print_db_method )(const Prop_ptr, OStream_ptr)
typedef void(*	Prop_print_method )(const Prop_ptr, OStream_ptr)
typedef void(*	Prop_set_environment_fsms_method )(const NuSMVEnv_ptr env, Prop_ptr)
typedef void(*	Prop_verify_method )(Prop_ptr)
Functions
void	prop_set_environment_fsms (const NuSMVEnv_ptr env, Prop_ptr prop)
	Sets the Prop fsms from the given environment.

Typedef Documentation

typedef Prop_ptr(* Prop_convert_to_invar_method)(Prop_ptr)

Todo:: Missing synopsis

Todo:: Missing description

typedef Expr_ptr(* Prop_get_expr_method)(const Prop_ptr)

Private and protected interface of class 'Prop'.

Author:: Roberto Cavada This file can be included only by derived and friend classes

Prop class definition derived from class Object This structure contains informations about a given property:

index: is the progressive number identifying the specification.
prop: is the specification formula (s-expression).
type: is the type of the specification (CTL, LTL, INVAR, COMPUTE).
cone: is the cone of influence of the formula.
status: is the actual checking status of the specification.
number: Result of a COMPUTE property.
trace: is the index of the counterexample produced when the formula is found to be false, otherwise is zero.
scalar_fsm: The FSM associated to the property in scalar format.
bool_fsm: The FSM associated to the property in boolean format.
bdd_fsm: The FSM associated to the property in BDD format.
be_fsm: The FSM associated to the property in BE format.