NuSMV/code/nusmv/core/bmc/bmcPkg.h File Reference

#include "nusmv/core/cinit/NuSMVEnv.h"

Go to the source code of this file.

Functions
int	Bmc_check_if_model_was_built (NuSMVEnv_ptr env, FILE *err, boolean forced)
	A service for commands, to check if bmc has been built.
void	Bmc_Init (NuSMVEnv_ptr env)
	Public interface for any package-related functionality.
void	Bmc_init_opt (NuSMVEnv_ptr env)
int	Bmc_Pkg_bmc_setup (NuSMVEnv_ptr env, boolean forced)
	Initialize the bmc package and optionally builds the be fsm and registers the trace executors.
void	Bmc_Pkg_build_master_be_fsm (const NuSMVEnv_ptr env)
	Creates the BE fsm from the Sexpr FSM. Currently the be enc is a singleton global private variable which is shared between all the BE FSMs. If not previoulsy committed (because a boolean encoder was not available at the time due to the use of coi) the determinization layer will be committed to the be encoder.
void	Bmc_Quit (NuSMVEnv_ptr env)
	Frees all resources allocated for the BMC model manager.
void	Bmc_QuitData (void)
	De0Initializes the BMC internal structures, but not all dependencies. Call Bmc_Quit to deinitialize everything it is is what you need instead.

---

Function Documentation

int Bmc_check_if_model_was_built	(	NuSMVEnv_ptr	env,
		FILE *	err,
		boolean	forced
	)

A service for commands, to check if bmc has been built.

If coi is not enabled than bmc must be set up, otherwise it is only required bmc to have initialized. Returns 1 if the execution should be stopped, and prints an error message if it is the case (to the given optional file). If everything is fine, returns 0 and prints nothing. If 'forced' is true, than the model is required to be built even if coi is enabled, and a message is printed accordingly (used by the commands that always require that the model is built (e.g. bmc_simulate).

void Bmc_Init

(

NuSMVEnv_ptr

env

)

Public interface for any package-related functionality.

Author:

Roberto Cavada

Todo:

: Missing description

AutomaticStart

Initializes the BMC structure It builds the vars manager, initializes the package and all sub packages, but only if not previously called.

void Bmc_init_opt

(

NuSMVEnv_ptr

env

)

Todo:

Missing synopsis

Todo:

Missing description

int Bmc_Pkg_bmc_setup	(	NuSMVEnv_ptr	env,
		boolean	forced
	)

Initialize the bmc package and optionally builds the be fsm and registers the trace executors.

void Bmc_Pkg_build_master_be_fsm

(

const NuSMVEnv_ptr

env

)

Creates the BE fsm from the Sexpr FSM. Currently the be enc is a singleton global private variable which is shared between all the BE FSMs. If not previoulsy committed (because a boolean encoder was not available at the time due to the use of coi) the determinization layer will be committed to the be encoder.

void Bmc_Quit

(

NuSMVEnv_ptr

env

)

Frees all resources allocated for the BMC model manager.

void Bmc_QuitData

(

void

)

De0Initializes the BMC internal structures, but not all dependencies. Call Bmc_Quit to deinitialize everything it is is what you need instead.