LCOV - code coverage report
Current view: top level - modal_formula/include/mcrl2/modal_formula - has_name_clashes.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 80 80 100.0 %
Date: 2020-02-21 00:44:40 Functions: 24 24 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/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         292 : 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         150 :     void pop()
      37             :     {
      38         150 :       m_name_stack.pop_back();
      39         150 :     }
      40             : 
      41             :     /// \brief Pushes name on the stack.
      42         162 :     void push(const core::identifier_string& name)
      43             :     {
      44             :       using utilities::detail::contains;
      45         162 :       if (contains(m_name_stack, name))
      46             :       {
      47           6 :         throw mcrl2::runtime_error("nested propositional variable " + std::string(name) + " clashes");
      48             :       }
      49         156 :       m_name_stack.push_back(name);
      50         156 :     }
      51             : 
      52          91 :     void enter(const mu& x)
      53             :     {
      54          91 :       push(x.name());
      55          85 :     }
      56             : 
      57          79 :     void leave(const mu&)
      58             :     {
      59          79 :       pop();
      60          79 :     }
      61             : 
      62          71 :     void enter(const nu& x)
      63             :     {
      64          71 :       push(x.name());
      65          71 :     }
      66             : 
      67          71 :     void leave(const nu&)
      68             :     {
      69          71 :       pop();
      70          71 :     }
      71             : };
      72             : 
      73             : /// \brief Traverser that checks for name clashes in parameters of nested mu's/nu's and forall/exists.
      74         270 : 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          40 :     void enter(const mu& x)
     101             :     {
     102          46 :       for (const data::assignment& a: x.assignments())
     103             :       {
     104           7 :         insert(a.lhs().name(), x);
     105             :       }
     106          39 :     }
     107             : 
     108          39 :     void leave(const mu& x)
     109             :     {
     110          45 :       for (const data::assignment& a: x.assignments())
     111             :       {
     112           6 :         erase(a.lhs().name());
     113             :       }
     114          39 :     }
     115             : 
     116         134 :     void enter(const nu& x)
     117             :     {
     118         140 :       for (const data::assignment& a: x.assignments())
     119             :       {
     120           6 :         insert(a.lhs().name(), x);
     121             :       }
     122         134 :     }
     123             : 
     124         133 :     void leave(const nu& x)
     125             :     {
     126         138 :       for (const data::assignment& a: x.assignments())
     127             :       {
     128           5 :         erase(a.lhs().name());
     129             :       }
     130         133 :     }
     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         146 : void check_state_variable_name_clashes(const state_formula& x)
     170             : {
     171         292 :   detail::state_variable_name_clash_checker checker;
     172         146 :   checker.apply(x);
     173         140 : }
     174             : 
     175             : /// \brief Returns true if the formula contains name clashes
     176             : inline
     177         146 : bool has_state_variable_name_clashes(const state_formula& x)
     178             : {
     179             :   try
     180             :   {
     181         146 :     check_state_variable_name_clashes(x);
     182             :   }
     183          12 :   catch (const mcrl2::runtime_error&)
     184             :   {
     185           6 :     return true;
     186             :   }
     187         140 :   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         135 : void check_data_variable_name_clashes(const state_formula& x)
     193             : {
     194         270 :   detail::state_formula_data_variable_name_clash_checker checker;
     195         135 :   checker.apply(x);
     196         134 : }
     197             : 
     198             : /// \brief Returns true if the formula contains parameter name clashes
     199             : inline
     200         135 : bool has_data_variable_name_clashes(const state_formula& x)
     201             : {
     202             :   try
     203             :   {
     204         135 :     check_data_variable_name_clashes(x);
     205             :   }
     206           2 :   catch (const mcrl2::runtime_error&)
     207             :   {
     208           1 :     return true;
     209             :   }
     210         134 :   return false;
     211             : }
     212             : 
     213             : } // namespace mcrl2::state_formulas
     214             : 
     215             : #endif // MCRL2_MODAL_FORMULA_HAS_NAME_CLASHES_H

Generated by: LCOV version 1.13