NuSMV/code/nusmv/core/hrc/HrcFlattener.h File Reference

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/hrc/HrcNode.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/compile/FlatHierarchy.h"
#include "nusmv/core/fsm/sexp/SexpFsm.h"
#include "nusmv/core/hrc/hrc.h"

Go to the source code of this file.

Defines
#define	HRC_FLATTENER(self)   ((HrcFlattener_ptr) self)
	To cast and check instances of class HrcFlattener.
#define	HRC_FLATTENER_CHECK_INSTANCE(self)   (nusmv_assert(HRC_FLATTENER(self) != HRC_FLATTENER(NULL)))
Typedefs
typedef struct HrcFlattener_TAG *	HrcFlattener_ptr
Functions
FlatHierarchy_ptr	HrcToFlatHierarchy (const NuSMVEnv_ptr env, HrcNode_ptr node, SymbTable_ptr symb_table, SymbLayer_ptr layer)
	HrcFlattener main routine.
SexpFsm_ptr	HrcToSexpFsm (const NuSMVEnv_ptr env, HrcNode_ptr node, SymbTable_ptr symb_table, SymbLayer_ptr layer)
	HrcFlattener main routine.

---

Define Documentation

#define HRC_FLATTENER

(

self

)

((HrcFlattener_ptr) self)

To cast and check instances of class HrcFlattener.

These macros must be used respectively to cast and to check instances of class HrcFlattener

#define HRC_FLATTENER_CHECK_INSTANCE

(

self

)

(nusmv_assert(HRC_FLATTENER(self) != HRC_FLATTENER(NULL)))

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef struct HrcFlattener_TAG* HrcFlattener_ptr

---

Function Documentation

FlatHierarchy_ptr HrcToFlatHierarchy	(	const NuSMVEnv_ptr	env,
		HrcNode_ptr	node,
		SymbTable_ptr	symb_table,
		SymbLayer_ptr	layer
	)

HrcFlattener main routine.

AutomaticStart

HrcFlattener top-level function. Given an Hrc hierarchy and a symbol table (and eventually a symbol layer), creates and returns a flat hierarchy. Parameter layer can be NULL. Is so, a new layer belonging to the given symbol table is created. If not NULL, the layer must belong to the given symbol table

See also:

HrcFlattener_create

SexpFsm_ptr HrcToSexpFsm	(	const NuSMVEnv_ptr	env,
		HrcNode_ptr	node,
		SymbTable_ptr	symb_table,
		SymbLayer_ptr	layer
	)

HrcFlattener main routine.

HrcFlattener top-level function. Given an Hrc hierarchy and a symbol table (and eventually a symbol layer), creates and returns a sexpfsm. Parameter layer can be NULL. Is so, a new layer belonging to the given symbol table is created. If not NULL, the layer must belong to the given symbol table

Adds new symbols to the given symbol table

See also:

HrcFlattener_create