Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseMdpParameterLiftingModelChecker.h
Go to the documentation of this file.
1#pragma once
2
3#include <boost/optional.hpp>
4#include <memory>
5#include <vector>
6
10
16
17namespace storm {
18namespace modelchecker {
19
20template<typename SparseModelType, typename ConstantType>
22 public:
26
27 virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel,
29 virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel,
30 CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false,
31 bool allowModelSimplification = true) override;
32 void specify_internal(Environment const& env, std::shared_ptr<SparseModelType> parametricModel,
33 CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification);
34
35 boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
36 boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
37 boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentPlayer1Scheduler();
38
39 protected:
41 virtual void specifyUntilFormula(Environment const& env, CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) override;
44
46
47 virtual std::unique_ptr<CheckResult> computeQuantitativeValues(
49 storm::solver::OptimizationDirection const& dirForParameters,
51 localMonotonicityResult = nullptr) override;
52
53 virtual void reset() override;
54
55 private:
56 void computePlayer1Matrix(boost::optional<storm::storage::BitVector> const& selectedRows = boost::none);
57
58 storm::storage::BitVector maybeStates;
59 std::vector<ConstantType> resultsForNonMaybeStates;
60 boost::optional<uint_fast64_t> stepBound;
61
62 std::unique_ptr<storm::modelchecker::SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>> instantiationChecker;
63
65 std::unique_ptr<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>> parameterLifter;
66 std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>> solverFactory;
67
68 // Results from the most recent solver call.
69 boost::optional<std::vector<uint_fast64_t>> minSchedChoices, maxSchedChoices;
70 boost::optional<std::vector<uint_fast64_t>> player1SchedChoices;
71 std::vector<ConstantType> x;
72 boost::optional<ConstantType> lowerResultBound, upperResultBound;
73 bool applyPreviousResultAsHint;
74};
75} // namespace modelchecker
76} // namespace storm
storm::storage::ParameterRegion< ParametricType >::VariableType VariableType
Class to efficiently check a formula on a parametric model with different parameter instantiations.
virtual void specifyReachabilityRewardFormula(Environment const &env, CheckTask< storm::logic::EventuallyFormula, ConstantType > const &checkTask) override
virtual storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType > & getInstantiationChecker() override
virtual void specify(Environment const &env, std::shared_ptr< storm::models::ModelBase > parametricModel, CheckTask< storm::logic::Formula, typename SparseModelType::ValueType > const &checkTask, bool generateRegionSplitEstimates=false, bool allowModelSimplification=true) override
virtual std::unique_ptr< CheckResult > computeQuantitativeValues(Environment const &env, storm::storage::ParameterRegion< typename SparseModelType::ValueType > const &region, storm::solver::OptimizationDirection const &dirForParameters, std::shared_ptr< storm::analysis::LocalMonotonicityResult< typename RegionModelChecker< typename SparseModelType::ValueType >::VariableType > > localMonotonicityResult=nullptr) override
boost::optional< storm::storage::Scheduler< ConstantType > > getCurrentMaxScheduler()
virtual void specifyUntilFormula(Environment const &env, CheckTask< storm::logic::UntilFormula, ConstantType > const &checkTask) override
boost::optional< storm::storage::Scheduler< ConstantType > > getCurrentMinScheduler()
virtual void specifyBoundedUntilFormula(const CheckTask< storm::logic::BoundedUntilFormula, ConstantType > &checkTask) override
virtual void specifyCumulativeRewardFormula(const CheckTask< storm::logic::CumulativeRewardFormula, ConstantType > &checkTask) override
boost::optional< storm::storage::Scheduler< ConstantType > > getCurrentPlayer1Scheduler()
virtual bool canHandle(std::shared_ptr< storm::models::ModelBase > parametricModel, CheckTask< storm::logic::Formula, typename SparseModelType::ValueType > const &checkTask) const override
void specify_internal(Environment const &env, std::shared_ptr< SparseModelType > parametricModel, CheckTask< storm::logic::Formula, typename SparseModelType::ValueType > const &checkTask, bool skipModelSimplification)
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
A class that holds a possibly non-square matrix in the compressed row storage format.
LabParser.cpp.
Definition cli.cpp:18