GameSolver.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
#include <memory>
#include <vector>
 
#include "storm/solver/AbstractEquationSolver.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/storage/Scheduler.h"
#include "storm/storage/sparse/StateType.h"
#include "storm/utility/macros.h"
 
#include "storm/exceptions/InvalidSettingsException.h"
 
namespace storm {
 
class Environment;
 
namespace storage {
template<typename T>
class SparseMatrix;
}
 
namespace solver {
 
template<class ValueType>
class GameSolver : public AbstractEquationSolver<ValueType> {
   public:
    virtual ~GameSolver() = default;
 
    virtual bool solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x,
                           std::vector<ValueType> const& b, std::vector<uint64_t>* player1Choices = nullptr,
                           std::vector<uint64_t>* player2Choices = nullptr) const = 0;
 
    virtual void repeatedMultiply(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x,
                                  std::vector<ValueType> const* b, uint_fast64_t n = 1) const = 0;
 
    void setTrackSchedulers(bool value = true);
 
    bool isTrackSchedulersSet() const;
 
    bool hasSchedulers() const;
 
    storm::storage::Scheduler<ValueType> computePlayer1Scheduler() const;
    storm::storage::Scheduler<ValueType> computePlayer2Scheduler() const;
 
    std::vector<uint_fast64_t> const& getPlayer1SchedulerChoices() const;
    std::vector<uint_fast64_t> const& getPlayer2SchedulerChoices() const;
 
    void setSchedulerHints(std::vector<uint_fast64_t>&& player1Choices, std::vector<uint_fast64_t>&& player2Choices);
 
    bool hasSchedulerHints() const;
 
    void setCachingEnabled(bool value);
 
    bool isCachingEnabled() const;
 
    /*
     * Clears the currently cached data that has been stored during previous calls of the solver.
     */
    virtual void clearCache() const;
 
    void setHasUniqueSolution(bool value = true);
 
    bool hasUniqueSolution() const;
 
   protected:
    GameSolver();
 
    bool trackSchedulers;
 
    mutable boost::optional<std::vector<uint_fast64_t>> player1SchedulerChoices;
    mutable boost::optional<std::vector<uint_fast64_t>> player2SchedulerChoices;
 
    // scheduler choices that might be considered by the solver as an initial guess
    boost::optional<std::vector<uint_fast64_t>> player1ChoicesHint;
    boost::optional<std::vector<uint_fast64_t>> player2ChoicesHint;
 
   private:
    bool uniqueSolution;
 
    bool cachingEnabled;
};
 
template<typename ValueType>
class GameSolverFactory {
   public:
    GameSolverFactory();
    virtual ~GameSolverFactory() = default;
 
    virtual std::unique_ptr<GameSolver<ValueType>> create(Environment const& env,
                                                          storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix,
                                                          storm::storage::SparseMatrix<ValueType> const& player2Matrix) const;
    virtual std::unique_ptr<GameSolver<ValueType>> create(Environment const& env,
                                                          storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix,
                                                          storm::storage::SparseMatrix<ValueType>&& player2Matrix) const;
 
    virtual std::unique_ptr<GameSolver<ValueType>> create(Environment const& env, std::vector<uint64_t> const& player1Grouping,
                                                          storm::storage::SparseMatrix<ValueType> const& player2Matrix) const;
    virtual std::unique_ptr<GameSolver<ValueType>> create(Environment const& env, std::vector<uint64_t>&& player1Grouping,
                                                          storm::storage::SparseMatrix<ValueType>&& player2Matrix) const;
};
 
}  // namespace solver
}  // namespace storm