Line data    Source code

       1             : // Author(s): 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/pbes/pbesinst_algorithm.h
      10             : /// \brief Algorithm for instantiating a PBES.
      11             : 
      12             : #ifndef MCRL2_PBES_PBESINST_ALGORITHM_H
      13             : #define MCRL2_PBES_PBESINST_ALGORITHM_H
      14             : 
      15             : #include "mcrl2/pbes/detail/bes_equation_limit.h"
      16             : #include "mcrl2/pbes/detail/instantiate_global_variables.h"
      17             : #include "mcrl2/pbes/rewriters/enumerate_quantifiers_rewriter.h"
      18             : #include "mcrl2/pbes/rewriters/one_point_rule_rewriter.h"
      19             : #include "mcrl2/pbes/rewriters/simplify_quantifiers_rewriter.h"
      20             : 
      21             : namespace mcrl2
      22             : {
      23             : 
      24             : namespace pbes_system
      25             : {
      26             : 
      27             : /// \brief Creates a substitution function for the pbesinst rewriter.
      28             : /// \param v A sequence of data variables
      29             : /// \param e A sequence of data expressions
      30             : /// \param sigma The substitution that maps the i-th element of \p v to the i-th element of \p e
      31             : inline
      32          98 : void make_pbesinst_substitution(const data::variable_list& v, const data::data_expression_list& e, data::rewriter::substitution_type& sigma)
      33             : {
      34          98 :   assert(v.size() == e.size());
      35          98 :   data::variable_list::iterator i = v.begin();
      36          98 :   data::data_expression_list::iterator j = e.begin();
      37         950 :   for (; i != v.end(); ++i, ++j)
      38             :   {
      39         852 :     sigma[*i] = *j;
      40             :   }
      41          98 : }
      42             : 
      43             : inline
      44         424 : bool pbesinst_is_constant(const pbes_expression& x)
      45             : {
      46         424 :   return pbes_system::find_free_variables(x).empty();
      47             : }
      48             : 
      49             : /// \brief Creates a unique name for a propositional variable instantiation. The
      50             : /// propositional variable instantiation must be closed.
      51             : /// Originally implemented by Alexander van Dam.
      52             : /// \return A name that uniquely corresponds to the propositional variable.
      53             : struct pbesinst_rename_long
      54             : {
      55         212 :   core::identifier_string operator()(const propositional_variable_instantiation& Ye) const
      56             :   {
      57         212 :     assert(pbesinst_is_constant(Ye));
      58         212 :     std::string name = Ye.name();
      59        2116 :     for (const data::data_expression& exp: Ye.parameters())
      60             :     {
      61        1904 :       if (is_function_symbol(exp) && exp.sort() != data::sort_pos::pos() && exp.sort() != data::sort_nat::nat())
      62             :       {
      63             :         // This case is dealt with separately, as it occurs often.
      64             :         // The use of pp as in the next case is correct for this case also, but very time consuming.
      65             :         // The exception to this rule is constants @c1 of sort Pos, @c0 of sort Nat.
      66        1212 :         name += "@";
      67        1212 :         name += atermpp::down_cast<data::function_symbol>(exp).name();
      68             :       }
      69         692 :       else if (is_function_symbol(exp) || is_application(exp) || is_abstraction(exp))
      70             :       {
      71         692 :         name += "@";
      72         692 :         name += data::pp(exp);
      73             :       }
      74             :       else
      75             :       {
      76           0 :         throw mcrl2::runtime_error(std::string("pbesinst_rename_long: could not rename the variable ") + pbes_system::pp(Ye) + " " + data::pp(exp));
      77             :       }
      78             :     }
      79         424 :     return name;
      80         212 :   }
      81             : };
      82             : 
      83             : /// \brief Creates a unique name for a propositional variable instantiation. The
      84             : /// propositional variable instantiation must be closed.
      85             : /// Originally implemented by Alexander van Dam.
      86             : /// \return A name that uniquely corresponds to the propositional variable.
      87             : struct pbesinst_rename
      88             : {
      89         212 :   propositional_variable_instantiation operator()(const propositional_variable_instantiation& Ye) const
      90             :   {
      91         212 :     if (!pbesinst_is_constant(Ye))
      92             :     {
      93           0 :       return Ye;
      94             :     }
      95         424 :     return propositional_variable_instantiation(pbesinst_rename_long()(Ye), data::data_expression_list());
      96             :   }
      97             : };
      98             : 
      99             : /// \brief Algorithm class for the pbesinst instantiation algorithm.
     100             : class pbesinst_algorithm
     101             : {
     102             :   protected:
     103             :     /// \brief Data rewriter.
     104             :     data::rewriter datar;
     105             : 
     106             :     /// \brief The rewriter.
     107             :     enumerate_quantifiers_rewriter R;
     108             : 
     109             :     /// \brief The number of generated equations.
     110             :     std::size_t m_equation_count;
     111             : 
     112             :     /// \brief Propositional variable instantiations that need to be handled.
     113             :     std::set<propositional_variable_instantiation> todo;
     114             : 
     115             :     /// \brief Propositional variable instantiations that have been handled.
     116             :     std::set<propositional_variable_instantiation> done;
     117             : 
     118             :     /// \brief Data structure for storing the result. E[i] corresponds to the equations
     119             :     /// generated from the i-th PBES equation.
     120             :     std::vector<std::vector<pbes_equation> > E;
     121             : 
     122             :     /// \brief The initial value.
     123             :     propositional_variable_instantiation init;
     124             : 
     125             :     /// \brief A lookup map for PBES equations.
     126             :     std::map<core::identifier_string, int> equation_index;
     127             : 
     128             :     /// \brief Print the equations to standard out.
     129             :     bool m_print_equations;
     130             : 
     131             :     /// \brief Prints a log message for every 1000-th equation
     132           0 :     std::string print_equation_count(std::size_t size) const
     133             :     {
     134           0 :       if (size > 0 && size % 1000 == 0)
     135             :       {
     136           0 :         std::ostringstream out;
     137           0 :         out << "Generated " << size << " BES equations" << std::endl;
     138           0 :         return out.str();
     139           0 :       }
     140           0 :       return "";
     141             :     }
     142             : 
     143             :     // renames propositional variables in x
     144          90 :     pbes_expression rho(const pbes_expression& x) const
     145             :     {
     146         180 :       return replace_propositional_variables(x, pbesinst_rename());
     147             :     }
     148             : 
     149             :   public:
     150             : 
     151             :     /// \brief Constructor.
     152             :     /// \param data_spec A data specification.
     153             :     /// \param rewrite_strategy A strategy for the data rewriter.
     154             :     /// \param print_equations If true, the generated equations are printed.
     155           8 :     explicit pbesinst_algorithm(data::data_specification const& data_spec,
     156             :                        data::rewriter::strategy rewrite_strategy = data::jitty,
     157             :                        bool print_equations = false
     158             :                       )
     159           8 :       :
     160           8 :         datar(data_spec, rewrite_strategy),
     161           8 :         R(datar, data_spec),
     162           8 :         m_equation_count(0),
     163           8 :         m_print_equations(print_equations)
     164           8 :     {}
     165             : 
     166             :     /// \brief Runs the algorithm. The result is obtained by calling the function \p get_result.
     167             :     /// \param p A PBES.
     168           8 :     void run(pbes& p)
     169             :     {
     170             :       using utilities::detail::pick_element;
     171             :       using utilities::detail::contains;
     172             : 
     173           8 :       pbes_system::detail::instantiate_global_variables(p);
     174             : 
     175             :       // simplify all right hand sides of p
     176             :       //
     177             :       // NOTE: This is not just an optimization. There are certain PBES
     178             :       // equations for which applying enumerate_quantifiers_rewriter directly
     179             :       // won't terminate, like:
     180             :       //
     181             :       // forall m: Nat . exists k: Nat . val(m == k)
     182             :       pbes_system::one_point_rule_rewriter one_point_rule_rewriter;
     183           8 :       pbes_system::simplify_quantifiers_data_rewriter<mcrl2::data::rewriter> simplify_rewriter(datar);
     184          21 :       for (pbes_equation& eqn: p.equations())
     185             :       {
     186          13 :         eqn.formula() = one_point_rule_rewriter(simplify_rewriter(eqn.formula()));
     187             :       }
     188             : 
     189             :       // initialize equation_index and E
     190           8 :       int eqn_index = 0;
     191           8 :       auto const& equations = p.equations();
     192          21 :       for (const pbes_equation& eqn : equations)
     193             :       {
     194          13 :         equation_index[eqn.variable().name()] = eqn_index++;
     195          13 :         E.emplace_back();
     196             :       }
     197           8 :       init = atermpp::down_cast<propositional_variable_instantiation>(R(p.initial_state()));
     198           8 :       todo.insert(init);
     199          98 :       while (!todo.empty())
     200             :       {
     201          90 :         auto const& X_e = pick_element(todo);
     202          90 :         done.insert(X_e);
     203          90 :         int index = equation_index[X_e.name()];
     204          90 :         const pbes_equation& eqn = p.equations()[index];
     205          90 :         data::rewriter::substitution_type sigma;
     206          90 :         make_pbesinst_substitution(eqn.variable().parameters(), X_e.parameters(), sigma);
     207          90 :         auto const& phi = eqn.formula();
     208          90 :         pbes_expression psi_e = R(phi, sigma);
     209          90 :         R.clear_identifier_generator();
     210         203 :         for (const propositional_variable_instantiation& v: find_propositional_variable_instantiations(psi_e))
     211             :         {
     212         113 :           if (!contains(done, v))
     213             :           {
     214          87 :             todo.insert(v);
     215             :           }
     216          90 :         }
     217         180 :         pbes_equation new_eqn(eqn.symbol(), propositional_variable(pbesinst_rename()(X_e).name(), data::variable_list()), rho(psi_e));
     218          90 :         if (m_print_equations)
     219             :         {
     220          74 :           mCRL2log(log::info) << eqn.symbol() << " " << X_e << " = " << psi_e << std::endl;
     221             :         }
     222          90 :         E[index].push_back(new_eqn);
     223          90 :         mCRL2log(log::verbose) << print_equation_count(++m_equation_count);
     224          90 :         detail::check_bes_equation_limit(m_equation_count);
     225          90 :       }
     226           8 :     }
     227             : 
     228             :     /// \brief Returns the computed bes in pbes format
     229             :     /// \return The computed bes in pbes format
     230           8 :     pbes get_result()
     231             :     {
     232           8 :       pbes result;
     233          21 :       for (const std::vector<pbes_equation>& equations: E)
     234             :       {
     235          13 :         result.equations().insert(result.equations().end(), equations.begin(), equations.end());
     236             :       }
     237           8 :       result.initial_state() = pbesinst_rename()(init);
     238           8 :       return result;
     239           0 :     }
     240             : 
     241             :     /// \brief Returns the flag for printing the generated bes equations
     242             :     /// \return The flag for printing the generated bes equations
     243             :     bool& print_equations()
     244             :     {
     245             :       return m_print_equations;
     246             :     }
     247             : 
     248             :     enumerate_quantifiers_rewriter& rewriter()
     249             :     {
     250             :       return R;
     251             :     }
     252             : };
     253             : 
     254             : } // namespace pbes_system
     255             : 
     256             : } // namespace mcrl2
     257             : 
     258             : #endif // MCRL2_PBES_PBESINST_ALGORITHM_H