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_TRAVERSER_H
      14             : #define MCRL2_PBES_DETAIL_PPG_TRAVERSER_H
      15             : 
      16             : #include "mcrl2/pbes/pbes_functions.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22             : namespace detail {
      23             : 
      24             : /// \cond INTERNAL_DOCS
      25             : /// \brief Visitor for checking if a pbes object is a PPG.
      26             : struct ppg_traverser: public pbes_expression_traverser<ppg_traverser>
      27             : {
      28             :   typedef pbes_expression_traverser<ppg_traverser> super;
      29             :   using super::enter;
      30             :   using super::leave;
      31             :   using super::apply;
      32             : 
      33             :   enum expression_mode {
      34             :     CONJUNCTIVE, UNIVERSAL,
      35             :     DISJUNCTIVE, EXISTENTIAL,
      36             :     UNDETERMINED
      37             :   };
      38             : 
      39             :   std::string print_mode(expression_mode mode)
      40             :   {
      41             :     switch(mode)
      42             :     {
      43             :     case CONJUNCTIVE:
      44             :       return "Conjunctive";
      45             :       break;
      46             :     case UNIVERSAL:
      47             :       return "Universal";
      48             :       break;
      49             :     case DISJUNCTIVE:
      50             :       return "Disjunctive";
      51             :       break;
      52             :     case EXISTENTIAL:
      53             :       return "Existential";
      54             :       break;
      55             :     case UNDETERMINED:
      56             :       return "Undetermined";
      57             :       break;
      58             :     default:
      59             :       throw(std::runtime_error("Unknown mode!"));
      60             :     }
      61             :   }
      62             : 
      63             :   bool result;
      64             :   std::stack<expression_mode> mode_stack;
      65             : 
      66          14 :   ppg_traverser()
      67          14 :     : result(true)
      68          14 :   {}
      69             : 
      70           0 :   void enter(const not_& x)
      71             :   {
      72           0 :     result = result && is_simple_expression(x);
      73           0 :   }
      74             : 
      75           0 :   void enter(const imp& x)
      76             :   {
      77           0 :     result = result && is_simple_expression(x);
      78           0 :   }
      79             : 
      80          36 :   void enter(const pbes_system::forall& x)
      81             :   {
      82          36 :     expression_mode mode = mode_stack.top();
      83          36 :     bool simple_body = is_simple_expression(x.body());
      84          36 :     if (!simple_body)
      85             :     {
      86             :       //std::clog << "Note: 'forall' in mode " << print_mode(mode) << std::endl;
      87          36 :       switch(mode)
      88             :       {
      89          28 :       case UNDETERMINED:
      90             :       case CONJUNCTIVE:
      91          28 :         mode = UNIVERSAL;
      92          36 :       case UNIVERSAL:
      93          36 :         break;
      94           0 :       case DISJUNCTIVE:
      95             :       case EXISTENTIAL:
      96           0 :         result = false;
      97           0 :         break;
      98           0 :       default:
      99           0 :         break;
     100             :       }
     101             :     }
     102          36 :     mode_stack.push(mode);
     103          36 :   }
     104             : 
     105          36 :   void leave(const pbes_system::forall& /*x*/)
     106             :   {
     107          36 :     mode_stack.pop();
     108          36 :   }
     109             : 
     110           4 :   void enter(const pbes_system::exists& x)
     111             :   {
     112           4 :     expression_mode mode = mode_stack.top();
     113           4 :     bool simple_body = is_simple_expression(x.body());
     114           4 :     if (!simple_body)
     115             :     {
     116             :       //std::clog << "Note: 'exists' in mode " << print_mode(mode) << std::endl;
     117           4 :       switch(mode)
     118             :       {
     119           2 :       case UNDETERMINED:
     120             :       case DISJUNCTIVE:
     121           2 :         mode = EXISTENTIAL;
     122           2 :       case EXISTENTIAL:
     123           2 :         break;
     124           2 :       case CONJUNCTIVE:
     125             :       case UNIVERSAL:
     126             :         //std::clog << "Invalid: 'exists' in mode " << print_mode(mode) << std::endl;
     127           2 :         result = false;
     128           2 :         break;
     129           0 :       default:
     130           0 :         break;
     131             :       }
     132             :     }
     133           4 :     mode_stack.push(mode);
     134           4 :   }
     135             : 
     136           4 :   void leave(const pbes_system::exists& /*x*/)
     137             :   {
     138           4 :     mode_stack.pop();
     139           4 :   }
     140             : 
     141          64 :   void enter(const pbes_system::and_& x)
     142             :   {
     143          64 :     expression_mode mode = mode_stack.top();
     144          64 :     bool is_simple = is_simple_expression(x);
     145          64 :     if (!is_simple)
     146             :     {
     147             :       //std::clog << "Note: 'and' in mode " << print_mode(mode) << std::endl;
     148          64 :       switch(mode)
     149             :       {
     150          22 :       case UNDETERMINED:
     151          22 :         mode = CONJUNCTIVE;
     152             :         //std::clog << "Note: to mode " << print_mode(mode) << std::endl;
     153          61 :       case CONJUNCTIVE:
     154          61 :         break;
     155           0 :       case UNIVERSAL:
     156             :         //std::clog << "and: " << core::pp(x) << std::endl;
     157             :         //std::clog << "Invalid: 'and' in mode " << print_mode(mode) << std::endl;
     158           0 :         result = false;
     159           0 :         break;
     160           3 :       case EXISTENTIAL:
     161             :       case DISJUNCTIVE:
     162             :       {
     163           3 :         std::size_t count = 0;
     164           3 :         std::vector<pbes_expression> conjuncts = split_conjuncts(x);
     165          10 :         for(const pbes_expression& conjunct : conjuncts)
     166             :         {
     167           7 :           if (!is_simple_expression(conjunct))
     168             :           {
     169             :             //std::clog << "and: " << core::pp(*it) << std::endl;
     170           3 :             count++;
     171           3 :             if (count > 1 || !is_propositional_variable_instantiation(conjunct))
     172             :             {
     173             :               //std::clog << "Invalid: 'and' in mode " << print_mode(mode) << std::endl;
     174           0 :               result = false;
     175           0 :               break;
     176             :             }
     177             :           }
     178             :         }
     179           3 :         break;
     180           3 :       }
     181           0 :       default:
     182           0 :         break;
     183             :       }
     184             :     }
     185          64 :     mode_stack.push(mode);
     186          64 :   }
     187             : 
     188          64 :   void leave(const pbes_system::and_& /*x*/)
     189             :   {
     190          64 :     mode_stack.pop();
     191          64 :   }
     192             : 
     193         100 :   void enter(const pbes_system::or_& x)
     194             :   {
     195         100 :     expression_mode mode = mode_stack.top();
     196         100 :     bool is_simple = is_simple_expression(x);
     197         100 :     if (!is_simple)
     198             :     {
     199             :       //std::clog << "Note: 'or' in mode " << print_mode(mode) << std::endl;
     200          96 :       switch(mode)
     201             :       {
     202           0 :       case UNDETERMINED:
     203           0 :         mode = DISJUNCTIVE;
     204           0 :       case DISJUNCTIVE:
     205           0 :         break;
     206           0 :       case EXISTENTIAL:
     207             :         //std::clog << "Invalid: 'or' in mode " << print_mode(mode) << std::endl;
     208           0 :         result = false;
     209           0 :         break;
     210          96 :       case UNIVERSAL:
     211             :       case CONJUNCTIVE:
     212             :       {
     213          96 :         std::size_t count = 0;
     214          96 :         std::vector<pbes_expression>  disjuncts = split_disjuncts(x);
     215         312 :         for(const pbes_expression& disjunct : disjuncts)
     216             :         {
     217         216 :           if (!is_simple_expression(disjunct))
     218             :           {
     219          96 :             count++;
     220          96 :             if (count > 1 || !is_propositional_variable_instantiation(disjunct))
     221             :             {
     222             :               ///std::clog << "Invalid: 'or' in mode " << print_mode(mode) << std::endl;
     223           0 :               result = false;
     224           0 :               break;
     225             :             }
     226             :           }
     227             :         }
     228          96 :         break;
     229          96 :       }
     230           0 :       default:
     231           0 :         break;
     232             :       }
     233             :     }
     234         100 :     mode_stack.push(mode);
     235         100 :   }
     236             : 
     237         100 :   void leave(const pbes_system::or_& /*x*/)
     238             :   {
     239         100 :     mode_stack.pop();
     240         100 :   }
     241             : 
     242          32 :   void enter(const pbes_equation& /*x*/)
     243             :   {
     244             :     //std::clog << "Equation " << x.variable().name() << std::endl;
     245          32 :     mode_stack.push(UNDETERMINED);
     246          32 :   }
     247             : 
     248          32 :   void leave(const pbes_equation& /*x*/)
     249             :   {
     250          32 :     mode_stack.pop();
     251          32 :   }
     252             : 
     253             : };
     254             : /// \endcond
     255             : 
     256             : /// \brief Determines if an expression is a PPG expression.
     257             : /// \param x a PBES object
     258             : /// \return true if x is a PPG expression.
     259             : template <typename T>
     260          14 : bool is_ppg(const T& x)
     261             : {
     262          14 :   ppg_traverser f;
     263          14 :   f.apply(x);
     264          14 :   return f.result;
     265          14 : }
     266             : 
     267             : } // namespace detail
     268             : 
     269             : } // namespace pbes_system
     270             : 
     271             : } // namespace mcrl2
     272             : 
     273             : #endif // MCRL2_PBES_DETAIL_PPG_TRAVERSER_H