void
CInit_BannerPrintLibrary(
FILE * file
)
- 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
- Defined in
cinitVers.c
void
CInit_BannerPrint_cudd(
FILE * file
)
- Prints the banner of cudd.
- Defined in
cinitVers.c
void
CInit_BannerPrint_minisat(
FILE * file
)
- Prints the banner of minisat.
- Defined in
cinitVers.c
void
CInit_BannerPrint_nusmv_library(
FILE * file
)
- To be used by tools linking against the NuSMV library
and using custom banner function
- Defined in
cinitVers.c
void
CInit_BannerPrint_zchaff(
FILE * file
)
- Prints the banner of zchaff.
- Defined in
cinitVers.c
void
CInit_BannerPrint(
FILE * file
)
- Prints the banner of NuSMV.
- Defined in
cinitVers.c
int
CInit_NuSMVEndPrintMore(
)
- This function is called to terminate piping
stdout through "more". It is important to call
CInit_NuSMVEndPrintMore before exiting your
function (preferably at the end of your
printing; failing to do so will cause the stdin
lines not to appear). The function returns a 0
if it fails.
- See Also
CInit_NuSMVInitPrintMore
- Defined in
cinitVers.c
void
CInit_NuSMVInitPrintMore(
)
- This function is called to initialize piping
stdout through "more". It is important to call
CInit_NuSMVEndPrintMore before returning from
your function and after calling
CInit_NuSMVInitPrintMore (preferably at the end
of your printing; failing to do so will cause
the stdin lines not to appear).
- See Also
CInit_NuSMVEndPrintMore
- Defined in
cinitVers.c
char*
CInit_NuSMVObtainLibrary(
)
- 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
- Defined in
cinitVers.c
char*
CInit_NuSMVReadVersion(
)
- Returns a static string giving the NuSMV version and compilation
timestamp. The user should not free this string.
- See Also
CInit_NuSMVObtainLibrary
- Defined in
cinitVers.c
int
CInit_NusmvrcSource(
)
- Sources the .nusmvrc file. Always sources the .nusmvrc from
library. Then source the .nusmvrc from the home directory. If there is none
in the home directory, then execute the one in the current directory if one
is present. Returns 1 if scripts were successfully executed, else return 0.
- See Also
optional
- Defined in
cinitMisc.c
void
CInit_end(
)
- Calls the end routines of all the packages.
- Side Effects Closes the output files if not the standard ones.
- See Also
CInit_Init
- Defined in
cinitInit.c
void
CInit_init(
)
- Calls the initialization routines of all the packages.
- Side Effects Sets the global variables nusmv_stdout, nusmv_stderr,
nusmv_historyFile.
- See Also
SmEnd
- Defined in
cinitInit.c
void
CInit_reset_first(
)
- Shuts down and restarts the system, shut down part
- See Also
CInit_reset_last
- Defined in
cinitInit.c
void
CInit_reset_last(
)
- Shuts down and restarts the system, restart part
- See Also
CInit_reset_first
- Defined in
cinitInit.c
int
CommandCmdReset(
int argc,
char ** argv
)
- Implements the reset command.
- Defined in
cinitCmd.c
int
CommandPrintUsage(
int argc,
char ** argv
)
- Implements the print_usage command.
- Side Effects required
- Defined in
cinitCmd.c
static char *
DateReadFromDateString(
char * datestr
)
- optional
- Defined in
cinitVers.c
void
NuSMVCore_add_env_command_line_option(
char* name,
char* usage,
char* parameter,
char* env_var,
boolean public,
boolean deprecated,
char* dependency,
char* conflict
)
- 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
- Defined in
cinitData.c
char*
NuSMVCore_get_bug_report_message(
)
- The Sm bug_report_message field getter
- See Also
NuSMVCore_set_bug_report_message
- Defined in
cinitData.c
char*
NuSMVCore_get_build_date(
)
- The Sm build_date field getter
- See Also
NuSMVCore_set_build_date
- Defined in
cinitData.c
char*
NuSMVCore_get_email(
)
- The Sm email field getter
- See Also
NuSMVCore_set_email
- Defined in
cinitData.c
char*
NuSMVCore_get_library_bug_report_message(
)
- The Sm library_bug_report_message field getter
- See Also
NuSMVCore_get_bug_report_message
- Defined in
cinitData.c
char*
NuSMVCore_get_library_build_date(
)
- The Sm library_build_date field getter
- See Also
NuSMVCore_get_build_date
- Defined in
cinitData.c
char*
NuSMVCore_get_library_email(
)
- The Sm library_email field getter
- See Also
NuSMVCore_get_email
- Defined in
cinitData.c
char*
NuSMVCore_get_library_name(
)
- The Sm library_name field getter
- See Also
NuSMVCore_get_tool_name
- Defined in
cinitData.c
char*
NuSMVCore_get_library_version(
)
- The Sm library_version field getter
- See Also
NuSMVCore_get_tool_version
- Defined in
cinitData.c
char*
NuSMVCore_get_library_website(
)
- The Sm library_website field getter
- See Also
NuSMVCore_get_website
- Defined in
cinitData.c
char*
NuSMVCore_get_linked_addons(
)
- The Sm linked_addons field getter
- See Also
NuSMVCore_set_linked_addons
- Defined in
cinitData.c
char*
NuSMVCore_get_prompt_string(
)
- The Sm prompt_string field getter
- See Also
NuSMVCore_set_prompt_string
- Defined in
cinitData.c
char*
NuSMVCore_get_tool_name(
)
- The Sm tool_name field getter
- See Also
NuSMVCore_set_tool_name
- Defined in
cinitData.c
char*
NuSMVCore_get_tool_rc_file_name(
)
- The Sm tool rc file name field getter
- See Also
NuSMVCore_set_tool_name
- Defined in
cinitData.c
char*
NuSMVCore_get_tool_version(
)
- The Sm tool_version field getter
- See Also
NuSMVCore_set_tool_version
- Defined in
cinitData.c
char*
NuSMVCore_get_website(
)
- The Sm website field getter
- See Also
NuSMVCore_set_website
- Defined in
cinitData.c
void
NuSMVCore_init_cmd_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
- Defined in
cinitData.c
void
NuSMVCore_init_data(
)
- 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
- Defined in
cinitData.c
void
NuSMVCore_init(
,
int num_funs
)
- 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_V funs[
- See Also
NuSMVCore_set_reset_first_fun
NuSMVCore_set_reset_last_fun
- Defined in
cinitData.c
boolean
NuSMVCore_main(
int argc,
char ** argv,
int* status
)
- Executes the main program.
- See Also
NuSMVCore_init
NuSMVCore_quit
- Defined in
cinitData.c
void
NuSMVCore_quit(
)
- 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
- Defined in
cinitData.c
void
NuSMVCore_reset(
)
- 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)
- See Also
NuSMVCore_set_reset_first_fun
NuSMVCore_set_reset_last_fun
- Defined in
cinitData.c
void
NuSMVCore_set_bug_report_message(
char* bug_report_message
)
- The Sm bug_report_message field setter
- See Also
NuSMVCore_get_bug_report_message
- Defined in
cinitData.c
void
NuSMVCore_set_build_date(
char* build_date
)
- The Sm build_date field setter
- See Also
NuSMVCore_get_build_date
- Defined in
cinitData.c
void
NuSMVCore_set_email(
char* email
)
- The Sm email field setter
- See Also
NuSMVCore_get_email
- Defined in
cinitData.c
void
NuSMVCore_set_linked_addons(
char* linked_addons
)
- The Sm linked_addons field setter
- See Also
NuSMVCore_get_linked_addons
- Defined in
cinitData.c
void
NuSMVCore_set_prompt_string(
char* prompt_string
)
- The Sm prompt_string field setter
- See Also
NuSMVCore_get_prompt_string
- Defined in
cinitData.c
void
NuSMVCore_set_tool_name(
char* tool_name
)
- The Sm tool_name field setter
- See Also
NuSMVCore_get_tool_name
- Defined in
cinitData.c
void
NuSMVCore_set_tool_version(
char* tool_version
)
- The Sm tool_version field setter
- See Also
NuSMVCore_get_tool_version
- Defined in
cinitData.c
void
NuSMVCore_set_website(
char* website
)
- The Sm website field setter
- See Also
NuSMVCore_get_website
- Defined in
cinitData.c
void
cinitBatchMain(
)
- The batch main. It first read the input file, than
flatten the hierarchy. Aftre this preliminar phase it creates the
boolean variables necessary for the encoding and then start
compiling the read model into BDD. Now computes the reachable states
depending if the flag has been set. before starting verifying if the
properties specified in the model hold or not it computes the
fairness constraints. You can also activate the reordering and
also choose to avoid the verification of the properties.
- Defined in
cinitMisc.c
void
cinit_banner_print(
FILE* file,
boolean is_linked
)
- Prints the banner of NuSMV. If is_linked is true,
also the NuSMV library banner is output
- Defined in
cinitVers.c
static boolean
core_data_set_fs(
OptsHandler_ptr opt,
char* val
)
- Check and apply function for the -f cmd line opt
- Defined in
cinitData.c
static char*
get_executable_name(
const char* command
)
- Given a command, returns the executable file name (with
extension if required)
- Side Effects If not already specified, extension suffix is appended
to the returned string. Returned string must be freed.
- Defined in
cinitInit.c
char*
get_preprocessor_call(
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
- Defined in
cinitInit.c
char*
get_preprocessor_filename(
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
- Defined in
cinitInit.c
char*
get_preprocessor_names(
)
- Gets the names of the avaliable pre-processors. Returned
string must be freed
- Defined in
cinitInit.c
int
get_preprocessors_num(
)
- Returns the number of available proprocessors
- Defined in
cinitInit.c
static void
init_preprocessors(
)
- Initializes information about the pre-processors avaliable.
- Defined in
cinitInit.c
static boolean
nusmv_core_check_rbc_fun(
OptsHandler_ptr opt,
char* val
)
- Check and apply function for the -rbc cmd line opt
- Defined in
cinitData.c
static boolean
nusmv_core_check_sin_fun(
OptsHandler_ptr opt,
char* val
)
- Check and apply function for the -sin cmd line opt
- Defined in
cinitData.c
static void
nusmv_core_deinit_opt(
CmdLineOpt_ptr opt
)
- Deinitializes and frees the internal representation
structure of a command line option
- See Also
nusmv_core_init_opt
- Defined in
cinitData.c
static void
nusmv_core_deinit(
)
- Deinitializes and frees the internal variable
core_data. This function should be called
only when terminating the program
- See Also
nusmv_core_get_instance
- Defined in
cinitData.c
static void
nusmv_core_free_line_options(
CoreData_ptr core_data
)
- Frees the line_options hash and all it's contents
- Defined in
cinitData.c
static CoreData_ptr
nusmv_core_get_instance(
)
- Initializes (once) the internal core_data variable
- See Also
nusmv_core_deinit
- Defined in
cinitData.c
static int
nusmv_core_get_next_word_length(
char* string
)
- Aux function for the nusmv_core_split function
- See Also
nusmv_core_split
- Defined in
cinitData.c
static CmdLineOpt_ptr
nusmv_core_init_opt(
)
- Initializes the internal representation structure
of a command line option
- See Also
nusmv_core_deinit_opt
- Defined in
cinitData.c
static char*
nusmv_core_merge(
Olist_ptr set
)
- Given a set of unique strings, returns a string
representing the set of strings, separated by a
white space
- See Also
nusmv_core_split
- Defined in
cinitData.c
static Olist_ptr
nusmv_core_olist_intersection(
Olist_ptr a,
Olist_ptr b
)
- Calculates the intersection list between a and b.
The returned list must be freed by the caller
- Defined in
cinitData.c
static void
nusmv_core_olist_union(
Olist_ptr a,
Olist_ptr b
)
- Adds all elements in b to a, if a does
not contain it already
- Defined in
cinitData.c
static int
nusmv_core_parse_line_options(
int argc,
char ** argv
)
- Parses the given command line options.
-h, -help and input-file are hardcoded options,
all other options should be registered using
NuSMVCore_add_env_command_line_option or
NuSMVCore_add_command_line_option
- See Also
NuSMVCore_add_env_command_line_option
NuSMVCore_add_command_line_option
- Defined in
cinitData.c
static void
nusmv_core_print_string(
FILE* out,
char* str,
int padding
)
- Prints the given string on the given stream, padded by
the given number. If the given string is longer
than MAX_PRINT_WIDTH, then a new-line is added
and the remaining part of the string is prinded
(padded as the previous one). The string is
divided in such way that no words are
truncated.
- Defined in
cinitData.c
static void
nusmv_core_print_usage(
boolean print_banner
)
- Prints the command line option usages.
If print_banner is true, also the banner is
printed out. Printed command line options are
taken from the list of registered ones.
- See Also
NuSMVCore_add_command_line_option
NuSMVCore_add_env_command_line_option
- Defined in
cinitData.c
static boolean
nusmv_core_set_cpp(
OptsHandler_ptr opt,
char* val
)
- Check and apply function for the -cpp cmd line opt
- Defined in
cinitData.c
static boolean
nusmv_core_set_dp(
OptsHandler_ptr opt,
char* val
)
- Check and apply function for the -dp cmd line opt
- Defined in
cinitData.c
static boolean
nusmv_core_set_iwls95_partition(
OptsHandler_ptr opt,
char* val
)
- Check and apply function for the -iwls95 cmd line opt
- Defined in
cinitData.c
static boolean
nusmv_core_set_mono_partition(
OptsHandler_ptr opt,
char* val
)
- Check and apply function for the -mono cmd line opt
- Defined in
cinitData.c
static boolean
nusmv_core_set_pre(
OptsHandler_ptr opt,
char* val
)
- Check and apply function for the -pre cmd line opt
- Defined in
cinitData.c
static boolean
nusmv_core_set_thresh_partition(
OptsHandler_ptr opt,
char* val
)
- Check and apply function for the -thresh cmd line opt
- Defined in
cinitData.c
static Olist_ptr
nusmv_core_split(
char* string
)
- Given a string of white-space separated strings,
splits the string and builds a set of unique strings
- See Also
nusmv_core_merge
- Defined in
cinitData.c
static char*
nusmv_core_tolower(
char* str
)
- Lowercases a string
- See Also
nusmv_core_merge
- Defined in
cinitData.c
void
print_usage(
FILE * file
)
- Prints on
nusmv_stdout
usage
statistics, i.e. the amount of memory used, the amount of time
spent, the number of BDD nodes allocated and the size of the model
in BDD.
- See Also
compilePrintBddModelStatistic
- Defined in
cinitMisc.c
static void
quit_preprocessors(
)
- Removes information regarding the avaliable pre-processors.
- Defined in
cinitInit.c
void
restore_nusmv_stderr(
)
-
- Defined in
cinitMisc.c
void
restore_nusmv_stdout(
)
-
- Defined in
cinitMisc.c
(
)
- 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
- Defined in
cinitData.c
(
)
- The Sm banner_print_fun field setter
- See Also
NuSMVCore_get_banner_print_fun
- Defined in
cinitData.c
(
)
- The Sm batch fun field setter
- See Also
NuSMVCore_get_batch_fun
- Defined in
cinitData.c