Line data    Source code

       1             : // Copyright (c) 2009-2013 University of Twente
       2             : // Copyright (c) 2009-2013 Michael Weber <michaelw@cs.utwente.nl>
       3             : // Copyright (c) 2009-2013 Maks Verver <maksverver@geocities.com>
       4             : // Copyright (c) 2009-2013 Eindhoven University of Technology
       5             : //
       6             : // Distributed under the Boost Software License, Version 1.0.
       7             : // (See accompanying file LICENSE_1_0.txt or copy at
       8             : // http://www.boost.org/LICENSE_1_0.txt)
       9             : 
      10             : #ifndef MCRL2_PG_ATTRACTOR_IMPL_H
      11             : #define MCRL2_PG_ATTRACTOR_IMPL_H
      12             : 
      13             : #include "mcrl2/pg/attractor.h"
      14             : #include "mcrl2/pg/ParityGame_impl.h"
      15             : 
      16             : #include <queue>
      17             : 
      18             : template<class ForwardIterator, class SetT>
      19           0 : bool is_subset_of(ForwardIterator it, ForwardIterator end, const SetT &set)
      20             : {
      21           0 :     for (; it != end; ++it) if (!set.count(*it)) return false;
      22           0 :     return true;
      23             : }
      24             : 
      25             : template<class SetT, class StrategyT>
      26             : void make_attractor_set( const ParityGame &game, ParityGame::Player player,
      27             :                          SetT &vertices, StrategyT &strategy )
      28             : {
      29             :     std::deque<verti> todo(vertices.begin(), vertices.end());
      30             :     return make_attractor_set(game, player, vertices, todo, strategy);
      31             : }
      32             : 
      33             : template<class SetT, class DequeT, class StrategyT>
      34           0 : void make_attractor_set( const ParityGame &game, ParityGame::Player player,
      35             :     SetT &vertices, DequeT &todo, StrategyT &strategy )
      36             : {
      37           0 :     const StaticGraph &graph = game.graph();
      38             : 
      39           0 :     while (!todo.empty())
      40             :     {
      41           0 :         const verti w = todo.front();
      42           0 :         todo.pop_front();
      43             : 
      44             :         // Check all predecessors v of w:
      45           0 :         for (StaticGraph::const_iterator it = graph.pred_begin(w);
      46           0 :              it != graph.pred_end(w); ++it)
      47             :         {
      48           0 :             const verti v = *it;
      49             : 
      50             :             // Skip predecessors that are already in the attractor set:
      51           0 :             if (vertices.find(v) != vertices.end()) continue;
      52             : 
      53           0 :             if (game.player(v) == player)
      54             :             {
      55             :                 // Store strategy for player-controlled vertex:
      56           0 :                 strategy[v] = w;
      57             :             }
      58             :             else  // opponent controls vertex
      59           0 :             if (is_subset_of(graph.succ_begin(v), graph.succ_end(v), vertices))
      60             :             {
      61             :                 // Store strategy for opponent-controlled vertex:
      62           0 :                 strategy[v] = NO_VERTEX;
      63             :             }
      64             :             else
      65             :             {
      66           0 :                 continue;  // not in the attractor set yet!
      67             :             }
      68             : 
      69             :             // Add vertex v to the attractor set:
      70           0 :             vertices.insert(v);
      71           0 :             todo.push_back(v);
      72             :         }
      73             :     }
      74           0 : }
      75             : 
      76             : template<class SetT, class StrategyT>
      77           0 : void make_attractor_set_2( const ParityGame &game, ParityGame::Player player,
      78             :                            SetT &vertices, StrategyT &strategy )
      79             : {
      80           0 :     std::deque<verti> todo(vertices.begin(), vertices.end());
      81           0 :     return make_attractor_set_2(game, player, vertices, todo, strategy);
      82           0 : }
      83             : 
      84             : // Experimental, alternate implementation.
      85             : // Only uses predecessor edges but uses O(|V|) extra space and O(|E|) extra time.
      86             : // TODO: document!
      87             : template<class SetT, class DequeT, class StrategyT>
      88           0 : void make_attractor_set_2( const ParityGame &game, ParityGame::Player player,
      89             :     SetT &vertices, DequeT &todo, StrategyT &strategy )
      90             : {
      91           0 :     const StaticGraph &graph = game.graph();
      92             : 
      93             :     // Initialize liberties so that liberties[v] == outdegree of v
      94           0 :     std::vector<verti> liberties(graph.V(), 0);
      95           0 :     for (verti v = 0; v < graph.V(); ++v)
      96             :     {
      97           0 :         for (StaticGraph::const_iterator it = graph.pred_begin(v);
      98           0 :              it != graph.pred_end(v); ++it) ++liberties[*it];
      99             :     }
     100             : 
     101             :     // Mark initial set as included:
     102           0 :     for (typename SetT::const_iterator it = vertices.begin();
     103           0 :          it != vertices.end(); ++it)
     104             :     {
     105           0 :         liberties[*it] = 0;
     106             :     }
     107             : 
     108             :     // Process queue:
     109           0 :     while (!todo.empty())
     110             :     {
     111           0 :         const verti w = todo.front();
     112           0 :         todo.pop_front();
     113             : 
     114             :         // Check all predecessors v of w:
     115           0 :         for (StaticGraph::const_iterator it = graph.pred_begin(w);
     116           0 :              it != graph.pred_end(w); ++it)
     117             :         {
     118           0 :             const verti v = *it;
     119             : 
     120             :             // Skip predecessors that are already in the attractor set:
     121           0 :             if (liberties[v] == 0) continue;
     122             : 
     123           0 :             if (game.player(v) == player)
     124             :             {
     125             :                 // Store strategy for player-controlled vertex:
     126           0 :                 strategy[v] = w;
     127           0 :                 liberties[v] = 0;
     128             :             }
     129             :             else  // opponent controls vertex
     130           0 :             if (--liberties[v] == 0)
     131             :             {
     132             :                 // Store strategy for opponent-controlled vertex:
     133           0 :                 strategy[v] = NO_VERTEX;
     134             :             }
     135             :             else
     136             :             {
     137           0 :                 continue;  // not in the attractor set yet!
     138             :             }
     139             : 
     140             :             // Add vertex v to the attractor set:
     141           0 :             vertices.insert(v);
     142           0 :             todo.push_back(v);
     143             :         }
     144             :     }
     145           0 : }
     146             : 
     147             : #endif // MCRL2_PG_ATTRACTOR_IMPL_H