LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes - typecheck.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 110 135 81.5 %
Date: 2024-03-08 02:52:28 Functions: 15 16 93.8 %
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/pbes/typecheck.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_TYPECHECK_H
      13             : #define MCRL2_PBES_TYPECHECK_H
      14             : 
      15             : #include "mcrl2/data/consistency.h"
      16             : #include "mcrl2/pbes/detail/pbes_context.h"
      17             : #include "mcrl2/pbes/normalize_sorts.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace pbes_system
      23             : {
      24             : 
      25             : namespace detail
      26             : {
      27             : 
      28             : struct typecheck_builder: public pbes_expression_builder<typecheck_builder>
      29             : {
      30             :   typedef pbes_expression_builder<typecheck_builder> super;
      31             :   using super::apply;
      32             : 
      33             :   data::data_type_checker& m_data_type_checker;
      34             :   data::detail::variable_context m_variable_context;
      35             :   const detail::pbes_context& m_pbes_context;
      36             : 
      37        3331 :   typecheck_builder(data::data_type_checker& data_typechecker,
      38             :                     const data::detail::variable_context& variables,
      39             :                     const detail::pbes_context& pbes_context
      40             :                    )
      41        3331 :     : m_data_type_checker(data_typechecker),
      42        3331 :       m_variable_context(variables),
      43        3331 :     m_pbes_context(pbes_context)
      44        3331 :   { }
      45             : 
      46             :   template <class T>
      47        3054 :   void apply(T& result, const data::data_expression& x)
      48             :   {
      49        3054 :     result = m_data_type_checker.typecheck_data_expression(x, data::bool_(), m_variable_context);
      50        3054 :   }
      51             : 
      52             :   template <class T>
      53         219 :   void apply(T& result, const forall& x)
      54             :   {
      55             :     try
      56             :     {
      57         219 :       data::detail::check_duplicate_variable_names(x.variables(), "quantifier variable");
      58         219 :       auto m_variable_context_copy = m_variable_context;
      59         219 :       m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
      60         219 :       pbes_expression body;
      61         219 :       (*this).apply(body, x.body());
      62         219 :       m_variable_context = m_variable_context_copy;
      63         219 :       result = forall(x.variables(), body);
      64         219 :     }
      65           0 :     catch (mcrl2::runtime_error& e)
      66             :     {
      67           0 :       throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + pbes_system::pp(x));
      68             :     }
      69         219 :   }
      70             : 
      71             :   template <class T>
      72         119 :   void apply(T& result, const exists& x)
      73             :   {
      74             :     try
      75             :     {
      76         119 :       data::detail::check_duplicate_variable_names(x.variables(), "quantifier variable");
      77         119 :       auto m_variable_context_copy = m_variable_context;
      78         119 :       m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
      79         119 :       pbes_expression body;
      80         119 :       (*this).apply(body, x.body());
      81         119 :       m_variable_context = m_variable_context_copy;
      82         119 :       result = exists(x.variables(), body);
      83         119 :     }
      84           0 :     catch (mcrl2::runtime_error& e)
      85             :     {
      86           0 :       throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + pbes_system::pp(x));
      87             :     }
      88         119 :   }
      89             : 
      90             :   template <class T>
      91         467 :   void apply(T& result, const propositional_variable_instantiation& x)
      92             :   {
      93         467 :     const core::identifier_string& name = x.name();
      94         467 :     if (!m_pbes_context.is_declared(name))
      95             :     {
      96           0 :       throw mcrl2::runtime_error("propositional variable " + core::pp(name) + " not declared");
      97             :     }
      98             : 
      99         467 :     data::sort_expression_list equation_sorts = m_pbes_context.propositional_variable_sorts(name);
     100         467 :     std::vector<data::data_expression> x_parameters(x.parameters().begin(), x.parameters().end());
     101             : 
     102         467 :     if (x_parameters.size() != equation_sorts.size())
     103             :     {
     104           0 :       throw mcrl2::runtime_error("propositional variable " + pbes_system::pp(x) + " has the wrong number of parameters");
     105             :     }
     106             : 
     107         467 :     auto ei = equation_sorts.begin();
     108         467 :     auto xi = x_parameters.begin();
     109         714 :     for (; ei != equation_sorts.end(); ++ei, ++xi)
     110             :     {
     111             :       try
     112             :       {
     113         247 :         *xi = m_data_type_checker.typecheck_data_expression(*xi, *ei, m_variable_context);
     114             :       }
     115           0 :       catch (mcrl2::runtime_error& e)
     116             :       {
     117           0 :         throw mcrl2::runtime_error(std::string(e.what()) + "\ncannot typecheck " + data::pp(*xi) + " as type " + data::pp(*ei) + " (while typechecking " + pbes_system::pp(x) + ")");
     118             :       }
     119             :     }
     120         467 :     make_propositional_variable_instantiation(result, name, data::data_expression_list(x_parameters.begin(), x_parameters.end()));
     121         467 :   }
     122             : 
     123             :   template <class T>
     124         787 :   void apply(T& result, const data::untyped_data_parameter& x)
     125             :   {
     126         787 :     const core::identifier_string& name = x.name();
     127         787 :     if (!m_pbes_context.is_declared(name))
     128             :     {
     129           0 :       result = data::typecheck_untyped_data_parameter(m_data_type_checker, x.name(), x.arguments(), data::bool_(), m_variable_context);
     130           0 :       return;
     131             :     }
     132             : 
     133         787 :     data::sort_expression_list equation_sorts = m_pbes_context.propositional_variable_sorts(name);
     134         787 :     std::vector<data::data_expression> x_parameters(x.arguments().begin(), x.arguments().end());
     135             : 
     136         787 :     if (x_parameters.size() != equation_sorts.size())
     137             :     {
     138           0 :       throw mcrl2::runtime_error("propositional variable " + data::pp(x) + " has the wrong number of parameters");
     139             :     }
     140             : 
     141         787 :     auto ei = equation_sorts.begin();
     142         787 :     auto xi = x_parameters.begin();
     143        1899 :     for (; ei != equation_sorts.end(); ++ei, ++xi)
     144             :     {
     145             :       try
     146             :       {
     147        1112 :         *xi = m_data_type_checker.typecheck_data_expression(*xi, *ei, m_variable_context);
     148             :       }
     149           0 :       catch (mcrl2::runtime_error& e)
     150             :       {
     151           0 :         throw mcrl2::runtime_error(std::string(e.what()) + "\ncannot typecheck " + data::pp(*xi) + " as type " + data::pp(*ei) + " (while typechecking " + data::pp(x) + ")");
     152             :       }
     153             :     }
     154         787 :     make_propositional_variable_instantiation(result, name, data::data_expression_list(x_parameters.begin(), x_parameters.end()));
     155         787 :   }
     156             : };
     157             : 
     158             : inline
     159        3331 : typecheck_builder make_typecheck_builder(
     160             :                     data::data_type_checker& data_typechecker,
     161             :                     const data::detail::variable_context& variables,
     162             :                     const detail::pbes_context& propositional_variables
     163             :                    )
     164             : {
     165        3331 :   return typecheck_builder(data_typechecker, variables, propositional_variables);
     166             : }
     167             : 
     168             : } // namespace detail
     169             : 
     170             : class pbes_type_checker
     171             : {
     172             :   protected:
     173             :     data::data_type_checker m_data_type_checker;
     174             :     data::detail::variable_context m_variable_context;
     175             :     detail::pbes_context m_pbes_context;
     176             : 
     177         467 :     std::vector<propositional_variable> equation_variables(const std::vector<pbes_equation>& equations)
     178             :     {
     179         467 :       std::vector<propositional_variable> result;
     180        3330 :       for (const pbes_equation& eqn: equations)
     181             :       {
     182        2863 :         result.push_back(eqn.variable());
     183             :       }
     184         467 :       return result;
     185           0 :     }
     186             : 
     187             :   public:
     188             :     /// \brief Default constructor
     189         467 :     pbes_type_checker(const data::data_specification& dataspec = data::data_specification())
     190         467 :       : m_data_type_checker(dataspec)
     191         467 :     {}
     192             : 
     193             :     /// \brief Constructor
     194             :     template <typename VariableContainer, typename PropositionalVariableContainer>
     195           1 :     pbes_type_checker(const data::data_specification& dataspec, const VariableContainer& global_variables, const PropositionalVariableContainer& propositional_variables)
     196           1 :       : m_data_type_checker(dataspec)
     197             :     {
     198           1 :       m_variable_context.add_context_variables(global_variables, m_data_type_checker);
     199           1 :       m_pbes_context.add_propositional_variables(propositional_variables, m_data_type_checker);
     200           1 :     }
     201             : 
     202             :     /// \brief Typecheck the pbes pbesspec
     203         467 :     void operator()(pbes& pbesspec)
     204             :     {
     205         467 :       mCRL2log(log::verbose) << "type checking PBES specification..." << std::endl;
     206             : 
     207         467 :       pbes_system::normalize_sorts(pbesspec, m_data_type_checker.typechecked_data_specification());
     208             : 
     209             :       // reset the context
     210         467 :       m_data_type_checker = data::data_type_checker(pbesspec.data());
     211         467 :       m_variable_context.clear();
     212         467 :       m_pbes_context.clear();
     213         467 :       m_variable_context.add_context_variables(pbesspec.global_variables(), m_data_type_checker);
     214         467 :       m_pbes_context.add_propositional_variables(equation_variables(pbesspec.equations()), m_data_type_checker);
     215             : 
     216             :       // typecheck the equations
     217        3330 :       for (pbes_equation& eqn: pbesspec.equations())
     218             :       {
     219        2863 :         data::detail::variable_context variable_context = m_variable_context;
     220             :         try
     221             :         {
     222        2863 :           data::detail::check_duplicate_variable_names(eqn.variable().parameters(), "propositional variable parameter");
     223             :         }
     224           0 :         catch (mcrl2::runtime_error& e)
     225             :         {
     226           0 :           throw mcrl2::runtime_error(std::string(e.what()) + " while typechecking " + pbes_system::pp(eqn.variable()));
     227           0 :         }
     228        2863 :         variable_context.add_context_variables(eqn.variable().parameters(), m_data_type_checker);
     229        2863 :         pbes_expression formula;
     230        2863 :         detail::make_typecheck_builder(m_data_type_checker, variable_context, m_pbes_context).apply(formula, eqn.formula());
     231        2863 :         eqn.formula() = formula;
     232        2863 :       }
     233             : 
     234             :       // typecheck the initial state
     235         467 :       propositional_variable_instantiation initial_state;
     236         467 :       detail::make_typecheck_builder(m_data_type_checker, m_variable_context, m_pbes_context).apply(initial_state, pbesspec.initial_state());
     237         467 :       pbesspec.initial_state() = initial_state;
     238             : 
     239             :       // typecheck the data specification
     240         467 :       pbesspec.data() = m_data_type_checker.typechecked_data_specification();
     241         467 :       pbesspec.data().translate_user_notation();
     242         467 :     }
     243             : 
     244             :      /** \brief     Type check a process expression.
     245             :       * Throws a mcrl2::runtime_error exception if the expression is not well typed.
     246             :       *  \param[in] x A process expression that has not been type checked.
     247             :       *  \return    a process expression where all untyped identifiers have been replace by typed ones.
     248             :       **/
     249           1 :     pbes_expression operator()(const pbes_expression& x)
     250             :     {
     251           1 :       pbes_expression result;
     252           1 :       detail::make_typecheck_builder(m_data_type_checker, m_variable_context, m_pbes_context).
     253           1 :              apply(result,pbes_system::normalize_sorts(x, m_data_type_checker.typechecked_data_specification()));
     254           1 :       return result;
     255           0 :     }
     256             : 
     257             :     protected:
     258             :       pbes_expression typecheck(const pbes_expression& x, const data::variable_list& parameters)
     259             :       {
     260             :         data::detail::variable_context variable_context = m_variable_context;
     261             :         variable_context.add_context_variables(parameters, m_data_type_checker);
     262             :         pbes_expression result;
     263             :         detail::make_typecheck_builder(m_data_type_checker, variable_context, m_pbes_context).apply(result, x);
     264             :         return result;
     265             :       }
     266             : };
     267             : 
     268             : /** \brief     Type check a parsed mCRL2 pbes specification.
     269             :  *  Throws an exception if something went wrong.
     270             :  *  \param[in] pbesspec A process specification  that has not been type checked.
     271             :  *  \post      pbesspec is type checked.
     272             :  **/
     273             : 
     274             : inline
     275         467 : void typecheck_pbes(pbes& pbesspec)
     276             : {
     277         467 :   pbes_type_checker type_checker;
     278             :   try
     279             :   {
     280         467 :     type_checker(pbesspec);
     281             :   }
     282           0 :   catch (mcrl2::runtime_error &e)
     283             :   {
     284           0 :     throw mcrl2::runtime_error(std::string(e.what()) + "\nCould not type check " + pbes_system::pp(pbesspec));
     285           0 :   }
     286         467 : }
     287             : 
     288             : /** \brief     Type check a parsed mCRL2 propositional variable.
     289             :  *  Throws an exception if something went wrong.
     290             :  *  \param[in] x A propositional variable.
     291             :  *  \param[in] variables A sequence of data variables that may appear in x.
     292             :  *  \param[in] dataspec A data specification.
     293             :  *  \return    the type checked expression
     294             :  **/
     295             : template <typename VariableContainer>
     296           2 : propositional_variable typecheck_propositional_variable(const propositional_variable& x,
     297             :                                                         const VariableContainer& variables,
     298             :                                                         const data::data_specification& dataspec = data::data_specification()
     299             :                                                        )
     300             : {
     301             :   // This function should be implemented using the PBES type checker, but it is not immediately clear how to do that.
     302             :   try
     303             :   {
     304           2 :     const data::variable_list& parameters = x.parameters();
     305           2 :     std::vector<data::variable> typed_parameters;
     306           7 :     for (const data::variable& parameter: parameters)
     307             :     {
     308           3 :       data::variable d = atermpp::down_cast<data::variable>(data::typecheck_data_expression(parameter, variables, dataspec));
     309           3 :       typed_parameters.push_back(d);
     310             :     }
     311           6 :     return propositional_variable(x.name(), data::variable_list(typed_parameters.begin(), typed_parameters.end()));
     312           2 :   }
     313           0 :   catch (mcrl2::runtime_error &e)
     314             :   {
     315           0 :     throw mcrl2::runtime_error(std::string(e.what()) + "\ncould not type check " + pbes_system::pp(x));
     316             :   }
     317             : }
     318             : 
     319             : /** \brief     Type check a parsed mCRL2 pbes expression.
     320             :  *  Throws an exception if something went wrong.
     321             :  *  \param[in] x A pbes expression.
     322             :  *  \param[in] variables A sequence of data variables that may appear in x.
     323             :  *  \param[in] propositional_variables A sequence of propositional variables that may appear in x.
     324             :  *  \param[in] dataspec A data specification.
     325             :  *  \return    the type checked expression
     326             :  **/
     327             : template <typename VariableContainer, typename PropositionalVariableContainer>
     328           1 : pbes_expression typecheck_pbes_expression(pbes_expression& x,
     329             :                                           const VariableContainer& variables,
     330             :                                           const PropositionalVariableContainer& propositional_variables,
     331             :                                           const data::data_specification& dataspec = data::data_specification()
     332             :                                          )
     333             : {
     334             :   try
     335             :   {
     336           1 :     pbes_type_checker type_checker(dataspec, variables, propositional_variables);
     337           2 :     return type_checker(x);
     338           1 :   }
     339           0 :   catch (mcrl2::runtime_error &e)
     340             :   {
     341           0 :     throw mcrl2::runtime_error(std::string(e.what()) + "\ncould not type check " + pbes_system::pp(x));
     342             :   }
     343             : }
     344             : 
     345             : } // namespace pbes_system
     346             : 
     347             : } // namespace mcrl2
     348             : 
     349             : #endif // MCRL2_PBES_TYPECHECK_H

Generated by: LCOV version 1.14