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

void 
Bmc_AddCmd(
    
)
Adds all bmc-related commands to the interactive shell

See Also CInit_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_CommandBmcIncSimulate(
  int  argc, 
  char** argv 
)
Bmc_CommandBmcIncSimulate does incremental simulation of the model starting from an initial state.

Side Effects None

Defined in bmcCmd.c

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

Defined in bmcCmd.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_CommandBmcSimulateCheckFeasibleConstraints(
  int  argc, 
  char ** argv 
)
Checks feasibility of a list of constraints for the simulation

Side Effects None

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_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

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, 
  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

Defined in bmcBmcInc.c

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.

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_Gen_UnrollingFragment(
  BeFsm_ptr  be_fsm, 
  const int  i 
)
Generates i-th fragment of BMC unrolling

Side Effects None

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_InitData(
    
)
Initializes the BMC internal structures, but not all dependencies. Call Bmc_Init to initialize everything it is is what you need instead.

Defined in bmcPkg.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_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

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

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

Defined in bmcModel.c

void 
Bmc_QuitData(
    
)
De0Initializes the BMC internal structures, but not all dependencies. Call Bmc_Quit to deinitialize everything it is is what you need instead.

Defined in bmcPkg.c

void 
Bmc_Quit(
    
)
Frees all resources allocated for the BMC model manager

Defined in bmcPkg.c

int 
Bmc_Simulate(
  const BeFsm_ptr  be_fsm, 
  BddEnc_ptr  bdd_enc, 
  be_ptr  be_constraints, 
  boolean  time_shift, 
  const int  k, 
  const boolean  print_trace, 
  const boolean  changes_only, 
  const Simulation_Mode  mode 
)
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

Defined in bmcSimulate.c

int 
Bmc_StepWiseSimulation(
  BeFsm_ptr  be_fsm, 
  BddEnc_ptr  bdd_enc, 
  TraceManager_ptr  trace_manager, 
  int  target_steps, 
  be_ptr  constraints, 
  boolean  time_shift, 
  boolean  print_trace, 
  boolean  changes_only, 
  Simulation_Mode  mode 
)
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: 'print_trace' : shows the generated trace 'changes_only' : shows only variables that actually change value between one step and it's next one

Side Effects The possibly partial generated simulaiton trace is added to the trace manager for possible reuse.

See Also optional
Defined in bmcSimulate.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 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
Defined in bmcTableau.c

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)

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 OUTCOME_SUCCESS if k and l are compatible, otherwise return OUTCOME_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_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

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_fill_cntexample(
  BeEnc_ptr  be_enc, 
  SatSolver_ptr  solver, 
  const int  k, 
  Trace_ptr  trace 
)
The filled trace is returned. The given trace must be empty

See Also Bmc_fill_trace_from_cnf_model Bmc_Utils_generate_cntexample
Defined in bmcUtils.c

Trace_ptr 
Bmc_Utils_generate_and_print_cntexample(
  BeEnc_ptr  be_enc, 
  SatSolver_ptr  solver, 
  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.

See Also Bmc_Utils_generate_cntexample Bmc_Utils_fill_cntexample
Defined in bmcUtils.c

Trace_ptr 
Bmc_Utils_generate_cntexample(
  BeEnc_ptr  be_enc, 
  SatSolver_ptr  solver, 
  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 is non-volatile

See Also Bmc_Utils_generate_and_print_cntexample
Defined in bmcUtils.c

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.

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 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.

Defined in bmcUtils.c

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
Defined in bmcUtils.c

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
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

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, 
  boolean* res_e 
)
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 OUTCOME_GENERIC_ERROR if an error has occurred; Returns OUTCOME_SUCCESS_REQUIRED_HELP if -h options had been specified; Returns OUTCOME_SUCCESS in all other cases.

Side Effects Result parameters might change

Defined in bmcCmd.c

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. The returned trace is non-volatile. For more control over the built trace, please see Bmc_fill_trace_from_cnf_model

Side Effects none

See Also Trace_create Mc_create_trace_from_bdd_input_list Bmc_fill_trace_from_cnf_model
Defined in bmcTrace.c

Trace_ptr 
Bmc_fill_trace_from_cnf_model(
  const BeEnc_ptr  be_enc, 
  const Slist_ptr  cnf_model, 
  int  k, 
  Trace_ptr  trace 
)
Fills the trace. The trace will be 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_fill_trace_from_bdd_input_list
Defined in bmcTrace.c

int 
Bmc_pick_state_from_constr(
  BeFsm_ptr  fsm, 
  BddEnc_ptr  bdd_enc, 
  be_ptr  constr, 
  Simulation_Mode  mode 
)
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

Defined in bmcSimulate.c

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

Defined in bmcInt.c

Prop_ptr 
Bmc_rewrite_invar(
  const Prop_ptr  prop, 
  const BddEnc_ptr  bdd_enc, 
  SymbLayer_ptr  layer 
)
Returns a rewrited property

Defined in bmcInt.c

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

Defined in bmcSimulate.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 
UsageBmcIncSimulate(
    
)
Usage string for UsageBmcIncSimulate

Side Effects None

See Also Bmc_CommandBmcIncSimulate
Defined in bmcCmd.c

static int 
UsageBmcPickState(
    
)
Usage string for UsageBmcPickState

Side Effects None

See Also CommandBmcPickState
Defined in bmcCmd.c

static int 
UsageBmcSetup(
    
)
Usage string for Bmc_CommandBmcSetup

See Also Bmc_CommandBmcSetup
Defined in bmcCmd.c

static int 
UsageBmcSimulateCheckFeasibleConstraints(
    
)
Usage string for UsageBmcSimulateCheckFeasibleConstraints

Side Effects None

See Also Bmc_CommandSimulateCheckFeasibleConstraints
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

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

Defined in bmcBmcInc.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

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_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.

Defined in bmcSimulate.c

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.

Defined in bmcSimulate.c

void 
bmc_simulate_enable_random_mode(
  SatSolver_ptr  solver 
)
Enables random mode in the given sat solver. Seed used in random

Defined in bmcSimulate.c

void 
bmc_simulate_set_curr_sim_trace(
  Trace_ptr  trace, 
  int  idx 
)
Internal function used during the simulation to set the current simulation trace

Defined in bmcSimulate.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 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

Defined in bmcTest.c

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

Defined in bmcTrace.c

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

Defined in bmcTrace.c

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

Defined in bmcUtils.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

static boolean 
isPureFuture_aux(
  const node_ptr  pltl_wff, 
  hash_ptr  memoiz 
)
Memoized private service of isPureFuture

Defined in bmcTableau.c

boolean 
isPureFuture(
  const node_ptr  pltl_wff 
)
Checks wether a formula contains only future operators

Defined in bmcTableau.c

static boolean 
opt_check_bmc_inc_invar_alg(
  OptsHandler_ptr  opts, 
  const char* val 
)
Check function for the bmc_inc_invar_alg function

Defined in bmcOpt.c

static boolean 
opt_check_bmc_invar_alg(
  OptsHandler_ptr  opts, 
  const char* val 
)
Check function for the bmc_invar_alg option

Defined in bmcOpt.c

static boolean 
opt_check_bmc_pb_length(
  OptsHandler_ptr  opts, 
  const char* val 
)
Check function for the bmc_pb_lenght option

Defined in bmcOpt.c

static boolean 
opt_check_bmc_pb_loop(
  OptsHandler_ptr  opts, 
  const char* val 
)
Check function for the bmc_pb_loop option

Defined in bmcOpt.c

static void* 
opt_get_bmc_inc_invar_alg(
  OptsHandler_ptr  opts, 
  const char* val 
)
Get function for the bmc_inc_invar_alg function

Defined in bmcOpt.c

static void* 
opt_get_bmc_invar_alg(
  OptsHandler_ptr  opts, 
  const char* val 
)
Get function for the bmc_invar_alg function

Defined in bmcOpt.c

static void * 
opt_get_integer(
  OptsHandler_ptr  opts, 
  const char * value 
)
Get the integer representation of the given string

Defined in bmcOpt.c

static void* 
opt_get_string(
  OptsHandler_ptr  opts, 
  const char* val 
)
Get function for simple strings

Defined in bmcOpt.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

 
(
    
)
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

Last updated on 2011/06/16 12h:15