3#include <boost/optional.hpp>
16namespace modelchecker {
18template<
typename SparseModelType,
typename ConstantType>
21 typedef typename SparseModelType::ValueType
ValueType;
36 bool allowModelSimplification =
true)
override;
46 virtual std::shared_ptr<storm::analysis::Order>
extendOrder(std::shared_ptr<storm::analysis::Order> order,
69 void computeRegionSplitEstimates(std::vector<ConstantType>
const& quantitativeResult, std::vector<uint_fast64_t>
const& schedulerChoices,
72 virtual void reset()
override;
79 std::vector<ConstantType> resultsForNonMaybeStates;
80 boost::optional<uint_fast64_t> stepBound;
82 std::unique_ptr<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>> instantiationChecker;
83 std::unique_ptr<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>> instantiationCheckerSAT;
84 std::unique_ptr<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>> instantiationCheckerVIO;
86 std::unique_ptr<storm::transformer::ParameterLifter<ValueType, ConstantType>> parameterLifter;
87 std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>> solverFactory;
88 bool solvingRequiresUpperRewardBounds;
91 boost::optional<std::vector<uint_fast64_t>> minSchedChoices, maxSchedChoices;
92 std::vector<ConstantType> x;
93 boost::optional<ConstantType> lowerResultBound, upperResultBound;
95 bool regionSplitEstimationsEnabled;
96 std::map<VariableType, double> regionSplitEstimates;
97 uint64_t maxSplitDimensions;
100 bool useRegionSplitEstimates;
101 std::unique_ptr<storm::analysis::MonotonicityChecker<ValueType>> monotonicityChecker;
Monotonicity
The results of monotonicity checking for a single Parameter Region.
storm::storage::ParameterRegion< ParametricType >::VariableType VariableType
virtual void extendLocalMonotonicityResult(storm::storage::ParameterRegion< ValueType > const ®ion, std::shared_ptr< storm::analysis::Order > order, std::shared_ptr< storm::analysis::LocalMonotonicityResult< VariableType > > localMonotonicityResult) override
virtual std::shared_ptr< storm::analysis::Order > extendOrder(std::shared_ptr< storm::analysis::Order > order, storm::storage::ParameterRegion< ValueType > region) override
SparseDtmcParameterLiftingModelChecker()
virtual void specifyReachabilityRewardFormula(Environment const &env, CheckTask< storm::logic::EventuallyFormula, ConstantType > const &checkTask) override
virtual storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType > & getInstantiationCheckerVIO() override
virtual void specify(Environment const &env, std::shared_ptr< storm::models::ModelBase > parametricModel, CheckTask< storm::logic::Formula, ValueType > const &checkTask, bool generateRegionSplitEstimates=false, bool allowModelSimplification=true) override
storm::analysis::MonotonicityResult< VariableType >::Monotonicity Monotonicity
virtual bool canHandle(std::shared_ptr< storm::models::ModelBase > parametricModel, CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
storm::storage::ParameterRegion< ValueType >::CoefficientType CoefficientType
virtual void reset() override
virtual storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType > & getInstantiationChecker() override
virtual ~SparseDtmcParameterLiftingModelChecker()=default
virtual std::unique_ptr< CheckResult > computeQuantitativeValues(Environment const &env, storm::storage::ParameterRegion< ValueType > const ®ion, storm::solver::OptimizationDirection const &dirForParameters, std::shared_ptr< storm::analysis::LocalMonotonicityResult< VariableType > > localMonotonicityResult=nullptr) override
virtual void specifyBoundedUntilFormula(const CheckTask< storm::logic::BoundedUntilFormula, ConstantType > &checkTask) override
SparseModelType::ValueType ValueType
virtual void splitSmart(storm::storage::ParameterRegion< ValueType > ®ion, std::vector< storm::storage::ParameterRegion< ValueType > > ®ionVector, storm::analysis::MonotonicityResult< VariableType > &monRes, bool splitForExtremum) const override
boost::optional< storm::storage::Scheduler< ConstantType > > getCurrentMinScheduler()
boost::optional< storm::storage::Scheduler< ConstantType > > getCurrentMaxScheduler()
RegionModelChecker< ValueType >::VariableType VariableType
virtual void specifyCumulativeRewardFormula(const CheckTask< storm::logic::CumulativeRewardFormula, ConstantType > &checkTask) override
virtual storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType > & getInstantiationCheckerSAT() override
void resetMaxSplitDimensions() override
When splitting, split in every dimension.
void computeRegionSplitEstimates(std::vector< ConstantType > const &quantitativeResult, std::vector< uint_fast64_t > const &schedulerChoices, storm::storage::ParameterRegion< ValueType > const ®ion, storm::solver::OptimizationDirection const &dirForParameters)
void setMaxSplitDimensions(uint64_t) override
When splitting, split in at most this many dimensions.
virtual void specifyUntilFormula(Environment const &env, CheckTask< storm::logic::UntilFormula, ConstantType > const &checkTask) override
void specify_internal(Environment const &env, std::shared_ptr< SparseModelType > parametricModel, CheckTask< storm::logic::Formula, ValueType > const &checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification)
virtual bool isRegionSplitEstimateSupported() const override
Returns true if region split estimation (a) was enabled when model and check task have been specified...
virtual std::map< VariableType, double > getRegionSplitEstimate() const override
Returns an estimate of the benefit of splitting the last checked region with respect to each paramete...
Class to efficiently check a formula on a parametric model with different parameter instantiations.
Class to approximatively check a formula on a parametric model for all parameter valuations within a ...
std::shared_ptr< SparseModelType > parametricModel
A bit vector that is internally represented as a vector of 64-bit values.
storm::utility::parametric::CoefficientType< ParametricType >::type CoefficientType