SymbolicMinMaxLinearEquationSolver.h

Go to the documentation of this file.

#ifndef STORM_SOLVER_SYMBOLICMINMAXLINEAREQUATIONSOLVER_H_
#define STORM_SOLVER_SYMBOLICMINMAXLINEAREQUATIONSOLVER_H_
 
#include <boost/optional.hpp>
#include <memory>
#include <set>
#include <vector>
 
#include "storm/solver/MinMaxLinearEquationSolverRequirements.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/solver/SolverStatus.h"
#include "storm/solver/SymbolicEquationSolver.h"
#include "storm/solver/SymbolicLinearEquationSolver.h"
 
#include "storm/utility/NumberTraits.h"
 
#include "SolverSelectionOptions.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/expressions/Variable.h"
 
namespace storm {
 
class Environment;
 
namespace dd {
template<storm::dd::DdType Type, typename ValueType>
class Add;
 
template<storm::dd::DdType T>
class Bdd;
}  // namespace dd
 
namespace solver {
template<storm::dd::DdType DdType, typename ValueType>
class SymbolicMinMaxLinearEquationSolver : public SymbolicEquationSolver<DdType, ValueType> {
   public:
    SymbolicMinMaxLinearEquationSolver();
    virtual ~SymbolicMinMaxLinearEquationSolver() = default;
 
    SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows,
                                       storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables,
                                       std::set<storm::expressions::Variable> const& columnMetaVariables,
                                       std::set<storm::expressions::Variable> const& choiceVariables,
                                       std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
                                       std::unique_ptr<SymbolicLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory);
 
    virtual storm::dd::Add<DdType, ValueType> solveEquations(Environment const& env, storm::solver::OptimizationDirection const& dir,
                                                             storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
 
    virtual storm::dd::Add<DdType, ValueType> multiply(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x,
                                                       storm::dd::Add<DdType, ValueType> const* b = nullptr, uint_fast64_t n = 1) const;
 
    void setInitialScheduler(storm::dd::Bdd<DdType> const& scheduler);
 
    storm::dd::Bdd<DdType> const& getInitialScheduler() const;
 
    bool hasInitialScheduler() const;
 
    virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env,
                                                                   boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
 
    void setHasUniqueSolution(bool value = true);
 
    bool hasUniqueSolution() const;
 
    void setRequirementsChecked(bool value = true);
 
    bool isRequirementsCheckedSet() const;
 
    bool isSolution(OptimizationDirection dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
 
   private:
    MinMaxMethod getMethod(Environment const& env, bool isExactMode) const;
 
    storm::dd::Add<DdType, ValueType> solveEquationsWithScheduler(Environment const& env, storm::dd::Bdd<DdType> const& scheduler,
                                                                  storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
    storm::dd::Add<DdType, ValueType> solveEquationsWithScheduler(Environment const& env, SymbolicLinearEquationSolver<DdType, ValueType>& solver,
                                                                  storm::dd::Bdd<DdType> const& scheduler, storm::dd::Add<DdType, ValueType> const& x,
                                                                  storm::dd::Add<DdType, ValueType> const& b,
                                                                  storm::dd::Add<DdType, ValueType> const& diagonal) const;
 
    storm::dd::Add<DdType, ValueType> solveEquationsValueIteration(Environment const& env, storm::solver::OptimizationDirection const& dir,
                                                                   storm::dd::Add<DdType, ValueType> const& x,
                                                                   storm::dd::Add<DdType, ValueType> const& b) const;
    storm::dd::Add<DdType, ValueType> solveEquationsPolicyIteration(Environment const& env, storm::solver::OptimizationDirection const& dir,
                                                                    storm::dd::Add<DdType, ValueType> const& x,
                                                                    storm::dd::Add<DdType, ValueType> const& b) const;
    storm::dd::Add<DdType, ValueType> solveEquationsRationalSearch(Environment const& env, storm::solver::OptimizationDirection const& dir,
                                                                   storm::dd::Add<DdType, ValueType> const& x,
                                                                   storm::dd::Add<DdType, ValueType> const& b) const;
 
    template<typename RationalType, typename ImpreciseType>
    static storm::dd::Add<DdType, RationalType> sharpen(OptimizationDirection dir, uint64_t precision,
                                                        SymbolicMinMaxLinearEquationSolver<DdType, RationalType> const& rationalSolver,
                                                        storm::dd::Add<DdType, ImpreciseType> const& x, storm::dd::Add<DdType, RationalType> const& rationalB,
                                                        bool& isSolution);
 
    template<typename RationalType, typename ImpreciseType>
    storm::dd::Add<DdType, RationalType> solveEquationsRationalSearchHelper(Environment const& env, OptimizationDirection dir,
                                                                            SymbolicMinMaxLinearEquationSolver<DdType, RationalType> const& rationalSolver,
                                                                            SymbolicMinMaxLinearEquationSolver<DdType, ImpreciseType> const& impreciseSolver,
                                                                            storm::dd::Add<DdType, RationalType> const& rationalB,
                                                                            storm::dd::Add<DdType, ImpreciseType> const& x,
                                                                            storm::dd::Add<DdType, ImpreciseType> const& b) const;
    template<typename ImpreciseType>
    typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && storm::NumberTraits<ValueType>::IsExact, storm::dd::Add<DdType, ValueType>>::type
    solveEquationsRationalSearchHelper(Environment const& env, storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x,
                                       storm::dd::Add<DdType, ValueType> const& b) const;
    template<typename ImpreciseType>
    typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && !storm::NumberTraits<ValueType>::IsExact, storm::dd::Add<DdType, ValueType>>::type
    solveEquationsRationalSearchHelper(Environment const& env, storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x,
                                       storm::dd::Add<DdType, ValueType> const& b) const;
    template<typename ImpreciseType>
    typename std::enable_if<!std::is_same<ValueType, ImpreciseType>::value, storm::dd::Add<DdType, ValueType>>::type solveEquationsRationalSearchHelper(
        Environment const& env, storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x,
        storm::dd::Add<DdType, ValueType> const& b) const;
 
    template<storm::dd::DdType DdTypePrime, typename ValueTypePrime>
    friend class SymbolicMinMaxLinearEquationSolver;
 
    struct ValueIterationResult {
        ValueIterationResult(SolverStatus status, uint64_t iterations, storm::dd::Add<DdType, ValueType> const& values)
            : status(status), iterations(iterations), values(values) {
            // Intentionally left empty.
        }
 
        SolverStatus status;
        uint64_t iterations;
        storm::dd::Add<DdType, ValueType> values;
    };
 
    ValueIterationResult performValueIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x,
                                               storm::dd::Add<DdType, ValueType> const& b, ValueType const& precision, bool relativeTerminationCriterion,
                                               uint64_t maximalIterations) const;
 
   protected:
    // The matrix defining the coefficients of the linear equation system.
    storm::dd::Add<DdType, ValueType> A;
 
    // A BDD characterizing the illegal choices.
    storm::dd::Bdd<DdType> illegalMask;
 
    // An ADD characterizing the illegal choices.
    storm::dd::Add<DdType, ValueType> illegalMaskAdd;
 
    // The row variables.
    std::set<storm::expressions::Variable> rowMetaVariables;
 
    // The column variables.
    std::set<storm::expressions::Variable> columnMetaVariables;
 
    // The choice variables.
    std::set<storm::expressions::Variable> choiceVariables;
 
    // The pairs of meta variables used for renaming.
    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
 
    // A factory for creating linear equation solvers when needed.
    std::unique_ptr<SymbolicLinearEquationSolverFactory<DdType, ValueType>> linearEquationSolverFactory;
 
    // Whether the solver can assume that the min-max equation system has a unique solution
    bool uniqueSolution;
 
    // A flag indicating whether the requirements were checked.
    bool requirementsChecked;
 
    // A scheduler that specifies with which schedulers to start.
    boost::optional<storm::dd::Bdd<DdType>> initialScheduler;
 
   private:
    void forwardBounds(storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>& solver) const;
};
 
template<storm::dd::DdType DdType, typename ValueType>
class SymbolicMinMaxLinearEquationSolverFactory {
   public:
    virtual ~SymbolicMinMaxLinearEquationSolverFactory() = default;
 
    virtual std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> create(
        storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask,
        std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables,
        std::set<storm::expressions::Variable> const& choiceVariables,
        std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const = 0;
 
    MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, bool hasUniqueSolution = false,
                                                           boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
 
   private:
    virtual std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> create() const = 0;
};
 
template<storm::dd::DdType DdType, typename ValueType>
class GeneralSymbolicMinMaxLinearEquationSolverFactory : public SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType> {
   public:
    virtual std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> create(
        storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask,
        std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables,
        std::set<storm::expressions::Variable> const& choiceVariables,
        std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const override;
 
   private:
    virtual std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> create() const override;
};
 
}  // namespace solver
}  // namespace storm
 
#endif /* STORM_SOLVER_SYMBOLICMINMAXLINEAREQUATIONSOLVER_H_ */