bmc.h
External header file
bmcInt.h
Internal header file
bmcBmcInc.c
High level functionalities layer for BMC (incremental) algorithms
bmcBmcNonInc.c
High level functionalities layer for non incremental sat solving
bmcCheck.c
Some useful functions to check propositional formulae. Temporary located into the bmc package
bmcCmd.c
Bmc.Cmd module
bmcConv.c
Convertion function of BE to corresponding BDD boolean expression, and viceversa
bmcDump.c
Dumping functionalities, like dimacs and others
bmcGen.c
Bmc.Gen module
bmcInt.c
Private interfaces implementation of package bmc
bmcModel.c
Bmc.Model module
bmcOpt.c
bmc Opt module
bmcPkg.c
Bmc.Pkg module
bmcSimulate.c
Incremental SAT Based simulation
bmcTableau.c
Bmc.Tableau module
bmcTableauLTLformula.c
Bmc.Tableau module
bmcTableauPLTLformula.c
Bmc.TableauPLTL module
bmcTest.c
Test routines for bmc package
bmcTrace.c
This module contains functions to build traces from BE models
bmcUtils.c
Utilities for the bmc package
bmcWff.c
Well Formed Formula manipulation routines

bmc.h

External header file

By: Roberto Cavada


bmcInt.h

Internal header file

By: Roberto Cavada


bmcBmcInc.c

High level functionalities layer for BMC (incremental) algorithms

By: Andrei Tchaltsev

User-commands directly use function defined in this module.

Bmc_GenSolveLtlInc()
Solves LTL problem the same way as the original Bmc_GenSolveLtl but just adds BE representing the path incrementaly.
Bmc_GenSolveInvarZigzag()
Solve an INVARSPEC problems with algorithm ZigZag
Bmc_GenSolveInvarDual()
Solve an INVARSPEC problems wiht algorithm Dual
Bmc_GenSolveInvarFalsification()
Solve an INVARSPEC problems wiht algorithm Fasification
bmc_add_be_into_solver()
Converts Be into CNF, and adds it into a group of a solver.
bmc_add_be_into_solver_positively()
Converts Be into CNF, and adds it into a group of a solver, sets polarity to 1, and then destroys the CNF.
bmc_build_uniqueness()
Builds the uniqueness contraint for dual and zigzag algorithms

bmcBmcNonInc.c

High level functionalities layer for non incremental sat solving

By: Roberto Cavada


bmcCheck.c

Some useful functions to check propositional formulae. Temporary located into the bmc package

By: Roberto Cavada

Bmc_CheckFairnessListForPropositionalFormulae()
Helper function to simplify calling to 'bmc_check_wff_list' for searching of propositional wff only. Returns a new list of wffs which contains legal wffs only
Bmc_WffListMatchProperty()
For each element belonging to a given list of wffs, calls the given matching function. If function matches, calls given answering function
Bmc_IsPropositionalFormula()
Given a wff returns 1 if wff is a propositional formula, zero (0) otherwise.
bmc_is_propositional_formula_aux()
Useful wrapper for Bmc_CheckFairnessListForPropositionalFormulae
bmc_check_if_wff_is_valid()
private service for Bmc_CheckFairnessListForPropositionalFormulae
bmc_add_valid_wff_to_list()
private service for Bmc_CheckFairnessListForPropositionalFormulae

bmcCmd.c

Bmc.Cmd module

By: Roberto Cavada

This module contains all the bmc commands implementation. Options parsing and checking is performed here, than the high-level Bmc layer is called

See AlsobmcPkg.c, bmcBmc.c

Bmc_CommandBmcSetup()
Initializes the bmc sub-system, and builds the model in a Boolean Expression format
UsageBmcSetup()
Usage string for Bmc_CommandBmcSetup
Bmc_CommandBmcSimulate()
Bmc_CommandBmcSimulate generates a trace of the problem represented from the simple path from 0 (zero) to k
UsageBmcSimulate()
Usage string for UsageBmcSimulate
Bmc_CommandBmcIncSimulate()
Bmc_CommandBmcIncSimulate does incremental simulation of the model starting from an initial state.
UsageBmcIncSimulate()
Usage string for UsageBmcIncSimulate
Bmc_CommandBmcPickState()
Picks a state from the set of initial states
UsageBmcPickState()
Usage string for UsageBmcPickState
Bmc_CommandBmcSimulateCheckFeasibleConstraints()
Checks feasibility of a list of constraints for the simulation
UsageBmcSimulateCheckFeasibleConstraints()
Usage string for UsageBmcSimulateCheckFeasibleConstraints
Bmc_CommandGenLtlSpecBmc()
Generates length_max+1 problems iterating the problem bound from zero to length_max, and dumps each problem to a dimacs file
UsageBmcGenLtlSpec()
Usage string for command gen_ltlspec_bmc
Bmc_CommandGenLtlSpecBmcOnePb()
Generates only one problem with fixed bound and loopback, and dumps the problem to a dimacs file. The single problem is dumped for the given LTL specification, or for all LTL specifications if no formula is given
UsageBmcGenLtlSpecOnePb()
Usage string for command gen_ltlspec_bmc_onepb
Bmc_CommandCheckLtlSpecBmc()
Checks the given LTL specification, or all LTL specifications in the properties database if no formula is given
UsageBmcCheckLtlSpec()
Usage string for command check_ltlspec_bmc
Bmc_CommandCheckLtlSpecBmcOnePb()
Checks the given LTL specification, or all LTL specifications if no formula is given. Checking parameters are the problem bound and the loopback values
UsageBmcCheckLtlSpecOnePb()
Usage string for command check_ltlspec_bmc_onepb
Bmc_CommandCheckLtlSpecBmcInc()
Checks the given LTL specification, or all LTL specifications in the properties database if no formula is given, using incremental algorithms
UsageBmcCheckLtlSpecInc()
Usage string for command check_ltlspec_bmc_inc
Bmc_CommandGenInvarBmc()
Generates and dumps the problem for the given invariant or for all invariants if no formula is given. SAT solver is not invoked.
UsageBmcGenInvar()
Usage string for command gen_invar_bmc
Bmc_CommandCheckInvarBmc()
Generates and solve the given invariant, or all invariants if no formula is given
UsageBmcCheckInvar()
Usage string for command check_invar_bmc
Bmc_CommandCheckInvarBmcInc()
Solve the given invariant, or all invariants if no formula is given, using incremental algorithms.
UsageBmcCheckInvarInc()
Usage string for command check_invar_bmc_inc
Bmc_check_psl_property()
Top-level function for bmc of PSL properties
Bmc_cmd_options_handling()
Bmc commands options handling for commands (optionally) acceping options -k -l -o -a -n -p -P -e
bmc_build_master_be_fsm()
Bmc_check_if_model_was_built()
A service for commands, to check if bmc has been built

bmcConv.c

Convertion function of BE to corresponding BDD boolean expression, and viceversa

By: Alessandro Cimatti, Lorenzo Delana, Michele Dorigatti

Bmc_Conv_Be2Bexp()
Given a be, constructs the corresponding boolean expression
Bmc_Conv_Bexp2Be()
Converts given boolean expression into correspondent reduced boolean circuit
Bmc_Conv_BexpList2BeList()
Converts given boolean expressions list into correspondent reduced boolean circuits list
Bmc_Conv_cleanup_cached_entries_about()
Removes from the cache those entries that depend on the given symbol
Bmc_Conv_get_BeModel2SymbModel()
This function converts a BE model (i.e. a list of BE literals) to symbolic expressions.
Bmc_Conv_init_cache()
Initializes module Conv
Bmc_Conv_quit_cache()
De-initializes module Conv
Be2bexpDfsData_push()
Sets a node into the stack
Be2bexpDfsData_head()
Be2bexpDfsData_head
Be2bexpDfsData_pop()
Be2bexpDfsData_pop
Be2bexp_Set()
Be2bexpSet
Be2bexp_First()
Be2bexpFirst
Be2bexp_Back()
Be2bexp_Back
Be2bexp_Last()
Be2bexp_Last
bmc_conv_set_cache()
Update the bexpr -> be cache
bmc_conv_query_cache()
Queries the bexpr->be cache
bmc_conv_bexp2be_recur()
Private service for Bmc_Conv_Bexp2Be

bmcDump.c

Dumping functionalities, like dimacs and others

By: Roberto Cavada, Marco Roveri

This module supplies services that dump a Bmc problem into a file, in DIMACS format and others


bmcGen.c

Bmc.Gen module

By: Roberto Cavada

This module contains all the problems generation functions

See AlsobmcBmc.c, bmcTableau.c, bmcModel.c

Bmc_Gen_InvarProblem()
Builds and returns the invariant problem of the given propositional formula
Bmc_Gen_LtlProblem()
Returns the LTL problem at length k with loopback l (single loop, no loop and all loopbacks are allowed)
Bmc_Gen_InvarBaseStep()
Returns the base step of the invariant construction
Bmc_Gen_InvarInductStep()
Returns the induction step of the invariant construction
Bmc_Gen_UnrollingFragment()
Generates i-th fragment of BMC unrolling

bmcInt.c

Private interfaces implementation of package bmc

By: Roberto Cavada

Bmc_GetTestTableau()
Bmc_rewrite_invar()
Rewrites an invariant specification containing input variables or next with an observer state variable
Bmc_rewrite_cleanup()
Crean up the memory after the rewritten property check

bmcModel.c

Bmc.Model module

By: Roberto Cavada

This module contains all the model-related operations

See AlsobmcGen.c, bmcTableau.c, bmcConv.c, bmcVarMgr.c

Bmc_Model_GetInit0()
Retrieves the init states from the given fsm, and compiles them into a BE at time 0
Bmc_Model_GetInitI()
Retrieves the init states from the given fsm, and compiles them into a BE at time i
Bmc_Model_GetInvarAtTime()
Retrieves the invars from the given fsm, and compiles them into a BE at the given time
Bmc_Model_GetTransAtTime()
Retrieves the trans from the given fsm, and compiles it into a MSatEnc at the given time
Bmc_Model_GetUnrolling()
Unrolls the transition relation from j to k, taking into account of invars
Bmc_Model_Invar_Dual_forward_unrolling()
Unrolls the transition relation from j to k, taking into account of invars
Bmc_Model_GetPathNoInit()
Returns the path for the model from 0 to k, taking into account the invariants (and no init)
Bmc_Model_GetPathWithInit()
Returns the path for the model from 0 to k, taking into account initial conditions and invariants
Bmc_Model_GetFairness()
Generates and returns an expression representing all fairnesses in a conjunctioned form

bmcOpt.c

bmc Opt module

By: Alessandro Mariotti

This module contains all the bmc options handling functions

opt_check_bmc_pb_length()
Check function for the bmc_pb_lenght option
opt_check_bmc_pb_loop()
Check function for the bmc_pb_loop option
opt_check_bmc_invar_alg()
Check function for the bmc_invar_alg option
opt_get_bmc_invar_alg()
Get function for the bmc_invar_alg function
opt_check_bmc_inc_invar_alg()
Check function for the bmc_inc_invar_alg function
opt_get_bmc_inc_invar_alg()
Get function for the bmc_inc_invar_alg function
opt_get_integer()
Get the integer representation of the given string
opt_get_string()
Get function for simple strings

bmcPkg.c

Bmc.Pkg module

By: Roberto Cavada

This module contains all the bmc package handling functions

Bmc_Init()
Initializes the BMC structure
Bmc_Quit()
Frees all resources allocated for the BMC model manager
Bmc_InitData()
Initializes the BMC internal structures, but not all dependencies. Call Bmc_Init to initialize everything it is is what you need instead.
Bmc_QuitData()
De0Initializes the BMC internal structures, but not all dependencies. Call Bmc_Quit to deinitialize everything it is is what you need instead.
Bmc_AddCmd()
Adds all bmc-related commands to the interactive shell

bmcSimulate.c

Incremental SAT Based simulation

By: Marco Roveri

Incremental SAT Based simulation

See Alsooptional

Bmc_Simulate()
Performs simulation
Bmc_StepWiseSimulation()
SAT Based Incremental simulation
Bmc_simulate_check_feasible_constraints()
Checks the truth value of a list of constraints on the current state, transitions and next states, from given starting state. This can be used in guided interactive simulation to propose the set of transitions which are allowed to occur in the interactive simulation.
Bmc_pick_state_from_constr()
Picks a state from the initial state, creates a trace from it.
bmc_simulate_set_curr_sim_trace()
Internal function used during the simulation to set the current simulation trace
bmc_simulate_add_be_into_inc_solver_positively()
Converts Be into CNF, and adds it into a group of a incremental solver, sets polarity to 1, and then destroys the CNF.
bmc_simulate_add_be_into_non_inc_solver_positively()
Converts Be into CNF, and adds it into a group of a non-incremental solver, sets polarity to 1, and then destroys the CNF.
bmc_simulate_enable_random_mode()
Enables random mode in the given sat solver

bmcTableau.c

Bmc.Tableau module

By: Marco Benedetti, Roberto Cavada

This module contains all the tableau-related operations

See AlsobmcModel.c, bmcConv.c, bmcVarMgr.c bmcTableau.c, bmcTableauLTLformula.c, bmcTableauPLTLformula.c, bmcGen.c

Bmc_Tableau_GetNoLoop()
Builds tableau without loop at time zero, taking into account of fairness
Bmc_Tableau_GetSingleLoop()
Builds tableau for all possible loops in [l, k], in the particular case in which depth is 1. This function takes into account of fairness
Bmc_Tableau_GetAllLoops()
Builds tableau for all possible loops in [l, k[, taking into account of fairness
Bmc_Tableau_GetAllLoopsDepth1()
Builds tableau for all possible loops in [l, k], in the particular case in which depth is 1. This function takes into account of fairness
Bmc_Tableau_GetLtlTableau()
Builds a tableau for the LTL at length k with loopback l (single loop, no loop and all loopbacks are allowed)
Bmc_TableauLTL_GetSingleLoopWithFairness()
Builds the tableau at time zero. Loop is allowed, fairness are taken into account
Bmc_TableauLTL_GetSingleLoop()
Builds the tableau at time zero. Loop is allowed, fairness are taken into account
Bmc_TableauLTL_GetNoLoop()
Builds tableau without loop at time zero, taking into account of fairness
Bmc_TableauLTL_GetAllLoops()
Builds tableau for all possible loops in [l, k[, taking into account of fairness
Bmc_TableauLTL_GetAllLoopsDepth1()
Builds tableau for all possible loops in [l, k], in the particular case in which depth is 1. This function takes into account of fairness
Bmc_TableauPLTL_GetNoLoop()
Returns the tableau for a PLTL formula on a bounded path of length k, reasoning on fairness conditions as well.
Bmc_TableauPLTL_GetSingleLoop()
Returns the tableau for a PLTL formula on a (k,l)-loop, conjuncted with both fairness conditions and the loop condition on time steps k and l.
Bmc_TableauPLTL_GetAllLoops()
Returns the conjunction of the single-loop tableaux for all possible (k,l)-loops for a fixed k. Each single-loop tableau takes into account of both fairness constraints and loop condition.
Bmc_TableauPLTL_GetAllLoopsDepth1()
Builds tableau for all possible (k,l)-loops for a fixed k, in the particular case depth==1. This function takes into account of fairness.
Bmc_Tableau_GetLoopCondition()
Builds a tableau that constraints state k to be equal to state l. This is the condition for a path of length (k+1) to represent a (k-l)loop (new semantics).
Bmc_Tableau_GetAllLoopsDisjunction()
Builds the disjunction of all the loops conditions for (k-l)-loops with l in [0, k[
isPureFuture()
Checks wether a formula contains only future operators
isPureFuture_aux()
Memoized private service of isPureFuture

bmcTableauLTLformula.c

Bmc.Tableau module

By: Roberto Cavada

This module contains all the operations related to the construction of tableaux for LTL formulas

See AlsobmcGen.c, bmcModel.c, bmcConv.c, bmcVarMgr.c

BmcInt_Tableau_GetAtTime()
Given a wff expressed in ltl builds the model-independent tableau at 'time' of a path formula bounded by [k, l]
bmc_tableauGetNextAtTime()
Resolves the NEXT operator, building the tableau for its argument
bmc_tableauGetEventuallyAtTime()
Resolves the future operator, and builds a conjunctive expression of tableaus, by iterating intime up to k in a different manner depending on the [l, k] interval form
bmc_tableauGetGloballyAtTime()
As bmc_tableauGetEventuallyAtTime, but builds a conjunctioned expression in order to be able to assure a global constraint
bmc_tableauGetUntilAtTime()
Builds an expression which evaluates the until operator
bmc_tableauGetReleasesAtTime()
Builds an expression which evaluates the release operator
bmc_tableauGetUntilAtTime_aux()
auxiliary part of bmc_tableauGetUntilAtTime
bmc_tableauGetReleasesAtTime_aux()
auxiliary part of bmc_tableauGetReleasesAtTime

bmcTableauPLTLformula.c

Bmc.TableauPLTL module

By: Marco Benedetti

Implements all the functions needed to build tableaux for PLTL formulas.

See AlsobmcTableau.c, bmcGen.c

()
()
Bmc_TableauPLTL_GetTableau()
Builds the tableau for a PLTL formula.
Bmc_TableauPLTL_GetAllTimeTableau()
Builds the conjunction of the tableaux for a PLTL formula computed on every time instant along a (k,l)-loop.
getTableauAtTime()
Builds the tableau for a PLTL formula "pltl_wff" at time "time".
evaluateOn()
Evaluates (either disjunctively or conjunctively) a PLTL formula over an interval of time.
projectOntoMainDomain()
Projects a (possibly open) interval [a,b
tau()
Gives an upper bound on the past temporal horizon of a PLTL formula.

bmcTest.c

Test routines for bmc package

By: Roberto Cavada, Marco Benedetti

Bmc_TestReset()
Call this function to reset the test sub-package (into the reset command for example)
Bmc_TestTableau()
The first time Bmc_TestTableau is called in the current session this function creates a smv file with a model and generates a random ltl spec to test tableau. The following times it is called it appends a new formula to the file.
UsageBmcTestTableau()
Usage string for Bmc_TestTableau
bmc_test_mk_loopback_ltl()
For each variable p in the set of state variables, generates the global equivalence of p and X^(loop length), starting from the loop start
bmc_test_gen_tableau()
Given a WFF in NNF, converts it into a tableau formula, then back to WFF_(k,l) and returns WFF -> WFF_(k,l)
bmc_test_gen_wff()
Builds a random LTL WFF with specified max depth and max connectives.
bmc_test_bexpr_output()
Write to specified FILE stream given node_ptr formula with specified output_type format. There are follow formats: BMC_BEXP_OUTPUT_SMV, BMC_BEXP_OUTPUT_LB

bmcTrace.c

This module contains functions to build traces from BE models

By: Marco Pensallorto

Bmc_create_trace_from_cnf_model()
Creates a trace out of a cnf model
Bmc_fill_trace_from_cnf_model()
Fills the given trace out of a cnf model
bmc_trace_utils_complete_trace()
Populates trace with valid defaults assignments
bmc_trace_utils_append_input_state()
Appends a _complete_ (i,S') pair to existing trace

bmcUtils.c

Utilities for the bmc package

By: Roberto Cavada

Bmc_Utils_ConvertLoopFromString()
Given a string representing a loopback possible value, returns the corresponding integer. The (optional) parameter result will be assigned to OUTCOME_SUCCESS if the conversion has been successfully performed, otherwise to OUTCOME_GENERIC_ERROR is the conversion failed. If result is NULL, OUTCOME_SUCCESS is the aspected value, and an assertion is implicitly performed to check the conversion outcome.
Bmc_Utils_ConvertLoopFromInteger()
Given an integer containing the inner representation of the loopback value, returns as parameter the corresponding user-side value as string
Bmc_Utils_IsNoLoopback()
Returns true if l has the internally encoded "no loop" value
Bmc_Utils_IsNoLoopbackString()
Returns true if the given string represents the no loopback value
Bmc_Utils_IsSingleLoopback()
Returns true if the given loop value represents a single (relative or absolute) loopback
Bmc_Utils_IsAllLoopbacks()
Returns true if the given loop value represents the "all possible loopbacks" semantic
Bmc_Utils_IsAllLoopbacksString()
Returns true if the given string represents the "all possible loops" value.
Bmc_Utils_GetNoLoopback()
Returns the integer value which represents the "no loop" semantic
Bmc_Utils_GetAllLoopbacks()
Returns the integer value which represents the "all loops" semantic
Bmc_Utils_GetAllLoopbacksString()
Returns a constant string which represents the "all loops" semantic.
Bmc_Utils_RelLoop2AbsLoop()
Converts a relative loop value (wich can also be an absolute loop value) to an absolute loop value
Bmc_Utils_Check_k_l()
Checks the (k,l) couple. l must be absolute.
Bmc_Utils_GetSuccTime()
Given time<=k and a [l, k] interval, returns next time, or BMC_NO_LOOP if time is equal to k and there is no loop
Bmc_Utils_ExpandMacrosInFilename()
Search into a given string any symbol which belongs to a determined set of symbols, and expand each found symbol, finally returning the resulting string
Bmc_Utils_generate_and_print_cntexample()
Given a problem, and a solver containing a model for that problem, generates and prints a counter-example
Bmc_Utils_generate_cntexample()
Given a problem, and a solver containing a model for that problem, generates a counter-example
Bmc_Utils_fill_cntexample()
Given a solver containing a model for a problem, fills the given counter-example correspondingly
Bmc_Utils_get_vars_list_for_uniqueness()
Creates a list of BE variables that are intended to be used by the routine that makes the state unique in invariant checking.
Bmc_Utils_get_vars_list_for_uniqueness_fsm()
Creates a list of BE variables that are intended to be used by the routine that makes the state unique in invariant checking.
Bmc_Utils_apply_inlining()
Applies inlining taking into account of current user settings
Bmc_Utils_apply_inlining4inc()
Applies inlining forcing inclusion of the conjunct set. Useful in the incremental SAT applications to guarantee soundness
Bmc_Utils_simple_costraint_from_string()
Reads a simple expression and builds the corresponding BE formula.
Bmc_Utils_next_costraint_from_string()
Reads a next expression and builds the corresponding BE formula.
bmc_utils_costraint_from_string()
Reads an expression and builds the corresponding BE formula. If accept_next_expr is true, then a next expression is parsed, otherwise a simple expression is parsed.

bmcWff.c

Well Formed Formula manipulation routines

By: Alessandro Cimatti and Lorenzo Delana

Bmc_Wff_MkTruth()
Makes a truth WFF
Bmc_Wff_MkFalsity()
Makes a false WFF
Bmc_Wff_MkNot()
Makes a not WFF
Bmc_Wff_MkAnd()
Makes an and WFF
Bmc_Wff_MkOr()
Makes an or WFF
Bmc_Wff_MkImplies()
Makes an implies WFF
Bmc_Wff_MkIff()
Makes an iff WFF
Bmc_Wff_MkNext()
Makes a next WFF
Bmc_Wff_MkXopNext()
Applies op_next x times
Bmc_Wff_MkOpNext()
Makes an op_next WFF
Bmc_Wff_MkOpPrec()
Makes an op_next WFF
Bmc_Wff_MkOpNotPrecNot()
Makes an op_next WFF
Bmc_Wff_MkGlobally()
Makes a globally WFF
Bmc_Wff_MkHistorically()
Makes a historically WFF
Bmc_Wff_MkEventually()
Makes an eventually WFF
Bmc_Wff_MkOnce()
Makes an once WFF
Bmc_Wff_MkUntil()
Makes an until WFF
Bmc_Wff_MkSince()
Makes an since WFF
Bmc_Wff_MkReleases()
Makes a releases WFF
Bmc_Wff_MkTriggered()
Makes a triggered WFF
Bmc_Wff_MkNnf()
Makes the negative normal form of given WFF
Bmc_Wff_GetDepth()
Returns the modal depth of the given formula
bmc_wff_mkBinary()
Makes a binary WFF
bmc_wff_mkUnary()
Makes a unary WFF
bmc_wff_mkConst()
Makes a constant WFF

Last updated on 2011/06/16 12h:15