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_CheckInvar(
  Prop_ptr  prop 
)
Verifies that M,s0 |= AG alpha, with alpha propositional.

See Also check_spec check_ltlspec
Defined in mcInvar.c

void 
Mc_CheckLanguageEmptiness(
  const BddFsm_ptr  fsm, 
  boolean  allinit, 
  boolean  verbose 
)
Checks whether the language is empty. 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. 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. if verbose is true, then some information on the set of initial states is printed out too.

Side Effects None

See Also BddFsm_get_fair_states
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

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

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

Trace_ptr 
check_AG_only(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  Prop_ptr  prop, 
  Expr_ptr  spec, 
  node_ptr  context 
)
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 
check_invariant_forward_backward(
  Fsm_BddPtr  fsm, 
  Expr_ptr  inv_expr 
)
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.

See Also check_invariant_forward
Defined in mcInvar.c

int 
check_invariant_forward(
  BddFsm_ptr  fsm, 
  Prop_ptr  inv_prop 
)
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. Returns 1 if the property is found true, 0 otherwise

See Also check_invariant_forward_opt
Defined in mcInvar.c

int 
compute_and_print_path_fb(
  BddFsm_ptr  fsm, 
  bdd_ptr  target_states, 
  bdd_ptr  f_target, 
  node_ptr  f_plan_reach_list, 
  int  f_step, 
  bdd_ptr  b_target, 
  node_ptr  b_plan_reach_list, 
  int  b_step 
)

Defined in mcInvar.c

int 
compute_and_print_path(
  BddFsm_ptr  fsm, 
  bdd_ptr  reached_goal_bdd, 
  node_ptr  path_slices, 
  int  nstep, 
  int  flag 
)
Extracts a counterexample that leads to a state not satisfying the invariant AG alpha. The counterexample produced is the shortest execution trace that exploits the falsity of the invariant. The computed counterexample is printed out.

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

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

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

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

void 
print_compute(
  FILE * file, 
  node_ptr  n 
)
Prints out a COMPUTE specification

Defined in mcMc.c

void 
print_invar(
  FILE * file, 
  node_ptr  n 
)
Print an invariant specification

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 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 2009/03/04 13h:34