Internal header file of the mc package.

void 
Check_TraceList_Sanity(
  BddEnc_ptr  enc, 
  node_ptr  path, 
  const char * varname 
)

Defined in mcExplain.c

int 
CommandCheckCompute(
  int  argc, 
  char ** argv 
)
Performs computation of quantitative characteristics

Defined in mcCmd.c

int 
CommandCheckCtlSpec(
  int  argc, 
  char ** argv 
)
Performs fair CTL model checking.

Defined in mcCmd.c

int 
CommandCheckInvar(
  int  argc, 
  char ** argv 
)
Performs model checking of invariants

Defined in mcCmd.c

int 
CommandCheckPslSpec(
  int  argc, 
  char ** argv 
)
Performs fair PSL model checking.

Defined in mcCmd.c

static int 
CommandCheckSpec(
  int  argc, 
  char ** argv 
)
Provided for backward compatibility

Defined in mcCmd.c

int 
CommandLanguageEmptiness(
  int  argc, 
  char ** argv 
)
Checks for language emptiness.

Defined in mcCmd.c

static node_ptr 
Extend_trace_with_state_input_pair(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  path, 
  bdd_ptr  starting_state, 
  bdd_ptr  next_states, 
  const char * comment 
)

Defined in mcExplain.c

static node_ptr 
Extend_trace_with_states_inputs_pair(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  path, 
  bdd_ptr  starting_states, 
  bdd_ptr  next_states, 
  const char * comment 
)

Defined in mcExplain.c

void 
Mc_CheckAGOnlySpec(
  Prop_ptr  prop 
)
The implicit assumption is that "spec" must be an AG formula (i.e. it must contain only conjunctions and AG's). No attempt is done to normalize the formula (e.g. push negations). The AG mode relies on the previous computation and storage of the reachable state space (reachable_states_layers), they are used in counterexample computation.

See Also check_spec
Defined in mcAGonly.c

void 
Mc_CheckCTLSpec(
  Prop_ptr  prop 
)
Verifies that M,s0 |= alpha using the fair CTL model checking.

Defined in mcMc.c

void 
Mc_CheckCompute(
  Prop_ptr  prop 
)
Compute the given quantitative characteristics on the model.

Defined in mcMc.c

void 
Mc_CheckInvarSilently(
  Prop_ptr  prop, 
  Trace_ptr* trace 
)
Verifies that M,s0 |= AG alpha, with alpha propositional. Uses strategy read from the option variable. If opt_counter_examples is setted and trace is not null, then a trace is stored (and must be released by caller) in trace parameter location. The result of model checking is stored in the given property.

See Also check_spec check_ltlspec Mc_CheckInvar_With_Strategy
Defined in mcInvar.c

void 
Mc_CheckInvar_With_Strategy(
  Prop_ptr  prop, 
  Check_Strategy  strategy, 
  Trace_ptr* output_trace, 
  boolean  silent 
)
Verifies that M,s0 |= AG alpha, with alpha propositional. Uses strategy given in input If opt_counter_examples is setted and trace is not null, then a trace is stored (and must be released by caller) in trace parameter location. The result of model checking is stored in the given property.

See Also check_spec check_ltlspec Mc_CheckInvar
Defined in mcInvar.c

void 
Mc_CheckInvar(
  Prop_ptr  prop 
)
Verifies that M,s0 |= AG alpha, with alpha propositional. Uses strategy read from the option variable.

See Also check_spec check_ltlspec Mc_CheckInvar_With_Strategy
Defined in mcInvar.c

void 
Mc_CheckLanguageEmptiness(
  const BddFsm_ptr  fsm, 
  boolean  allinit, 
  boolean  verbose 
)
Checks whether the language is empty. Basically just a wrapper function that calls the language emptiness algorithm given by the value of the oreg_justice_emptiness_bdd_algorithm option. If allinit is true the check is performed by verifying whether all initial states are included in the set of fair states. If it is the case from all initial states there exists a fair path and thus the language is not empty. On the other hand, if allinit is false, the check is performed by verifying whether there exists at least one initial state that is also a fair state. In this case there is an initial state from which it starts a fair path and thus the lnaguage is not empty. allinit is not supported for forward Emerson-Lei. Depending on the global option use_reachable_states the set of fair states computed can be restricted to reachable states only. In this latter case the check can be further simplified. Forward Emerson-Lei requires forward_search and use_reachable_states to be enabled. If verbose is true, then some information on the set of initial states is printed out too. verbose is ignored for forward Emerson-Lei.

Side Effects None

See Also mc_check_language_emptiness_el_bwd mc_check_language_emptiness_el_fwd
Defined in mcLE.c

void 
Mc_End(
    
)
Quit the mc package

Defined in mcCmd.c

void 
Mc_Init(
    
)
Initializes the mc package.

Defined in mcCmd.c

int 
Mc_check_psl_property(
  Prop_ptr  prop 
)
The parameters are: - prop is the PSL property to be checked

Side Effects None

Defined in mcCmd.c

Trace_ptr 
Mc_create_trace_from_bdd_state_input_list(
  const BddEnc_ptr  bdd_enc, 
  const NodeList_ptr  symbols, 
  const char* desc, 
  const TraceType  type, 
  node_ptr  path 
)
Creates a trace out of a < S (i, S)* > bdd list

Side Effects none

See Also Trace_create Bmc_create_trace_from_cnf_model
Defined in mcTrace.c

bdd_ptr 
Mc_fair_si_iteration(
  BddFsm_ptr  fsm, 
  BddStatesInputs  states, 
  BddStatesInputs  subspace 
)
Perform one iteration over the list of fairness conditions (order is statically determined). Compute states that are backward reachable from each of the fairness conditions. MAP( ApplicableStatesInputs ) over Fairness constraints (Q / ex_si ( Z / AND_i eu_si(Z, (Z/ StatesInputFC_i))))

Defined in mcMc.c

BddStatesInputs 
Mc_get_fair_si_subset(
  BddFsm_ptr  fsm, 
  BddStatesInputs  si 
)
Returns the set of state-input pairs in si that are fair, i.e. beginning of a fair path.

Defined in mcMc.c

SexpFsm_ptr 
Mc_rewrite_invar_get_sexp_fsm(
  const Prop_ptr  prop, 
  SymbLayer_ptr  layer, 
  node_ptr* created_var 
)
Returns the scalar fsm and the third argument will be filled with the name of the monitor variable

Defined in mcInvar.c

void 
Mc_trace_step_put_input_from_bdd(
  Trace_ptr  trace, 
  TraceIter  step, 
  BddEnc_ptr  bdd_enc, 
  bdd_ptr  bdd 
)
Populates a trace step with input assignments

Side Effects none

Defined in mcTrace.c

void 
Mc_trace_step_put_state_from_bdd(
  Trace_ptr  trace, 
  TraceIter  step, 
  BddEnc_ptr  bdd_enc, 
  bdd_ptr  bdd 
)
Populates a trace step with state assignments

Side Effects none

Defined in mcTrace.c

BddStates 
abu(
  BddFsm_ptr  fsm, 
  BddStates  f, 
  BddStates  g, 
  int  inf, 
  int  sup 
)
Computes the set of states satisfying A[f U^{inf..sup} g].

See Also au
Defined in mcMc.c

BddStates 
au(
  BddFsm_ptr  fsm, 
  BddStates  f, 
  BddStates  g 
)
Computes the set of states satisfying A[f U g].

See Also ax af ex ef
Defined in mcMc.c

static Step_Direction 
backward_heuristic(
  DdManager* dd, 
  bdd_ptr  reachable_frontier, 
  bdd_ptr  bad_frontier, 
  bdd_ptr  reachable_states, 
  bdd_ptr  bad_states, 
  int  turn 
)
Constant function to perform backward analysis

Defined in mcInvar.c

static bdd_ptr 
binary_bdd_op(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  BDDPFDBB  op, 
  node_ptr  n, 
  int  resflag, 
  int  argflag1, 
  int  argflag2, 
  node_ptr  context 
)
Takes in input the expression n and a binary operation op. Extracts from n the operands and evaluates them. The binary operator op is then applied to these partial results. The sign of the partial results and of the result depends respectively from the flags argflag1, argflag2 and resflag.

See Also unary_bdd_op ternary_bdd_op quaternary_bdd_op
Defined in mcEval.c

static bdd_ptr 
binary_mod_bdd_op_ns(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  BDDPFFBB  op, 
  node_ptr  n, 
  int  resflag, 
  int  argflag1, 
  int  argflag2, 
  node_ptr  context 
)
Takes in input the expression n and a binary operation op. Extracts from n the operands and evaluates them. The binary operator op is then applied to these partial results. The sign of the partial results and of the result depends respectively from the flags argflag1, argflag2 and resflag.
The only difference between this and "binary_mod_bdd_op" is that the result of the application of the operation passed as argument is not referenced. This is used for example in the "minu" and "maxu" operations.

See Also unary_bdd_op ternary_bdd_op quaternary_bdd_op
Defined in mcEval.c

static bdd_ptr 
binary_mod_bdd_op(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  BDDPFFBB  op, 
  node_ptr  n, 
  int  resflag, 
  int  argflag1, 
  int  argflag2, 
  node_ptr  context 
)
Takes in input the expression n and a binary operation op. Extracts from n the operands and evaluates them. The binary operator op is then applied to these partial results. The sign of the partial results and of the result depends respectively from the flags argflag1, argflag2 and resflag.

See Also unary_bdd_op ternary_bdd_op quaternary_bdd_op
Defined in mcEval.c

static boolean 
check_AG_only(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  Prop_ptr  prop, 
  Expr_ptr  spec, 
  node_ptr  context, 
  NodeList_ptr  symbols, 
  Trace_ptr* out_trace 
)
The implicit assumption is that "spec" must be an AG formula (i.e. it must contain only conjunctions and AG's). No attempt is done to normalize the formula (e.g. push negations). The AG mode relies on the previous computation and storage of the reachable state space (reachable_states_layers), they are used in counterexample computation. Returns true iff the property is true.

Side Effects *out_trace contains the counterexample trace (where applicable)

See Also check_spec
Defined in mcAGonly.c

int 
check_invariant_forward_backward_with_break(
  BddFsm_ptr  fsm, 
  Prop_ptr  inv_prop, 
  heuristic_type  heuristic, 
  stopping_heuristic_type  stopping_h, 
  NodeList_ptr  symbols, 
  Trace_ptr* output_trace 
)
During the computation of reachable states it checks invariants. If the invariant is not satisfied, then an execution trace leading to a state not satisfing the invariant is printed out. This function differs from check_invariant_forward since it performs backward and forward search. NOTE: returns 0 if the property is false, 1 if it is true, 2 if BMC was not able to solve the problem If opt_counter_examples is setted and trace is not null, then a trace is stored (and must be released by caller) in trace parameter location. The result of model checking is stored in the given property.

See Also check_invariant_forward
Defined in mcInvar.c

static int 
check_invariant(
  BddFsm_ptr  fsm, 
  Prop_ptr  inv_prop, 
  Check_Strategy  strategy, 
  NodeList_ptr  symbols, 
  Trace_ptr* trace 
)
If opt_counter_examples is setted and trace is not null, then a trace is stored (and must be released by caller) in trace parameter location. The result of model checking is stored in the given property.

Defined in mcInvar.c

static Trace_ptr 
complete_bmc_trace_with_bdd(
  Trace_ptr* trace, 
  NodeList_ptr  symbols, 
  BddEnc_ptr  bdd_enc, 
  BddFsm_ptr  bdd_fsm, 
  node_ptr  f_list, 
  node_ptr  b_list 
)
The free of the returned trace is demanded to the caller

Defined in mcInvar.c

static Trace_ptr 
compute_and_complete_path(
  BddFsm_ptr  fsm, 
  bdd_ptr  start_fw_state, 
  bdd_ptr  start_bw_state, 
  node_ptr  f_list, 
  node_ptr  b_list, 
  NodeList_ptr  symbols, 
  Trace_ptr* middle_trace 
)
Generates a counterexample from a path forward and a path backward completing the two parts with the specified middle trace if needed

Defined in mcInvar.c

static Trace_ptr 
compute_path_fb(
  BddFsm_ptr  fsm, 
  bdd_ptr  target_states, 
  node_ptr  f_list, 
  node_ptr  b_list, 
  NodeList_ptr  symbols 
)
Generates a counterexample from a path forward and a path backward

Defined in mcInvar.c

BddStates 
ebf(
  BddFsm_ptr  fsm, 
  BddStates  g, 
  int  inf, 
  int  sup 
)
Computes the set of states satisfying EF^{inf..sup}(g).

See Also ef
Defined in mcMc.c

node_ptr 
ebg_explain(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  path, 
  bdd_ptr  g, 
  int  inf, 
  int  sup 
)
This function finds a path of length (sup-inf) that is an example for EG(g)^{sup}_{inf}. The first element of p is the BDD that represents the first state of the path. It is an initial state from which the example has to be found.

See Also explain
Defined in mcExplain.c

BddStates 
ebg(
  BddFsm_ptr  fsm, 
  BddStates  g, 
  int  inf, 
  int  sup 
)
Computes the set of states satisfying EG^{inf..sup}(g).

See Also eg
Defined in mcMc.c

node_ptr 
ebu_explain(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  path, 
  bdd_ptr  f, 
  bdd_ptr  g, 
  int  inf, 
  int  sup 
)
This function finds a path that is a witness for E[f U g]^{sup}_{inf}. The first element of path is a BDD that represents the first state of the path. It is an initial state from which the example can be found. The procedure is to try to execute ebu(f, g, inf, sup), looking for a path, with length (sup - inf), from p to a state where g is valid using only transitions from states satisfying f.

See Also explain
Defined in mcExplain.c

BddStates 
ebu(
  BddFsm_ptr  fsm, 
  BddStates  f, 
  BddStates  g, 
  int  inf, 
  int  sup 
)
Computes the set of states satisfying E[f U^{inf..sup} g].

See Also eu
Defined in mcMc.c

BddStates 
ef(
  BddFsm_ptr  fsm, 
  BddStates  g 
)
Computes the set of states satisfying EF(g).

See Also eu ex
Defined in mcMc.c

node_ptr 
eg_explain(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  witness_path, 
  bdd_ptr  arg_g 
)
This function finds a path that is an example for EG(g). The first element p is the BDD that represents the first state of the path. It is an initial state from which the example can be found.
The procedure is based on the greatest fixed point characterization for the CTL operator EG. The CTL formula EG(g) under fairness constraints means that there exists a path beginning with current state on which g holds globally (invariantly) and each formula in the set of fairness constraints holds infinitely often on the path. If we denote with EG(g) the set of states that satisfy EG(g) under fairness constraints, we can construct the witness path incrementally by giving a sequence of prefixes of the path of increasing length until a cycle is found. At each step in the construction we must ensure that the current prefix can be extended to a fair path along which each state satisfies EG(g).

See Also explain
Defined in mcExplain.c

bdd_ptr 
eg_si(
  BddFsm_ptr  fsm, 
  bdd_ptr  g_si 
)
Set of states-inputs satisfying EG(g).

See Also eu ex
Defined in mcMc.c

BddStates 
eg(
  BddFsm_ptr  fsm, 
  BddStates  g 
)
Computes the set of states satisfying EG(g).

See Also eu ex
Defined in mcMc.c

node_ptr 
eu_explain(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  path, 
  bdd_ptr  f, 
  bdd_ptr  g 
)
This function finds a path that is a witness for E[f U g]. The first element of path is a BDD p that represents the first state of the witness path. It is an initial state from which the example can be found. The procedure is to try to execute eu(f,g) again, looking for a path from p to a state where g is valid. At each step we generate a set of states s_i that can be reached in one step from s_{i-1}. We extract one minterm form each s_i and we store it in a list.

See Also explain
Defined in mcExplain.c

node_ptr 
eu_si_explain(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  path, 
  bdd_ptr  f, 
  bdd_ptr  g_si, 
  bdd_ptr  hulk 
)
This function finds a path that is a witness for E[f U g] when g is a set of state-inputs

See Also explain
Defined in mcExplain.c

BddStatesInputs 
eu_si(
  BddFsm_ptr  fsm, 
  bdd_ptr  f, 
  bdd_ptr  g 
)
Computes the set of state-input pairs that satisfy E(f U g), with f and g sets of state-input pairs.

Defined in mcMc.c

BddStates 
eu(
  BddFsm_ptr  fsm, 
  BddStates  f, 
  BddStates  g 
)
Computes the set of states satisfying E[ f U g ].

See Also ebu
Defined in mcMc.c

static int 
eval_compute_recur(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  n, 
  node_ptr  context 
)
Performs the recursive step of eval_compute.

See Also eval_compute
Defined in mcEval.c

int 
eval_compute(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  n, 
  node_ptr  context 
)
This function performs the invocation of the routines to compute the length of the shortest and longest execution path between two set of states s_1 and s_2.

See Also eval_ctl_spec
Defined in mcEval.c

static bdd_ptr 
eval_ctl_spec_recur(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  n, 
  node_ptr  context 
)
Performs the recursive step of eval_ctl_spec.

See Also eval_ctl_spec
Defined in mcEval.c

bdd_ptr 
eval_ctl_spec(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  n, 
  node_ptr  context 
)
Compile a CTL formula into BDD and performs Model Checking.

See Also eval_compute
Defined in mcEval.c

node_ptr 
eval_formula_list(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  nodes, 
  node_ptr  context 
)
This function takes as input a list of formulae, and return as output the list of the corresponding BDDs, obtained by evaluating each formula in the given context.

Defined in mcEval.c

node_ptr 
ex_explain(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  path, 
  bdd_ptr  f 
)
This function finds a path that is a witness for EX(f). path is a BDD which represents the first state of the path. It essentially is an initial state from which the example can be found. The formula EX(f) holds under fairness constraints in a state s_i iff there is a successor state s_{i+1} such that s_{i+1} satisfies f and s_{i+1} is the beginning of some fair computation path. We look for states that can be reached from the state stored as first element in path, which are fair and in which f is satisfied. The algorithm computes more than one state, in order to have only one state we apply bdd_pick_one_state. The result of this application is then put in AND with path to form the witness.

See Also explain
Defined in mcExplain.c

BddStatesInputs 
ex_si(
  BddFsm_ptr  fsm, 
  BddStatesInputs  si 
)
Computes the set of states satisfying EG(g).

See Also eu ex ef
Defined in mcMc.c

node_ptr 
explain_and(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  path, 
  node_ptr  formula_expr, 
  node_ptr  context 
)
Generates a witness path for car(formula) AND cdr(formula)

Side Effects None

See Also explain_recur
Defined in mcExplain.c

node_ptr 
explain_eval(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  path, 
  node_ptr  formula_expr, 
  node_ptr  context 
)
optional

Side Effects required

See Also optional
Defined in mcExplain.c

static node_ptr 
explain_recur(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  path, 
  node_ptr  formula_expr, 
  node_ptr  context 
)
Recursively traverse the formula CTL and rewrite it in order to use the base witnesses generator functions.
The rewritings performed use the equivalence between CTL formulas, i.e. A[f U g] is equivalent to !(E[!g U (!g & !f)] | EG !g).

See Also explain
Defined in mcExplain.c

node_ptr 
explain(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  path, 
  node_ptr  spec_formula, 
  node_ptr  context 
)
This function takes as input a CTL formula and returns a witness showing how the given formula does not hold. The result consists of a list of states (i.e. an execution trace) that leads to a state in which the given formula does not hold.

See Also explain_recur ex_explain eu_explain eg_explain ebg_explain ebu_explain
Defined in mcExplain.c

BddStates 
ex(
  BddFsm_ptr  fsm, 
  BddStates  g 
)
Computes the set of states satisfying EX(g).

See Also eu ef eg
Defined in mcMc.c

static node_ptr 
fairness_explain(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  witness_path, 
  bdd_ptr  hulk_si, 
  JusticeList_ptr  fairness_constrainst_list 
)
In the computation of the witness for the formula EG f, at each step we must ensure that the current prefix can be extended to a fair path along which each state satisfies f. This function performs the inner fixpoint computation for each fairness constraints in the fix point computation of the formula EG(f). For every constraints h, we obtain an increasing sequence of approximations Q_0^h, Q_1^h, ..., where each Q_i^h is the set of states from which a state in the accumulated set can be reached in i or fewer steps, while satisfying f.

See Also explain eg_explain fair_iter eg
Defined in mcExplain.c

static Step_Direction 
forward_backward_heuristic(
  DdManager* dd, 
  bdd_ptr  reachable_frontier, 
  bdd_ptr  bad_frontier, 
  bdd_ptr  reachable_states, 
  bdd_ptr  bad_states, 
  int  turn 
)
Heuristic function used to decide the sept to perform in forward-backward analysis

Defined in mcInvar.c

static Step_Direction 
forward_heuristic(
  DdManager* dd, 
  bdd_ptr  reachable_frontier, 
  bdd_ptr  bad_frontier, 
  bdd_ptr  reachable_states, 
  bdd_ptr  bad_states, 
  int  turn 
)
Constant function to perform forward analysis

Defined in mcInvar.c

void 
free_formula_list(
  DdManager* dd, 
  node_ptr  formula_list 
)
Frees a list of BDD as generated by eval_formula_list

See Also eval_formula_list
Defined in mcEval.c

static boolean 
is_AG_only_formula_recur(
  node_ptr  n, 
  int* ag_count 
)
Recursive function that helps is_AG_only_formula.

See Also is_AG_only_formula
Defined in mcAGonly.c

static boolean 
is_AG_only_formula(
  node_ptr  n 
)
returns true , if the formula is AGOnly formula.

See Also is_AG_only_formula_recur
Defined in mcAGonly.c

static node_ptr 
make_AG_counterexample(
  BddFsm_ptr  fsm, 
  BddStates  target_states 
)
Compute a counterexample starting from a given state. Returned counterexample is a sequence of "state (input, state)*"

Defined in mcAGonly.c

int 
maxu(
  BddFsm_ptr  fsm, 
  bdd_ptr  f, 
  bdd_ptr  g 
)
This function computes the maximum length of the shortest path from f to g. It starts from !g and proceeds backward until no states in f can be found. In other words, it looks for the maximum length of f->AG!g. Notice that this function works correctly only if -f option is used. Returns -1 if infinity, -2 if undefined

See Also minu
Defined in mcMc.c

void 
mc_check_language_emptiness_el_bwd(
  const BddFsm_ptr  fsm, 
  boolean  allinit, 
  boolean  verbose 
)
See Mc_CheckLanguageEmptiness.

See Also BddFsm_get_fair_states
Defined in mcLE.c

void 
mc_check_language_emptiness_el_fwd(
  const BddFsm_ptr  fsm, 
  boolean  allinit, 
  boolean  verbose 
)
See Mc_CheckLanguageEmptiness.

See Also BddFsm_get_revfair_states
Defined in mcLE.c

void 
mc_rewrite_cleanup(
  Prop_ptr  rewritten_prop, 
  SymbLayer_ptr  layer 
)
Crean up the memory after the rewritten property check

Defined in mcInvar.c

Prop_ptr 
mc_rewrite_invar(
  const Prop_ptr  prop, 
  SymbLayer_ptr  layer 
)
Returns a rewrited property

Defined in mcInvar.c

int 
minu(
  BddFsm_ptr  fsm, 
  bdd_ptr  arg_f, 
  bdd_ptr  arg_g 
)
This function computes the minimum length of the shortest path from f to g.
Starts from f and proceeds forward until finds a state in g. Notice that this function works correctly only if -f option is used.

See Also maxu
Defined in mcMc.c

static boolean 
never_stopping_heuristic(
  DdManager* dd, 
  bdd_ptr  reachable_frontier, 
  bdd_ptr  bad_frontier, 
  bdd_ptr  reachable_states, 
  bdd_ptr  bad_states, 
  int  turn 
)
Constant function to perform backward, forward and FB analysis

Defined in mcInvar.c

void 
print_compute(
  FILE * file, 
  Prop_ptr  p 
)
Prints out a COMPUTE specification

Defined in mcMc.c

void 
print_invar(
  FILE * file, 
  Prop_ptr  p 
)
Print an invariant specification

Defined in mcInvar.c

static void 
print_result(
  Prop_ptr  p 
)
Print an invariant specification check result

Defined in mcInvar.c

void 
print_spec(
  FILE * file, 
  Prop_ptr  prop 
)
Prints out a CTL specification

Defined in mcMc.c

static bdd_ptr 
quad_mod_bdd_op(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  BDDPFFBBII  op, 
  node_ptr  n, 
  int  resflag, 
  int  argflag1, 
  int  argflag2, 
  node_ptr  context 
)
Takes in input the expression n and a quaternary operation op. Extracts from n the operands and evaluates them.
The third and fourth arguments have to evaluate to numbers. And op is a function that takes as input two BDD and two integers. The quaternary operator op is then applied to these partial results. The sign of the partial result and of the result depends respectively from the flags argflag1, argflag2 and resflag.

See Also unary_bdd_op binary_bdd_op ternary_bdd_op
Defined in mcEval.c

static boolean 
stopping_heuristic(
  DdManager* dd, 
  bdd_ptr  reachable_frontier, 
  bdd_ptr  bad_frontier, 
  bdd_ptr  reachable_states, 
  bdd_ptr  bad_states, 
  int  turn 
)
True means continue with BDD false means swap to BMC

Defined in mcInvar.c

static bdd_ptr 
ternary_mod_bdd_op(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  BDDPFFBII  op, 
  node_ptr  n, 
  int  resflag, 
  int  argflag, 
  node_ptr  context 
)
Takes in input the expression n and a ternary operation op. Extracts from n the operands and evaluates them.
The second and third arguments have to evaluate to numbers. And op is a function that takes as input an BDD an two integers. The ternary operator op is then applied to these partial results. The sign of the partial result and of the result depends respectively from the flags argflag and resflag.

See Also unary_bdd_op binary_bdd_op quaternary_bdd_op
Defined in mcEval.c

static bdd_ptr 
unary_bdd_op(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  BDDPFDB  op, 
  node_ptr  n, 
  int  resflag, 
  int  argflag, 
  node_ptr  context 
)
Takes in input the expression n and a unary operation op. Evaluates n and applies to this partial result the unary operator op. The sign of the partial result and of the result depends respectively from the flag argflag and resflag.

See Also binary_bdd_op ternary_bdd_op quaternary_bdd_op
Defined in mcEval.c

static bdd_ptr 
unary_mod_bdd_op(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  BDDPFFB  op, 
  node_ptr  n, 
  int  resflag, 
  int  argflag, 
  node_ptr  context 
)
Takes in input the expression n and a unary operation op. Evaluates n and applies to this partial result the unary operator op. The sign of the partial result and of the result depends respectively from the flag argflag and resflag.

See Also binary_bdd_op ternary_bdd_op quaternary_bdd_op
Defined in mcEval.c

Last updated on 2010/05/19 22h:26