static void
BannerPrint(
FILE * file
)
- Prints the banner of NuSMV.
- Defined in
smMain.c
int
CommandCmdReset(
int argc,
char ** argv
)
- Implements the reset command.
- Defined in
smCmd.c
int
CommandPrintUsage(
int argc,
char ** argv
)
- Implements the print_usage command.
- Side Effects required
- Defined in
smCmd.c
static char *
DateReadFromDateString(
char * datestr
)
- optional
- Defined in
smVers.c
static int
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
smMain.c
void
Sm_End(
)
- Calls the end routines of all the packages.
- Side Effects Closes the output files if not the standard ones.
- See Also
Sm_Init
- Defined in
smInit.c
void
Sm_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
smInit.c
int
Sm_NuSMVEndPrintMore(
)
- This function is called to terminate piping
stdout through "more". It is important to call Sm_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
Sm_NuSMVInitPrintMore
- Defined in
smVers.c
void
Sm_NuSMVInitPrintMore(
)
- This function is called to initialize piping
stdout through "more". It is important to call Sm_NuSMVEndPrintMore before
returning from your function and after
calling Sm_NuSMVInitPrintMore (preferably at the end of your printing;
failing to do so will cause the stdin lines not to appear).
- See Also
Sm_NuSMVEndPrintMore
- Defined in
smVers.c
char*
Sm_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
Sm_NuSMVReadVersion
- Defined in
smVers.c
char*
Sm_NuSMVReadVersion(
)
- Returns a static string giving the NuSMV version and compilation
timestamp. The user should not free this string.
- See Also
Sm_NuSMVObtainLibrary
- Defined in
smVers.c
void
Sm_Reset(
)
- Shuts down and restarts the system
- Defined in
smInit.c
static void
UsagePrint(
char * program,
char * unknown_option
)
- Prints the usage of the NuSMV shell interface.
- See Also
optional
- Defined in
smMain.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
smInit.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
smInit.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
smInit.c
char*
get_preprocessor_names(
)
- Gets the names of the avaliable pre-processors. Returned
string must be freed
- Defined in
smInit.c
int
get_preprocessors_num(
)
- Returns the number of available proprocessors
- Defined in
smInit.c
static void
init_preprocessors(
)
- Initializes information about the pre-processors avaliable.
- Defined in
smInit.c
int
main(
int argc,
char ** argv
)
- optional
- Side Effects required
- See Also
optional
- Defined in
smMain.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
smMisc.c
static void
quit_preprocessors(
)
- Removes information regarding the avaliable pre-processors.
- Defined in
smInit.c
void
restore_nusmv_stderr(
)
-
- Defined in
smMisc.c
void
restore_nusmv_stdout(
)
-
- Defined in
smMisc.c
void
smBatchMain(
)
- 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
smMisc.c
void
sm_ParseLineOptions(
int argc,
char ** argv,
options_ptr options
)
- Parses the command line options.
- Defined in
smMain.c