BeliefExplorationPomdpModelChecker.h

Go to the documentation of this file.

#include "storm-pomdp/builder/BeliefMdpExplorer.h"
#include "storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerOptions.h"
#include "storm-pomdp/storage/BeliefManager.h"
#include "storm/utility/logging.h"
 
#include "storm/storage/jani/Property.h"
#include "storm/utility/Stopwatch.h"
 
namespace storm {
class Environment;
 
namespace models {
namespace sparse {
template<class ValueType, typename RewardModelType>
class Pomdp;
}
}  // namespace models
namespace logic {
class Formula;
}
 
namespace pomdp {
namespace modelchecker {
 
template<typename ValueType>
struct POMDPValueBounds {
    // values generated by memoryless schedulers during pre-processing
    storm::pomdp::storage::PreprocessingPomdpValueBounds<ValueType> trivialPomdpValueBounds;
    // values for clipping compensation
    storm::pomdp::storage::ExtremePOMDPValueBound<ValueType> extremePomdpValueBound;
    // values generated by a finite memory schedulers. Each scheduler is represented by a vector of maps representing (memory node x state) -> value
    std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>> fmSchedulerValueList;
};
template<typename PomdpModelType, typename BeliefValueType = typename PomdpModelType::ValueType, typename BeliefMDPType = typename PomdpModelType::ValueType>
class BeliefExplorationPomdpModelChecker {
   public:
    typedef BeliefMDPType ValueType;
    typedef typename PomdpModelType::RewardModelType RewardModelType;
    typedef storm::storage::BeliefManager<PomdpModelType, BeliefValueType> BeliefManagerType;
    typedef storm::builder::BeliefMdpExplorer<PomdpModelType, BeliefValueType> ExplorerType;
    typedef BeliefExplorationPomdpModelCheckerOptions<ValueType> Options;
 
    /* Struct Definition(s) */
    enum class Status {
        Uninitialized,
        Exploring,
        ModelExplorationFinished,
        ResultAvailable,
        Terminated,
        Converged,
    };
 
    struct Result {
        Result(ValueType lower, ValueType upper);
        ValueType lowerBound;
        ValueType upperBound;
        ValueType diff(bool relative = false) const;
        bool updateLowerBound(ValueType const& value);
        bool updateUpperBound(ValueType const& value);
        std::shared_ptr<storm::models::sparse::Model<ValueType>> schedulerAsMarkovChain;
        std::vector<storm::storage::Scheduler<ValueType>> cutoffSchedulers;
    };
 
    /* Functions */
 
    explicit BeliefExplorationPomdpModelChecker(std::shared_ptr<PomdpModelType> pomdp, Options options = Options());
 
    Result check(storm::Environment const& env, storm::logic::Formula const& formula, storm::Environment const& preProcEnv,
                 std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>> const& additionalUnderApproximationBounds =
                     std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>>());
    Result check(storm::logic::Formula const& formula, storm::Environment const& preProcEnv,
                 std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>> const& additionalUnderApproximationBounds =
                     std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>>());
    Result check(storm::logic::Formula const& formula,
                 std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>> const& additionalUnderApproximationBounds =
                     std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>>());
    Result check(storm::Environment const& env, storm::logic::Formula const& formula,
                 std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>> const& additionalUnderApproximationBounds =
                     std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>>());
 
    void printStatisticsToStream(std::ostream& stream) const;
 
    void precomputeValueBounds(const logic::Formula& formula, storm::Environment const& preProcEnv);
 
    void unfoldInteractively(storm::Environment const& env, std::set<uint32_t> const& targetObservations, bool min, std::optional<std::string> rewardModelName,
                             storm::pomdp::modelchecker::POMDPValueBounds<ValueType> const& valueBounds, Result& result);
    void unfoldInteractively(std::set<uint32_t> const& targetObservations, bool min, std::optional<std::string> rewardModelName,
                             storm::pomdp::modelchecker::POMDPValueBounds<ValueType> const& valueBounds, Result& result);
 
    void pauseUnfolding();
 
    void continueUnfolding();
 
    void terminateUnfolding();
 
    bool isResultReady();
 
    bool isExploring();
 
    bool hasConverged();
 
    Result getInteractiveResult();
 
    std::shared_ptr<ExplorerType> getInteractiveBeliefExplorer();
 
    void setFMSchedValueList(std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>> valueList);
 
    int64_t getStatus();
 
   private:
    /* Struct Definition(s) */
 
    enum class UnfoldingControl { Run, Pause, Terminate };
 
    struct Statistics {
        Statistics();
        std::optional<uint64_t> refinementSteps;
        storm::utility::Stopwatch totalTime;
 
        bool beliefMdpDetectedToBeFinite;
        bool refinementFixpointDetected;
 
        std::optional<uint64_t> overApproximationStates;
        bool overApproximationBuildAborted;
        storm::utility::Stopwatch overApproximationBuildTime;
        storm::utility::Stopwatch overApproximationCheckTime;
        std::optional<BeliefValueType> overApproximationMaxResolution;
 
        std::optional<uint64_t> underApproximationStates;
        bool underApproximationBuildAborted;
        storm::utility::Stopwatch underApproximationBuildTime;
        storm::utility::Stopwatch underApproximationCheckTime;
        std::optional<uint64_t> underApproximationStateLimit;
        std::optional<uint64_t> nrClippingAttempts;
        std::optional<uint64_t> nrClippedStates;
        std::optional<uint64_t> nrTruncatedStates;
        storm::utility::Stopwatch clipWatch;
        storm::utility::Stopwatch clippingPreTime;
 
        bool aborted;
    };
 
    struct HeuristicParameters {
        ValueType gapThreshold;
        ValueType observationThreshold;
        uint64_t sizeThreshold;
        ValueType optimalChoiceValueEpsilon;
    };
 
    /* Functions */
 
    PomdpModelType const& pomdp() const;
 
    void refineReachability(storm::Environment const& env, std::set<uint32_t> const& targetObservations, bool min, std::optional<std::string> rewardModelName,
                            storm::pomdp::modelchecker::POMDPValueBounds<ValueType> const& valueBounds, Result& result);
 
    bool buildOverApproximation(storm::Environment const& env, std::set<uint32_t> const& targetObservations, bool min, bool computeRewards, bool refine,
                                HeuristicParameters const& heuristicParameters, std::vector<BeliefValueType>& observationResolutionVector,
                                std::shared_ptr<BeliefManagerType>& beliefManager, std::shared_ptr<ExplorerType>& overApproximation);
 
    bool buildUnderApproximation(storm::Environment const& env, std::set<uint32_t> const& targetObservations, bool min, bool computeRewards, bool refine,
                                 HeuristicParameters const& heuristicParameters, std::shared_ptr<BeliefManagerType>& beliefManager,
                                 std::shared_ptr<ExplorerType>& underApproximation, bool interactive);
 
    void clipToGrid(uint64_t clippingStateId, bool computeRewards, bool min, std::shared_ptr<BeliefManagerType>& beliefManager,
                    std::shared_ptr<ExplorerType>& beliefExplorer);
 
    bool clipToGridExplicitly(uint64_t clippingStateId, bool computeRewards, std::shared_ptr<BeliefManagerType>& beliefManager,
                              std::shared_ptr<ExplorerType>& beliefExplorer, uint64_t localActionIndex);
 
    BeliefValueType rateObservation(typename ExplorerType::SuccessorObservationInformation const& info, BeliefValueType const& observationResolution,
                                    BeliefValueType const& maxResolution);
 
    std::vector<BeliefValueType> getObservationRatings(std::shared_ptr<ExplorerType> const& overApproximation,
                                                       std::vector<BeliefValueType> const& observationResolutionVector);
 
    typename PomdpModelType::ValueType getGap(typename PomdpModelType::ValueType const& l, typename PomdpModelType::ValueType const& u);
 
    void setUnfoldingControl(UnfoldingControl newUnfoldingControl);
 
    /* Variables */
 
    Statistics statistics;
    Options options;
 
    std::shared_ptr<PomdpModelType> inputPomdp;
    std::shared_ptr<PomdpModelType> preprocessedPomdp;
 
    storm::utility::ConstantsComparator<BeliefValueType> beliefTypeCC;
    storm::utility::ConstantsComparator<ValueType> valueTypeCC;
 
    storm::pomdp::modelchecker::POMDPValueBounds<ValueType> pomdpValueBounds;
 
    std::shared_ptr<ExplorerType> interactiveUnderApproximationExplorer;
 
    Status unfoldingStatus;
    UnfoldingControl unfoldingControl;
    Result interactiveResult = Result(-storm::utility::infinity<ValueType>(), storm::utility::infinity<ValueType>());
};
 
}  // namespace modelchecker
}  // namespace pomdp
}  // namespace storm