Be2bexpDfsData_head()
Be2bexpDfsData_head
Be2bexpDfsData_pop()
Be2bexpDfsData_pop
Be2bexpDfsData_push()
Sets a node into the stack
Be2bexp_Back()
Be2bexp_Back
Be2bexp_First()
Be2bexpFirst
Be2bexp_Last()
Be2bexp_Last
Be2bexp_Set()
Be2bexpSet
BmcInt_Tableau_GetAtTime()
Given a wff expressed in ltl builds the model-independent tableau at 'time' of a path formula bounded by [k, l]
Bmc_AddCmd()
Adds all bmc-related commands to the interactive shell
Bmc_CheckFairnessListForPropositionalFormulae()
Helper function to simplify calling to 'bmc_check_wff_list' for searching of propositional wff only. Returns a new list of wffs which contains legal wffs only
Bmc_CommandBmcIncSimulate()
Bmc_CommandBmcIncSimulate does incremental simulation of the model starting from an initial state.
Bmc_CommandBmcPickState()
Picks a state from the set of initial states
Bmc_CommandBmcSetup()
Initializes the bmc sub-system, and builds the model in a Boolean Expression format
Bmc_CommandBmcSimulateCheckFeasibleConstraints()
Checks feasibility of a list of constraints for the simulation
Bmc_CommandBmcSimulate()
Bmc_CommandBmcSimulate generates a trace of the problem represented from the simple path from 0 (zero) to k
Bmc_CommandCheckInvarBmcInc()
Solve the given invariant, or all invariants if no formula is given, using incremental algorithms.
Bmc_CommandCheckInvarBmc()
Generates and solve the given invariant, or all invariants if no formula is given
Bmc_CommandCheckLtlSpecBmcInc()
Checks the given LTL specification, or all LTL specifications in the properties database if no formula is given, using incremental algorithms
Bmc_CommandCheckLtlSpecBmcOnePb()
Checks the given LTL specification, or all LTL specifications if no formula is given. Checking parameters are the problem bound and the loopback values
Bmc_CommandCheckLtlSpecBmc()
Checks the given LTL specification, or all LTL specifications in the properties database if no formula is given
Bmc_CommandGenInvarBmc()
Generates and dumps the problem for the given invariant or for all invariants if no formula is given. SAT solver is not invoked.
Bmc_CommandGenLtlSpecBmcOnePb()
Generates only one problem with fixed bound and loopback, and dumps the problem to a dimacs file. The single problem is dumped for the given LTL specification, or for all LTL specifications if no formula is given
Bmc_CommandGenLtlSpecBmc()
Generates length_max+1 problems iterating the problem bound from zero to length_max, and dumps each problem to a dimacs file
Bmc_Conv_Be2Bexp()
Given a be, constructs the corresponding boolean expression
Bmc_Conv_Bexp2Be()
Converts given boolean expression into correspondent reduced boolean circuit
Bmc_Conv_BexpList2BeList()
Converts given boolean expressions list into correspondent reduced boolean circuits list
Bmc_Conv_cleanup_cached_entries_about()
Removes from the cache those entries that depend on the given symbol
Bmc_Conv_get_BeModel2SymbModel()
This function converts a BE model (i.e. a list of BE literals) to symbolic expressions.
Bmc_Conv_init_cache()
Initializes module Conv
Bmc_Conv_quit_cache()
De-initializes module Conv
Bmc_GenSolveInvarDual()
Solve an INVARSPEC problems wiht algorithm Dual
Bmc_GenSolveInvarFalsification()
Solve an INVARSPEC problems wiht algorithm Fasification
Bmc_GenSolveInvarZigzag()
Solve an INVARSPEC problems with algorithm ZigZag
Bmc_GenSolveLtlInc()
Solves LTL problem the same way as the original Bmc_GenSolveLtl but just adds BE representing the path incrementaly.
Bmc_Gen_InvarBaseStep()
Returns the base step of the invariant construction
Bmc_Gen_InvarInductStep()
Returns the induction step of the invariant construction
Bmc_Gen_InvarProblem()
Builds and returns the invariant problem of the given propositional formula
Bmc_Gen_LtlProblem()
Returns the LTL problem at length k with loopback l (single loop, no loop and all loopbacks are allowed)
Bmc_Gen_UnrollingFragment()
Generates i-th fragment of BMC unrolling
Bmc_GetTestTableau()
Bmc_InitData()
Initializes the BMC internal structures, but not all dependencies. Call Bmc_Init to initialize everything it is is what you need instead.
Bmc_Init()
Initializes the BMC structure
Bmc_IsPropositionalFormula()
Given a wff returns 1 if wff is a propositional formula, zero (0) otherwise.
Bmc_Model_GetFairness()
Generates and returns an expression representing all fairnesses in a conjunctioned form
Bmc_Model_GetInit0()
Retrieves the init states from the given fsm, and compiles them into a BE at time 0
Bmc_Model_GetInitI()
Retrieves the init states from the given fsm, and compiles them into a BE at time i
Bmc_Model_GetInvarAtTime()
Retrieves the invars from the given fsm, and compiles them into a BE at the given time
Bmc_Model_GetPathNoInit()
Returns the path for the model from 0 to k, taking into account the invariants (and no init)
Bmc_Model_GetPathWithInit()
Returns the path for the model from 0 to k, taking into account initial conditions and invariants
Bmc_Model_GetTransAtTime()
Retrieves the trans from the given fsm, and compiles it into a MSatEnc at the given time
Bmc_Model_GetUnrolling()
Unrolls the transition relation from j to k, taking into account of invars
Bmc_Model_Invar_Dual_forward_unrolling()
Unrolls the transition relation from j to k, taking into account of invars
Bmc_QuitData()
De0Initializes the BMC internal structures, but not all dependencies. Call Bmc_Quit to deinitialize everything it is is what you need instead.
Bmc_Quit()
Frees all resources allocated for the BMC model manager
Bmc_Simulate()
Performs simulation
Bmc_StepWiseSimulation()
SAT Based Incremental simulation
Bmc_TableauLTL_GetAllLoopsDepth1()
Builds tableau for all possible loops in [l, k], in the particular case in which depth is 1. This function takes into account of fairness
Bmc_TableauLTL_GetAllLoops()
Builds tableau for all possible loops in [l, k[, taking into account of fairness
Bmc_TableauLTL_GetNoLoop()
Builds tableau without loop at time zero, taking into account of fairness
Bmc_TableauLTL_GetSingleLoopWithFairness()
Builds the tableau at time zero. Loop is allowed, fairness are taken into account
Bmc_TableauLTL_GetSingleLoop()
Builds the tableau at time zero. Loop is allowed, fairness are taken into account
Bmc_TableauPLTL_GetAllLoopsDepth1()
Builds tableau for all possible (k,l)-loops for a fixed k, in the particular case depth==1. This function takes into account of fairness.
Bmc_TableauPLTL_GetAllLoops()
Returns the conjunction of the single-loop tableaux for all possible (k,l)-loops for a fixed k. Each single-loop tableau takes into account of both fairness constraints and loop condition.
Bmc_TableauPLTL_GetAllTimeTableau()
Builds the conjunction of the tableaux for a PLTL formula computed on every time instant along a (k,l)-loop.
Bmc_TableauPLTL_GetNoLoop()
Returns the tableau for a PLTL formula on a bounded path of length k, reasoning on fairness conditions as well.
Bmc_TableauPLTL_GetSingleLoop()
Returns the tableau for a PLTL formula on a (k,l)-loop, conjuncted with both fairness conditions and the loop condition on time steps k and l.
Bmc_TableauPLTL_GetTableau()
Builds the tableau for a PLTL formula.
Bmc_Tableau_GetAllLoopsDepth1()
Builds tableau for all possible loops in [l, k], in the particular case in which depth is 1. This function takes into account of fairness
Bmc_Tableau_GetAllLoopsDisjunction()
Builds the disjunction of all the loops conditions for (k-l)-loops with l in [0, k[
Bmc_Tableau_GetAllLoops()
Builds tableau for all possible loops in [l, k[, taking into account of fairness
Bmc_Tableau_GetLoopCondition()
Builds a tableau that constraints state k to be equal to state l. This is the condition for a path of length (k+1) to represent a (k-l)loop (new semantics).
Bmc_Tableau_GetLtlTableau()
Builds a tableau for the LTL at length k with loopback l (single loop, no loop and all loopbacks are allowed)
Bmc_Tableau_GetNoLoop()
Builds tableau without loop at time zero, taking into account of fairness
Bmc_Tableau_GetSingleLoop()
Builds tableau for all possible loops in [l, k], in the particular case in which depth is 1. This function takes into account of fairness
Bmc_TestReset()
Call this function to reset the test sub-package (into the reset command for example)
Bmc_TestTableau()
The first time Bmc_TestTableau is called in the current session this function creates a smv file with a model and generates a random ltl spec to test tableau. The following times it is called it appends a new formula to the file.
Bmc_Utils_Check_k_l()
Checks the (k,l) couple. l must be absolute.
Bmc_Utils_ConvertLoopFromInteger()
Given an integer containing the inner representation of the loopback value, returns as parameter the corresponding user-side value as string
Bmc_Utils_ConvertLoopFromString()
Given a string representing a loopback possible value, returns the corresponding integer. The (optional) parameter result will be assigned to OUTCOME_SUCCESS if the conversion has been successfully performed, otherwise to OUTCOME_GENERIC_ERROR is the conversion failed. If result is NULL, OUTCOME_SUCCESS is the aspected value, and an assertion is implicitly performed to check the conversion outcome.
Bmc_Utils_ExpandMacrosInFilename()
Search into a given string any symbol which belongs to a determined set of symbols, and expand each found symbol, finally returning the resulting string
Bmc_Utils_GetAllLoopbacksString()
Returns a constant string which represents the "all loops" semantic.
Bmc_Utils_GetAllLoopbacks()
Returns the integer value which represents the "all loops" semantic
Bmc_Utils_GetNoLoopback()
Returns the integer value which represents the "no loop" semantic
Bmc_Utils_GetSuccTime()
Given time<=k and a [l, k] interval, returns next time, or BMC_NO_LOOP if time is equal to k and there is no loop
Bmc_Utils_IsAllLoopbacksString()
Returns true if the given string represents the "all possible loops" value.
Bmc_Utils_IsAllLoopbacks()
Returns true if the given loop value represents the "all possible loopbacks" semantic
Bmc_Utils_IsNoLoopbackString()
Returns true if the given string represents the no loopback value
Bmc_Utils_IsNoLoopback()
Returns true if l has the internally encoded "no loop" value
Bmc_Utils_IsSingleLoopback()
Returns true if the given loop value represents a single (relative or absolute) loopback
Bmc_Utils_RelLoop2AbsLoop()
Converts a relative loop value (wich can also be an absolute loop value) to an absolute loop value
Bmc_Utils_apply_inlining4inc()
Applies inlining forcing inclusion of the conjunct set. Useful in the incremental SAT applications to guarantee soundness
Bmc_Utils_apply_inlining()
Applies inlining taking into account of current user settings
Bmc_Utils_fill_cntexample()
Given a solver containing a model for a problem, fills the given counter-example correspondingly
Bmc_Utils_generate_and_print_cntexample()
Given a problem, and a solver containing a model for that problem, generates and prints a counter-example
Bmc_Utils_generate_cntexample()
Given a problem, and a solver containing a model for that problem, generates a counter-example
Bmc_Utils_get_vars_list_for_uniqueness_fsm()
Creates a list of BE variables that are intended to be used by the routine that makes the state unique in invariant checking.
Bmc_Utils_get_vars_list_for_uniqueness()
Creates a list of BE variables that are intended to be used by the routine that makes the state unique in invariant checking.
Bmc_Utils_next_costraint_from_string()
Reads a next expression and builds the corresponding BE formula.
Bmc_Utils_simple_costraint_from_string()
Reads a simple expression and builds the corresponding BE formula.
Bmc_WffListMatchProperty()
For each element belonging to a given list of wffs, calls the given matching function. If function matches, calls given answering function
Bmc_check_if_model_was_built()
A service for commands, to check if bmc has been built
Bmc_check_psl_property()
Top-level function for bmc of PSL properties
Bmc_cmd_options_handling()
Bmc commands options handling for commands (optionally) acceping options -k -l -o -a -n -p -P -e
Bmc_create_trace_from_cnf_model()
Creates a trace out of a cnf model
Bmc_fill_trace_from_cnf_model()
Fills the given trace out of a cnf model
Bmc_pick_state_from_constr()
Picks a state from the initial state, creates a trace from it.
Bmc_rewrite_cleanup()
Crean up the memory after the rewritten property check
Bmc_rewrite_invar()
Rewrites an invariant specification containing input variables or next with an observer state variable
Bmc_simulate_check_feasible_constraints()
Checks the truth value of a list of constraints on the current state, transitions and next states, from given starting state. This can be used in guided interactive simulation to propose the set of transitions which are allowed to occur in the interactive simulation.
UsageBmcCheckInvarInc()
Usage string for command check_invar_bmc_inc
UsageBmcCheckInvar()
Usage string for command check_invar_bmc
UsageBmcCheckLtlSpecInc()
Usage string for command check_ltlspec_bmc_inc
UsageBmcCheckLtlSpecOnePb()
Usage string for command check_ltlspec_bmc_onepb
UsageBmcCheckLtlSpec()
Usage string for command check_ltlspec_bmc
UsageBmcGenInvar()
Usage string for command gen_invar_bmc
UsageBmcGenLtlSpecOnePb()
Usage string for command gen_ltlspec_bmc_onepb
UsageBmcGenLtlSpec()
Usage string for command gen_ltlspec_bmc
UsageBmcIncSimulate()
Usage string for UsageBmcIncSimulate
UsageBmcPickState()
Usage string for UsageBmcPickState
UsageBmcSetup()
Usage string for Bmc_CommandBmcSetup
UsageBmcSimulateCheckFeasibleConstraints()
Usage string for UsageBmcSimulateCheckFeasibleConstraints
UsageBmcSimulate()
Usage string for UsageBmcSimulate
UsageBmcTestTableau()
Usage string for Bmc_TestTableau
bmc_add_be_into_solver_positively()
Converts Be into CNF, and adds it into a group of a solver, sets polarity to 1, and then destroys the CNF.
bmc_add_be_into_solver()
Converts Be into CNF, and adds it into a group of a solver.
bmc_add_valid_wff_to_list()
private service for Bmc_CheckFairnessListForPropositionalFormulae
bmc_build_master_be_fsm()
bmc_build_uniqueness()
Builds the uniqueness contraint for dual and zigzag algorithms
bmc_check_if_wff_is_valid()
private service for Bmc_CheckFairnessListForPropositionalFormulae
bmc_conv_bexp2be_recur()
Private service for Bmc_Conv_Bexp2Be
bmc_conv_query_cache()
Queries the bexpr->be cache
bmc_conv_set_cache()
Update the bexpr -> be cache
bmc_is_propositional_formula_aux()
Useful wrapper for Bmc_CheckFairnessListForPropositionalFormulae
bmc_simulate_add_be_into_inc_solver_positively()
Converts Be into CNF, and adds it into a group of a incremental solver, sets polarity to 1, and then destroys the CNF.
bmc_simulate_add_be_into_non_inc_solver_positively()
Converts Be into CNF, and adds it into a group of a non-incremental solver, sets polarity to 1, and then destroys the CNF.
bmc_simulate_ask_for_state()
Aux function for interactive simulation. Asks the user for a number from 0 to max_choice.
bmc_simulate_enable_random_mode()
Enables random mode in the given sat solver
bmc_simulate_interactive_step()
Performs a step of interactive simulation
bmc_simulate_print_state()
Aux function for interactive simulation. Prints the given set of assignments
bmc_simulate_set_curr_sim_trace()
Internal function used during the simulation to set the current simulation trace
bmc_simulate_trace_step_print()
Aux function for interactive simulation. Prints the given set of assignments
bmc_tableauGetEventuallyAtTime()
Resolves the future operator, and builds a conjunctive expression of tableaus, by iterating intime up to k in a different manner depending on the [l, k] interval form
bmc_tableauGetGloballyAtTime()
As bmc_tableauGetEventuallyAtTime, but builds a conjunctioned expression in order to be able to assure a global constraint
bmc_tableauGetNextAtTime()
Resolves the NEXT operator, building the tableau for its argument
bmc_tableauGetReleasesAtTime_aux()
auxiliary part of bmc_tableauGetReleasesAtTime
bmc_tableauGetReleasesAtTime()
Builds an expression which evaluates the release operator
bmc_tableauGetUntilAtTime_aux()
auxiliary part of bmc_tableauGetUntilAtTime
bmc_tableauGetUntilAtTime()
Builds an expression which evaluates the until operator
bmc_test_bexpr_output()
Write to specified FILE stream given node_ptr formula with specified output_type format. There are follow formats: BMC_BEXP_OUTPUT_SMV, BMC_BEXP_OUTPUT_LB
bmc_test_gen_tableau()
Given a WFF in NNF, converts it into a tableau formula, then back to WFF_(k,l) and returns WFF -> WFF_(k,l)
bmc_test_gen_wff()
Builds a random LTL WFF with specified max depth and max connectives.
bmc_test_mk_loopback_ltl()
For each variable p in the set of state variables, generates the global equivalence of p and X^(loop length), starting from the loop start
bmc_trace_utils_append_input_state()
Appends a _complete_ (i,S') pair to existing trace
bmc_trace_utils_complete_trace()
Populates trace with valid defaults assignments
bmc_utils_costraint_from_string()
Reads an expression and builds the corresponding BE formula. If accept_next_expr is true, then a next expression is parsed, otherwise a simple expression is parsed.
evaluateOn()
Evaluates (either disjunctively or conjunctively) a PLTL formula over an interval of time.
getTableauAtTime()
Builds the tableau for a PLTL formula "pltl_wff" at time "time".
isPureFuture_aux()
Memoized private service of isPureFuture
isPureFuture()
Checks wether a formula contains only future operators
opt_check_bmc_inc_invar_alg()
Check function for the bmc_inc_invar_alg function
opt_check_bmc_invar_alg()
Check function for the bmc_invar_alg option
opt_check_bmc_pb_length()
Check function for the bmc_pb_lenght option
opt_check_bmc_pb_loop()
Check function for the bmc_pb_loop option
opt_get_bmc_inc_invar_alg()
Get function for the bmc_inc_invar_alg function
opt_get_bmc_invar_alg()
Get function for the bmc_invar_alg function
opt_get_integer()
Get the integer representation of the given string
opt_get_string()
Get function for simple strings
projectOntoMainDomain()
Projects a (possibly open) interval [a,b
tau()
Gives an upper bound on the past temporal horizon of a PLTL formula.
()
()

Last updated on 2012/11/18 14h:16