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

void 
Sm_BannerPrint_cudd(
  FILE * file, 
  char* name 
)
Prints the banner of cudd.

Defined in smVers.c

void 
Sm_BannerPrint_minisat(
  FILE * file, 
  char* name 
)
Prints the banner of minisat.

Defined in smVers.c

void 
Sm_BannerPrint_nusmv_library(
  FILE * file, 
  char* name 
)
To be used by addons linking against the NuSMV library.

Defined in smVers.c

void 
Sm_BannerPrint_zchaff(
  FILE * file, 
  char* name 
)
Prints the banner of zchaff.

Defined in smVers.c

void 
Sm_BannerPrint(
  FILE * file 
)
Prints the banner of NuSMV.

Defined in smVers.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

int 
Sm_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 smMisc.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, 
  OptsHandler_ptr  options 
)
Parses the command line options.

Defined in smMain.c

Last updated on 2010/05/19 15h:56