LCOV - code coverage report
Current view: top level - pg/source - ParityGame.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 158 0.0 %
Date: 2024-03-08 02:52:28 Functions: 0 15 0.0 %
Legend: Lines: hit not hit

          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             : #include "mcrl2/pg/ParityGame_impl.h"
      11             : 
      12             : #include <deque>
      13             : #include <map>
      14             : #include <cstdlib>
      15             : 
      16           0 : ParityGame::ParityGame()
      17           0 :     : d_(0), vertex_(NULL), cardinality_(NULL)
      18             : {
      19           0 : }
      20             : 
      21           0 : ParityGame::~ParityGame()
      22             : {
      23           0 :     delete[] vertex_;
      24           0 :     delete[] cardinality_;
      25           0 : }
      26             : 
      27           0 : void ParityGame::clear()
      28             : {
      29           0 :     delete[] vertex_;
      30           0 :     delete[] cardinality_;
      31             : 
      32           0 :     d_ = 0;
      33           0 :     graph_.clear();
      34           0 :     vertex_ = NULL;
      35           0 :     cardinality_ = NULL;
      36           0 : }
      37             : 
      38           0 : void ParityGame::assign(const ParityGame &game)
      39             : {
      40           0 :     if (&game == this) return;
      41             : 
      42           0 :     graph_.assign(game.graph_);
      43           0 :     verti V = graph_.V();
      44           0 :     reset(V, game.d_);
      45           0 :     std::copy(game.vertex_, game.vertex_ + V, vertex_);
      46           0 :     recalculate_cardinalities(V);
      47             : }
      48             : 
      49           0 : void ParityGame::assign(const StaticGraph& g, ParityGameVertex* v)
      50             : {
      51           0 :     delete[] vertex_;
      52           0 :     delete[] cardinality_;
      53             : 
      54           0 :     vertex_ = v;
      55           0 :     graph_.assign(g);
      56           0 :     d_ = 0;
      57           0 :     for(verti i = 0; i < g.V(); i++)
      58             :     {
      59           0 :         d_ = std::max(d_, static_cast<int>(v[i].priority + 1));
      60             :     }
      61           0 :     cardinality_ = new verti[d_];
      62           0 :     recalculate_cardinalities(g.V());
      63           0 : }
      64             : 
      65           0 : void ParityGame::reset(verti V, int d)
      66             : {
      67           0 :     delete[] vertex_;
      68           0 :     delete[] cardinality_;
      69             : 
      70           0 :     d_ = d;
      71           0 :     vertex_ = new ParityGameVertex[V];
      72           0 :     cardinality_ = new verti[d_];
      73           0 : }
      74             : 
      75           0 : void ParityGame::recalculate_cardinalities(verti num_vertices)
      76             : {
      77           0 :     std::fill(cardinality_, cardinality_ + d_, 0);
      78           0 :     for (verti v = 0; v < num_vertices; ++v)
      79             :     {
      80           0 :         cardinality_[vertex_[v].priority] += 1;
      81             :     }
      82           0 : }
      83             : 
      84           0 : void ParityGame::make_random( verti V, unsigned clustersize, unsigned outdeg,
      85             :                               StaticGraph::EdgeDirection edge_dir, int d )
      86             : {
      87           0 :     graph_.make_random_clustered(clustersize > 0 ? clustersize : V,
      88             :                                  V, outdeg, edge_dir);
      89           0 :     if (clustersize > 0) graph_.shuffle_vertices();
      90           0 :     reset(V, d);
      91           0 :     for (verti v = 0; v < V; ++v)
      92             :     {
      93           0 :         vertex_[v].player   = (rand()%2 == 0) ? PLAYER_EVEN : PLAYER_ODD;
      94           0 :         vertex_[v].priority = rand()%d;
      95             :     }
      96           0 :     recalculate_cardinalities(V);
      97           0 : }
      98             : 
      99           0 : void ParityGame::make_dual()
     100             : {
     101             :     // For each vertex, invert player and increase priority by one
     102           0 :     for (verti v = 0; v < graph_.V(); ++v)
     103             :     {
     104           0 :         vertex_[v].player   = opponent(vertex_[v].player);
     105           0 :         vertex_[v].priority = vertex_[v].priority + 1;
     106             :     }
     107             : 
     108             :     // Update priority counts (move each on space to the right)
     109           0 :     verti *new_cardinality = new verti[d_ + 1];
     110           0 :     new_cardinality[0] = 0;
     111           0 :     std::copy(cardinality_, cardinality_ + d_, new_cardinality + 1);
     112           0 :     delete[] cardinality_;
     113           0 :     cardinality_ = new_cardinality;
     114           0 :     d_ = d_ + 1;
     115             : 
     116             :     // Try to compress priorities
     117           0 :     compress_priorities();
     118           0 : }
     119             : 
     120           0 : void ParityGame::shuffle(const std::vector<verti> &perm)
     121             : {
     122             :     // N.B. maximum priority and priorities cardinalities remain unchanged.
     123             : 
     124             :     /* NOTE: shuffling could probably be done more efficiently (in-place?)
     125             :              if performance becomes an issue. */
     126           0 :     graph_.shuffle_vertices(perm);
     127             : 
     128             :     // Create new vertex info
     129           0 :     ParityGameVertex *new_vertex = new ParityGameVertex[graph_.V()];
     130           0 :     for (verti v = 0; v < graph_.V(); ++v) new_vertex[perm[v]] = vertex_[v];
     131           0 :     delete[] vertex_;
     132           0 :     vertex_ = new_vertex;
     133           0 : }
     134             : 
     135           0 : void ParityGame::compress_priorities( const verti cardinality[],
     136             :                                                     bool preserve_parity )
     137             : {
     138           0 :     if (cardinality == 0) cardinality = cardinality_;
     139             : 
     140             :     // Quickly check if we have anything to compress first:
     141           0 :     if ( empty() || std::find( cardinality + preserve_parity,
     142           0 :                                cardinality + d_, 0 ) == cardinality + d_ )
     143             :     {
     144           0 :         return;
     145             :     }
     146             : 
     147             :     // Find out how to map old priorities to new priorities
     148           0 :     std::vector<int> prio_map(d_, -1);
     149           0 :     int first_prio = 0, last_prio = 0;
     150           0 :     if (!preserve_parity)
     151             :     {
     152             :         // Find lowest priority in use:
     153           0 :         while (cardinality[first_prio] == 0) ++first_prio;
     154           0 :         assert(first_prio < d_);  // fails only if cardinality count is invalid!
     155             :     }
     156           0 :     int swap_players = first_prio%2;
     157           0 :     prio_map[first_prio] = last_prio;
     158           0 :     for (int p = first_prio + 1; p < d_; ++p)
     159             :     {
     160           0 :         if (cardinality[p] == 0) continue;  // remove priority p
     161           0 :         if ((last_prio ^ p)%2 != swap_players) ++last_prio;
     162           0 :         prio_map[p] = last_prio;
     163             :     }
     164             : 
     165             :     // Update priority limit and cardinality counts
     166           0 :     int new_d = last_prio + 1;
     167           0 :     verti *new_cardinality = new verti[new_d];
     168           0 :     std::fill(new_cardinality, new_cardinality + new_d, 0);
     169           0 :     for (int p = 0; p < d_; ++p)
     170             :     {
     171           0 :         if (prio_map[p] >= 0)
     172             :         {
     173           0 :             new_cardinality[prio_map[p]] += cardinality_[p];
     174             :         }
     175             :     }
     176           0 :     delete[] cardinality_;
     177           0 :     cardinality_ = new_cardinality;
     178           0 :     d_ = new_d;
     179             : 
     180             :     // Remap priorities and players of all vertices
     181           0 :     for (verti v = 0; v < graph_.V(); ++v)
     182             :     {
     183           0 :         assert(prio_map[vertex_[v].priority] >= 0);
     184           0 :         vertex_[v].priority = prio_map[vertex_[v].priority];
     185           0 :         if (0 != swap_players) vertex_[v].player = opponent(vertex_[v].player);
     186             :     }
     187             : 
     188           0 :     return;
     189           0 : }
     190             : 
     191           0 : int ParityGame::propagate_priority( verti v, StaticGraph::const_iterator it,
     192             :                                              StaticGraph::const_iterator end )
     193             : {
     194           0 :     int p = priority(v), q = 0;
     195           0 :     for ( ; it != end; ++it)
     196             :     {
     197           0 :         verti w = *it;
     198           0 :         int r = priority(w);
     199           0 :         if (r >= p) return 0;
     200           0 :         if (r > q) q = r;
     201             :     }
     202           0 :     vertex_[v].priority = q;
     203           0 :     --cardinality_[p];
     204           0 :     ++cardinality_[q];
     205           0 :     return p - q;
     206             : }
     207             : 
     208             : /* N.B. this method is designed to be reasonably fast and use little memory
     209             :     in the common case that few priorities can be propagated, which is why the
     210             :     algorithm starts with a first pass looking for vertices which can be
     211             :     updated, rather than putting them all in the initial queue, which would be
     212             :     simpler but require more memory up-front. */
     213           0 : long long ParityGame::propagate_priorities()
     214             : {
     215           0 :     long long res = 0;
     216           0 :     std::deque<verti> todo;
     217             : 
     218             :     // Make an initial pass to look for updatable vertices:
     219           0 :     for (verti v = 0; v < graph_.V(); ++v)
     220             :     {
     221           0 :         if (priority(v) > 0)
     222             :         {
     223           0 :             int change = propagate_priority(v, graph_.succ_begin(v),
     224             :                                                graph_.succ_end(v) )
     225           0 :                        + propagate_priority(v, graph_.pred_begin(v),
     226           0 :                                                graph_.pred_end(v) );
     227           0 :             if (change > 0) {
     228           0 :                 res += change;
     229           0 :                 todo.push_back(v);
     230             :             }
     231             :         }
     232             :     }
     233             : 
     234             :     // Check neighbours of updated vertices again:
     235           0 :     while (!todo.empty())
     236             :     {
     237           0 :         verti w = todo.front();
     238           0 :         priority_t p = priority(w);
     239           0 :         todo.pop_front();
     240             : 
     241             :         // Perform backwards propagation on predecessors:
     242           0 :         for ( StaticGraph::const_iterator it = graph_.pred_begin(w);
     243           0 :               it != graph_.pred_end(w); ++it )
     244             :         {
     245           0 :             verti v = *it;
     246           0 :             if (priority(v) > p)
     247             :             {
     248           0 :                 int change = propagate_priority(v, graph_.succ_begin(v),
     249             :                                                    graph_.succ_end(v) );
     250           0 :                 if (change > 0) {
     251           0 :                     res += change;
     252           0 :                     todo.push_back(v);
     253             :                 }
     254             :             }
     255             :         }
     256             : 
     257             :         // Perform forwards propagation on successors:
     258           0 :         for ( StaticGraph::const_iterator it = graph_.succ_begin(w);
     259           0 :               it != graph_.succ_end(w); ++it )
     260             :         {
     261           0 :             verti v = *it;
     262           0 :             if (priority(v) > p)
     263             :             {
     264           0 :                 int change = propagate_priority(v, graph_.pred_begin(v),
     265             :                                                    graph_.pred_end(v) );
     266           0 :                 if (change > 0) {
     267           0 :                     res += change;
     268           0 :                     todo.push_back(v);
     269             :                 }
     270             :             }
     271             :         }
     272             :     }
     273             : 
     274           0 :     return res;
     275           0 : }
     276             : 
     277           0 : bool ParityGame::proper() const
     278             : {
     279           0 :     for (verti v = 0; v < graph_.V(); ++v)
     280             :     {
     281           0 :         if (graph_.succ_begin(v) == graph_.succ_end(v)) return false;
     282             :     }
     283           0 :     return true;
     284             : }
     285             : 
     286           0 : void ParityGame::swap(ParityGame &pg)
     287             : {
     288             :     using std::swap;
     289           0 :     swap(d_, pg.d_);
     290           0 :     swap(graph_, pg.graph_);
     291           0 :     swap(vertex_, pg.vertex_);
     292           0 :     swap(cardinality_, pg.cardinality_);
     293           0 : }
     294             : 
     295             : #ifdef WITH_THREADS
     296             : void ParityGame::make_subgame_threads( const ParityGame &game,
     297             :                                        const verti *verts,
     298             :                                        const verti nvert,
     299             :                                        bool proper,
     300             :                                        StaticGraph::EdgeDirection edge_dir )
     301             : {
     302             :     assert(this != &game);
     303             :     reset(nvert, game.d());
     304             : 
     305             :     //#pragma omp parallel for
     306             :     for (verti v = 0; v < nvert; ++v)
     307             :     {
     308             :         vertex_[v] = game.vertex_[verts[v]];
     309             :     }
     310             : 
     311             :     graph_.make_subgraph_threads(game.graph_, verts, nvert,  proper, edge_dir);
     312             : 
     313             :     // FIXME: parallellize this?
     314             :     recalculate_cardinalities(nvert);
     315             : }
     316             : #endif

Generated by: LCOV version 1.14