LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes - abstract.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 43 50 86.0 %
Date: 2024-03-08 02:52:28 Functions: 7 8 87.5 %
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/abstract.h
      10             : /// \brief The PBES abstract algorithm.
      11             : 
      12             : #ifndef MCRL2_PBES_ABSTRACT_H
      13             : #define MCRL2_PBES_ABSTRACT_H
      14             : 
      15             : #include "mcrl2/data/consistency.h"
      16             : #include "mcrl2/pbes/builder.h"
      17             : #include "mcrl2/pbes/detail/pbes_parameter_map.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace pbes_system
      23             : {
      24             : 
      25             : namespace detail
      26             : {
      27             : 
      28             : /// \brief Visitor that implements the pbes-abstract algorithm.
      29             : struct pbes_abstract_builder: public pbes_expression_builder<pbes_abstract_builder>
      30             : {
      31             :   typedef pbes_expression_builder<pbes_abstract_builder> super;
      32             :   using super::apply;
      33             : 
      34             :   std::vector<data::variable_list> m_quantifier_stack;
      35             :   const std::vector<data::variable> m_selected_variables;
      36             :   const data::data_expression m_value;
      37             : 
      38           3 :   pbes_abstract_builder(const std::vector<data::variable>& selected_variables, bool value_true)
      39           3 :     : m_selected_variables(selected_variables),
      40           6 :       m_value(value_true ? data::true_() : data::false_())
      41           3 :   {}
      42             : 
      43             :   /// \brief Returns true if the m_quantifier_stack contains a given data variable
      44           2 :   bool is_bound(const data::variable& v) const
      45             :   {
      46           2 :     for (const data::variable_list& variables: m_quantifier_stack)
      47             :     {
      48           1 :       for (const data::variable& w: variables)
      49             :       {
      50           1 :         if (w == v)
      51             :         {
      52           1 :           return true;
      53             :         }
      54             :       }
      55             :     }
      56           1 :     return false;
      57             :   }
      58             : 
      59             :   /// \brief Adds a sequence of variables to the quantifier stack.
      60           1 :   void push_variables(const data::variable_list& variables)
      61             :   {
      62           1 :     m_quantifier_stack.push_back(variables);
      63           1 :   }
      64             : 
      65             :   /// \brief Removes the last added sequence of variables from the quantifier stack.
      66           1 :   void pop_variables()
      67             :   {
      68           1 :     m_quantifier_stack.pop_back();
      69           1 :   }
      70             : 
      71             :   /// \brief Visit data_expression node
      72             :   template <class T>
      73           3 :   void apply(T& result, const data::data_expression& d)
      74             :   {
      75           3 :     std::set<data::variable> FV = data::find_free_variables(d);
      76           5 :     for (const data::variable& v: FV)
      77             :     {
      78           3 :       if (std::find(m_selected_variables.begin(), m_selected_variables.end(), v) == m_selected_variables.end())
      79             :       {
      80           1 :         continue;
      81             :       }
      82           2 :       if (!is_bound(v))
      83             :       {
      84             :         //std::clog << "Reducing data expression " << data::pp(d) << " to " << data::pp(m_value) << "." << std::endl;
      85           1 :         result = m_value;
      86           1 :         return;
      87             :       }
      88             :     }
      89           2 :     result = d;
      90           3 :   }
      91             : 
      92             :   /// \brief Visit forall node
      93             :   template <class T>
      94           0 :   void apply(T& result, const forall& x)
      95             :   {
      96           0 :     push_variables(x.variables());
      97           0 :     pbes_expression new_expression;
      98           0 :     apply(new_expression, x.body());
      99           0 :     pop_variables();
     100           0 :     result = make_forall_(x.variables(), new_expression);
     101           0 :   }
     102             : 
     103             :   /// \brief Visit exists node
     104             :   template <class T>
     105           1 :   void apply(T& result, const exists& x)
     106             :   {
     107           1 :     push_variables(x.variables());
     108           1 :     pbes_expression new_expression;
     109           1 :     apply(new_expression, x.body());
     110           1 :     pop_variables();
     111           1 :     result = make_exists_(x.variables(), new_expression);
     112           1 :   }
     113             : };
     114             : 
     115             : } // namespace detail
     116             : 
     117             : 
     118             : /// \brief Algorithm class for the abstract algorithm
     119             : class pbes_abstract_algorithm
     120             : {
     121             :   public:
     122             :     /// \brief Runs the algorithm.
     123             :     /// \param p A PBES.
     124             :     /// \param parameter_map A map containing the parameters that should be expanded by the algorithm.
     125             :     /// \param value_true An indication whether the abstraction is towards true or towards false.
     126           3 :     void run(pbes& p,
     127             :              const detail::pbes_parameter_map& parameter_map,
     128             :              bool value_true
     129             :             )
     130             :     {
     131           8 :       for (pbes_equation& eqn: p.equations())
     132             :       {
     133           5 :         auto j = parameter_map.find(eqn.variable().name());
     134           5 :         if (j != parameter_map.end())
     135             :         {
     136           3 :           detail::pbes_abstract_builder builder(j->second, value_true);
     137           3 :           pbes_expression result;
     138           3 :           builder.apply(result, eqn.formula());
     139           3 :           eqn.formula() = result;
     140           3 :         }
     141             :       }
     142           3 :     }
     143             : };
     144             : 
     145             : } // namespace pbes_system
     146             : 
     147             : } // namespace mcrl2
     148             : 
     149             : #endif // MCRL2_PBES_ABSTRACT_H

Generated by: LCOV version 1.14