Prop Struct Reference

Definition of the public accessor for class Prop. More...

#include <Prop_private.h>

Public Member Functions
	INHERITS_FROM (EnvObject)
Data Fields
BddFsm_ptr	bdd_fsm
BeFsm_ptr	be_fsm
BoolSexpFsm_ptr	bool_fsm
Set_t	cone
Prop_convert_to_invar_method	convert_to_invar
FsmBuilder_ptr	fsm_mgr
Prop_get_expr_method	get_expr
Prop_get_type_as_string_method	get_type_as_string
unsigned int	index
node_ptr	name
int	number
Prop_print_method	print
Prop_print_db_method	print_db_tabular
Prop_print_db_method	print_db_xml
Prop_print_method	print_truncated
Expr_ptr	prop
SexpFsm_ptr	scalar_fsm
Prop_set_environment_fsms_method	set_environment_fsms
Prop_Status	status
int	trace
Prop_Type	type
Prop_verify_method	verify
Related Functions
(Note that these are not member functions.)
int	Prop_check_type (const Prop_ptr self, Prop_Type type)
	Check if a property in the database is of a given type.
Set_t	Prop_compute_cone (const Prop_ptr self, FlatHierarchy_ptr hierarchy, SymbTable_ptr symb_table)
	Computes the COI for the given property.
Prop_ptr	prop_convert_to_invar (Prop_ptr self)
	Convert self to an invar, if possible.
Prop_ptr	Prop_convert_to_invar (Prop_ptr self)
	Convert, if possible, a property to an equivalent invarspec.
Prop_ptr	Prop_create (const NuSMVEnv_ptr env)
	The Prop class constructor.
Prop_ptr	Prop_create_from_string (NuSMVEnv_ptr env, char *str, Prop_Type type)
	A constructor from a string.
Prop_ptr	Prop_create_partial (const NuSMVEnv_ptr env, Expr_ptr expr, Prop_Type type)
	Creates a property, but does not insert it within the database, so the property can be used on the fly.
void	prop_deinit (Prop_ptr self)
	The Prop class private deinitializer.
void	Prop_destroy (Prop_ptr self)
	The Prop class destructor.
void	Prop_destroy_coi_for_bmc (Prop_ptr self)
	Cleans up part of the stuff generated by Prop_apply_coi_for_bmc.
BddFsm_ptr	Prop_get_bdd_fsm (const Prop_ptr self)
	Returns the BDD FSM of a property.
BeFsm_ptr	Prop_get_be_fsm (const Prop_ptr self)
	Returns the BE FSM of a property.
BoolSexpFsm_ptr	Prop_get_bool_sexp_fsm (const Prop_ptr self)
	Returns the boolean FSM of a property.
Set_t	Prop_get_cone (const Prop_ptr self)
	Returns the cone of a property.
char *	Prop_get_context_text (const Prop_ptr self)
	Returns the context name of a property.
Expr_ptr	prop_get_expr (const Prop_ptr self)
Expr_ptr	Prop_get_expr (const Prop_ptr self)
	Returns the property as it has been parsed and created.
Expr_ptr	Prop_get_expr_core (const Prop_ptr self)
	Returns the property, but it is converted before in terms of core symbols.
Expr_ptr	Prop_get_expr_core_for_coi (const Prop_ptr self)
	Derived from Prop_get_expr_core, but for PSL only removes forall replicators rather than converting the whole expression into LTL.
Expr_ptr	Prop_get_flattened_expr (const Prop_ptr self, SymbTable_ptr st)
	Derived from Prop_get_expr_core, it flattens the expression to properly remove the "CONTEXT" token if any as top level operator.
int	Prop_get_index (const Prop_ptr self)
	Returns the index of a property.
node_ptr	Prop_get_name (const Prop_ptr self)
	Gets the name of a property.
char *	Prop_get_name_as_string (const Prop_ptr self)
	Gets the name of a property as a string.
int	Prop_get_number (const Prop_ptr self)
	Returns the number of the property.
char *	Prop_get_number_as_string (const Prop_ptr self)
	Returns the number value as a string (only for compute types).
SexpFsm_ptr	Prop_get_scalar_sexp_fsm (const Prop_ptr self)
	Returns the scalar FSM of a property.
Prop_Status	Prop_get_status (const Prop_ptr self)
	Returns the status of the property.
const char *	Prop_get_status_as_string (const Prop_ptr self)
	Returns the a string associated to a property status.
SymbTable_ptr	Prop_get_symb_table (const Prop_ptr self)
	Retrieves the Symbol Table from the property.
char *	Prop_get_text (const Prop_ptr self)
	Returns the property text, with no explicit context.
int	Prop_get_trace (const Prop_ptr self)
	Returns the trace number associated to a property.
Prop_Type	Prop_get_type (const Prop_ptr self)
	Returns the property type.
const char *	prop_get_type_as_string (const Prop_ptr self)
const char *	Prop_get_type_as_string (Prop_ptr self)
	Returns the a string associated to a property type.
void	prop_init (Prop_ptr self, const NuSMVEnv_ptr env)
	The Prop class private initializer.
boolean	Prop_is_psl_ltl (const Prop_ptr self)
	Returns true if the property is PSL property and it is LTL compatible.
boolean	Prop_is_psl_obe (const Prop_ptr self)
	Returns true if the property is PSL property and it is CTL compatible.
void	prop_print (const Prop_ptr self, OStream_ptr file)
void	Prop_print (Prop_ptr self, OStream_ptr file, Prop_PrintFmt fmt)
	Prints a property.
void	Prop_print_db (Prop_ptr self, OStream_ptr file, PropDb_PrintFmt)
	Prints a property with info or its position and status within the database.
void	prop_print_db_tabular (const Prop_ptr self, OStream_ptr file)
void	prop_print_db_xml (const Prop_ptr self, OStream_ptr file)
void	prop_print_truncated (const Prop_ptr self, OStream_ptr file)
void	prop_set_bdd_fsm (Prop_ptr self, BddFsm_ptr fsm, const boolean duplicate)
void	Prop_set_bdd_fsm (Prop_ptr self, BddFsm_ptr fsm)
	Sets the boolean FSM in BDD of a property.
void	prop_set_be_fsm (Prop_ptr self, BeFsm_ptr fsm, const boolean duplicate)
void	Prop_set_be_fsm (Prop_ptr self, BeFsm_ptr fsm)
	Sets the boolean BE FSM of a property.
void	prop_set_bool_sexp_fsm (Prop_ptr self, BoolSexpFsm_ptr fsm, const boolean duplicate)
void	Prop_set_bool_sexp_fsm (Prop_ptr self, BoolSexpFsm_ptr fsm)
	Sets the boolean FSM of a property.
void	Prop_set_cone (Prop_ptr self, Set_t cone)
	Sets the cone of a property.
void	Prop_set_index (Prop_ptr self, const int index)
	Sets the index of a property.
void	Prop_set_name (Prop_ptr self, const node_ptr name)
	Sets the name of a property.
void	Prop_set_number (Prop_ptr self, int n)
	Sets the number of the property.
void	Prop_set_number_infinite (Prop_ptr self)
	Sets the number of the property to INFINITE.
void	Prop_set_number_undefined (Prop_ptr self)
	Sets the number of the property to UNDEFINED.
void	prop_set_scalar_sexp_fsm (Prop_ptr self, SexpFsm_ptr fsm, const boolean duplicate)
void	Prop_set_scalar_sexp_fsm (Prop_ptr self, SexpFsm_ptr fsm)
	Sets the scalar FSM of a property.
void	Prop_set_status (Prop_ptr self, Prop_Status s)
	Sets the status of the property.
void	Prop_set_trace (Prop_ptr self, int t)
	Sets the trace number.
void	prop_verify (Prop_ptr self)
void	Prop_verify (Prop_ptr self)
	Verifies a given property.

Detailed Description

Definition of the public accessor for class Prop.

Member Function Documentation

Prop::INHERITS_FROM ( EnvObject )

Friends And Related Function Documentation

int Prop_check_type	(	const Prop_ptr	self,
		Prop_Type	type
	)			`[related]`

Check if a property in the database is of a given type.

Checks if a property in the database is of a given type. If the type is correct, value 0 is returned, otherwise an error message is emitted and value 1 is returned.

Set_t Prop_compute_cone	(	const Prop_ptr	self,
		FlatHierarchy_ptr	hierarchy,
		SymbTable_ptr	symb_table
	)			`[related]`

Computes the COI for the given property.

Computes the COI for the given property. The caller should free the returned set

Prop_ptr prop_convert_to_invar ( Prop_ptr self ) [related]

Convert self to an invar, if possible.

Convert self to an invar, if possible

Prop_ptr Prop_convert_to_invar ( Prop_ptr self ) [related]

Convert, if possible, a property to an equivalent invarspec.

Convert, if possible, a property to an equivalent invarspec

Prop_ptr Prop_create ( const NuSMVEnv_ptr env ) [related]

The Prop class constructor.

AutomaticStart

Allocate a property. If no more room is available then a call to numsv_exit is performed. All the fields of the prop structure are initialized to either NULL or the corresponding default type (e.g. Prop_NoType for property type).

See also:: Prop_destroy

Prop_ptr Prop_create_from_string	(	NuSMVEnv_ptr	env,
		char *	str,
		Prop_Type	type
	)			`[related]`

A constructor from a string.

Returns NULL on failure

Prop_ptr Prop_create_partial	(	const NuSMVEnv_ptr	env,
		Expr_ptr	expr,
		Prop_Type	type
	)			`[related]`

Creates a property, but does not insert it within the database, so the property can be used on the fly.

Creates a property structure filling only the property and property type fields. The property index within the db is not set.

void prop_deinit ( Prop_ptr self ) [related]

The Prop class private deinitializer.

The Prop class private deinitializer

See also:: Prop_destroy

void Prop_destroy ( Prop_ptr self ) [related]

The Prop class destructor.

Free a property. Notice that before freeing the property all the elements of the property that needs to be freed will be automatically freed.

See also:: Prop_create

void Prop_destroy_coi_for_bmc ( Prop_ptr self ) [related]

Cleans up part of the stuff generated by Prop_apply_coi_for_bmc.

Removes the layer created by Prop_apply_coi_for_bmc from be_enc, bdd_enc, and bool_enc and destroys layer. Fsms are assumed to be destroyed upon destroying the property.

Prop_apply_coi_for_bmc

BddFsm_ptr Prop_get_bdd_fsm ( const Prop_ptr self ) [related]

Returns the BDD FSM of a property.

Returns the BDD FSM associated to the property. Self keeps the ownership of the given fsm

BeFsm_ptr Prop_get_be_fsm ( const Prop_ptr self ) [related]

Returns the BE FSM of a property.

Returns the boolean BE FSM associated to the property. Self keeps the ownership of the given fsm

BoolSexpFsm_ptr Prop_get_bool_sexp_fsm ( const Prop_ptr self ) [related]

Returns the boolean FSM of a property.

Returns the boolean FSM associated to the property. Self keeps the ownership of the given fsm

Set_t Prop_get_cone ( const Prop_ptr self ) [related]

Returns the cone of a property.

If the cone of influence of a property has been computed, this function returns it.

char * Prop_get_context_text ( const Prop_ptr self ) [related]

Returns the context name of a property.

If the property has no explicit context, 'Main' will be returned. The returned string must be deleted by the caller.

Expr_ptr prop_get_expr ( const Prop_ptr self ) [related]

Todo:

Expr_ptr Prop_get_expr ( const Prop_ptr self ) [related]

Returns the property as it has been parsed and created.

Returns the property stored in the prop. If the property is PSL, the result should be converted to core symbols before model checking (see Prop_get_expr_core or PslNode_convert_psl_to_core).

See also:: Prop_get_expr_core

Expr_ptr Prop_get_expr_core ( const Prop_ptr self ) [related]

Returns the property, but it is converted before in terms of core symbols.

Returns the property in a form that it can be handled by the system (model checking, dependency finder, etc.). This may imply a conversion and a different structure of the resulting formula. For example in PSL FORALLs are expanded, SERE are removed, global operators G and AG are simplified, etc.

Use this function at system-level, and Prop_get_expr to get the original formula instead

See also:: Prop_get_expr

Expr_ptr Prop_get_expr_core_for_coi ( const Prop_ptr self ) [related]

Derived from Prop_get_expr_core, but for PSL only removes forall replicators rather than converting the whole expression into LTL.

See also:: Prop_get_expr

Expr_ptr Prop_get_flattened_expr	(	const Prop_ptr	self,
		SymbTable_ptr	st
	)			`[related]`

Derived from Prop_get_expr_core, it flattens the expression to properly remove the "CONTEXT" token if any as top level operator.

See also:: Prop_get_expr_core, Prop_get_expr

int Prop_get_index ( const Prop_ptr self ) [related]

Returns the index of a property.

Returns the unique identifier of a property

node_ptr Prop_get_name ( const Prop_ptr self ) [related]

Gets the name of a property.

Get the property name

char * Prop_get_name_as_string ( const Prop_ptr self ) [related]

Gets the name of a property as a string.

Get the property name as a string, must be freed

Todo:

int Prop_get_number ( const Prop_ptr self ) [related]

Returns the number of the property.

For COMPUTE properties returns the number resulting from the evaluation of the property.

char * Prop_get_number_as_string ( const Prop_ptr self ) [related]

Returns the number value as a string (only for compute types).

Returns a number, 'Inifinite' or 'Unchecked'. The returned string is dynamically created, and caller must free it.

SexpFsm_ptr Prop_get_scalar_sexp_fsm ( const Prop_ptr self ) [related]

Returns the scalar FSM of a property.

Returns the scalar FSM associated to the property. Self keeps the ownership of the given fsm

Prop_Status Prop_get_status ( const Prop_ptr self ) [related]

Returns the status of the property.

Returns the status of the property

const char * Prop_get_status_as_string ( const Prop_ptr self ) [related]

Returns the a string associated to a property status.

Returns the string corresponding to a property status for printing it. The caller must NOT free the returned string, dince it is a constant.

SymbTable_ptr Prop_get_symb_table ( const Prop_ptr self ) [related]

Retrieves the Symbol Table from the property.

Retrieves the symbol table from the property. If there is an FSM associated to the property, then it takes the symbol table associated to the FSM, otherwise it returns NULL, and it will be the responsibility of the caller to handle this case.

char * Prop_get_text ( const Prop_ptr self ) [related]

Returns the property text, with no explicit context.

The returned string must be deleted by the caller.

int Prop_get_trace ( const Prop_ptr self ) [related]

Returns the trace number associated to a property.

For unsatisfied properties, the trace number of the asscociated counterexample is returned. 0 is returned if no trace is available

Prop_Type Prop_get_type ( const Prop_ptr self ) [related]

Returns the property type.

Returns the property kind of the stroed property, i.e. CTL, LTL, ...

const char * prop_get_type_as_string ( const Prop_ptr self ) [related]

Todo:

const char * Prop_get_type_as_string ( Prop_ptr self ) [related]

Returns the a string associated to a property type.

Returns the string corresponding to a property type for printing it. Returned string must NOT be deleted

void prop_init	(	Prop_ptr	self,
		const NuSMVEnv_ptr	env
	)			`[related]`

The Prop class private initializer.

The Prop class private initializer

See also:: Prop_create

boolean Prop_is_psl_ltl ( const Prop_ptr self ) [related]

Returns true if the property is PSL property and it is LTL compatible.

boolean Prop_is_psl_obe ( const Prop_ptr self ) [related]

Returns true if the property is PSL property and it is CTL compatible.

void prop_print	(	const Prop_ptr	self,
		OStream_ptr	file
	)			`[related]`

Todo:

void Prop_print	(	Prop_ptr	self,
		OStream_ptr	file,
		Prop_PrintFmt	fmt
	)			`[related]`

Prints a property.

Prints a property. PSL properties are specially handled.

void Prop_print_db	(	Prop_ptr	self,
		OStream_ptr	file,
		PropDb_PrintFmt
	)			`[related]`

Prints a property with info or its position and status within the database.

Prints a property on the specified FILE stream. Some of the information stored in the property structure are printed out (e.g. property, property kind, property status, ...).

The property is printed in the given format. Use PROPDB_PRINT_FMT_DEFAULT for a default format.

void prop_print_db_tabular	(	const Prop_ptr	self,
		OStream_ptr	file
	)			`[related]`

Todo:

void prop_print_db_xml	(	const Prop_ptr	self,
		OStream_ptr	file
	)			`[related]`

Todo:

void prop_print_truncated	(	const Prop_ptr	self,
		OStream_ptr	file
	)			`[related]`

Todo:

void prop_set_bdd_fsm	(	Prop_ptr	self,
		BddFsm_ptr	fsm,
		const boolean	duplicate
	)			`[related]`

Todo:

void Prop_set_bdd_fsm	(	Prop_ptr	self,
		BddFsm_ptr	fsm
	)			`[related]`

Sets the boolean FSM in BDD of a property.

The given fsm will be duplicated, so the caller keeps the ownership of fsm

void prop_set_be_fsm	(	Prop_ptr	self,
		BeFsm_ptr	fsm,
		const boolean	duplicate
	)			`[related]`

Todo:

void Prop_set_be_fsm	(	Prop_ptr	self,
		BeFsm_ptr	fsm
	)			`[related]`

Sets the boolean BE FSM of a property.

The given fsm will be duplicated, so the caller keeps the ownership of fsm

void prop_set_bool_sexp_fsm	(	Prop_ptr	self,
		BoolSexpFsm_ptr	fsm,
		const boolean	duplicate
	)			`[related]`

Todo:

void Prop_set_bool_sexp_fsm	(	Prop_ptr	self,
		BoolSexpFsm_ptr	fsm
	)			`[related]`

Sets the boolean FSM of a property.

The given fsm will be duplicated, so the caller keeps the ownership of fsm

void Prop_set_cone	(	Prop_ptr	self,
		Set_t	cone
	)			`[related]`

Sets the cone of a property.

Stores the cone of influence of the property

void Prop_set_index	(	Prop_ptr	self,
		const int	index
	)			`[related]`

Sets the index of a property.

Sets the unique identifier of a property

void Prop_set_name	(	Prop_ptr	self,
		const node_ptr	name
	)			`[related]`

Sets the name of a property.

Sets the name of a property

void Prop_set_number	(	Prop_ptr	self,
		int	n
	)			`[related]`

Sets the number of the property.

Sets the number resulting from the evaluation of the property.

void Prop_set_number_infinite ( Prop_ptr self ) [related]

Sets the number of the property to INFINITE.

Sets the to INFINITE the number resulting from the evaluation of the property.

void Prop_set_number_undefined ( Prop_ptr self ) [related]

Sets the number of the property to UNDEFINED.

Sets the to UNDEFINED the number resulting from the evaluation of the property.

void prop_set_scalar_sexp_fsm	(	Prop_ptr	self,
		SexpFsm_ptr	fsm,
		const boolean	duplicate
	)			`[related]`

Todo:

void Prop_set_scalar_sexp_fsm	(	Prop_ptr	self,
		SexpFsm_ptr	fsm
	)			`[related]`

Sets the scalar FSM of a property.

The given fsm will be duplicated, so the caller keeps the ownership of fsm

void Prop_set_status	(	Prop_ptr	self,
		Prop_Status	s
	)			`[related]`

Sets the status of the property.

Sets the status of the property

void Prop_set_trace	(	Prop_ptr	self,
		int	t
	)			`[related]`

Sets the trace number.

Sets the trace number for an unsatisfied property.

void prop_verify ( Prop_ptr self ) [related]

Todo:

void Prop_verify ( Prop_ptr self ) [related]

Verifies a given property.

Depending the property, different model checking algorithms are called. The status of the property is updated accordingly to the result of the verification process.