static node_ptr
Be2bexpDfsData_head(
Be2bexpDfsData* data
)
- Be2bexpDfsData_head
- Side Effects None
- Defined in
bmcConv.c
static node_ptr
Be2bexpDfsData_pop(
Be2bexpDfsData* data
)
- Be2bexpDfsData_pop
- Side Effects None
- Defined in
bmcConv.c
static void
Be2bexpDfsData_push(
Be2bexpDfsData* data,
node_ptr value
)
- Sets a node into the stack
- Side Effects None
- Defined in
bmcConv.c
static void
Be2bexp_Back(
be_ptr be,
char* Be2bexpData,
nusmv_ptrint sign
)
- Be2bexp_Back
- Side Effects None
- Defined in
bmcConv.c
static void
Be2bexp_First(
be_ptr be,
char* Be2bexpData,
nusmv_ptrint sign
)
- Be2bexpFirst
- Side Effects None
- Defined in
bmcConv.c
static void
Be2bexp_Last(
be_ptr be,
char* Be2bexpData,
nusmv_ptrint sign
)
- Be2bexp_Last
- Side Effects None
- Defined in
bmcConv.c
static int
Be2bexp_Set(
be_ptr be,
char* Be2bexpData,
nusmv_ptrint sign
)
- Be2bexpSet
- Side Effects None
- Defined in
bmcConv.c
be_ptr
BmcInt_Tableau_GetAtTime(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
const int time,
const int k,
const int l
)
- This function is the entry point of a mutual recursive
calling stack. All logical connectives are resolved, excepted for NOT, which
closes the recursive calling stack. Also variables and falsity/truth
constants close the recursion.
- See Also
bmc_tableauGetNextAtTime
bmc_tableauGetGloballyAtTime
bmc_tableauGetEventuallyAtTime
bmc_tableauGetUntilAtTime
bmc_tableauGetReleasesAtTime
- Defined in
bmcTableauLTLformula.c
BmcSatTrace_ptr
BmcSatTrace_create(
be_ptr beProb,
lsList beModel
)
- The method gets a satisfiable assignment of literals,
expressed in terms of be indices, and the original be problem which this
assignments had been calculated from.
- See Also
BmcSatTrace_destroy
- Defined in
bmcSatTrace.c
void
BmcSatTrace_destroy(
BmcSatTrace_ptr* self_ref
)
- Call when you no longer need the given instance
- Side Effects self will be invalidated
- Defined in
bmcSatTrace.c
NodeList_ptr
BmcSatTrace_get_symbolic_model(
const BmcSatTrace_ptr self,
const BeEnc_ptr be_enc,
const int k
)
- Returns the symbolic counterexample with max length k.
The BeEnc instance is required by the conversion routine.
Conversion is performed with memoizing, so you can call efficiently call
this method more than one time. Returned object belongs to self
- Side Effects self's internal state can change
- Defined in
bmcSatTrace.c
void
Bmc_AddCmd(
)
- Adds all bmc-related commands to the interactive shell
- See Also
Sm_Init
- Defined in
bmcPkg.c
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
- Defined in
bmcCheck.c
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
- Defined in
bmcCmd.c
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
- Defined in
bmcCmd.c
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
- Defined in
bmcCmd.c
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
- Defined in
bmcCmd.c
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
- Defined in
bmcCmd.c
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
- Defined in
bmcCmd.c
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
- Defined in
bmcCmd.c
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
- Defined in
bmcCmd.c
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
- Defined in
bmcCmd.c
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
- Defined in
bmcCmd.c
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.
- Defined in
bmcConv.c
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
- Defined in
bmcConv.c
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
- Defined in
bmcConv.c
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.
- Defined in
bmcConv.c
void
Bmc_Conv_init_cache(
)
- This package function is called by bmcPkg module
- Defined in
bmcConv.c
void
Bmc_Conv_quit_cache(
)
- This package function is called by bmcPkg module
- Defined in
bmcConv.c
int
Bmc_GenSolveInvarDual(
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.
- Defined in
bmcBmcInc.c
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
- Defined in
bmcBmcInc.c
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
- Defined in
bmcBmcInc.c
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
- Defined in
bmcGen.c
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
- Defined in
bmcGen.c
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
- Defined in
bmcGen.c
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)
- Defined in
bmcGen.c
be_ptr
Bmc_GetTestTableau(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
const int k,
const int l
)
-
- Defined in
bmcInt.c
void
Bmc_Init(
)
- It builds the vars manager, initializes the package and
all sub packages, but only if not previously called.
- Defined in
bmcPkg.c
boolean
Bmc_IsPropositionalFormula(
node_ptr wff
)
- Given a wff returns 1 if wff is a propositional formula,
zero (0) otherwise.
- Defined in
bmcCheck.c
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
- Defined in
bmcModel.c
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
- Defined in
bmcModel.c
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
- Defined in
bmcModel.c
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
- Defined in
bmcModel.c
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
- Defined in
bmcModel.c
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
- Defined in
bmcModel.c
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
- Defined in
bmcModel.c
void
Bmc_Quit(
)
- Frees all resources allocated for the BMC model manager
- Defined in
bmcPkg.c
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
- Defined in
bmcTableau.c
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.
- Defined in
bmcTableau.c
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
- Defined in
bmcTableau.c
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
- Defined in
bmcTableau.c
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
- Defined in
bmcTableau.c
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.
- Defined in
bmcTableau.c
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.
- Defined in
bmcTableau.c
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
- Defined in
bmcTableauPLTLformula.c
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.
- Defined in
bmcTableau.c
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.
- Defined in
bmcTableau.c
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
- Defined in
bmcTableauPLTLformula.c
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
- Defined in
bmcTableau.c
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
- Defined in
bmcTableau.c
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.
- Defined in
bmcTableau.c
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 variable Vi.
- See Also
Bmc_Tableau_GetAllLoopsDisjunction
- Defined in
bmcTableau.c
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
- Defined in
bmcTableau.c
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
- Defined in
bmcTableau.c
void
Bmc_TestReset(
)
- Call this function to reset the test sub-package (into
the reset command for example)
- Defined in
bmcTest.c
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.
- Defined in
bmcTest.c
outcome
Bmc_Utils_Check_k_l(
const int k,
const int l
)
- Returns SUCCESS if k and l are compatible, otherwise
return GENERIC_ERROR
- Defined in
bmcUtils.c
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
- Defined in
bmcUtils.c
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
- Defined in
bmcUtils.c
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
- Defined in
bmcUtils.c
const char*
Bmc_Utils_GetAllLoopbacksString(
)
- Returns a constant string which represents the
"all loops" semantic.
- Defined in
bmcUtils.c
int
Bmc_Utils_GetAllLoopbacks(
)
- Returns the integer value which represents the
"all loops" semantic
- Defined in
bmcUtils.c
int
Bmc_Utils_GetNoLoopback(
)
- Returns the integer value which represents the
"no loop" semantic
- Defined in
bmcUtils.c
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
- Defined in
bmcUtils.c
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.
- Defined in
bmcUtils.c
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.
- Defined in
bmcUtils.c
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.
- Defined in
bmcUtils.c
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.
- Defined in
bmcUtils.c
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.
- Defined in
bmcUtils.c
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
- Defined in
bmcUtils.c
be_ptr
Bmc_Utils_apply_inlining(
Be_Manager_ptr be_mgr,
be_ptr f
)
- Applies inlining taking into account of current user
settings
- Defined in
bmcUtils.c
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
)
- 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.
- Defined in
bmcUtils.c
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 given property actually depends on. Otherwise
the set of state boolean vars will occur in the list.
Returned list must be destroyed by the called.
- Defined in
bmcUtils.c
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
- Defined in
bmcCheck.c
int
Bmc_Wff_GetDepth(
node_ptr ltl_wff
)
- Returns 0 for propositional formulae, 1 or more for
temporal formulae
- Side Effects none
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkAnd(
node_ptr arg1,
node_ptr arg2
)
- Makes an and WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkEventually(
node_ptr arg
)
- Makes an eventually WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkFalsity(
)
- Makes a false WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkGlobally(
node_ptr arg
)
- Makes a globally WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkHistorically(
node_ptr arg
)
- Makes a historically WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkIff(
node_ptr arg1,
node_ptr arg2
)
- Makes an iff WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkImplies(
node_ptr arg1,
node_ptr arg2
)
- Makes an implies WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkNext(
node_ptr arg
)
- Makes a next WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkNnf(
node_ptr wff
)
- A positive (1) polarity will not negate entire formula
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkNot(
node_ptr arg
)
- Makes a not WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkOnce(
node_ptr arg
)
- Makes an once WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkOpNext(
node_ptr arg
)
- Makes an op_next WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkOpNotPrecNot(
node_ptr arg
)
- Makes an op_next WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkOpPrec(
node_ptr arg
)
- Makes an op_next WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkOr(
node_ptr arg1,
node_ptr arg2
)
- Makes an or WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkReleases(
node_ptr arg1,
node_ptr arg2
)
- Makes a releases WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkSince(
node_ptr arg1,
node_ptr arg2
)
- Makes an since WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkTriggered(
node_ptr arg1,
node_ptr arg2
)
- Makes a triggered WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkTruth(
)
- Makes a truth WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkUntil(
node_ptr arg1,
node_ptr arg2
)
- Makes an until WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
Bmc_Wff_MkXopNext(
node_ptr arg,
int x
)
- Applies op_next x times
- Side Effects node hash may change
- Defined in
bmcWff.c
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).
- Defined in
bmcCmd.c
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
- Defined in
bmcCmd.c
static int
UsageBmcCheckInvarInc(
)
- The function is compiled only if there is at least
one incremental SAT solver
- Side Effects None
- See Also
Bmc_CommandCheckInvarBmcInc
- Defined in
bmcCmd.c
static int
UsageBmcCheckInvar(
)
- Usage string for command check_invar_bmc
- Side Effects None
- See Also
Bmc_CommandCheckInvarBmc
- Defined in
bmcCmd.c
static int
UsageBmcCheckLtlSpecInc(
)
- The function is compiled only if there is at least
one incremental SAT solver.
- Side Effects None
- See Also
Bmc_CommandCheckLtlSpecBmc
- Defined in
bmcCmd.c
static int
UsageBmcCheckLtlSpecOnePb(
)
- Usage string for command check_ltlspec_bmc_onepb
- Side Effects None
- See Also
Bmc_CommandCheckLtlSpecBmcOnePb
- Defined in
bmcCmd.c
static int
UsageBmcCheckLtlSpec(
)
- Usage string for command check_ltlspec_bmc
- Side Effects None
- See Also
Bmc_CommandCheckLtlSpecBmc
- Defined in
bmcCmd.c
static int
UsageBmcGenInvar(
)
- Usage string for command gen_invar_bmc
- Side Effects None
- See Also
Bmc_CommandGenInvarBmc
- Defined in
bmcCmd.c
static int
UsageBmcGenLtlSpecOnePb(
)
- Usage string for command gen_ltlspec_bmc_onepb
- Side Effects None
- See Also
Bmc_CommandGenLtlSpecBmcOnePb
- Defined in
bmcCmd.c
static int
UsageBmcGenLtlSpec(
)
- Usage string for command gen_ltlspec_bmc
- Side Effects None
- See Also
Bmc_CommandGenLtlSpecBmc
- Defined in
bmcCmd.c
static int
UsageBmcSetup(
)
- Usage string for Bmc_CommandBmcSetup
- See Also
Bmc_CommandBmcSetup
- Defined in
bmcCmd.c
static int
UsageBmcSimulate(
)
- Usage string for UsageBmcSimulate
- Side Effects None
- See Also
Bmc_CommandBmcSimulate
- Defined in
bmcCmd.c
static int
UsageBmcTestTableau(
)
- Usage string for Bmc_TestTableau
- Side Effects None
- Defined in
bmcTest.c
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.
- Defined in
bmcBmcInc.c
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)
- Defined in
bmcBmcInc.c
void
bmc_add_valid_wff_to_list(
node_ptr wff,
int index,
void* _pList
)
- private service for
Bmc_CheckFairnessListForPropositionalFormulae
- See Also
Bmc_CheckFairnessListForPropositionalFormulae
- Defined in
bmcCheck.c
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
- Defined in
bmcCmd.c
int
bmc_check_if_wff_is_valid(
node_ptr wff,
int index,
void* _aiIndexes
)
- private service for
Bmc_CheckFairnessListForPropositionalFormulae
- See Also
Bmc_CheckFairnessListForPropositionalFormulae
- Defined in
bmcCheck.c
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_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
- Defined in
bmcCmd.c
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
- Defined in
bmcConv.c
be_ptr
bmc_conv_query_cache(
node_ptr bexp
)
- Return NULL if association not found
- Defined in
bmcConv.c
void
bmc_conv_set_cache(
node_ptr bexp,
be_ptr be
)
- Update the bexpr -> be cache
- Defined in
bmcConv.c
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
- Defined in
bmcCheck.c
void
bmc_sat_trace_calculateSymbModel(
const BmcSatTrace_ptr self,
const BeEnc_ptr be_enc,
const int k
)
- Private service for class BmcSatTrace methods
- Defined in
bmcSatTrace.c
void
bmc_sat_trace_clear_model(
BmcSatTrace_ptr self
)
- Clears the list of bdds that represents the model
- Defined in
bmcSatTrace.c
NodeList_ptr
bmc_sat_trace_prop2symb(
const BmcSatTrace_ptr self,
const BeEnc_ptr be_enc
)
- Example of mapping of STATE VARIABLES and BE VARIABLES:
----------------------------------------------------------
VAR x y x' y' x0 y0 x1 y1 x2 y2
BE index 0 1 2 3 4 5 6 7 8 9
CNF index 10 1 2 3 4 5 6 7 8 9
Time -2 | -1 | 0 | 1 | 2 |
Varindex 0 1 | 0 1 | 0 1 | 0 1 | 0 1 |
- Defined in
bmcSatTrace.c
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
- Defined in
bmcTableauLTLformula.c
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
- Defined in
bmcTableauLTLformula.c
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
- Defined in
bmcTableauLTLformula.c
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
- Defined in
bmcTableauLTLformula.c
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
- Defined in
bmcTableauLTLformula.c
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
- Defined in
bmcTableauLTLformula.c
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
- Defined in
bmcTableauLTLformula.c
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
- Defined in
bmcTest.c
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
- Defined in
bmcTest.c
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
- Defined in
bmcTest.c
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 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
- Defined in
bmcTest.c
node_ptr
bmc_wff_mkBinary(
int type,
node_ptr arg1,
node_ptr arg2
)
- Makes a binary WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
bmc_wff_mkConst(
int type
)
- Makes a constant WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
node_ptr
bmc_wff_mkUnary(
int type,
node_ptr arg
)
- Makes a unary WFF
- Side Effects node hash may change
- Defined in
bmcWff.c
static be_ptr
evaluateOn(
const BeEnc_ptr be_enc,
const node_ptr pltl_f,
const node_ptr pltl_g,
const int fromTime,
const int toTime,
const int k,
const int l,
const int evalType,
const int evalDir
)
- When only one argument is passed in (pltl_g==NULL), the
tableaux at the proper time instants for that argument are
computed (throught recursive calls to "getTableauAtTime")
and either disjunctively or conjunctively put together
(depending on the value of the "evalType" parameter).
When two arguments are given, the second one is evaluated
according to the following scheme (here we represent the
disjunctive case; "and" and "or" have to be exchanged to
obtain the conjunctive case):
(Aj or (Bi and Bi+1 and ... and Bj-1))
where A is the first argument, B is the second one, j is the
time the first argument is currently being evaluated on, and
i is the starting time for the whole evaluation (this
evaluation scheme is adopted as it is shared by all the
binary time operators in the PLTL logic).
In both cases, the proper evaluation set is computed
by calling the "projectOntoMainDomain" function, which deals
with both bounded and loop paths.
- See Also
getTableauAtTime
projectOntoMainDomain
- Defined in
bmcTableauPLTLformula.c
static be_ptr
getTableauAtTime(
const BeEnc_ptr be_enc,
const node_ptr pltl_wff,
const int time,
const int k,
const int l
)
- Tableaux for constant expressions and (negated) literals are
built immediately, while complex formulas are evaluated in a
compositional way. In particular, propositional operators are
evaluated throught recursive calls to the procedure
"getTableauAtTime" itself (no split on time instants is
necessary in this case). Time operators are evaluated (in a
uniform way) by means of a doubly recursive call, which
involves the "evaluateOn" procedure as a counterpart.
A concise representation of the set of time instants each time
operator refers to (together with its argument(s))
is passed to the "evaluateOn" procedure, which is then
responsible for recursively evaluating these arguments on the
proper set of integer time instants by calling
"getTableauAtTime" in turn.
- See Also
evaluateOn
- Defined in
bmcTableauPLTLformula.c
boolean
isPureFuture(
const node_ptr pltl_wff
)
- Checks wether a formula contains only future operators
- Defined in
bmcTableau.c
static EvalSet
projectOntoMainDomain(
const node_ptr pltl_wff,
int a,
int b,
const int k,
const int l,
const int interval_type,
const int eval_dir
)
- For bounded paths, the projection of the interval [a,b
- See Also
rho
evaluateOn
- Defined in
bmcTableauPLTLformula.c
static int
tau(
const node_ptr pltl_wff
)
- Recursively computes the (maximum) nesting depth of past
operators in the formula, which is an upper bound on its past
temporal horizon.
- See Also
projectOntoMainDomain
- Defined in
bmcTableauPLTLformula.c
(
)
- Builds a tableau for the LTL at length k with loopback l
(single loop, no loop and all loopbacks are allowed)
- Defined in
bmcTableau.c
(
)
- The function "rho" projects the time instant "i"
onto the main domain of a function f on a (k,l)-loop,
where l_f=l+p*tau(f) and k_f=k+p*tau(f)
(with p=k-l). It is rho(i,l,k)=i, when i
- Defined in
bmcTableauPLTLformula.c
(
)
- This control structure iterates on all the time
instants "i" in the EvalSet "set", according to the semantics of
EvalSet given above.
- Defined in
bmcTableauPLTLformula.c