CommandHrcWriteModel()
Writes the SMV model contained in the root node of the hrc structure.
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.
UsageHrcWriteModel()
Prints the usage of the command UsageHrcWriteModel
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_array_defines()
Writes the ARRAY DEFINE declarations contained in hrcNode.
hrc_write_print_assign()
Prints an assignement statement
hrc_write_print_defines()
Writes DEFINE declarations in SMV format on a file.
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.
print_scalar_type()
Prints the scalar type of a variable.
print_variable_type()
Prints the type of a variable.
()
Suffix used to rename module names and module variables

Last updated on 2011/04/06 21h:12