Cluster Struct Reference

The header file of trans cluster class. More...

#include <Cluster.h>

Related Functions
(Note that these are not member functions.)
Cluster_ptr	Cluster_create (DDMgr_ptr dd)
	The "Cluster" class constructor.
bdd_ptr	Cluster_get_quantification_state (const Cluster_ptr self)
	Returns a pointer to the list of variables (state vars only) to be quantified.
bdd_ptr	Cluster_get_quantification_state_input (const Cluster_ptr self)
	Returns a pointer to the list of variables (both state and input vars) to be quantified.
bdd_ptr	Cluster_get_trans (const Cluster_ptr self)
	Retrives the clusterized transition relation of the self
boolean	Cluster_is_equal (const Cluster_ptr self, const Cluster_ptr other)
	Checks if two clusters are equal.
void	Cluster_set_quantification_state (Cluster_ptr self, DDMgr_ptr dd, bdd_ptr new_val)
	Sets the list of variables (state vars only) to be quantified inside the cluster.
void	Cluster_set_quantification_state_input (Cluster_ptr self, DDMgr_ptr dd, bdd_ptr new_val)
	Sets the list of variables (both state and input vars) to be quantified inside the cluster.
void	Cluster_set_trans (Cluster_ptr self, DDMgr_ptr dd, bdd_ptr current)
	Sets the transition relation inside the cluster.

---

Detailed Description

The header file of trans cluster class.

Author:

Roberto Cavada

Todo:

: Missing description

Cluster Class This class contains informations about a cluster:

curr_cluster

The clusterized transition relation.

ex_state_input

List of variables (state and input vars) that can be existentially quantified when curr_cluster is multiplied in the product.

ex_state

List of variables (only state vars) that can be existentially quantified when curr_cluster is multiplied in the product.

Note that frozen variables are not taken into account because they are never abstracted away (or used some other way) in pre- or post-image computation.
In addition, this class inherits from the Object class and contains a virtual copy constructor.

---

Friends And Related Function Documentation

Cluster_ptr Cluster_create

(

DDMgr_ptr

dd

)

[related]

The "Cluster" class constructor.

Allocates and initializes a cluster.

See also:

Object_destroy

bdd_ptr Cluster_get_quantification_state

(

const Cluster_ptr

self

)

[related]

Returns a pointer to the list of variables (state vars only) to be quantified.

Returned value is referenced

bdd_ptr Cluster_get_quantification_state_input

(

const Cluster_ptr

self

)

[related]

Returns a pointer to the list of variables (both state and input vars) to be quantified.

Returns a pointer to the list of variables to be quantified respect to the transition relation inside the cluster. Returned bdd is referenced.

bdd_ptr Cluster_get_trans

(

const Cluster_ptr

self

)

[related]

Retrives the clusterized transition relation of the self

Returned bdd will be referenced

boolean Cluster_is_equal	(	const Cluster_ptr	self,
		const Cluster_ptr	other
	)			[related]

Checks if two clusters are equal.

Notice that the check is performed only using the \"curr_cluster\" field of the Cluster class.

void Cluster_set_quantification_state	(	Cluster_ptr	self,
		DDMgr_ptr	dd,
		bdd_ptr	new_val
	)			[related]

Sets the list of variables (state vars only) to be quantified inside the cluster.

Given value will be referenced

void Cluster_set_quantification_state_input	(	Cluster_ptr	self,
		DDMgr_ptr	dd,
		bdd_ptr	new_val
	)			[related]

Sets the list of variables (both state and input vars) to be quantified inside the cluster.

Given value will be referenced

void Cluster_set_trans	(	Cluster_ptr	self,
		DDMgr_ptr	dd,
		bdd_ptr	current
	)			[related]

Sets the transition relation inside the cluster.

The given bdd will be referenced. Previously stored bdd will be released

---

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

• NuSMV/code/nusmv/core/trans/bdd/Cluster.h