sbmcBmc.c
High level functionalities for SBMC
sbmcBmcInc.c
High level functionalities for Incrememntal SBMC
sbmcCmd.c
Bmc.Cmd module
sbmcGen.c
Bmc.Gen module
sbmcHash.c
An has table for (node, unsigned) pairs
sbmcNodeStack.c
A stack of node_ptr
sbmcPkg.c
Bmc.Pkg module
sbmcUtil.c
Utilities for SBMC functionalities
sbmcTableau.c
Bmc.Tableau module
sbmcTableauInc.c
High level generic tableau routines for incremental SBMC.
sbmcTableauIncLTLformula.c
Bmc.Tableau module
sbmcTableauLTLformula.c
Bmc.Tableau module
sbmcUtils.c
Utilities function for SBMC package

sbmcBmc.c

High level functionalities for SBMC

By: Timo Latvala, Marco Roveri

User-commands directly use function defined in this module. This is the highest level in the SBMC API architecture. For further information about this implementation see: T. Latvala, A. Biere, K. Heljanko, and T. Junttila. Simple is Better: Efficient Bounded Model Checking for Past LTL. In: R. Cousot (ed.), Verification, Model Checking, and Abstract Interpretation, 6th International Conference VMCAI 2005, Paris, France, Volume 3385 of LNCS, pp. 380-395, Springer, 2005. Copyright Springer-Verlag.

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_expandFilename()
This is only a useful wrapper for easily call Bmc_Utils_ExpandMacrosInFilename

sbmcBmcInc.c

High level functionalities for Incrememntal SBMC

By: Tommi Junttila, Marco Roveri

User-commands directly use function defined in this module. This is the highest level in the Incrememntal SBMC API architecture. For further information about this implementation, see: K. Heljanko, T. Junttila and T. Latvala. Incremental and Complete Bounded Model Checking for Full PLTL. In K. Etessami and S. Rajamani (eds.), Computer Aided Verification, Edinburgh, Scotland, Volume 3576 of LNCS, pp. 98-111, Springer, 2005. Copyright Springer-Verlag.


sbmcCmd.c

Bmc.Cmd module

By: Timo Latvala, Tommi Juntilla, Marco Roveri Copyright [ This file is part of the ``bmc.sbmc'' package of NuSMV version 2. Copyright (C) 2004 Timo Latvala Copyright (C) 2006 Tommi Junttila. NuSMV version 2 is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. NuSMV version 2 is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA. For more information of NuSMV see or email to . Please report bugs to . To contact the NuSMV development board, email to .

This module contains all the sbmc commands implementation. Options parsing and checking is performed here, than the high-level SBMC layer is called

See AlsobmcPkg.c, bmcBmc.c

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_check_psl_property()
Top-level function for bmc of PSL properties
sbmc_cmd_options_handling()
Sbmc commands options handling for commands (optionally) acceping options -k -l -o -p -n -N -c

sbmcGen.c

Bmc.Gen module

By: Timo Latvala, Marco Roveri

This module contains all the problems generation functions

See AlsobmcBmc.c, bmcTableau.c, bmcModel.c

Bmc_Gen_SBMCProblem()
Returns the LTL problem at length k with loopback l (single loop, no loop and all loopbacks are allowed)

sbmcHash.c

An has table for (node, unsigned) pairs

By: Timo Latvala

An has table for (node, unsigned) pairs

Bmc_Hash_new_htable()
Create a new hash_table
Bmc_Hash_find()
Find a node in the table
Bmc_Hash_size()
Return the number of occupied slots
Bmc_Hash_insert()
Insert an element in the table
Bmc_Hash_delete_table()
Delete the table
find()
Return index of node, a free index if the node is not in the table

sbmcNodeStack.c

A stack of node_ptr

By: Timo Latvala

A stack of node_ptr

Bmc_Stack_new_stack()
Create a new stack
Bmc_Stack_push()
Push a node unto the stack
Bmc_Stack_size()
Return the number of occupied slots
Bmc_Stack_pop()
Pop an element from the stack
Bmc_Stack_delete()
Delete the stack
Bmc_Stack_top()
Return the top element of the stack

sbmcPkg.c

Bmc.Pkg module

By: Timo Latvala, Marco Roveri

This module contains all the bmc package handling functions

SBmc_Init()
Initializes the SBMC sub package
SBmc_Quit()
Frees all resources allocated for SBMC
SBmc_AddCmd()
Adds all bmc-related commands to the interactive shell

sbmcUtil.c

Utilities for SBMC functionalities

By: Tommi Junttila, Timo Latvala, Marco Roveri

This file contains utilities for the Simple Bounded Model Checking algorithms published in the paper by Heljanko, Junttila and Latvala at CAV 2005.


sbmcTableau.c

Bmc.Tableau module

By: Timo Latvala, Marco Roveri

This module contains all the tableau-related operations

See AlsobmcModel.c, bmcConv.c, bmcVarMgr.c bmcTableau.c, bmcTableauLTLformula.c, bmcTableauPLTLformula.c, sbmcTableauLTLformula.c, bmcGen.c sbmcGen.c

Bmc_SBMCTableau_GetNoLoop()
Builds tableau without loop
Bmc_SBMCTableau_GetSingleLoop()
Builds tableau for a single loop. This function takes into account of fairness
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_get_fairness()
Builds AND_i G F fc_i

sbmcTableauInc.c

High level generic tableau routines for incremental SBMC.

By: Tommi Junttila, Marco Roveri

High level generic tableau routines for incremental SBMC.

sbmc_equal_vectors_formula()
Makes the BE formula "land_{v in vars} s_i = s_j"
sbmc_init_LTL_info()
Associates each subformula node of ltlspec with a sbmc_LTL_info.
sbmc_init_state_vector()
Initialize trans_bes[i
sbmc_build_InLoop_i()
Build InLoop_i
sbmc_SimplePaths()
Build SimplePath_{i,k} for each 0<=i

sbmcTableauIncLTLformula.c

Bmc.Tableau module

By: Tommi Junttila, Marco Roveri

This module contains all the operations related to the construction of SBMC incremental tableaux for LTL formulas

sbmc_unroll_base()
Creates the BASE constraints.
sbmc_unroll_invariant_propositional()
Create the k-invariant constraints for propositional operators at time i.
sbmc_unroll_invariant_f()
Create the k-invariant constraints for propositional and future temporal operators at time i.
sbmc_unroll_invariant_p()
Create the k-invariant constraints at time i.
sbmc_formula_dependent()
Create the formula specific k-dependent constraints.
sbmc_unroll_invariant()
Unroll future and past fragment from previous_k+1 upto and including new_k.
sbmc_dependent()
required

sbmcTableauLTLformula.c

Bmc.Tableau module

By: Timo Latvala, Marco Roveri

This module contains all the operations related to the construction of SBMC tableaux for LTL formulas

See AlsobmcGen.c, bmcModel.c, bmcConv.c, bmcVarMgr.c

BmcInt_SBMCTableau_GetAtTime()
Given a wff expressed in ltl builds the model-independent tableau at 'time' of a path formula bounded by [k, l]
bmcSBMC_tableau_GF_FG_last()
Construct f(k) att full pastdepth for the GF-,F-,FG-, or G-operator
last_g()
Generate the last f(k) for operators that use the auxillary encoding g.
last_f()
Generate f(k,pastdepth) when pastdepth is less than maximum pastdepth, except for OP_NEXT where pastdepth can also be the maximum.
formulaMap()
Map temporal subformulas to an integer, returns the number subformulas with temporal connectives
get_f_at_time()
Genrates a boolean expression which is true iff the ltl formula ltl_wff is true at time
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_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_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_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_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_g_at_time()
get_el_at_time()
Returns a pointer to the el(time) variable
AtMostOnce()
Creates an expression which allows at most one el_i to be true
Loop()
Creates the expression: wedge_{i=0}^{k-1} el_i => (s_i <=> s_k)
get_il_at_time()
Returns a pointer to the il(time) variable
get_loop_exists()
Returns a pointer to the le variable
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.
bmc_cache_init()
Initialises the chache used to store f_i(time) and g_(time) values.
bmc_cache_delete()
Frees the arrays used by the cache
bmc_past_depth()
Computes the maximum nesting depth of past operators in PLTL formula

sbmcUtils.c

Utilities function for SBMC package

By: Tommi Junttila, Timo Latvala, Marco Roveri

Utilities function for SBMC package

sbmc_print_node()
Print a node_ptr expression by prefixing and suffixing it.
sbmc_print_node_list()
Prints a lsList of node_ptr
sbmc_add_new_state_variable()
Declare a new boolean state variable in the layer.
sbmc_find_formula_vars()
Compute the variables that occur in the formula ltlspec.
sbmc_print_varmap()
Prints some of the information associated to a subformula
sbmc_print_Gvarmap()
Prints some of the information associated to a G formula
sbmc_print_Fvarmap()
Prints some of the information associated to a F formula
sbmc_1_fresh_state_var()
Creates a new fresh state variable.
sbmc_n_fresh_state_vars()
Creates N new fresh state variables.
sbmc_allocate_trans_vars()
Creates info->pastdepth+1 new state variables for the main translation in info->trans_vars.
sbmc_make_boolean_formula()
Takes a property and return the negation of the property conjoined with the big and of fairness conditions.
sbmc_find_relevant_vars()
Find state and input variables that occurr in the formula.
Sbmc_Utils_generate_and_print_cntexample()
Extracts a trace from a sat assignment.
sbmc_L_state()
Routines for the state indexing scheme
sbmc_E_state()
Routines for the state indexing scheme
sbmc_real_k()
Routines for the state indexing scheme
sbmc_model_k()
Routines for the state indexing scheme
sbmc_real_k_string()
Routines for the state indexing scheme
sbmc_MS_create()
Creates a meta solver wrapper
sbmc_MS_destroy()
Destroy a meta solver wrapper
sbmc_MS_create_volatile_group()
Create the volatile group in the 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_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_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_force_true()
Forces a BE to be true in the solver.
sbmc_MS_force_constraint_list()
Forces a list of BEs to be true in the solver.
sbmc_MS_solve()
Solves all groups belonging to the solver and returns the flag.
sbmc_MS_get_model()
Returns the model (of previous solving)
sbmc_add_loop_variable()
Declares a new layer to contain the loop variable.
sbmc_remove_loop_variable()
Remove the new layer to contain the loop variable.
sbmc_loop_var_name_set()
Sets the name of the loop variable.
sbmc_loop_var_name_get()
Gets the name of the loop variable.

Last updated on 2007/04/06 14h:44