SmallProgressMeasures.h

Go to the documentation of this file.

// Copyright (c) 2009-2013 University of Twente
// Copyright (c) 2009-2013 Michael Weber <michaelw@cs.utwente.nl>
// Copyright (c) 2009-2013 Maks Verver <maksverver@geocities.com>
// Copyright (c) 2009-2013 Eindhoven University of Technology
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
 
#ifndef MCRL2_PG_SMALL_PROGRESS_MEASURES_H
#define MCRL2_PG_SMALL_PROGRESS_MEASURES_H
 
#include "mcrl2/pg/ParityGameSolver.h"
#include "mcrl2/pg/LiftingStrategy.h"
#include "mcrl2/utilities/logger.h"
 
class LiftingStatistics
{
public:
    LiftingStatistics(const ParityGame &game, long long max_lifts = -1);
 
#if 0
    void merge(const LiftingStatistics &other, const verti *mapping = NULL);
#endif
 
    long long lifts_attempted() const { return lifts_attempted_; }
    long long lifts_succeeded() const { return lifts_succeeded_; }
    long long lifts_attempted(verti v) const { return vertex_stats_[v].first; }
    long long lifts_succeeded(verti v) const { return vertex_stats_[v].second; }
 
    void add_lifts_attempted(long long count) { lifts_attempted_ += count; }
    void add_lifts_succeeded(long long count) { lifts_succeeded_ += count; }
    void add_lifts_attempted(verti v, long long count)
    {
        vertex_stats_[v].first += count;
    }
    void add_lifts_succeeded(verti v, long long count)
    {
        vertex_stats_[v].second += count;
    }
 
private:
    void record_lift(verti v, bool success);
    friend class SmallProgressMeasures;
 
private:
    long long lifts_attempted_, lifts_succeeded_;
    std::vector<std::pair<long long, long long> > vertex_stats_;
    long long max_lifts_;
};
 
class SmallProgressMeasures
{
public:
    static const int work_size = 10000;
 
    SmallProgressMeasures(
        const ParityGame &game, ParityGame::Player player,
        LiftingStatistics *stats = 0,
        const verti *vmap = 0, verti vmap_size = 0 );
 
    virtual ~SmallProgressMeasures();
 
    long long solve_some( LiftingStrategy &ls,
                          long long attempts = work_size );
    long long solve_some( LiftingStrategy2 &ls,
                          long long attempts = work_size );
 
    std::pair<verti, bool> solve_one(LiftingStrategy &ls);
    verti solve_one(LiftingStrategy2 &ls);
 
    verti get_strategy(verti v) const;
 
    void get_strategy(ParityGame::Strategy &strat) const;
 
    template<class OutputIterator>
    void get_winning_set(ParityGame::Player player, OutputIterator result);
 
    inline bool lift_to_top(verti v);
 
    bool lift_to(verti v, const verti vec2[], bool carry = 0);
 
    bool less_than(verti v, const verti vec2[], bool carry = 0);
 
    void debug_print() const;
    void debug_print_vertex(int v) const;
 
    bool verify_solution();
 
    const ParityGame &game() const { return game_; }
 
    ParityGame::Player player() const { return (ParityGame::Player)p_; }
 
    int len() const { return len_; }
 
    const verti *M() const { return M_; }
 
    void set_M(const verti *new_M) { std::copy(new_M, new_M + len_, M_); }
 
    void decr_M(int i) { assert(M_[i] > 1); --M_[i]; }
 
    int len(verti v) const { return (game_.priority(v) + 1 + p_)/2; }
 
    bool is_top(const verti vec[]) const { return vec[0] == NO_VERTEX; }
 
    bool is_top(verti v) const { return is_top(vec(v)); }
 
    // The following functions are implemented in derived classes that
    // implement the actual storage of progress measure vectors:
 
    // virtual verti *vec(verti v) = 0;
    virtual const verti *vec(verti v) const = 0;
 
    virtual void set_vec(verti v, const verti src[], bool carry) = 0;
 
    virtual void set_vec_to_top(verti v) = 0;
 
    void initialize_lifting_strategy(LiftingStrategy2 &ls);
 
protected:
    void initialize_loops();
 
    inline void set_top(verti v);
 
private:
    SmallProgressMeasures(const SmallProgressMeasures &);
    SmallProgressMeasures &operator=(const SmallProgressMeasures &);
 
private:
    inline int vector_cmp(const verti vec1[], const verti vec2[], int N) const;
 
    inline int vector_cmp(verti v, verti w, int N) const;
 
    inline bool take_max(verti v) const { return game_.player(v) != p_; }
 
    inline bool compare_strict(verti v) const { return game_.priority(v)%2 != p_; }
 
    inline verti get_ext_succ(verti v, bool take_max) const;
 
    inline verti get_ext_succ(verti v) const;
 
    inline verti get_min_succ(verti v) const { return get_ext_succ(v, false); }
 
    inline verti get_max_succ(verti v) const { return get_ext_succ(v, true); }
 
    inline verti get_successor(verti v) const { return strategy_[v]; }
 
    inline bool is_dirty(verti v) const { return dirty_[v]; }
 
    // Allow selected lifting strategies to access the SPM internals:
    friend class PredecessorLiftingStrategy;
    friend class MaxMeasureLiftingStrategy2;
    friend class OldMaxMeasureLiftingStrategy;
 
protected:
    const ParityGame       &game_;     
    const std::size_t           p_;         
    LiftingStatistics      *stats_;    
    const verti            *vmap_;     
    verti                  vmap_size_; 
    std::size_t                 len_;       
    verti                  *M_;        
    ParityGame::Strategy   strategy_;  
    bool                   *dirty_;    
};
 
class DenseSPM : public SmallProgressMeasures
{
public:
    DenseSPM(
        const ParityGame &game, ParityGame::Player player,
        LiftingStatistics *stats = 0,
        const verti *vertex_map = 0, verti vertex_map_size = 0 );
    ~DenseSPM();
 
    // verti *vec(verti v) { return &spm_[(std::size_t)len_*v]; }
    const verti *vec(verti v) const { return &spm_[(std::size_t)len_*v]; }
    void set_vec(verti v, const verti src[], bool carry) ;
    void set_vec_to_top(verti v);
 
protected:
    verti *spm_;  
};
 
 
class SmallProgressMeasuresSolver
    : public ParityGameSolver
{
protected:
    class SetToTopIterator
    {
    public:
        SetToTopIterator(SmallProgressMeasures &spm) : spm(spm) { }
        SetToTopIterator& operator++() { return *this; }
        SetToTopIterator& operator++(int) { return *this; }
        SetToTopIterator& operator*() { return *this; }
        SetToTopIterator& operator=(verti v)
        {
            spm.lift_to_top(v);
            return *this;
        }
 
    private:
        SmallProgressMeasures &spm;
    };
 
public:
    SmallProgressMeasuresSolver( const ParityGame &game,
                                 std::shared_ptr<LiftingStrategyFactory> lsf,
                                 bool alternate = false,
                                 LiftingStatistics *stats = 0,
                                 const verti *vmap = 0,
                                 verti vmap_size = 0 );
 
    ParityGame::Strategy solve();
 
    virtual ParityGame::Strategy solve_normal();
 
    virtual ParityGame::Strategy solve_alternate();
 
    static void preprocess_game(ParityGame &game);
 
private:
    SmallProgressMeasuresSolver(const SmallProgressMeasuresSolver&);
    SmallProgressMeasuresSolver &operator=(const SmallProgressMeasuresSolver&);
 
protected:
    std::shared_ptr<LiftingStrategyFactory> lsf_;   
    bool alternate_;                
    LiftingStatistics *stats_;      
    const verti *vmap_;             
    const verti vmap_size_;         
};
 
class SmallProgressMeasuresSolver2 : public SmallProgressMeasuresSolver
{
public:
    SmallProgressMeasuresSolver2( const ParityGame &game,
                                  std::shared_ptr<LiftingStrategyFactory> lsf,
                                  bool alternate = false,
                                  LiftingStatistics *stats = 0,
                                  const verti *vmap = 0,
                                  verti vmap_size = 0 );
 
    ParityGame::Strategy solve_normal();
    ParityGame::Strategy solve_alternate();
 
private:
    SmallProgressMeasuresSolver2(const SmallProgressMeasuresSolver2&);
    SmallProgressMeasuresSolver2 &operator=(const SmallProgressMeasuresSolver2&);
};
 
class SmallProgressMeasuresSolverFactory : public ParityGameSolverFactory
{
public:
    SmallProgressMeasuresSolverFactory(std::shared_ptr<LiftingStrategyFactory> lsf,
        int version = 1, bool alt = false, LiftingStatistics *stats = 0 );
 
    ParityGameSolver *create( const ParityGame &game,
                              const verti *vmap,
                              verti vmap_size );
 
private:
    std::shared_ptr<LiftingStrategyFactory>  lsf_;
    int                     version_;
    bool                    alt_;
    LiftingStatistics       *stats_;
};
 
#include "SmallProgressMeasures_impl.h"
 
#endif /* ndef MCRL2_PG_SMALL_PROGRESS_MEASURES_H */