|
| invelm_algorithm (Specification &a_lps, const data::rewriter::strategy a_rewrite_strategy=data::jitty, const int a_time_limit=0, const bool a_path_eliminator=false, const data::detail::smt_solver_type a_solver_type=data::detail::solver_type_cvc, const bool a_apply_induction=false, const bool a_simplify_all=false) |
|
void | run (const data::data_expression &invariant, bool apply_prover) |
|
| lps_algorithm (Specification &spec) |
| Constructor.
|
|
bool | verbose () const |
| Flag for verbose output.
|
|
data::data_expression | next_state (const action_summand &s, const data::variable &v) const |
| Applies the next state substitution to the variable v.
|
|
void | instantiate_free_variables () |
| Attempts to eliminate the free variables of the specification, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown.
|
|
void | remove_parameters (const std::set< data::variable > &to_be_removed) |
| Removes formal parameters from the specification.
|
|
void | remove_singleton_sorts () |
| Removes parameters with a singleton sort.
|
|
void | remove_trivial_summands () |
| Removes summands with condition equal to false.
|
|
void | remove_unused_summand_variables () |
| Removes unused summand variables.
|
|
template<class Specification>
class mcrl2::lps::invelm_algorithm< Specification >
The class invariant_eliminator is initialized with an LPS using the constructor invariant_eliminator::invariant_eliminator. After initialization, the method invariant_eliminator::simplify can be called any number of times to simplify or eliminate the summands of this LPS using an invariant. A new instance of the class invariant_eliminator has to be created for each new LPS that has to be processed.
The class invariant_eliminator uses an instance of the class BDD_Prover to simplify or eliminate summands of an mCRL2 LPS. The constructor invariant_eliminator::invariant_eliminator initializes the BDD based prover with the parameters a_rewrite_strategy, a_time_limit, a_path_eliminator, a_solver_type, and the data specification of the LPS passed as parameter a_lps. The parameter a_rewrite_strategy specifies which rewrite strategy is used by the prover's rewriter. It can be set to either GS_REWR_JITTY or GS_REWR_JITTYC. The parameter a_time_limit specifies the maximum amount of time in seconds to be spent by the prover on proving a single expression. If a_time_limit is set to 0, no time limit will be enforced. The parameter a_path_eliminator specifies whether or not path elimination is applied. When path elimination is applied, the prover uses an SMT solver to remove inconsistent paths from BDDs. The parameter a_solver_type specifies which SMT solver is used for path elimination. Either the SMT solver ario (http://www.eecs.umich.edu/~ario/) or cvc-lite (http://www.cs.nyu.edu/acsys/cvcl/) can be used. To use one of these solvers, the directory containing the corresponding executable must be in the path. If the parameter a_path_eliminator is set to false, the parameter a_solver_type is ignored. The parameter a_apply_induction indicates whether or not induction on list will be applied.
The parameter a_dot_file_name specifies whether a file in dot format of the resulting BDD is saved each time the prover cannot determine whether an expression is a contradiction or a tautology. If the parameter is set to 0, no .dot files are saved. If a string is passed as parameter a_dot_file_name, this string will be used as the prefix of the filenames. An instance of the class BDD2Dot is used to save these files in dot format.
If the parameter a_simplify_all is set to false, the summands whose conditions in conjunction with the invariant prove to be a contradiction are eliminated. If parameter a_simplify_all is set to true, in addition to removing those summands, the conditions of all other summands of the LPS are simplified when calling method invariant_eliminator::simplify.
The method invariant_eliminator::simplify returns the LPS passed as parameter a_lps of the constructor after simplification or elimination using the invariant passed as parameter a_invariant. If a_summand_number differs from 0, only the summand with the number passed as parameter a_summand_number will be eliminated or simplified. One instance of the class invariant_eliminator can check any number of invariants on the same LPS. For each new LPS to be checked, a new instance of the class has to be created.
Given an LPS,
P(d: D) = ...
- sum ei: Ei. ci(d, ei) -> ai(fi(d, ei)) . P(gi(d, ei))
- ...;
an instance of the class invariant_eliminator will generate a formula of the form
inv(d) /\ ci(d, ei)
for each of the summands or for the chosen summand only, where inv() is the invariant passed as parameter a_invariant. If such a formula is a contradiction according to the prover, the corresponding summand will be eliminated. If the parameter a_simplify_all is set, the condition of each summand is replaced by the BDD obtained from the prover after proving that summand's formula.
Definition at line 76 of file invelm_algorithm.h.