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_OLD_MAX_MEASURE_LIFTING_STRATEGY_H
      11             : #define MCRL2_PG_OLD_MAX_MEASURE_LIFTING_STRATEGY_H
      12             : 
      13             : #include "mcrl2/pg/SmallProgressMeasures.h"
      14             : 
      15             : /*! \ingroup LiftingStrategies
      16             : 
      17             :     Old implementation of MaxMeasureLiftingStrategy.
      18             : 
      19             :     This is strategy is rather inefficient (in time and space) because it stores
      20             :     both vertex indices and a copy of the highest successor's progress measure
      21             :     in a std::set.
      22             : 
      23             :     This class is basically obsolete, but retained in order to be able to test
      24             :     for regressions.
      25             : */
      26             : class OldMaxMeasureLiftingStrategy : public LiftingStrategy
      27             : {
      28             : public:
      29             :     OldMaxMeasureLiftingStrategy( const ParityGame &game,
      30             :                                   const SmallProgressMeasures &spm );
      31             :     ~OldMaxMeasureLiftingStrategy();
      32             : 
      33             :     void lifted(verti v);
      34             :     verti next();
      35             : 
      36             : protected:
      37           0 :     std::vector<verti> vec(verti v) {
      38           0 :         return std::vector<verti>(spm_.vec(v), spm_.vec(v) + spm_.len(v));
      39             :     }
      40             : 
      41             : private:
      42             :     OldMaxMeasureLiftingStrategy(const OldMaxMeasureLiftingStrategy &);
      43             :     OldMaxMeasureLiftingStrategy operator=(const OldMaxMeasureLiftingStrategy &);
      44             : 
      45             : private:
      46             :     const SmallProgressMeasures &spm_;
      47             :     typedef std::set<std::pair<std::vector<verti>, verti> > queue_t;
      48             :     queue_t queue_;
      49             :     std::vector<queue_t::iterator> queue_pos_;
      50             : };
      51             : 
      52             : /*! \ingroup LiftingStrategies
      53             :     A factory class for OldMaxMeasureLiftingStrategy instances. */
      54             : class OldMaxMeasureLiftingStrategyFactory : public LiftingStrategyFactory
      55             : {
      56             : public:
      57             :     LiftingStrategy *create( const ParityGame &game,
      58             :                              const SmallProgressMeasures &spm );
      59             : };
      60             : 
      61             : #endif /* ndef OLD_PREDECESSOR_LIFTING_STRATEGY_H_INCLUDED */