RegionOptions.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <optional>
#include <set>
 
#include "storm-pars/modelchecker/region/RegionCheckEngine.h"
#include "storm-pars/modelchecker/region/RegionSplittingStrategy.h"
#include "storm-pars/storage/ParameterRegion.h"
 
#include "storm/api/properties.h"
#include "storm/modelchecker/CheckTask.h"
#include "storm/models/sparse/Model.h"
 
namespace storm {
namespace pars {
namespace modelchecker {
 
struct MonotonicityOptions {
    bool useMonotonicity;
    bool useOnlyGlobalMonotonicity;
    bool useBoundsFromPLA;
 
    explicit MonotonicityOptions(bool useMonotonicity = false, bool useOnlyGlobalMonotonicity = false, bool useBoundsFromPLA = false) {
        this->useMonotonicity = useMonotonicity;
        this->useOnlyGlobalMonotonicity = useOnlyGlobalMonotonicity;
        this->useBoundsFromPLA = useBoundsFromPLA;
    }
};
 
template<typename ValueType>
struct RegionRefinementOptions {
    std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
    storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> task;
    storm::modelchecker::RegionCheckEngine engine;
    storm::modelchecker::RegionSplittingStrategy regionSplittingStrategy;
 
    MonotonicityOptions monotonicitySetting;
    std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> const& discreteVariables;
    bool allowModelSimplification;
    bool graphPreserving;
    bool preconditionsValidated;
    std::optional<std::pair<std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType>,
                            std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType>>>
        monotoneParameters;
 
    RegionRefinementOptions(std::shared_ptr<storm::models::sparse::Model<ValueType>> model,
                            storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> task, storm::modelchecker::RegionCheckEngine engine,
                            storm::modelchecker::RegionSplittingStrategy regionSplittingStrategy,
                            MonotonicityOptions monotonicitySetting = MonotonicityOptions(),
                            std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> const& discreteVariables = {},
                            bool allowModelSimplification = true, bool graphPreserving = true, bool preconditionsValidated = false,
                            std::optional<std::pair<std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType>,
                                                    std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType>>>
                                monotoneParameters = std::nullopt)
        : model(std::move(model)),
          task(std::move(task)),
          engine(engine),
          regionSplittingStrategy(std::move(regionSplittingStrategy)),
          monotonicitySetting(std::move(monotonicitySetting)),
          discreteVariables(discreteVariables),
          allowModelSimplification(allowModelSimplification),
          graphPreserving(graphPreserving),
          preconditionsValidated(preconditionsValidated),
          monotoneParameters(std::move(monotoneParameters)) {}
};
 
}  // namespace modelchecker
}  // namespace pars
}  // namespace storm