ClusterList Struct Reference

The header file of ClusterList class. More...

#include <ClusterList.h>

Related Functions
(Note that these are not member functions.)
void	ClusterList_append_cluster (ClusterList_ptr self, Cluster_ptr cluster)
	Appends given cluster to the list.
ClusterList_ptr	ClusterList_apply_iwls95_partition (const ClusterList_ptr self, bdd_ptr state_vars_cube, bdd_ptr input_vars_cube, bdd_ptr next_state_vars_cube, const ClusterOptions_ptr cl_options)
	Orders the clusters according to the IWLS95 algo. to perform image computation.
ClusterList_ptr	ClusterList_apply_monolithic (const ClusterList_ptr self)
	It returns a monolithic transition cluster corresponding to the cluster list of the "self".
void	ClusterList_apply_synchronous_product (ClusterList_ptr self, const ClusterList_ptr other)
	Performs the synchronous product between two cluster lists.
ClusterList_ptr	ClusterList_apply_threshold (const ClusterList_ptr self, const ClusterOptions_ptr cl_options)
	It returns a threshold based cluster list corresponding to the cluster list of the "self".
ClusterListIterator_ptr	ClusterList_begin (const ClusterList_ptr self)
	Returns an Iterator to iterate the self.
void	ClusterList_build_schedule (ClusterList_ptr self, bdd_ptr state_vars_cube, bdd_ptr input_vars_cube)
	It builds the quantification schedule of the variables inside the clusters of the "self".
boolean	ClusterList_check_equality (const ClusterList_ptr self, const ClusterList_ptr other)
	Returns true if two clusters list are logically equivalent.
boolean	ClusterList_check_schedule (const ClusterList_ptr self)
	Check the schedule for self. Call after you applied the schedule.
ClusterList_ptr	ClusterList_copy (const ClusterList_ptr self)
	Returns a copy of the "self".
ClusterList_ptr	ClusterList_create (DDMgr_ptr dd)
	Class ClusterList Constructor.
void	ClusterList_destroy (ClusterList_ptr self)
	ClusterList Class dectructor.
Cluster_ptr	ClusterList_get_cluster (const ClusterList_ptr self, const ClusterListIterator_ptr iter)
	Returns the cluster kept at the position given by the iterator.
bdd_ptr	ClusterList_get_clusters_cube (const ClusterList_ptr self)
	Computes the cube of the set of support of all the clusters.
DDMgr_ptr	ClusterList_get_dd_manager (const ClusterList_ptr self)
	Returns an Iterator to iterate the self.
bdd_ptr	ClusterList_get_image_state (const ClusterList_ptr self, bdd_ptr s)
	Computes the image of the given bdd "s" using the clusters of the "self" while quantifying state vars only.
bdd_ptr	ClusterList_get_image_state_input (const ClusterList_ptr self, bdd_ptr s)
	Computes the image of the given bdd "s" using the clusters of the "self" while quantifying both state and input vars.
bdd_ptr	ClusterList_get_k_image_state (const ClusterList_ptr self, bdd_ptr s, int k)
	Computes the k image of the given bdd "s" using the clusters of the "self" while quantifying state vars only.
bdd_ptr	ClusterList_get_k_image_state_input (const ClusterList_ptr self, bdd_ptr s, int k)
	Computes the k image of the given bdd "s" using the clusters of the "self" while quantifying both state and input vars.
bdd_ptr	ClusterList_get_monolithic_bdd (const ClusterList_ptr self)
	Returns the monolithic bdd corresponding to the "self".
int	ClusterList_length (const ClusterList_ptr self)
	Returns the number of the clusters stored in "self".
void	ClusterList_prepend_cluster (ClusterList_ptr self, Cluster_ptr cluster)
	Prepends given cluster to the list.
void	ClusterList_print_short_info (const ClusterList_ptr self, FILE *file)
	Prints size of each cluster of the "self".
int	ClusterList_remove_cluster (ClusterList_ptr self, Cluster_ptr cluster)
	Deletes every occurrence of the given cluster from the self.
void	ClusterList_reverse (ClusterList_ptr self)
	Reverses the list of clusters.
void	ClusterList_set_cluster (ClusterList_ptr self, const ClusterListIterator_ptr iter, Cluster_ptr cluster)
	Sets the cluster of the "self" at the position given by iterator "iter" to cluster "cluster".

Detailed Description

The header file of ClusterList class.

Author:: Roberto Cavada

ClusterList Class. This class forms a list of clusters.

Friends And Related Function Documentation

void ClusterList_append_cluster	(	ClusterList_ptr	self,
		Cluster_ptr	cluster
	)			`[related]`

Appends given cluster to the list.

List becomes the owner of the given cluster, if the user is going to call standard destructor

ClusterList_ptr ClusterList_apply_iwls95_partition	(	const ClusterList_ptr	self,
		bdd_ptr	state_vars_cube,
		bdd_ptr	input_vars_cube,
		bdd_ptr	next_state_vars_cube,
		const ClusterOptions_ptr	cl_options
	)			`[related]`

Orders the clusters according to the IWLS95 algo. to perform image computation.

This function builds the data structures to perform image computation.
This process consists of the following steps:

Ordering of the clusters given as input accordingly with the heuristic described in IWLS95.
Clustering of the result of previous step accordingly the threshold value stored in the option \"image_cluster_size\".
Ordering of the result of previous step accordingly with the heuristic described in IWLS95.

ClusterList_ptr ClusterList_apply_monolithic ( const ClusterList_ptr self ) [related]

It returns a monolithic transition cluster corresponding to the cluster list of the "self".

"self" remains unchanged.

void ClusterList_apply_synchronous_product	(	ClusterList_ptr	self,
		const ClusterList_ptr	other
	)			`[related]`

Performs the synchronous product between two cluster lists.

All clusters into other are simply appended to "self". The result goes into "self", no changes on other. The scheduling is done with the variables from both cluster lists. Precondition: both lists should have scheduling done.

self will change

ClusterList_ptr ClusterList_apply_threshold	(	const ClusterList_ptr	self,
		const ClusterOptions_ptr	cl_options
	)			`[related]`

It returns a threshold based cluster list corresponding to the cluster list of the "self".

"self" remains unchanged.

ClusterListIterator_ptr ClusterList_begin ( const ClusterList_ptr self ) [related]

Returns an Iterator to iterate the self.

void ClusterList_build_schedule	(	ClusterList_ptr	self,
		bdd_ptr	state_vars_cube,
		bdd_ptr	input_vars_cube
	)			`[related]`

It builds the quantification schedule of the variables inside the clusters of the "self".

boolean ClusterList_check_equality	(	const ClusterList_ptr	self,
		const ClusterList_ptr	other
	)			`[related]`

Returns true if two clusters list are logically equivalent.

It compares BDDs not Clusters.

boolean ClusterList_check_schedule ( const ClusterList_ptr self ) [related]

Check the schedule for self. Call after you applied the schedule.

Let Ci and Ti be the ith cube and relation in the list. The schedule is correct iff

For all Tj: j > i, S(Tj) and S(Ci) do not intersect, i.e., the variables which are quantified in Ci should not appear in the Tj for j>i.

where S(T) is the set of support of the BDD T. Returns true if the schedule is correct, false otherwise. This function is implemented for checking the correctness of the clustering algorithm only.
This function returns true if schedule is correct, false otherwise.

ClusterList_ptr ClusterList_copy ( const ClusterList_ptr self ) [related]

Returns a copy of the "self".

Duplicates self and each cluster inside it.

ClusterList_ptr ClusterList_create ( DDMgr_ptr dd ) [related]

Class ClusterList Constructor.

The reference to DdManager passed here is internally stored but self does not become owner of it.

void ClusterList_destroy ( ClusterList_ptr self ) [related]

ClusterList Class dectructor.

Destroys the cluster list and all cluster instances inside it.

Cluster_ptr ClusterList_get_cluster	(	const ClusterList_ptr	self,
		const ClusterListIterator_ptr	iter
	)			`[related]`

Returns the cluster kept at the position given by the iterator.

self keeps the ownership of the returned cluster

bdd_ptr ClusterList_get_clusters_cube ( const ClusterList_ptr self ) [related]

Computes the cube of the set of support of all the clusters.

Given a list of clusters, it computes their set of support. Returned bdd is referenced.

DDMgr_ptr ClusterList_get_dd_manager ( const ClusterList_ptr self ) [related]

Returns an Iterator to iterate the self.

bdd_ptr ClusterList_get_image_state	(	const ClusterList_ptr	self,
		bdd_ptr	s
	)			`[related]`

Computes the image of the given bdd "s" using the clusters of the "self" while quantifying state vars only.

Returned bdd is referenced

bdd_ptr ClusterList_get_image_state_input	(	const ClusterList_ptr	self,
		bdd_ptr	s
	)			`[related]`

Computes the image of the given bdd "s" using the clusters of the "self" while quantifying both state and input vars.

Returned bdd is referenced

bdd_ptr ClusterList_get_k_image_state	(	const ClusterList_ptr	self,
		bdd_ptr	s,
		int	k
	)			`[related]`

Computes the k image of the given bdd "s" using the clusters of the "self" while quantifying state vars only.

Returned bdd is referenced

bdd_ptr ClusterList_get_k_image_state_input	(	const ClusterList_ptr	self,
		bdd_ptr	s,
		int	k
	)			`[related]`

Computes the k image of the given bdd "s" using the clusters of the "self" while quantifying both state and input vars.

Returned bdd is referenced

bdd_ptr ClusterList_get_monolithic_bdd ( const ClusterList_ptr self ) [related]

Returns the monolithic bdd corresponding to the "self".

The returned bdd is referenced

int ClusterList_length ( const ClusterList_ptr self ) [related]

Returns the number of the clusters stored in "self".

void ClusterList_prepend_cluster	(	ClusterList_ptr	self,
		Cluster_ptr	cluster
	)			`[related]`

Prepends given cluster to the list.

List becomes the owner of the given cluster

void ClusterList_print_short_info	(	const ClusterList_ptr	self,
		FILE *	file
	)			`[related]`

Prints size of each cluster of the "self".

int ClusterList_remove_cluster	(	ClusterList_ptr	self,
		Cluster_ptr	cluster
	)			`[related]`

Deletes every occurrence of the given cluster from the self.

Returns the number of removed occurrences. Clusters found won't be destroyed, simply their references will be removed from the list

void ClusterList_reverse ( ClusterList_ptr self ) [related]

Reverses the list of clusters.

void ClusterList_set_cluster	(	ClusterList_ptr	self,
		const ClusterListIterator_ptr	iter,
		Cluster_ptr	cluster
	)			`[related]`

Sets the cluster of the "self" at the position given by iterator "iter" to cluster "cluster".

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

NuSMV/code/nusmv/core/trans/bdd/ClusterList.h

ClusterList Struct Reference

Related Functions

Detailed Description

Friends And Related Function Documentation