void
Bmc_AddCmd(
)
- Adds all bmc-related commands to the interactive shell
- See Also
Sm_Init
node_ptr
Bmc_CheckFairnessListForPropositionalFormulae(
node_ptr wffList
)
- 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
- See Also
bmc_check_wff_list
int
Bmc_CommandBmcIncSimulate(
int argc,
char** argv
)
- Bmc_CommandBmcIncSimulate does incremental
simulation of the model starting from an initial state.
- Side Effects None
int
Bmc_CommandBmcPickState(
int argc,
char ** argv
)
- Picks a state from the set of initial states
- Side Effects The state chosen is stored in the traces_hash table as
the first state of a new trace
int
Bmc_CommandBmcSetup(
int argc,
char** argv
)
- Initializes the bmc sub-system, and builds the model in
a Boolean Expression format
- Side Effects Overall the bmc system
int
Bmc_CommandBmcSimulateCheckFeasibleConstraints(
int argc,
char ** argv
)
- Checks feasibility of a list of constraints for the
simulation
- Side Effects None
int
Bmc_CommandBmcSimulate(
int argc,
char** argv
)
- Bmc_CommandBmcSimulate does not require a specification
to build the problem, because only the model is used to build it.
- Side Effects None
int
Bmc_CommandCheckInvarBmcInc(
int argc,
char** argv
)
- The function is compiled only if there is at least
one incremental SAT solver
- Side Effects Property database may change
- See Also
Bmc_CommandCheckInvarBmc
int
Bmc_CommandCheckInvarBmc(
int argc,
char** argv
)
- After command line processing calls Bmc_GenSolveInvar
to solve and eventually dump the generated invariant problem. If you specify
the -o "filename" option a dimacs file will be generated, otherwise
no dimacs dump will be performed
- Side Effects Property database may change
- See Also
Bmc_GenSolveInvar
int
Bmc_CommandCheckLtlSpecBmcInc(
int argc,
char** argv
)
- Parameters are the maximum length and the loopback
values. The function is compiled only if there is at least
one incremental SAT solver
- Side Effects Properties database may change
- See Also
Bmc_CommandCheckLtlSpecBmcOnePb
Bmc_CommandCheckLtlSpecBmc
int
Bmc_CommandCheckLtlSpecBmcOnePb(
int argc,
char** argv
)
- After command line processing this function calls
the Bmc_GenSolveLtl which generates and solve the singleton
problem with bound k and loopback l.
- Side Effects Property database may change
- See Also
Bmc_CommandCheckLtlSpecBmc
Bmc_GenSolveLtl
int
Bmc_CommandCheckLtlSpecBmc(
int argc,
char** argv
)
- After command line processing this function calls
the Bmc_GenSolveLtl to generate and solve all problems from 0 to k.
Parameters are the maximum length and the loopback values.
- Side Effects Properties database may change
- See Also
Bmc_CommandCheckLtlSpecBmcOnePb
Bmc_GenSolveLtl
int
Bmc_CommandGenInvarBmc(
int argc,
char** argv
)
- After command line processing calls Bmc_GenSolveInvar
to dump the generated invariant problem.
If you specify the -o "filename" option a dimacs file named
"filename" will be created, otherwise the environment variable
bmc_invar_dimacs_filename value will be considered.
- Side Effects Property database may change
- See Also
Bmc_GenSolveInvar
int
Bmc_CommandGenLtlSpecBmcOnePb(
int argc,
char** argv
)
- After command line processing it calls
the function Bmc_GenSolveLtl to generate and dump the single problem.
- Side Effects Property database may change
- See Also
Bmc_CommandGenLtlSpecBmc
Bmc_GenSolveLtl
int
Bmc_CommandGenLtlSpecBmc(
int argc,
char** argv
)
- Each problem is dumped for the given LTL specification,
or for all LTL specifications if no formula is given.
Generation parameters are the maximum bound and the loopback values.
After command line processing it calls the function Bmc_GenSolveLtl
to generate and dump all problems from zero to k.
- Side Effects Property database may change
- See Also
Bmc_CommandGenLtlSpecBmcOnePb
Bmc_GenSolveLtl
node_ptr
Bmc_Conv_Be2Bexp(
BeEnc_ptr be_enc,
be_ptr be
)
- Descends the structure of the BE with dag-level
primitives. Uses the be encoding to perform all time-related operations.
be_ptr
Bmc_Conv_Bexp2Be(
BeEnc_ptr be_enc,
node_ptr bexp
)
- Uses the be encoding to perform all
time-related operations.
- Side Effects be hash may change
node_ptr
Bmc_Conv_BexpList2BeList(
BeEnc_ptr be_enc,
node_ptr bexp_list
)
- Converts given boolean expressions list
into correspondent reduced boolean circuits list
- Side Effects be hash may change
void
Bmc_Conv_cleanup_cached_entries_about(
BeEnc_ptr be_enc,
NodeList_ptr symbs
)
- Called by the BeEnc when removing a layer, to make safe
later declaration of symbols with the same name but different
semantics.
void
Bmc_Conv_get_BeModel2SymbModel(
const BeEnc_ptr be_enc,
const Slist_ptr be_model,
int k,
boolean convert_to_scalars,
node_ptr* frozen,
array_t** states,
array_t** inputs
)
- be_model is the model which will be transformed, i.e llList of
BE literal.
k is the number of steps (i.e. times+1) in the model.
The returned results will be provided in:
*frozen will point to expression over frozen variables,
*states will point to an array of size k+1 to expressions over state vars.
*inputs will point to an array of size k+1 to expressions over input vars.
In arrays every index corresponds to the corresponding time,
beginning from 0 for initial state.
Every expressions is a list with AND used as connection and Nil at
the end, i.e. it can be used as a list and as an expression.
Every element of the list can have form:
1) "var" or "!var" (if parameter convert_to_scalars is false)
2) "var=const" (if parameter convert_to_scalar is true).
By default BE literals are converted to bits of symbolic
variables. With parameter convert_to_scalars set up the bits are
converted to actual symbolic variables and scalar/word/etc
values. Note however that if BE model does not provide a value for
particular BE index then the corresponding bit may not be presented
in the result expressions or may be given some random value
(sometimes with convert_to_scalars set up). Note that in both cases
the returned assignments may be incomplete.
It is the responsibility of the invoker to free all arrays and the
lists of expressions (i.e. run free_list on *frozen and every
element of arrays returned). EQUAL nodes (when convert_to_scalars
is set up) are created with find_nodes, i.e. no freeing is need.
No caching or other side-effect are applied
void
Bmc_Conv_init_cache(
)
- This package function is called by bmcPkg module
void
Bmc_Conv_quit_cache(
)
- This package function is called by bmcPkg module
int
Bmc_GenSolveInvarDual(
Prop_ptr invarprop,
const int max_k,
bmc_invar_closure_strategy strategy
)
- The function tries to solve the problem
with not more then max_k transitions. If the problem is not
solved after max_k transition then the function returns 0.
If the no_closure flag is true, only the "base" encoding is used
int
Bmc_GenSolveInvarFalsification(
Prop_ptr invarprop,
const int max_k
)
- The function tries to solve the problem
with not more then max_k transitions. If the problem is not
solved after max_k transition then the function returns 0.
int
Bmc_GenSolveInvarZigzag(
Prop_ptr invarprop,
const int max_k
)
- The function will run not more then max_k transitions,
then if the problem is not proved the function just returns 0
int
Bmc_GenSolveLtlInc(
Prop_ptr ltlprop,
const int k,
const int relative_loop,
const boolean must_inc_length
)
- Solves LTL problem the same way as the original
Bmc_GenSolveLtl but just adds BE representing the path incrementaly.
- See Also
Bmc_GenSolve_Action
be_ptr
Bmc_Gen_InvarBaseStep(
const BeFsm_ptr be_fsm,
const node_ptr wff
)
- Returns I0 -> P0, where I0 is the init and
invar at time 0, and P0 is the given formula at time 0
- See Also
Bmc_Gen_InvarInductStep
be_ptr
Bmc_Gen_InvarInductStep(
const BeFsm_ptr be_fsm,
const node_ptr wff
)
- Returns (P0 and R01) -> P1, where P0 is the formula
at time 0, R01 is the transition (without init) from time 0 to 1,
and P1 is the formula at time 1
- See Also
Bmc_Gen_InvarBaseStep
be_ptr
Bmc_Gen_InvarProblem(
const BeFsm_ptr be_fsm,
const node_ptr wff
)
- Builds the negation of
(I0 imp P0) and ((P0 and R01) imp P1)
that must be unsatisfiable.
- See Also
Bmc_Gen_InvarBaseStep
Bmc_Gen_InvarInductStep
be_ptr
Bmc_Gen_LtlProblem(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k,
const int l
)
- Returns the LTL problem at length k with loopback l
(single loop, no loop and all loopbacks are allowed)
be_ptr
Bmc_GetTestTableau(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
const int k,
const int l
)
-
void
Bmc_Init(
)
- It builds the vars manager, initializes the package and
all sub packages, but only if not previously called.
boolean
Bmc_IsPropositionalFormula(
node_ptr wff
)
- Given a wff returns 1 if wff is a propositional formula,
zero (0) otherwise.
be_ptr
Bmc_Model_GetFairness(
const BeFsm_ptr be_fsm,
const int k,
const int l
)
- Uses bmc_model_getFairness_aux which recursively calls
itself to conjuctive all fairnesses by constructing a top-level 'and'
operation.
Moreover bmc_model_getFairness_aux calls the recursive function
bmc_model_getSingleFairness, which resolves a single fairness as
a disjunctioned expression in which each ORed element is a shifting of
the single fairness across [l, k] if a loop exists.
If no loop exists, nothing can be issued, so a falsity value is returned
- See Also
bmc_model_getFairness_aux
bmc_model_getSingleFairness
be_ptr
Bmc_Model_GetInit0(
const BeFsm_ptr be_fsm
)
- Use this function instead of explicitly get the init
from the fsm and shift them at time 0 using the vars manager layer.
- See Also
Bmc_Model_GetInvarAtTime
be_ptr
Bmc_Model_GetInitI(
const BeFsm_ptr be_fsm,
const int i
)
- Use this function instead of explicitly get the init
from the fsm and shift them at time i using the vars manager layer.
- See Also
Bmc_Model_GetInvarAtTime
be_ptr
Bmc_Model_GetInvarAtTime(
const BeFsm_ptr be_fsm,
const int time
)
- Use this function instead of explicitly get the invar
from the fsm and shift them at the requested time using the vars
manager layer.
- See Also
Bmc_Model_GetInit0
be_ptr
Bmc_Model_GetPathNoInit(
const BeFsm_ptr be_fsm,
const int k
)
- Returns the path for the model from 0 to k,
taking into account the invariants (and no init)
- See Also
Bmc_Model_GetPathWithInit
be_ptr
Bmc_Model_GetPathWithInit(
const BeFsm_ptr be_fsm,
const int k
)
- Returns the path for the model from 0 to k,
taking into account initial conditions and invariants
- See Also
Bmc_Model_GetPathNoInit
be_ptr
Bmc_Model_GetTransAtTime(
const BeFsm_ptr be_fsm,
const int time
)
- Use this function instead of explicitly get the trans
from the fsm and shift it at the requested
time using the vars manager layer
- Side Effects None
be_ptr
Bmc_Model_GetUnrolling(
const BeFsm_ptr be_fsm,
const int j,
const int k
)
- Using of invars over next variables instead of the
previuos variables is a specific implementation aspect
- See Also
Bmc_Model_GetPathWithInit
Bmc_Model_GetPathNoInit
be_ptr
Bmc_Model_Invar_Dual_forward_unrolling(
const BeFsm_ptr be_fsm,
const be_ptr invarspec,
int i
)
- Using of invars over previous variables instead of the
next variables is a specific implementation aspect
void
Bmc_Quit(
)
- Frees all resources allocated for the BMC model manager
int
Bmc_Simulate(
const BeFsm_ptr be_fsm,
BddEnc_ptr bdd_enc,
const int k,
const boolean print_trace,
const boolean changes_only
)
- Generate a problem with no property, and search for a
solution, appending it to the current simulation trace.
Returns 1 if solver could not be created, 0 if everything went smooth
- Side Effects None
int
Bmc_StepWiseSimulation(
BeFsm_ptr be_fsm,
BddEnc_ptr bdd_enc,
TraceManager_ptr trace_manager,
int target_steps,
be_ptr constraints,
boolean verbose,
boolean enable_defines
)
- This function performs incremental sat based
simulation up to target_steps.
Simulation starts from an initial state internally selected.
It accepts a constraint to direct the simulation to paths satisfying
such constraints. The constraints is assumed to be over state, input
and next state variables. Thus, please carefully consider this
information while providing constraints to this routine.
The simulation stops if either the target_steps steps of
simulation have been performed, or the simulation bumped in a
deadlock (that might be due to the constraints that are too strong).
Parameters:
'enable_defines' make the trace create/compute
defines in the trace (additionally to variables).
- Side Effects The possibly partial generated simulaiton trace
is added to the trace manager for possible reuse.
- See Also
optional
be_ptr
Bmc_TableauLTL_GetAllLoopsDepth1(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k
)
- Builds the tableau in the case depth==1 as suggested
by R. Sebastiani
be_ptr
Bmc_TableauLTL_GetAllLoops(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k,
const int l
)
- Each tableau takes into account of fairnesses relative
to its step. All tableau are collected together into a disjunctive form.
be_ptr
Bmc_TableauLTL_GetNoLoop(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k
)
- Fairness evaluate to true if there are not fairness
in the model, otherwise them evaluate to false because of no loop
be_ptr
Bmc_TableauLTL_GetSingleLoopWithFairness(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k,
const int l
)
- Builds the tableau at time zero. Loop is allowed,
fairness are taken into account
- See Also
BmcInt_Tableau_GetAtTime
be_ptr
Bmc_TableauLTL_GetSingleLoop(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k,
const int l
)
- Builds the tableau at time zero. Loop is allowed,
fairness are taken into account
- See Also
BmcInt_Tableau_GetAtTime
be_ptr
Bmc_TableauPLTL_GetAllLoopsDepth1(
const BeFsm_ptr be_fsm,
const node_ptr pltl_wff,
const int k
)
- Builds the tableau in the case depth==1 as suggested
by R. Sebastiani.
be_ptr
Bmc_TableauPLTL_GetAllLoops(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k,
const int startFromL
)
- 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.
be_ptr
Bmc_TableauPLTL_GetAllTimeTableau(
const BeEnc_ptr be_enc,
const node_ptr pltl_wff,
const int k
)
- This function is a special case of "evaluateOn", thus it
computes its answer by calling "evaluateOn" with some specifc
arguments. The only use of this function is in constructing
optimized tableaux for those depth-one formulas where
"RELEASES" is the unique operator.
- See Also
evaluateOn
be_ptr
Bmc_TableauPLTL_GetNoLoop(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k
)
- Returns the tableau for a PLTL formula on a bounded path
of length k, reasoning on fairness conditions as well.
be_ptr
Bmc_TableauPLTL_GetSingleLoop(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k,
const int l
)
- 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.
be_ptr
Bmc_TableauPLTL_GetTableau(
const BeEnc_ptr be_enc,
const node_ptr pltl_wff,
const int k,
const int l
)
- Builds both the bounded-tableau and the loop-tableau for a PLTL
formula "pltl_wff" (depending on the value of l). The time
the tableau refers to is (implicitly) time zero.
- See Also
getTableauAtTime
be_ptr
Bmc_Tableau_GetAllLoopsDepth1(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k
)
- Builds the tableau in the case depth==1 as suggested
by R. Sebastiani
be_ptr
Bmc_Tableau_GetAllLoopsDisjunction(
const BeEnc_ptr be_enc,
const int k
)
- Builds a formula which is a disjunction over all the
loop conditions on k-loops, with l=0,1,...,k-1.
- See Also
Bmc_Tableau_GetLoopCondition
be_ptr
Bmc_Tableau_GetAllLoops(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k,
const int l
)
- Each tableau takes into account of fairnesses relative
to its step. All tableau are collected together into a disjunctive form.
be_ptr
Bmc_Tableau_GetLoopCondition(
const BeEnc_ptr be_enc,
const int k,
const int l
)
- State l and state k are forced to represent the same
state by conjuncting the if-and-only-if conditions
{Vil<->Vik} between Vil (variable i at time l) and Vik
(variable i at time k) for each state variable Vi.
Note:frozen vars do not participate in this conjunct,
since they are implicitly keep their valus over all states
- See Also
Bmc_Tableau_GetAllLoopsDisjunction
be_ptr
Bmc_Tableau_GetLtlTableau(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k,
const int l
)
- Builds a tableau for the LTL at length k with loopback l
(single loop, no loop and all loopbacks are allowed)
be_ptr
Bmc_Tableau_GetNoLoop(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k
)
- Fairness evaluate to true if there are not fairness
in the model, otherwise them evaluate to false because of no loop
be_ptr
Bmc_Tableau_GetSingleLoop(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k,
const int l
)
- Builds the tableau in the case depth==1 as suggested
by R. Sebastiani
void
Bmc_TestReset(
)
- Call this function to reset the test sub-package (into
the reset command for example)
int
Bmc_TestTableau(
int argc,
char ** argv
)
- If you call this command with a loopback set to
BMC_ALL_LOOPS you command execution is aborted.
outcome
Bmc_Utils_Check_k_l(
const int k,
const int l
)
- Returns SUCCESS if k and l are compatible, otherwise
return GENERIC_ERROR
void
Bmc_Utils_ConvertLoopFromInteger(
const int iLoopback,
char* szLoopback,
const int _bufsize
)
- Inverse semantic of
Bmc_Utils_ConvertLoopFromString. bufsize is the maximum
buffer size
- Side Effects String buffer passed as argument will change
- See Also
Bmc_Utils_ConvertLoopFromString
int
Bmc_Utils_ConvertLoopFromString(
const char* strValue,
outcome* result
)
- Use this function to correctly convert a string
containing a loopback user-side value to the internal
representation of the same loopback value
- Side Effects result will change if supplied
void
Bmc_Utils_ExpandMacrosInFilename(
const char* filename_to_be_expanded,
const SubstString* table_ptr,
const size_t table_len,
char* filename_expanded,
size_t buf_len
)
- This function is used in order to perform the macro
expansion of filenames. table_ptr is the pointer to a
previously prepared table which fixes any
corrispondence from symbol to strings to be
substituited from. table_len is the number of rows in
the table (i.e. the number of symbols to search for.)
- Side Effects filename_expanded string data will change
const char*
Bmc_Utils_GetAllLoopbacksString(
)
- Returns a constant string which represents the "all loops"
semantic.
int
Bmc_Utils_GetAllLoopbacks(
)
- Returns the integer value which represents the "all loops"
semantic
int
Bmc_Utils_GetNoLoopback(
)
- Returns the integer value which represents the "no loop"
semantic
int
Bmc_Utils_GetSuccTime(
const int time,
const int k,
const int l
)
- 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
boolean
Bmc_Utils_IsAllLoopbacksString(
const char* str
)
- This is supplied in order to hide the internal value of
loopback which corresponds to the "all loops"
semantic.
boolean
Bmc_Utils_IsAllLoopbacks(
const int l
)
- This is supplied in order to hide the internal value of
loopback which corresponds to the "all loops"
semantic.
boolean
Bmc_Utils_IsNoLoopbackString(
const char* str
)
- This is supplied in order to hide the internal value of
loopback which corresponds to the "no loop" semantic.
boolean
Bmc_Utils_IsNoLoopback(
const int l
)
- This is supplied in order to hide the internal value of
loopback which corresponds to the "no loop" semantic.
boolean
Bmc_Utils_IsSingleLoopback(
const int l
)
- Both cases "no loop" and "all loops" make this function
returning false, since these values are not single
loops.
int
Bmc_Utils_RelLoop2AbsLoop(
const int upov_loop,
const int k
)
- For example the -4 value when k is 10 is the value 6,
but the value 4 (absolute loop value) is still 4
be_ptr
Bmc_Utils_apply_inlining4inc(
Be_Manager_ptr be_mgr,
be_ptr f
)
- Applies inlining forcing inclusion of the conjunct
set. Useful in the incremental SAT applications to
guarantee soundness
be_ptr
Bmc_Utils_apply_inlining(
Be_Manager_ptr be_mgr,
be_ptr f
)
- Applies inlining taking into account of current user
settings
Trace_ptr
Bmc_Utils_generate_and_print_cntexample(
BeEnc_ptr be_enc,
SatSolver_ptr solver,
BddEnc_ptr bdd_enc,
be_ptr be_prob,
const int k,
const char* trace_name,
NodeList_ptr symbols
)
- A trace is generated and printed using the currently
selected plugin. Generated trace is returned, in order
to make possible for the caller to do some other
operation, like association with the checked
property. Returned trace object *cannot* be destroyed
by the caller.
Trace_ptr
Bmc_Utils_generate_cntexample(
BeEnc_ptr be_enc,
SatSolver_ptr solver,
BddEnc_ptr bdd_enc,
be_ptr be_prob,
const int k,
const char* trace_name,
NodeList_ptr symbols
)
- Generated trace is returned, in order to make possible
for the caller to do some other operation, like
association with the checked property. Returned trace
object *cannot* be destroyed by the caller.
lsList
Bmc_Utils_get_vars_list_for_uniqueness_fsm(
BeEnc_ptr be_enc,
SexpFsm_ptr bool_sexp_fsm
)
- If coi is enabled, than the returned list will contain
only those boolean state variable the given property
actually depends on. Otherwise the full set of state
boolean vars will occur in the list. Frozen variables
are not required, since they do not change from state
to state, thus, cannot make a state distinguishable
from other states.
Returned list must be destroyed by the called.
lsList
Bmc_Utils_get_vars_list_for_uniqueness(
BeEnc_ptr be_enc,
Prop_ptr invarprop
)
- If coi is enabled, than the returned list will contain
only those boolean state variable the given property
actually depends on. Otherwise the full set of state
boolean vars will occur in the list. Frozen variables
are not required, since they do not change from state
to state, thus, cannot make a state distinguishable
from other states.
Returned list must be destroyed by the called.
be_ptr
Bmc_Utils_next_costraint_from_string(
BeEnc_ptr be_enc,
BddEnc_ptr bdd_enc,
const char* str,
Expr_ptr* node_expr
)
- Reads a next expression and builds the corresponding BE
formula. Exceptions are raised if the expression cannot
be parsed or has type errors. If node_expr is not NULL,
it will be set to the parsed expression.
- Side Effects None
- See Also
Bmc_Utils_simple_costraint_from_string
be_ptr
Bmc_Utils_simple_costraint_from_string(
BeEnc_ptr be_enc,
BddEnc_ptr bdd_enc,
const char* str,
Expr_ptr* node_expr
)
- Reads a simple expression and builds the corresponding
BE formula. Exceptions are raised if the expression
cannot be parsed or has type errors.
- Side Effects None
- See Also
Bmc_Utils_next_costraint_from_string
int
Bmc_WffListMatchProperty(
node_ptr wffList,
BMC_PF_MATCH pCheck,
void* pCheckOptArgument,
int iMaxMatches,
unsigned int* aiMatchedIndexes,
BMC_PF_MATCH_ANSWER pAnswer,
void* pAnswerOptArgument
)
- This is a generic searching function for a property
across a list of wffs. Please note that searching is specific for a list
of wffs, but the searching semantic and behaviour are generic and
customizable.
Searching may be stopped after the Nth match, or can be continued till all
list elements have been checked (specify -1 in this case).
In any case searching cannot be carried out over the MAX_MATCHES
value.
Arguments:
Parameter name | Description |
wffList | A list of wffs to iterate in |
pCheck | Pointer to matching function.
The checking function type is BMC_PF_MATCH, and has three
parameters:
wff the formula to check for
index index of wff into list
pOpt generic pointer to custom structure (optional) |
pCheckOptArgument | Argument passed to pCheck
(specify NULL if you do not use it.) |
iMaxMatches | Maximum number of matching to be
found before return. This must be less of MAX_MATCHES.
Specify -1 to iterate across the entire list. |
aiMatchedIndexes | Optional int array which
will contain all match indexes.
Specify NULL if you do not need this functionality.
Array size must be less of MAX_MATCHES. |
pAnswer | Pointer to answer function
of type BMC_PF_MATCH_ANSWER. This function is called everytime
a match is found.
Specify NULL if you do not need for this functionality.
The answer function has the following prototype:
void answer(node_ptr wff, int index, void* pOpt)
where:
wff the formula that matches the criteria
index is the index of wff into the list
pOpt pointer to generic & customizable structure
(see pAnswerOptArgument below)
pAnswerOptArgument optional parameter for pAnswer function,
in order to ensure more flexibility. Specify NULL if you do not need
for this functionality.) |
- Side Effects Given aiMatchedIndexes array changes if at least one
match has found out
int
Bmc_Wff_GetDepth(
node_ptr ltl_wff
)
- Returns 0 for propositional formulae, 1 or more for
temporal formulae
- Side Effects none
node_ptr
Bmc_Wff_MkAnd(
node_ptr arg1,
node_ptr arg2
)
- Makes an and WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkEventually(
node_ptr arg
)
- Makes an eventually WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkFalsity(
)
- Makes a false WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkGlobally(
node_ptr arg
)
- Makes a globally WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkHistorically(
node_ptr arg
)
- Makes a historically WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkIff(
node_ptr arg1,
node_ptr arg2
)
- Makes an iff WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkImplies(
node_ptr arg1,
node_ptr arg2
)
- Makes an implies WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkNext(
node_ptr arg
)
- Makes a next WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkNnf(
node_ptr wff
)
- A positive (1) polarity will not negate entire formula
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkNot(
node_ptr arg
)
- Makes a not WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkOnce(
node_ptr arg
)
- Makes an once WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkOpNext(
node_ptr arg
)
- Makes an op_next WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkOpNotPrecNot(
node_ptr arg
)
- Makes an op_next WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkOpPrec(
node_ptr arg
)
- Makes an op_next WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkOr(
node_ptr arg1,
node_ptr arg2
)
- Makes an or WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkReleases(
node_ptr arg1,
node_ptr arg2
)
- Makes a releases WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkSince(
node_ptr arg1,
node_ptr arg2
)
- Makes an since WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkTriggered(
node_ptr arg1,
node_ptr arg2
)
- Makes a triggered WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkTruth(
)
- Makes a truth WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkUntil(
node_ptr arg1,
node_ptr arg2
)
- Makes an until WFF
- Side Effects node hash may change
node_ptr
Bmc_Wff_MkXopNext(
node_ptr arg,
int x
)
- Applies op_next x times
- Side Effects node hash may change
int
Bmc_check_if_model_was_built(
FILE* err,
boolean forced
)
- If coi is not enabled than bmc must be set up,
otherwise it is only required bmc to have initialized. Returns 1 if
the execution should be stopped, and prints an error message if it
is the case (to the given optional file). If everything is fine,
returns 0 and prints nothing. If 'forced' is true, than the model is
required to be built even if coi is enabled, and a message is
printed accordingly (used by the commands that always require that
the model is built (e.g. bmc_simulate).
int
Bmc_check_psl_property(
Prop_ptr prop,
boolean dump_prob,
boolean inc_sat,
boolean single_prob,
int k,
int rel_loop
)
- The parameters are:
- prop is the PSL property to be checked
- dump_prob is true if the problem must be dumped as DIMACS file (default filename
from system corresponding variable)
- inc_sat is true if incremental sat must be used. If there is no
support for inc sat, an internal error will occur.
- single_prob is true if k must be not incremented from 0 to k_max
(single problem)
- k and rel_loop are the bmc parameters.
- Side Effects None
outcome
Bmc_cmd_options_handling(
int argc,
char** argv,
Prop_Type prop_type,
Prop_ptr* res_prop,
int* res_k,
int* res_l,
char** res_a,
char** res_s,
char** res_o
)
- Output variables called res_* are pointers to
variables that will be changed if the user specified a value for the
corresponding option. For example if the user specified "-k 2", then
*res_k will be assigned to 2. The caller can selectively choose which
options can be specified by the user, by passing either a valid pointer
as output parameter, or NULL to disable the corresponding option.
For example by passing NULL as actual parameter of res_l, option -l will
be not accepted.
If both specified, k and l will be checked for mutual consistency.
Loop will contain a relative value, like the one the user specified.
prop_type is the expected property type, if specified.
All integers values will not be changed if the corresponding options
had not be specified by the user, so the caller might assign them to
default values before calling this function.
All strings will be allocated by the function if the corresponding
options had been used by the user. In this case it is responsability
of the caller to free them. Strings will be assigned to NULL if the
user had not specified any corresponding option.
Returns GENERIC_ERROR if an error has occurred;
Returns SUCCESS_REQUIRED_HELP if -h options had been specified;
Returns SUCCESS in all other cases.
- Side Effects Result parameters might change
Trace_ptr
Bmc_create_trace_from_cnf_model(
const BeEnc_ptr be_enc,
const NodeList_ptr symbols,
const char* desc,
const TraceType type,
const Slist_ptr cnf_model,
int k
)
- Creates a complete, k steps long trace in the language
of "symbols" out a cnf model from a sat solver.
- Side Effects none
- See Also
Trace_create
Mc_create_trace_from_bdd_input_list
int
Bmc_pick_state_from_constr(
BeFsm_ptr fsm,
BddEnc_ptr bdd_enc,
be_ptr constr
)
- The trace is added into the trace manager.
Returns the index of the added trace, or -1 if
no trace was created.
- Side Effects A new trace possibly created into the trace manager
void
Bmc_rewrite_cleanup(
Prop_ptr rewritten_prop,
const BddEnc_ptr bdd_enc,
SymbLayer_ptr layer
)
- Crean up the memory after the rewritten property check
Prop_ptr
Bmc_rewrite_invar(
const Prop_ptr prop,
const BddEnc_ptr bdd_enc,
SymbLayer_ptr layer
)
- Returns a rewrited property
Olist_ptr
Bmc_simulate_check_feasible_constraints(
BeFsm_ptr be_fsm,
BddEnc_ptr bdd_enc,
Olist_ptr constraints,
be_ptr from_state
)
- Given a list of constraints (next-expressions as be_ptr),
checks which (flattened) constraints are
satisfiable from a given state. Iff
from_state is NULL (and not TRUE), the
initial state of the fsm is
considered. Returned list contains values in
{0,1}, and has to be freed.
- Side Effects None
inline static void
bmc_add_be_into_solver_positively(
SatSolver_ptr solver,
SatSolverGroup group,
be_ptr prob,
BeEnc_ptr be_enc
)
- Outputs into nusmv_stdout the total time
of conversion, adding, setting polarity and destroying BE.
inline static Be_Cnf_ptr
bmc_add_be_into_solver(
SatSolver_ptr solver,
SatSolverGroup group,
be_ptr prob,
int polarity,
BeEnc_ptr be_enc
)
- Outputs into nusmv_stdout the total time
of conversion and adding BE to solver. It is resposibility of the invoker
to destroy returned CNF (with Be_Cnf_Delete)
- Side Effects creates an instance of CNF formula. (do not forget to
delete it)
void
bmc_add_valid_wff_to_list(
node_ptr wff,
int index,
void* _pList
)
- private service for
Bmc_CheckFairnessListForPropositionalFormulae
- See Also
Bmc_CheckFairnessListForPropositionalFormulae
void
bmc_build_master_be_fsm(
)
- Creates the BE fsm from the Sexpr FSM. Currently the be
enc is a singleton global private variable which is shared between
all the BE FSMs. If not previoulsy committed (because a boolean
encoder was not available at the time due to the use of coi) the
determinization layer will be committed to the be encoder
be_ptr
bmc_build_uniqueness(
const BeFsm_ptr be_fsm,
const lsList state_vars,
const int init_state,
const int last_state
)
- Builds the uniqueness contraint for dual and zigzag
algorithms
int
bmc_check_if_wff_is_valid(
node_ptr wff,
int index,
void* _aiIndexes
)
- private service for
Bmc_CheckFairnessListForPropositionalFormulae
- See Also
Bmc_CheckFairnessListForPropositionalFormulae
be_ptr
bmc_conv_bexp2be_recur(
BeEnc_ptr be_enc,
node_ptr bexp
)
- Recursive service for Bmc_Conv_Bexp2Be, with caching of
results
- See Also
Bmc_Conv_Bexp2Be
be_ptr
bmc_conv_query_cache(
node_ptr bexp
)
- Return NULL if association not found
void
bmc_conv_set_cache(
node_ptr bexp,
be_ptr be
)
- Update the bexpr -> be cache
int
bmc_is_propositional_formula_aux(
node_ptr wff,
int index,
void* pOpt
)
- Wrapper that makes
Bmc_CheckFairnessListForPropositionalFormulae able to call
Bmc_IsPropositionalFormula with a mode generic interface.
Arguments 2 and 3 are practically unused, supplied to respect the generic
interface only.
- See Also
Bmc_CheckFairnessListForPropositionalFormulae
void
bmc_simulate_add_be_into_inc_solver_positively(
SatIncSolver_ptr solver,
SatSolverGroup group,
be_ptr prob,
BeEnc_ptr be_enc
)
- Outputs into nusmv_stdout the total time of conversion,
adding, setting polarity and destroying BE.
void
bmc_simulate_add_be_into_non_inc_solver_positively(
SatSolver_ptr solver,
be_ptr prob,
BeEnc_ptr be_enc
)
- Outputs into nusmv_stdout the total time of conversion,
adding, setting polarity and destroying BE.
void
bmc_simulate_set_curr_sim_trace(
Trace_ptr trace,
int idx
)
- Internal function used during the simulation to set the
current simulation trace
be_ptr
bmc_tableauGetEventuallyAtTime(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
const int intime,
const int k,
const int l
)
- ltl_wff is the 'p' part in 'F p'.
If intime<=k is out of [l, k] or if there is no loop,
iterates from intime to k, otherwise iterates from l to k
be_ptr
bmc_tableauGetGloballyAtTime(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
const int intime,
const int k,
const int l
)
- ltl_wff is the 'p' part in 'G p'
- See Also
bmc_tableauGetEventuallyAtTime
be_ptr
bmc_tableauGetNextAtTime(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
const int time,
const int k,
const int l
)
- Returns a falsity constants if the next operator leads
out of [l, k] and there is no loop
be_ptr
bmc_tableauGetReleasesAtTime_aux(
const BeEnc_ptr be_enc,
const node_ptr p,
const node_ptr q,
const int time,
const int k,
const int l,
const int steps
)
- Builds the release operator expression
be_ptr
bmc_tableauGetReleasesAtTime(
const BeEnc_ptr be_enc,
const node_ptr p,
const node_ptr q,
const int time,
const int k,
const int l
)
- Carries out the steps number to be performed, depending
on l,k and time, then calls bmc_tableauGetReleasesAtTime_aux
- See Also
bmc_tableauGetReleasesAtTime_aux
be_ptr
bmc_tableauGetUntilAtTime_aux(
const BeEnc_ptr be_enc,
const node_ptr p,
const node_ptr q,
const int time,
const int k,
const int l,
const int steps
)
- auxiliary part of bmc_tableauGetUntilAtTime
be_ptr
bmc_tableauGetUntilAtTime(
const BeEnc_ptr be_enc,
const node_ptr p,
const node_ptr q,
const int time,
const int k,
const int l
)
- Carries out the steps number to be performed, depending
on l,k and time, then calls bmc_tableauGetUntilAtTime_aux
- See Also
bmc_tableauGetUntilAtTime_aux
void
bmc_test_bexpr_output(
const BeEnc_ptr be_enc,
FILE* f,
const node_ptr bexp,
const int output_type
)
- 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
- Side Effects None
node_ptr
bmc_test_gen_tableau(
const BeFsm_ptr be_fsm,
const node_ptr ltl_nnf_wff,
const int k,
const int l,
boolean usePastOperators
)
- This function is used to test tableau formulae
node_ptr
bmc_test_gen_wff(
const BeEnc_ptr be_enc,
int max_depth,
int max_conns,
boolean usePastOperators
)
- Builds a random LTL WFF with specified
max depth and max connectives.
- Side Effects node hash may change
node_ptr
bmc_test_mk_loopback_ltl(
const BeEnc_ptr be_enc,
const int k,
const int l
)
- In the following example we suppose the loop starts
from 2 and finishes to 6 (the bound).
,-----------.
V |
o--o--o--o--o--o--o--o--o--o--o--o--o- (...continues indefinitely)
0 1 2 3 4 5 6 7 8 9 10 11 12
In general all state variables in time 2 must be forced to be equivalent
to the corresponding variables timed in 6, the variables in 3 to 7,
and so on up to the variables in 6 (equivalent to variables in
10). Then variables in 7 (or 3 again) must be forced to be equivalent
to the varaibles in 11, and so on indefinitely.
In formula (let suppose we have only one boolean variable):
(p2 <-> p6) && (p6 <-> p10) ...
In a more compact (and finite!) form, related to this example:
XX(G (p <-> XXXX(p)))
The first two neXtes force the formula to be effective only from the loop
starting point.
The generic formula implemented in the code is the following one:
X^(l) (G ((p0 <-> X^(k-l)(p0)) &&
(p1 <-> X^(k-l)(p1)) &&
.
.
.
(pn <-> X^(k-l)(pn)))
)
where:
p0..pn are all boolean variables into the model
X^(n) is expanded to XXX..X n-times.
Note that frozen vars can be ignored since they are always equal to their previous
values
void
bmc_trace_utils_append_input_state(
Trace_ptr trace,
BeEnc_ptr be_enc,
const Slist_ptr cnf_model
)
- This is a private service of BmcStepWise_Simulation
void
bmc_trace_utils_complete_trace(
Trace_ptr trace,
const BoolEnc_ptr bool_enc
)
- Populates trace with valid defaults assignments.
The trace can be safely considered complete when this
function returns. Existing assignments will not be
affected.
- Side Effects Trace is populated with default values
be_ptr
bmc_utils_costraint_from_string(
BeEnc_ptr be_enc,
BddEnc_ptr bdd_enc,
const char* str,
boolean accept_next_expr,
Expr_ptr* node_expr
)
- Reads a either simple or next expression and builds the
corresponding BE formula. Exceptions are raised if the
expression cannot be parsed or has type
errors. Internal service.
- Side Effects None
node_ptr
bmc_wff_mkBinary(
int type,
node_ptr arg1,
node_ptr arg2
)
- Makes a binary WFF
- Side Effects node hash may change
node_ptr
bmc_wff_mkConst(
int type
)
- Makes a constant WFF
- Side Effects node hash may change
node_ptr
bmc_wff_mkUnary(
int type,
node_ptr arg
)
- Makes a unary WFF
- Side Effects node hash may change