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_builder.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_STRUCTURE_GRAPH_BUILDER_H
      13             : #define MCRL2_PBES_STRUCTURE_GRAPH_BUILDER_H
      14             : 
      15             : #include <mcrl2/atermpp/standard_containers/unordered_map.h>
      16             : #include "mcrl2/pbes/pbessolve_vertex_set.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22             : namespace detail {
      23             : 
      24             : struct structure_graph_builder
      25             : {
      26             :   using index_type = structure_graph::index_type;
      27             : 
      28             :   structure_graph& m_graph;
      29             :   atermpp::utilities::unordered_map<pbes_expression, 
      30             :     index_type,
      31             :     std::hash<atermpp::detail::reference_aterm<pbes_expression> >,
      32             :     std::equal_to<atermpp::detail::reference_aterm<pbes_expression> >,
      33             :     std::allocator< std::pair<const atermpp::detail::reference_aterm<pbes_expression>, atermpp::detail::reference_aterm<index_type> > >,
      34             :     true> m_vertex_map;
      35             :   pbes_expression m_initial_state; // The initial state.
      36             : 
      37         137 :   explicit structure_graph_builder(structure_graph& G)
      38         137 :     : m_graph(G), m_initial_state(data::undefined_data_expression())
      39         137 :   {}
      40             : 
      41           0 :   std::size_t extent() const
      42             :   {
      43           0 :     return m_graph.extent();
      44             :   }
      45             : 
      46        7784 :   structure_graph::vertex_vector& vertices()
      47             :   {
      48        7784 :     return m_graph.m_vertices;
      49             :   }
      50             : 
      51             :   const structure_graph::vertex_vector& vertices() const
      52             :   {
      53             :     return m_graph.m_vertices;
      54             :   }
      55             : 
      56       15611 :   structure_graph::vertex& vertex(index_type u)
      57             :   {
      58       15611 :     return m_graph.m_vertices[u];
      59             :   }
      60             : 
      61             :   const structure_graph::vertex& vertex(index_type u) const
      62             :   {
      63             :     return m_graph.m_vertices[u];
      64             :   }
      65             : 
      66        7535 :   structure_graph::decoration_type decoration(const pbes_expression& x) const
      67             :   {
      68        7535 :     if (is_true(x))
      69             :     {
      70          60 :       return structure_graph::d_true;
      71             :     }
      72        7475 :     else if (is_false(x))
      73             :     {
      74         571 :       return structure_graph::d_false;
      75             :     }
      76        6904 :     else if (is_propositional_variable_instantiation(x))
      77             :     {
      78        4813 :       return structure_graph::d_none;
      79             :     }
      80        2091 :     else if (is_and(x))
      81             :     {
      82        1588 :       return structure_graph::d_conjunction;
      83             :     }
      84         503 :     else if (is_or(x))
      85             :     {
      86         503 :       return structure_graph::d_disjunction;
      87             :     }
      88           0 :     throw std::runtime_error("structure_graph_builder: encountered unsupported pbes_expression " + pp(x));
      89             :   }
      90             : 
      91        3892 :   index_type create_vertex(const pbes_expression& x)
      92             :   {
      93        3892 :     assert(m_vertex_map.find(x) == m_vertex_map.end());
      94             : 
      95        3892 :     vertices().emplace_back(x, decoration(x));
      96        3892 :     index_type index = vertices().size() - 1;
      97        3892 :     m_vertex_map.insert({ x, index });
      98        3892 :     return index;
      99             :   }
     100             : 
     101             :   // insert the variable corresponding to the equation x = phi; overwrites existing value, but leaves pred/succ intact
     102        3643 :   index_type insert_variable(const pbes_expression& x, const pbes_expression& psi, std::size_t k)
     103             :   {
     104        3643 :     auto i = m_vertex_map.find(x);
     105        3643 :     index_type ui = i == m_vertex_map.end() ? create_vertex(x) : static_cast<unsigned int>(i->second);
     106        3643 :     auto& u = vertex(ui);
     107        3643 :     u.decoration = decoration(psi);
     108        3643 :     u.rank = k;
     109        3643 :     return ui;
     110             :   }
     111             : 
     112             :   // insert the variable x; does not overwrite existing value
     113        1170 :   index_type insert_variable(const pbes_expression& x)
     114             :   {
     115        1170 :     auto i = m_vertex_map.find(x);
     116        1170 :     if (i != m_vertex_map.end())
     117             :     {
     118         862 :       return i->second;
     119             :     }
     120             :     else
     121             :     {
     122         308 :       return create_vertex(x);
     123             :     }
     124             :   }
     125             : 
     126        4814 :   index_type insert_vertex(const pbes_expression& x)
     127             :   {
     128             :     // if the vertex already exists, return it
     129        4814 :     auto i = m_vertex_map.find(x);
     130        4814 :     if (i != m_vertex_map.end())
     131             :     {
     132        1367 :       return i->second;
     133             :     }
     134             : 
     135             :     // create a new vertex, and return it
     136        3447 :     return create_vertex(x);
     137             :   }
     138             : 
     139        5984 :   void insert_edge(index_type ui, index_type vi)
     140             :   {
     141             :     using utilities::detail::contains;
     142        5984 :     auto& u = vertex(ui);
     143        5984 :     auto& v = vertex(vi);
     144        5984 :     if (!contains(u.successors, vi))
     145             :     {
     146        5982 :       u.successors.push_back(vi);
     147        5982 :       v.predecessors.push_back(ui);
     148             :     }
     149        5984 :   }
     150             : 
     151         137 :   void set_initial_state(const propositional_variable_instantiation& x)
     152             :   {
     153         137 :     m_initial_state = x;
     154         137 :   }
     155             : 
     156         137 :   structure_graph::index_type initial_vertex() const
     157             :   {
     158         137 :     auto i = m_vertex_map.find(m_initial_state);
     159         137 :     assert (i != m_vertex_map.end());
     160         137 :     return i->second;
     161             :   }
     162             : 
     163             :   // call at the end, to put the results into m_graph
     164         137 :   void finalize()
     165             :   {
     166         137 :     m_graph.m_initial_vertex = initial_vertex();
     167         137 :     m_graph.m_exclude = boost::dynamic_bitset<>(m_graph.extent());
     168         137 :   }
     169             : 
     170             :   index_type find_vertex(const pbes_expression& x) const
     171             :   {
     172             :     auto i = m_vertex_map.find(x);
     173             :     if (i == m_vertex_map.end())
     174             :     {
     175             :       return undefined_vertex();
     176             :     }
     177             :     return i->second;
     178             :   }
     179             : 
     180             :   // Erases all vertices in the set U.
     181             :   void erase_vertices(const vertex_set& U)
     182             :   {
     183             :     // mCRL2log(log::debug) << "erasing nodes " << U << std::endl;
     184             : 
     185             :     using utilities::detail::contains;
     186             : 
     187             :     // compute new index for the vertices
     188             :     std::vector<index_type> index;
     189             :     structure_graph::index_type count = 0;
     190             :     for (index_type u = 0; u != vertices().size(); u++)
     191             :     {
     192             :       index.push_back(U.contains(u) ? undefined_vertex() : count++);
     193             :     }
     194             : 
     195             :     // computes new predecessors / successors
     196             :     auto update = [&](const std::vector<index_type>& V) {
     197             :       std::vector<index_type> result;
     198             :       for (auto v: V)
     199             :       {
     200             :         if (index[v] != undefined_vertex())
     201             :         {
     202             :           result.push_back(index[v]);
     203             :         }
     204             :       }
     205             :       return result;
     206             :     };
     207             : 
     208             :     for (index_type u = 0; u != vertices().size(); u++)
     209             :     {
     210             :       if (index[u] != undefined_vertex())
     211             :       {
     212             :         structure_graph::vertex& u_ = vertex(u);
     213             :         u_.predecessors = update(u_.predecessors);
     214             :         u_.successors = update(u_.successors);
     215             :         if (u_.strategy != undefined_vertex())
     216             :         {
     217             :           u_.strategy = index[u_.strategy];
     218             :         }
     219             :         if (index[u] != u)
     220             :         {
     221             :           std::swap(vertex(u), vertex(index[u]));
     222             :         }
     223             :       }
     224             :     }
     225             : 
     226             :     vertices().erase(vertices().begin() + vertices().size() - U.size(), vertices().end());
     227             : 
     228             :     // Recreate the index
     229             :     m_vertex_map.clear();
     230             :     for (std::size_t i = 0; i < vertices().size(); i++)
     231             :     {
     232             :       m_vertex_map.insert({vertex(i).formula(), i});
     233             :     }
     234             :   }
     235             : };
     236             : 
     237             : struct manual_structure_graph_builder
     238             : {
     239             :   typedef structure_graph::index_type index_type;
     240             : 
     241             :   structure_graph& m_graph;
     242             :   structure_graph::vertex_vector m_vertices;
     243             :   index_type m_initial_state; // The initial state.
     244             : 
     245             :   explicit manual_structure_graph_builder(structure_graph& G)
     246             :     : m_graph(G)
     247             :   {}
     248             : 
     249             :   /// \brief Create a vertex, returns the index of the new vertex
     250             :   index_type insert_vertex(bool is_conjunctive, std::size_t rank)
     251             :   {
     252             :     m_vertices.emplace_back(pbes_expression(), is_conjunctive ? structure_graph::d_conjunction : structure_graph::d_disjunction, rank);
     253             :     return m_vertices.size() - 1;
     254             :   }
     255             : 
     256             :   void insert_edge(index_type ui, index_type vi)
     257             :   {
     258             :     using utilities::detail::contains;
     259             :     structure_graph::vertex& u = m_vertices[ui];
     260             :     structure_graph::vertex& v = m_vertices[vi];
     261             :     if (!contains(u.successors, vi))
     262             :     {
     263             :       u.successors.push_back(vi);
     264             :       v.predecessors.push_back(ui);
     265             :     }
     266             :   }
     267             : 
     268             :   void remove_edge(index_type ui, index_type vi)
     269             :   {
     270             :     structure_graph::vertex& u = m_vertices[ui];
     271             :     structure_graph::vertex& v = m_vertices[vi];
     272             :     u.remove_successor(vi);
     273             :     v.remove_predecessor(ui);
     274             :   }
     275             : 
     276             :   void set_initial_state(const index_type i)
     277             :   {
     278             :     m_initial_state = i;
     279             :   }
     280             : 
     281             :   /// \brief call at the end, to put the results into m_graph
     282             :   /// \details May be called more than once. Does not invalidate this builder.
     283             :   void finalize()
     284             :   {
     285             :     m_graph.m_vertices = m_vertices;
     286             :     m_graph.m_initial_vertex = m_initial_state;
     287             : 
     288             :     std::size_t N = m_vertices.size();
     289             :     m_graph.m_exclude = boost::dynamic_bitset<>(N);
     290             :   }
     291             : };
     292             : 
     293             : } // namespace detail
     294             : 
     295             : } // namespace pbes_system
     296             : 
     297             : } // namespace mcrl2
     298             : 
     299             : #endif // MCRL2_PBES_STRUCTURE_GRAPH_BUILDER_H