GuessingValueIterationHelper.h

Go to the documentation of this file.

#pragma once
 
#include <vector>
 
#include "storm/solver/helper/ValueIterationOperator.h"
 
#include "storm/solver/OptimizationDirection.h"
#include "storm/solver/SolverStatus.h"
#include "storm/storage/BitVector.h"
 
namespace storm::solver::helper {
 
template<typename ValueType>
struct GVIData {
    std::vector<ValueType> const& x;
    std::vector<ValueType> const& y;
    SolverStatus const status;
};
 
namespace gviinternal {
 
typedef uint64_t IndexType;
enum class VerifyResult { Verified, Converged, Unverified };
 
template<typename ValueType>
class IterationHelper {
   public:
    IterationHelper(storm::storage::SparseMatrix<ValueType> const& matrix_);
 
    IndexType selectRowGroupToGuess(const std::vector<ValueType>& lowerX, const std::vector<ValueType>& upperX);
 
    bool checkConvergence(std::vector<ValueType> const& lower, std::vector<ValueType> const& upper, bool relative, ValueType const& precision) const;
    ValueType getSumLength(std::vector<ValueType>& lower, std::vector<ValueType>& upper) const;
 
   private:
    storm::storage::SparseMatrix<ValueType> const& matrix;
    // this is only used to avoid reallocations
    std::vector<ValueType> weights;
 
    void swipeWeights();
};
 
}  // namespace gviinternal
 
template<typename ValueType, OptimizationDirection Dir>
class GVIBackend;

template<typename ValueType, bool TrivialRowGrouping>
class GuessingValueIterationHelper {
   public:
    explicit GuessingValueIterationHelper(std::shared_ptr<ValueIterationOperator<ValueType, TrivialRowGrouping>> viOperator,
                                          const storage::SparseMatrix<ValueType>& matrix);

    SolverStatus solveEquations(std::vector<ValueType>& lowerX, std::vector<ValueType>& upperX, const std::vector<ValueType>& b, uint64_t& numIterations,
                                bool relative, ValueType precision, std::optional<storm::solver::OptimizationDirection> dir,
                                std::function<SolverStatus(GVIData<ValueType> const&)> const& iterationCallback);
 
   private:
    std::shared_ptr<ValueIterationOperator<ValueType, TrivialRowGrouping>> viOperator;
    gviinternal::IterationHelper<ValueType> iterationHelper;
    std::vector<ValueType> guessLower, guessUpper;
    gviinternal::IndexType selectRowGroupToGuess(std::vector<ValueType>& lowerX, std::vector<ValueType>& upperX);
 
    template<OptimizationDirection Dir>
    SolverStatus solveEquations(std::vector<ValueType>& lowerX, std::vector<ValueType>& upperX, const std::vector<ValueType>& b, uint64_t& numIterations,
                                bool relative, ValueType precision, std::function<SolverStatus(GVIData<ValueType> const&)> const& iterationCallback);
 
    template<OptimizationDirection Dir>
    void applyInPlace(std::vector<ValueType>& lowerX, std::vector<ValueType>& upperX, const std::vector<ValueType>& b, GVIBackend<ValueType, Dir>& backend);
 
    template<OptimizationDirection Dir>
    std::pair<gviinternal::VerifyResult, SolverStatus> tryVerify(std::vector<ValueType>& lowerX, std::vector<ValueType>& upperX,
                                                                 const std::vector<ValueType>& b, uint64_t& numIterations,
                                                                 gviinternal::IndexType rowGroupToGuess, ValueType guessValue, bool relative,
                                                                 ValueType precision,
                                                                 std::function<SolverStatus(GVIData<ValueType> const&)> const& iterationCallback);
 
    template<OptimizationDirection Dir>
    SolverStatus doIterations(std::vector<ValueType>& lowerX, std::vector<ValueType>& upperX, const std::vector<ValueType>& b, uint64_t& numIterations,
                              std::optional<uint64_t> maxIterations, bool relative, const ValueType& precision,
                              std::function<SolverStatus(GVIData<ValueType> const&)> const& iterationCallback);
};
}  // namespace storm::solver::helper