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_MAX_MEASURE_LIFTING_STRATEGY_H
      11             : #define MCRL2_PG_MAX_MEASURE_LIFTING_STRATEGY_H
      12             : 
      13             : #include "mcrl2/pg/SmallProgressMeasures.h"
      14             : 
      15             : /*! \ingroup LiftingStrategies
      16             : 
      17             :     A lifting strategy that propagate maximum measures first.
      18             : 
      19             :     Conceptually this is a specialization of the predecessor lifting strategy.
      20             :     However, of all feasible vertices to select for the next lifting attempt,
      21             :     one is chosen specifically that has the largest maximum progress measure
      22             :     vector.
      23             : 
      24             :     The implementation uses a custom heap structure to act as a priority queue.
      25             :     Special care must be taken to maintain the heap property, because lifting
      26             :     vertices changes the associated progress measure!
      27             : */
      28             : class MaxMeasureLiftingStrategy2 : public LiftingStrategy2
      29             : {
      30             : public:
      31             :     enum Order { QUEUE = 0, STACK = 1, HEAP = 2 }; 
      32             :     enum Metric { MAX_VALUE = 0, MAX_STEP = 1, MIN_VALUE = 2 };
      33             : 
      34             :     MaxMeasureLiftingStrategy2( const ParityGame &game,
      35             :                                 const SmallProgressMeasures &spm,
      36             :                                 Order order, Metric metric );
      37             :     ~MaxMeasureLiftingStrategy2();
      38             : 
      39             :     void push(verti v);
      40             :     void bump(verti v);
      41             :     verti pop();
      42             : 
      43             : protected:
      44             : 
      45             :     /*! Moves the element at index i up the heap until the heap property
      46             :         is restored. */
      47             :     void move_up(verti i);
      48             : 
      49             :     /*! Moves the element at index i down the heap until the heap property
      50             :         is restored. */
      51             :     void move_down(verti i);
      52             : 
      53             :     /*! Swaps the elements at indices i and j in the heap. */
      54             :     void swap(verti i, verti j);
      55             : 
      56             :     /*! Removes the vertex from the queue, if it is present. */
      57             :     //void remove(verti v);
      58             : 
      59             :     /*! Compares the vertices referred through indices i and j in the heap. */
      60             :     int cmp(verti i, verti j);
      61             : 
      62             :     /*! Checks if the queue satisfies the heap property (used for debugging) */
      63             :     bool check();
      64             : 
      65             : private:
      66             :     MaxMeasureLiftingStrategy2(const MaxMeasureLiftingStrategy2 &);
      67             :     MaxMeasureLiftingStrategy2 &operator=(const MaxMeasureLiftingStrategy2 &);
      68             : 
      69             : private:
      70             :     const SmallProgressMeasures &spm_;  //!< SPM instance being solved
      71             :     const Order order_;                 //!< vertex extraction order
      72             :     const Metric metric_;               //!< comparison metric
      73             : 
      74             :     uint64_t next_id_;        //!< number of insertions
      75             :     uint64_t * insert_id_;    //!< for each vertex: last insertion time
      76             : 
      77             :     verti * const pq_pos_;      //!< for each vertex: position in the p.q. or -1
      78             :     verti * const pq_;          //!< priority queue of lifted vertices
      79             :     verti pq_size_;             //!< priority queue size
      80             : 
      81             :     std::vector<verti> bumped_;
      82             : };
      83             : 
      84             : /*! \ingroup LiftingStrategies
      85             :     A factory class for MaxMeasureLiftingStrategy instances. */
      86             : class MaxMeasureLiftingStrategyFactory : public LiftingStrategyFactory
      87             : {
      88             : public:
      89           0 :     MaxMeasureLiftingStrategyFactory(
      90             :             MaxMeasureLiftingStrategy2::Order order =
      91             :                 MaxMeasureLiftingStrategy2::HEAP,
      92             :             MaxMeasureLiftingStrategy2::Metric metric =
      93             :                 MaxMeasureLiftingStrategy2::MAX_VALUE )
      94           0 :         : order_(order), metric_(metric) { };
      95             : 
      96             :     bool supports_version(int version);
      97             : 
      98             :     LiftingStrategy *create(const ParityGame&, const SmallProgressMeasures &);
      99             : 
     100             :     LiftingStrategy2 *create2( const ParityGame &game,
     101             :                                const SmallProgressMeasures &spm );
     102             : 
     103             : private:
     104             :     const MaxMeasureLiftingStrategy2::Order  order_;
     105             :     const MaxMeasureLiftingStrategy2::Metric metric_;
     106             : };
     107             : 
     108             : #endif /* ndef PREDECESSOR_LIFTING_STRATEGY_H_INCLUDED */