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

#include "cudd/util.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/opt/OptsHandler.h"
#include "nusmv/core/cinit/NuSMVEnv.h"

Go to the source code of this file.

Defines
#define	CINIT_IS_DEPRECATED true
#define	CINIT_IS_PUBLIC true
#define	CINIT_NO_CONFLICT NULL
#define	CINIT_NO_DEPENDENCY NULL
#define	CINIT_NO_PARAMETER NULL
#define	NUSMV_LIBRARY_BUGREPORT "Please report bugs to <nusmv-users@fbk.eu>"
#define	NUSMV_LIBRARY_BUILD_DATE "<compile date not supplied>"
#define	NUSMV_LIBRARY_EMAIL "nusmv-users@list.fbk.eu"
#define	NUSMV_LIBRARY_NAME "NuSMV"
	"Main" package of NuSMV ("cinit" = core init).
#define	NUSMV_LIBRARY_VERSION "2.5.0"
#define	NUSMV_LIBRARY_WEBSITE "http://nusmv.fbk.eu"
Typedefs
typedef void(*	FP_V_E )(NuSMVEnv_ptr)
Functions
void	CInit_BannerPrint (FILE *file)
	Prints the banner of NuSMV.
void	CInit_BannerPrint_cudd (FILE *file)
	Prints the banner of cudd.
void	CInit_BannerPrint_minisat (FILE *file)
	Prints the banner of minisat.
void	CInit_BannerPrint_nusmv_library (FILE *file)
	Prints the banner of the NuSMV library.
void	CInit_BannerPrint_zchaff (FILE *file)
	Prints the banner of zchaff.
void	CInit_BannerPrintLibrary (FILE *file)
	Prints the COMPLETE banner of the NuSMV library.
char *	CInit_NuSMVObtainLibrary (void)
	Returns the NuSMV library path.
char *	CInit_NuSMVReadVersion (void)
	Returns the current NuSMV version.
char *	get_preprocessor_call (const NuSMVEnv_ptr env, const char *name)
	Gets the command line call for the specified pre-processor name. Returns NULL if given name is not available, or a string that must be NOT freed.
char *	get_preprocessor_filename (const NuSMVEnv_ptr env, const char *name)
	Gets the actual program name of the specified pre-processor. Returns NULL if given name is not available, or a string that must be freed.
char *	get_preprocessor_names (const NuSMVEnv_ptr env)
	Gets the names of the avaliable pre-processors. Returned string must be freed.
int	get_preprocessors_num (const NuSMVEnv_ptr env)
	Returns the number of available proprocessors.
void	init_preprocessors (const NuSMVEnv_ptr env)
	Initializes information about the pre-processors avaliable.
void	NuSMVCore_add_command_line_option (char name, char usage, char parameter, boolean(check_and_apply)(OptsHandler_ptr, char , NuSMVEnv_ptr), boolean is_deprecated, boolean is_public, char dependency, char *conflict)
	Adds a command line option to the system.
void	NuSMVCore_add_env_command_line_option (char name, char usage, char parameter, char env_var, boolean is_deprecated, boolean is_public, char dependency, char conflict)
	Adds a command line option to the system.
char *	NuSMVCore_get_bug_report_message (void)
	The Sm bug_report_message field getter.
char *	NuSMVCore_get_build_date (void)
	The Sm build_date field getter.
char *	NuSMVCore_get_email (void)
	The Sm email field getter.
char *	NuSMVCore_get_library_bug_report_message (void)
	The Sm library_bug_report_message field getter.
char *	NuSMVCore_get_library_build_date (void)
	The Sm library_build_date field getter.
char *	NuSMVCore_get_library_email (void)
	The Sm library_email field getter.
char *	NuSMVCore_get_library_name (void)
	The Sm library_name field getter.
char *	NuSMVCore_get_library_version (void)
	The Sm library_version field getter.
char *	NuSMVCore_get_library_website (void)
	The Sm library_website field getter.
char *	NuSMVCore_get_linked_addons (void)
	The Sm linked_addons field getter.
char *	NuSMVCore_get_prompt_string (void)
	The Sm prompt_string field getter.
char *	NuSMVCore_get_tool_name (void)
	The Sm tool_name field getter.
char *	NuSMVCore_get_tool_rc_file_name (void)
	The Sm tool rc file name field getter.
char *	NuSMVCore_get_tool_version (void)
	The Sm tool_version field getter.
char *	NuSMVCore_get_website (void)
	The Sm website field getter.
void	NuSMVCore_init (NuSMVEnv_ptr env, FP_V_E fns[][2], int)
	Initializes the system.
void	NuSMVCore_init_cmd_options (NuSMVEnv_ptr env)
	Initializes all NuSMV library command line options.
void	NuSMVCore_init_data (void)
	Initializes the NuSMVCore data. This function has to be called _BEFORE_ doing anything else with the library.
boolean	NuSMVCore_main (NuSMVEnv_ptr env, int argc, char *argv, int status)
	Executes the main program.
void	NuSMVCore_quit (NuSMVEnv_ptr env)
	Shuts down the system.
void	NuSMVCore_quit_extended (NuSMVEnv_ptr env, const boolean keep_core_data)
	Shuts down the system.
void	NuSMVCore_reset (NuSMVEnv_ptr env)
	Shuts down and restarts the system.
void	NuSMVCore_set_banner_print_fun (void(banner_print_fun)(FILE ))
	The Sm banner_print_fun field setter.
void	NuSMVCore_set_batch_fun (void(*batch_fun)(NuSMVEnv_ptr))
	The Sm batch fun field setter.
void	NuSMVCore_set_bug_report_message (char *bug_report_message)
	The Sm bug_report_message field setter.
void	NuSMVCore_set_build_date (char *build_date)
	The Sm build_date field setter.
void	NuSMVCore_set_email (char *email)
	The Sm email field setter.
void	NuSMVCore_set_library_build_date (const char *)
	The Sm library_build_date field getter.
void	NuSMVCore_set_library_email (const char *)
	The Sm library_email field getter.
void	NuSMVCore_set_library_name (const char *)
	The Sm library_name field getter.
void	NuSMVCore_set_library_website (const char *)
	The Sm library_website field setter.
void	NuSMVCore_set_linked_addons (char *linked_addons)
	The Sm linked_addons field setter.
void	NuSMVCore_set_prompt_string (char *prompt_string)
	The Sm prompt_string field setter.
void	NuSMVCore_set_tool_name (char *tool_name)
	The Sm tool_name field setter.
void	NuSMVCore_set_tool_version (char *tool_version)
	The Sm tool_version field setter.
void	NuSMVCore_set_website (char *website)
	The Sm website field setter.
void	quit_preprocessors (const NuSMVEnv_ptr env)
	Removes information regarding the avaliable pre-processors.
Variables
FILE *	nusmv_historyFile

Define Documentation

#define CINIT_IS_DEPRECATED true

Todo:: Missing synopsis

Todo:: Missing description

#define CINIT_IS_PUBLIC true

Todo:: Missing synopsis

Todo:: Missing description

#define CINIT_NO_CONFLICT NULL

Todo:: Missing synopsis

Todo:: Missing description

#define CINIT_NO_DEPENDENCY NULL

Todo:: Missing synopsis

Todo:: Missing description

#define CINIT_NO_PARAMETER NULL

Todo:: Missing synopsis

Todo:: Missing description

#define NUSMV_LIBRARY_BUGREPORT "Please report bugs to <nusmv-users@fbk.eu>"

Todo:: Missing synopsis

Todo:: Missing description

#define NUSMV_LIBRARY_BUILD_DATE "<compile date not supplied>"

Todo:: Missing synopsis

Todo:: Missing description

#define NUSMV_LIBRARY_EMAIL "nusmv-users@list.fbk.eu"

Todo:: Missing synopsis

Todo:: Missing description

#define NUSMV_LIBRARY_NAME "NuSMV"

"Main" package of NuSMV ("cinit" = core init).

Author:: Adapted to NuSMV by Marco Roveri

Todo:: : Missing description

Todo:: Missing synopsis

Todo:: Missing description

#define NUSMV_LIBRARY_VERSION "2.5.0"

Todo:: Missing synopsis

Todo:: Missing description

#define NUSMV_LIBRARY_WEBSITE "http://nusmv.fbk.eu"

Todo:: Missing synopsis

Todo:: Missing description

Typedef Documentation

typedef void(* FP_V_E)(NuSMVEnv_ptr)

Todo:: Missing synopsis

Todo:: Missing description

Function Documentation

void CInit_BannerPrint ( FILE * file )

Prints the banner of NuSMV.

void CInit_BannerPrint_cudd ( FILE * file )

Prints the banner of cudd.

void CInit_BannerPrint_minisat ( FILE * file )

Prints the banner of minisat.

void CInit_BannerPrint_nusmv_library ( FILE * file )

Prints the banner of the NuSMV library.

To be used by tools linking against the NuSMV library and using custom banner function

void CInit_BannerPrint_zchaff ( FILE * file )

Prints the banner of zchaff.

void CInit_BannerPrintLibrary ( FILE * file )

Prints the COMPLETE banner of the NuSMV library.

To be used by addons linking against the NuSMV library. You can use this as banner print function if you don't need a special banner print function and you are linking against NuSMV

char* CInit_NuSMVObtainLibrary ( void )

Returns the NuSMV library path.

Returns a string giving the directory which contains the standard NuSMV library. Used to find things like the default .nusmvrc, the on-line help files, etc. It is the responsibility of the user to free the returned string.

See also:: CInit_NuSMVReadVersion

char* CInit_NuSMVReadVersion ( void )

Returns the current NuSMV version.

AutomaticStart

Returns a static string giving the NuSMV version and compilation timestamp. The user should not free this string.

See also:: CInit_NuSMVObtainLibrary

char* get_preprocessor_call	(	const NuSMVEnv_ptr	env,
		const char *	name
	)

Gets the command line call for the specified pre-processor name. Returns NULL if given name is not available, or a string that must be NOT freed.

Todo:: Missing description

char* get_preprocessor_filename	(	const NuSMVEnv_ptr	env,
		const char *	name
	)

Gets the actual program name of the specified pre-processor. Returns NULL if given name is not available, or a string that must be freed.

Todo:: Missing description

char* get_preprocessor_names ( const NuSMVEnv_ptr env )

Gets the names of the avaliable pre-processors. Returned string must be freed.

Todo:: Missing description

int get_preprocessors_num ( const NuSMVEnv_ptr env )

Returns the number of available proprocessors.

Todo:: Missing description

void init_preprocessors ( const NuSMVEnv_ptr env )

Initializes information about the pre-processors avaliable.

Todo:: Missing description

void NuSMVCore_add_command_line_option	(	char *	name,
		char *	usage,
		char *	parameter,
		boolean()(OptsHandler_ptr, char , NuSMVEnv_ptr)	check_and_apply,
		boolean	is_deprecated,
		boolean	is_public,
		char *	dependency,
		char *	conflict
	)

Adds a command line option to the system.

When the command line option is specified, the check_and_apply function is called, which should first check that the (possible) parameter is valid, and then perform an action on it.

Function arguments: 1) name -> The name of the cmd line option (e.g. -int) 2) usage -> The usage string that will be printed in the help (i.e. -help) 3) parameter -> NULL if none, a string value if any. e.g: "k" for bmc_length 4) check_and_apply -> The function that checks the (possible) parameter value and performs an action 5) public -> Tells whether the cmd line option is public or not. If not, the usage is not printed when invoking the tool with -h. 6) deprecated -> Tells whether the cmd line options is deprecated or not 7) dependency -> The possibly option name on which this one dependens on. NULL if none. e.g. -bmc_length depends on -bmc 8) conflict -> The list of option names that conflict with this one. e.g. -mono conflicts with "-thresh -iwls95"

See also:: NuSMVCore_add_env_command_line_option

void NuSMVCore_add_env_command_line_option	(	char *	name,
		char *	usage,
		char *	parameter,
		char *	env_var,
		boolean	is_deprecated,
		boolean	is_public,
		char *	dependency,
		char *	conflict
	)

Adds a command line option to the system.

Adds a command line option to the system. The command line option MUST have an environment option associated. When the command line option is specified, the environment option is automatically set to the correct value (In case of boolean options, the current value is negated, in any other case, the cmd option requires an argument which is set to the associated option

Function arguments: 1) name -> The name of the cmd line option (e.g. -int) 2) usage -> The usage string that will be printed in the help (i.e. -help) 3) parameter -> NULL if none, a string value if any. e.g: "k" for bmc_length 4) env_var -> The associated environment variable name 5) public -> Tells whether the cmd line option is public or not. If not, the usage is not printed when invoking the tool with -h. 6) deprecated -> Tells whether the cmd line options is deprecated or not 7) dependency -> The possibly option name on which this one dependens on. NULL if none. e.g. -bmc_length depends on -bmc 8) conflict -> The list of option names that conflict with this one. e.g. -mono conflicts with "-thresh -iwls95"

See also:: NuSMVCore_add_command_line_option

char* NuSMVCore_get_bug_report_message ( void )

The Sm bug_report_message field getter.

The Sm bug_report_message field getter

See also:: NuSMVCore_set_bug_report_message

char* NuSMVCore_get_build_date ( void )

The Sm build_date field getter.

The Sm build_date field getter

See also:: NuSMVCore_set_build_date

char* NuSMVCore_get_email ( void )

The Sm email field getter.

The Sm email field getter

See also:: NuSMVCore_set_email

char* NuSMVCore_get_library_bug_report_message ( void )

The Sm library_bug_report_message field getter.

The Sm library_bug_report_message field getter

See also:: NuSMVCore_get_bug_report_message

char* NuSMVCore_get_library_build_date ( void )

The Sm library_build_date field getter.

The Sm library_build_date field getter

See also:: NuSMVCore_get_build_date

char* NuSMVCore_get_library_email ( void )

The Sm library_email field getter.

The Sm library_email field getter

See also:: NuSMVCore_get_email

char* NuSMVCore_get_library_name ( void )

The Sm library_name field getter.

The Sm library_name field getter

See also:: NuSMVCore_get_tool_name

char* NuSMVCore_get_library_version ( void )

The Sm library_version field getter.

The Sm library_version field getter

See also:: NuSMVCore_get_tool_version

char* NuSMVCore_get_library_website ( void )

The Sm library_website field getter.

The Sm library_website field getter

See also:: NuSMVCore_get_website

char* NuSMVCore_get_linked_addons ( void )

The Sm linked_addons field getter.

The Sm linked_addons field getter

See also:: NuSMVCore_set_linked_addons

char* NuSMVCore_get_prompt_string ( void )

The Sm prompt_string field getter.

The Sm prompt_string field getter

See also:: NuSMVCore_set_prompt_string

char* NuSMVCore_get_tool_name ( void )

The Sm tool_name field getter.

The Sm tool_name field getter

See also:: NuSMVCore_set_tool_name

char* NuSMVCore_get_tool_rc_file_name ( void )

The Sm tool rc file name field getter.

The Sm tool rc file name field getter

See also:: NuSMVCore_set_tool_name

char* NuSMVCore_get_tool_version ( void )

The Sm tool_version field getter.

The Sm tool_version field getter

See also:: NuSMVCore_set_tool_version

char* NuSMVCore_get_website ( void )

The Sm website field getter.

The Sm website field getter

See also:: NuSMVCore_set_website

void NuSMVCore_init	(	NuSMVEnv_ptr	env,
		FP_V_E	fns[][2],
		int
	)

Initializes the system.

Initializes the system. First calls the NuSMVCore initialization function, and then calls each initialization function that is in the given list. The order of the list is followed. The list must be declared as follows:

FP_V_E funs[][2] = {{Init_1, Quit_1}, {Init_2, Quit_2}, ... {Init_n, Quit_n} }

See also:: NuSMVCore_set_reset_first_fun NuSMVCore_set_reset_last_fun

void NuSMVCore_init_cmd_options ( NuSMVEnv_ptr env )

Initializes all NuSMV library command line options.

Initializes all NuSMV library command line options. All command line options are registered within the library. If standard command line options are needed, this function has to be called before NuSMVCore_main and after NuSMVCore_init

See also:: Package_init Package_main

void NuSMVCore_init_data ( void )

Initializes the NuSMVCore data. This function has to be called _BEFORE_ doing anything else with the library.

Initializes the NuSMVCore data. The following operations are performed:

1) Initialize the internal class 2) Sets all fields to default for NuSMV

See also:: Package_init_cmd_options Package_init

boolean NuSMVCore_main	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv,
		int *	status
	)

Executes the main program.

See also:: NuSMVCore_init NuSMVCore_quit

void NuSMVCore_quit ( NuSMVEnv_ptr env )

Shuts down the system.

Shuts down the system. First all quit functions in the list given to NuSMVCore_init are called. Then all complex structures that have a dependency among some internal packages are deinitialized. After that, the Core is shut down and finally all simple internal structures are freed

See also:: NuSMVCore_set_reset_first_fun NuSMVCore_set_reset_last_fun, NuSMVCore_quit_extended

void NuSMVCore_quit_extended	(	NuSMVEnv_ptr	env,
		const boolean	keep_core_data
	)

Shuts down the system.

Shuts down the system. First all quit functions in the list given to NuSMVCore_init are called. Then all complex structures that have a dependency among some internal packages are deinitialized. After that, the Core is shut down and finally, if keep_core_data is false, all simple internal structures are freed

Lot of code duplication with NuSMVCore_quit. The parameter keep_core_data is useful to avoid issues related to the non-reentrancy of data structure in cinitData.c (core_data) See bug 4119.

See also:: NuSMVCore_set_reset_first_fun NuSMVCore_set_reset_last_fun

void NuSMVCore_reset ( NuSMVEnv_ptr env )

Shuts down and restarts the system.

Shuts down and restarts the system. 4 steps are done: 1) Call the reset_first function (if any). 2) Call the NuSMV package reset_first function 3) Call the NuSMV package reset_last function 4) Call the reset_last function (if any)