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/modal_formula/detail/state_variable_context.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_DETAIL_STATE_VARIABLE_CONTEXT_H
      13             : #define MCRL2_MODAL_FORMULA_DETAIL_STATE_VARIABLE_CONTEXT_H
      14             : 
      15             : #include "mcrl2/data/detail/data_utility.h"
      16             : #include "mcrl2/data/sort_type_checker.h"
      17             : #include "mcrl2/modal_formula/state_formula.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace state_formulas {
      22             : 
      23             : namespace detail {
      24             : 
      25             : class state_variable_context
      26             : {
      27             :   private:
      28             :     std::map<core::identifier_string, data::sort_expression_list> m_state_variables;
      29             : 
      30             :   public:
      31             :     bool is_declared(const core::identifier_string& name) const
      32             :     {
      33             :       return m_state_variables.find(name) != m_state_variables.end();
      34             :     }
      35             : 
      36         168 :     void add_state_variable(const core::identifier_string& name, const data::variable_list& parameters, const data::sort_type_checker& sort_typechecker)
      37             :     {
      38         168 :       data::sort_expression_list sorts = data::detail::parameter_sorts(parameters);
      39         183 :       for (const data::sort_expression& s: sorts)
      40             :       {
      41          15 :         sort_typechecker(s);
      42             :       }
      43         168 :       m_state_variables[name] = sorts;
      44         168 :     }
      45             : 
      46         143 :     data::sort_expression_list matching_state_variable_sorts(const core::identifier_string& name, const data::data_expression_list& arguments) const
      47             :     {
      48         143 :       auto i = m_state_variables.find(name);
      49         143 :       if (i == m_state_variables.end())
      50             :       {
      51           1 :         throw mcrl2::runtime_error("undefined state variable " + core::pp(name) + " with arguments " + data::pp(arguments));
      52             :       }
      53         142 :       const data::sort_expression_list& result = i->second;
      54         142 :       if (result.size() != arguments.size())
      55             :       {
      56           0 :         throw mcrl2::runtime_error("incorrect number of arguments for state variable " + core::pp(name));
      57             :       }
      58         284 :       return result;
      59             :     }
      60             : 
      61             :     void clear()
      62             :     {
      63             :       m_state_variables.clear();
      64             :     }
      65             : };
      66             : 
      67             : } // namespace detail
      68             : 
      69             : } // namespace state_formulas
      70             : 
      71             : } // namespace mcrl2
      72             : 
      73             : #endif // MCRL2_MODAL_FORMULA_DETAIL_STATE_VARIABLE_CONTEXT_H