LCOV - code coverage report
Current view: top level - modal_formula/include/mcrl2/modal_formula/detail - state_variable_context.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 14 15 93.3 %
Date: 2019-09-14 00:54:39 Functions: 6 6 100.0 %
Legend: Lines: hit not hit

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

Generated by: LCOV version 1.12