Hrc_WriteModel()
Prints the SMV module for the hrcNode.
Hrc_init_cmd()
Initializes the commands of the hrc package.
Hrc_init()
Initializes the hrc package.
Hrc_quit_cmd()
Removes the commands provided by the hrc package.
Hrc_quit()
Quits the hrc package.
hrc_prefix_utils_add_context()
Build the expression prefixed by context.
hrc_prefix_utils_assign_module_name()
Creates a new name for the module instance.
hrc_prefix_utils_flatten_instance_name()
Given an instance returns its flattened name.
hrc_prefix_utils_get_first_subcontext()
Get the first subcontext of the given symbol.
hrc_prefix_utils_get_prefix_symbols()
Given a set of symbol returns a new set that contains only symbols that have a given prefix.
hrc_prefix_utils_is_subprefix()
Returns true if subprefix is contained in prefix.
hrc_prefix_utils_remove_context()
Removes context from identifier.
hrc_write_assign_list()
Writes ASSIGN declarations in SMV format on a file.
hrc_write_constants()
Prints in the output file the SMV representations of constants list.
hrc_write_declare_module_variables()
Declare a module variables, setting the module to use and the actual parameters.
hrc_write_expr_split()
Writes an expression in SMV format on a file.
hrc_write_expr()
Writes expression in SMV format on a file.
hrc_write_module_instance()
Writes the SMV translation of the instance module contained in hrcNode on file.
hrc_write_parameters()
Prints a list of parameters for module declaration or instantiation.
hrc_write_print_assign()
Prints an assignement statement
hrc_write_print_defines()
Writes DEFINE declarations in SMV format on a file.
hrc_write_print_mdefines()
Writes the MDEFINE declarations contained in hrcNode.
hrc_write_print_var_list()
Prints a list of variables.
hrc_write_print_vars()
Prints the variable of the module contained in hrcNode.
hrc_write_spec_pair_list()
Writes a list of specification that contains pairs in SMV format.
hrc_write_spec_split()
Writes a specification list in SMV format on a file.
hrc_write_specifications()
Writes all the specifications of a module instance.
hrc_write_spec()
Prints the given specification.

Last updated on 2010/05/19 22h:26