-
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
-
bmcPkg.c
- Bmc.Pkg module
-
BmcSatTrace.c
- Contains the definition of class BmcSatTrace
-
bmcTableau.c
- Bmc.Tableau module
-
bmcTableauLTLformula.c
- Bmc.Tableau module
-
bmcTableauPLTLformula.c
- Bmc.TableauPLTL module
-
bmcTest.c
- Test routines for bmc package
-
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_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.
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_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
-
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 and Lorenzo Delana
This implementation is still depedent on the rbc package
-
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_bexp2be_recur()
- Private service for Bmc_Conv_Bexp2Be
-
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_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
bmcDump.c
Dumping functionalities, like dimacs and others
By: Roberto Cavada
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
bmcInt.c
Private interfaces implementation of package bmc
By: Roberto Cavada
-
Bmc_GetTestTableau()
-
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_GetUnrolling()
- 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
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_AddCmd()
- Adds all bmc-related commands to the interactive shell
BmcSatTrace.c
Contains the definition of class BmcSatTrace
By: Roberto Cavada
See Alsothe
sat
package
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
-
()
- 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
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
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 SUCCESS if the conversion
has been successfully performed, otherwise to GENERIC_ERROR is the conversion
failed. If result is NULL, 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_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_apply_inlining()
- Applies inlining taking into account of current user
settings
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 2009/03/04 12h:51