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/process/is_guarded.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_IS_GUARDED_H
      13             : #define MCRL2_PROCESS_IS_GUARDED_H
      14             : 
      15             : #include "mcrl2/process/find.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace process {
      20             : 
      21             : namespace detail {
      22             : 
      23             : bool is_guarded(const process_expression& x, const std::vector<process_equation>& equations, std::set<process_identifier>& W);
      24             : 
      25             : struct is_guarded_traverser: public process_expression_traverser<is_guarded_traverser>
      26             : {
      27             :   typedef process_expression_traverser<is_guarded_traverser> super;
      28             :   using super::enter;
      29             :   using super::leave;
      30             :   using super::apply;
      31             : 
      32             :   const std::vector<process_equation>& equations;
      33             :   std::set<process_identifier>& W;
      34             :   bool result;
      35             : 
      36          16 :   is_guarded_traverser(const std::vector<process_equation>& equations_, std::set<process_identifier>& W_)
      37          16 :     : equations(equations_), W(W_), result(true)
      38          16 :   {}
      39             : 
      40             :   // P(e1, ..., en)
      41           9 :   void enter(const process::process_instance& x)
      42             :   {
      43             :     using utilities::detail::contains;
      44           9 :     if (!contains(W, x.identifier()))
      45             :     {
      46           8 :       W.insert(x.identifier());
      47           8 :       const process_equation& eqn = find_equation(equations, x.identifier());
      48           8 :       result = result && is_guarded(eqn.expression(), equations, W);
      49             :     }
      50             :     else
      51             :     {
      52           1 :       result = false;
      53             :     }
      54           9 :   }
      55             : 
      56             :   // P(d1 = e1, ..., dn = en)
      57           0 :   void enter(const process::process_instance_assignment& x)
      58             :   {
      59             :     using utilities::detail::contains;
      60           0 :     if (!contains(W, x.identifier()))
      61             :     {
      62           0 :       W.insert(x.identifier());
      63           0 :       const process_equation& eqn = find_equation(equations, x.identifier());
      64           0 :       result = result && is_guarded(eqn.expression(), equations, W);
      65             :     }
      66             :     else
      67             :     {
      68           0 :       result = false;
      69             :     }
      70           0 :   }
      71             : 
      72             :   // p . q
      73           6 :   void apply(const process::seq& x)
      74             :   {
      75           6 :     apply(x.left()); // only p needs to be guarded
      76           6 :   }
      77             : 
      78             :   // p << q
      79             :   void operator()(const process::bounded_init& x)
      80             :   {
      81             :     apply(x.left()); // only p needs to be guarded
      82             :   }
      83             : };
      84             : 
      85             : inline
      86          16 : bool is_guarded(const process_expression& x, const std::vector<process_equation>& equations, std::set<process_identifier>& W)
      87             : {
      88          16 :   detail::is_guarded_traverser f(equations, W);
      89          16 :   f.apply(x);
      90          16 :   return f.result;
      91             : }
      92             : 
      93             : } // namespace detail
      94             : 
      95             : /// \brief Checks if a process expression is guarded.
      96             : inline
      97           8 : bool is_guarded(const process_expression& x, const std::vector<process_equation>& equations)
      98             : {
      99           8 :   std::set<process_identifier> W;
     100          16 :   return detail::is_guarded(x, equations, W);
     101           8 : }
     102             : 
     103             : } // namespace process
     104             : 
     105             : } // namespace mcrl2
     106             : 
     107             : #endif // MCRL2_PROCESS_IS_GUARDED_H