BeliefBasedModelCheckerOptions.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <optional>
#include <vector>
 
#include <storm-pomdp/beliefs/exploration/ExplorationQueueOrder.h>
 
namespace storm::pomdp::beliefs {
enum explorationTerminationCriterion { MAX_EXPLORATION_SIZE, MAX_EXPLORATION_TIME, MAX_EXPLORATION_SIZE_AND_TIME, NONE };
 
template<typename ValueType>
struct BeliefBasedModelCheckerOptions {
    bool buildChoiceLabeling = true;
    bool useClipping = false;
    bool cutZeroGap = false;
 
    ExplorationQueueOrder explorationQueueOrder = ExplorationQueueOrder::FIFO;
 
    // Clipping abstraction parameters
    std::optional<std::vector<uint64_t>> clippingResolutions;
 
    // Termination criteria
    std::optional<uint64_t> maxExplorationSize = std::nullopt;
    std::optional<uint64_t> maxExplorationTime = std::nullopt;

    [[nodiscard]] explorationTerminationCriterion getTerminationCriterion() const {
        if (maxExplorationSize.has_value() && maxExplorationTime.has_value()) {
            return explorationTerminationCriterion::MAX_EXPLORATION_SIZE_AND_TIME;
        }
        if (maxExplorationSize.has_value()) {
            return explorationTerminationCriterion::MAX_EXPLORATION_SIZE;
        }
        if (maxExplorationTime.has_value()) {
            return explorationTerminationCriterion::MAX_EXPLORATION_TIME;
        }
        return explorationTerminationCriterion::NONE;
    }
};
}  // namespace storm::pomdp::beliefs