LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes - substitutions.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 27 27 100.0 %
Date: 2024-03-08 02:52:28 Functions: 5 5 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/pbes/substitutions.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_SUBSTITUTIONS_H
      13             : #define MCRL2_PBES_SUBSTITUTIONS_H
      14             : 
      15             : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
      16             : #include "mcrl2/pbes/replace.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22             : /** \brief Substitution function for propositional variables
      23             :  *
      24             :  * Model of Substitution.
      25             :  *
      26             :  **/
      27             : class propositional_variable_substitution
      28             : {
      29             :   public:
      30             :     // maps X to (phi, d), where X(d) is the propositional variable corresponding to X
      31             :     typedef std::map<core::identifier_string, std::pair<pbes_expression, data::variable_list> > map_type;
      32             : 
      33             :     typedef map_type::iterator iterator;
      34             :     typedef map_type::const_iterator const_iterator;
      35             : 
      36             :   protected:
      37             :     map_type m_map;
      38             : 
      39             :   public:
      40             :     /// \brief type used to represent variables
      41             :     typedef propositional_variable_instantiation variable_type;
      42             : 
      43             :     /// \brief type used to represent expressions
      44             :     typedef pbes_expression expression_type;
      45             : 
      46             :     /// \brief Apply this substitution to a single variable expression.
      47             :     /// \param[in] v The variable for which to give the associated expression.
      48             :     /// \return expression equivalent to s(e), or a reference to such an expression.
      49         121 :     pbes_expression operator()(const variable_type& v) const
      50             :     {
      51         121 :       auto i = m_map.find(v.name());
      52         121 :       if (i == m_map.end())
      53             :       {
      54          65 :         return v;
      55             :       }
      56          56 :       pbes_expression phi = i->second.first;
      57          56 :       const data::variable_list& d = i->second.second;
      58          56 :       const data::data_expression_list& e = v.parameters();
      59          56 :       data::mutable_map_substitution<> sigma;
      60          56 :       auto j = d.begin();
      61          56 :       auto k = e.begin();
      62         178 :       for (; j != d.end(); ++j, ++k)
      63             :       {
      64         122 :         sigma[*j] = *k;
      65             :       }
      66             : 
      67             :       // return phi[d := e]
      68          56 :       phi = pbes_system::replace_variables_capture_avoiding(phi, sigma);
      69          56 :       return phi;
      70          56 :     }
      71             : 
      72             :     /// \brief Wrapper class for internal storage and substitution updates using operator()
      73             :     class assignment
      74             :     {
      75             :       private:
      76             :         const propositional_variable& m_variable;
      77             :         map_type&                     m_map;
      78             : 
      79             :       public:
      80             : 
      81             :         /// \brief Constructor.
      82             :         ///
      83             :         /// \param[in] v a variable.
      84             :         /// \param[in] m a mapping of variables to expressions.
      85          87 :         assignment(const propositional_variable& v, map_type& m) :
      86          87 :           m_variable(v), m_map(m)
      87          87 :         { }
      88             : 
      89             :         /** \brief Assigns expression on the right-hand side
      90             :          * \param[in] e the expression to associate to the variable for the owning substitution object
      91             :          * \code
      92             :          *  template< typename E, typename V >
      93             :          *  void example(V const& v, E const& e) {
      94             :          *    substitution< E, V > s;         // substitution
      95             :          *
      96             :          *    s[v] = e;
      97             :          *
      98             :          *    assert(s(v) == e);
      99             :          * \endcode
     100             :          **/
     101          87 :         void operator=(const pbes_expression& e)
     102             :         {
     103          87 :           m_map[m_variable.name()] = std::make_pair(e, m_variable.parameters());
     104          87 :         }
     105             :     };
     106             : 
     107             :     propositional_variable_substitution() = default;
     108             : 
     109             :     propositional_variable_substitution(const map_type& other)
     110             :       : m_map(other)
     111             :     {
     112             :     }
     113             : 
     114             :     /** \brief Update substitution for a single variable
     115             :      *
     116             :      * \param[in] v the variable for which to update the value
     117             :      *
     118             :      * \code
     119             :      *  template< typename E, typename V >
     120             :      *  void example(V const& v, E const& e) {
     121             :      *    substitution< E, V > s;         // substitution
     122             :      *
     123             :      *    std::cout << s(x) << std::endl; // prints x
     124             :      *
     125             :      *    s[v] = e;
     126             :      *
     127             :      *    std::cout << s(x) << std::endl; // prints e
     128             :      *  }
     129             :      * \endcode
     130             :      *
     131             :      * \return expression assignment for variable v, effect
     132             :      **/
     133          87 :     assignment operator[](const propositional_variable& v)
     134             :     {
     135          87 :       return { v, this->m_map };
     136             :     }
     137             : 
     138             :     /// \brief Constructor. Initializes the substitution with the assignment X := phi.
     139          87 :     propositional_variable_substitution(const propositional_variable& X, const pbes_expression& phi)
     140          87 :     {
     141          87 :       (*this)[X] = phi;
     142          87 :     }
     143             : 
     144             :     /// \brief Returns an iterator pointing to the beginning of the sequence of assignments
     145             :     const_iterator begin() const
     146             :     {
     147             :       return m_map.begin();
     148             :     }
     149             : 
     150             :     /// \brief Returns an iterator pointing past the end of the sequence of assignments
     151             :     const_iterator end() const
     152             :     {
     153             :       return m_map.end();
     154             :     }
     155             : 
     156             :     /// \brief Returns an iterator pointing to the beginning of the sequence of assignments
     157             :     iterator begin()
     158             :     {
     159             :       return this->m_map.begin();
     160             :     }
     161             : 
     162             :     /// \brief Returns an iterator pointing past the end of the sequence of assignments
     163             :     iterator end()
     164             :     {
     165             :       return this->m_map.end();
     166             :     }
     167             : 
     168             :     /// \brief Returns an iterator that references the expression associated with v or is equal to m_map.end()
     169             :     iterator find(const variable_type &v)
     170             :     {
     171             :       return this->m_map.find(static_cast<core::identifier_string>(v));
     172             :     }
     173             : 
     174             :     /// \brief Removes the substitution to the propositional variable v.
     175             :     map_type::size_type erase(const propositional_variable& v)
     176             :     {
     177             :       return m_map.erase(static_cast<core::identifier_string>(v));
     178             :     }
     179             : 
     180             :     /// \brief Returns an iterator that references the expression associated with v or is equal to m_map.end()
     181             :     const_iterator find(variable_type const& v) const
     182             :     {
     183             :       return m_map.find(static_cast<core::identifier_string>(v));
     184             :     }
     185             : 
     186             :     /// \brief Returns true if the sequence of assignments is empty
     187             :     bool empty() const
     188             :     {
     189             :       return this->m_map.empty();
     190             :     }
     191             : };
     192             : 
     193             : } // namespace pbes_system
     194             : 
     195             : } // namespace mcrl2
     196             : 
     197             : #endif // MCRL2_PBES_SUBSTITUTIONS_H

Generated by: LCOV version 1.14