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_LIFTING_STRATEGY_H
      11             : #define MCRL2_PG_LIFTING_STRATEGY_H
      12             : 
      13             : #include "mcrl2/pg/ParityGame.h"
      14             : #include "mcrl2/pg/RefCounted.h"
      15             : 
      16             : #include <string>
      17             : 
      18             : class SmallProgressMeasures;
      19             : 
      20             : /*! \defgroup LiftingStrategies
      21             : 
      22             :     Lifting strategies for the Small Progress Measures solving algorithm.
      23             : */
      24             : 
      25             : 
      26             : /*! \ingroup LiftingStrategies
      27             : 
      28             :     Version 1 API for lifting strategies.
      29             : 
      30             :     Instances of this class encapsulate vertex lifting strategies to be used
      31             :     with the small progress measures parity game solver.
      32             : 
      33             :     These are expected to initialize and maintain the set of dirty vertices
      34             :     themselves, and inform the SPM implementation when the set becomes empty by
      35             :     returning NO_VERTEX from next().
      36             : */
      37             : class LiftingStrategy
      38             : {
      39             : public:
      40           0 :     virtual ~LiftingStrategy() { }
      41             : 
      42             :     /*! Record that the given vertex was lifted: */
      43             :     virtual void lifted(verti vertex) = 0;
      44             : 
      45             :     /*! Select the next vertex to lift. This method is called repeatedly by the
      46             :         SPM solver until it returns NO_VERTEX to indicate the solution is
      47             :         complete.
      48             : 
      49             :         \see lifted(verti vertex)
      50             :     */
      51             :     virtual verti next() = 0;
      52             : };
      53             : 
      54             : 
      55             : /*! \ingroup LiftingStrategies
      56             : 
      57             :     Version 2 API for lifting strategies.
      58             : 
      59             :     Instances of this class encapsulate vertex lifting strategies to be used
      60             :     with the small progress measures parity game solver.
      61             : 
      62             :     The SPM implementation manages the set of dirty vertices; it will call
      63             :     push() to add a vertex to the set, pop() to remove one (which one is at the
      64             :     discretion of the lifting strategy implementation) and bump() when an
      65             :     already-queued vertex's progress measure has been increased.
      66             : */
      67             : class LiftingStrategy2
      68             : {
      69             : public:
      70           0 :     virtual ~LiftingStrategy2() { }
      71             : 
      72             :     // TODO: document each separately like LiftingStrategy above
      73             :     virtual void push(verti vertex) = 0;
      74             :     virtual void bump(verti vertex) = 0;
      75             :     virtual verti pop() = 0;
      76             : };
      77             : 
      78             : 
      79             : /*! \ingroup LiftingStrategies
      80             :     Abstract base class for lifting strategy factories. */
      81             : class LiftingStrategyFactory : public RefCounted
      82             : {
      83             : public:
      84             :     virtual ~LiftingStrategyFactory();
      85             : 
      86             :     /*! Returns pre-formatted plain-text documentation of the description
      87             :         strings accepted by create(), intended to be shown to the user.
      88             :         \see create(const std::string &description) */
      89             :     static const char *usage();
      90             : 
      91             :     /*! Creates a lifting strategy factory from a string description.
      92             :     \returns A factory object or NULL if the description could not be parsed.
      93             :     \see usage() for a description of available format strings. */
      94             :     static LiftingStrategyFactory *create(const std::string &description);
      95             : 
      96           0 :     virtual bool supports_version(int version) { return version == 1; }
      97             : 
      98             :     /*! Create a lifting strategy for the given game, to be used by the given
      99             :         Small Progress Measures solver. */
     100             :     virtual LiftingStrategy *create( const ParityGame &game,
     101             :                                      const SmallProgressMeasures &spm ) = 0;
     102             : 
     103           0 :     virtual LiftingStrategy2 *create2( const ParityGame & /*game*/,
     104           0 :                                        const SmallProgressMeasures &/*spm*/ ) { return 0; }
     105             : };
     106             : 
     107             : 
     108             : #endif /* ndef MCRL2_PG_LIFTING_STRATEGY_H */