AtMostOnce()
Creates an expression which allows at most one el_i to be true
BmcInt_SBMCTableau_GetAtTime()
Given a wff expressed in ltl builds the model-independent tableau at 'time' of a path formula bounded by [k, l]
Bmc_Gen_SBMCProblem()
Returns the LTL problem at length k with loopback l (single loop, no loop and all loopbacks are allowed)
Bmc_Hash_delete_table()
Delete the table
Bmc_Hash_find()
Find a node in the table
Bmc_Hash_insert()
Insert an element in the table
Bmc_Hash_new_htable()
Create a new hash_table
Bmc_Hash_size()
Return the number of occupied slots
Bmc_SBMCGenSolveLtl()
Given a LTL property generates and solve the problems for all Ki (k_min<=i<=k_max). If bIncreaseK is 0 then k_min==k_max==k and only one problem is generated. If bIncreaseK is 1 then k_min == 0 and k_max == k. Each problem Ki takes into account of all possible loops from k_min to Ki if loopback is '*' (BMC_ALL_LOOPS).
Also see the Bmc_GenSolve_Action possible values
Bmc_SBMCTableau_GetAllLoops()
Builds tableau for all possible loops in [l, k[, taking into account of fairness using Kepa/Timo method
Bmc_SBMCTableau_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_SBMCTableau_GetNoLoop()
Builds tableau without loop
Bmc_SBMCTableau_GetSingleLoop()
Builds tableau for a single loop. This function takes into account of fairness
Bmc_Stack_delete()
Delete the stack
Bmc_Stack_new_stack()
Create a new stack
Bmc_Stack_pop()
Pop an element from the stack
Bmc_Stack_push()
Push a node unto the stack
Bmc_Stack_size()
Return the number of occupied slots
Bmc_Stack_top()
Return the top element of the stack
Loop()
Creates the expression: wedge_{i=0}^{k-1} el_i => (s_i <=> s_k)
SBmc_AddCmd()
Adds all bmc-related commands to the interactive shell
SBmc_Init()
Initializes the SBMC sub package
SBmc_Quit()
Frees all resources allocated for SBMC
Sbmc_CommandCheckLtlSpecSBmc()
Uses Kepa's and Timo's method for doing bmc
Sbmc_CommandGenLtlSpecSBmc()
Generate length_max+1 problems iterating the problem bound from zero to length_max, and dumps each problem to a dimacs file. Uses Kepa's and Timo's method for doing bmc
Sbmc_CommandLTLCheckZigzagInc()
Uses Kepa's and Timo's method for doing incremental bmc
Sbmc_Utils_fill_cntexample()
Fills the given trace using the given sat assignment.
Sbmc_Utils_generate_and_print_cntexample()
Extracts a trace from a sat assignment, and prints it.
Sbmc_Utils_generate_cntexample()
Extracts a trace from a sat assignment.
Sbmc_check_psl_property()
Top-level function for bmc of PSL properties
bmcSBMC_tableau_GF_FG_last()
Construct f(k) att full pastdepth for the GF-,F-,FG-, or G-operator
bmc_cache_delete()
Frees the arrays used by the cache
bmc_cache_init()
Initialises the chache used to store f_i(time) and g_(time) values.
bmc_expandFilename()
This is only a useful wrapper for easily call Bmc_Utils_ExpandMacrosInFilename
bmc_past_depth()
Computes the maximum nesting depth of past operators in PLTL formula
bmc_tableauGetEventuallyIL_opt()
Returns an expression which initialises f(k+1) for an F or an GF formula when we use the il-optimisation.
bmc_tableauGetGloballyIL_opt()
Returns an expression which initialises f(k+1) for a 'globally' or an FG formula when we use the il-optimisation.
find()
Return index of node, a free index if the node is not in the table
formulaMap()
Map temporal subformulas to an integer, returns the number subformulas with temporal connectives
get_Eventually_at_time()
Genrates a boolean expression which is true iff the ltl formula ltl_wff is true at time, handles the FINALLY operator
get_Globally_at_time()
Generates a boolean expression which is true iff the ltl formula ltl_wff is true at time, handles the GLOBALLY operator
get_Historically_at_time()
Genrates a boolean expression which is true iff the ltl formula ltl_wff is true at time, handles the HISTORICALLY operator
get_Once_at_time()
Genrates a boolean expression which is true iff the ltl formula ltl_wff is true at time, handles the ONCE operator
get_Since_at_time()
Genrates a boolean expression which is true iff the ltl formula ltl_wff is true at time, handles the SINCE operator
get_Trigger_at_time()
Genrates a boolean expression which is true iff the ltl formula ltl_wff is true at time, handles the TRIGGER operator
get_Until_at_time()
Genrates a boolean expression which is true iff the ltl formula ltl_wff is true at time, handles the UNTIL operator
get_V_at_time()
Genrates a boolean expression which is true iff the ltl formula ltl_wff is true at time, handles the RELEASE operator
get_el_at_time()
Returns a pointer to the el(time) variable
get_f_at_time()
Genrates a boolean expression which is true iff the ltl formula ltl_wff is true at time
get_g_at_time()
get_il_at_time()
Returns a pointer to the il(time) variable
get_loop_exists()
Returns a pointer to the le variable
last_f()
Generate f(k,pastdepth) when pastdepth is less than maximum pastdepth, except for OP_NEXT where pastdepth can also be the maximum.
last_g()
Generate the last f(k) for operators that use the auxillary encoding g.
sbmc_1_fresh_state_var()
Creates a new fresh state variable.
sbmc_E_state()
Routines for the state indexing scheme
sbmc_L_state()
Routines for the state indexing scheme
sbmc_MS_create_volatile_group()
Create the volatile group in the meta solver wrapper
sbmc_MS_create()
Creates a meta solver wrapper
sbmc_MS_destroy_volatile_group()
Destroy the volatile group of the meta solver wrapper and force use of the permanent one
sbmc_MS_destroy()
Destroy a meta solver wrapper
sbmc_MS_force_constraint_list()
Forces a list of BEs to be true in the solver.
sbmc_MS_force_true()
Forces a BE to be true in the solver.
sbmc_MS_get_conflicts()
Returns the underlying solver
sbmc_MS_get_model()
Returns the model (of previous solving)
sbmc_MS_get_solver()
Returns the underlying solver
sbmc_MS_goto_permanent_group()
Destroy the volatile group of the meta solver wrapper
sbmc_MS_goto_volatile_group()
Create and force use of the volatile group of the meta solver wrapper
sbmc_MS_solve_assume()
Solves all groups belonging to the solver assuming the CNF assumptions and returns the flag.
sbmc_MS_solve()
Solves all groups belonging to the solver and returns the flag.
sbmc_MS_switch_to_permanent_group()
Force use of the permanent group of the meta solver wrapper
sbmc_MS_switch_to_volatile_group()
Force use of the volatile group of the meta solver wrapper
sbmc_SimplePaths()
Build SimplePath_{i,k} for each 0<=i sbmc_add_loop_variable()
Declares a new layer to contain the loop variable.
sbmc_add_new_state_variable()
Declare a new boolean state variable in the layer.
sbmc_alloc_node_info()
Creates an empty structure to hold information associated to each subformula.
sbmc_allocate_trans_vars()
Creates info->pastdepth+1 new state variables for the main translation in info->trans_vars.
sbmc_build_InLoop_i()
Build InLoop_i
sbmc_cmd_options_handling()
Sbmc commands options handling for commands (optionally) acceping options -k -l -o -p -n -N -c
sbmc_dependent()
required
sbmc_equal_vectors_formula()
Makes the BE formula "land_{v in vars} s_i = s_j"
sbmc_find_formula_vars()
Compute the variables that occur in the formula ltlspec.
sbmc_find_relevant_vars()
Find state and input variables that occurr in the formula.
sbmc_formula_dependent()
Create the formula specific k-dependent constraints.
sbmc_init_LTL_info()
Associates each subformula node of ltlspec with a sbmc_LTL_info.
sbmc_init_state_vector()
Initialize trans_bes[i
sbmc_loop_var_name_get()
Gets the name of the loop variable.
sbmc_loop_var_name_set()
Sets the name of the loop variable.
sbmc_make_boolean_formula()
Takes a property and return the negation of the property conjoined with the big and of fairness conditions.
sbmc_model_k()
Routines for the state indexing scheme
sbmc_n_fresh_state_vars()
Creates N new fresh state variables.
sbmc_node_info_assoc_create()
Creates an asociative list for pairs node_ptr sbmc_node_info *
sbmc_node_info_assoc_find()
Return the information associated to a subformula if any.
sbmc_node_info_assoc_free()
Creates an asociative list for pairs node_ptr sbmc_node_info *
sbmc_node_info_assoc_insert()
Insert in the assoc table the infomrnation for the subformula.
sbmc_node_info_free()
Frees a structure to hold information associated to each subformula.
sbmc_print_Fvarmap()
Prints some of the information associated to a F formula
sbmc_print_Gvarmap()
Prints some of the information associated to a G formula
sbmc_print_node_list()
Prints a lsList of node_ptr
sbmc_print_node()
Print a node_ptr expression by prefixing and suffixing it.
sbmc_print_varmap()
Prints some of the information associated to a subformula
sbmc_real_k_string()
Routines for the state indexing scheme
sbmc_real_k()
Routines for the state indexing scheme
sbmc_remove_loop_variable()
Remove the new layer to contain the loop variable.
sbmc_set_create()
Creates an associtative list to avoid duplicates of node_ptr
sbmc_set_destroy()
Destroy an associative list used to avoid duplicates of node_ptr.
sbmc_set_insert()
Insert a node in the hash
sbmc_set_is_in()
Checks if a node_ptr was already inserted.
sbmc_state_vars_create()
Creates an empty state_vars_struct
sbmc_state_vars_destroy()
state_vars_struct destroyer
sbmc_state_vars_get_LastState_var()
getter for field "LastState_var"
sbmc_state_vars_get_LoopExists_var()
getter for field "LoopExists_var"
sbmc_state_vars_get_formula_input_vars()
getter for field "formula_input_vars"
sbmc_state_vars_get_formula_state_vars()
getter for field "formula_state_vars"
sbmc_state_vars_get_l_var()
getter for field "l_var"
sbmc_state_vars_get_simple_path_system_vars()
getter for field "simple_path_system_vars"
sbmc_state_vars_get_trans_state_vars()
getter for field "trans_state_vars"
sbmc_state_vars_get_translation_vars_aux()
getter for field "translation_vars_aux"
sbmc_state_vars_get_translation_vars_pd0()
getter for field "translation_vars_pd0"
sbmc_state_vars_get_translation_vars_pdx()
getter for field "translation_vars_pdx"
sbmc_state_vars_print()
Print a state_vars_struct
sbmc_state_vars_set_LastState_var()
setter for field "LastState_var"
sbmc_state_vars_set_LoopExists_var()
setter for field "LoopExists_var"
sbmc_state_vars_set_formula_input_vars()
setter for field "formula_input_vars"
sbmc_state_vars_set_formula_state_vars()
setter for field "formula_state_vars"
sbmc_state_vars_set_l_var()
setter for field "l_var"
sbmc_state_vars_set_simple_path_system_vars()
setter for field "simple_path_system_vars"
sbmc_state_vars_set_trans_state_vars()
setter for field "transition_state_vars"
sbmc_state_vars_set_translation_vars_aux()
setter for field "translation_vars_aux"
sbmc_state_vars_set_translation_vars_pd0()
setter for field "translation_state_vars_pd0"
sbmc_state_vars_set_translation_vars_pdx()
setter for field "translation_vars_pdx"
sbmc_unroll_base()
Creates the BASE constraints.
sbmc_unroll_invariant_f()
Create the k-invariant constraints for propositional and future temporal operators at time i.
sbmc_unroll_invariant_propositional()
Create the k-invariant constraints for propositional operators at time i.
sbmc_unroll_invariant_p()
Create the k-invariant constraints at time i.
sbmc_unroll_invariant()
Unroll future and past fragment from previous_k+1 upto and including new_k.

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