Be_Manager Struct Reference

The private interface of the Be_Manager class. More...

#include <beManagerInt.h>

Data Fields
Be_Be2Spec_fun	be2spec_converter
NuSMVEnv_ptr	environment
Be_Spec2Be_fun	spec2be_converter
void *	spec_manager
void *	support_data
Related Functions
(Note that these are not member functions.)
void *	Be_Manager_Be2Spec (const Be_Manager_ptr self, be_ptr be)
	Converts a generic BE into a specific-format boolean expression (for example in rbc format).
Be_Manager_ptr	Be_Manager_Create (const NuSMVEnv_ptr env, void *spec_manager, Be_Spec2Be_fun spec2be_converter, Be_Be2Spec_fun be2spec_converter)
	Creates a generic Be_Manager.
void	Be_Manager_Delete (Be_Manager_ptr self)
	Be_Manager destroyer.
void *	Be_Manager_GetData (const Be_Manager_ptr self)
	Derived classes data can be retrieved by this method.
NuSMVEnv_ptr	Be_Manager_GetEnvironment (const Be_Manager_ptr self)
	Private service of MSatEnc_term_to_expr.
void *	Be_Manager_GetSpecManager (Be_Manager_ptr self)
	Gets the specific manager under the be manager.
void	Be_Manager_SetData (Be_Manager_ptr self, void *data)
	Sets specific structure manager data into the generic manager.
be_ptr	Be_Manager_Spec2Be (const Be_Manager_ptr self, void *spec_expr)
	Converts a specific-format boolean expression (for example in rbc format) into a generic BE.

Detailed Description

The private interface of the Be_Manager class.

Author:: Roberto Cavada This interface is privately used into this package only. Be_Manager can be considered as a "virtual base class" which must be instantiated via inheritance by more specific classes whose implementations depend on the real low-level structure them use (i.e. the rbc manager) Files beRbc.{h,c} define and implement the derived class which implements the RBC layer. Look at them as a possible template and example.

The generic Boolean Expressions Manager (private declaration) To access this structure you must use the Be_Manager_ptr type.

See also:: Be_Manager_ptr

Friends And Related Function Documentation

void * Be_Manager_Be2Spec	(	const Be_Manager_ptr	self,
		be_ptr	be
	)			`[related]`

Converts a generic BE into a specific-format boolean expression (for example in rbc format).

See also:: Be_Manager_Spec2Be

Be_Manager_ptr Be_Manager_Create	(	const NuSMVEnv_ptr	env,
		void *	spec_manager,
		Be_Spec2Be_fun	spec2be_converter,
		Be_Be2Spec_fun	be2spec_converter
	)			`[related]`

Creates a generic Be_Manager.

AutomaticStart

spec_manager is the specific structure which is used to manage the low-level structure. For example the RbcManager class in the RBC dependant implementation. This does not assume the ownership of 'spec_manager'. If you have dynamically created the spec_manager instance, you are responsible for deleting it after you deleted the Be_manager instance. This "virtual" function is supplied in order to be called by any specific class derived from Be_Manager, in its constructor code. spec2be and be2spec converters are gateways in order to polymorphically convert the low level support structure (for example a rbc pointer) to the generic be_ptr and viceversa.

See also:: Be_RbcManager_Create, Be_Manager_Delete

void Be_Manager_Delete ( Be_Manager_ptr self ) [related]

Be_Manager destroyer.

Call this function from the destructor of the derived class that implements the Be_Manager class. Any other use is to be considered unusual.

self will be deleted from memory.

See also:: Be_RbcManager_Delete, Be_Manager_Create

void * Be_Manager_GetData ( const Be_Manager_ptr self ) [related]

Derived classes data can be retrieved by this method.

When you instantiate a derived BE manager (for example the rbc manager) you can store any useful specific data by using Be_Manager_SetData. Those data can be lately retrieved by Be_Manager_GetData which gets a generic, structure-independent Be_Manager.

See also:: Be_Manager_SetData

NuSMVEnv_ptr Be_Manager_GetEnvironment ( const Be_Manager_ptr self ) [related]

Private service of MSatEnc_term_to_expr.

Private service of MSatEnc_term_to_expr

void * Be_Manager_GetSpecManager ( Be_Manager_ptr self ) [related]

Gets the specific manager under the be manager.

Gets the specific manager under the be manager

void Be_Manager_SetData	(	Be_Manager_ptr	self,
		void *	data
	)			`[related]`

Sets specific structure manager data into the generic manager.

You can retieve saved data by using the method Be_Manager_GetData. This implements a kind of inheritance mechanism.

self will change its internal state.

See also:: Be_Manager_GetData

be_ptr Be_Manager_Spec2Be	(	const Be_Manager_ptr	self,
		void *	spec_expr
	)			`[related]`

Converts a specific-format boolean expression (for example in rbc format) into a generic BE.

Calls self->spec2be_converter in order to implement the polymorphism mechanism

Calls self->be2spec_converter in order to implement the polymorphism mechanism

See also:: Be_Manager_Be2Spec

Field Documentation

Be_Be2Spec_fun Be_Manager::be2spec_converter

NuSMVEnv_ptr Be_Manager::environment

Be_Spec2Be_fun Be_Manager::spec2be_converter

void* Be_Manager::spec_manager

void* Be_Manager::support_data

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

NuSMV/code/nusmv/core/be/beManagerInt.h
NuSMV/code/nusmv/core/be/be.h

Be_Manager Struct Reference

Data Fields

Related Functions

Detailed Description

Friends And Related Function Documentation

Field Documentation