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:

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.

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_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:

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