Line data Source code
1 : // Author(s): Luc Engelen, Wieger Wesselink 2 : // Copyright: see the accompanying file COPYING or copy at 3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING 4 : // 5 : // Distributed under the Boost Software License, Version 1.0. 6 : // (See accompanying file LICENSE_1_0.txt or copy at 7 : // http://www.boost.org/LICENSE_1_0.txt) 8 : // 9 : /// \file mcrl2/lps/invelm_algorithm.h 10 : /// \brief Interface to class invariant_eliminator 11 : 12 : #ifndef MCRL2_LPS_INVELM_ALGORITHM_H 13 : #define MCRL2_LPS_INVELM_ALGORITHM_H 14 : 15 : #include "mcrl2/data/parse.h" 16 : #include "mcrl2/lps/detail/lps_algorithm.h" 17 : #include "mcrl2/lps/invariant_checker.h" 18 : 19 : namespace mcrl2 20 : { 21 : 22 : namespace lps 23 : { 24 : 25 : /// The class invariant_eliminator is initialized with an LPS using the constructor 26 : /// invariant_eliminator::invariant_eliminator. After initialization, the method invariant_eliminator::simplify can be 27 : /// called any number of times to simplify or eliminate the summands of this LPS using an invariant. A new instance of the 28 : /// class invariant_eliminator has to be created for each new LPS that has to be processed. 29 : /// 30 : /// The class invariant_eliminator uses an instance of the class BDD_Prover to simplify or eliminate summands of an mCRL2 31 : /// LPS. The constructor invariant_eliminator::invariant_eliminator initializes the BDD based prover with the parameters 32 : /// a_rewrite_strategy, a_time_limit, a_path_eliminator, a_solver_type, and the data specification of the LPS passed as 33 : /// parameter a_lps. The parameter a_rewrite_strategy specifies which rewrite strategy is used by the prover's rewriter. 34 : /// It can be set to either GS_REWR_JITTY or GS_REWR_JITTYC. The parameter a_time_limit 35 : /// specifies the maximum amount of time in seconds to be spent by the prover on proving a single expression. If 36 : /// a_time_limit is set to 0, no time limit will be enforced. The parameter a_path_eliminator specifies whether or not 37 : /// path elimination is applied. When path elimination is applied, the prover uses an SMT solver to remove inconsistent 38 : /// paths from BDDs. The parameter a_solver_type specifies which SMT solver is used for path elimination. Either the SMT 39 : /// solver ario (http://www.eecs.umich.edu/~ario/) or cvc-lite (http://www.cs.nyu.edu/acsys/cvcl/) can be used. To use one 40 : /// of these solvers, the directory containing the corresponding executable must be in the path. If the parameter 41 : /// a_path_eliminator is set to false, the parameter a_solver_type is ignored. The parameter a_apply_induction indicates 42 : /// whether or not induction on list will be applied. 43 : /// 44 : /// The parameter a_dot_file_name specifies whether a file in dot format of the resulting BDD is saved each time the 45 : /// prover cannot determine whether an expression is a contradiction or a tautology. If the parameter is set to 0, no .dot 46 : /// files are saved. If a string is passed as parameter a_dot_file_name, this string will be used as the prefix of the 47 : /// filenames. An instance of the class BDD2Dot is used to save these files in dot format. 48 : /// 49 : /// If the parameter a_simplify_all is set to false, the summands whose conditions in conjunction with the invariant prove 50 : /// to be a contradiction are eliminated. If parameter a_simplify_all is set to true, in addition to removing those 51 : /// summands, the conditions of all other summands of the LPS are simplified when calling method 52 : /// invariant_eliminator::simplify. 53 : /// 54 : /// The method invariant_eliminator::simplify returns the LPS passed as parameter a_lps of the constructor after 55 : /// simplification or elimination using the invariant passed as parameter a_invariant. If a_summand_number differs from 0, 56 : /// only the summand with the number passed as parameter a_summand_number will be eliminated or simplified. One instance 57 : /// of the class invariant_eliminator can check any number of invariants on the same LPS. For each new LPS to be checked, 58 : /// a new instance of the class has to be created. 59 : /// 60 : /// Given an LPS, 61 : /// 62 : /// P(d: D) = ... 63 : /// + sum ei: Ei. ci(d, ei) -> ai(fi(d, ei)) . P(gi(d, ei)) 64 : /// + ...; 65 : /// 66 : /// an instance of the class invariant_eliminator will generate a formula of the form 67 : /// 68 : /// inv(d) /\ ci(d, ei) 69 : /// 70 : /// for each of the summands or for the chosen summand only, where inv() is the invariant passed as parameter a_invariant. 71 : /// If such a formula is a contradiction according to the prover, the corresponding summand will be eliminated. If the 72 : /// parameter a_simplify_all is set, the condition of each summand is replaced by the BDD obtained from the prover after 73 : /// proving that summand's formula. 74 : 75 : template <class Specification> 76 : class invelm_algorithm: public detail::lps_algorithm<Specification> 77 : { 78 : typedef typename detail::lps_algorithm<Specification> super; 79 : typedef typename Specification::process_type process_type; 80 : typedef typename process_type::action_summand_type action_summand_type; 81 : using super::m_spec; 82 : 83 : private: 84 : data::detail::BDD_Prover f_bdd_prover; 85 : bool f_simplify_all; 86 : 87 : /// \brief Adds an invariant to the condition of the summand s, and optionally applies the prover to it 88 : /// \param s The summand that needs to be simplified 89 : /// \param invariant A data expression 90 : /// \param apply_prover If true, the prover is applied to the condition 91 26 : void simplify_summand(summand_base& s, const data::data_expression& invariant, bool apply_prover) 92 : { 93 26 : data::data_expression new_condition = data::lazy::and_(invariant, s.condition()); 94 : 95 26 : if (apply_prover) 96 : { 97 21 : f_bdd_prover.set_formula(new_condition); 98 21 : new_condition = f_bdd_prover.get_bdd(); 99 : } 100 26 : if (f_simplify_all || data::sort_bool::is_false_function_symbol(new_condition)) 101 : { 102 11 : s.condition() = new_condition; 103 : } 104 26 : } 105 : 106 : template <typename SummandSequence> 107 8 : void simplify_summands(SummandSequence& summands, const data::data_expression& invariant, bool apply_prover) 108 : { 109 34 : for (summand_base& s: summands) 110 : { 111 26 : simplify_summand(s, invariant, apply_prover); 112 : } 113 8 : } 114 : 115 : public: 116 : /// precondition: the argument passed as parameter a_lps is a valid mCRL2 LPS 117 : /// precondition: the argument passed as parameter a_time_limit is greater than or equal to 0. If the argument is equal 118 : /// to 0, no time limit will be enforced 119 4 : invelm_algorithm( 120 : Specification& a_lps, 121 : const data::rewriter::strategy a_rewrite_strategy = data::jitty, 122 : const int a_time_limit = 0, 123 : const bool a_path_eliminator = false, 124 : const data::detail::smt_solver_type a_solver_type = data::detail::solver_type_cvc, 125 : const bool a_apply_induction = false, 126 : const bool a_simplify_all = false 127 : ) 128 : : detail::lps_algorithm<Specification>(a_lps), 129 4 : f_bdd_prover(a_lps.data(), data::used_data_equation_selector(a_lps.data()),a_rewrite_strategy, a_time_limit, a_path_eliminator, a_solver_type, a_apply_induction), 130 4 : f_simplify_all(a_simplify_all) 131 4 : {} 132 : 133 4 : void run(const data::data_expression& invariant, bool apply_prover) 134 : { 135 4 : simplify_summands(m_spec.process().action_summands(), invariant, apply_prover); 136 4 : simplify_summands(m_spec.process().deadlock_summands(), invariant, apply_prover); 137 4 : super::remove_trivial_summands(); 138 4 : } 139 : }; 140 : 141 : } // namespace lps 142 : 143 : } // namespace mcrl2 144 : 145 : #endif // MCRL2_LPS_INVELM_ALGORITHM_H