NuSMV/code/nusmv/shell/hrc/hrcCmd.h File Reference

#include "nusmv/core/utils/utils.h"

Go to the source code of this file.

Functions
int	CommandHrcDumpModel (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandHrcWriteModel (NuSMVEnv_ptr env, int argc, char **argv)
	The header file for the shell interface of the hrc packace.
void	Hrc_init_cmd (NuSMVEnv_ptr env)
	Initializes the commands of the hrc package.
void	Hrc_quit_cmd (NuSMVEnv_ptr env)
	Removes the commands provided by the hrc package.

---

Function Documentation

int CommandHrcDumpModel	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

hrc_dump_model: Writes the hrc structure from root node to a given SMV file

Command arguments: [-h] | [-o "filename"] [-d] Writes the currently loaded SMV model stored in hrc structure in the specified file. If no file is specified the standard output is used.

Command Options:

-f "format"

Dumps in the given format (debug, smv or xml).

-o "filename"

Dumps output to "filename"

-d

Renames every module name appending the suffix "_hrc"

-i

Disable indentation.

int CommandHrcWriteModel	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

The header file for the shell interface of the hrc packace.

Author:

Sergio Mover

Todo:

: Missing description

AutomaticStart

Command:

hrc_write_model: Writes the hrc structure from root node to a given SMV file

Command arguments: [-h] | [-o "filename"] [-d]

Writes the currently loaded SMV model stored in hrc structure in the specified file. If no file is specified the

standard output is used.

Command Options:

-o "filename"

Attempts to write the SMV model in "filename".

-d

Renames modules appending "_hrc" the the original module name.

void Hrc_init_cmd

(

NuSMVEnv_ptr

env

)

Initializes the commands of the hrc package.

AutomaticEnd

void Hrc_quit_cmd

(

NuSMVEnv_ptr

env

)

Removes the commands provided by the hrc package.