MinMaxLinearEquationSolver.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <memory>
#include <vector>
 
#include <boost/optional.hpp>
 
#include "storm/solver/AbstractEquationSolver.h"
#include "storm/solver/MinMaxLinearEquationSolverRequirements.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/solver/SolverSelectionOptions.h"
#include "storm/solver/UncertaintyResolutionMode.h"
#include "storm/storage/sparse/StateType.h"
 
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/utility/macros.h"
 
namespace storm {
 
class Environment;
 
namespace storage {
template<typename T>
class SparseMatrix;
template<typename ValueType>
class Scheduler;
}  // namespace storage
 
namespace solver {
 
template<typename ValueType, typename SolutionType = ValueType>
class MinMaxLinearEquationSolver : public AbstractEquationSolver<SolutionType> {
   protected:
    MinMaxLinearEquationSolver(OptimizationDirectionSetting direction = OptimizationDirectionSetting::Unset);
 
   public:
    virtual ~MinMaxLinearEquationSolver();
 
    virtual void setMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) = 0;
    virtual void setMatrix(storm::storage::SparseMatrix<ValueType>&& matrix) = 0;
 
    bool solveEquations(Environment const& env, OptimizationDirection d, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
 
    void solveEquations(Environment const& env, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
 
    void setOptimizationDirection(OptimizationDirection direction);
 
    void unsetOptimizationDirection();
 
    void setUncertaintyResolutionMode(UncertaintyResolutionMode uncertaintyResolutionMode);
 
    UncertaintyResolutionMode getUncertaintyResolutionMode() const;
 
    virtual void setSchedulerFixedForRowGroup(storm::storage::BitVector&& schedulerFixedForRowGroup);
 
    void setHasUniqueSolution(bool value = true);
 
    bool hasUniqueSolution() const;
 
    void setHasNoEndComponents(bool value = true);
 
    bool hasNoEndComponents() const;
 
    void setTrackScheduler(bool trackScheduler = true);
 
    bool isTrackSchedulerSet() const;
 
    bool hasScheduler() const;
 
    storm::storage::Scheduler<ValueType> computeScheduler() const;
 
    std::vector<uint_fast64_t> const& getSchedulerChoices() const;
 
    std::vector<uint_fast64_t> const& getRobustSchedulerIndex() const;
 
    void setCachingEnabled(bool value);
 
    bool isCachingEnabled() const;
 
    virtual void clearCache() const;
 
    void setInitialScheduler(std::vector<uint_fast64_t>&& choices);
 
    bool hasInitialScheduler() const;
 
    std::vector<uint_fast64_t> const& getInitialScheduler() const;
 
    virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env,
                                                                   boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none,
                                                                   bool const& hasInitialScheduler = false) const;
 
    void setRequirementsChecked(bool value = true);
 
    bool isRequirementsCheckedSet() const;
 
   protected:
    virtual bool internalSolveEquations(Environment const& env, OptimizationDirection d, std::vector<SolutionType>& x,
                                        std::vector<ValueType> const& b) const = 0;
 
    OptimizationDirectionSetting direction;
 
    bool trackScheduler;
 
    mutable boost::optional<std::vector<uint_fast64_t>> schedulerChoices;
 
    mutable boost::optional<std::vector<uint_fast64_t>> robustSchedulerIndex;
 
    boost::optional<std::vector<uint_fast64_t>> initialScheduler;
 
    boost::optional<storm::storage::BitVector> choiceFixedForRowGroup;
 
   private:
    bool uniqueSolution;
 
    bool noEndComponents;
 
    bool cachingEnabled;
 
    bool requirementsChecked;
 
    UncertaintyResolutionMode uncertaintyResolutionMode;
};
 
template<typename ValueType, typename SolutionType = ValueType>
class MinMaxLinearEquationSolverFactory {
   public:
    MinMaxLinearEquationSolverFactory();
    virtual ~MinMaxLinearEquationSolverFactory() = default;
 
    std::unique_ptr<MinMaxLinearEquationSolver<ValueType, SolutionType>> create(Environment const& env,
                                                                                storm::storage::SparseMatrix<ValueType> const& matrix) const;
    std::unique_ptr<MinMaxLinearEquationSolver<ValueType, SolutionType>> create(Environment const& env, storm::storage::SparseMatrix<ValueType>&& matrix) const;
    virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType, SolutionType>> create(Environment const& env) const = 0;
 
    MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, bool hasUniqueSolution = false, bool hasNoEndComponents = false,
                                                           boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none,
                                                           bool hasInitialScheduler = false, bool trackScheduler = false) const;
    void setRequirementsChecked(bool value = true);
    bool isRequirementsCheckedSet() const;
 
   private:
    bool requirementsChecked;
};
 
template<typename ValueType, typename SolutionType = ValueType>
class GeneralMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory<ValueType, SolutionType> {
   public:
    GeneralMinMaxLinearEquationSolverFactory();
 
    // Make the other create methods visible.
    using MinMaxLinearEquationSolverFactory<ValueType, SolutionType>::create;
 
    virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType, SolutionType>> create(Environment const& env) const override;
 
   protected:
    MinMaxMethod getMethod(Environment env) const;
};
 
}  // namespace solver
}  // namespace storm