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 mcrl2/lps/is_stochastic.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_IS_STOCHASTIC_H
      13             : #define MCRL2_LPS_IS_STOCHASTIC_H
      14             : 
      15             : #include "mcrl2/lps/traverser.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace lps {
      20             : 
      21             : namespace detail {
      22             : 
      23             : struct is_stochastic_traverser: public lps::data_expression_traverser<is_stochastic_traverser>
      24             : {
      25             :   typedef lps::data_expression_traverser<is_stochastic_traverser> super;
      26             :   using super::enter;
      27             :   using super::leave;
      28             :   using super::apply;
      29             : 
      30             :   bool result;
      31             : 
      32         206 :   is_stochastic_traverser()
      33         206 :     : result(false)
      34         206 :   {}
      35             : 
      36         692 :   void apply(const lps::stochastic_distribution& x)
      37             :   {
      38         692 :     if (x.is_defined())
      39             :     {
      40         135 :       result = true;
      41             :     }
      42         692 :   }
      43             : 
      44             : };
      45             : 
      46             : } // namespace detail
      47             : 
      48             : /// \brief Returns true if the LPS object x contains a stochastic distribution in one of its attributes.
      49             : template <typename T>
      50         206 : bool is_stochastic(const T& x)
      51             : {
      52         206 :   detail::is_stochastic_traverser f;
      53         206 :   f.apply(x);
      54         206 :   return f.result;
      55             : }
      56             : 
      57             : } // namespace lps
      58             : 
      59             : } // namespace mcrl2
      60             : 
      61             : #endif // MCRL2_LPS_IS_STOCHASTIC_H