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/process/remove_equations.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_REMOVE_EQUATIONS_H
      13             : #define MCRL2_PROCESS_REMOVE_EQUATIONS_H
      14             : 
      15             : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
      16             : #include "mcrl2/process/replace.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace process {
      21             : 
      22             : namespace detail {
      23             : 
      24             : // Uses a bisimulation algorithm to find duplicate equations. For example in the following
      25             : // list of equations
      26             : //
      27             : // S(b: Bool) = sum d: D. r1(d) . T(d, b);
      28             : // T(d: D, b: Bool) = s2(d, b) . (r6(b) . S(!b) + (r6(!b) + r6(e)) . T(d, b));
      29             : // R(b: Bool) = sum d: D. r3(d, b) . s4(d) . s5(b) . R(!b) + (sum d: D. r3(d, !b) + r3(e)) . s5(!b) . R(b);
      30             : // K = sum d: D, b: Bool. r2(d, b) . (i . s3(d, b) + i . s3(e)) . K;
      31             : // L = sum b: Bool. r5(b) . (i . s6(b) + i . s6(e)) . L;
      32             : // S2(b: Bool) = sum d: D. r1(d) . T1(d, b);
      33             : // T1(d: D, b: Bool) = s2(d, b) . (r6(b) . S2(!b) + (r6(!b) + r6(e)) . T1(d, b));
      34             : //
      35             : // the equations for S2 and T1 will be removed
      36             : struct duplicate_equation_removal
      37             : {
      38             :   typedef std::vector<process_equation>::const_iterator iterator;
      39             :   typedef std::set<iterator> group;
      40             :   typedef data::mutable_map_substitution<std::map<process_identifier, process_identifier> > substitution;
      41             : 
      42             :   process_specification& procspec;
      43             :   data::set_identifier_generator generator;
      44             :   std::vector<group> groups;
      45             : 
      46           2 :   std::string print_group(const group& g)
      47             :   {
      48           2 :     std::ostringstream out;
      49           5 :     for (auto i: g)
      50             :     {
      51           3 :       const process_equation& eq = *i;
      52             : 
      53             :       // use a custom print for equations, since by default they are printed on multiple lines...
      54           3 :       bool print_parens = !eq.formal_parameters().empty();
      55           3 :       out << eq.identifier().name();
      56           3 :       if (print_parens)
      57             :       {
      58           1 :         out << "(";
      59             :       }
      60           3 :       out << data::pp(eq.formal_parameters());
      61           3 :       if (print_parens)
      62             :       {
      63           1 :         out << ")";
      64             :       }
      65           3 :       out << " = " << eq.expression() << ";\n";
      66             :     }
      67           4 :     return out.str();
      68           2 :   }
      69             : 
      70           2 :   std::string print_groups()
      71             :   {
      72           2 :     std::ostringstream out;
      73           2 :     std::size_t index = 0;
      74           4 :     for (auto& group: groups)
      75             :     {
      76           2 :       out << "--- group " << index++ << " ---\n" << print_group(group) << std::endl;
      77             :     }
      78           4 :     return out.str();
      79           2 :   }
      80             : 
      81           2 :   duplicate_equation_removal(process_specification& procspec_)
      82           2 :     : procspec(procspec_)
      83             :   {
      84           2 :     generator.add_identifiers(process::find_identifiers(procspec));
      85           2 :     generator.add_identifiers(data::function_and_mapping_identifiers(procspec.data()));
      86           2 :     std::map<data::variable_list, group> s;
      87           5 :     for (auto i = procspec.equations().begin(); i != procspec.equations().end(); ++i)
      88             :     {
      89           3 :       s[i->formal_parameters()].insert(i);
      90             :     }
      91           4 :     for (auto& i: s)
      92             :     {
      93           2 :       groups.push_back(i.second);
      94             :     }
      95           2 :     mCRL2log(log::debug) << "==========================================================\n" << print_groups() << std::endl;
      96           2 :   }
      97             : 
      98             :   // assigns a unique process identifier to each process identifier within a group
      99           2 :   substitution make_substitution()
     100             :   {
     101           2 :     substitution result;
     102           4 :     for (const group& g: groups)
     103             :     {
     104           2 :       const process_equation& first_equation = **g.begin();
     105           4 :       process_identifier id(generator("X"), first_equation.formal_parameters());
     106           5 :       for (iterator i: g)
     107             :       {
     108           3 :         const process_equation& eq = *i;
     109           3 :         result[eq.identifier()] = id;
     110             :       }
     111           2 :     }
     112           2 :     return result;
     113           0 :   }
     114             : 
     115             :   // splits the group g into multiple groups, and appends them to result
     116           2 :   void split_group(const group& g, const substitution& sigma, std::vector<group>& result)
     117             :   {
     118           2 :     std::map<process_expression, group> m;
     119           5 :     for (auto i: g)
     120             :     {
     121           3 :       const process_equation& eq = *i;
     122           3 :       process_expression expr = replace_process_identifiers(eq.expression(), sigma);
     123           3 :       m[expr].insert(i);
     124           3 :     }
     125           4 :     for (auto &i : m)
     126             :     {
     127           2 :       result.push_back(i.second);
     128             :     }
     129           2 :   }
     130             : 
     131             :   // splits all groups
     132             :   // returns true if at least one of the groups was split into multiple groups
     133           2 :   bool split_groups()
     134             :   {
     135           2 :     substitution sigma = make_substitution();
     136           2 :     std::vector<group> new_groups;
     137           4 :     for (auto& group: groups)
     138             :     {
     139           2 :       split_group(group, sigma, new_groups);
     140             :     }
     141           2 :     bool result = new_groups.size() > groups.size();
     142           2 :     groups = new_groups;
     143           2 :     return result;
     144           2 :   }
     145             : 
     146           2 :   void run()
     147             :   {
     148             :     // Compute groups of equal equations
     149             :     for (;;)
     150             :     {
     151           2 :       if (!split_groups())
     152             :       {
     153           2 :         break;
     154             :       }
     155           0 :       mCRL2log(log::debug) << "==========================================================\n" << print_groups() << std::endl;
     156             :     }
     157             : 
     158             :     // Choose one equation per group (the one with the lowest index in equations),
     159             :     // and prepare a substitution sigma that removes the others
     160           2 :     std::vector<process_equation> new_equations;
     161           2 :     substitution sigma;
     162           4 :     for (auto& i : groups)
     163             :     {
     164             :       // optimization for the case of only one equation in a group
     165           2 :       if (i.size() == 1)
     166             :       {
     167           1 :         new_equations.push_back(**(i.begin()));
     168           1 :         continue;
     169             :       }
     170             : 
     171           1 :       group::const_iterator j = std::min_element(i.begin(), i.end());
     172           1 :       new_equations.push_back(**j);
     173           3 :       for (group::const_iterator k = i.begin(); k != i.end(); ++k)
     174             :       {
     175           2 :         if (k != j)
     176             :         {
     177           1 :           sigma[(**k).identifier()] = (**j).identifier();
     178             :         }
     179             :       }
     180             :     }
     181             : 
     182             :     // Apply sigma to the new equations and the initial state
     183           4 :     for (auto& new_equation : new_equations)
     184             :     {
     185           2 :       new_equation = process_equation(new_equation.identifier(), new_equation.formal_parameters(), replace_process_identifiers(new_equation.expression(), sigma));
     186             :     }
     187           2 :     procspec.init() = replace_process_identifiers(procspec.init(), sigma);
     188           2 :     procspec.equations() = new_equations;
     189           2 :   }
     190             : };
     191             : 
     192             : } // namespace detail
     193             : 
     194             : inline
     195             : /// \brief Removes duplicate equations from a process specification, using a bisimulation algorithm
     196           2 : void remove_duplicate_equations(process_specification& procspec)
     197             : {
     198           2 :   detail::duplicate_equation_removal f(procspec);
     199           2 :   f.run();
     200           2 : }
     201             : 
     202             : } // namespace process
     203             : 
     204             : } // namespace mcrl2
     205             : 
     206             : #endif // MCRL2_PROCESS_REMOVE_EQUATIONS_H