BeliefBasedModelChecker.h

Go to the documentation of this file.

#pragma once
 
#include "BeliefBasedModelCheckerOptions.h"
#include "BeliefBasedModelCheckerResult.h"
#include "storm-pomdp/beliefs/verification/PropertyInformation.h"
#include "storm-pomdp/storage/BeliefExplorationBounds.h"
 
namespace storm {
class Environment;
 
namespace pomdp::beliefs {
 
template<typename PomdpModelType, typename BeliefValueType = typename PomdpModelType::ValueType,
         typename BeliefMdpValueType = typename PomdpModelType::ValueType>
class BeliefBasedModelChecker {
   public:
    using PomdpValueType = typename PomdpModelType::ValueType;
    explicit BeliefBasedModelChecker(PomdpModelType const& pomdp);

    BeliefBasedModelCheckerResult<BeliefMdpValueType> checkUnfold(storm::Environment const& env, PropertyInformation const& propertyInformation,
                                                                  BeliefBasedModelCheckerOptions<BeliefMdpValueType> const& options,
                                                                  storage::BeliefExplorationBounds<PomdpValueType> const& valueBounds);

    BeliefBasedModelCheckerResult<BeliefMdpValueType> checkDiscretize(storm::Environment const& env, PropertyInformation const& propertyInformation,
                                                                      storm::pomdp::beliefs::BeliefBasedModelCheckerOptions<BeliefMdpValueType> const& options,
                                                                      uint64_t resolution, bool useDynamic,
                                                                      storage::BeliefExplorationBounds<PomdpValueType> const& valueBounds);

    BeliefBasedModelCheckerResult<BeliefMdpValueType> checkRewardAwareUnfold(
        storm::Environment const& env, PropertyInformation const& propertyInformation,
        storm::pomdp::beliefs::BeliefBasedModelCheckerOptions<BeliefMdpValueType> const& options,
        storage::BeliefExplorationBounds<typename PomdpModelType::ValueType> const& valueBounds, std::vector<std::string> const& relevantRewardModelNames);

    BeliefBasedModelCheckerResult<BeliefMdpValueType> checkRewardAwareDiscretize(
        storm::Environment const& env, PropertyInformation const& propertyInformation,
        storm::pomdp::beliefs::BeliefBasedModelCheckerOptions<BeliefMdpValueType> const& options, uint64_t resolution, bool useDynamic,
        storage::BeliefExplorationBounds<typename PomdpModelType::ValueType> const& valueBounds, std::vector<std::string> const& relevantRewardModelNames);
 
   private:
    PomdpModelType const& inputPomdp;
};
}  // namespace pomdp::beliefs
}  // namespace storm