
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
Usercommands 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. 380395, Springer, 2005. Copyright ©
SpringerVerlag.

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
Usercommands 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. 98111, Springer, 2005.
Copyright © SpringerVerlag.
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 021111307 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 highlevel 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()
 Toplevel 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 bmcrelated 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 tableaurelated 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 (kl)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 kinvariant constraints for
propositional operators at time i.

sbmc_unroll_invariant_f()
 Create the kinvariant constraints for propositional and
future temporal operators at time i.

sbmc_unroll_invariant_p()
 Create the kinvariant constraints at time i.

sbmc_formula_dependent()
 Create the formula specific kdependent 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 modelindependent
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 Goperator

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}^{k1} 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 iloptimisation.

bmc_tableauGetGloballyIL_opt()
 Returns an expression which initialises f(k+1) for
a 'globally' or an FG formula when we use the iloptimisation.

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