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 pbes/include/mcrl2/pbes/pbes_functions.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_PBES_FUNCTIONS_H
      13             : #define MCRL2_PBES_PBES_FUNCTIONS_H
      14             : 
      15             : #include "mcrl2/pbes/traverser.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace pbes_system {
      20             : 
      21             : /// \brief Visitor for printing the root node of a PBES.
      22             : struct print_brief_traverser: public pbes_expression_traverser<print_brief_traverser>
      23             : {
      24             :   typedef pbes_expression_traverser<print_brief_traverser> super;
      25             :   using super::enter;
      26             :   using super::leave;
      27             :   using super::apply;
      28             : 
      29             :   std::string result;
      30             : 
      31             :   print_brief_traverser()
      32             :     : result("")
      33             :   {}
      34             : 
      35             :   void apply(const not_& /* x */)
      36             :   {
      37             :     result = "not";
      38             :   }
      39             : 
      40             :   void apply(const imp& /* x */)
      41             :   {
      42             :     result = "imp";
      43             :   }
      44             : 
      45             :   void apply(const forall& /* x */)
      46             :   {
      47             :     result = "forall";
      48             :   }
      49             : 
      50             :   void apply(const exists& /* x */)
      51             :   {
      52             :     result = "exists";
      53             :   }
      54             : 
      55             :   void apply(const propositional_variable_instantiation& x)
      56             :   {
      57             :     result = "propvar " + std::string(x.name());
      58             :   }
      59             : 
      60             :   void apply(const pbes_equation& x)
      61             :   {
      62             :     result = "equation " + std::string(x.variable().name());
      63             :   }
      64             : };
      65             : 
      66             : /// \brief Returns a string representation of the root node of a PBES.
      67             : /// \param x a PBES object
      68             : template <typename T>
      69             : std::string print_brief(const T& x)
      70             : {
      71             :   print_brief_traverser f;
      72             :   f.apply(x);
      73             :   return f.result;
      74             : }
      75             : 
      76             : 
      77             : /// \cond INTERNAL_DOCS
      78             : /// \brief Visitor for checking if a pbes object is a simple pbes expression.
      79             : struct is_simple_expression_traverser: public pbes_expression_traverser<is_simple_expression_traverser>
      80             : {
      81             :   typedef pbes_expression_traverser<is_simple_expression_traverser> super;
      82             :   using super::enter;
      83             :   using super::leave;
      84             :   using super::apply;
      85             : 
      86             :   bool result;
      87             : 
      88        1038 :   is_simple_expression_traverser()
      89        1038 :     : result(true)
      90        1038 :   {}
      91             : 
      92        1057 :   void enter(const propositional_variable_instantiation& /*x*/)
      93             :   {
      94        1057 :     result = false;
      95        1057 :   }
      96             : };
      97             : /// \endcond
      98             : 
      99             : /// \brief Determines if an expression is a simple expression.
     100             : /// An expression is simple if it is free of propositional variables.
     101             : /// \param x a PBES object
     102             : /// \return true if x is a simple expression.
     103             : template <typename T>
     104        1038 : bool is_simple_expression(const T& x)
     105             : {
     106        1038 :   is_simple_expression_traverser f;
     107        1038 :   f.apply(x);
     108        1038 :   return f.result;
     109             : }
     110             : 
     111             : /// \brief Test for a disjunction
     112             : /// \param t A PBES expression
     113             : /// \return True if it is a disjunction and not a simple expression
     114         342 : inline bool is_non_simple_disjunct(const pbes_expression& t)
     115             : {
     116         342 :   return is_pbes_or(t) && !is_simple_expression(t);
     117             : }
     118             : 
     119             : /// \brief Test for a conjunction
     120             : /// \param t A PBES expression
     121             : /// \return True if it is a conjunction and not a simple expression
     122          33 : inline bool is_non_simple_conjunct(const pbes_expression& t)
     123             : {
     124          33 :   return is_pbes_and(t) && !is_simple_expression(t);
     125             : }
     126             : 
     127             : /// \brief Splits a disjunction into a sequence of operands.
     128             : /// Given a pbes expression of the form p1 || p2 || .... || pn, this will yield a
     129             : /// set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main
     130             : /// function symbol.
     131             : /// \param expr A PBES expression.
     132             : /// \param split_simple_expr If true, pbes disjuncts are split, even if
     133             : ///        no proposition variables occur. If false, pbes disjuncts are only split
     134             : ///        if a proposition variable occurs somewhere in \a expr.
     135             : /// \note This never splits data disjuncts.
     136             : /// \return A sequence of operands.
     137             : inline
     138          98 : std::vector<pbes_expression> split_disjuncts(const pbes_expression& expr, bool split_simple_expr = false)
     139             : {
     140             :   using namespace accessors;
     141          98 :   std::vector<pbes_expression> result;
     142             : 
     143          98 :   if (split_simple_expr)
     144             :   {
     145           0 :     utilities::detail::split(expr, std::back_insert_iterator<std::vector<pbes_expression> >(result), is_or, left, right);
     146             :   }
     147             :   else
     148             :   {
     149          98 :     utilities::detail::split(expr, std::back_insert_iterator<std::vector<pbes_expression> >(result), is_non_simple_disjunct, left, right);
     150             :   }
     151             : 
     152          98 :   return result;
     153           0 : }
     154             : 
     155             : /// \brief Splits a conjunction into a sequence of operands
     156             : /// Given a pbes expression of the form p1 && p2 && .... && pn, this will yield a
     157             : /// set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main
     158             : /// function symbol.
     159             : /// \param expr A PBES expression
     160             : /// \param split_simple_expr If true, pbes conjuncts are split, even if
     161             : ///        no proposition variables occur. If false, pbes conjuncts are only split
     162             : ///        if a proposition variable occurs somewhere in \a expr.
     163             : /// \note This never splits data conjuncts.
     164             : /// \return A sequence of operands
     165             : inline
     166           9 : std::vector<pbes_expression> split_conjuncts(const pbes_expression& expr, bool split_simple_expr = false)
     167             : {
     168             :   using namespace accessors;
     169           9 :   std::vector<pbes_expression> result;
     170             : 
     171           9 :   if (split_simple_expr)
     172             :   {
     173           0 :     utilities::detail::split(expr, std::back_insert_iterator<std::vector<pbes_expression> >(result), is_and, left, right);
     174             :   }
     175             :   else
     176             :   {
     177           9 :     utilities::detail::split(expr, std::back_insert_iterator<std::vector<pbes_expression> >(result), is_non_simple_conjunct, left, right);
     178             :   }
     179             : 
     180           9 :   return result;
     181           0 : }
     182             : 
     183             : } // namespace pbes_system
     184             : 
     185             : } // namespace mcrl2
     186             : 
     187             : #endif // MCRL2_PBES_PBES_FUNCTIONS_H