The class is used to store results of flattening a hierarchy. More...
#include <FlatHierarchy.h>
Related Functions | |
(Note that these are not member functions.) | |
| void | FlatHierarchy_add_constant_constrains (FlatHierarchy_ptr self, node_ptr expr, int type) |
| Adds the given expressions to the list of constrains associated to constants. | |
| void | FlatHierarchy_add_constrains (FlatHierarchy_ptr self, node_ptr name, node_ptr expr) |
| Adds the given expressions to the list of constrains associated to the given variable. | |
| void | FlatHierarchy_calculate_vars_constrains (FlatHierarchy_ptr self) |
| Creates association between variables and all the expressions the variables occur in. | |
| void | FlatHierarchy_clear_constants_associations (FlatHierarchy_ptr self) |
| Clears the association between hierarchy sections and constant expressions. | |
| void | FlatHierarchy_clear_var_expr_associations (FlatHierarchy_ptr self) |
| This function cleans the association between a variable name and expressions the variable is used in. | |
| FlatHierarchy_ptr | FlatHierarchy_copy (const FlatHierarchy_ptr self) |
| Returns a newly created instance that is a copy of self. | |
| FlatHierarchy_ptr | FlatHierarchy_create (SymbTable_ptr st) |
| The constructor. | |
| FlatHierarchy_ptr | FlatHierarchy_create_from_members (SymbTable_ptr st, node_ptr init, node_ptr invar, node_ptr trans, node_ptr input, node_ptr justice, node_ptr compassion) |
| Class FlatHierarcy destructorUtility constructor. | |
| void | FlatHierarchy_destroy (FlatHierarchy_ptr self) |
| Class FlatHierarcy destructor. | |
| hash_ptr | FlatHierarchy_get_constants_associations (FlatHierarchy_ptr self) |
| This function returns the hash table storing the association between the hierarchy section and constants expressions. | |
| NuSMVEnv_ptr | FlatHierarchy_get_environment (const FlatHierarchy_ptr self) |
| Returns the Flat Hierarchy SymbolTable's environment. | |
| NodeList_ptr | FlatHierarchy_get_ordered_vars (const FlatHierarchy_ptr self, hash_ptr *outbound_edges) |
| Returns an ordered list of variables. | |
| SymbTable_ptr | FlatHierarchy_get_symb_table (const FlatHierarchy_ptr self) |
| Returns the associated symbol table. | |
| hash_ptr | FlatHierarchy_get_var_expr_associations (FlatHierarchy_ptr self) |
| This function returns the hash table storing the association between a variable name and expressions the variable is used in. | |
| void | FlatHierarchy_insert_assign (FlatHierarchy_ptr self, node_ptr name, node_ptr assign) |
| Insert the right handside of an assignment which has "name" as the left handside. | |
| node_ptr | FlatHierarchy_lookup_assign (FlatHierarchy_ptr self, node_ptr name) |
| Returns the right handside of an assignment which has "name" as the left handside. | |
| node_ptr | FlatHierarchy_lookup_constant_constrains (FlatHierarchy_ptr self, int type) |
| Retrieves the list of constrains associated to constants. | |
| node_ptr | FlatHierarchy_lookup_constrains (FlatHierarchy_ptr self, node_ptr name) |
| Returns a list of constrains which contain a variable of the given name. | |
| void | FlatHierarchy_mergeinto (FlatHierarchy_ptr self, const FlatHierarchy_ptr other) |
| Merges the contents of other into self (leaves other intact). | |
| void | FlatHierarchy_remove_var (FlatHierarchy_ptr self, node_ptr n) |
| Remove a variable name to the list of variables declared in the given hierarchy. | |
| void | FlatHierarchy_self_check (const FlatHierarchy_ptr self) |
| Performs a self check of the instance content wrt the set of language self was declared to contain. | |
| void | FlatHierarchy_set_constants_associations (FlatHierarchy_ptr self, hash_ptr h) |
| This function sets the hash table storing the association between the hierarchy section and constants expressions. | |
| void | FlatHierarchy_set_symb_table (const FlatHierarchy_ptr self, SymbTable_ptr symb_table) |
| Returns the associated symbol table. | |
| void | FlatHierarchy_set_var_expr_associations (FlatHierarchy_ptr self, hash_ptr h) |
| This function sets the hash table storing the association between a variable name and expressions the variable is used in to h. | |
| void | FlatHierarchy_type_check (FlatHierarchy_ptr self) |
The class is used to store results of flattening a hierarchy.
Also this structure has a hash table to associate 1. a variable on the left handside of an assignment to its right handside. 2. a variable name to all constrains (INIT, TRANS, INVAR) which constain the given variable.
See FlatHierarchy_create for more info on this class.
The FlatHierarchy type The struct store info of flattened modules
| void FlatHierarchy_add_constant_constrains | ( | FlatHierarchy_ptr | self, | |
| node_ptr | expr, | |||
| int | type | |||
| ) | [related] |
Adds the given expressions to the list of constrains associated to constants.
Adds the given expressions to the list of constrains associated to constants. Type must be one of "INIT, INVAR or TRANS"
| void FlatHierarchy_add_constrains | ( | FlatHierarchy_ptr | self, | |
| node_ptr | name, | |||
| node_ptr | expr | |||
| ) | [related] |
Adds the given expressions to the list of constrains associated to the given variable.
The parameter "name" can be a usual variable name then an expression is expected to be INVAR body. The parameter "name" can have a form init(var-name) then an expression is expected to be INIT body. The parameter "name" can have a form next(var-name) then an expression is expected to be TRANS body.
In any case the variable name should be fully resolved (and created with find_node).
NB: All given expressions should have been declared in the given hierarchy.
| void FlatHierarchy_calculate_vars_constrains | ( | FlatHierarchy_ptr | self | ) | [related] |
Creates association between variables and all the expressions the variables occur in.
For every variable var-name in the given expressions the function creates association between: 1. var-name and and the INVAR expression list the variable occur. 2. init(var-name) and INIT expression list 3. next(var-name) and TRANS expression list. The result is remembered by flatHierarchy.
The function compileFlattenProcess works similarly but with assignments.
| void FlatHierarchy_clear_constants_associations | ( | FlatHierarchy_ptr | self | ) | [related] |
Clears the association between hierarchy sections and constant expressions.
Clears the association between hierarchy sections and constant expressions
| void FlatHierarchy_clear_var_expr_associations | ( | FlatHierarchy_ptr | self | ) | [related] |
This function cleans the association between a variable name and expressions the variable is used in.
Practically, this function cleans association created by FlatHierarchy_insert_assign and FlatHierarchy_add_constrains such that functions FlatHierarchy_lookup_assign and FlatHierarchy_lookup_constrains will return Nil for any var name.
Note: you should know what you are doing when invoke this function since it makes COI and various checks of FSM incorrect.
| FlatHierarchy_ptr FlatHierarchy_copy | ( | const FlatHierarchy_ptr | self | ) | [related] |
Returns a newly created instance that is a copy of self.
| FlatHierarchy_ptr FlatHierarchy_create | ( | SymbTable_ptr | st | ) | [related] |
The constructor.
The class is used to store information obtained after flattening module hierarchy. These class stores: the list of TRANS, INIT, INVAR, ASSIGN, SPEC, COMPUTE, LTLSPEC, PSLSPEC, INVARSPEC, JUSTICE, COMPASSION, a full list of variables declared in the hierarchy, a hash table associating variables to their assignments and constrains.
NOTE: this structure is filled in by compileFlatten.c routines. There are a few assumptions about the content stored in this class: 1. All expressions are stored in the same order as in the input file (in module body or module instantiation order). 2. Assigns are stored as a list of pairs {process instance name, assignments in it}. 3. Variable list contains only vars declared in this hierarchy. 4. The association var->assignments should be for assignments of this hierarchy only. Note that var may potentially be from another hierarchy. For example, with Games of the GAME package an assignment in the body of one hierarchy (one player) may have on the left hand side a variable from another hierarchy (another player). See FlatHierarchy_lookup_assign, FlatHierarchy_insert_assign 5. The association var->constrains (init, trans, invar) should be for constrains of this hierarchy only. Similar to var->assignment association (see above) a variable may potentially be from another hierarchy. See FlatHierarchy_lookup_constrains, FlatHierarchy_add_constrains
| FlatHierarchy_ptr FlatHierarchy_create_from_members | ( | SymbTable_ptr | st, | |
| node_ptr | init, | |||
| node_ptr | invar, | |||
| node_ptr | trans, | |||
| node_ptr | input, | |||
| node_ptr | justice, | |||
| node_ptr | compassion | |||
| ) | [related] |
Class FlatHierarcy destructorUtility constructor.
Use this constructor to set the main hierarchy members
FlatHierarchy_create
| void FlatHierarchy_destroy | ( | FlatHierarchy_ptr | self | ) | [related] |
Class FlatHierarcy destructor.
The destoructor does not destroy the nodes given to it with access functions.
FlatHierarchy_create
| hash_ptr FlatHierarchy_get_constants_associations | ( | FlatHierarchy_ptr | self | ) | [related] |
This function returns the hash table storing the association between the hierarchy section and constants expressions.
self retains ownership of returned value. Note: you should know what you are doing when performing modifications on the table.
| NuSMVEnv_ptr FlatHierarchy_get_environment | ( | const FlatHierarchy_ptr | self | ) | [related] |
Returns the Flat Hierarchy SymbolTable's environment.
Returns the Flat Hierarchy SymbolTable's environment
| NodeList_ptr FlatHierarchy_get_ordered_vars | ( | const FlatHierarchy_ptr | self, | |
| hash_ptr * | outbound_edges | |||
| ) | [related] |
Returns an ordered list of variables.
Starting from hierarchy assignments, creates a DAG and returns the topological sort of it. The set of nodes contained in this dag is the union of the dependencies of all assings expressions of the hierarchy. If not NULL, outbound_edges will contain a map between vars and their respective outgoing edges to other variables
| SymbTable_ptr FlatHierarchy_get_symb_table | ( | const FlatHierarchy_ptr | self | ) | [related] |
Returns the associated symbol table.
| hash_ptr FlatHierarchy_get_var_expr_associations | ( | FlatHierarchy_ptr | self | ) | [related] |
This function returns the hash table storing the association between a variable name and expressions the variable is used in.
self retains ownership of returned value.
Note: you should know what you are doing when performing modifications on the table.
| void FlatHierarchy_insert_assign | ( | FlatHierarchy_ptr | self, | |
| node_ptr | name, | |||
| node_ptr | assign | |||
| ) | [related] |
Insert the right handside of an assignment which has "name" as the left handside.
The name can be a usual variable name, init(var-name) or next(var-name). The variable name should be fully resolved (and created with find_node).
NB: All given assignments should have been declared in the given hierarchy.
| node_ptr FlatHierarchy_lookup_assign | ( | FlatHierarchy_ptr | self, | |
| node_ptr | name | |||
| ) | [related] |
Returns the right handside of an assignment which has "name" as the left handside.
The name can be a usual variable name, init(variable name) or next(variable name). The name should be fully resolved (and created with find_node).
NB: All returned assignments are supposed to be declared in the given hierarchy.
| node_ptr FlatHierarchy_lookup_constant_constrains | ( | FlatHierarchy_ptr | self, | |
| int | type | |||
| ) | [related] |
Retrieves the list of constrains associated to constants.
Retrieves the list of constrains associated to constants for the given hierarchy section. Type must be one of "INIT, INVAR or TRANS"
| node_ptr FlatHierarchy_lookup_constrains | ( | FlatHierarchy_ptr | self, | |
| node_ptr | name | |||
| ) | [related] |
Returns a list of constrains which contain a variable of the given name.
If the parameter "name" is a usual variable name then the INVAR expressions are returned. If the parameter "name" has a form init(var-name) then the INIT expressions are returned. If the parameter "name" has a form next(var-name) then the TRANS expressions are returned.
The name should be fully resolved (and created with find_node).
NB: All returned expressions are supposed to be declared in the given hierarchy.
| void FlatHierarchy_mergeinto | ( | FlatHierarchy_ptr | self, | |
| const FlatHierarchy_ptr | other | |||
| ) | [related] |
Merges the contents of other into self (leaves other intact).
flat_hierarchy_mergeinto, SexpFsm_apply_synchronous_product
| void FlatHierarchy_remove_var | ( | FlatHierarchy_ptr | self, | |
| node_ptr | n | |||
| ) | [related] |
Remove a variable name to the list of variables declared in the given hierarchy.
| void FlatHierarchy_self_check | ( | const FlatHierarchy_ptr | self | ) | [related] |
Performs a self check of the instance content wrt the set of language self was declared to contain.
| void FlatHierarchy_set_constants_associations | ( | FlatHierarchy_ptr | self, | |
| hash_ptr | h | |||
| ) | [related] |
This function sets the hash table storing the association between the hierarchy section and constants expressions.
self retains ownership of h. Note: you should know what you are doing when performing modifications on the table.
| void FlatHierarchy_set_symb_table | ( | const FlatHierarchy_ptr | self, | |
| SymbTable_ptr | symb_table | |||
| ) | [related] |
Returns the associated symbol table.
| void FlatHierarchy_set_var_expr_associations | ( | FlatHierarchy_ptr | self, | |
| hash_ptr | h | |||
| ) | [related] |
This function sets the hash table storing the association between a variable name and expressions the variable is used in to h.
self obtains ownership of h.
Note: you should know what you are doing when using this function. You are fully responsible that the contents of h make sense - no checks are performed whatsoever.
| void FlatHierarchy_type_check | ( | FlatHierarchy_ptr | self | ) | [related] |
1.6.1
