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/has_name_clashes.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_HAS_NAME_CLASHES_H
      13             : #define MCRL2_MODAL_FORMULA_HAS_NAME_CLASHES_H
      14             : 
      15             : #include "mcrl2/modal_formula/traverser.h"
      16             : 
      17             : namespace mcrl2::state_formulas {
      18             : 
      19             : namespace detail
      20             : {
      21             : 
      22             : /// \brief Traverser that checks for name clashes in nested mu's/nu's.
      23             : class state_variable_name_clash_checker: public state_formulas::state_formula_traverser<state_variable_name_clash_checker>
      24             : {
      25             :   public:
      26             :     typedef state_formulas::state_formula_traverser<state_variable_name_clash_checker> super;
      27             : 
      28             :     using super::apply;
      29             :     using super::enter;
      30             :     using super::leave;
      31             : 
      32             :     /// \brief The stack of names.
      33             :     std::vector<core::identifier_string> m_name_stack;
      34             : 
      35             :     /// \brief Pops the stack
      36         162 :     void pop()
      37             :     {
      38         162 :       m_name_stack.pop_back();
      39         162 :     }
      40             : 
      41             :     /// \brief Pushes name on the stack.
      42         178 :     void push(const core::identifier_string& name)
      43             :     {
      44             :       using utilities::detail::contains;
      45         178 :       if (contains(m_name_stack, name))
      46             :       {
      47           8 :         throw mcrl2::runtime_error("nested propositional variable " + std::string(name) + " clashes");
      48             :       }
      49         170 :       m_name_stack.push_back(name);
      50         170 :     }
      51             : 
      52         104 :     void enter(const mu& x)
      53             :     {
      54         104 :       push(x.name());
      55          97 :     }
      56             : 
      57          90 :     void leave(const mu&)
      58             :     {
      59          90 :       pop();
      60          90 :     }
      61             : 
      62          74 :     void enter(const nu& x)
      63             :     {
      64          74 :       push(x.name());
      65          73 :     }
      66             : 
      67          72 :     void leave(const nu&)
      68             :     {
      69          72 :       pop();
      70          72 :     }
      71             : };
      72             : 
      73             : /// \brief Traverser that checks for name clashes in parameters of nested mu's/nu's and forall/exists.
      74             : class state_formula_data_variable_name_clash_checker: public state_formulas::state_formula_traverser<state_formula_data_variable_name_clash_checker>
      75             : {
      76             :   public:
      77             :     typedef state_formulas::state_formula_traverser<state_formula_data_variable_name_clash_checker> super;
      78             : 
      79             :     using super::apply;
      80             :     using super::enter;
      81             :     using super::leave;
      82             : 
      83             :     std::set<core::identifier_string> m_names;
      84             : 
      85             :     // throws an exception if name was already present in m_names
      86          28 :     void insert(const core::identifier_string& name, const state_formula& x)
      87             :     {
      88          28 :       auto p = m_names.insert(name);
      89          28 :       if (!p.second)
      90             :       {
      91           1 :         throw mcrl2::runtime_error("Data parameter " + data::pp(name) + " in subformula " + state_formulas::pp(x) + " clashes with a data parameter in an enclosing formula.");
      92             :       }
      93          27 :     }
      94             : 
      95          26 :     void erase(const core::identifier_string& name)
      96             :     {
      97          26 :       m_names.erase(name);
      98          26 :     }
      99             : 
     100          54 :     void enter(const mu& x)
     101             :     {
     102          60 :       for (const data::assignment& a: x.assignments())
     103             :       {
     104           7 :         insert(a.lhs().name(), x);
     105             :       }
     106          53 :     }
     107             : 
     108          53 :     void leave(const mu& x)
     109             :     {
     110          59 :       for (const data::assignment& a: x.assignments())
     111             :       {
     112           6 :         erase(a.lhs().name());
     113             :       }
     114          53 :     }
     115             : 
     116         151 :     void enter(const nu& x)
     117             :     {
     118         157 :       for (const data::assignment& a: x.assignments())
     119             :       {
     120           6 :         insert(a.lhs().name(), x);
     121             :       }
     122         151 :     }
     123             : 
     124         150 :     void leave(const nu& x)
     125             :     {
     126         155 :       for (const data::assignment& a: x.assignments())
     127             :       {
     128           5 :         erase(a.lhs().name());
     129             :       }
     130         150 :     }
     131             : 
     132          11 :     void enter(const forall& x)
     133             :     {
     134          22 :       for (const data::variable& v: x.variables())
     135             :       {
     136          11 :         insert(v.name(), x);
     137             :       }
     138          11 :     }
     139             : 
     140          11 :     void leave(const forall& x)
     141             :     {
     142          22 :       for (const data::variable& v: x.variables())
     143             :       {
     144          11 :         erase(v.name());
     145             :       }
     146          11 :     }
     147             : 
     148           4 :     void enter(const exists& x)
     149             :     {
     150           8 :       for (const data::variable& v: x.variables())
     151             :       {
     152           4 :         insert(v.name(), x);
     153             :       }
     154           4 :     }
     155             : 
     156           4 :     void leave(const exists& x)
     157             :     {
     158           8 :       for (const data::variable& v: x.variables())
     159             :       {
     160           4 :         erase(v.name());
     161             :       }
     162           4 :     }
     163             : };
     164             : 
     165             : } // namespace detail
     166             : 
     167             : /// \brief Throws an exception if the formula contains name clashes
     168             : inline
     169         155 : void check_state_variable_name_clashes(const state_formula& x)
     170             : {
     171         155 :   detail::state_variable_name_clash_checker checker;
     172         155 :   checker.apply(x);
     173         155 : }
     174             : 
     175             : /// \brief Returns true if the formula contains name clashes
     176             : inline
     177         155 : bool has_state_variable_name_clashes(const state_formula& x)
     178             : {
     179             :   try
     180             :   {
     181         155 :     check_state_variable_name_clashes(x);
     182             :   }
     183           8 :   catch (const mcrl2::runtime_error&)
     184             :   {
     185           8 :     return true;
     186           8 :   }
     187         147 :   return false;
     188             : }
     189             : 
     190             : /// \brief Throws an exception if the formula contains name clashes in the parameters of mu/nu/exists/forall
     191             : inline
     192         144 : void check_data_variable_name_clashes(const state_formula& x)
     193             : {
     194         144 :   detail::state_formula_data_variable_name_clash_checker checker;
     195         144 :   checker.apply(x);
     196         144 : }
     197             : 
     198             : /// \brief Returns true if the formula contains parameter name clashes
     199             : inline
     200         144 : bool has_data_variable_name_clashes(const state_formula& x)
     201             : {
     202             :   try
     203             :   {
     204         144 :     check_data_variable_name_clashes(x);
     205             :   }
     206           1 :   catch (const mcrl2::runtime_error&)
     207             :   {
     208           1 :     return true;
     209           1 :   }
     210         143 :   return false;
     211             : }
     212             : 
     213             : } // namespace mcrl2::state_formulas
     214             : 
     215             : #endif // MCRL2_MODAL_FORMULA_HAS_NAME_CLASHES_H