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/detail/action_context.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_DETAIL_ACTION_CONTEXT_H
      13             : #define MCRL2_PROCESS_DETAIL_ACTION_CONTEXT_H
      14             : 
      15             : #include "mcrl2/data/typecheck.h"
      16             : #include "mcrl2/process/action_label.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace process {
      21             : 
      22             : namespace detail {
      23             : 
      24             : class action_context
      25             : {
      26             :   private:
      27             :     std::multimap<core::identifier_string, action_label> m_actions;
      28             : 
      29             :   public:
      30        6982 :     bool is_declared(const core::identifier_string& name) const
      31             :     {
      32        6982 :       return m_actions.find(name) != m_actions.end();
      33             :     }
      34             : 
      35             :     // Adds the elements of actions to action_map
      36             :     // Throws an exception if the sorts of the actions are not declared
      37             :     template <typename ActionLabelContainer>
      38        1348 :     void add_context_action_labels(const ActionLabelContainer& actions, const data::sort_type_checker& sort_typechecker)
      39             :     {
      40        6845 :       for (const process::action_label& a: actions)
      41             :       {
      42       11596 :         for (const data::sort_expression& s: a.sorts())
      43             :         {
      44        3298 :           sort_typechecker(s);
      45             :         }
      46             : 
      47             :         // Insert a in m_action_context; N.B. Before that check if it already exists
      48        4149 :         auto range = m_actions.equal_range(a.name());
      49        4149 :         if (range.first != m_actions.end())
      50             :         {
      51        1546 :           for (auto i = range.first; i != range.second; ++i)
      52             :           {
      53         546 :             if (i->second == a)
      54             :             {
      55           0 :               throw mcrl2::runtime_error("double declaration of action " + process::pp(a));
      56             :             }
      57             :           }
      58             :         }
      59        4149 :         m_actions.insert(range.first, std::make_pair(a.name(), a));
      60             :       }
      61        1348 :     }
      62             : 
      63         585 :     data::sorts_list matching_action_sorts(const core::identifier_string& name) const
      64             :     {
      65         585 :       auto range = m_actions.equal_range(name);
      66         585 :       assert(range.first != m_actions.end());
      67         585 :       data::sorts_list result;
      68        1278 :       for (auto k = range.first; k != range.second; ++k)
      69             :       {
      70         693 :         const action_label& a = k->second;
      71         693 :         result.push_front(a.sorts());
      72             :       }
      73        1170 :       return atermpp::reverse(result);
      74         585 :     }
      75             : 
      76        3082 :     data::sorts_list matching_action_sorts(const core::identifier_string& name, const data::data_expression_list& parameters) const
      77             :     {
      78        3082 :       data::sorts_list result;
      79        3082 :       auto range = m_actions.equal_range(name);
      80        6448 :       for (auto k = range.first; k != range.second; ++k)
      81             :       {
      82        3366 :         const action_label& a = k->second;
      83        3366 :         if (a.sorts().size() == parameters.size())
      84             :         {
      85        3218 :           result.push_front(a.sorts());
      86             :         }
      87             :       }
      88        6164 :       return atermpp::reverse(result);
      89        3082 :     }
      90             : 
      91        1142 :     void clear()
      92             :     {
      93        1142 :       m_actions.clear();
      94        1142 :     }
      95             : };
      96             : 
      97             : } // namespace detail
      98             : 
      99             : } // namespace process
     100             : 
     101             : } // namespace mcrl2
     102             : 
     103             : #endif // MCRL2_PROCESS_DETAIL_ACTION_CONTEXT_H