-
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_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.
Last updated on 2010/11/03 21h:54