-
Be2bexpDfsData_head()
- Be2bexpDfsData_head
-
Be2bexpDfsData_pop()
- Be2bexpDfsData_pop
-
Be2bexpDfsData_push()
- Sets a node into the stack
-
Be2bexp_Back()
- Be2bexp_Back
-
Be2bexp_First()
- Be2bexpFirst
-
Be2bexp_Last()
- Be2bexp_Last
-
Be2bexp_Set()
- Be2bexpSet
-
BmcInt_Tableau_GetAtTime()
- Given a wff expressed in ltl builds the model-independent
tableau at 'time' of a path formula bounded by [k, l]
-
BmcSatTrace_create()
- Class BmcSatTrace constructor
-
BmcSatTrace_destroy()
- Class BmcSatTrace destructor
-
BmcSatTrace_get_symbolic_model()
- Returns the bdd-based symbolic model
-
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
-
UsageBmcCheckInvarInc()
- Usage string for command check_invar_bmc_inc
-
UsageBmcCheckInvar()
- Usage string for command check_invar_bmc
-
UsageBmcCheckLtlSpecInc()
- Usage string for command check_ltlspec_bmc_inc
-
UsageBmcCheckLtlSpecOnePb()
- Usage string for command check_ltlspec_bmc_onepb
-
UsageBmcCheckLtlSpec()
- Usage string for command check_ltlspec_bmc
-
UsageBmcGenInvar()
- Usage string for command gen_invar_bmc
-
UsageBmcGenLtlSpecOnePb()
- Usage string for command gen_ltlspec_bmc_onepb
-
UsageBmcGenLtlSpec()
- Usage string for command gen_ltlspec_bmc
-
UsageBmcSetup()
- Usage string for Bmc_CommandBmcSetup
-
UsageBmcSimulate()
- Usage string for UsageBmcSimulate
-
UsageBmcTestTableau()
- Usage string for Bmc_TestTableau
-
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
-
evaluateOn()
- Evaluates (either disjunctively or conjunctively) a PLTL
formula over an interval of time.
-
getTableauAtTime()
- Builds the tableau for a PLTL formula "pltl_wff" at time
"time".
-
isPureFuture()
- Checks wether a formula contains only future operators
-
projectOntoMainDomain()
- Projects a (possibly open) interval [a,b
-
tau()
- Gives an upper bound on the past temporal horizon of a
PLTL formula.
-
()
-
-
()
-
-
()
- Builds a tableau for the LTL at length k with loopback l
(single loop, no loop and all loopbacks are allowed)
Last updated on 2009/03/04 12h:51