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

#include "nusmv/core/hrc/HrcNode.h"
#include "nusmv/core/hrc/dumpers/HrcDumper.h"
#include "nusmv/core/set/set.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/cinit/NuSMVEnv.h"

Go to the source code of this file.

Enumerations
enum	HrcDumpFormat { HRC_DUMP_FORMAT_INVALID = 0, HRC_DUMP_FORMAT_DEBUG = 1, HRC_DUMP_FORMAT_SMV, HRC_DUMP_FORMAT_XML }
	The package to manage the NuSMV module hierachy. More...
Functions
char *	Hrc_dump_format_enum_to_str (HrcDumpFormat format)
char *	Hrc_dump_format_get_available (void)
HrcDumpFormat	Hrc_dump_format_str_to_enum (char *format)
int	Hrc_dump_model (const NuSMVEnv_ptr env, HrcDumpFormat format, FILE *ofileid, const boolean append_suffix, const boolean use_indent)
	Writes the SMV model contained in the root node of the hrc structure.
void	Hrc_DumpModel (HrcNode_ptr hrcNode, HrcDumper_ptr dumper)
	Prints the SMV module for the hrcNode.
void	Hrc_init (NuSMVEnv_ptr env)
	Initializes the hrc package.
void	Hrc_quit (NuSMVEnv_ptr env)
	Quits the hrc package.
int	Hrc_WriteModel (HrcNode_ptr self, FILE *ofile, boolean append_suffix)
	DEPRECATED Prints the SMV module for the hrcNode.

---

Enumeration Type Documentation

enum HrcDumpFormat

The package to manage the NuSMV module hierachy.

Author:

Marco Roveri The package to manage the NuSMV module hierachy.

The possible type of printing of an hrc

Enumerator:

HRC_DUMP_FORMAT_INVALID
HRC_DUMP_FORMAT_DEBUG
HRC_DUMP_FORMAT_SMV
HRC_DUMP_FORMAT_XML

---

Function Documentation

char* Hrc_dump_format_enum_to_str

(

HrcDumpFormat

format

)

char* Hrc_dump_format_get_available

(

void

)

HrcDumpFormat Hrc_dump_format_str_to_enum

(

char *

format

)

int Hrc_dump_model	(	const NuSMVEnv_ptr	env,
		HrcDumpFormat	format,
		FILE *	ofileid,
		const boolean	append_suffix,
		const boolean	use_indent
	)

Writes the SMV model contained in the root node of the hrc structure.

Based on the format, constructs the right dumper. Then dump the hrc model. ownership of ofileid is taken (by the dumpers)

void Hrc_DumpModel	(	HrcNode_ptr	hrcNode,
		HrcDumper_ptr	dumper
	)

Prints the SMV module for the hrcNode.

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

(

NuSMVEnv_ptr

env

)

Initializes the hrc package.

AutomaticStart

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

(

NuSMVEnv_ptr

env

)

Quits the hrc package.

Quits the hrc package, freeing the global variable mainHrcNode and removing the hrc commands.

See also:

TracePkg_init

int Hrc_WriteModel	(	HrcNode_ptr	self,
		FILE *	ofile,
		boolean	append_suffix
	)

DEPRECATED Prints the SMV module for the hrcNode.

Deprecated function. Use Hrc_DumpModel or Hrc_dump_model instead.

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.