HrcNode Struct Reference

Private and protected interface of class 'HrcNode'. More...

#include <HrcNode_private.h>

Public Member Functions
	INHERITS_FROM (EnvObject)
Data Fields
Olist_ptr	actual_parameters
Olist_ptr	array_defines
hash_ptr	assigns_table
Slist_ptr	childs
Olist_ptr	compassion
Olist_ptr	compute_props
Olist_ptr	constants
Olist_ptr	ctl_props
Olist_ptr	defines
Olist_ptr	formal_parameters
Olist_ptr	frozen_functions
Olist_ptr	frozen_variables
Olist_ptr	init_assign
Olist_ptr	init_expr
Olist_ptr	input_variables
node_ptr	instance_name
Olist_ptr	invar_assign
Olist_ptr	invar_expr
Olist_ptr	invar_props
Olist_ptr	justice
int	lineno
Olist_ptr	ltl_props
node_ptr	name
Olist_ptr	next_assign
Olist_ptr	next_expr
HrcNode_ptr	parent
Olist_ptr	psl_props
SymbTable_ptr	st
Olist_ptr	state_functions
Olist_ptr	state_variables
void *	undef
Related Functions
(Note that these are not member functions.)
void	hrc_node_deinit (HrcNode_ptr self)
	The HrcNode class private deinitializer.
void	hrc_node_init (HrcNode_ptr self, const NuSMVEnv_ptr env)
	The HrcNode class private initializer.
void	HrcNode_add_actual_parameter (HrcNode_ptr self, node_ptr par)
	Adds an actual parameter to the current node.
void	HrcNode_add_array_define (HrcNode_ptr self, node_ptr mdef)
	Adds an ARRAY DEFINE to the current node.
void	HrcNode_add_child_hrc_node (HrcNode_ptr self, HrcNode_ptr node)
	Adds a child node to the current node.
void	HrcNode_add_compassion_expr (HrcNode_ptr self, node_ptr compassion)
	Adds a COMPASSION constraint.
void	HrcNode_add_compute_property_expr (HrcNode_ptr self, node_ptr compute)
	Adds a COMPUTE property.
void	HrcNode_add_constants (HrcNode_ptr self, node_ptr constant)
	Adds a CONSTANTS declaration to the list of constants.
void	HrcNode_add_ctl_property_expr (HrcNode_ptr self, node_ptr ctl)
	Adds a CTL property.
void	HrcNode_add_define (HrcNode_ptr self, node_ptr def)
	Adds a DEFINE to the current node.
void	HrcNode_add_formal_parameter (HrcNode_ptr self, node_ptr par)
	Adds a formal parameter to the the current node.
void	HrcNode_add_frozen_function (HrcNode_ptr self, node_ptr fun)
	Adds a frozen function to the current node.
void	HrcNode_add_frozen_variable (HrcNode_ptr self, node_ptr var)
	Adds a frozen variable to the current node.
void	HrcNode_add_init_assign_expr (HrcNode_ptr self, node_ptr assign)
	Adds an init(*) := assignment to the current node.
void	HrcNode_add_init_expr (HrcNode_ptr self, node_ptr expr)
	Adds an INIT expression to the current node.
void	HrcNode_add_input_variable (HrcNode_ptr self, node_ptr var)
	Adds a input variable to the current node.
void	HrcNode_add_invar_assign_expr (HrcNode_ptr self, node_ptr assign)
	Adds an (*) := assignment to the current node.
void	HrcNode_add_invar_expr (HrcNode_ptr self, node_ptr expr)
	Adds an INVAR expression to the current node.
void	HrcNode_add_invar_property_expr (HrcNode_ptr self, node_ptr invar)
	Adds an INVARIANT property.
void	HrcNode_add_justice_expr (HrcNode_ptr self, node_ptr justice)
	Adds a JUSTICE constraint.
void	HrcNode_add_ltl_property_expr (HrcNode_ptr self, node_ptr ltl)
	Adds an LTL property.
void	HrcNode_add_next_assign_expr (HrcNode_ptr self, node_ptr assign)
	Adds an next(*) := assignment to the current node.
void	HrcNode_add_psl_property_expr (HrcNode_ptr self, node_ptr psl)
	Adds an PSL property.
void	HrcNode_add_state_variable (HrcNode_ptr self, node_ptr var)
	Adds a state variable to the current node.
void	HrcNode_add_trans_expr (HrcNode_ptr self, node_ptr expr)
	Adds an TRANS expression to the current node.
boolean	HrcNode_can_declare_assign (HrcNode_ptr self, node_ptr symbol, int assign_type)
	Checks if an assignment can be declared within the node.
void	HrcNode_cleanup (HrcNode_ptr self)
	Resets all fields of the given node.
HrcNode_ptr	HrcNode_copy (const HrcNode_ptr self)
	Creates a new node that is a copy of self without considering children.
HrcNode_ptr	HrcNode_copy_rename (const HrcNode_ptr self, node_ptr new_module_name)
	Creates a new node that is a copy of self without considering children. The name of the module of the new node is set as new_module_name.
HrcNode_ptr	HrcNode_create (const NuSMVEnv_ptr env)
	The HrcNode class constructor.
void	HrcNode_destroy (HrcNode_ptr self)
	The HrcNode class destructor.
void	HrcNode_destroy_recur (HrcNode_ptr self)
	The HrcNode class destructor. It recurses on the childs.
node_ptr	HrcNode_find_define (const HrcNode_ptr self, node_ptr def_name)
	Returns the define (def_name, def_body).
node_ptr	HrcNode_find_formal_parameter (const HrcNode_ptr self, node_ptr par_name)
	Returns the formal param (pair name, type).
HrcNode_ptr	HrcNode_find_hrc_node_by_instance_name (const HrcNode_ptr self, node_ptr name)
	Returns the pointer to the a module instance of a of given name.
HrcNode_ptr	HrcNode_find_hrc_node_by_mod_type (const HrcNode_ptr self, node_ptr mod_type)
	Returns the pointer to a node instance of mod_type.
Olist_ptr	HrcNode_find_hrc_nodes_by_mod_type (const HrcNode_ptr self, const node_ptr mod_type)
	Returns all the node instances of mod_type, from given root.
node_ptr	HrcNode_find_var (HrcNode_ptr self, node_ptr var_name, int type)
	Returns the variable var_name of type var_type.
node_ptr	HrcNode_find_var_all (HrcNode_ptr self, node_ptr var_name)
	Returns the variable var_name searching in all types.
Oiter	HrcNode_get_actual_parameters_iter (const HrcNode_ptr self)
	Gets the actual parameters of the current node.
int	HrcNode_get_actual_parameters_length (const HrcNode_ptr self)
	Returns the number of actual parameters.
Oiter	HrcNode_get_array_defines_iter (const HrcNode_ptr self)
	Gets the local ARRAY DEFINES of the current node.
int	HrcNode_get_array_defines_num (const HrcNode_ptr self)
	Returns the number of all declared array define.
Slist_ptr	HrcNode_get_child_hrc_nodes (const HrcNode_ptr self)
Oiter	HrcNode_get_compassion_exprs_iter (const HrcNode_ptr self)
	Gets the list of COMPASSION constraints.
Oiter	HrcNode_get_compute_properties_iter (const HrcNode_ptr self)
	Gets the list of COMPUTE properties.
Oiter	HrcNode_get_constants_iter (const HrcNode_ptr self)
	Gets the list of CONSTANTS declarations.
int	HrcNode_get_constants_num (const HrcNode_ptr self)
	Returns the number of all declared constants.
node_ptr	HrcNode_get_crude_name (const HrcNode_ptr self)
	Gets the MOD_TYPE name of the node.
Oiter	HrcNode_get_ctl_properties_iter (const HrcNode_ptr self)
	Gets the list of CTL properties.
Oiter	HrcNode_get_defines_iter (const HrcNode_ptr self)
	Gets the local DEFINES of the current node.
int	HrcNode_get_defines_num (const HrcNode_ptr self)
	Returns the number of all declared defines.
node_ptr	HrcNode_get_flattened_instance_name (const HrcNode_ptr self)
	Gets the flattened instance name of the node.
Oiter	HrcNode_get_formal_parameters_iter (const HrcNode_ptr self)
	Gets the formal parameters of the current node.
int	HrcNode_get_formal_parameters_length (const HrcNode_ptr self)
	Returns the number of formal parameters.
Oiter	HrcNode_get_frozen_functions_iter (const HrcNode_ptr self)
	Gets the frozen functions of the current node.
Oiter	HrcNode_get_frozen_variables_iter (const HrcNode_ptr self)
	Gets the local frozen variables of the current node.
int	HrcNode_get_frozen_vars_num (const HrcNode_ptr self)
	Returns the number of all declared frozen variables.
int	HrcNode_get_functions_num (const HrcNode_ptr self)
	Returns the number of all NFunctions.
Oiter	HrcNode_get_init_assign_exprs_iter (const HrcNode_ptr self)
	Gets the init(*) := expressions for the current node.
Oiter	HrcNode_get_init_exprs_iter (const HrcNode_ptr self)
	Sets the INIT expressions for the current node.
Oiter	HrcNode_get_input_variables_iter (const HrcNode_ptr self)
	Gets the local input variables of the current node.
int	HrcNode_get_input_vars_num (const HrcNode_ptr self)
	Returns the number of all declared input variables.
node_ptr	HrcNode_get_instance_name (const HrcNode_ptr self)
	Gets the instance name of the node.
Oiter	HrcNode_get_invar_assign_exprs_iter (const HrcNode_ptr self)
	Gets the (*) := expressions for the current node.
Oiter	HrcNode_get_invar_exprs_iter (const HrcNode_ptr self)
	Sets the INVAR expressions for the current node.
Oiter	HrcNode_get_invar_properties_iter (const HrcNode_ptr self)
	Gets the list of INVARIANT properties.
Oiter	HrcNode_get_justice_exprs_iter (const HrcNode_ptr self)
	Gets the list of JUSTICE constraints.
int	HrcNode_get_lineno (const HrcNode_ptr self)
	Gets the MOD_TYPE lineno of the node.
Oiter	HrcNode_get_ltl_properties_iter (const HrcNode_ptr self)
	Gets the list of LTL properties.
node_ptr	HrcNode_get_name (const HrcNode_ptr self)
	Gets the MOD_TYPE name of the node.
Oiter	HrcNode_get_next_assign_exprs_iter (const HrcNode_ptr self)
	Gets the next(*) := expressions for the current node.
int	HrcNode_get_parameters_num (const HrcNode_ptr self)
	Returns the number of all parameters.
HrcNode_ptr	HrcNode_get_parent (const HrcNode_ptr self)
	Get the parent node of the node.
Oiter	HrcNode_get_psl_properties_iter (const HrcNode_ptr self)
	Gets the list of PSL properties.
HrcNode_ptr	HrcNode_get_root (const HrcNode_ptr self)
	Get the parent node of the node.
Oiter	HrcNode_get_state_variables_iter (const HrcNode_ptr self)
	Gets the local state variables of the current node.
int	HrcNode_get_state_vars_num (const HrcNode_ptr self)
	Returns the number of all declared state variables.
SymbTable_ptr	HrcNode_get_symbol_table (HrcNode_ptr self)
	Gets the symbol table.
int	HrcNode_get_symbols_num (const HrcNode_ptr self)
	Returns the number of all symbols.
Oiter	HrcNode_get_trans_exprs_iter (const HrcNode_ptr self)
	Gets the TRANS expressions for the current node.
void *	HrcNode_get_undef (const HrcNode_ptr self)
	Getter for the undef field.
int	HrcNode_get_vars_num (const HrcNode_ptr self)
	Returns the number of all declared variables.
boolean	HrcNode_is_leaf (const HrcNode_ptr self)
	Checks wether current node is a leaf node in the hierarchy.
boolean	HrcNode_is_root (const HrcNode_ptr self)
	Checks wether current node is the root of the hierarchy.
void	HrcNode_link_nodes (HrcNode_ptr self, HrcNode_ptr child)
	Link two nodes.
HrcNode_ptr	HrcNode_recursive_copy (const HrcNode_ptr self)
void	HrcNode_remove_frozen_variable (HrcNode_ptr self, node_ptr var)
	Remove a frozen variable from the current node.
void	HrcNode_remove_input_variable (HrcNode_ptr self, node_ptr var)
	Remove a input variable from the current node.
void	HrcNode_remove_state_variable (HrcNode_ptr self, node_ptr var)
	Remove a state variable from the current node.
void	HrcNode_replace_actual_parameters (HrcNode_ptr self, Olist_ptr par)
	Replaces the actual parameters of the current node.
void	HrcNode_replace_array_defines (HrcNode_ptr self, Olist_ptr mdefs)
	Replaces the local ARRAY DEFINES of the current node.
void	HrcNode_replace_compassion_exprs (HrcNode_ptr self, Olist_ptr compassions)
	Replaces the list of COMPASSION constraints.
void	HrcNode_replace_compute_properties (HrcNode_ptr self, Olist_ptr computes)
	Replaces the list of COMPUTE properties.
void	HrcNode_replace_constants (HrcNode_ptr self, Olist_ptr constants)
	Replaces the list of CONSTANTS declarations.
void	HrcNode_replace_ctl_properties (HrcNode_ptr self, Olist_ptr ctls)
	Replaces the list of CTL properties.
void	HrcNode_replace_defines (HrcNode_ptr self, Olist_ptr defs)
	Replaces the local DEFINES of the current node.
void	HrcNode_replace_formal_parameters (HrcNode_ptr self, Olist_ptr par)
	Replaces the formal parameters of the current node.
void	HrcNode_replace_frozen_functions (HrcNode_ptr self, Olist_ptr functions)
	Replaces the local frozen functions of the current node.
void	HrcNode_replace_frozen_variables (HrcNode_ptr self, Olist_ptr vars)
	Replaces the local frozen variables of the current node.
void	HrcNode_replace_init_assign_exprs (HrcNode_ptr self, Olist_ptr assigns)
	Replaces the init(*) := expressions for the current node.
void	HrcNode_replace_init_exprs (HrcNode_ptr self, Olist_ptr exprs)
	Replaces the INIT expressions for the current node.
void	HrcNode_replace_input_variables (HrcNode_ptr self, Olist_ptr vars)
	Replacess the local input variables of the current node.
void	HrcNode_replace_invar_assign_exprs (HrcNode_ptr self, Olist_ptr assigns)
	Replaces the (*) := expressions for the current node.
void	HrcNode_replace_invar_exprs (HrcNode_ptr self, Olist_ptr exprs)
	Replaces the INVAR expressions for the current node.
void	HrcNode_replace_invar_properties (HrcNode_ptr self, Olist_ptr invars)
	Replaces the list of INVARIANT properties.
void	HrcNode_replace_justice_exprs (HrcNode_ptr self, Olist_ptr justices)
	Replaces the list of JUSTICE constraints.
void	HrcNode_replace_ltl_properties (HrcNode_ptr self, Olist_ptr ltls)
	Replaces the list of LTL properties.
void	HrcNode_replace_next_assign_exprs (HrcNode_ptr self, Olist_ptr assigns)
	Replaces the next(*) := expressions for the current node.
void	HrcNode_replace_psl_properties (HrcNode_ptr self, Olist_ptr psls)
	Replaces the list of PSL properties.
void	HrcNode_replace_state_variables (HrcNode_ptr self, Olist_ptr vars)
	Replaces the local state variables of the current node.
void	HrcNode_replace_trans_exprs (HrcNode_ptr self, Olist_ptr exprs)
	Replaces the TRANS expressions for the current node.
void	HrcNode_set_child_hrc_nodes (HrcNode_ptr self, Slist_ptr list)
	Sets the list of local childs for the current node.
void	HrcNode_set_instance_name (HrcNode_ptr self, node_ptr name)
	Sets the instance name of the node.
void	HrcNode_set_lineno (HrcNode_ptr self, int lineno)
	Sets the MOD_TYPE lineno of the node.
void	HrcNode_set_name (HrcNode_ptr self, node_ptr name)
	Sets the MOD_TYPE name of the node.
void	HrcNode_set_parent (const HrcNode_ptr self, HrcNode_ptr father)
	Sets the parent node of the node.
void	HrcNode_set_symbol_table (HrcNode_ptr self, SymbTable_ptr st)
	Sets the symbol table inside the node.
void	HrcNode_set_undef (const HrcNode_ptr self, void *undef)
	Getter for the undef field.
void	HrcNode_unlink_nodes (HrcNode_ptr self, HrcNode_ptr child)
	Unlink two nodes.

Detailed Description

Private and protected interface of class 'HrcNode'.

Public interface of class 'HrcNode'.

Author:: Sergio Mover This file can be included only by derived and friend classes

HrcNode class definition derived from class EnvObject

See also:: Base class EnvObject

Author:: Marco Roveri

Todo:: : Missing description

Definition of the public accessor for class HrcNode

Member Function Documentation

HrcNode::INHERITS_FROM ( EnvObject )

Friends And Related Function Documentation

void hrc_node_deinit ( HrcNode_ptr self ) [related]

The HrcNode class private deinitializer.

The HrcNode class private deinitializer

See also:: HrcNode_destroy

void hrc_node_init	(	HrcNode_ptr	self,
		const NuSMVEnv_ptr	env
	)			`[related]`

The HrcNode class private initializer.

The HrcNode class private initializer

See also:: HrcNode_create

void HrcNode_add_actual_parameter	(	HrcNode_ptr	self,
		node_ptr	par
	)			`[related]`

Adds an actual parameter to the current node.

Adds an actual parameter to the current node. It should be a pair (name . expr), where expr specifies the expression the parameter has been instantiated to.

Structure is updated

See also:: optional

void HrcNode_add_array_define	(	HrcNode_ptr	self,
		node_ptr	mdef
	)			`[related]`

Adds an ARRAY DEFINE to the current node.

Adds a ARRAY DEFINE declaration to the current node. The array define should be a pairs (name . expr) where expr is the body of the current DEFINE symbol.

Structure is updated

See also:: optional

void HrcNode_add_child_hrc_node	(	HrcNode_ptr	self,
		HrcNode_ptr	node
	)			`[related]`

Adds a child node to the current node.

Add a child node to the current node. The parent of the child should have been set by someone else and it is expected to be the current one.

Structure is updated

See also:: optional

void HrcNode_add_compassion_expr	(	HrcNode_ptr	self,
		node_ptr	compassion
	)			`[related]`

Adds a COMPASSION constraint.

Structure is updated

See also:: optional

void HrcNode_add_compute_property_expr	(	HrcNode_ptr	self,
		node_ptr	compute
	)			`[related]`

Adds a COMPUTE property.

Structure is updated

See also:: optional

void HrcNode_add_constants	(	HrcNode_ptr	self,
		node_ptr	constant
	)			`[related]`

Adds a CONSTANTS declaration to the list of constants.

Adds a CONSTANTS declaration to the list of constants. All constants are kept in a unique list.

constant is a list of constants.

Structure is updated

See also:: optional

void HrcNode_add_ctl_property_expr	(	HrcNode_ptr	self,
		node_ptr	ctl
	)			`[related]`

Adds a CTL property.

Structure is updated

See also:: optional

void HrcNode_add_define	(	HrcNode_ptr	self,
		node_ptr	def
	)			`[related]`

Adds a DEFINE to the current node.

Adds a define declaration to the current node. The define should be a pairs (name . expr) where expr is the body of the current DEFINE symbol.

Structure is updated

See also:: optional

void HrcNode_add_formal_parameter	(	HrcNode_ptr	self,
		node_ptr	par
	)			`[related]`

Adds a formal parameter to the the current node.

Adds a formal parameter to the current node. It should be a pair (name . type), where type specifies the type of the parameter if known, otherwise it is Nil.

Structure is updated

See also:: optional

void HrcNode_add_frozen_function	(	HrcNode_ptr	self,
		node_ptr	fun
	)			`[related]`

Adds a frozen function to the current node.

Structure is updated

See also:: optional

void HrcNode_add_frozen_variable	(	HrcNode_ptr	self,
		node_ptr	var
	)			`[related]`

Adds a frozen variable to the current node.

Adds a frozen variable to the current node. The var should be a pairs (name . type) where type is the type of the corresponding variable.

Structure is updated

See also:: optional

void HrcNode_add_init_assign_expr	(	HrcNode_ptr	self,
		node_ptr	assign
	)			`[related]`

Adds an init(*) := assignment to the current node.

Adds an init(*) := assignment to the current node. An assignment is an ASSIGN node that has as left child init(*) and as right child the assignment.

Structure is updated

See also:: optional

void HrcNode_add_init_expr	(	HrcNode_ptr	self,
		node_ptr	expr
	)			`[related]`

Adds an INIT expression to the current node.

Structure is updated

See also:: optional

void HrcNode_add_input_variable	(	HrcNode_ptr	self,
		node_ptr	var
	)			`[related]`

Adds a input variable to the current node.

Adds a input variable to the current node. The var should be a pairs (name . type) where type is the type of the corresponding variable.

Structure is updated

See also:: optional

void HrcNode_add_invar_assign_expr	(	HrcNode_ptr	self,
		node_ptr	assign
	)			`[related]`

Adds an (*) := assignment to the current node.

Adds an (*) := assignment to the current node. An assignment is an ASSIGN node that has as left child (*) and as right child the assignment.

Structure is updated

See also:: optional

void HrcNode_add_invar_expr	(	HrcNode_ptr	self,
		node_ptr	expr
	)			`[related]`

Adds an INVAR expression to the current node.

Structure is updated

See also:: optional

void HrcNode_add_invar_property_expr	(	HrcNode_ptr	self,
		node_ptr	invar
	)			`[related]`

Adds an INVARIANT property.

Structure is updated

See also:: optional

void HrcNode_add_justice_expr	(	HrcNode_ptr	self,
		node_ptr	justice
	)			`[related]`

Adds a JUSTICE constraint.

Structure is updated

See also:: optional

void HrcNode_add_ltl_property_expr	(	HrcNode_ptr	self,
		node_ptr	ltl
	)			`[related]`

Adds an LTL property.

Structure is updated

See also:: optional

void HrcNode_add_next_assign_expr	(	HrcNode_ptr	self,
		node_ptr	assign
	)			`[related]`

Adds an next(*) := assignment to the current node.

Adds an next(*) := assignment to the current node. An assignment is an ASSIGN node that has as left child next(*) and as right child the assignment.

Structure is updated

See also:: optional

void HrcNode_add_psl_property_expr	(	HrcNode_ptr	self,
		node_ptr	psl
	)			`[related]`

Adds an PSL property.

Structure is updated

See also:: optional

void HrcNode_add_state_variable	(	HrcNode_ptr	self,
		node_ptr	var
	)			`[related]`

Adds a state variable to the current node.

Adds a state variable to the current node. The var should be a pairs (name . type) where type is the type of the corresponding variable.

Structure is updated

See also:: optional

void HrcNode_add_trans_expr	(	HrcNode_ptr	self,
		node_ptr	expr
	)			`[related]`

Adds an TRANS expression to the current node.

Structure is updated

See also:: optional

boolean HrcNode_can_declare_assign	(	HrcNode_ptr	self,
		node_ptr	symbol,
		int	assign_type
	)			`[related]`

Checks if an assignment can be declared within the node.

Checks if an assignment can be declared within the node. If an INIT/NEXT assign is already declared for a symbol, then only a NEXT/INIT assign can be declared. If an INVAR assignment is already declared, then no other assignments can be declared

void HrcNode_cleanup ( HrcNode_ptr self ) [related]

Resets all fields of the given node.

Resets all fields of the given node. This is needed for safely recycle a node instance. For example, if a parsing error occurs. Children are destroyed.

HrcNode_ptr HrcNode_copy ( const HrcNode_ptr self ) [related]

Creates a new node that is a copy of self without considering children.

The copy does not even link a node with its parent.

See also:: HrcNode_copyRename

HrcNode_ptr HrcNode_copy_rename	(	const HrcNode_ptr	self,
		node_ptr	new_module_name
	)			`[related]`

Creates a new node that is a copy of self without considering children. The name of the module of the new node is set as new_module_name.

Creates a new node that is a copy of self without considering childre. The name of the module of the new node is set as new_module_name.

The copy does not even link a node with its parent.

See also:: HrcNode_copy

HrcNode_ptr HrcNode_create ( const NuSMVEnv_ptr env ) [related]

The HrcNode class constructor.

AutomaticStart

The HrcNode class constructor

See also:: HrcNode_destroy

void HrcNode_destroy ( HrcNode_ptr self ) [related]

The HrcNode class destructor.

The HrcNode class destructor

The node is freed

See also:: HrcNode_create

void HrcNode_destroy_recur ( HrcNode_ptr self ) [related]

The HrcNode class destructor. It recurses on the childs.

The whole hierarchy tree is freed

See also:: HrcNode_create, HrcNode_destroy

node_ptr HrcNode_find_define	(	const HrcNode_ptr	self,
		node_ptr	def_name
	)			`[related]`

Returns the define (def_name, def_body).

Returns the define def_name with body. The search is performed only inside self node, thus the function does not recur over hierarchy.

A cons between the found name and define body is returned upon success. Returned cons must be freed by the caller. Nil is returned if define is not found.

def_name is the name of the define.

node_ptr HrcNode_find_formal_parameter	(	const HrcNode_ptr	self,
		node_ptr	par_name
	)			`[related]`

Returns the formal param (pair name, type).

Returns the parameter par_name of type par_type. The search is performed only inside self node, thus the function does not recur over hierarchy. A cons between the found name and its type is returned upon success. Returned cons must be freed by the caller. Nil is returned if parameter is not found.

par_name is the name of the formal parameter.

Note that given parameter may have type set to Nil.

HrcNode_ptr HrcNode_find_hrc_node_by_instance_name	(	const HrcNode_ptr	self,
		node_ptr	name
	)			`[related]`

Returns the pointer to the a module instance of a of given name.

Returns the pointer to the a module instance of a of given name. Returns HRC_NODE(NULL) if no instance exists.

None

See also:: optional

HrcNode_ptr HrcNode_find_hrc_node_by_mod_type	(	const HrcNode_ptr	self,
		node_ptr	mod_type
	)			`[related]`

Returns the pointer to a node instance of mod_type.

Returns the pointer to the first instance of a module of type mod_type encountered in a depth first traversal of the hierarchy tree. Returns HRC_NODE(NULL) if no instance exists.

None

See also:: optional

Olist_ptr HrcNode_find_hrc_nodes_by_mod_type	(	const HrcNode_ptr	self,
		const node_ptr	mod_type
	)			`[related]`

Returns all the node instances of mod_type, from given root.

Returns a list of pointers to all the instances of a module of type mod_type encountered in a depth first traversal of the hierarchy tree. Returned list must be freed by the caller.

None

See also:: optional

node_ptr HrcNode_find_var	(	HrcNode_ptr	self,
		node_ptr	var_name,
		int	type
	)			`[related]`

Returns the variable var_name of type var_type.

Returns the variable var_name of type var_type. The search is performed only inside self node, thus the function does not recur over hierarchy. A cons between the found variable and its type is returned upon success. Returned cons must be freed by the caller. Nil is returned if variable is not found.

var_name is the name of the variable while type is the type of variable to search (VAR, FROZENVAR, IVAR).

[MD] bad interface, the input is a symbol, the output is a pair symbol, type (returned as a CONS)

node_ptr HrcNode_find_var_all	(	HrcNode_ptr	self,
		node_ptr	var_name
	)			`[related]`

Returns the variable var_name searching in all types.

Like HrcNode_find_var, but it searches in all variable types VAR, FROZENVAR, INVAR

Oiter HrcNode_get_actual_parameters_iter ( const HrcNode_ptr self ) [related]

Gets the actual parameters of the current node.

Gets the actual parameters of the current node. The result is a list of pairs (name . expr), where expr specifies the expression the current current formal parameter node has been instatiated to.

None

See also:: optional

int HrcNode_get_actual_parameters_length ( const HrcNode_ptr self ) [related]

Returns the number of actual parameters.

Todo:: Missing description

Oiter HrcNode_get_array_defines_iter ( const HrcNode_ptr self ) [related]

Gets the local ARRAY DEFINES of the current node.

Gets the local ARRAY DEFINES of the current node. The result is a list of pairs (name . expr) where expr is the body of the ARRAY DEFINEd symbol.

None

See also:: optional

int HrcNode_get_array_defines_num ( const HrcNode_ptr self ) [related]

Returns the number of all declared array define.

Slist_ptr HrcNode_get_child_hrc_nodes ( const HrcNode_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

Oiter HrcNode_get_compassion_exprs_iter ( const HrcNode_ptr self ) [related]

Gets the list of COMPASSION constraints.

None

See also:: optional

Oiter HrcNode_get_compute_properties_iter ( const HrcNode_ptr self ) [related]

Gets the list of COMPUTE properties.

None

See also:: optional

Oiter HrcNode_get_constants_iter ( const HrcNode_ptr self ) [related]

Gets the list of CONSTANTS declarations.

None

See also:: optional

int HrcNode_get_constants_num ( const HrcNode_ptr self ) [related]

Returns the number of all declared constants.

Warning: this functions returns a number that can be different from the one returned by SymbTable_get_constants_num (constants within types could be not counted here)

node_ptr HrcNode_get_crude_name ( const HrcNode_ptr self ) [related]

Gets the MOD_TYPE name of the node.

Gets the MOD_TYPE name of the node. WARNING: the returned name is the name passed to SetName, and it is not 'normalized' like in GetName. This can be used to obtain the node as produced by the parser.

None

See also:: optional

Oiter HrcNode_get_ctl_properties_iter ( const HrcNode_ptr self ) [related]

Gets the list of CTL properties.

None

See also:: optional

Oiter HrcNode_get_defines_iter ( const HrcNode_ptr self ) [related]

Gets the local DEFINES of the current node.

Gets the local DEFINES of the current node. The result is a list of pairs (name . expr) where expr is the body of the DEFINEd symbol.

None

See also:: optional

int HrcNode_get_defines_num ( const HrcNode_ptr self ) [related]

Returns the number of all declared defines.

node_ptr HrcNode_get_flattened_instance_name ( const HrcNode_ptr self ) [related]

Gets the flattened instance name of the node.

The hierarchy is visited upward from self until main node is found. The flattened and normalized instance node is built and returned.

The flattened instance name is the name obtained considering all the anchestors instance of the current node.

The result of this operation could also be memoized to improve performances (this would avoid to recompute the same path twice).

Oiter HrcNode_get_formal_parameters_iter ( const HrcNode_ptr self ) [related]

Gets the formal parameters of the current node.

Gets the formal parameters of the current node. The result is a list of pairs (name . type), where type specifies the type of the parameter if know, otherwise it is Nil.

None

See also:: optional

int HrcNode_get_formal_parameters_length ( const HrcNode_ptr self ) [related]

Returns the number of formal parameters.

Todo:: Missing description

Oiter HrcNode_get_frozen_functions_iter ( const HrcNode_ptr self ) [related]

Gets the frozen functions of the current node.

Gets the frozen functions of the current node. The result is a list of pairs (name . type), where type specifies the type of the function if know, otherwise it is Nil.

None

See also:: optional

Oiter HrcNode_get_frozen_variables_iter ( const HrcNode_ptr self ) [related]

Gets the local frozen variables of the current node.

Gets the local frozen variables of the current node. The result is a list of pairs (name . type) where type is the type of the corresponding variable.

None

See also:: optional

int HrcNode_get_frozen_vars_num ( const HrcNode_ptr self ) [related]

Returns the number of all declared frozen variables.

int HrcNode_get_functions_num ( const HrcNode_ptr self ) [related]

Returns the number of all NFunctions.

Oiter HrcNode_get_init_assign_exprs_iter ( const HrcNode_ptr self ) [related]

Gets the init(*) := expressions for the current node.

Gets the init(*) := expressions for the current node. It is a list of implicitly conjoined assignments.

Structure is updated

See also:: optional

Oiter HrcNode_get_init_exprs_iter ( const HrcNode_ptr self ) [related]

Sets the INIT expressions for the current node.

Sets the INIT expressions for the current node. It is a possibly empty list of implicitly conjoined expressions.

None

See also:: optional

Oiter HrcNode_get_input_variables_iter ( const HrcNode_ptr self ) [related]

Gets the local input variables of the current node.

Gets the local input variables of the current node. The result is a list of pairs (name . type) where type is the type of the corresponding variable.

None

See also:: optional

int HrcNode_get_input_vars_num ( const HrcNode_ptr self ) [related]

Returns the number of all declared input variables.

node_ptr HrcNode_get_instance_name ( const HrcNode_ptr self ) [related]

Gets the instance name of the node.

None

See also:: optional

Oiter HrcNode_get_invar_assign_exprs_iter ( const HrcNode_ptr self ) [related]

Gets the (*) := expressions for the current node.

Gets the (*) := expressions for the current node. It is a list of implicitly conjoined assignments.

Structure is updated

See also:: optional

Oiter HrcNode_get_invar_exprs_iter ( const HrcNode_ptr self ) [related]

Sets the INVAR expressions for the current node.

Sets the INVAR expressions for the current node. It is a possibly empty list of implicitly conjoined expressions.

None

See also:: optional

Oiter HrcNode_get_invar_properties_iter ( const HrcNode_ptr self ) [related]

Gets the list of INVARIANT properties.

None

See also:: optional

Oiter HrcNode_get_justice_exprs_iter ( const HrcNode_ptr self ) [related]

Gets the list of JUSTICE constraints.

None

See also:: optional

int HrcNode_get_lineno ( const HrcNode_ptr self ) [related]

Gets the MOD_TYPE lineno of the node.

None

See also:: optional

Oiter HrcNode_get_ltl_properties_iter ( const HrcNode_ptr self ) [related]

Gets the list of LTL properties.

None

See also:: optional

node_ptr HrcNode_get_name ( const HrcNode_ptr self ) [related]

Gets the MOD_TYPE name of the node.

Gets the MOD_TYPE name of the node. WARNING: the returned name is 'normalized' and can be used as hash value.

None

See also:: optional

Oiter HrcNode_get_next_assign_exprs_iter ( const HrcNode_ptr self ) [related]

Gets the next(*) := expressions for the current node.

Gets the next(*) := expressions for the current node. It is a list of implicitly conjoined assignments.

Structure is updated

See also:: optional

int HrcNode_get_parameters_num ( const HrcNode_ptr self ) [related]

Returns the number of all parameters.

HrcNode_ptr HrcNode_get_parent ( const HrcNode_ptr self ) [related]

Get the parent node of the node.

Get the parent node of the node. HRC_NODE(NULL) is returned if no father available.

None

See also:: optional

Oiter HrcNode_get_psl_properties_iter ( const HrcNode_ptr self ) [related]

Gets the list of PSL properties.

None

See also:: optional

HrcNode_ptr HrcNode_get_root ( const HrcNode_ptr self ) [related]

Get the parent node of the node.

Get the parent node of the node. HRC_NODE(NULL) is returned if no father available.

None

See also:: optional

Oiter HrcNode_get_state_variables_iter ( const HrcNode_ptr self ) [related]

Gets the local state variables of the current node.

Gets the local state variables of the current node. The result is a list of pairs (name . type) where type is the type of the corresponding variable.

None

See also:: optional

int HrcNode_get_state_vars_num ( const HrcNode_ptr self ) [related]

Returns the number of all declared state variables.

SymbTable_ptr HrcNode_get_symbol_table ( HrcNode_ptr self ) [related]

Gets the symbol table.

None

See also:: optional

int HrcNode_get_symbols_num ( const HrcNode_ptr self ) [related]

Returns the number of all symbols.

Oiter HrcNode_get_trans_exprs_iter ( const HrcNode_ptr self ) [related]

Gets the TRANS expressions for the current node.

Gets the TRANS expressions for the current node. It is a possibly empty list of implicitly conjoined expressions.

None

See also:: optional

void * HrcNode_get_undef ( const HrcNode_ptr self ) [related]

Getter for the undef field.

Getter for the undef field

See also:: HrcNode_set_undef

int HrcNode_get_vars_num ( const HrcNode_ptr self ) [related]

Returns the number of all declared variables.

boolean HrcNode_is_leaf ( const HrcNode_ptr self ) [related]

Checks wether current node is a leaf node in the hierarchy.

Checks wether current node is a leaf node in the hierarchy. Returns true if it is a leaf node, false otherwise.

None

See also:: optional

boolean HrcNode_is_root ( const HrcNode_ptr self ) [related]

Checks wether current node is the root of the hierarchy.

Checks wether current node is the root of the hierarchy. Returns true if it is the root, false otherwise.

None

See also:: optional

void HrcNode_link_nodes	(	HrcNode_ptr	self,
		HrcNode_ptr	child
	)			`[related]`

Link two nodes.

Link two nodes

HrcNode_ptr HrcNode_recursive_copy ( const HrcNode_ptr self ) [related]

Creates a copy of self and recursively of all its children.

void HrcNode_remove_frozen_variable	(	HrcNode_ptr	self,
		node_ptr	var
	)			`[related]`

Remove a frozen variable from the current node.

The symbol table is not modified. Linear in the number of frozen variables

void HrcNode_remove_input_variable	(	HrcNode_ptr	self,
		node_ptr	var
	)			`[related]`

Remove a input variable from the current node.

The symbol table is not modified. Linear in the number of input variables

void HrcNode_remove_state_variable	(	HrcNode_ptr	self,
		node_ptr	var
	)			`[related]`

Remove a state variable from the current node.

The symbol table is not modified. Linear in the number of state variables

void HrcNode_replace_actual_parameters	(	HrcNode_ptr	self,
		Olist_ptr	par
	)			`[related]`

Replaces the actual parameters of the current node.

Structure is updated

See also:: optional

void HrcNode_replace_array_defines	(	HrcNode_ptr	self,
		Olist_ptr	mdefs
	)			`[related]`

Replaces the local ARRAY DEFINES of the current node.

Replaces the local ARRAY DEFINES for the current node.

Structure is updated

See also:: optional

void HrcNode_replace_compassion_exprs	(	HrcNode_ptr	self,
		Olist_ptr	compassions
	)			`[related]`

Replaces the list of COMPASSION constraints.

Structure is updated

See also:: optional

void HrcNode_replace_compute_properties	(	HrcNode_ptr	self,
		Olist_ptr	computes
	)			`[related]`

Replaces the list of COMPUTE properties.

Structure is updated

See also:: optional

void HrcNode_replace_constants	(	HrcNode_ptr	self,
		Olist_ptr	constants
	)			`[related]`

Replaces the list of CONSTANTS declarations.

Structure is updated

See also:: optional

void HrcNode_replace_ctl_properties	(	HrcNode_ptr	self,
		Olist_ptr	ctls
	)			`[related]`

Replaces the list of CTL properties.

Structure is updated

See also:: optional

void HrcNode_replace_defines	(	HrcNode_ptr	self,
		Olist_ptr	defs
	)			`[related]`

Replaces the local DEFINES of the current node.

Replaces the local DEFINES for the current node.

Structure is updated

See also:: optional

void HrcNode_replace_formal_parameters	(	HrcNode_ptr	self,
		Olist_ptr	par
	)			`[related]`

Replaces the formal parameters of the current node.

Relaces the formal parameters of the current node.

Structure is updated

See also:: optional

void HrcNode_replace_frozen_functions	(	HrcNode_ptr	self,
		Olist_ptr	functions
	)			`[related]`

Replaces the local frozen functions of the current node.

Structure is updated

See also:: optional

void HrcNode_replace_frozen_variables	(	HrcNode_ptr	self,
		Olist_ptr	vars
	)			`[related]`

Replaces the local frozen variables of the current node.

Structure is updated

See also:: optional

void HrcNode_replace_init_assign_exprs	(	HrcNode_ptr	self,
		Olist_ptr	assigns
	)			`[related]`

Replaces the init(*) := expressions for the current node.

Structure is updated

See also:: optional

void HrcNode_replace_init_exprs	(	HrcNode_ptr	self,
		Olist_ptr	exprs
	)			`[related]`

Replaces the INIT expressions for the current node.

Structure is updated

See also:: optional

void HrcNode_replace_input_variables	(	HrcNode_ptr	self,
		Olist_ptr	vars
	)			`[related]`

Replacess the local input variables of the current node.

Replaces the local input variables of the current node.

Structure is updated

See also:: optional

void HrcNode_replace_invar_assign_exprs	(	HrcNode_ptr	self,
		Olist_ptr	assigns
	)			`[related]`

Replaces the (*) := expressions for the current node.

Structure is updated

See also:: optional

void HrcNode_replace_invar_exprs	(	HrcNode_ptr	self,
		Olist_ptr	exprs
	)			`[related]`

Replaces the INVAR expressions for the current node.

Structure is updated

See also:: optional

void HrcNode_replace_invar_properties	(	HrcNode_ptr	self,
		Olist_ptr	invars
	)			`[related]`

Replaces the list of INVARIANT properties.

Structure is updated

See also:: optional

void HrcNode_replace_justice_exprs	(	HrcNode_ptr	self,
		Olist_ptr	justices
	)			`[related]`

Replaces the list of JUSTICE constraints.

Structure is updated

See also:: optional

void HrcNode_replace_ltl_properties	(	HrcNode_ptr	self,
		Olist_ptr	ltls
	)			`[related]`

Replaces the list of LTL properties.

Structure is updated

See also:: optional

void HrcNode_replace_next_assign_exprs	(	HrcNode_ptr	self,
		Olist_ptr	assigns
	)			`[related]`

Replaces the next(*) := expressions for the current node.

Replaces the next(*) := expressions for the current node. It is a list of implicitly conjoined assignments.

Structure is updated

See also:: optional

void HrcNode_replace_psl_properties	(	HrcNode_ptr	self,
		Olist_ptr	psls
	)			`[related]`

Replaces the list of PSL properties.

Structure is updated

See also:: optional

void HrcNode_replace_state_variables	(	HrcNode_ptr	self,
		Olist_ptr	vars
	)			`[related]`

Replaces the local state variables of the current node.

Structure is updated

See also:: optional

void HrcNode_replace_trans_exprs	(	HrcNode_ptr	self,
		Olist_ptr	exprs
	)			`[related]`

Replaces the TRANS expressions for the current node.

Structure is updated

See also:: optional

void HrcNode_set_child_hrc_nodes	(	HrcNode_ptr	self,
		Slist_ptr	list
	)			`[related]`

Sets the list of local childs for the current node.

Sets the list of local childs for the current node. Assumption is that the child nodes have the current node as parent.

Structure is updated

See also:: optional

void HrcNode_set_instance_name	(	HrcNode_ptr	self,
		node_ptr	name
	)			`[related]`

Sets the instance name of the node.

Structure is updated

See also:: optional

void HrcNode_set_lineno	(	HrcNode_ptr	self,
		int	lineno
	)			`[related]`

Sets the MOD_TYPE lineno of the node.

Structure is updated

See also:: optional

void HrcNode_set_name	(	HrcNode_ptr	self,
		node_ptr	name
	)			`[related]`

Sets the MOD_TYPE name of the node.

Structure is updated

See also:: optional

void HrcNode_set_parent	(	const HrcNode_ptr	self,
		HrcNode_ptr	father
	)			`[related]`

Sets the parent node of the node.

Structure is updated

See also:: optional

void HrcNode_set_symbol_table	(	HrcNode_ptr	self,
		SymbTable_ptr	st
	)			`[related]`

Sets the symbol table inside the node.

Structure is updated

See also:: optional

void HrcNode_set_undef	(	const HrcNode_ptr	self,
		void *	undef
	)			`[related]`

Getter for the undef field.

Getter for the undef field

See also:: HrcNode_set_undef

void HrcNode_unlink_nodes	(	HrcNode_ptr	self,
		HrcNode_ptr	child
	)			`[related]`

Unlink two nodes.

Unlink two nodes and "deinstantiate" child, since its instantiation makes sense only as a child of self

Field Documentation

Olist_ptr HrcNode::actual_parameters

Olist_ptr HrcNode::array_defines

hash_ptr HrcNode::assigns_table

Slist_ptr HrcNode::childs

Olist_ptr HrcNode::compassion

Olist_ptr HrcNode::compute_props

Olist_ptr HrcNode::constants

Olist_ptr HrcNode::ctl_props

Olist_ptr HrcNode::defines

Olist_ptr HrcNode::formal_parameters

Olist_ptr HrcNode::frozen_functions

Olist_ptr HrcNode::frozen_variables

Olist_ptr HrcNode::init_assign

Olist_ptr HrcNode::init_expr

Olist_ptr HrcNode::input_variables

node_ptr HrcNode::instance_name

Olist_ptr HrcNode::invar_assign

Olist_ptr HrcNode::invar_expr

Olist_ptr HrcNode::invar_props

Olist_ptr HrcNode::justice

int HrcNode::lineno

Olist_ptr HrcNode::ltl_props

node_ptr HrcNode::name

Olist_ptr HrcNode::next_assign

Olist_ptr HrcNode::next_expr

HrcNode_ptr HrcNode::parent

Olist_ptr HrcNode::psl_props

SymbTable_ptr HrcNode::st

Olist_ptr HrcNode::state_functions

Olist_ptr HrcNode::state_variables

void* HrcNode::undef

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

NuSMV/code/nusmv/core/hrc/HrcNode_private.h
NuSMV/code/nusmv/core/hrc/HrcNode.h

HrcNode Struct Reference

Public Member Functions

Data Fields

Related Functions

Detailed Description

Member Function Documentation

Friends And Related Function Documentation

Field Documentation