Bmc_AddCmd()
Adds all bmc-related commands to the interactive shell
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_CommandBmcSetup()
Initializes the bmc sub-system, and builds the model in a Boolean Expression format
Bmc_CommandBmcSimulate()
Bmc_CommandBmcSimulate generates a trace of the problem represented from the simple path from 0 (zero) to k
Bmc_CommandCheckInvarBmcInc()
Solve the given invariant, or all invariants if no formula is given, using incremental algorithms.
Bmc_CommandCheckInvarBmc()
Generates and solve the given invariant, or all invariants if no formula is given
Bmc_CommandCheckLtlSpecBmcInc()
Checks the given LTL specification, or all LTL specifications in the properties database if no formula is given, using incremental algorithms
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
Bmc_CommandCheckLtlSpecBmc()
Checks the given LTL specification, or all LTL specifications in the properties database if no formula is given
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.
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
Bmc_CommandGenLtlSpecBmc()
Generates length_max+1 problems iterating the problem bound from zero to length_max, and dumps each problem to a dimacs file
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_init_cache()
Initializes module Conv
Bmc_Conv_quit_cache()
De-initializes module Conv
Bmc_GenSolveInvarDual()
Solve an INVARSPEC problems wiht algorithm Dual
Bmc_GenSolveInvarZigzag()
Solve an INVARSPEC problems with algorithm ZigZag
Bmc_GenSolveLtlInc()
Solves LTL problem the same way as the original Bmc_GenSolveLtl but just adds BE representing the path incrementaly.
Bmc_Gen_InvarBaseStep()
Returns the base step of the invariant construction
Bmc_Gen_InvarInductStep()
Returns the induction step of the invariant construction
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_GetTestTableau()
Bmc_Init()
Initializes the BMC structure
Bmc_IsPropositionalFormula()
Given a wff returns 1 if wff is a propositional formula, zero (0) otherwise.
Bmc_Model_GetFairness()
Generates and returns an expression representing all fairnesses in a conjunctioned form
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_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_GetUnrolling()
Unrolls the transition relation from j to k, taking into account of invars
Bmc_Quit()
Frees all resources allocated for the BMC model manager
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_TableauLTL_GetAllLoops()
Builds tableau for all possible loops in [l, k[, taking into account of fairness
Bmc_TableauLTL_GetNoLoop()
Builds tableau without loop at time zero, taking into account of fairness
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_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_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_GetAllTimeTableau()
Builds the conjunction of the tableaux for a PLTL formula computed on every time instant along a (k,l)-loop.
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_GetTableau()
Builds the tableau for a PLTL formula.
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_GetAllLoopsDisjunction()
Builds the disjunction of all the loops conditions for (k-l)-loops with l in [0, k[
Bmc_Tableau_GetAllLoops()
Builds tableau for all possible loops in [l, k[, taking 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_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_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.
Bmc_Utils_Check_k_l()
Checks the (k,l) couple. l must be absolute.
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_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_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_GetAllLoopbacksString()
Returns a constant string which represents the "all loops" semantic.
Bmc_Utils_GetAllLoopbacks()
Returns the integer value which represents the "all loops" semantic
Bmc_Utils_GetNoLoopback()
Returns the integer value which represents the "no loop" semantic
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_IsAllLoopbacksString()
Returns true if the given string represents the "all possible loops" value.
Bmc_Utils_IsAllLoopbacks()
Returns true if the given loop value represents the "all possible loopbacks" semantic
Bmc_Utils_IsNoLoopbackString()
Returns true if the given string represents the no loopback value
Bmc_Utils_IsNoLoopback()
Returns true if l has the internally encoded "no loop" value
Bmc_Utils_IsSingleLoopback()
Returns true if the given loop value represents a single (relative or absolute) loopback
Bmc_Utils_RelLoop2AbsLoop()
Converts a relative loop value (wich can also be an absolute loop value) to an absolute loop value
Bmc_Utils_apply_inlining()
Applies inlining taking into account of current user settings
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_WffListMatchProperty()
For each element belonging to a given list of wffs, calls the given matching function. If function matches, calls given answering function
Bmc_Wff_GetDepth()
Returns the modal depth of the given formula
Bmc_Wff_MkAnd()
Makes an and WFF
Bmc_Wff_MkEventually()
Makes an eventually WFF
Bmc_Wff_MkFalsity()
Makes a false WFF
Bmc_Wff_MkGlobally()
Makes a globally WFF
Bmc_Wff_MkHistorically()
Makes a historically WFF
Bmc_Wff_MkIff()
Makes an iff WFF
Bmc_Wff_MkImplies()
Makes an implies WFF
Bmc_Wff_MkNext()
Makes a next WFF
Bmc_Wff_MkNnf()
Makes the negative normal form of given WFF
Bmc_Wff_MkNot()
Makes a not WFF
Bmc_Wff_MkOnce()
Makes an once WFF
Bmc_Wff_MkOpNext()
Makes an op_next WFF
Bmc_Wff_MkOpNotPrecNot()
Makes an op_next WFF
Bmc_Wff_MkOpPrec()
Makes an op_next WFF
Bmc_Wff_MkOr()
Makes an or WFF
Bmc_Wff_MkReleases()
Makes a releases WFF
Bmc_Wff_MkSince()
Makes an since WFF
Bmc_Wff_MkTriggered()
Makes a triggered WFF
Bmc_Wff_MkTruth()
Makes a truth WFF
Bmc_Wff_MkUntil()
Makes an until WFF
Bmc_Wff_MkXopNext()
Applies op_next x times
Bmc_check_if_model_was_built()
A service for commands, to check if bmc has been built
Bmc_check_psl_property()
Top-level function for bmc of PSL properties
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_add_be_into_solver()
Converts Be into CNF, and adds it into a group of a solver.
bmc_add_valid_wff_to_list()
private service for Bmc_CheckFairnessListForPropositionalFormulae
bmc_build_master_be_fsm()
bmc_check_if_wff_is_valid()
private service for Bmc_CheckFairnessListForPropositionalFormulae
bmc_cmd_options_handling()
Bmc commands options handling for commands (optionally) acceping options -k -l -o -a -n -p
bmc_conv_bexp2be_recur()
Private service for Bmc_Conv_Bexp2Be
bmc_conv_query_cache()
Queries the bexpr->be cache
bmc_conv_set_cache()
Update the bexpr -> be cache
bmc_is_propositional_formula_aux()
Useful wrapper for Bmc_CheckFairnessListForPropositionalFormulae
bmc_sat_trace_calculateSymbModel()
Private service for class BmcSatTrace methods
bmc_sat_trace_clear_model()
Service function
bmc_sat_trace_prop2symb()
Private service for BmcSatTrace methods
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_tableauGetNextAtTime()
Resolves the NEXT operator, building the tableau for its argument
bmc_tableauGetReleasesAtTime_aux()
auxiliary part of bmc_tableauGetReleasesAtTime
bmc_tableauGetReleasesAtTime()
Builds an expression which evaluates the release operator
bmc_tableauGetUntilAtTime_aux()
auxiliary part of bmc_tableauGetUntilAtTime
bmc_tableauGetUntilAtTime()
Builds an expression which evaluates the until operator
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
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_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_wff_mkBinary()
Makes a binary WFF
bmc_wff_mkConst()
Makes a constant WFF
bmc_wff_mkUnary()
Makes a unary WFF

Last updated on 2009/01/30 15h:04