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_visitor.h
      10             : /// \brief Visitor 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             : ///
      14             : /// DEPRECATED
      15             : #ifndef MCRL2_PBES_DETAIL_PPG_VISITOR_H
      16             : #define MCRL2_PBES_DETAIL_PPG_VISITOR_H
      17             : 
      18             : #include "mcrl2/pbes/detail/bqnf_visitor.h"
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace pbes_system {
      23             : 
      24             : namespace detail {
      25             : 
      26             : class ppg_visitor
      27             :   {
      28             :   public:
      29             :     /// \brief The BQNF visitor type.
      30             :     typedef bqnf_visitor bqnf;
      31             : 
      32             :     /// \brief Destructor.
      33           6 :     virtual ~ppg_visitor()
      34           6 :     { }
      35             : 
      36             :     /// \brief Constructor.
      37           6 :     ppg_visitor()
      38           6 :     { }
      39             : 
      40             :     /// \brief Returns a string representation of the type of the root node of the expression.
      41             :     /// \param e a PBES expression
      42             :     /// \return a string representation of the type of the root node of the expression.
      43             :     static std::string print_brief(const pbes_expression& e)
      44             :     {
      45             :       return bqnf::print_brief(e);
      46             :     }
      47             : 
      48             :     /// \brief Visits a simple expression.
      49             :     /// An expression is simple if it does not contain propositional variables.
      50             :     /// \param e a PBES expression
      51             :     /// \return true if the expression e is a simple expression.
      52           0 :     virtual bool visit_simple_expression(const pbes_expression& e)
      53             :     {
      54             :       //std::clog << "visit_simple_expression: " << print_brief(e) << std::endl;
      55           0 :       bool result = is_simple_expression(e);
      56           0 :       return result;
      57             :     }
      58             : 
      59             :     /// \brief Visits a propositional variable expression.
      60             :     /// \param e PBES expression
      61             :     /// \return true if the expression is a propositional variable or a simple expression.
      62           0 :     virtual bool visit_propositional_variable(const pbes_expression& e)
      63             :     {
      64             :       //std::clog << "visit_propositional_variable: " << print_brief(e) << std::endl;
      65           0 :       bool result = true;
      66           0 :       if (!(is_propositional_variable_instantiation(e) || visit_simple_expression(e))) {
      67             :         //std::clog << "Not a propositional variable or simple expression!" << std::endl;
      68           0 :         result = false;
      69             :       }
      70           0 :       return result;
      71             :     }
      72             : 
      73             :     /// \brief Visits a conjunctive expression within an inner existential quantifier expression.
      74             :     /// \param e a PBES expression
      75             :     /// \return true if the expression e conforms to PPG.
      76           0 :     virtual bool visit_inner_and(const pbes_expression& e)
      77             :     {
      78             :       //std::clog << "visit_inner_and: " << print_brief(e) << std::endl;
      79           0 :       bool result = true;
      80           0 :       if (is_and(e)) {
      81           0 :         pbes_expression l = pbes_system::accessors::left(e);
      82           0 :         pbes_expression r = pbes_system::accessors::right(e);
      83           0 :         if (visit_simple_expression(l)) {
      84           0 :           result &= visit_inner_and(r);
      85             :         } else {
      86           0 :           result &= visit_propositional_variable(e);
      87             :         }
      88           0 :       } else {
      89           0 :         result &= visit_propositional_variable(e);
      90             :       }
      91           0 :       return result;
      92             :     }
      93             : 
      94             :     /// \brief Visits a bounded existential quantifier expression within a disjunctive expression.
      95             :     /// \param e a PBES expression
      96             :     /// \return true if the expression e conforms to PPG.
      97           0 :     virtual bool visit_inner_bounded_exists(const pbes_expression& e)
      98             :     {
      99             :       //std::clog << "visit_inner_bounded_exists: " << print_brief(e) << std::endl;
     100           0 :       pbes_expression qexpr = e;
     101           0 :       data::variable_list qvars;
     102           0 :       while (is_exists(qexpr)) {
     103           0 :         qvars = qvars + quantifier_variables(qexpr);
     104           0 :         qexpr = pbes_system::accessors::arg(qexpr);
     105             :       }
     106           0 :       return visit_inner_and(qexpr);
     107           0 :     }
     108             : 
     109             :     /// \brief Visits a disjunctive expression.
     110             :     /// \param e a PBES expression
     111             :     /// \return true if the expression e conforms to PPG.
     112           0 :     virtual bool visit_or(const pbes_expression& e)
     113             :     {
     114             :       //std::clog << "visit_or: " << print_brief(e) << std::endl;
     115           0 :       bool result = true;
     116           0 :       if (is_or(e)) {
     117           0 :         pbes_expression l = pbes_system::accessors::left(e);
     118           0 :         pbes_expression r = pbes_system::accessors::right(e);
     119           0 :         result &= visit_or(l);
     120           0 :         result &= visit_or(r);
     121           0 :       } else {
     122           0 :         result &= visit_inner_bounded_exists(e);
     123             :       }
     124           0 :       return result;
     125             :     }
     126             : 
     127             :     /// \brief Visits a disjunctive expression within an inner universal quantifier expression.
     128             :     /// \param e a PBES expression
     129             :     /// \return true if the expression e conforms to PPG.
     130           0 :     virtual bool visit_inner_implies(const pbes_expression& e)
     131             :     {
     132             :       //std::clog << "visit_inner_implies: " << print_brief(e) << std::endl;
     133           0 :       bool result = true;
     134           0 :       if (is_or(e) || is_imp(e)) {
     135           0 :         pbes_expression l = pbes_system::accessors::left(e);
     136           0 :         pbes_expression r = pbes_system::accessors::right(e);
     137           0 :         if (visit_simple_expression(l)) {
     138           0 :           result &= visit_inner_implies(r);
     139             :         } else {
     140           0 :           result &= visit_propositional_variable(e);
     141             :         }
     142           0 :       } else {
     143           0 :         result &= visit_propositional_variable(e);
     144             :       }
     145           0 :       return result;
     146             :     }
     147             : 
     148             :     /// \brief Visits a bounded universal quantifier expression within a conjunctive expression.
     149             :     /// \param e a PBES expression
     150             :     /// \return true if the expression e conforms to PPG.
     151           0 :     virtual bool visit_inner_bounded_forall(const pbes_expression& e)
     152             :     {
     153             :       //std::clog << "visit_inner_bounded_forall: " << print_brief(e) << std::endl;
     154           0 :       pbes_expression qexpr = e;
     155           0 :       data::variable_list qvars;
     156           0 :       while (is_forall(qexpr)) {
     157           0 :         qvars = qvars + quantifier_variables(qexpr);
     158           0 :         qexpr = pbes_system::accessors::arg(qexpr);
     159             :       }
     160           0 :       return visit_inner_implies(qexpr);
     161           0 :     }
     162             : 
     163             :     /// \brief Visits a conjunctive expression.
     164             :     /// \param e a PBES expression
     165             :     /// \return true if the expression e conforms to PPG.
     166           0 :     virtual bool visit_and(const pbes_expression& e)
     167             :     {
     168             :       //std::clog << "visit_and: " << print_brief(e) << std::endl;
     169           0 :       bool result = true;
     170           0 :       if (is_and(e)) {
     171           0 :         pbes_expression l = pbes_system::accessors::left(e);
     172           0 :         pbes_expression r = pbes_system::accessors::right(e);
     173           0 :         result &= visit_and(l);
     174           0 :         result &= visit_and(r);
     175           0 :       } else {
     176           0 :         result &= visit_inner_bounded_forall(e);
     177             :       }
     178           0 :       return result;
     179             :     }
     180             : 
     181             :     /// \brief Visits a PPG expression.
     182             :     /// \param e a PBES expression
     183             :     /// \return true if the expression e is in PPG form.
     184           0 :     virtual bool visit_ppg_expression(const pbes_expression& e)
     185             :     {
     186             :       //std::clog << "visit_ppg_expression." << std::endl;
     187           0 :       bool result = true;
     188           0 :       if (visit_propositional_variable(e)) {
     189           0 :         result = true;
     190           0 :       } else if (is_and(e)) {
     191           0 :         result &= visit_inner_and(e) || visit_and(e);
     192           0 :       } else if (is_or(e)) {
     193           0 :         result &= visit_inner_implies(e) || visit_or(e);
     194           0 :       } else if (is_imp(e)) {
     195           0 :         result &= visit_inner_implies(e);
     196           0 :       } else if (is_forall(e)) {
     197           0 :         result &= visit_inner_bounded_forall(e);
     198           0 :       } else if (is_exists(e)) {
     199           0 :         result &= visit_inner_bounded_exists(e);
     200             :       } else {
     201             : 
     202             :       }
     203             :       //std::clog << "visit_ppg_expression: equation is " << (result ? "" : "NOT ") << "in PPG form." << std::endl;
     204           0 :       return result;
     205             :     }
     206             :   };
     207             : 
     208             : } // namespace detail
     209             : 
     210             : } // namespace pbes_system
     211             : 
     212             : } // namespace mcrl2
     213             : 
     214             : #endif // MCRL2_PBES_DETAIL_PPG_VISITOR_H