void Check_TraceList_Sanity( BddEnc_ptr enc, node_ptr path, const char * varname )
mcExplain.c
int CommandCheckCompute( int argc, char ** argv )
mcCmd.c
int CommandCheckCtlSpec( int argc, char ** argv )
mcCmd.c
int CommandCheckInvar( int argc, char ** argv )
mcCmd.c
int CommandCheckPslSpec( int argc, char ** argv )
mcCmd.c
static int CommandCheckSpec( int argc, char ** argv )
mcCmd.c
int CommandLanguageEmptiness( int argc, char ** argv )
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 )
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 )
mcExplain.c
void Mc_CheckAGOnlySpec( Prop_ptr prop )
check_spec
mcAGonly.c
void Mc_CheckCTLSpec( Prop_ptr prop )
mcMc.c
void Mc_CheckCompute( Prop_ptr prop )
mcMc.c
void Mc_CheckInvar( Prop_ptr prop )
check_spec
check_ltlspec
mcInvar.c
void Mc_CheckLanguageEmptiness( const BddFsm_ptr fsm, boolean allinit, boolean verbose )
BddFsm_get_fair_states
mcLE.c
void Mc_End( )
mcCmd.c
void Mc_Init( )
mcCmd.c
int Mc_check_psl_property( Prop_ptr prop )
mcCmd.c
bdd_ptr Mc_fair_si_iteration( BddFsm_ptr fsm, BddStatesInputs states, BddStatesInputs subspace )
mcMc.c
BddStatesInputs Mc_get_fair_si_subset( BddFsm_ptr fsm, BddStatesInputs si )
mcMc.c
BddStates abu( BddFsm_ptr fsm, BddStates f, BddStates g, int inf, int sup )
au
mcMc.c
BddStates au( BddFsm_ptr fsm, BddStates f, BddStates g )
ax
af
ex
ef
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 )
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