#include "nusmv/core/utils/utils.h"#include "nusmv/core/dd/dd.h"#include "nusmv/core/node/node.h"#include "nusmv/core/opt/opt.h"#include "nusmv/core/compile/compile.h"#include "nusmv/core/fsm/bdd/BddFsm.h"#include "nusmv/core/fsm/FsmBuilder.h"#include "nusmv/core/trace/TraceMgr.h"#include "nusmv/core/trace/Trace.h"Go to the source code of this file.
Functions | |
| node_ptr | ebg_explain (BddFsm_ptr, BddEnc_ptr, node_ptr, bdd_ptr, int, int) |
This function finds a path of length (sup-inf) that is an example for EG(g)^{sup}_{inf}. | |
| node_ptr | ebu_explain (BddFsm_ptr, BddEnc_ptr, node_ptr, bdd_ptr, bdd_ptr, int, int) |
| This function finds a path that is a witness for E\[f U g\]^{sup}_{inf}. | |
| node_ptr | eg_explain (BddFsm_ptr, BddEnc_ptr, node_ptr, bdd_ptr) |
| This function finds a path that is an example for EG(g). | |
| BddStatesInputs | eg_si (BddFsm_ptr fsm, bdd_ptr g_si) |
| Set of states-inputs satisfying EG(g). | |
| node_ptr | eu_explain (BddFsm_ptr, BddEnc_ptr, node_ptr, bdd_ptr, bdd_ptr) |
| This function finds a path that is a witness for E\[f U g\]. | |
| 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. | |
| 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. | |
| node_ptr | ex_explain (BddFsm_ptr, BddEnc_ptr, node_ptr, bdd_ptr) |
| This function computes a path that is a witness for EX(f). | |
| BddStatesInputs | ex_si (BddFsm_ptr fsm, bdd_ptr si) |
| Set of states satisfying EG(g). | |
Variables | |
| cmp_struct_ptr | cmps |
| FsmBuilder_ptr | global_fsm_builder |
| TraceMgr_ptr | global_trace_manager |
| int | nusmv_yylineno |
| Internal header file of the mc package. | |
| node_ptr ebg_explain | ( | BddFsm_ptr | , | |
| BddEnc_ptr | , | |||
| node_ptr | , | |||
| bdd_ptr | , | |||
| int | , | |||
| int | ||||
| ) |
This function finds a path of length (sup-inf) that is an example for EG(g)^{sup}_{inf}.
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.
| node_ptr ebu_explain | ( | BddFsm_ptr | , | |
| BddEnc_ptr | , | |||
| node_ptr | , | |||
| bdd_ptr | , | |||
| bdd_ptr | , | |||
| int | , | |||
| int | ||||
| ) |
This function finds a path that is a witness for E\[f U g\]^{sup}_{inf}.
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.
| node_ptr eg_explain | ( | BddFsm_ptr | , | |
| BddEnc_ptr | , | |||
| node_ptr | , | |||
| bdd_ptr | ||||
| ) |
This function finds a path that is an example for EG(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).
| BddStatesInputs eg_si | ( | BddFsm_ptr | fsm, | |
| bdd_ptr | g_si | |||
| ) |
| node_ptr eu_explain | ( | BddFsm_ptr | , | |
| BddEnc_ptr | , | |||
| node_ptr | , | |||
| bdd_ptr | , | |||
| bdd_ptr | ||||
| ) |
This function finds a path that is a witness for E\[f U g\].
This function finds a path of single states that is a witness for E\[f U g\]. The first element of path is a BDD p representing a set of states from which the first state of the witness path is taken.
The procedure is to try to execute eu(f,g) again, looking for a path from p along states satisfying f to a state where g is valid. The found path is then stored in path in reverse order. Note that in the found path every state is a minterm, i.e. a single state, not a set. Also the original first element of path is reset to minterm.
If a witness is not found then Nil is return and nothing is modified.
| 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.
| 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.
| node_ptr ex_explain | ( | BddFsm_ptr | , | |
| BddEnc_ptr | , | |||
| node_ptr | , | |||
| bdd_ptr | ||||
| ) |
This function computes a path that is a witness for EX(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.
| BddStatesInputs ex_si | ( | BddFsm_ptr | fsm, | |
| bdd_ptr | si | |||
| ) |
| cmp_struct_ptr cmps |
| int nusmv_yylineno |
Internal header file of the mc package.
1.6.1