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/detail/action_utility.h
      10             : /// \brief Add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_DETAIL_ACTION_UTILITY_H
      13             : #define MCRL2_LPS_DETAIL_ACTION_UTILITY_H
      14             : 
      15             : #include "mcrl2/data/detail/data_utility.h"
      16             : #include "mcrl2/process/process_expression.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace lps
      22             : {
      23             : 
      24             : namespace detail
      25             : {
      26             : 
      27             : /// \brief Returns true if the sorts of the given actions are contained in sorts.
      28             : /// \param actions A sequence of actions
      29             : /// \param sorts A set of sort expressions
      30             : /// \return True if the sorts of the given actions are contained in sorts.
      31             : inline
      32             : bool check_action_sorts(const process::action_list& actions, const std::set<data::sort_expression>& sorts)
      33             : {
      34             :   for (const process::action& a: actions)
      35             :   {
      36             :     for (const data::sort_expression& s: a.label().sorts())
      37             :     {
      38             :       if (!data::detail::check_sort(s, sorts))
      39             :       {
      40             :         return false;
      41             :       }
      42             :     }
      43             :   }
      44             :   return true;
      45             : }
      46             : 
      47             : /// \brief Returns true if the labels of the given actions are contained in labels.
      48             : /// \param actions A sequence of actions
      49             : /// \param labels A set of action labels
      50             : /// \return True if the labels of the given actions are contained in labels.
      51             : inline
      52        1498 : bool check_action_labels(const process::action_list& actions, const std::set<process::action_label>& labels)
      53             : {
      54             :   using utilities::detail::contains;
      55        3328 :   for (const process::action& a: actions)
      56             :   {
      57        1830 :     if (!contains(labels, a.label()))
      58             :     {
      59           0 :       return false;
      60             :     }
      61             :   }
      62        1498 :   return true;
      63             : }
      64             : 
      65             : /// \brief Returns true if the sorts of the given action labels are contained in sorts.
      66             : /// \param action_labels A sequence of action labels
      67             : /// \param sorts A set of sort expressions
      68             : /// \return True if the sorts of the given action labels are contained in sorts.
      69             : inline
      70         634 : bool check_action_label_sorts(const process::action_label_list& action_labels, const std::set<data::sort_expression>& sorts)
      71             : {
      72        2038 :   for (const process::action_label& label: action_labels)
      73             :   {
      74        2161 :     for (const data::sort_expression& s: label.sorts())
      75             :     {
      76         757 :       if (!data::detail::check_sort(s, sorts))
      77             :       {
      78           0 :         return false;
      79             :       }
      80             :     }
      81             :   }
      82         634 :   return true;
      83             : }
      84             : 
      85             : } // namespace detail
      86             : 
      87             : } // namespace lps
      88             : 
      89             : } // namespace mcrl2
      90             : 
      91             : #endif // MCRL2_LPS_DETAIL_ACTION_UTILITY_H