Public interface of class 'HrcFlattener'. More...
#include <HrcFlattener.h>
Related Functions | |
(Note that these are not member functions.) | |
| HrcFlattener_ptr | HrcFlattener_create (const NuSMVEnv_ptr env, HrcNode_ptr node, SymbTable_ptr symb_table, SymbLayer_ptr layer) |
| The HrcFlattener class constructor. | |
| void | HrcFlattener_destroy (HrcFlattener_ptr self) |
| The HrcFlattener class destructor. | |
| void | HrcFlattener_flatten_hierarchy (HrcFlattener_ptr self) |
| Does the actual flattening. | |
| FlatHierarchy_ptr | HrcFlattener_get_flat_hierarchy (HrcFlattener_ptr self) |
| Get the built flat hierarchy. | |
| SymbLayer_ptr | HrcFlattener_get_symbol_layer (HrcFlattener_ptr self) |
| Get the symbol layer. | |
| SymbTable_ptr | HrcFlattener_get_symbol_table (HrcFlattener_ptr self) |
| Get the symbol table. | |
| void | HrcFlattener_populate_symbol_table (HrcFlattener_ptr self) |
| Fills the symbol table without building any flat hierarchy. | |
| void | HrcFlattener_write_flatten_model (HrcFlattener_ptr self, FILE *out) |
| Dumps the flatten model on file "out". | |
Public interface of class 'HrcFlattener'.
Definition of the public accessor for class HrcFlattener
| HrcFlattener_ptr HrcFlattener_create | ( | const NuSMVEnv_ptr | env, | |
| HrcNode_ptr | node, | |||
| SymbTable_ptr | symb_table, | |||
| SymbLayer_ptr | layer | |||
| ) | [related] |
The HrcFlattener class constructor.
The HrcFlattener class constructor. 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. The given hrc node must be the top-level node. Hrc Localize methods should be used first if trying to flatten an instance which is not the main one
| void HrcFlattener_destroy | ( | HrcFlattener_ptr | self | ) | [related] |
| void HrcFlattener_flatten_hierarchy | ( | HrcFlattener_ptr | self | ) | [related] |
Does the actual flattening.
This method does the actual flattening job. Takes the input hrc node and processes it in 2 steps: in the first step a first version of the hierarchy is build, where expressions are just contextualized but not flattened. After this Compile_ProcessHierarchy is called and the actual flat hierachy is built. The symbol table is also filled
| FlatHierarchy_ptr HrcFlattener_get_flat_hierarchy | ( | HrcFlattener_ptr | self | ) | [related] |
Get the built flat hierarchy.
Get the internally built flat hierarchy. The hierarchy is populated only if HrcFlattener_flatten_hierarchy was previously called
| SymbLayer_ptr HrcFlattener_get_symbol_layer | ( | HrcFlattener_ptr | self | ) | [related] |
Get the symbol layer.
Gets the internally populated symbol layer. The layer is populated only if HrcFlattener_flatten_hierarchy was previously called
| SymbTable_ptr HrcFlattener_get_symbol_table | ( | HrcFlattener_ptr | self | ) | [related] |
Get the symbol table.
Gets the internally populated symbol table. The st is populated only if HrcFlattener_flatten_hierarchy was previously called
| void HrcFlattener_populate_symbol_table | ( | HrcFlattener_ptr | self | ) | [related] |
Fills the symbol table without building any flat hierarchy.
Fills the symbol table without building any flat hierarchy
| void HrcFlattener_write_flatten_model | ( | HrcFlattener_ptr | self, | |
| FILE * | out | |||
| ) | [related] |
Dumps the flatten model on file "out".
Dumps the flatten model on file "out"
1.6.1
