LCOV - code coverage report
Current view: top level - lps/include/mcrl2/lps - invelm_algorithm.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 22 22 100.0 %
Date: 2020-09-16 00:45:56 Functions: 6 12 50.0 %
Legend: Lines: hit not hit

          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           4 : 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          52 :       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           8 :         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

Generated by: LCOV version 1.13