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/LinearLiftingStrategy.h"
      11             : 
      12           0 : LinearLiftingStrategy::LinearLiftingStrategy(
      13           0 :     const ParityGame &game, bool alternate )
      14           0 :     : LiftingStrategy(), alternate_(alternate),
      15           0 :       last_vertex_(game.graph().V() - 1),
      16           0 :       dir_(0), vertex_(NO_VERTEX), failed_lifts_(0) 
      17             : {
      18           0 : }
      19             : 
      20           0 : void LinearLiftingStrategy::lifted(verti v)
      21             : {
      22             :     (void)v;  // unused
      23           0 :     failed_lifts_ = 0;
      24           0 : }
      25             : 
      26           0 : verti LinearLiftingStrategy::next()
      27             : {
      28           0 :     if (failed_lifts_ > last_vertex_) return NO_VERTEX;
      29             : 
      30           0 :     if (vertex_ == NO_VERTEX)
      31             :     {
      32           0 :         dir_          = 0;
      33           0 :         vertex_       = 0;
      34           0 :         failed_lifts_ = 0;
      35             :     }
      36             :     else
      37             :     {
      38           0 :         ++failed_lifts_;  // count last vertex being lifted
      39             : 
      40           0 :         if (dir_ == 0)  // forward
      41             :         {
      42           0 :             if (vertex_ < last_vertex_)
      43             :             {
      44           0 :                 ++vertex_;
      45             :             }
      46             :             else
      47           0 :             if (!alternate_)
      48             :             {
      49           0 :                 vertex_ = 0;
      50             :             }
      51             :             else
      52             :             {
      53           0 :                 dir_ = 1;
      54           0 :                 vertex_ = vertex_ - failed_lifts_ - 1;
      55             :             }
      56             :         }
      57             :         else  // backward
      58             :         {
      59           0 :             if (vertex_ > 0)
      60             :             {
      61           0 :                 --vertex_;
      62             :             }
      63             :             else
      64           0 :             if (!alternate_)
      65             :             {
      66           0 :                 vertex_ = last_vertex_;
      67             :             }
      68             :             else
      69             :             {
      70           0 :                 dir_ = 0;
      71           0 :                 vertex_ = failed_lifts_;
      72             :             }
      73             :         }
      74             :     }
      75           0 :     return vertex_;
      76             : }
      77             : 
      78           0 : LiftingStrategy *LinearLiftingStrategyFactory::create(
      79             :     const ParityGame &game, const SmallProgressMeasures &spm )
      80             : {
      81             :     (void)spm;  // unused
      82           0 :     return new LinearLiftingStrategy(game, alternate_);
      83             : }