-
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_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 2010/11/03 21h:54