void 
Hrc_WriteModel(
  HrcNode_ptr  hrcNode, 
  FILE * ofile, 
  boolean  append_suffix 
)
Prints the SMV module for the hrcNode. If the flag append_suffix is true then the suffix HRC_WRITE_MODULE_SUFFIX is appended when a module type is printed. So HRC_WRITE_MODULE_SUFFIX is appended to the module name in module declarations and to the module name in a module instantiation. The feature is needed for testing to avoid name clash among modules names when the original model and the model generated from hrc are merged.


void 
Hrc_init_cmd(
    
)
Initializes the commands of the hrc package.


void 
Hrc_init(
    
)
Initializes the hrc package. The initialization consists of the allocation of the mainHrcNode global variable and the initialization of the hrc package commands.

See Also TracePkg_quit

void 
Hrc_quit_cmd(
    
)
Removes the commands provided by the hrc package.


void 
Hrc_quit(
    
)
Quits the hrc package, freeing the global variable mainHrcNode and removing the hrc commands.

See Also TracePkg_init

node_ptr 
hrc_prefix_utils_add_context(
  node_ptr  context, 
  node_ptr  expression 
)
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. The generated module name is _


node_ptr 
hrc_prefix_utils_flatten_instance_name(
  HrcNode_ptr  instance 
)
Given an instance returns its flattened name.


node_ptr 
hrc_prefix_utils_get_first_subcontext(
  node_ptr  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 
)
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(
  node_ptr  identifier, 
  node_ptr  context 
)
Removes context from identifier. If context is not


boolean 
hrc_write_assign_list(
  FILE* out, 
  int  assign_node_type, 
  node_ptr  assign_list 
)
Writes ASSIGN declarations in SMV format on a file. Function returns true if at least an assign was written


boolean 
hrc_write_constants(
  FILE * out, 
  node_ptr  constants_list 
)
Prints in the output file the SMV representations of constants list. Function returns true if at least a constant was printed.


void 
hrc_write_declare_module_variables(
  FILE * ofile, 
  HrcNode_ptr  child, 
  st_table* printed_module_map, 
  boolean  append_suffix 
)
Declare a module variables, setting the module to use and the actual parameters.

Side Effects printed_module_map is changed in the recursive calls of the the function.


boolean 
hrc_write_expr_split(
  FILE* out, 
  node_ptr  n, 
  const char* s 
)
Writes a generic expression prefixed by a given string in SMV format on a file. Returns true if at least one expression was printed.


void 
hrc_write_expr(
  FILE* out, 
  node_ptr  n, 
  const char* s 
)
Writes a generic expression prefixed by a given string in SMV format on a file.


void 
hrc_write_module_instance(
  FILE * ofile, 
  HrcNode_ptr  hrcNode, 
  st_table* printed_module_map, 
  boolean  append_suffix 
)
Writes the SMV translation of the instance module contained in hrcNode on file.

Side Effects printed_module_map is changed to keep track of printed modules.


void 
hrc_write_parameters(
  FILE* ofile, 
  node_ptr  parameters_list 
)
Prints a list of parameters for module declaration or instantiation. The parameter list is printed enclosed by brackets, every parameter is separated by colon.


void 
hrc_write_print_assign(
  FILE * out, 
  node_ptr  lhs, 
  node_ptr  rhs 
)
Prints an assignement statement


void 
hrc_write_print_defines(
  FILE* out, 
  HrcNode_ptr  hrcNode 
)
Writes DEFINE declarations in SMV format on a file.


void 
hrc_write_print_mdefines(
  FILE* out, 
  HrcNode_ptr  hrcNode 
)
Writes the MDEFINE declarations contained in hrcNode.


void 
hrc_write_print_var_list(
  FILE* out, 
  node_ptr  var_list 
)
Prints a list of variables.


void 
hrc_write_print_vars(
  FILE* out, 
  HrcNode_ptr  hrcNode 
)
Prints the variable of the module contained in hrcNode. The sections printed are VAR, IVAR and FROZENVAR.


void 
hrc_write_spec_pair_list(
  FILE* out, 
  node_ptr  pair_list, 
  char* section_name 
)
Writes a list of specification that contains pairs in SMV format.


boolean 
hrc_write_spec_split(
  FILE* out, 
  node_ptr  n, 
  const char* s 
)
Writes a specification list prefixed by a given string in SMV format on a file. Returns true if at least one specification was printed.


void 
hrc_write_specifications(
  FILE* out, 
  HrcNode_ptr  hrcNode 
)
Writes all the specifications of a module instance.


void 
hrc_write_spec(
  FILE* out, 
  node_ptr  spec, 
  const char* msg 
)
Prints in out file the specification.


Last updated on 2010/05/19 15h:56