Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseDtmcParameterLiftingModelChecker.h
Go to the documentation of this file.
1#pragma once
2
3#include <boost/optional.hpp>
4#include <memory>
5#include <vector>
6
14
15namespace storm {
16namespace modelchecker {
17
18template<typename SparseModelType, typename ConstantType>
20 public:
21 typedef typename SparseModelType::ValueType ValueType;
22
26
30
31 virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel,
32 CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
33
34 virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel,
35 CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool generateRegionSplitEstimates = false,
36 bool allowModelSimplification = true) override;
37 void specify_internal(Environment const& env, std::shared_ptr<SparseModelType> parametricModel,
38 CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification);
39
40 boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
41 boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
42
43 virtual bool isRegionSplitEstimateSupported() const override;
44 virtual std::map<VariableType, double> getRegionSplitEstimate() const override;
45
46 virtual std::shared_ptr<storm::analysis::Order> extendOrder(std::shared_ptr<storm::analysis::Order> order,
48
49 virtual void extendLocalMonotonicityResult(storm::storage::ParameterRegion<ValueType> const& region, std::shared_ptr<storm::analysis::Order> order,
50 std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>> localMonotonicityResult) override;
51
52 void setMaxSplitDimensions(uint64_t) override;
53 void resetMaxSplitDimensions() override;
54
55 protected:
57 virtual void specifyUntilFormula(Environment const& env, CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) override;
60
64
65 virtual std::unique_ptr<CheckResult> computeQuantitativeValues(
67 std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>> localMonotonicityResult = nullptr) override;
68
69 void computeRegionSplitEstimates(std::vector<ConstantType> const& quantitativeResult, std::vector<uint_fast64_t> const& schedulerChoices,
71
72 virtual void reset() override;
73
75 storm::analysis::MonotonicityResult<VariableType>& monRes, bool splitForExtremum) const override;
76
77 private:
78 storm::storage::BitVector maybeStates;
79 std::vector<ConstantType> resultsForNonMaybeStates;
80 boost::optional<uint_fast64_t> stepBound;
81
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;
85
86 std::unique_ptr<storm::transformer::ParameterLifter<ValueType, ConstantType>> parameterLifter;
87 std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>> solverFactory;
88 bool solvingRequiresUpperRewardBounds;
89
90 // Results from the most recent solver call.
91 boost::optional<std::vector<uint_fast64_t>> minSchedChoices, maxSchedChoices;
92 std::vector<ConstantType> x;
93 boost::optional<ConstantType> lowerResultBound, upperResultBound;
94
95 bool regionSplitEstimationsEnabled;
96 std::map<VariableType, double> regionSplitEstimates;
97 uint64_t maxSplitDimensions;
98
99 // Used for monotonicity
100 bool useRegionSplitEstimates;
101 std::unique_ptr<storm::analysis::MonotonicityChecker<ValueType>> monotonicityChecker;
102};
103} // namespace modelchecker
104} // namespace storm
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 &region, 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
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 storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType > & getInstantiationChecker() override
virtual std::unique_ptr< CheckResult > computeQuantitativeValues(Environment const &env, storm::storage::ParameterRegion< ValueType > const &region, 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
virtual void splitSmart(storm::storage::ParameterRegion< ValueType > &region, std::vector< storm::storage::ParameterRegion< ValueType > > &regionVector, storm::analysis::MonotonicityResult< VariableType > &monRes, bool splitForExtremum) const override
boost::optional< storm::storage::Scheduler< ConstantType > > getCurrentMinScheduler()
boost::optional< storm::storage::Scheduler< ConstantType > > getCurrentMaxScheduler()
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 &region, 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 ...
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
storm::utility::parametric::CoefficientType< ParametricType >::type CoefficientType
LabParser.cpp.
Definition cli.cpp:18