-
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_CommandBmcIncSimulate()
- Bmc_CommandBmcIncSimulate does incremental
simulation of the model starting from an initial state.
-
Bmc_CommandBmcPickState()
- Picks a state from the set of initial states
-
Bmc_CommandBmcSetup()
- Initializes the bmc sub-system, and builds the model in
a Boolean Expression format
-
Bmc_CommandBmcSimulateCheckFeasibleConstraints()
- Checks feasibility of a list of constraints for the
simulation
-
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_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
-
Bmc_GenSolveInvarDual()
- Solve an INVARSPEC problems wiht algorithm Dual
-
Bmc_GenSolveInvarFalsification()
- Solve an INVARSPEC problems wiht algorithm Fasification
-
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_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_Quit()
- Frees all resources allocated for the BMC model manager
-
Bmc_Simulate()
- Performs simulation
-
Bmc_StepWiseSimulation()
- SAT Based Incremental simulation
-
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_GetLtlTableau()
- Builds a tableau for the LTL at length k with loopback l
(single loop, no loop and all loopbacks are allowed)
-
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_inlining4inc()
- Applies inlining forcing inclusion of the conjunct
set. Useful in the incremental SAT applications to
guarantee soundness
-
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_generate_cntexample()
- Given a problem, and a solver containing a model for that
problem, generates a counter-example
-
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_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_next_costraint_from_string()
- Reads a next expression and builds the corresponding BE
formula.
-
Bmc_Utils_simple_costraint_from_string()
- Reads a simple expression and builds the corresponding BE
formula.
-
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_cmd_options_handling()
- Bmc commands options handling for commands (optionally)
acceping options -k -l -o -a -n -p -P
-
Bmc_create_trace_from_cnf_model()
- Creates a trace out of a cnf model
-
Bmc_pick_state_from_constr()
- Picks a state from the initial state, creates a trace
from it.
-
Bmc_rewrite_cleanup()
- Crean up the memory after the rewritten property check
-
Bmc_rewrite_invar()
- Rewrites an invariant specification containing input
variables or next with an observer state variable
-
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_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_build_uniqueness()
- Builds the uniqueness contraint for dual and zigzag
algorithms
-
bmc_check_if_wff_is_valid()
- private service for
Bmc_CheckFairnessListForPropositionalFormulae
-
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_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_set_curr_sim_trace()
- Internal function used during the simulation to set the
current simulation trace
-
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_trace_utils_append_input_state()
- Appends a _complete_ (i,S') pair to existing trace
-
bmc_trace_utils_complete_trace()
- Populates trace with valid defaults assignments
-
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.
-
bmc_wff_mkBinary()
- Makes a binary WFF
-
bmc_wff_mkConst()
- Makes a constant WFF
-
bmc_wff_mkUnary()
- Makes a unary WFF
Last updated on 2011/04/06 21h:13