LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/detail - is_well_typed.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 37 125 29.6 %
Date: 2024-03-08 02:52:28 Functions: 7 16 43.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/detail/is_well_typed.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_IS_WELL_TYPED_H
      13             : #define MCRL2_PBES_DETAIL_IS_WELL_TYPED_H
      14             : 
      15             : #include "mcrl2/data/detail/data_utility.h"
      16             : #include "mcrl2/pbes/traverser.h"
      17             : #include <boost/iterator/transform_iterator.hpp>
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace pbes_system {
      22             : 
      23             : namespace detail {
      24             : 
      25             : /// Visitor for collecting the quantifier variables that occur in a pbes expression.
      26             : struct find_quantifier_variables_traverser: public pbes_expression_traverser<find_quantifier_variables_traverser>
      27             : {
      28             :   typedef pbes_expression_traverser<find_quantifier_variables_traverser> super;
      29             :   using super::enter;
      30             :   using super::leave;
      31             :   using super::apply;
      32             : 
      33             :   std::set<data::variable> result;
      34             : 
      35         289 :   void enter(const forall& x)
      36             :   {
      37         289 :     auto const& v = x.variables();
      38         289 :     result.insert(v.begin(), v.end());
      39         289 :   }
      40             : 
      41         563 :   void enter(const exists& x)
      42             :   {
      43         563 :     auto const& v = x.variables();
      44         563 :     result.insert(v.begin(), v.end());
      45         563 :   }
      46             : };
      47             : 
      48             : inline
      49        1026 : std::set<data::variable> find_quantifier_variables(const pbes_expression& x)
      50             : {
      51        1026 :   find_quantifier_variables_traverser f;
      52        1026 :   f.apply(x);
      53        2052 :   return f.result;
      54        1026 : }
      55             : 
      56             : /// \brief Visitor for determining if within the scope of a quantifier there are quantifier
      57             : /// variables of free variables with the same name.
      58             : struct has_quantifier_name_clashes_traverser: public pbes_expression_traverser<has_quantifier_name_clashes_traverser>
      59             : {
      60             :   typedef pbes_expression_traverser<has_quantifier_name_clashes_traverser> super;
      61             :   using super::enter;
      62             :   using super::leave;
      63             :   using super::apply;
      64             : 
      65             :   std::vector<data::variable_list> quantifier_stack;
      66             :   bool result;
      67             :   data::variable name_clash; // if result is true, then this attribute contains the conflicting variable
      68             : 
      69           0 :   has_quantifier_name_clashes_traverser()
      70           0 :     : result(false)
      71           0 :   {}
      72             : 
      73             :   /// \brief Returns true if the quantifier_stack contains a data variable with the given name
      74             :   /// \param name A
      75             :   /// \return True if the quantifier_stack contains a data variable with the given name
      76           0 :   bool is_in_quantifier_stack(const core::identifier_string& name) const
      77             :   {
      78           0 :     for (const data::variable_list& vars: quantifier_stack)
      79             :     {
      80           0 :       if (std::find(boost::make_transform_iterator(vars.begin(), data::detail::variable_name()),
      81           0 :                     boost::make_transform_iterator(vars.end()  , data::detail::variable_name()),
      82             :                     name
      83           0 :                    ) != boost::make_transform_iterator(vars.end()  , data::detail::variable_name())
      84             :          )
      85             :       {
      86           0 :         return true;
      87             :       }
      88             :     }
      89           0 :     return false;
      90             :   }
      91             : 
      92             :   /// \brief Adds variables to the quantifier stack, and adds replacements for the name clashes to replacements.
      93             :   /// \param variables A sequence of data variables
      94             :   /// \return The number of replacements that were added.
      95           0 :   void push(const data::variable_list& variables)
      96             :   {
      97           0 :     if (result)
      98             :     {
      99           0 :       return;
     100             :     }
     101           0 :     for (const data::variable& v: variables)
     102             :     {
     103           0 :       if (is_in_quantifier_stack(v.name()))
     104             :       {
     105           0 :         result = true;
     106           0 :         name_clash = v;
     107           0 :         return;
     108             :       }
     109             :     }
     110           0 :     quantifier_stack.push_back(variables);
     111             :   }
     112             : 
     113             :   /// \brief Pops the quantifier stack
     114           0 :   void pop()
     115             :   {
     116           0 :     if (result)
     117             :     {
     118           0 :       return;
     119             :     }
     120           0 :     quantifier_stack.pop_back();
     121             :   }
     122             : 
     123           0 :   void enter(const forall& x)
     124             :   {
     125           0 :     push(x.variables());
     126           0 :   }
     127             : 
     128           0 :   void leave(const forall&)
     129             :   {
     130           0 :     pop();
     131           0 :   }
     132             : 
     133           0 :   void enter(const exists& x)
     134             :   {
     135           0 :     push(x.variables());
     136           0 :   }
     137             : 
     138           0 :   void leave(const exists&)
     139             :   {
     140           0 :     pop();
     141           0 :   }
     142             : };
     143             : 
     144             : inline
     145             : bool has_quantifier_name_clashes(const pbes_expression& x)
     146             : {
     147             :   has_quantifier_name_clashes_traverser f;
     148             :   f.apply(x);
     149             :   return f.result;
     150             : }
     151             : 
     152             : /// \brief Checks if the equation is well typed
     153             : /// \return True if
     154             : /// <ul>
     155             : /// <li>the binding variable parameters have unique names</li>
     156             : /// <li>the names of the quantifier variables in the equation are disjoint with the binding variable parameter names</li>
     157             : /// <li>within the scope of a quantifier variable in the formula, no other quantifier variables with the same name may occur</li>
     158             : /// </ul>
     159             : inline
     160           0 : bool is_well_typed(const pbes_equation& eqn)
     161             : {
     162             :   // check 1)
     163           0 :   if (data::detail::sequence_contains_duplicates(
     164           0 :         boost::make_transform_iterator(eqn.variable().parameters().begin(), data::detail::variable_name()),
     165           0 :         boost::make_transform_iterator(eqn.variable().parameters().end()  , data::detail::variable_name())
     166             :       )
     167             :      )
     168             :   {
     169           0 :     mCRL2log(log::error) << "pbes_equation::is_well_typed() failed: the names of the binding variable parameters are not unique" << std::endl;
     170           0 :     return false;
     171             :   }
     172             : 
     173             :   // check 2)
     174           0 :   std::set<data::variable> qvariables = detail::find_quantifier_variables(eqn.formula());
     175           0 :   if (data::detail::sequences_do_overlap(
     176           0 :         boost::make_transform_iterator(eqn.variable().parameters().begin(), data::detail::variable_name()),
     177           0 :         boost::make_transform_iterator(eqn.variable().parameters().end()  , data::detail::variable_name()),
     178             :         boost::make_transform_iterator(qvariables.begin()     , data::detail::variable_name()),
     179             :         boost::make_transform_iterator(qvariables.end()       , data::detail::variable_name())
     180             :       )
     181             :      )
     182             :   {
     183           0 :     mCRL2log(log::error) << "pbes_equation::is_well_typed() failed: the names of the quantifier variables and the names of the binding variable parameters are not disjoint in expression " << pbes_system::pp(eqn.formula()) << std::endl;
     184           0 :     return false;
     185             :   }
     186             : 
     187             :   // check 3)
     188           0 :   has_quantifier_name_clashes_traverser nvisitor;
     189           0 :   nvisitor.apply(eqn.formula());
     190           0 :   if (nvisitor.result)
     191             :   {
     192           0 :     mCRL2log(log::error) << "pbes_equation::is_well_typed() failed: the quantifier variable " << nvisitor.name_clash << " occurs within the scope of a quantifier variable with the same name." << std::endl;
     193           0 :     return false;
     194             :   }
     195             : 
     196           0 :   return true;
     197           0 : }
     198             : 
     199             : /// \brief Checks if the propositional variable instantiation v has a conflict with the
     200             : /// sequence of propositional variable declarations [first, last).
     201             : /// \param first Start of a sequence of propositional variable declarations
     202             : /// \param last End of a sequence of propositional variable declarations
     203             : /// \return True if a conflict has been detected
     204             : /// \param v A propositional variable instantiation
     205             : template <typename Iter>
     206        2565 : bool has_conflicting_type(Iter first, Iter last, const propositional_variable_instantiation& v, const data::data_specification& data_spec)
     207             : {
     208       39298 :   for (Iter i = first; i != last; ++i)
     209             :   {
     210       36733 :     if (i->name() == v.name() && !data::detail::equal_sorts(i->parameters(), v.parameters(), data_spec))
     211             :     {
     212           0 :       return true;
     213             :     }
     214             :   }
     215        2565 :   return false;
     216             : }
     217             : 
     218             : inline
     219        1026 : bool is_well_typed_equation(const pbes_equation& eqn,
     220             :                             const std::set<data::sort_expression>& declared_sorts,
     221             :                             const std::set<data::variable>& declared_global_variables,
     222             :                             const data::data_specification& data_spec
     223             :                            )
     224             : {
     225             :   // check 2)
     226        1026 :   const data::variable_list& variables = eqn.variable().parameters();
     227        1026 :   if (!data::detail::check_sorts(
     228        1026 :         boost::make_transform_iterator(variables.begin(), data::detail::sort_of_variable()),
     229        2052 :         boost::make_transform_iterator(variables.end()  , data::detail::sort_of_variable()),
     230             :         declared_sorts
     231             :       )
     232             :      )
     233             :   {
     234           0 :     mCRL2log(log::error) << "pbes::is_well_typed() failed: some of the sorts of the binding variable "
     235           0 :               << eqn.variable()
     236           0 :               << " are not declared in the data specification "
     237           0 :               << data_spec
     238           0 :               << std::endl;
     239           0 :     return false;
     240             :   }
     241             : 
     242             :   // check 3)
     243        1026 :   std::set<data::variable> quantifier_variables = detail::find_quantifier_variables(eqn.formula());
     244        1026 :   if (!data::detail::check_sorts(
     245             :         boost::make_transform_iterator(quantifier_variables.begin(), data::detail::sort_of_variable()),
     246             :         boost::make_transform_iterator(quantifier_variables.end()  , data::detail::sort_of_variable()),
     247             :         declared_sorts
     248             :       )
     249             :      )
     250             :   {
     251           0 :     mCRL2log(log::error) << "pbes::is_well_typed() failed: some of the sorts of the quantifier variables "
     252           0 :               << data::pp(quantifier_variables)
     253           0 :               << " are not declared in the data specification "
     254           0 :               << data_spec
     255           0 :               << std::endl;
     256           0 :     return false;
     257             :   }
     258             : 
     259             :   // check 7)
     260        1026 :   if (!utilities::detail::set_intersection(declared_global_variables, quantifier_variables).empty())
     261             :   {
     262           0 :     mCRL2log(log::error) << "pbes::is_well_typed() failed: the declared free variables and the quantifier variables have collisions" << std::endl;
     263           0 :     return false;
     264             :   }
     265        1026 :   return true;
     266        1026 : }
     267             : 
     268             : inline
     269         280 : bool is_well_typed_pbes(const std::set<data::sort_expression>& declared_sorts,
     270             :                         const std::set<data::variable>& declared_global_variables,
     271             :                         const std::set<data::variable>& occurring_global_variables,
     272             :                         const std::set<propositional_variable>& declared_variables,
     273             :                         const std::set<propositional_variable_instantiation>& occ,
     274             :                         const propositional_variable_instantiation& init,
     275             :                         const data::data_specification& data_spec
     276             :                        )
     277             : {
     278             :   // check 1)
     279         280 :   if (!data::detail::check_sorts(
     280             :         boost::make_transform_iterator(declared_global_variables.begin(), data::detail::sort_of_variable()),
     281             :         boost::make_transform_iterator(declared_global_variables.end()  , data::detail::sort_of_variable()),
     282             :         declared_sorts
     283             :       )
     284             :      )
     285             :   {
     286           0 :     mCRL2log(log::error) << "pbes::is_well_typed() failed: some of the sorts of the free variables "
     287           0 :               << data::pp(declared_global_variables)
     288           0 :               << " are not declared in the data specification "
     289           0 :               << data_spec
     290           0 :               << std::endl;
     291           0 :     return false;
     292             :   }
     293             : 
     294             :   // check 4)
     295        1026 :   auto propvar_name = [](const propositional_variable& x) { return x.name(); };
     296         280 :   if (data::detail::sequence_contains_duplicates(
     297             :         boost::make_transform_iterator(declared_variables.begin(), propvar_name),
     298             :         boost::make_transform_iterator(declared_variables.end()  , propvar_name)
     299             :       )
     300             :      )
     301             :   {
     302           0 :     mCRL2log(log::error) << "pbes::is_well_typed() failed: the names of the binding variables are not unique" << std::endl;
     303           0 :     return false;
     304             :   }
     305             : 
     306             :   // check 5)
     307         280 :   if (!std::includes(declared_global_variables.begin(),
     308             :                      declared_global_variables.end(),
     309             :                      occurring_global_variables.begin(),
     310             :                      occurring_global_variables.end()
     311             :                     )
     312             :      )
     313             :   {
     314           0 :     mCRL2log(log::error) << "pbes::is_well_typed() failed: not all of the free variables are declared\n"
     315           0 :               << "free variables: " << data::pp(occurring_global_variables) << "\n"
     316           0 :               << "declared free variables: " << data::pp(declared_global_variables)
     317           0 :               << std::endl;
     318           0 :     return false;
     319             :   }
     320             : 
     321             :   // check 6)
     322         280 :   if (data::detail::sequence_contains_duplicates(
     323             :         boost::make_transform_iterator(occurring_global_variables.begin(), data::detail::variable_name()),
     324             :         boost::make_transform_iterator(occurring_global_variables.end()  , data::detail::variable_name())
     325             :       )
     326             :      )
     327             :   {
     328           0 :     mCRL2log(log::error) << "pbes::is_well_typed() failed: the free variables have no unique names" << std::endl;
     329           0 :     return false;
     330             :   }
     331             : 
     332             :   // check 8)
     333        2565 :   for (const propositional_variable_instantiation& v: occ)
     334             :   {
     335        2285 :     if (has_conflicting_type(declared_variables.begin(), declared_variables.end(), v, data_spec))
     336             :     {
     337           0 :       mCRL2log(log::error) << "pbes::is_well_typed() failed: the occurring variable " << pbes_system::pp(v) << " conflicts with its declaration!" << std::endl;
     338           0 :       return false;
     339             :     }
     340             :   }
     341             : 
     342             :   // check 9)
     343         280 :   if (has_conflicting_type(declared_variables.begin(), declared_variables.end(), init, data_spec))
     344             :   {
     345           0 :     mCRL2log(log::error) << "pbes::is_well_typed() failed: the initial state " << pbes_system::pp(init) << " conflicts with its declaration!" << std::endl;
     346           0 :     return false;
     347             :   }
     348         280 :   return true;
     349             : }
     350             : 
     351             : } // namespace detail
     352             : 
     353             : } // namespace pbes_system
     354             : 
     355             : } // namespace mcrl2
     356             : 
     357             : #endif // MCRL2_PBES_DETAIL_IS_WELL_TYPED_H

Generated by: LCOV version 1.14