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 pbes/include/mcrl2/pbes/is_bes.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_IS_BES_H
      13             : #define MCRL2_PBES_IS_BES_H
      14             : 
      15             : #include "mcrl2/data/consistency.h"
      16             : #include "mcrl2/pbes/traverser.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22             : /// \cond INTERNAL_DOCS
      23             : /// \brief Visitor for checking if a pbes object is in BES form.
      24             : struct is_bes_traverser: public pbes_expression_traverser<is_bes_traverser>
      25             : {
      26             :   typedef pbes_expression_traverser<is_bes_traverser> super;
      27             :   using super::enter;
      28             :   using super::leave;
      29             :   using super::apply;
      30             : 
      31             :   bool result;
      32             : 
      33           4 :   is_bes_traverser()
      34           4 :     : result(true)
      35           4 :   {}
      36             : 
      37           4 :   void enter(const forall& /* x */)
      38             :   {
      39           4 :     result = false;
      40           4 :   }
      41             : 
      42           0 :   void enter(const exists& /* x */)
      43             :   {
      44           0 :     result = false;
      45           0 :   }
      46             : 
      47           3 :   void enter(const data::data_expression& x)
      48             :   {
      49           3 :     if (x != data::true_() && x != data::false_())
      50             :     {
      51           2 :       result = false;
      52             :     }
      53           3 :   }
      54             : 
      55          92 :   void enter(const propositional_variable_instantiation& x)
      56             :   {
      57          92 :     if (result)
      58             :     {
      59          92 :       result = x.parameters().empty();
      60             :     }
      61          92 :   }
      62             : 
      63          76 :   void enter(const pbes_equation& x)
      64             :   {
      65          76 :     if (result)
      66             :     {
      67          76 :       result = x.variable().parameters().empty();
      68             :     }
      69          76 :   }
      70             : };
      71             : /// \endcond
      72             : 
      73             : /// \brief Returns true if a PBES object is in BES form.
      74             : /// \param x a PBES object
      75             : template <typename T>
      76           4 : bool is_bes(const T& x)
      77             : {
      78           4 :   is_bes_traverser f;
      79           4 :   f.apply(x);
      80           4 :   return f.result;
      81             : }
      82             : 
      83             : } // namespace pbes_system
      84             : 
      85             : } // namespace mcrl2
      86             : 
      87             : #endif // MCRL2_PBES_IS_BES_H