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

Last updated on 2011/04/06 21h:13