PropDb Struct Reference

Public interface of class 'PropDb'. More...

#include <PropDb_private.h>

Public Member Functions
	INHERITS_FROM (EnvObject)
Data Fields
PropDb_PrintFmt	print_fmt
PropDb_prop_create_and_add_method	prop_create_and_add
array_t *	prop_database
PropDb_verify_all_method	verify_all
Related Functions
(Note that these are not member functions.)
void	prop_db_deinit (PropDb_ptr self)
	The PropDb class private deinitializer.
void	prop_db_init (PropDb_ptr self, NuSMVEnv_ptr environment)
	The PropDb class private initializer.
int	prop_db_prop_create_and_add (PropDb_ptr self, SymbTable_ptr symb_table, node_ptr spec, Prop_Type type)
	Inserts a property in the DB of properties.
void	prop_db_verify_all (const PropDb_ptr self)
	Verifies all the properties in the DB.
boolean	PropDb_add (PropDb_ptr self, Prop_ptr)
	Inserts a property in the DB of properties.
int	PropDb_check_property (const PropDb_ptr self, const Prop_Type pt, const char *formula, const int prop_no)
	Checks properties.
void	PropDb_clean (PropDb_ptr self)
	Disposes the DB of properties.
PropDb_ptr	PropDb_create (NuSMVEnv_ptr env)
	The PropDb class constructor.
void	PropDb_destroy (PropDb_ptr self)
	The PropDb class destructor.
int	PropDb_fill (PropDb_ptr self, SymbTable_ptr symb_table, node_ptr, node_ptr, node_ptr, node_ptr, node_ptr)
	Fills the DB of properties.
NodeList_ptr	PropDb_get_coi_grouped_properties (const PropDb_ptr self, const FlatHierarchy_ptr hierarchy)
	Get the list of properties, grouped by COI.
Prop_ptr	PropDb_get_last (const PropDb_ptr self)
	Returns the last entered property in the DB.
NodeList_ptr	PropDb_get_ordered_properties (const PropDb_ptr self, const FlatHierarchy_ptr hierarchy)
	Get the list of properties ordered by COI size.
lsList	PropDb_get_ordered_props_of_type (const PropDb_ptr self, const FlatHierarchy_ptr hierarchy, const Prop_Type type)
	Return the list of properties of a given type, ordered by COI size.
PropDb_PrintFmt	PropDb_get_print_fmt (const PropDb_ptr self)
	Returns the currently set print format.
Prop_ptr	PropDb_get_prop_at_index (const PropDb_ptr self, int num)
	Returns the property indexed by index.
int	PropDb_get_prop_index_from_string (const PropDb_ptr self, const char *idx)
	Get a valid property index from a string.
int	PropDb_get_prop_index_from_trace_index (const PropDb_ptr self, const int trace_idx)
	Returns the index of the property associated to a trace.
int	PropDb_get_prop_name_index (const PropDb_ptr self, const node_ptr name)
	Returns the property with the given name.
Set_t	PropDb_get_props_at_indices (const PropDb_ptr self, const ErrorMgr_ptr errmgr, const char *indices)
	Produces a set of properties from a delimited string containing properties indices.
lsList	PropDb_get_props_of_type (const PropDb_ptr self, const Prop_Type type)
	Return the list of properties of a given type Returned list to be disposed by the caller.
int	PropDb_get_size (const PropDb_ptr self)
	Returns the size of the DB.
boolean	PropDb_is_prop_registered (PropDb_ptr self, Prop_ptr prop)
	Checks if "prop" is registered within self.
void	PropDb_ordered_verify_all (const PropDb_ptr self, const FlatHierarchy_ptr hierarchy)
	Verifies all the properties in the DB.
void	PropDb_ordered_verify_all_type (const PropDb_ptr self, const FlatHierarchy_ptr hierarchy, const Prop_Type type)
	Verifies all properties of a given type, ordered by COI size.
lsList	PropDb_prepare_prop_list (const PropDb_ptr self, const Prop_Type type)
	Wrapper for PropDb_get_ordered_props_of_type, PropDb_get_props_of_type.
void	PropDb_print_all (const PropDb_ptr self, OStream_ptr file)
	Prints all the properties stored in the DB.
void	PropDb_print_all_status (const PropDb_ptr self, OStream_ptr file, Prop_Status status)
	Prints all the properties stored in the DB.
void	PropDb_print_all_status_type (const PropDb_ptr self, OStream_ptr file, Prop_Status status, Prop_Type type)
	Prints all the properties stored in the DB.
void	PropDb_print_all_type (const PropDb_ptr self, OStream_ptr file, Prop_Type type)
	Prints all the properties stored in the DB.
void	PropDb_print_list_footer (const PropDb_ptr self, OStream_ptr file)
	Prints the footer of the property list.
void	PropDb_print_list_header (const PropDb_ptr self, OStream_ptr file)
	Prints the header of the property list.
int	PropDb_print_prop_at_index (const PropDb_ptr self, OStream_ptr file, const int index)
int	PropDb_prop_create_and_add (PropDb_ptr self, SymbTable_ptr symb_table, node_ptr, Prop_Type)
	Inserts a property in the DB of properties.
int	PropDb_prop_parse_and_add (const PropDb_ptr self, SymbTable_ptr symb_table, const char *str, const Prop_Type type, const node_ptr expr_name)
	Add a property to the database from a string and a type.
int	PropDb_prop_parse_name (const PropDb_ptr self, const char *str)
	Given a string representing a property name, returns the property index, if it exists.
PropDb_PrintFmt	PropDb_set_print_fmt (const PropDb_ptr self, PropDb_PrintFmt new_fmt)
	Sets the current print format.
int	PropDb_show_property (const PropDb_ptr self, const boolean print_props_num, const PropDb_PrintFmt fmt, const Prop_Type type, const Prop_Status status, const int prop_no, FILE *outstream)
	Shows the currently stored properties.
void	PropDb_verify_all (const PropDb_ptr self)
	Verifies all the properties in the DB.
void	PropDb_verify_all_type (const PropDb_ptr self, Prop_Type)
	Verifies all properties of a given type.
void	PropDb_verify_prop_at_index (const PropDb_ptr self, const int index)
	Verifies a given property.

Detailed Description

Public interface of class 'PropDb'.

Author:: Roberto Cavada

Todo:: : Missing description

Definition of the public accessor for class PropDb

Member Function Documentation

PropDb::INHERITS_FROM ( EnvObject )

Friends And Related Function Documentation

void prop_db_deinit ( PropDb_ptr self ) [related]

The PropDb class private deinitializer.

The PropDb class private deinitializer

See also:: PropDb_destroy

void prop_db_init	(	PropDb_ptr	self,
		NuSMVEnv_ptr	environment
	)			`[related]`

The PropDb class private initializer.

The PropDb class private initializer

See also:: PropDb_create

int prop_db_prop_create_and_add	(	PropDb_ptr	self,
		SymbTable_ptr	symb_table,
		node_ptr	spec,
		Prop_Type	type
	)			`[related]`

Inserts a property in the DB of properties.

Given a formula and its type, a property is created and stored in the DB of properties. It returns either -1 in case of failure, or the index of the inserted property.

void prop_db_verify_all ( const PropDb_ptr self ) [related]

Verifies all the properties in the DB.

All the properties stored in the database not yet verified will be verified. The properties are verified following the order CTL/COMPUTE/LTL/INVAR.

boolean PropDb_add	(	PropDb_ptr	self,
		Prop_ptr
	)			`[related]`

Inserts a property in the DB of properties.

Insert a property in the DB of properties. If not previously set, sets the property index. Returns true if out of memory

int PropDb_check_property	(	const PropDb_ptr	self,
		const Prop_Type	pt,
		const char *	formula,
		const int	prop_no
	)			`[related]`

Checks properties.

Check the property type and the property index and calls the proper ProbDb_verify_* function.

void PropDb_clean ( PropDb_ptr self ) [related]

Disposes the DB of properties.

Disposes the DB of properties

PropDb_ptr PropDb_create ( NuSMVEnv_ptr env ) [related]

The PropDb class constructor.

AutomaticStart

The PropDb class constructor

See also:: PropDb_destroy

void PropDb_destroy ( PropDb_ptr self ) [related]

The PropDb class destructor.

The PropDb class destructor

See also:: PropDb_create

int PropDb_fill	(	PropDb_ptr	self,
		SymbTable_ptr	symb_table,
		node_ptr	,
		node_ptr	,
		node_ptr	,
		node_ptr	,
		node_ptr
	)			`[related]`

Fills the DB of properties.

Given for each kind of property a list of respective formulae, this function is responsible to fill the DB with them. Returns 1 if an error occurred, 0 otherwise

NodeList_ptr PropDb_get_coi_grouped_properties	(	const PropDb_ptr	self,
		const FlatHierarchy_ptr	hierarchy
	)			`[related]`

Get the list of properties, grouped by COI.

Get the list of properties, grouped by COI. A list of couples is returned. The left part of the couple is the COI (represented as a Set_t). The right part of the couple is a Set containing all properties with that COI. The returned list is ordered by COI size. The list, all couples and all sets should be freed by the caller

See also:: PropDb_get_ordered_properties

Prop_ptr PropDb_get_last ( const PropDb_ptr self ) [related]

Returns the last entered property in the DB.

Returns the last entered property in the DB of properties.

NodeList_ptr PropDb_get_ordered_properties	(	const PropDb_ptr	self,
		const FlatHierarchy_ptr	hierarchy
	)			`[related]`

Get the list of properties ordered by COI size.

List elements are couples made using cons: the car part points to the property, while the cdr part points to the COI. The list and it's elements (cons nodes and COI sets) should be freed by the caller

Note: here "cons" could be substituted by Pair

lsList PropDb_get_ordered_props_of_type	(	const PropDb_ptr	self,
		const FlatHierarchy_ptr	hierarchy,
		const Prop_Type	type
	)			`[related]`

Return the list of properties of a given type, ordered by COI size.

Returned list must be disposed by the caller.

PropDb_PrintFmt PropDb_get_print_fmt ( const PropDb_ptr self ) [related]

Returns the currently set print format.

When printing, the currenlty set format is used.

See also:: PropDb_set_print_fmt

Prop_ptr PropDb_get_prop_at_index	(	const PropDb_ptr	self,
		int	num
	)			`[related]`

Returns the property indexed by index.

Returns the property whose unique identifier is provided in input. Returns NULL if not found.

int PropDb_get_prop_index_from_string	(	const PropDb_ptr	self,
		const char *	idx
	)			`[related]`

Get a valid property index from a string.

Gets the index of a property form a string. If the string does not contain a valid index, an error message is emitted and -1 is returned.

int PropDb_get_prop_index_from_trace_index	(	const PropDb_ptr	self,
		const int	trace_idx
	)			`[related]`

Returns the index of the property associated to a trace.

Returns the index of the property associated to a trace. -1 if no property is associated to the given trace.

int PropDb_get_prop_name_index	(	const PropDb_ptr	self,
		const node_ptr	name
	)			`[related]`

Returns the property with the given name.

Returns the property with the given name, rapresented as flattened nodes hierarchy, -1 if not found.

Set_t PropDb_get_props_at_indices	(	const PropDb_ptr	self,
		const ErrorMgr_ptr	errmgr,
		const char *	indices
	)			`[related]`

Produces a set of properties from a delimited string containing properties indices.

Indices are names separated by ':' or ',' A range can be specified with 'A-B' where B >= A. This can be handy in commands.

In case of error in input, an exception is raised.

Returned set must be disposed by the caller

lsList PropDb_get_props_of_type	(	const PropDb_ptr	self,
		const Prop_Type	type
	)			`[related]`

Return the list of properties of a given type Returned list to be disposed by the caller.

int PropDb_get_size ( const PropDb_ptr self ) [related]

Returns the size of the DB.

Returns the size (i.e. the number of entries) stored in the DB of properties.

boolean PropDb_is_prop_registered	(	PropDb_ptr	self,
		Prop_ptr	prop
	)			`[related]`

Checks if "prop" is registered within self.

void PropDb_ordered_verify_all	(	const PropDb_ptr	self,
		const FlatHierarchy_ptr	hierarchy
	)			`[related]`

Verifies all the properties in the DB.

All the properties stored in the database not yet verified will be verified. The properties are verified following the COI size order (from smaller to bigger)

void PropDb_ordered_verify_all_type	(	const PropDb_ptr	self,
		const FlatHierarchy_ptr	hierarchy,
		const Prop_Type	type
	)			`[related]`

Verifies all properties of a given type, ordered by COI size.

The DB of properties is searched for a property of the given type. All the found properties are then verified calling the appropriate model checking algorithm. Properties already checked will be ignored. Properties found with the given type are checked in order, based on the COI size. If type is Prop_NoType, all properties are checked

lsList PropDb_prepare_prop_list	(	const PropDb_ptr	self,
		const Prop_Type	type
	)			`[related]`

Wrapper for PropDb_get_ordered_props_of_type, PropDb_get_props_of_type.

Call the correct PropDb_get...props_of_type depending on opt_use_coi_size_sorting. the list must be freed by the user.

void PropDb_print_all	(	const PropDb_ptr	self,
		OStream_ptr	file
	)			`[related]`

Prints all the properties stored in the DB.

Prints on the given file stream all the property stored in the DB of properties.

void PropDb_print_all_status	(	const PropDb_ptr	self,
		OStream_ptr	file,
		Prop_Status	status
	)			`[related]`

Prints all the properties stored in the DB.

Prints on the given file stream all the property stored in the DB of properties whose status match the requested one.

void PropDb_print_all_status_type	(	const PropDb_ptr	self,
		OStream_ptr	file,
		Prop_Status	status,
		Prop_Type	type
	)			`[related]`

Prints all the properties stored in the DB.

Prints on the given file stream all the property stored in the DB of properties whose type and status match the requested ones. Prop_NoStatus and Prop_NoType serve as wildcards.

void PropDb_print_all_type	(	const PropDb_ptr	self,
		OStream_ptr	file,
		Prop_Type	type
	)			`[related]`

Prints all the properties stored in the DB.

Prints on the given file stream all the property stored in the DB of properties whose type match the requested one.

void PropDb_print_list_footer	(	const PropDb_ptr	self,
		OStream_ptr	file
	)			`[related]`

Prints the footer of the property list.

This method has to be called after PropDb_print_list_header.

PropDb_print_list_header

void PropDb_print_list_header	(	const PropDb_ptr	self,
		OStream_ptr	file
	)			`[related]`

Prints the header of the property list.

This method has to be called before PropDb_print_list_footer.

PropDb_print_list_footer

int PropDb_print_prop_at_index	(	const PropDb_ptr	self,
		OStream_ptr	file,
		const int	index
	)			`[related]`

Todo:

int PropDb_prop_create_and_add	(	PropDb_ptr	self,
		SymbTable_ptr	symb_table,
		node_ptr	,
		Prop_Type
	)			`[related]`

Inserts a property in the DB of properties.

Given a formula and its type, a property is created and stored in the DB of properties. It returns either -1 in case of failure, or the index of the inserted property.

int PropDb_prop_parse_and_add	(	const PropDb_ptr	self,
		SymbTable_ptr	symb_table,
		const char *	str,
		const Prop_Type	type,
		const node_ptr	expr_name
	)			`[related]`

Add a property to the database from a string and a type.

Parses and creates a property of a given type from a string. If the formula is correct, it is added to the property database and its index is returned. Otherwise, -1 is returned. Valid types are Prop_Ctl, Prop_Ltl, Prop_Psl, Prop_Invar and Prop_Compute. If expr_name is not NULL, it is set as the name of the property.

int PropDb_prop_parse_name	(	const PropDb_ptr	self,
		const char *	str
	)			`[related]`

Given a string representing a property name, returns the property index, if it exists.

Parses the given name, builds it's node_ptr interpretation and looks into the PropDb if the property exists.

See also:: PropDb_get_prop_name_index

PropDb_PrintFmt PropDb_set_print_fmt	(	const PropDb_ptr	self,
		PropDb_PrintFmt	new_fmt
	)			`[related]`

Sets the current print format.

When printing, the given format will be used. Returns the previously set format.

See also:: PropDb_get_print_fmt

int PropDb_show_property	(	const PropDb_ptr	self,
		const boolean	print_props_num,
		const PropDb_PrintFmt	fmt,
		const Prop_Type	type,
		const Prop_Status	status,
		const int	prop_no,
		FILE *	outstream
	)			`[related]`

Shows the currently stored properties.

Shows the currently stored properties. If type is Prop_NoType, all properties will be printed. If status is Prop_NoStatus, all status will be considered.

void PropDb_verify_all ( const PropDb_ptr self ) [related]

Verifies all the properties in the DB.

All the properties stored in the database not yet verified will be verified. The properties are verified following the order CTL/COMPUTE/LTL/INVAR.

void PropDb_verify_all_type	(	const PropDb_ptr	self,
		Prop_Type
	)			`[related]`

Verifies all properties of a given type.

The DB of properties is searched for a property of the given type. All the found properties are then verified calling the appropriate model checking algorithm. Properties already checked will be ignored.

void PropDb_verify_prop_at_index	(	const PropDb_ptr	self,
		const int	index
	)			`[related]`

Verifies a given property.

The DB of properties is searched for a property whose unique identifier match the identifier provided and then if such a property exists it will be verified calling the appropriate model checking algorithm. If the property was checked before, then the property is not checked again.

Field Documentation

PropDb_PrintFmt PropDb::print_fmt

PropDb_prop_create_and_add_method PropDb::prop_create_and_add

array_t* PropDb::prop_database

PropDb_verify_all_method PropDb::verify_all

The documentation for this struct was generated from the following files:

NuSMV/code/nusmv/core/prop/PropDb_private.h
NuSMV/code/nusmv/core/prop/PropDb.h

PropDb Struct Reference

Public Member Functions

Data Fields

Related Functions

Detailed Description

Member Function Documentation

Friends And Related Function Documentation

Field Documentation