static be_ptr
AtMostOnce(
const BeEnc_ptr be_enc,
const int k
)
- Creates an expression which allows at most one el_i to
be true
- See Also
get_el_at_time
- Defined in
sbmcTableauLTLformula.c
be_ptr
BmcInt_SBMCTableau_GetAtTime(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
const int time,
const int k,
const int l
)
- The function generates the necessary auxilliary
predicates (loop, atmostonce) and calls on
get_f_at_time to generate the tableau for the ltl
formula.
- See Also
AtMostOnce
Loop
get_f_at_time
- Defined in
sbmcTableauLTLformula.c
be_ptr
Bmc_Gen_SBMCProblem(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k,
const int l
)
- Returns the LTL problem at length k with loopback l
(single loop, no loop and all loopbacks are allowed)
- Defined in
sbmcGen.c
void
Bmc_Hash_delete_table(
hashPtr hash
)
- Delete the table
- Side Effects None
- Defined in
sbmcHash.c
int
Bmc_Hash_find(
hashPtr table,
node_ptr node
)
- Find a node in the table. Return BMC_HASH_NOTFOUND if the
node is not present
- Side Effects None
- Defined in
sbmcHash.c
void
Bmc_Hash_insert(
hashPtr table,
node_ptr key,
int data
)
- Insert an element in the table
- Side Effects None
- Defined in
sbmcHash.c
hashPtr
Bmc_Hash_new_htable(
)
- Create a new hash_table
- Side Effects None
- Defined in
sbmcHash.c
unsigned
Bmc_Hash_size(
hashPtr hash
)
- Return the number of occupied slots
- Side Effects None
- Defined in
sbmcHash.c
int
Bmc_SBMCGenSolveLtl(
Prop_ptr ltlprop,
const int k,
const int relative_loop,
const boolean must_inc_length,
const boolean must_solve,
const Bmc_DumpType dump_type,
const char* dump_fname_template
)
- 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
- See Also
Bmc_GenSolve_Action
- Defined in
sbmcBmc.c
be_ptr
Bmc_SBMCTableau_GetAllLoops(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k,
const int l
)
- Fairness is taken care of by adding it to the formula.
- Defined in
sbmcTableau.c
be_ptr
Bmc_SBMCTableau_GetLoopCondition(
const BeEnc_ptr be_enc,
const int k,
const int l
)
- State l and state k are forced to represent the same
state by conjuncting the if-and-only-if conditions
{Vil<->Vik} between Vil (variable i at time l) and Vik
(variable i at time k) for each variable Vi.
- See Also
Bmc_Tableau_GetAllLoopsDisjunction
- Defined in
sbmcTableau.c
be_ptr
Bmc_SBMCTableau_GetNoLoop(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k
)
- Fairness is ignored
- Defined in
sbmcTableau.c
be_ptr
Bmc_SBMCTableau_GetSingleLoop(
const BeFsm_ptr be_fsm,
const node_ptr ltl_wff,
const int k,
const int l
)
- Builds tableau for a single loop. This function takes
into account of fairness
- Defined in
sbmcTableau.c
void
Bmc_Stack_delete(
Bmc_Stack_ptr thestack
)
- Delete the stack
- Side Effects None
- Defined in
sbmcNodeStack.c
Bmc_Stack_ptr
Bmc_Stack_new_stack(
)
- Create a new stack
- Side Effects None
- Defined in
sbmcNodeStack.c
node_ptr
Bmc_Stack_pop(
Bmc_Stack_ptr thestack
)
- Pop an element from the stack
- Side Effects None
- Defined in
sbmcNodeStack.c
void
Bmc_Stack_push(
Bmc_Stack_ptr thestack,
node_ptr node
)
- Push a node unto the stack
- Side Effects None
- Defined in
sbmcNodeStack.c
unsigned
Bmc_Stack_size(
Bmc_Stack_ptr thestack
)
- Return the number of occupied slots
- Side Effects None
- Defined in
sbmcNodeStack.c
node_ptr
Bmc_Stack_top(
Bmc_Stack_ptr thestack
)
- Return the top element of the stack
- Side Effects None
- Defined in
sbmcNodeStack.c
static be_ptr
Loop(
const BeEnc_ptr be_enc,
const int k
)
- The expression when coupled with AtMostOnce forces
state i to be equivalent with state k, if el_i
is true.
SideEffects [
- Defined in
sbmcTableauLTLformula.c
void
SBmc_AddCmd(
)
- Adds all bmc-related commands to the interactive shell
- See Also
Sm_Init
- Defined in
sbmcPkg.c
void
SBmc_Init(
)
- Initializes the SBMC sub package
- Defined in
sbmcPkg.c
void
SBmc_Quit(
)
- Frees all resources allocated for the SBMC model manager
- Defined in
sbmcPkg.c
int
Sbmc_CommandCheckLtlSpecSBmc(
int argc,
char** argv
)
- Model check using sbmc
- Side Effects None
- Defined in
sbmcCmd.c
int
Sbmc_CommandGenLtlSpecSBmc(
int argc,
char** argv
)
- Each problem is dumped for the given LTL specification,
or for all LTL specifications if no formula is given.
Generation parameters are the maximum bound and the loopback values.
After command line processing it calls the function Bmc_SBMCGenSolveLtl
to generate and dump all problems from zero to k.Uses Kepa's and Timo's method for doing bmc
- Side Effects None
- Defined in
sbmcCmd.c
int
Sbmc_CommandLTLCheckZigzagInc(
int argc,
char** argv
)
- 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.
- Side Effects required
- See Also
optional
- Defined in
sbmcCmd.c
Trace_ptr
Sbmc_Utils_generate_and_print_cntexample(
BeEnc_ptr be_enc,
sbmc_MetaSolver * solver,
BddEnc_ptr bdd_enc,
node_ptr l_var,
const int k,
const char * trace_name
)
- Extracts a trace from a sat assignment.
- Side Effects None
- See Also
Bmc_Utils_generate_and_print_cntexample
- Defined in
sbmcUtils.c
int
Sbmc_check_psl_property(
Prop_ptr prop,
boolean dump_prob,
boolean inc_sat,
boolean do_completeness_check,
boolean do_virtual_unrolling,
boolean single_prob,
int k,
int rel_loop
)
- The parameters are:
- prop is the PSL property to be checked
- dump_prob is true if the problem must be dumped as DIMACS file (default filename
from system corresponding variable)
- inc_sat is true if incremental sat must be used. If there is no
support for inc sat, an internal error will occur.
- single_prob is true if k must be not incremented from 0 to k_max
(single problem)
- k and rel_loop are the bmc parameters.
- Side Effects None
- Defined in
sbmcCmd.c
static be_ptr
bmcSBMC_tableau_GF_FG_last(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
const int k,
const int l,
const unsigned pastdepth,
hashPtr table
)
- Checks if the il-optimisation is enabled and generates
f(k) accordingly
- See Also
bmc_tableau_GetEventuallyIL_opt
bmc_tableau_GetGloballyIL_opt
- Defined in
sbmcTableauLTLformula.c
static void
bmc_cache_delete(
)
- Frees the arrays used by the cache
- See Also
bmc_init_cache
- Defined in
sbmcTableauLTLformula.c
static void
bmc_cache_init(
const int count,
const int k,
const unsigned pastdepth
)
- The function allocates an array of size (k+1)*count for
both f and g. The array is used to cache values
of f_i(time) and g_i(time). Only values for
temporal formulas are stored.
- See Also
bmc_delete_cache
- Defined in
sbmcTableauLTLformula.c
static void
bmc_expandFilename(
const int k,
const int l,
const int prop_idx,
const char* filename_to_be_expanded,
char* filename_expanded,
const size_t filename_expanded_maxlen
)
- This is only a useful wrapper for easily call
Bmc_Utils_ExpandMacrosInFilename
- Side Effects None
- Defined in
sbmcBmc.c
static node_ptr
bmc_get_fairness(
const int l
)
- Builds AND_i G F fc_i
- Side Effects None
- Defined in
sbmcTableau.c
static unsigned
bmc_past_depth(
const node_ptr ltl_wff
)
- Computes the maximum nesting depth of past operators in PLTL formula
- Defined in
sbmcTableauLTLformula.c
static be_ptr
bmc_tableauGetEventuallyIL_opt(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
const int k,
const int l,
const unsigned pastdepth,
hashPtr table
)
- Creates the expression f(k+1):=vee_{i=1}^k il(i)wedge
f1(i)
- Defined in
sbmcTableauLTLformula.c
static be_ptr
bmc_tableauGetGloballyIL_opt(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
const int k,
const int l,
const unsigned pastdepth,
hashPtr table
)
- Creates the expression f(k+1):=lewedge wedge_{i=1}^k neg il(i)vee f1(i)
- Defined in
sbmcTableauLTLformula.c
static int
find(
hashPtr table,
node_ptr node
)
- Return index of node, a free index if the node is not in the table
- Side Effects None
- Defined in
sbmcHash.c
static int
formulaMap(
hashPtr table,
const node_ptr ltl_wff,
unsigned TLcount
)
- Stores the nodes of the ltl expression in a table and
maps each formula to an integer. Temporal
subformulas are numbered from 0...N while all
other subformulas are mapped to -2
- Defined in
sbmcTableauLTLformula.c
static be_ptr
get_Eventually_at_time(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
hashPtr table,
const int time,
const int k,
const int l,
const unsigned pastdepth
)
- The function recursively traverses the formula and genrates
the needed boolean expression.
- See Also
get_f_at_time
get_g_at_time
- Defined in
sbmcTableauLTLformula.c
static be_ptr
get_Globally_at_time(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
hashPtr table,
const int time,
const int k,
const int l,
const unsigned pastdepth
)
- The function recursively traverses the formula and
generates the needed boolean expression.
- See Also
get_f_at_time
get_g_at_time
- Defined in
sbmcTableauLTLformula.c
static be_ptr
get_Historically_at_time(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
hashPtr table,
const int time,
const int k,
const int l,
const unsigned pastdepth
)
- The function recursively traverses the formula and genrates
the needed boolean expression.
- See Also
get_f_at_time
get_g_at_time
- Defined in
sbmcTableauLTLformula.c
static be_ptr
get_Once_at_time(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
hashPtr table,
const int time,
const int k,
const int l,
const unsigned pastdepth
)
- The function recursively traverses the formula and genrates
the needed boolean expression.
- See Also
get_f_at_time
get_g_at_time
- Defined in
sbmcTableauLTLformula.c
static be_ptr
get_Since_at_time(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
hashPtr table,
const int time,
const int k,
const int l,
const unsigned pastdepth
)
- The function recursively traverses the formula and
genrates the needed boolean expression.
- See Also
get_f_at_time
get_g_at_time
- Defined in
sbmcTableauLTLformula.c
static be_ptr
get_Trigger_at_time(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
hashPtr table,
const int time,
const int k,
const int l,
const unsigned pastdepth
)
- The function recursively traverses the formula and
genrates the needed boolean expression.
- See Also
get_f_at_time
get_g_at_time
- Defined in
sbmcTableauLTLformula.c
static be_ptr
get_Until_at_time(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
hashPtr table,
const int time,
const int k,
const int l,
const unsigned pastdepth
)
- The function recursively traverses the formula and genrates
the needed boolean expression.
- See Also
get_f_at_time
get_g_at_time
- Defined in
sbmcTableauLTLformula.c
static be_ptr
get_V_at_time(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
hashPtr table,
const int time,
const int k,
const int l,
const unsigned pastdepth
)
- The function recursively traverses the formula and
genrates the needed boolean expression.
- See Also
get_f_at_time
get_g_at_time
- Defined in
sbmcTableauLTLformula.c
static be_ptr
get_el_at_time(
const BeEnc_ptr be_enc,
const int time,
const int k
)
- The variables el(time) describe if the state s_time
should be equivalent with s_k
- Defined in
sbmcTableauLTLformula.c
static be_ptr
get_f_at_time(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
hashPtr table,
const int time,
const int k,
const int l,
const unsigned pastdepth
)
- The function recursively traverses the formula and genrates
the needed boolean expression.
- See Also
get_g_at_time
- Defined in
sbmcTableauLTLformula.c
static be_ptr
get_g_at_time(
const BeEnc_ptr be_enc,
const node_ptr ltl_wff,
hashPtr table,
const int time,
const int k,
const int l,
const unsigned pastdepth
)
- Returns a pointer to the g_i(time) variable
- Defined in
sbmcTableauLTLformula.c
static be_ptr
get_il_at_time(
const BeEnc_ptr be_enc,
const int time,
const int k
)
- The il(i) variable describes if the state 'i' is a
a state of the loop.
- Defined in
sbmcTableauLTLformula.c
static be_ptr
get_loop_exists(
const BeEnc_ptr be_enc,
const int k
)
- The le variable is true if a loop exists.
- Defined in
sbmcTableauLTLformula.c
static be_ptr
last_f(
const BeEnc_ptr be_enc,
node_ptr ltl_wff,
hashPtr table,
const int l,
const int k,
const unsigned pastdepth
)
- The function checks which loop setting is active
and genrates f(k) accordingly.
- Defined in
sbmcTableauLTLformula.c
static be_ptr
last_g(
const BeEnc_ptr be_enc,
node_ptr ltl_wff,
hashPtr table,
const int l,
const int k,
const unsigned pastdepth
)
- The function checks which loop setting is active
and genrates f(k) accordingly.
- Defined in
sbmcTableauLTLformula.c
node_ptr
sbmc_1_fresh_state_var(
SymbLayer_ptr layer,
unsigned int * index
)
- Creates a new fresh state variable. The name is
according to the pattern #LTL_t%u, being %u an unsigned integer. The
index is incremented by one.
- Side Effects index is incremented by one.
- Defined in
sbmcUtils.c
int
sbmc_E_state(
)
- State 1 is the E state
- Side Effects None
- See Also
sbmc_L_state
sbmc_real_k
sbmc_model_k
sbmc_real_k_string
- Defined in
sbmcUtils.c
int
sbmc_L_state(
)
- State 0 is the L state
- Side Effects None
- See Also
sbmc_E_state
sbmc_real_k
sbmc_model_k
sbmc_real_k_string
- Defined in
sbmcUtils.c
void
sbmc_MS_create_volatile_group(
sbmc_MetaSolver * ms
)
- Create the volatile group in the meta solver wrapper. Use
of the volatile group is not forced
- Side Effects None
- Defined in
sbmcUtils.c
sbmc_MetaSolver *
sbmc_MS_create(
BeEnc_ptr be_enc
)
- Creates a meta solver wrapper
- Side Effects None
- Defined in
sbmcUtils.c
void
sbmc_MS_destroy_volatile_group(
sbmc_MetaSolver * ms
)
- Destroy the volatile group of the meta solver wrapper and
force use of the permanent one
- Side Effects None
- Defined in
sbmcUtils.c
void
sbmc_MS_destroy(
sbmc_MetaSolver * ms
)
- Destroy a meta solver wrapper
- Side Effects None
- Defined in
sbmcUtils.c
void
sbmc_MS_force_constraint_list(
sbmc_MetaSolver * ms,
lsList constraints
)
- Forces a list of BEs to be true in the
solver. Each is converted to CNF, the CNF is then forced in the
group in use, i.e. in the permanent or in the volatile group.
- Side Effects None
- See Also
sbmc_MS_force_true
- Defined in
sbmcUtils.c
void
sbmc_MS_force_true(
sbmc_MetaSolver * ms,
be_ptr be_constraint
)
- Forces a BE to be true in the solver. The BE
converted to CNF, the CNF is then forced in the group in use,
i.e. in the permanent or in the volatile group.
- Side Effects None
- Defined in
sbmcUtils.c
lsList
sbmc_MS_get_model(
sbmc_MetaSolver * ms
)
- The previous solving call should have returned SATISFIABLE.
The returned list is a list of values in dimac form (positive literal
is included as the variable index, negative literal as the negative
variable index, if a literal has not been set its value is not included).
Returned list must be NOT destroyed.
- Defined in
sbmcUtils.c
void
sbmc_MS_goto_permanent_group(
sbmc_MetaSolver * ms
)
- Destroy the volatile group of the meta solver
wrapper, thus only considering the permanent group.
- Side Effects None
- Defined in
sbmcUtils.c
void
sbmc_MS_goto_volatile_group(
sbmc_MetaSolver * ms
)
- Create and force use of the volatile group of
the meta solver wrapper.
- Side Effects None
- Defined in
sbmcUtils.c
SatSolverResult
sbmc_MS_solve(
sbmc_MetaSolver * ms
)
- Solves all groups belonging to the solver and
returns the flag.
- Side Effects None
- See Also
SatSolver_solve_all_groups
- Defined in
sbmcUtils.c
void
sbmc_MS_switch_to_permanent_group(
sbmc_MetaSolver * ms
)
- Force use of the permanent group of
the meta solver wrapper. Volatile group is left in place, if existing
- Side Effects None
- Defined in
sbmcUtils.c
void
sbmc_MS_switch_to_volatile_group(
sbmc_MetaSolver * ms
)
- Force use of the volatile group of
the meta solver wrapper. The volatile group must have been previously
created
- Side Effects None
- Defined in
sbmcUtils.c
lsList
sbmc_SimplePaths(
const BeEnc_ptr be_enc,
const state_vars_struct * state_vars,
array_t * InLoop_array,
const unsigned int k
)
- Build SimplePath_{i,k} for each 0<=i
- Side Effects None
- Defined in
sbmcTableauInc.c
void
sbmc_add_loop_variable(
BeFsm_ptr be_fsm
)
- Declares a new layer to contain the loop variable.
- Defined in
sbmcUtils.c
node_ptr
sbmc_add_new_state_variable(
SymbLayer_ptr layer,
char * name
)
- Declare a new boolean state variable in the
layer. The name is specified as a string. If the variable already
exists, then an error is generated.
- Side Effects None
- Defined in
sbmcUtils.c
sbmc_node_info *
sbmc_alloc_node_info(
)
- Creates an empty structure to hold information
associated to each subformula.
- Side Effects None
- Defined in
sbmcStructs.c
void
sbmc_allocate_trans_vars(
sbmc_node_info * info,
SymbLayer_ptr layer,
lsList state_vars_formula_pd0,
lsList state_vars_formula_pdx,
unsigned int* new_var_index
)
- Creates info->pastdepth+1 new state variables
for the main translation in info->trans_vars. state_vars_formula_pd0,
state_vars_formula_pdx and new_var_index are updated accordingly.
- Side Effects new_var_index is incremented accordingly to the
number of variables created. state_vars_formula_pd0,
state_vars_formula_pdx and new_var_index are updated accordingly.
- Defined in
sbmcUtils.c
be_ptr
sbmc_build_InLoop_i(
const BeEnc_ptr be_enc,
const state_vars_struct * state_vars,
array_t * InLoop_array,
const unsigned int i_model
)
- Build InLoop_i stuff
Define InLoop_i = (InLoop_{i-1} || l_i)
Returns the BE constraint InLoop_{i-1} => !l_i (or 0 when i=0)
- Side Effects None
- Defined in
sbmcTableauInc.c
static outcome
sbmc_cmd_options_handling(
int argc,
char** argv,
Prop_Type prop_type,
Prop_ptr* res_prop,
int* res_k,
int* res_l,
char** res_o,
boolean* res_N,
boolean* res_c,
boolean* res_1
)
- Output variables called res_* are pointers to
variables that will be changed if the user specified a value for the
corresponding option. For example if the user specified "-k 2", then
*res_k will be assigned to 2. The caller can selectively choose which
options can be specified by the user, by passing either a valid pointer
as output parameter, or NULL to disable the corresponding option.
For example by passing NULL as actual parameter of res_l, option -l will
be not accepted.
If both specified, k and l will be checked for mutual consistency.
Loop will contain a relative value, like the one the user specified.
prop_type is the expected property type, if specified.
All integers values will not be changed if the corresponding options
had not be specified by the user, so the caller might assign them to
default values before calling this function.
All strings will be allocated by the function if the corresponding
options had been used by the user. In this case it is responsability
of the caller to free them. Strings will be assigned to NULL if the
user had not specified any corresponding option.
Returns GENERIC_ERROR if an error has occurred;
Returns SUCCESS_REQUIRED_HELP if -h options had been specified;
Returns SUCCESS in all other cases.
- Side Effects Result parameters might change
- Defined in
sbmcCmd.c
lsList
sbmc_dependent(
const BeEnc_ptr be_enc,
const node_ptr bltlspec,
const int k,
const state_vars_struct * state_vars,
array_t * InLoop_array,
const be_ptr be_LoopExists,
const hash_ptr info_map
)
- Creates several constraints:
- Create the constraint l_{k+1} <=> FALSE
- Create the constraint s_E = s_k
- Create the constraint LoopExists <=> InLoop_k
- Create the formula specific k-dependent constraints
- Side Effects None
- Defined in
sbmcTableauIncLTLformula.c
be_ptr
sbmc_equal_vectors_formula(
const BeEnc_ptr be_enc,
lsList vars,
const unsigned int i,
const unsigned int j
)
- Creates the BE for the formula "land_{v in vars} s_i = s_j"
- Side Effects None
- Defined in
sbmcTableauInc.c
lsList
sbmc_find_formula_vars(
node_ptr ltlspec
)
- Compute the variables that occur in the formula ltlspec.
The formula ltlspec must be in NNF.
- Side Effects None
- Defined in
sbmcUtils.c
void
sbmc_find_relevant_vars(
state_vars_struct * svs,
BeFsm_ptr be_fsm,
node_ptr bltlspec
)
- Find state and input variables that occurr in the formula.
Build the list of system variables for simple path constraints.
- state_vars->formula_state_vars will have the state vars occurring
in the formula bltlspec
- state_vars->formula_input_vars will have the input vars occurring
in the formula bltlspec
- state_vars->simple_path_system_vars will be the union of
state_vars->transition_state_vars,
state_vars->formula_state_vars, and
state_vars->formula_input_vars
- Side Effects svs is modified to store retrieved information.
- Defined in
sbmcUtils.c
lsList
sbmc_formula_dependent(
const BeEnc_ptr be_enc,
const node_ptr ltlspec,
const unsigned int k_model,
const hash_ptr info_map
)
- Create the formula specific k-dependent constraints.
Return a list of be_ptrs for the created constraints.
- Side Effects None
- Defined in
sbmcTableauIncLTLformula.c
hash_ptr
sbmc_init_LTL_info(
SymbLayer_ptr layer,
node_ptr ltlspec,
lsList state_vars_formula_pd0,
lsList state_vars_formula_pdx,
lsList state_vars_formula_aux,
const int opt_force_state_vars,
const int opt_do_virtual_unrolling
)
- Associates each subformula node of ltlspec with
a sbmc_LTL_info. Returns a hash from node_ptr to sbmc_LTL_info*.
New state variables named #LTL_t'i' can be allocate to 'layer'.
The new state vars are inserted in state_vars_formula_??? appropriately.
- Side Effects None
- Defined in
sbmcTableauInc.c
void
sbmc_init_state_vector(
const BeEnc_ptr be_enc,
const node_ptr ltlspec,
const hash_ptr info_map,
const unsigned int i_real,
const node_ptr LastState_var,
const be_ptr be_LoopExists
)
- Initialize trans_bes[i
- Side Effects None
- Defined in
sbmcTableauInc.c
node_ptr
sbmc_loop_var_name_get(
)
- Gets the name of the loop variable.
- Defined in
sbmcUtils.c
void
sbmc_loop_var_name_set(
node_ptr n
)
- Sets the name of the loop variable.
- Defined in
sbmcUtils.c
node_ptr
sbmc_make_boolean_formula(
Prop_ptr ltlprop
)
- Takes a property and return the negation of the
property conjoined with the big and of fairness conditions.
- Side Effects None
- Defined in
sbmcUtils.c
unsigned int
sbmc_model_k(
int k
)
- Given a real k return the corresponding model k (real - 2)
- Side Effects None
- See Also
sbmc_L_state
sbmc_E_state
sbmc_real_k
sbmc_real_k_string
- Defined in
sbmcUtils.c
array_t *
sbmc_n_fresh_state_vars(
SymbLayer_ptr layer,
const unsigned int n,
unsigned int * index
)
- Creates N new fresh state variables. The name is
according to the pattern #LTL_t%u, being %u an unsigned integer. The
index is incremented by N. The new variables are stroed into an
array of node_ptr
- Side Effects index is incremented by N.
- Defined in
sbmcUtils.c
hash_ptr
sbmc_node_info_assoc_create(
)
- Creates an asociative list for pairs node_ptr
sbmc_node_info *
- Side Effects None
- Defined in
sbmcStructs.c
sbmc_node_info *
sbmc_node_info_assoc_find(
hash_ptr a,
node_ptr n
)
- Return the information associated to a
subformula if any.
- Side Effects None
- Defined in
sbmcStructs.c
void
sbmc_node_info_assoc_free(
hash_ptr * a
)
- Creates an asociative list for pairs node_ptr
sbmc_node_info *
- Side Effects None
- Defined in
sbmcStructs.c
void
sbmc_node_info_assoc_insert(
hash_ptr a,
node_ptr n,
sbmc_node_info * i
)
- Insert in the assoc table the infomrnation for
the subformula.
- Side Effects None
- Defined in
sbmcStructs.c
void
sbmc_node_info_free(
sbmc_node_info * info
)
- Frees a structure to hold information
associated to each subformula.
- Side Effects None
- Defined in
sbmcStructs.c
void
sbmc_print_Fvarmap(
FILE * out,
node_ptr var,
node_ptr formula
)
- Prints some of the information associated to a F
formula.
- Side Effects None
- Defined in
sbmcUtils.c
void
sbmc_print_Gvarmap(
FILE * out,
node_ptr var,
node_ptr formula
)
- Prints some of the information associated to a G
formula.
- Side Effects None
- Defined in
sbmcUtils.c
void
sbmc_print_node_list(
FILE * out,
lsList l
)
- Prints a lsList of node_ptr in a file stream.
- Side Effects None
- Defined in
sbmcUtils.c
void
sbmc_print_node(
FILE * out,
const char * prefix,
node_ptr node,
const char * postfix
)
- Prints a node_ptr expression in a file stream by
prefixing and suffixing it with a string. If the prefix and suffix
strings are NULL they are not printed out.
- Side Effects None
- Defined in
sbmcUtils.c
void
sbmc_print_varmap(
FILE * out,
node_ptr node,
sbmc_node_info * info
)
- Prints some of the information associated to a
subformula.
- Side Effects None
- Defined in
sbmcUtils.c
char*
sbmc_real_k_string(
const unsigned int k_real
)
- Returns a string correspondingg to the state considered. E, L, Real
- Side Effects The returned value must be freed
- See Also
sbmc_L_state
sbmc_E_state
sbmc_real_k
sbmc_model_k
- Defined in
sbmcUtils.c
int
sbmc_real_k(
int k
)
- The first real state is 2
- Side Effects None
- See Also
sbmc_L_state
sbmc_E_state
sbmc_model_k
sbmc_real_k_string
- Defined in
sbmcUtils.c
void
sbmc_remove_loop_variable(
BeFsm_ptr be_fsm
)
- Remove the new layer to contain the loop variable.
- Defined in
sbmcUtils.c
hash_ptr
sbmc_set_create(
)
- An associtative list to avoid duplicates of
node_ptr. If a node is in this set, it has a constant 1 associated
to it in the associative hash.
- Side Effects None
- Defined in
sbmcStructs.c
void
sbmc_set_destroy(
hash_ptr hash
)
- Destroy an associative list used to avoid
duplicates of node_ptr.
- Side Effects None
- Defined in
sbmcStructs.c
void
sbmc_set_insert(
hash_ptr hash,
node_ptr bexp
)
- Insert a node in the hash associating constant 1
- Side Effects None
- Defined in
sbmcStructs.c
int
sbmc_set_is_in(
hash_ptr hash,
node_ptr bexp
)
- Checks whether a node_ptr was already
inserted. In affermative case return 1, else 0.
- Side Effects None
- Defined in
sbmcStructs.c
state_vars_struct*
sbmc_state_vars_create(
)
- Creates an empty state_vars_struct
- Side Effects None
- Defined in
sbmcStructs.c
void
sbmc_state_vars_destroy(
state_vars_struct* svs
)
- state_vars_struct destroyer
- Side Effects None
- Defined in
sbmcStructs.c
void
sbmc_state_vars_print(
state_vars_struct * svs,
FILE* out
)
- Print a state_vars_struct to 'out'
- Side Effects None
- Defined in
sbmcStructs.c
lsList
sbmc_unroll_base(
const BeEnc_ptr be_enc,
const node_ptr ltlspec,
const hash_ptr info_map,
const be_ptr be_LoopExists,
const int do_optimization
)
- Create the BASE constraints.
Return a list of be_ptr for the created constraints.
Create the following constraints:
- !LoopExists => ([[f
- Side Effects None
- Defined in
sbmcTableauIncLTLformula.c
static lsList
sbmc_unroll_invariant_f(
const BeEnc_ptr be_enc,
const node_ptr ltlspec,
const unsigned int i_model,
const hash_ptr info_map,
const be_ptr be_InLoop_i,
const be_ptr be_l_i,
const be_ptr be_LastState_i,
const be_ptr be_LoopExists,
const int do_optimization
)
- Create the k-invariant constraints for propositional and
future temporal operators at time i. Return a list of be_ptrs for the
created constraints.
- Side Effects None
- Defined in
sbmcTableauIncLTLformula.c
lsList
sbmc_unroll_invariant_propositional(
const BeEnc_ptr be_enc,
const node_ptr ltlspec,
const unsigned int i_model,
const hash_ptr info_map,
const be_ptr be_InLoop_i,
const be_ptr be_l_i,
const int do_optimization
)
- Create the k-invariant constraints for
propositional operators at time i. Return a list of be_ptrs for the
created constraints.
- Side Effects None
- Defined in
sbmcTableauIncLTLformula.c
static lsList
sbmc_unroll_invariant_p(
const BeEnc_ptr be_enc,
const node_ptr ltlspec,
const unsigned int i_model,
const hash_ptr info_map,
const be_ptr be_InLoop_i,
const be_ptr be_l_i,
const int do_optimization
)
- Create the k-invariant constraints at time
i. Return a list of be_ptrs for the created constraints.
- Side Effects None
- Defined in
sbmcTableauIncLTLformula.c
lsList
sbmc_unroll_invariant(
const BeEnc_ptr be_enc,
const node_ptr bltlspec,
const int previous_k,
const int new_k,
const state_vars_struct * state_vars,
array_t * InLoop_array,
const hash_ptr info_map,
const be_ptr be_LoopExists,
const int opt_do_optimization
)
- Unroll future and past fragment from previous_k+1
upto and including new_k. Return a list of constraints.
- Side Effects None
- Defined in
sbmcTableauIncLTLformula.c