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

#include "nusmv/core/set/set.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/hrc/hrc.h"
#include "nusmv/core/cinit/NuSMVEnv.h"

Go to the source code of this file.

Functions
node_ptr	hrc_prefix_utils_add_context (NodeMgr_ptr nodemgr, node_ptr context, node_ptr expression)
	Build the expression prefixed by context.
node_ptr	hrc_prefix_utils_assign_module_name (HrcNode_ptr instance, node_ptr instance_name)
	Creates a new name for the module instance.
node_ptr	hrc_prefix_utils_concat_context (const NuSMVEnv_ptr env, node_ptr ctx1, node_ptr ctx2)
node_ptr	hrc_prefix_utils_contextualize_expr (const NuSMVEnv_ptr env, node_ptr expr, node_ptr context)
node_ptr	hrc_prefix_utils_get_first_subcontext (node_ptr symbol)
	Get the first subcontext of the given symbol.
Set_t	hrc_prefix_utils_get_prefix_symbols (Set_t symbol_set, node_ptr prefix)
	Header of hrcPrefixUtils.c.
boolean	hrc_prefix_utils_is_subprefix (node_ptr subprefix, node_ptr prefix)
	Returns true if subprefix is contained in prefix.
node_ptr	hrc_prefix_utils_remove_context (NodeMgr_ptr nodemgr, node_ptr identifier, node_ptr context)
	Removes context from identifier.

---

Function Documentation

node_ptr hrc_prefix_utils_add_context	(	NodeMgr_ptr	nodemgr,
		node_ptr	context,
		node_ptr	expression
	)

Build the expression prefixed by context.

Build the expression prefixed by context.

If expression is of DOT or CONTEXT type we cannot build the tree DOT(context, expression). We need to recursively visit expression to build a correct DOT tree.

node_ptr hrc_prefix_utils_assign_module_name	(	HrcNode_ptr	instance,
		node_ptr	instance_name
	)

Creates a new name for the module instance.

Creates a new name for the module instance.

The generated module name is <module_name>_<module_instance_flattened_name>

node_ptr hrc_prefix_utils_concat_context	(	const NuSMVEnv_ptr	env,
		node_ptr	ctx1,
		node_ptr	ctx2
	)

node_ptr hrc_prefix_utils_contextualize_expr	(	const NuSMVEnv_ptr	env,
		node_ptr	expr,
		node_ptr	context
	)

node_ptr hrc_prefix_utils_get_first_subcontext

(

node_ptr

symbol

)

Get the first subcontext of the given symbol.

Get the first subcontext of the given symbol.

Search the second CONTEXT or DOT node in symbol and returns it. If it is not found then Nil is returned.

DOT and CONTEXT nodes are always searched in the car node.

Set_t hrc_prefix_utils_get_prefix_symbols	(	Set_t	symbol_set,
		node_ptr	prefix
	)

Header of hrcPrefixUtils.c.

Author:

Sergio Mover

Todo:

: Missing description

AutomaticStart

Given a set of symbol returns a new set that contains only symbols that have a given prefix. Given a set of symbol returns a new set that contains only symbols that have a given prefix.

The returned set must be destroyed by the caller.

boolean hrc_prefix_utils_is_subprefix	(	node_ptr	subprefix,
		node_ptr	prefix
	)

Returns true if subprefix is contained in prefix.

node_ptr hrc_prefix_utils_remove_context	(	NodeMgr_ptr	nodemgr,
		node_ptr	identifier,
		node_ptr	context
	)

Removes context from identifier.

Removes context from identifier. If context is not