LCOV - code coverage report
Current view: top level - modal_formula/include/mcrl2/modal_formula - typecheck.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 125 182 68.7 %
Date: 2020-02-21 00:44:40 Functions: 35 44 79.5 %
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/typecheck.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_TYPECHECK_H
      13             : #define MCRL2_MODAL_FORMULA_TYPECHECK_H
      14             : 
      15             : #include "mcrl2/lps/typecheck.h"
      16             : #include "mcrl2/modal_formula/detail/state_variable_context.h"
      17             : #include "mcrl2/modal_formula/is_monotonous.h"
      18             : #include "mcrl2/modal_formula/normalize_sorts.h"
      19             : 
      20             : namespace mcrl2
      21             : {
      22             : 
      23             : namespace action_formulas
      24             : {
      25             : 
      26             : namespace detail
      27             : {
      28             : 
      29         207 : struct typecheck_builder: public action_formula_builder<typecheck_builder>
      30             : {
      31             :   typedef action_formula_builder<typecheck_builder> super;
      32             :   using super::apply;
      33             : 
      34             :   data::data_type_checker& m_data_type_checker;
      35             :   data::detail::variable_context m_variable_context;
      36             :   const process::detail::action_context& m_action_context;
      37             : 
      38         207 :   typecheck_builder(data::data_type_checker& data_typechecker,
      39             :                     const data::detail::variable_context& variable_context,
      40             :                     const process::detail::action_context& action_context
      41             :                    )
      42         207 :     : m_data_type_checker(data_typechecker),
      43             :       m_variable_context(variable_context),
      44         207 :       m_action_context(action_context)
      45         207 :   {}
      46             : 
      47         161 :   process::action typecheck_action(const core::identifier_string& name, const data::data_expression_list& parameters)
      48             :   {
      49         161 :     return process::typecheck_action(name, parameters, m_data_type_checker, m_variable_context, m_action_context);
      50             :   }
      51             : 
      52           0 :   action_formula apply(const data::data_expression& x)
      53             :   {
      54           0 :     return m_data_type_checker.typecheck_data_expression(x, data::sort_bool::bool_(), m_variable_context);
      55             :   }
      56             : 
      57           0 :   action_formula apply(const action_formulas::at& x)
      58             :   {
      59           0 :     data::data_expression new_time = m_data_type_checker.typecheck_data_expression(x.time_stamp(), data::sort_real::real_(), m_variable_context);
      60           0 :     return at((*this).apply(x.operand()), new_time);
      61             :   }
      62             : 
      63         161 :   action_formula apply(const process::untyped_multi_action& x)
      64             :   {
      65             :     // If x has size 1, first try to type check it as a data expression.
      66         161 :     if (x.actions().size() == 1)
      67             :     {
      68         161 :       const data::untyped_data_parameter& y = x.actions().front();
      69             :       try
      70             :       {
      71         161 :         return data::typecheck_untyped_data_parameter(m_data_type_checker, y.name(), y.arguments(), data::sort_bool::bool_(), m_variable_context);
      72             :       }
      73         161 :       catch (mcrl2::runtime_error& )
      74             :       {
      75             :         // skip
      76             :       }
      77             :     }
      78             :     // Type check it as a multi action
      79         322 :     process::action_list new_arguments;
      80         322 :     for (const data::untyped_data_parameter& a: x.actions())
      81             :     {
      82         161 :       new_arguments.push_front(typecheck_action(a.name(), a.arguments()));
      83             :     }
      84         161 :     new_arguments = atermpp::reverse(new_arguments);
      85         161 :     return action_formulas::multi_action(new_arguments);
      86             :   }
      87             : 
      88           3 :   action_formula apply(const action_formulas::forall& x)
      89             :   {
      90             :     try
      91             :     {
      92           6 :       auto m_variable_context_copy = m_variable_context;
      93           3 :       m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
      94           6 :       action_formula body = (*this).apply(x.body());
      95           3 :       m_variable_context = m_variable_context_copy;
      96           6 :       return forall(x.variables(), body);
      97             :     }
      98           0 :     catch (mcrl2::runtime_error& e)
      99             :     {
     100           0 :       throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + action_formulas::pp(x));
     101             :     }
     102             :   }
     103             : 
     104           2 :   action_formula apply(const action_formulas::exists& x)
     105             :   {
     106             :     try
     107             :     {
     108           4 :       auto m_variable_context_copy = m_variable_context;
     109           2 :       m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
     110           4 :       action_formula body = (*this).apply(x.body());
     111           2 :       m_variable_context = m_variable_context_copy;
     112           4 :       return exists(x.variables(), body);
     113             :     }
     114           0 :     catch (mcrl2::runtime_error& e)
     115             :     {
     116           0 :       throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + action_formulas::pp(x));
     117             :     }
     118             :   }
     119             : };
     120             : 
     121             : inline
     122         207 : typecheck_builder make_typecheck_builder(
     123             :                     data::data_type_checker& data_typechecker,
     124             :                     const data::detail::variable_context& variables,
     125             :                     const process::detail::action_context& actions
     126             :                    )
     127             : {
     128         207 :   return typecheck_builder(data_typechecker, variables, actions);
     129             : }
     130             : 
     131             : } // namespace detail
     132             : 
     133             : template <typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable> >
     134             : action_formula typecheck_action_formula(const action_formula& x,
     135             :                                         const data::data_specification& dataspec,
     136             :                                         const VariableContainer& variables,
     137             :                                         const ActionLabelContainer& actions
     138             :                                        )
     139             : {
     140             :   data::data_type_checker data_typechecker(dataspec);
     141             :   data::detail::variable_context variable_context;
     142             :   variable_context.add_context_variables(variables, data_typechecker);
     143             :   process::detail::action_context action_context;
     144             :   action_context.add_context_action_labels(actions, data_typechecker);
     145             :   return detail::make_typecheck_builder(data_typechecker, variable_context, action_context).apply(action_formulas::normalize_sorts(x, data_typechecker.typechecked_data_specification()));
     146             : }
     147             : 
     148             : inline
     149             : action_formula typecheck_action_formula(const action_formula& x, const lps::specification& lpsspec)
     150             : {
     151             :   return typecheck_action_formula(x, lpsspec.data(), lpsspec.global_variables(), lpsspec.action_labels());
     152             : }
     153             : 
     154             : } // namespace action_formulas
     155             : 
     156             : namespace regular_formulas
     157             : {
     158             : 
     159             : namespace detail
     160             : {
     161             : 
     162             : struct typecheck_builder: public regular_formula_builder<typecheck_builder>
     163             : {
     164             :   typedef regular_formula_builder<typecheck_builder> super;
     165             :   using super::apply;
     166             : 
     167             :   data::data_type_checker& m_data_type_checker;
     168             :   const data::detail::variable_context& m_variable_context;
     169             :   const process::detail::action_context& m_action_context;
     170             : 
     171         204 :   typecheck_builder(data::data_type_checker& data_typechecker,
     172             :                     const data::detail::variable_context& variables,
     173             :                     const process::detail::action_context& actions
     174             :                    )
     175         204 :     : m_data_type_checker(data_typechecker),
     176             :       m_variable_context(variables),
     177         204 :       m_action_context(actions)
     178         204 :   {}
     179             : 
     180           0 :   data::data_expression make_fbag_union(const data::data_expression& left, const data::data_expression& right)
     181             :   {
     182           0 :     const data::sort_expression& s = atermpp::down_cast<data::application>(left).head().sort();
     183           0 :     const data::container_sort& cs = atermpp::down_cast<data::container_sort>(s);
     184           0 :     return data::sort_fbag::union_(cs.element_sort(), left, right);
     185             :   }
     186             : 
     187           0 :   data::data_expression make_bag_union(const data::data_expression& left, const data::data_expression& right)
     188             :   {
     189           0 :     const data::sort_expression& s = atermpp::down_cast<data::application>(left).head().sort();
     190           0 :     const data::container_sort& cs = atermpp::down_cast<data::container_sort>(s);
     191           0 :     return data::sort_bag::union_(cs.element_sort(), left, right);
     192             :   }
     193             : 
     194           0 :   data::data_expression make_fset_union(const data::data_expression& left, const data::data_expression& right)
     195             :   {
     196           0 :     const data::sort_expression& s = atermpp::down_cast<data::application>(left).head().sort();
     197           0 :     const data::container_sort& cs = atermpp::down_cast<data::container_sort>(s);
     198           0 :     return data::sort_fset::union_(cs.element_sort(), left, right);
     199             :   }
     200             : 
     201           0 :   data::data_expression make_set_union(const data::data_expression& left, const data::data_expression& right)
     202             :   {
     203           0 :     const data::sort_expression& s = atermpp::down_cast<data::application>(left).head().sort();
     204           0 :     const data::container_sort& cs = atermpp::down_cast<data::container_sort>(s);
     205           0 :     return data::sort_set::union_(cs.element_sort(), left, right);
     206             :   }
     207             : 
     208           0 :   data::data_expression make_plus(const data::data_expression& left, const data::data_expression& right)
     209             :   {
     210           0 :     if (data::sort_real::is_real(left.sort()) || data::sort_real::is_real(right.sort()))
     211             :     {
     212           0 :       return data::sort_real::plus(left, right);
     213             :     }
     214           0 :     else if (data::sort_int::is_int(left.sort()) || data::sort_int::is_int(right.sort()))
     215             :     {
     216           0 :       return data::sort_int::plus(left, right);
     217             :     }
     218           0 :     else if (data::sort_nat::is_nat(left.sort()) || data::sort_nat::is_nat(right.sort()))
     219             :     {
     220           0 :       return data::sort_nat::plus(left, right);
     221             :     }
     222           0 :     else if (data::sort_pos::is_pos(left.sort()) || data::sort_pos::is_pos(right.sort()))
     223             :     {
     224           0 :       return data::sort_pos::plus(left, right);
     225             :     }
     226           0 :     else if (data::sort_bag::is_union_application(left) || data::sort_bag::is_union_application(right))
     227             :     {
     228           0 :       return make_bag_union(left, right);
     229             :     }
     230           0 :     else if (data::sort_fbag::is_union_application(left) || data::sort_fbag::is_union_application(right))
     231             :     {
     232           0 :       return make_fbag_union(left, right);
     233             :     }
     234           0 :     else if (data::sort_set::is_union_application(left) || data::sort_set::is_union_application(right))
     235             :     {
     236           0 :       return make_set_union(left, right);
     237             :     }
     238           0 :     else if (data::sort_fset::is_union_application(left) || data::sort_fset::is_union_application(right))
     239             :     {
     240           0 :       return make_fset_union(left, right);
     241             :     }
     242           0 :     throw mcrl2::runtime_error("could not typecheck " + data::pp(left) + " + " + data::pp(right));
     243             :   }
     244             : 
     245           0 :   data::data_expression make_element_at(const data::data_expression& left, const data::data_expression& right) const
     246             :   {
     247           0 :     const data::sort_expression& s = atermpp::down_cast<data::application>(left).head().sort();
     248           0 :     const data::container_sort& cs = atermpp::down_cast<data::container_sort>(s);
     249           0 :     return data::sort_list::element_at(cs.element_sort(), left, right);
     250             :   }
     251             : 
     252           3 :   regular_formula apply(const regular_formulas::untyped_regular_formula& x)
     253             :   {
     254           6 :     regular_formula left = (*this).apply(x.left());
     255           6 :     regular_formula right = (*this).apply(x.right());
     256           3 :     if (data::is_data_expression(left) && data::is_data_expression(right))
     257             :     {
     258           0 :       if (x.name() == core::identifier_string("."))
     259             :       {
     260           0 :         return make_element_at(atermpp::down_cast<data::data_expression>(left), atermpp::down_cast<data::data_expression>(right));
     261             :       }
     262             :       else
     263             :       {
     264           0 :         return make_plus(atermpp::down_cast<data::data_expression>(left), atermpp::down_cast<data::data_expression>(right));
     265             :       }
     266             :     }
     267             :     else
     268             :     {
     269           3 :       if (x.name() == core::identifier_string("."))
     270             :       {
     271           3 :         return seq(left, right);
     272             :       }
     273             :       else
     274             :       {
     275           0 :         return alt(left, right);
     276             :       }
     277             :     }
     278             :   }
     279             : 
     280         207 :   regular_formula apply(const action_formulas::action_formula& x)
     281             :   {
     282         207 :     return action_formulas::detail::make_typecheck_builder(m_data_type_checker, m_variable_context, m_action_context).apply(x);
     283             :   }
     284             : };
     285             : 
     286             : inline
     287         204 : typecheck_builder make_typecheck_builder(
     288             :                     data::data_type_checker& data_typechecker,
     289             :                     const data::detail::variable_context& variables,
     290             :                     const process::detail::action_context& actions
     291             :                    )
     292             : {
     293         204 :   return typecheck_builder(data_typechecker, variables, actions);
     294             : }
     295             : 
     296             : } // namespace detail
     297             : 
     298             : template <typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable> >
     299             : regular_formula typecheck_regular_formula(const regular_formula& x,
     300             :                                           const data::data_specification& dataspec,
     301             :                                           const VariableContainer& variables,
     302             :                                           const ActionLabelContainer& actions
     303             :                                          )
     304             : {
     305             :   data::data_type_checker data_typechecker(dataspec);
     306             :   data::detail::variable_context variable_context;
     307             :   variable_context.add_context_variables(variables, data_typechecker);
     308             :   process::detail::action_context action_context;
     309             :   action_context.add_context_action_labels(actions, data_typechecker);
     310             :   return detail::make_typecheck_builder(data_typechecker, variable_context, action_context).apply(regular_formulas::normalize_sorts(x, data_typechecker.typechecked_data_specification()));
     311             : }
     312             : 
     313             : inline
     314             : regular_formula typecheck_regular_formula(const regular_formula& x, const lps::specification& lpsspec)
     315             : {
     316             :   return typecheck_regular_formula(x, lpsspec.data(), lpsspec.global_variables(), lpsspec.action_labels());
     317             : }
     318             : 
     319             : } // namespace regular_formulas
     320             : 
     321             : namespace state_formulas
     322             : {
     323             : 
     324             : namespace detail
     325             : {
     326             : 
     327         169 : struct typecheck_builder: public state_formula_builder<typecheck_builder>
     328             : {
     329             :   typedef state_formula_builder<typecheck_builder> super;
     330             :   using super::apply;
     331             : 
     332             :   data::data_type_checker& m_data_type_checker;
     333             :   data::detail::variable_context m_variable_context;
     334             :   const process::detail::action_context& m_action_context;
     335             :   detail::state_variable_context m_state_variable_context;
     336             : 
     337         169 :   typecheck_builder(data::data_type_checker& data_typechecker,
     338             :                     const data::detail::variable_context& variable_context,
     339             :                     const process::detail::action_context& action_context,
     340             :                     const detail::state_variable_context& state_variable_context
     341             :                    )
     342         169 :     : m_data_type_checker(data_typechecker),
     343             :       m_variable_context(variable_context),
     344             :       m_action_context(action_context),
     345         169 :       m_state_variable_context(state_variable_context)
     346         169 :   {}
     347             : 
     348          24 :   state_formula apply(const data::data_expression& x)
     349             :   {
     350          24 :     return m_data_type_checker.typecheck_data_expression(x, data::sort_bool::bool_(), m_variable_context);
     351             :   }
     352             : 
     353          19 :   state_formula apply(const state_formulas::forall& x)
     354             :   {
     355             :     try
     356             :     {
     357          38 :       auto m_variable_context_copy = m_variable_context;
     358          19 :       m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
     359          38 :       state_formula body = (*this).apply(x.body());
     360          19 :       m_variable_context = m_variable_context_copy;
     361          38 :       return forall(x.variables(), body);
     362             :     }
     363           0 :     catch (mcrl2::runtime_error& e)
     364             :     {
     365           0 :       throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + state_formulas::pp(x));
     366             :     }
     367             :   }
     368             : 
     369           8 :   state_formula apply(const state_formulas::exists& x)
     370             :   {
     371             :     try
     372             :     {
     373          16 :       auto m_variable_context_copy = m_variable_context;
     374           8 :       m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
     375          16 :       state_formula body = (*this).apply(x.body());
     376           8 :       m_variable_context = m_variable_context_copy;
     377          16 :       return exists(x.variables(), body);
     378             :     }
     379           0 :     catch (mcrl2::runtime_error& e)
     380             :     {
     381           0 :       throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + state_formulas::pp(x));
     382             :     }
     383             :   }
     384             : 
     385          75 :   state_formula apply(const state_formulas::may& x)
     386             :   {
     387          75 :     return may(regular_formulas::detail::make_typecheck_builder(m_data_type_checker, m_variable_context, m_action_context).apply(x.formula()), (*this).apply(x.operand()));
     388             :   }
     389             : 
     390         132 :   state_formula apply(const state_formulas::must& x)
     391             :   {
     392         132 :     return must(regular_formulas::detail::make_typecheck_builder(m_data_type_checker, m_variable_context, m_action_context).apply(x.formula()), (*this).apply(x.operand()));
     393             :   }
     394             : 
     395           3 :   state_formula apply(const state_formulas::delay_timed& x)
     396             :   {
     397           6 :     data::data_expression new_time = m_data_type_checker.typecheck_data_expression(x.time_stamp(), data::sort_real::real_(), m_variable_context);
     398           6 :     return delay_timed(new_time);
     399             :   }
     400             : 
     401           1 :   state_formula apply(const state_formulas::yaled_timed& x)
     402             :   {
     403           2 :     data::data_expression new_time = m_data_type_checker.typecheck_data_expression(x.time_stamp(), data::sort_real::real_(), m_variable_context);
     404           2 :     return yaled_timed(new_time);
     405             :   }
     406             : 
     407         139 :   state_formula apply_untyped_parameter(const core::identifier_string& name, const data::data_expression_list& arguments)
     408             :   {
     409         277 :     data::sort_expression_list expected_sorts = m_state_variable_context.matching_state_variable_sorts(name, arguments);
     410         276 :     data::data_expression_list new_arguments;
     411         138 :     auto q1 = expected_sorts.begin();
     412         138 :     auto q2 = arguments.begin();
     413         154 :     for (; q1 != expected_sorts.end(); ++q1, ++q2)
     414             :     {
     415           8 :       new_arguments.push_front(m_data_type_checker.typecheck_data_expression(*q2, *q1, m_variable_context));
     416             :     }
     417         138 :     new_arguments = atermpp::reverse(new_arguments);
     418         276 :     return state_formulas::variable(name, new_arguments);
     419             :   }
     420             : 
     421           0 :   state_formula apply(const state_formulas::variable& x)
     422             :   {
     423           0 :     return apply_untyped_parameter(x.name(), x.arguments());
     424             :   }
     425             : 
     426         139 :   state_formula apply(const data::untyped_data_parameter& x)
     427             :   {
     428         139 :     return apply_untyped_parameter(x.name(), x.arguments());
     429             :   }
     430             : 
     431         163 :   data::variable_list assignment_variables(const data::assignment_list& x) const
     432             :   {
     433         326 :     std::vector<data::variable> result;
     434         178 :     for (const data::assignment& a: x)
     435             :     {
     436          15 :       result.push_back(a.lhs());
     437             :     }
     438         326 :     return data::variable_list(result.begin(), result.end());
     439             :   }
     440             : 
     441             :   template <typename MuNuFormula>
     442         163 :   state_formula apply_mu_nu(const MuNuFormula& x, bool is_mu)
     443             :   {
     444         326 :     data::assignment_list new_assignments = m_data_type_checker.typecheck_assignment_list(x.assignments(), m_variable_context);
     445             : 
     446             :     // add the assignment variables to the context
     447         326 :     auto m_variable_context_copy = m_variable_context;
     448         326 :     data::variable_list x_variables = assignment_variables(x.assignments());
     449         163 :     m_variable_context.add_context_variables(x_variables, m_data_type_checker);
     450             : 
     451             :     // add x to the state variable context
     452         326 :     auto m_state_variable_context_copy = m_state_variable_context;
     453         163 :     m_state_variable_context.add_state_variable(x.name(), x_variables, m_data_type_checker);
     454             : 
     455             :     // typecheck the operand
     456         324 :     state_formula new_operand = (*this).apply(x.operand());
     457             : 
     458             :     // restore the context
     459         161 :     m_variable_context = m_variable_context_copy;
     460         161 :     m_state_variable_context = m_state_variable_context_copy;
     461             : 
     462         161 :     if (is_mu)
     463             :     {
     464          96 :       return mu(x.name(), new_assignments, new_operand);
     465             :     }
     466             :     else
     467             :     {
     468          65 :       return nu(x.name(), new_assignments, new_operand);
     469             :     }
     470             :   }
     471             : 
     472          66 :   state_formula apply(const state_formulas::nu& x)
     473             :   {
     474          66 :     return apply_mu_nu(x, false);
     475             :   }
     476             : 
     477          97 :   state_formula apply(const state_formulas::mu& x)
     478             :   {
     479          97 :     return apply_mu_nu(x, true);
     480             :   }
     481             : };
     482             : 
     483             : inline
     484         169 : typecheck_builder make_typecheck_builder(
     485             :                     data::data_type_checker& data_typechecker,
     486             :                     const data::detail::variable_context& variable_context,
     487             :                     const process::detail::action_context& action_context,
     488             :                     const detail::state_variable_context& state_variable_context
     489             :                    )
     490             : {
     491         169 :   return typecheck_builder(data_typechecker, variable_context, action_context, state_variable_context);
     492             : }
     493             : 
     494             : } // namespace detail
     495             : 
     496         169 : class state_formula_type_checker
     497             : {
     498             :   protected:
     499             :     data::data_type_checker m_data_type_checker;
     500             :     data::detail::variable_context m_variable_context;
     501             :     process::detail::action_context m_action_context;
     502             :     detail::state_variable_context m_state_variable_context;
     503             : 
     504             :   public:
     505             :     /** \brief     Constructor for a state_formula type checker.
     506             :      *  \param[in] dataspec The data specification against which state formulas are checked.
     507             :      *  \param[in] action_labels The data labels that can occur in a state formula.
     508             :      *  \param[in] variables A container containing variables that can occur in state formulas.
     509             :      **/
     510             :     template <typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable> >
     511         169 :     state_formula_type_checker(const data::data_specification& dataspec,
     512             :                                const ActionLabelContainer& action_labels = ActionLabelContainer(),
     513             :                                const VariableContainer& variables = VariableContainer()
     514             :                               )
     515         169 :       : m_data_type_checker(dataspec)
     516             :     {
     517         169 :       m_variable_context.add_context_variables(variables, m_data_type_checker);
     518         169 :       m_action_context.add_context_action_labels(action_labels, m_data_type_checker);
     519         169 :     }
     520             : 
     521             :     //check correctness of the state formula as follows:
     522             :     //1) determine the types of actions according to the definitions
     523             :     //   in spec
     524             :     //2) determine the types of data expressions according to the
     525             :     //   definitions in spec
     526             :     //3) check for name conflicts of data variable declarations in
     527             :     //   forall, exists, mu and nu quantifiers
     528             :     //4) check for monotonicity of fixpoint variables
     529         169 :     state_formula typecheck_state_formula(const state_formula& x)
     530             :     {
     531         169 :       mCRL2log(log::verbose) << "type checking state formula..." << std::endl;
     532         170 :       return detail::make_typecheck_builder(m_data_type_checker, m_variable_context, m_action_context, m_state_variable_context).apply(state_formulas::normalize_sorts(x, m_data_type_checker.typechecked_data_specification()));
     533             :     }
     534             : };
     535             : 
     536             : /** \brief     Type check a state formula.
     537             :  *  Throws an exception if something went wrong.
     538             :  *  \param[in] x A state formula that has not been type checked.
     539             :  *  \param[in] dataspec The data specification against which the formulas is checked.
     540             :  *  \param[in] action_labels A declaration of action labels that can be used in the state formulas.
     541             :  *  \param[in] variables A container with global data variables.
     542             :  *  \post      formula is type checked.
     543             :  **/
     544             : template <typename VariableContainer, typename ActionLabelContainer>
     545         169 : state_formula typecheck_state_formula(const state_formula& x,
     546             :                                       const data::data_specification& dataspec = data::data_specification(),
     547             :                                       const ActionLabelContainer& action_labels = ActionLabelContainer(),
     548             :                                       const VariableContainer& variables = VariableContainer()
     549             :                                      )
     550             : {
     551             :   try
     552             :   {
     553         338 :     state_formula_type_checker type_checker(dataspec, action_labels, variables);
     554         337 :     return type_checker.typecheck_state_formula(x);
     555             :   }
     556           2 :   catch (mcrl2::runtime_error& e)
     557             :   {
     558           1 :     throw mcrl2::runtime_error(std::string(e.what()) + "\ncould not type check modal formula " + state_formulas::pp(x));
     559             :   }
     560             : }
     561             : 
     562             : /** \brief     Type check a state formula.
     563             :  *  Throws an exception if something went wrong.
     564             :  *  \param[in] x A state formula that has not been type checked.
     565             :  *  \param[in] lpsspec A linear process specifications containing data, action and global variable declarations
     566             :  *                     to be used when typechecking the formula.
     567             :  *  \post      formula is type checked.
     568             :  **/
     569             : inline
     570         168 : state_formula typecheck_state_formula(const state_formula& x,
     571             :                                       const lps::specification& lpsspec
     572             :                                      )
     573             : {
     574         168 :   return typecheck_state_formula(x, lpsspec.data(), lpsspec.action_labels(), lpsspec.global_variables());
     575             : }
     576             : 
     577             : /// \brief Typecheck the state formula specification formspec. It is assumed that the formula is self contained,
     578             : /// i.e. all actions and sorts must be declared.
     579             : inline
     580             : void typecheck_state_formula_specification(state_formula_specification& formspec)
     581             : {
     582             :   try
     583             :   {
     584             :     data::data_type_checker checker(formspec.data());
     585             :     data::data_specification dataspec = checker.typechecked_data_specification();
     586             :     state_formulas::normalize_sorts(formspec, dataspec);
     587             :     state_formula_type_checker type_checker(dataspec, formspec.action_labels(), std::vector<data::variable>());
     588             :     formspec.formula() = type_checker.typecheck_state_formula(formspec.formula());
     589             :     formspec.data() = checker.typechecked_data_specification();
     590             :   }
     591             :   catch (mcrl2::runtime_error& e)
     592             :   {
     593             :     throw mcrl2::runtime_error(std::string(e.what()) + "\ncould not type check modal formula specification " + state_formulas::pp(formspec));
     594             :   }
     595             : }
     596             : 
     597             : /// \brief Typecheck the state formula specification formspec. It is assumed that the formula is not self contained,
     598             : /// i.e. some of the actions and sorts may be declared in lpsspec.
     599             : inline
     600             : void typecheck_state_formula_specification(state_formula_specification& formspec, const lps::specification& lpsspec)
     601             : {
     602             :   try
     603             :   {
     604             :     data::data_type_checker checker(formspec.data());
     605             :     data::data_specification dataspec = checker.typechecked_data_specification();
     606             :     state_formulas::normalize_sorts(formspec, dataspec);
     607             :     state_formula_type_checker type_checker(dataspec, lpsspec.action_labels() + formspec.action_labels(), lpsspec.global_variables());
     608             :     formspec.formula() = type_checker.typecheck_state_formula(formspec.formula());
     609             :     formspec.data() = checker.typechecked_data_specification();
     610             :   }
     611             :   catch (mcrl2::runtime_error& e)
     612             :   {
     613             :     throw mcrl2::runtime_error(std::string(e.what()) + "\ncould not type check modal formula specification " + state_formulas::pp(formspec));
     614             :   }
     615             : }
     616             : 
     617             : } // namespace state_formulas
     618             : 
     619             : } // namespace mcrl2
     620             : 
     621             : #endif // MCRL2_MODAL_FORMULA_TYPECHECK_H

Generated by: LCOV version 1.13