LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes - structure_graph.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 47 107 43.9 %
Date: 2024-03-08 02:52:28 Functions: 21 32 65.6 %
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/structure_graph.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_STRUCTURE_GRAPH_H
      13             : #define MCRL2_PBES_STRUCTURE_GRAPH_H
      14             : 
      15             : #include <iomanip>
      16             : #include <boost/dynamic_bitset.hpp>
      17             : #include <boost/range/adaptor/filtered.hpp>
      18             : 
      19             : #include "mcrl2/atermpp/standard_containers/vector.h"
      20             : #include "mcrl2/core/detail/print_utility.h"
      21             : #include "mcrl2/pbes/pbes.h"
      22             : 
      23             : namespace mcrl2 {
      24             : 
      25             : namespace pbes_system {
      26             : 
      27             : namespace detail {
      28             : 
      29             : struct structure_graph_builder;
      30             : struct manual_structure_graph_builder;
      31             : 
      32             : } // namespace detail
      33             : 
      34             : constexpr inline
      35        6267 : unsigned int undefined_vertex()
      36             : {
      37        6267 :   return std::numeric_limits<unsigned int>::max();
      38             : }
      39             : 
      40             : // A structure graph with a facility to exclude a subset of the vertices.
      41             : // It has the same interface as simple_structure_graph.
      42             : class structure_graph
      43             : {
      44             :   friend struct detail::structure_graph_builder;
      45             :   friend struct detail::manual_structure_graph_builder;
      46             : 
      47             : 
      48             :   public:
      49             :     enum decoration_type
      50             :     {
      51             :       d_disjunction = 0,
      52             :       d_conjunction = 1,
      53             :       d_true,
      54             :       d_false,
      55             :       d_none
      56             :     };
      57             : 
      58             :     using index_type = unsigned int;
      59             : 
      60             :     struct vertex
      61             :     {
      62             :       atermpp::detail::reference_aterm<pbes_expression> m_formula;
      63             :       decoration_type decoration;
      64             :       std::size_t rank;
      65             :       std::vector<index_type> predecessors;
      66             :       std::vector<index_type> successors;
      67             :       mutable index_type strategy;
      68             : 
      69        3776 :       explicit vertex(pbes_expression  formula_,
      70             :              decoration_type decoration_ = structure_graph::d_none,
      71             :              std::size_t rank_ = data::undefined_index(),
      72             :              std::vector<index_type> pred_ = std::vector<index_type>(),
      73             :              std::vector<index_type> succ_ = std::vector<index_type>(),
      74             :              index_type strategy_ = undefined_vertex()
      75             :             )
      76        3776 :         : m_formula(std::move(formula_)),
      77        3776 :           decoration(decoration_),
      78        3776 :           rank(rank_),
      79        3776 :           predecessors(std::move(pred_)),
      80        3776 :           successors(std::move(succ_)),
      81        3776 :           strategy(strategy_)
      82        3776 :       {}
      83             : 
      84             :       void remove_predecessor(index_type u)
      85             :       {
      86             :         predecessors.erase(std::remove(predecessors.begin(), predecessors.end(), u), predecessors.end());
      87             :       }
      88             : 
      89             :       // Downcast reference aterm
      90           0 :       inline pbes_expression formula() const
      91             :       {
      92           0 :         return m_formula;
      93             :       }
      94             : 
      95             :       void remove_successor(index_type u)
      96             :       {
      97             :         successors.erase(std::remove(successors.begin(), successors.end(), u), successors.end());
      98             :       }
      99             : 
     100        3776 :       bool is_defined() const
     101             :       {
     102        1161 :         return  ((decoration != structure_graph::d_none) || (rank != data::undefined_index()))
     103        4937 :              && (!successors.empty() || (decoration == d_true || decoration == d_false));
     104             :       }
     105             :       
     106           0 :       void inline mark(atermpp::term_mark_stack& todo) const
     107             :       {
     108           0 :         mark_term(m_formula, todo);
     109           0 :       }
     110             :     };
     111             : 
     112             :     using vertex_vector = atermpp::vector<vertex, std::allocator<atermpp::detail::reference_aterm<vertex>>, mcrl2::utilities::detail::GlobalThreadSafe>;
     113             : 
     114             :   protected:
     115             :     vertex_vector m_vertices;
     116             :     index_type m_initial_vertex = 0;
     117             :     boost::dynamic_bitset<> m_exclude;
     118             : 
     119             :     struct integers_not_contained_in
     120             :     {
     121             :       const boost::dynamic_bitset<>& subset;
     122             : 
     123        8244 :       explicit integers_not_contained_in(const boost::dynamic_bitset<>& subset_)
     124        8244 :         : subset(subset_)
     125        8244 :       {}
     126             : 
     127       11735 :       bool operator()(index_type i) const
     128             :       {
     129       11735 :         return !subset[i];
     130             :       }
     131             :     };
     132             : 
     133             :     struct vertices_not_contained_in
     134             :     {
     135             :       const vertex_vector& vertices;
     136             :       const boost::dynamic_bitset<>& subset;
     137             : 
     138             :       vertices_not_contained_in(const vertex_vector& vertices_, const boost::dynamic_bitset<>& subset_)
     139             :         : vertices(vertices_),
     140             :           subset(subset_)
     141             :       {}
     142             : 
     143             :       bool operator()(const vertex& v) const
     144             :       {
     145             :         std::size_t i = &v - &static_cast<const vertex&>(vertices.front());
     146             :         return !subset[i];
     147             :       }
     148             :     };
     149             : 
     150             :   public:
     151         133 :     structure_graph() = default;
     152             : 
     153           0 :     structure_graph(vertex_vector vertices, index_type initial_vertex, boost::dynamic_bitset<> exclude)
     154           0 :       : m_vertices(std::move(vertices)),
     155           0 :         m_initial_vertex(initial_vertex),
     156           0 :         m_exclude(std::move(exclude))
     157           0 :     {}
     158             : 
     159         209 :     index_type initial_vertex() const
     160             :     {
     161         209 :       return m_initial_vertex;
     162             :     }
     163             : 
     164         575 :     std::size_t extent() const
     165             :     {
     166         575 :       return m_vertices.size();
     167             :     }
     168             : 
     169        3072 :     decoration_type decoration(index_type u) const
     170             :     {
     171        3072 :       return find_vertex(u).decoration;
     172             :     }
     173             : 
     174             :     std::size_t rank(index_type u) const
     175             :     {
     176             :       return find_vertex(u).rank;
     177             :     }
     178             : 
     179         219 :     const vertex_vector& all_vertices() const
     180             :     {
     181         219 :       return m_vertices;
     182             :     }
     183             : 
     184        3791 :     const std::vector<index_type>& all_predecessors(index_type u) const
     185             :     {
     186        3791 :       return find_vertex(u).predecessors;
     187             :     }
     188             : 
     189        4453 :     const std::vector<index_type>& all_successors(index_type u) const
     190             :     {
     191        4453 :       return find_vertex(u).successors;
     192             :     }
     193             : 
     194             :     boost::filtered_range<vertices_not_contained_in, const vertex_vector> vertices() const
     195             :     {
     196             :       return all_vertices() | boost::adaptors::filtered(vertices_not_contained_in(m_vertices, m_exclude));
     197             :     }
     198             : 
     199        3791 :     boost::filtered_range<integers_not_contained_in, const std::vector<index_type>> predecessors(index_type u) const
     200             :     {
     201        7582 :       return all_predecessors(u) | boost::adaptors::filtered(integers_not_contained_in(m_exclude));
     202             :     }
     203             : 
     204        4453 :     boost::filtered_range<integers_not_contained_in, const std::vector<index_type>> successors(index_type u) const
     205             :     {
     206        8906 :       return all_successors(u) | boost::adaptors::filtered(integers_not_contained_in(m_exclude));
     207             :     }
     208             : 
     209           0 :     index_type strategy(index_type u) const
     210             :     {
     211           0 :       return find_vertex(u).strategy;
     212             :     }
     213             : 
     214        4476 :     vertex& find_vertex(index_type u)
     215             :     {
     216        4476 :       return m_vertices[u];
     217             :     }
     218             : 
     219       15370 :     const vertex& find_vertex(index_type u) const
     220             :     {
     221       15370 :       return m_vertices[u];
     222             :     }
     223             : 
     224           0 :     const boost::dynamic_bitset<>& exclude() const
     225             :     {
     226           0 :       return m_exclude;
     227             :     }
     228             : 
     229         479 :     boost::dynamic_bitset<>& exclude()
     230             :     {
     231         479 :       return m_exclude;
     232             :     }
     233             : 
     234        5796 :     bool contains(index_type u) const
     235             :     {
     236        5796 :       return !m_exclude[u];
     237             :     }
     238             : 
     239             :     // TODO: avoid this linear time check
     240         176 :     bool is_empty() const
     241             :     {
     242         176 :       return m_exclude.all();
     243             :     }
     244             : 
     245             :     // Returns true if all vertices have a rank and a decoration
     246         133 :     bool is_defined() const
     247             :     {
     248        3909 :       return std::all_of(m_vertices.begin(), m_vertices.end(), [](const vertex& u) { return u.is_defined(); });
     249             :     }
     250             : };
     251             : 
     252             : template <typename StructureGraph>
     253           0 : std::vector<typename StructureGraph::index_type> structure_graph_predecessors(const StructureGraph& G, typename StructureGraph::index_type u)
     254             : {
     255           0 :   std::vector<typename StructureGraph::index_type> result;
     256           0 :   for (auto v: G.predecessors(u))
     257             :   {
     258           0 :     result.push_back(v);
     259             :   }
     260           0 :   return result;
     261           0 : }
     262             : 
     263             : template <typename StructureGraph>
     264           0 : std::vector<typename StructureGraph::index_type> structure_graph_successors(const StructureGraph& G, typename StructureGraph::index_type u)
     265             : {
     266           0 :   std::vector<typename StructureGraph::index_type> result;
     267           0 :   for (auto v: G.successors(u))
     268             :   {
     269           0 :     result.push_back(v);
     270             :   }
     271           0 :   return result;
     272           0 : }
     273             : 
     274             : inline
     275           0 : std::ostream& operator<<(std::ostream& out, const structure_graph::decoration_type& decoration)
     276             : {
     277           0 :   switch (decoration)
     278             :   {
     279           0 :     case structure_graph::d_conjunction : { out << "conjunction"; break; }
     280           0 :     case structure_graph::d_disjunction : { out << "disjunction"; break; }
     281           0 :     case structure_graph::d_true        : { out << "true";        break; }
     282           0 :     case structure_graph::d_false       : { out << "false";       break; }
     283           0 :     default                             : { out << "none";        break; }
     284             :   }
     285           0 :   return out;
     286             : }
     287             : 
     288             : inline
     289           0 : std::ostream& operator<<(std::ostream& out, const structure_graph::vertex& u)
     290             : {
     291           0 :   out << "vertex(formula = " << u.formula()
     292           0 :       << ", decoration = " << u.decoration
     293           0 :       << ", rank = " << (u.rank == data::undefined_index() ? std::string("undefined") : std::to_string(u.rank))
     294           0 :       << ", predecessors = " << core::detail::print_list(u.predecessors)
     295           0 :       << ", successors = " << core::detail::print_list(u.successors)
     296           0 :       << ", strategy = " << (u.strategy == undefined_vertex() ? std::string("undefined") : std::to_string(u.strategy))
     297           0 :       << ")";
     298           0 :   return out;
     299             : }
     300             : 
     301             : template <typename StructureGraph>
     302           0 : std::ostream& print_structure_graph(std::ostream& out, const StructureGraph& G)
     303             : {
     304           0 :   auto N = G.all_vertices().size();
     305           0 :   for (std::size_t i = 0; i < N; i++)
     306             :   {
     307           0 :     if (G.contains(i))
     308             :     {
     309           0 :       const structure_graph::vertex& u = G.find_vertex(i);
     310           0 :       out << std::setw(4) << i << " "
     311           0 :           << "vertex(formula = " << u.formula()
     312           0 :           << ", decoration = " << u.decoration
     313           0 :           << ", rank = " << (u.rank == data::undefined_index() ? std::string("undefined") : std::to_string(u.rank))
     314             :           << ", predecessors = " << core::detail::print_list(structure_graph_predecessors(G, i))
     315             :           << ", successors = " << core::detail::print_list(structure_graph_successors(G, i))
     316           0 :           << ", strategy = " << (u.strategy == undefined_vertex() ? std::string("undefined") : std::to_string(u.strategy))
     317           0 :           << ")"
     318           0 :           << std::endl;
     319             :     }
     320             :   }
     321           0 :   if (G.is_empty())
     322             :   {
     323           0 :     out << "  empty" << std::endl;
     324             :   }
     325           0 :   return out;
     326             : }
     327             : 
     328             : inline
     329           0 : std::ostream& operator<<(std::ostream& out, const structure_graph& G)
     330             : {
     331           0 :   return print_structure_graph(out, G);
     332             : }
     333             : 
     334             : } // namespace pbes_system
     335             : 
     336             : } // namespace mcrl2
     337             : 
     338             : #endif // MCRL2_PBES_STRUCTURE_GRAPH_H

Generated by: LCOV version 1.14