Private and protected interface of class 'FormulaDependency'. More...
#include <FormulaDependency_private.h>
Public Member Functions | |
| INHERITS_FROM (MasterNodeWalker) | |
Related Functions | |
(Note that these are not member functions.) | |
| void | formula_dependency_deinit (FormulaDependency_ptr self) |
| The FormulaDependency class private deinitializer. | |
| Set_t | formula_dependency_get_definition_dependencies (FormulaDependency_ptr self, SymbTable_ptr symb_table, node_ptr formula, SymbFilterType filter, boolean preserve_time, int time, hash_ptr dependencies_hash) |
| Compute the dependencies of an atom. | |
| Set_t | formula_dependency_get_dependencies (FormulaDependency_ptr self, SymbTable_ptr symb_table, node_ptr formula, node_ptr context, SymbFilterType filter, boolean preserve_time, int time, hash_ptr dependencies_hash) |
| Get the set of dependencies for formula. | |
| hash_ptr | formula_dependency_get_hash (FormulaDependency_ptr self, SymbTable_ptr symb_table) |
| Call SymbTable_get_handled_hash_ptr to get the hash table used to store the dependencies. | |
| void | formula_dependency_init (FormulaDependency_ptr self, const NuSMVEnv_ptr env) |
| The FormulaDependency class private initializer. | |
| FormulaDependency_ptr | FormulaDependency_create (const NuSMVEnv_ptr env) |
| The FormulaDependency class constructor. | |
| void | FormulaDependency_destroy (FormulaDependency_ptr self) |
| The FormulaDependency class destructor. | |
| Set_t | FormulaDependency_formulae_get_dependencies (FormulaDependency_ptr self, SymbTable_ptr symb_table, node_ptr formula, node_ptr justice, node_ptr compassion) |
| Compute the dependencies of two set of formulae. | |
| Set_t | FormulaDependency_formulae_get_dependencies_by_type (FormulaDependency_ptr, SymbTable_ptr, node_ptr, node_ptr, node_ptr, SymbFilterType, boolean) |
| Compute the dependencies of two set of formulae by given type. | |
| Set_t | FormulaDependency_get_dependencies (FormulaDependency_ptr self, SymbTable_ptr symb_table, node_ptr formula, node_ptr context) |
| Computes dependencies of a given expression. | |
| Set_t | FormulaDependency_get_dependencies_by_type (FormulaDependency_ptr self, SymbTable_ptr symb_table, node_ptr formula, node_ptr context, SymbFilterType filter, boolean preserve_time) |
| Computes the dependencies of an SMV expression by type. | |
Private and protected interface of class 'FormulaDependency'.
Public interface of class 'FormulaDependency'.
FormulaDependency class definition derived from class MasterNodeWalker
Definition of the public accessor for class FormulaDependency
| FormulaDependency::INHERITS_FROM | ( | MasterNodeWalker | ) |
| void formula_dependency_deinit | ( | FormulaDependency_ptr | self | ) | [related] |
The FormulaDependency class private deinitializer.
The FormulaDependency class private deinitializer
| Set_t formula_dependency_get_definition_dependencies | ( | FormulaDependency_ptr | self, | |
| SymbTable_ptr | symb_table, | |||
| node_ptr | formula, | |||
| SymbFilterType | filter, | |||
| boolean | preserve_time, | |||
| int | time, | |||
| hash_ptr | dependencies_hash | |||
| ) | [related] |
Compute the dependencies of an atom.
This function computes the dependencies of an atom. If the atom corresponds to a variable then the singleton with the variable is returned. If the atom corresponds to a "running" condition the singleton with variable PROCESS_SELECTOR_VAR_NAME is returned. Otherwise if the atom corresponds to a defined symbol the dependency set corresponding to the body of the definition is computed and returned. filter specifies what variables we are interested to, as in Formula_GetDependenciesByType, and is_inside_next is supposed to be true if the atom is inside a Next, false otherwise. Returned set must be disposed by the caller
The dependencies_hash is modified in order to memoize previously computed dependencies of defined symbols.
| Set_t formula_dependency_get_dependencies | ( | FormulaDependency_ptr | self, | |
| SymbTable_ptr | symb_table, | |||
| node_ptr | formula, | |||
| node_ptr | context, | |||
| SymbFilterType | filter, | |||
| boolean | preserve_time, | |||
| int | time, | |||
| hash_ptr | dependencies_hash | |||
| ) | [related] |
Get the set of dependencies for formula.
Get the set of dependencies for formula.
| hash_ptr formula_dependency_get_hash | ( | FormulaDependency_ptr | self, | |
| SymbTable_ptr | symb_table | |||
| ) | [related] |
Call SymbTable_get_handled_hash_ptr to get the hash table used to store the dependencies.
| void formula_dependency_init | ( | FormulaDependency_ptr | self, | |
| const NuSMVEnv_ptr | env | |||
| ) | [related] |
The FormulaDependency class private initializer.
The FormulaDependency class private initializer
| FormulaDependency_ptr FormulaDependency_create | ( | const NuSMVEnv_ptr | env | ) | [related] |
The FormulaDependency class constructor.
AutomaticStart
The FormulaDependency class constructor
| void FormulaDependency_destroy | ( | FormulaDependency_ptr | self | ) | [related] |
The FormulaDependency class destructor.
The FormulaDependency class destructor
| Set_t FormulaDependency_formulae_get_dependencies | ( | FormulaDependency_ptr | self, | |
| SymbTable_ptr | symb_table, | |||
| node_ptr | formula, | |||
| node_ptr | justice, | |||
| node_ptr | compassion | |||
| ) | [related] |
Compute the dependencies of two set of formulae.
Given a formula and a list of fairness constraints, the set of variables occurring in them is computed. Returned Set must be disposed by the caller
| Set_t FormulaDependency_formulae_get_dependencies_by_type | ( | FormulaDependency_ptr | , | |
| SymbTable_ptr | , | |||
| node_ptr | , | |||
| node_ptr | , | |||
| node_ptr | , | |||
| SymbFilterType | , | |||
| boolean | ||||
| ) | [related] |
Compute the dependencies of two set of formulae by given type.
Given a formula and a list of fairness constraints, the set of symbols of the given type occurring in them is computed. Returned Set must be disposed by the caller.
| Set_t FormulaDependency_get_dependencies | ( | FormulaDependency_ptr | self, | |
| SymbTable_ptr | symb_table, | |||
| node_ptr | formula, | |||
| node_ptr | context | |||
| ) | [related] |
Computes dependencies of a given expression.
The set of dependencies of a given formula are computed. A traversal of the formula is performed. Each time a variable is encountered, it is added to the so far computed set. When a formula depends on a next variable, then the corresponding current variable is added to the set. When an atom is found a call to formula_dependency_get_definition_dependencies is performed to compute the dependencies. Returned set must be disposed by the caller. This is the same as calling Formula_GetDependenciesByType with filter = VFT_CNIF and preserve_time = false
| Set_t FormulaDependency_get_dependencies_by_type | ( | FormulaDependency_ptr | self, | |
| SymbTable_ptr | symb_table, | |||
| node_ptr | formula, | |||
| node_ptr | context, | |||
| SymbFilterType | filter, | |||
| boolean | preserve_time | |||
| ) | [related] |
Computes the dependencies of an SMV expression by type.
The set of dependencies of a given formula are computed, as in Formula_GetDependencies, but the variable type filters the dependency collection.
If flag preserve_time is true, then entries in the returned set will preserve the time they occur within the formula. For example, formula 'a & next(b) = 2 & attime(c, 2) < 4' returns {a,b,c} if preserve_time is false, and {a, next(b), attime(c, 2)} if preserve_time is true.
Returned set must be disposed by the caller
1.6.1
