verification.h

Go to the documentation of this file.

#pragma once
 
#include <limits>
#include <memory>
#include <unordered_map>
#include <vector>
 
#include "storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.h"
#include "storm/environment/Environment.h"
#include "storm/modelchecker/CheckTask.h"
#include "storm/models/sparse/Model.h"
#include "storm/models/sparse/Pomdp.h"
#include "storm/storage/Scheduler.h"
#include "storm/utility/constants.h"
 
namespace storm {
namespace pomdp {
namespace api {

template<typename ValueType>
typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>>::Result underapproximateWithCutoffs(
    std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> pomdp, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task,
    uint64_t sizeThreshold,
    std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>> additionalPomdpStateValues =
        std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>>()) {
    storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType> options(false, true);
    options.useClipping = false;
    options.useStateEliminationCutoff = false;
    options.sizeThresholdInit = sizeThreshold;
    storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> modelchecker(pomdp, options);
    return modelchecker.check(task.getFormula(), additionalPomdpStateValues);
}

template<typename ValueType>
typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>>::Result underapproximateWithoutHeuristicValues(
    std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> pomdp, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task,
    uint64_t sizeThreshold, std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>> pomdpStateValues) {
    storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType> options(false, true);
    options.skipHeuristicSchedulers = true;
    options.useClipping = false;
    options.useStateEliminationCutoff = false;
    options.sizeThresholdInit = sizeThreshold;
    storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> modelchecker(pomdp, options);
    return modelchecker.check(task.getFormula(), pomdpStateValues);
}
 
// Interactive Interface
template<typename ValueType>
storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> createInteractiveUnfoldingModelChecker(
    storm::Environment const& env, std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> pomdp, bool useClipping) {
    storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType> options(false, true);
    options.skipHeuristicSchedulers = false;
    options.useClipping = useClipping;
    options.useStateEliminationCutoff = false;
    options.sizeThresholdInit = std::numeric_limits<uint64_t>::max();  // i.e. no size limit
    options.interactiveUnfolding = true;
    options.refine = false;
    options.gapThresholdInit = 0;
    options.cutZeroGap = false;
    storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> modelchecker(pomdp, options);
    return modelchecker;
}

template<typename ValueType>
void startInteractiveExploration(storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>>& modelchecker,
                                 storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task,
                                 std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>> additionalPomdpStateValues =
                                     std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>>()) {
    modelchecker.check(task.getFormula(), additionalPomdpStateValues);
}

template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> extractSchedulerAsMarkovChain(
    typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>>::Result modelcheckingResult) {
    return modelcheckingResult.schedulerAsMarkovChain;
}

template<typename ValueType>
storm::storage::Scheduler<ValueType> getCutoffScheduler(
    typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>>::Result modelcheckingResult,
    uint64_t schedId) {
    return modelcheckingResult.cutoffSchedulers.at(schedId);
}

template<typename ValueType>
uint64_t getNumberOfPreprocessingSchedulers(
    typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>>::Result modelcheckingResult) {
    return modelcheckingResult.cutoffSchedulers.size();
}
}  // namespace api
}  // namespace pomdp
}  // namespace storm