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/PredecessorLiftingStrategy.h"
      11             : 
      12           0 : PredecessorLiftingStrategy::PredecessorLiftingStrategy(
      13             :     const ParityGame &game, const SmallProgressMeasures &spm,
      14           0 :     bool stack, int version )
      15           0 :     : LiftingStrategy(), LiftingStrategy2(), spm_(spm), stack_(stack)
      16             : {
      17           0 :     assert(game.graph().edge_dir() & StaticGraph::EDGE_PREDECESSOR);
      18             : 
      19             :     // Initialize data
      20           0 :     const verti V = game.graph().V();
      21           0 :     queue_ = new verti[V];
      22           0 :     queue_capacity_ = V;
      23           0 :     queue_begin_ = queue_end_ = queue_size_ = 0;
      24             : 
      25           0 :     if (version == 1)
      26             :     {
      27             :         // v1 API requires explicit tracking of queued vertices.
      28           0 :         queued_ = new bool[V]();
      29           0 :         for (verti v = 0; v < V; ++v)
      30             :         {
      31           0 :             if (!spm_.is_top(v))
      32             :             {
      33           0 :                 queued_[v] = true;
      34           0 :                 push(v);
      35             :             }
      36             :         }
      37             :     }
      38             :     else  // version != 1
      39             :     {
      40           0 :         assert(version == 2);
      41           0 :         queued_ = NULL;
      42             :     }
      43           0 : }
      44             : 
      45           0 : PredecessorLiftingStrategy::~PredecessorLiftingStrategy()
      46             : {
      47           0 :     delete[] queue_;
      48           0 :     delete[] queued_;
      49           0 : }
      50             : 
      51           0 : void PredecessorLiftingStrategy::push(verti v)
      52             : {
      53           0 :     mCRL2log(mcrl2::log::debug) << "push(" << v << ")" << std::endl;
      54           0 :     queue_[queue_end_++] = v;
      55           0 :     if (queue_end_ == queue_capacity_) queue_end_ = 0;
      56           0 :     ++queue_size_;
      57           0 :     assert(queue_size_ <= queue_capacity_);
      58           0 : }
      59             : 
      60           0 : verti PredecessorLiftingStrategy::pop()
      61             : {
      62           0 :     if (queue_size_ == 0) return NO_VERTEX;
      63             : 
      64             :     // Remove an element from the queue
      65             :     verti res;
      66           0 :     if (stack_)
      67             :     {
      68             :         // Remove from the back of the queue
      69           0 :         if (queue_end_ == 0) queue_end_ = queue_capacity_;
      70           0 :         res = queue_[--queue_end_];
      71             :     }
      72             :     else
      73             :     {
      74             :         // Remove from the front of the queue
      75           0 :         res = queue_[queue_begin_++];
      76           0 :         if (queue_begin_ == queue_capacity_) queue_begin_ = 0;
      77             :     }
      78           0 :     --queue_size_;
      79           0 :     mCRL2log(mcrl2::log::debug) << "pop() -> " << res << std::endl;
      80           0 :     return res;
      81             : }
      82             : 
      83           0 : void PredecessorLiftingStrategy::lifted(verti v)
      84             : {
      85           0 :     const StaticGraph &graph = spm_.game().graph();
      86           0 :     for ( StaticGraph::const_iterator it = graph.pred_begin(v);
      87           0 :           it != graph.pred_end(v); ++it )
      88             :     {
      89           0 :         verti u = *it;
      90           0 :         if (!queued_[u] && !spm_.is_top(u))
      91             :         {
      92           0 :             queued_[u] = true;
      93           0 :             push(u);
      94             :         }
      95             :     }
      96           0 : }
      97             : 
      98           0 : verti PredecessorLiftingStrategy::next()
      99             : {
     100           0 :     verti res = pop();
     101           0 :     if (res != NO_VERTEX) queued_[res] = false;
     102           0 :     return res;
     103             : }
     104             : 
     105           0 : bool PredecessorLiftingStrategyFactory::supports_version(int version)
     106             : {
     107           0 :     return version == 1 || version == 2;
     108             : }
     109             : 
     110           0 : LiftingStrategy *PredecessorLiftingStrategyFactory::create(
     111             :     const ParityGame &game, const SmallProgressMeasures &spm )
     112             : {
     113           0 :     return new PredecessorLiftingStrategy(game, spm, stack_, 1);
     114             : }
     115             : 
     116           0 : LiftingStrategy2 *PredecessorLiftingStrategyFactory::create2(
     117             :     const ParityGame &game, const SmallProgressMeasures &spm )
     118             : {
     119           0 :     return new PredecessorLiftingStrategy(game, spm, stack_, 2);
     120             : }