Line data    Source code

       1             : // Author(s): Gijs Kant
       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/detail/ppg_traverser.h
      10             : /// \brief Traverser class for Parameterised Parity Games (PPG), PBES expressions of the form:
      11             : /// PPG :== /\_{i: I} f_i && /\_{j: J} forall v: D_j . ( g_j => X_j(e_j) )
      12             : ///       | \/_{i: I} f_i || \/_{j: J} exists v: D_j . ( g_j && X_j(e_j) ).
      13             : #ifndef MCRL2_PBES_DETAIL_PPG_REWRITER_H
      14             : #define MCRL2_PBES_DETAIL_PPG_REWRITER_H
      15             : 
      16             : #include "mcrl2/pbes/algorithms.h"
      17             : #include "mcrl2/pbes/join.h"
      18             : #include "mcrl2/pbes/pbes_functions.h"
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace pbes_system {
      23             : 
      24             : namespace detail {
      25             : 
      26             : struct fresh_variable_name_generator
      27             : {
      28             :   /// \brief The set of variable names already in use.
      29             :   std::set<std::string> variable_names;
      30             :   /// \brief A map from variable name prefix to the last suffix that has been added.
      31             :   std::map<std::string,int> variable_name_suffix;
      32             : 
      33             :   template <typename Container>
      34           1 :   fresh_variable_name_generator(const Container& equations)
      35           1 :   {
      36           2 :     for (typename Container::const_iterator eqn = equations.begin(); eqn != equations.end(); ++eqn) {
      37           1 :       propositional_variable var = (*eqn).variable();
      38           1 :       variable_names.insert(std::string(var.name()));
      39             :     }
      40           1 :   }
      41             : 
      42             :   /// \brief Generates a fresh variable name, based on s (extending s).
      43             :   /// \param s A string.
      44             :   /// \return a fresh variable name.
      45           2 :   std::string generate_name(const std::string& s) {
      46             :     //std::clog << "fresh_variable_name: ";
      47           2 :     std::string base; std::string name;
      48           2 :     name = base = s;
      49           2 :     int suffix = 1;
      50           4 :     while (variable_names.find(name)!=variable_names.end()) {
      51           2 :       if (variable_name_suffix.find(base) != variable_name_suffix.end()) {
      52           1 :         suffix = variable_name_suffix[base] + 1;
      53             :       }
      54           2 :       variable_name_suffix[base] = suffix;
      55           2 :       std::stringstream ss;
      56           2 :       ss << base << "_" << suffix;
      57           2 :       ss >> name;
      58           2 :     }
      59           2 :     variable_names.insert(name);
      60             :     //std::clog << name << std::endl;
      61           4 :     return name;
      62           2 :   }
      63             : };
      64             : 
      65             : /// \cond INTERNAL_DOCS
      66             : /// \brief Traverser that rewrites the given PBES to PPG format.
      67             : struct ppg_rewriter: public pbes_expression_traverser<ppg_rewriter>
      68             : {
      69             :   typedef pbes_expression_traverser<ppg_rewriter> super;
      70             :   using super::enter;
      71             :   using super::leave;
      72             :   using super::apply;
      73             : 
      74             :   enum expression_mode {
      75             :     CONJUNCTIVE, UNIVERSAL,
      76             :     DISJUNCTIVE, EXISTENTIAL,
      77             :     UNDETERMINED
      78             :   };
      79             : 
      80             :   std::vector<pbes_equation> equations;
      81             :   std::stack<expression_mode> mode_stack;
      82             :   std::stack<fixpoint_symbol> symbol_stack;
      83             :   std::stack<propositional_variable> variable_stack;
      84             :   std::stack<data::variable_list> quantifier_variable_stack;
      85             :   std::stack<pbes_expression> expression_stack;
      86             :   fresh_variable_name_generator name_generator;
      87             : 
      88             :   template <typename Container>
      89           1 :   ppg_rewriter(const Container& equations)
      90           1 :     : name_generator(equations)
      91           1 :   {}
      92             : 
      93           0 :   void apply(const not_& x)
      94             :   {
      95           0 :     throw mcrl2::runtime_error("Unexpected negation in PPG rewriter: " + pp(x));
      96             :   }
      97             : 
      98           0 :   void apply(const imp& x)
      99             :   {
     100           0 :     throw mcrl2::runtime_error("Unexpected implication in PPG rewriter: " + pp(x));
     101             :   }
     102             : 
     103           0 :   void enter(const data::data_expression& x)
     104             :   {
     105           0 :     expression_stack.push(x);
     106           0 :   }
     107             : 
     108           0 :   void enter(const propositional_variable_instantiation& x)
     109             :   {
     110           0 :     expression_stack.push(x);
     111           0 :   }
     112             : 
     113           2 :   propositional_variable_instantiation split_here(const pbes_expression& x)
     114             :   {
     115           2 :     fixpoint_symbol symbol = symbol_stack.top();
     116           2 :     propositional_variable variable = variable_stack.top();
     117           4 :     core::identifier_string fresh_varname = core::identifier_string(name_generator.generate_name(variable.name()));
     118           2 :     data::variable_list variable_parameters = variable.parameters() + quantifier_variable_stack.top();
     119             :     // Create fresh propositional variable.
     120             :     propositional_variable fresh_var =
     121           2 :         propositional_variable(fresh_varname, variable_parameters);
     122           2 :     pbes_equation new_eqn = pbes_equation(symbol, fresh_var, x);
     123           2 :     this->apply(new_eqn);
     124             :     propositional_variable_instantiation fresh_var_instantiation =
     125           2 :         propositional_variable_instantiation(fresh_varname, atermpp::container_cast<data::data_expression_list>(variable_parameters));
     126           4 :     return fresh_var_instantiation;
     127           2 :   }
     128             : 
     129           0 :   void apply(const pbes_system::forall& x)
     130             :   {
     131           0 :     this->enter(x);
     132           0 :     bool simple_body = is_simple_expression(x.body());
     133           0 :     if (simple_body)
     134             :     {
     135           0 :       expression_stack.push(x);
     136             :     }
     137             :     else
     138             :     {
     139           0 :       expression_mode mode = mode_stack.top();
     140           0 :       switch(mode)
     141             :       {
     142           0 :       case UNDETERMINED:
     143             :       case CONJUNCTIVE:
     144           0 :         mode = UNIVERSAL;
     145             :         [[fallthrough]];
     146           0 :       case UNIVERSAL:
     147             :       {
     148           0 :         quantifier_variable_stack.push(quantifier_variable_stack.top() + x.variables());
     149           0 :         mode_stack.push(mode);
     150           0 :         this->apply(x.body());
     151           0 :         mode_stack.pop();
     152           0 :         pbes_expression body = expression_stack.top();
     153           0 :         expression_stack.pop();
     154           0 :         pbes_expression expr = forall(x.variables(), body);
     155           0 :         expression_stack.push(expr);
     156           0 :         quantifier_variable_stack.pop();
     157           0 :         break;
     158           0 :       }
     159           0 :       case DISJUNCTIVE:
     160             :       case EXISTENTIAL:
     161           0 :         expression_stack.push(split_here(x));
     162           0 :         break;
     163           0 :       default:
     164           0 :         std::clog << "mode = " << mode << std::endl;
     165           0 :         throw std::runtime_error("unexpected forall");
     166             :         break;
     167             :       }
     168             :     }
     169           0 :     this->leave(x);
     170           0 :   }
     171             : 
     172           4 :   void apply(const pbes_system::exists& x)
     173             :   {
     174           4 :     this->enter(x);
     175           4 :     bool simple_body = is_simple_expression(x.body());
     176           4 :     if (simple_body)
     177             :     {
     178           0 :       expression_stack.push(x);
     179             :     }
     180             :     else
     181             :     {
     182           4 :       expression_mode mode = mode_stack.top();
     183           4 :       switch(mode)
     184             :       {
     185           2 :       case UNDETERMINED:
     186             :       case DISJUNCTIVE:
     187           2 :         mode = EXISTENTIAL;
     188             :         [[fallthrough]];
     189           2 :       case EXISTENTIAL:
     190             :       {
     191           2 :         quantifier_variable_stack.push(quantifier_variable_stack.top() + x.variables());
     192           2 :         mode_stack.push(mode);
     193           2 :         this->apply(x.body());
     194           2 :         mode_stack.pop();
     195           2 :         pbes_expression body = expression_stack.top();
     196           2 :         expression_stack.pop();
     197           2 :         pbes_expression expr = exists(x.variables(), body);
     198           2 :         expression_stack.push(expr);
     199           2 :         quantifier_variable_stack.pop();
     200           2 :         break;
     201           2 :       }
     202           2 :       case CONJUNCTIVE:
     203             :       case UNIVERSAL:
     204           2 :         expression_stack.push(split_here(x));
     205           2 :         break;
     206           0 :       default:
     207           0 :         std::clog << "mode = " << mode << std::endl;
     208           0 :         throw std::runtime_error("unexpected exists");
     209             :         break;
     210             :       }
     211             :     }
     212           4 :     this->leave(x);
     213           4 :   }
     214             : 
     215           3 :   void apply(const pbes_system::and_& x)
     216             :   {
     217           3 :     this->enter(x);
     218           3 :     bool is_simple = is_simple_expression(x);
     219           3 :     if (is_simple)
     220             :     {
     221           0 :       expression_stack.push(x);
     222             :     }
     223             :     else
     224             :     {
     225           3 :       expression_mode mode = mode_stack.top();
     226           3 :       switch(mode)
     227             :       {
     228           1 :       case UNDETERMINED:
     229           1 :         mode = CONJUNCTIVE;
     230             :         [[fallthrough]];
     231           1 :       case CONJUNCTIVE:
     232             :       {
     233           1 :         mode_stack.push(mode);
     234           1 :         this->apply(x.left());
     235           1 :         this->apply(x.right());
     236           1 :         mode_stack.pop();
     237           1 :         pbes_expression r = expression_stack.top();
     238           1 :         expression_stack.pop();
     239           1 :         pbes_expression l = expression_stack.top();
     240           1 :         expression_stack.pop();
     241           1 :         pbes_expression expr = and_(l, r);
     242           1 :         expression_stack.push(expr);
     243           1 :         break;
     244           1 :       }
     245           0 :       case UNIVERSAL:
     246           0 :         expression_stack.push(split_here(x));
     247           0 :         break;
     248           2 :       case EXISTENTIAL:
     249             :       case DISJUNCTIVE:
     250             :       {
     251           2 :         std::vector<pbes_expression> conjuncts = split_conjuncts(x);
     252           2 :         bool split = false;
     253           2 :         std::size_t count = 0;
     254           7 :         for(const pbes_expression& conjunct: conjuncts)
     255             :         {
     256           5 :           if (!is_simple_expression(conjunct))
     257             :           {
     258           2 :             count++;
     259           2 :             if (count > 1 || !is_propositional_variable_instantiation(conjunct))
     260             :             {
     261           0 :               split = true;
     262           0 :               break;
     263             :             }
     264             :           }
     265             :         }
     266           2 :         if (split)
     267             :         {
     268           0 :           std::vector<pbes_expression> simple_conjuncts;
     269           0 :           std::vector<pbes_expression> new_conjuncts;
     270           0 :           for(const pbes_expression& conjunct : conjuncts)
     271             :           {
     272           0 :             if (is_simple_expression(conjunct))
     273             :             {
     274           0 :               simple_conjuncts.push_back(conjunct);
     275             :             }
     276             :             else
     277             :             {
     278           0 :               new_conjuncts.push_back(conjunct);
     279             :             }
     280             :           }
     281           0 :           pbes_expression new_conj = join_and(new_conjuncts.begin(), new_conjuncts.end());
     282           0 :           pbes_expression expr = split_here(new_conj);
     283           0 :           if (simple_conjuncts.size() > 0)
     284             :           {
     285           0 :             pbes_expression simple_conj = join_and(simple_conjuncts.begin(), simple_conjuncts.end());
     286           0 :             expr = and_(simple_conj, expr);
     287           0 :           }
     288           0 :           expression_stack.push(expr);
     289           0 :         }
     290             :         else
     291             :         {
     292           2 :           expression_stack.push(x);
     293             :         }
     294           2 :         break;
     295           2 :       }
     296           0 :       default:
     297           0 :         std::clog << "mode = " << mode << std::endl;
     298           0 :         throw std::runtime_error("unexpected and");
     299             :         break;
     300             :       }
     301             :     }
     302           3 :     this->leave(x);
     303           3 :   }
     304             : 
     305           0 :   void apply(const pbes_system::or_& x)
     306             :   {
     307           0 :     this->enter(x);
     308           0 :     bool is_simple = is_simple_expression(x);
     309           0 :     if (is_simple)
     310             :     {
     311           0 :       expression_stack.push(x);
     312             :     }
     313             :     else
     314             :     {
     315           0 :       expression_mode mode = mode_stack.top();
     316           0 :       switch(mode)
     317             :       {
     318           0 :       case UNDETERMINED:
     319           0 :         mode = DISJUNCTIVE;
     320             :         [[fallthrough]];
     321           0 :       case DISJUNCTIVE:
     322             :       {
     323           0 :         mode_stack.push(mode);
     324           0 :         this->apply(x.left());
     325           0 :         this->apply(x.right());
     326           0 :         mode_stack.pop();
     327           0 :         pbes_expression r = expression_stack.top();
     328           0 :         expression_stack.pop();
     329           0 :         pbes_expression l = expression_stack.top();
     330           0 :         expression_stack.pop();
     331           0 :         pbes_expression expr = or_(l, r);
     332           0 :         expression_stack.push(expr);
     333           0 :         break;
     334           0 :       }
     335           0 :       case EXISTENTIAL:
     336           0 :         expression_stack.push(split_here(x));
     337           0 :         break;
     338           0 :       case UNIVERSAL:
     339             :       case CONJUNCTIVE:
     340             :       {
     341           0 :         std::vector<pbes_expression> disjuncts = split_disjuncts(x);
     342           0 :         bool split = false;
     343           0 :         std::size_t count = 0;
     344           0 :         for(const pbes_expression& disjunct: disjuncts)
     345             :         {
     346           0 :           if (!is_simple_expression(disjunct))
     347             :           {
     348           0 :             count++;
     349           0 :             if (count > 1 || !is_propositional_variable_instantiation(disjunct))
     350             :             {
     351           0 :               split = true;
     352           0 :               break;
     353             :             }
     354             :           }
     355             :         }
     356           0 :         if (split)
     357             :         {
     358           0 :           std::vector<pbes_expression> simple_disjuncts;
     359           0 :           std::vector<pbes_expression> new_disjuncts;
     360           0 :           for(const pbes_expression& disjunct : disjuncts)
     361             :           {
     362           0 :             if (is_simple_expression(disjunct))
     363             :             {
     364           0 :               simple_disjuncts.push_back(disjunct);
     365             :             }
     366             :             else
     367             :             {
     368           0 :               new_disjuncts.push_back(disjunct);
     369             :             }
     370             :           }
     371           0 :           pbes_expression new_disj = join_or(new_disjuncts.begin(), new_disjuncts.end());
     372           0 :           pbes_expression expr = split_here(new_disj);
     373           0 :           if (simple_disjuncts.size() > 0)
     374             :           {
     375           0 :             pbes_expression simple_disj = join_or(simple_disjuncts.begin(), simple_disjuncts.end());
     376           0 :             expr = or_(simple_disj, expr);
     377           0 :           }
     378           0 :           expression_stack.push(expr);
     379             : 
     380           0 :         }
     381             :         else
     382             :         {
     383           0 :           expression_stack.push(x);
     384             :         }
     385           0 :         break;
     386           0 :       }
     387           0 :       default:
     388           0 :         std::clog << "mode = " << mode << std::endl;
     389           0 :         throw std::runtime_error("unexpected or");
     390             :         break;
     391             :       }
     392             :     }
     393           0 :     this->leave(x);
     394           0 :   }
     395             : 
     396           3 :   void enter(const pbes_equation& x)
     397             :   {
     398           3 :     symbol_stack.push(x.symbol());
     399           3 :     variable_stack.push(x.variable());
     400           3 :     data::variable_list l;
     401           3 :     quantifier_variable_stack.push(l);
     402           3 :     mode_stack.push(UNDETERMINED);
     403           3 :   }
     404             : 
     405             : #ifndef NDEBUG
     406           3 :   void leave(const pbes_equation& x)
     407             : #else
     408             :   void leave(const pbes_equation&)
     409             : #endif
     410             :   {
     411           3 :     fixpoint_symbol symbol = symbol_stack.top();
     412           3 :     symbol_stack.pop();
     413           3 :     assert(symbol==x.symbol());
     414           3 :     propositional_variable variable = variable_stack.top();
     415           3 :     variable_stack.pop();
     416           3 :     assert(variable==x.variable());
     417           3 :     mode_stack.pop();
     418           3 :     pbes_expression expr = expression_stack.top();
     419           3 :     pbes_equation e(symbol, variable, expr);
     420           3 :     equations.push_back(e);
     421           3 :     expression_stack.pop();
     422           3 :   }
     423             : 
     424             : };
     425             : /// \endcond
     426             : 
     427             : /// \brief Rewrites a PBES to a PPG.
     428             : /// \param x a PBES
     429             : /// \return a PPG.
     430             : inline
     431           1 : pbes to_ppg(pbes x)
     432             : {
     433           1 :   algorithms::normalize(x);
     434           1 :   ppg_rewriter f(x.equations());
     435           1 :   f.apply(x);
     436             :   pbes result(
     437           1 :       x.data(),
     438             :       f.equations,
     439           2 :       x.initial_state());
     440           2 :   return result;
     441           1 : }
     442             : 
     443             : } // namespace detail
     444             : 
     445             : } // namespace pbes_system
     446             : 
     447             : } // namespace mcrl2
     448             : 
     449             : #endif // MCRL2_PBES_DETAIL_PPG_REWRITER_H