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/OldMaxMeasureLiftingStrategy.h"
      11             : 
      12             : /* NOTE: this code abuses the fact that verti is unsigned, making the top vector
      13             :          strictly greater than vectors of other measures. */
      14             : 
      15           0 : OldMaxMeasureLiftingStrategy::OldMaxMeasureLiftingStrategy(
      16           0 :     const ParityGame &game, const SmallProgressMeasures &spm )
      17           0 :         : LiftingStrategy(), spm_(spm),
      18           0 :           queue_pos_(game.graph().V(), queue_.end())
      19             : {
      20             :     // Initialize queue
      21           0 :     for (verti v = 0; v < game.graph().V(); ++v)
      22             :     {
      23           0 :         queue_pos_[v] =
      24           0 :             queue_.insert(std::make_pair(std::vector<verti>(), v)).first;
      25             :     }
      26           0 : }
      27             : 
      28           0 : OldMaxMeasureLiftingStrategy::~OldMaxMeasureLiftingStrategy()
      29             : {
      30           0 : }
      31             : 
      32           0 : void OldMaxMeasureLiftingStrategy::lifted(verti v)
      33             : {
      34           0 :     std::vector<verti> m = vec(v);
      35             : 
      36             :     // Add predecessors to queue
      37           0 :     const StaticGraph &graph = spm_.game().graph();
      38           0 :     for ( StaticGraph::const_iterator it = graph.pred_begin(v);
      39           0 :           it != graph.pred_end(v); ++it )
      40             :     {
      41           0 :         verti u = *it;
      42           0 :         queue_t::iterator it1 = queue_pos_[u];
      43             : 
      44             :         /* Skip this predecessor if it is already queued with an
      45             :             equal or greater weight. */
      46           0 :         if (it1 != queue_.end() && it1->first >= m) continue;
      47             : 
      48             :         // If we have an old entry in the queue, remove it first.
      49           0 :         if (it1 != queue_.end()) queue_.erase(queue_pos_[u]);
      50             : 
      51             :         // Add new entry to the queue
      52           0 :         queue_pos_[u] = queue_.insert(std::make_pair(m, u)).first;
      53             :     }
      54           0 : }
      55             : 
      56           0 : verti OldMaxMeasureLiftingStrategy::next()
      57             : {
      58             :     // Take a predecessor from the queue
      59           0 :     verti v = NO_VERTEX;
      60           0 :     queue_t::iterator it = queue_.end();
      61           0 :     if (it != queue_.begin())
      62             :     {
      63           0 :         --it;
      64           0 :         v = it->second;
      65           0 :         queue_.erase(it);
      66           0 :         queue_pos_[v] = queue_.end();
      67             :     }
      68           0 :     return v;
      69             : }
      70             : 
      71           0 : LiftingStrategy *OldMaxMeasureLiftingStrategyFactory::create(
      72             :     const ParityGame &game, const SmallProgressMeasures &spm )
      73             : {
      74           0 :     return new OldMaxMeasureLiftingStrategy(game, spm);
      75             : }