-
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
-
sbmcStructs.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
sbmcStructs.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.
-
sbmc_state_vars_create()
- Creates an empty state_vars_struct
-
sbmc_state_vars_destroy()
- state_vars_struct destroyer
-
sbmc_state_vars_get_trans_state_vars()
- getter for field "trans_state_vars"
-
sbmc_state_vars_get_l_var()
- getter for field "l_var"
-
sbmc_state_vars_get_LoopExists_var()
- getter for field "LoopExists_var"
-
sbmc_state_vars_get_LastState_var()
- getter for field "LastState_var"
-
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_get_translation_vars_aux()
- getter for field "translation_vars_aux"
-
sbmc_state_vars_get_formula_state_vars()
- getter for field "formula_state_vars"
-
sbmc_state_vars_get_formula_input_vars()
- getter for field "formula_input_vars"
-
sbmc_state_vars_get_simple_path_system_vars()
- getter for field "simple_path_system_vars"
-
sbmc_state_vars_set_trans_state_vars()
- setter for field "transition_state_vars"
-
sbmc_state_vars_set_l_var()
- setter for field "l_var"
-
sbmc_state_vars_set_LoopExists_var()
- setter for field "LoopExists_var"
-
sbmc_state_vars_set_LastState_var()
- setter for field "LastState_var"
-
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_state_vars_set_translation_vars_aux()
- setter for field "translation_vars_aux"
-
sbmc_state_vars_set_formula_state_vars()
- setter for field "formula_state_vars"
-
sbmc_state_vars_set_formula_input_vars()
- setter for field "formula_input_vars"
-
sbmc_state_vars_set_simple_path_system_vars()
- setter for field "simple_path_system_vars"
-
sbmc_state_vars_print()
- Print a state_vars_struct
-
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_alloc_node_info()
- Creates an empty structure to hold information
associated to each subformula.
-
sbmc_node_info_free()
- Frees a structure to hold information
associated to each subformula.
-
sbmc_node_info_assoc_create()
- Creates an asociative list for pairs node_ptr
sbmc_node_info *
-
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_assoc_find()
- Return the information associated to a
subformula if any.
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).
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, and prints it.
-
Sbmc_Utils_generate_cntexample()
- Extracts a trace from a sat assignment.
-
Sbmc_Utils_fill_cntexample()
- Fills the given trace using the given 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_solve_assume()
- Solves all groups belonging to the solver assuming
the CNF assumptions and returns the flag.
-
sbmc_MS_get_solver()
- Returns the underlying solver
-
sbmc_MS_get_conflicts()
- Returns the underlying solver
-
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 2012/11/18 14h:16