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: 37 42 88.1 %
Date: 2020-09-16 00:45:56 Functions: 8 9 88.9 %
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           3 : 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           3 :       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           3 :   pbes_expression apply(const data::data_expression& d)
      73             :   {
      74           6 :     std::set<data::variable> FV = data::find_free_variables(d);
      75           5 :     for (const data::variable& v: FV)
      76             :     {
      77           3 :       if (std::find(m_selected_variables.begin(), m_selected_variables.end(), v) == m_selected_variables.end())
      78             :       {
      79           1 :         continue;
      80             :       }
      81           2 :       if (!is_bound(v))
      82             :       {
      83             :         //std::clog << "Reducing data expression " << data::pp(d) << " to " << data::pp(m_value) << "." << std::endl;
      84           1 :         return m_value;
      85             :       }
      86             :     }
      87           2 :     return d;
      88             :   }
      89             : 
      90             :   /// \brief Visit forall node
      91           0 :   pbes_expression apply(const forall& x)
      92             :   {
      93           0 :     push_variables(x.variables());
      94           0 :     pbes_expression new_expression = apply(x.body());
      95           0 :     pop_variables();
      96           0 :     return make_forall(x.variables(), new_expression);
      97             :   }
      98             : 
      99             :   /// \brief Visit exists node
     100           1 :   pbes_expression apply(const exists& x)
     101             :   {
     102           1 :     push_variables(x.variables());
     103           2 :     pbes_expression new_expression = apply(x.body());
     104           1 :     pop_variables();
     105           2 :     return make_exists(x.variables(), new_expression);
     106             :   }
     107             : };
     108             : 
     109             : } // namespace detail
     110             : 
     111             : 
     112             : /// \brief Algorithm class for the abstract algorithm
     113             : class pbes_abstract_algorithm
     114             : {
     115             :   public:
     116             :     /// \brief Runs the algorithm.
     117             :     /// \param p A PBES.
     118             :     /// \param parameter_map A map containing the parameters that should be expanded by the algorithm.
     119             :     /// \param value_true An indication whether the abstraction is towards true or towards false.
     120           3 :     void run(pbes& p,
     121             :              const detail::pbes_parameter_map& parameter_map,
     122             :              bool value_true
     123             :             )
     124             :     {
     125           8 :       for (pbes_equation& eqn: p.equations())
     126             :       {
     127           5 :         auto j = parameter_map.find(eqn.variable().name());
     128           5 :         if (j != parameter_map.end())
     129             :         {
     130           6 :           detail::pbes_abstract_builder builder(j->second, value_true);
     131           3 :           eqn.formula() = builder.apply(eqn.formula());
     132             :         }
     133             :       }
     134           3 :     }
     135             : };
     136             : 
     137             : } // namespace pbes_system
     138             : 
     139             : } // namespace mcrl2
     140             : 
     141             : #endif // MCRL2_PBES_ABSTRACT_H

Generated by: LCOV version 1.13