Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ValidatingSparseParameterLiftingModelChecker.h
Go to the documentation of this file.
1#pragma once
2
7
8namespace storm {
9namespace modelchecker {
10
11template<typename SparseModelType, typename ImpreciseType, typename PreciseType>
12class ValidatingSparseParameterLiftingModelChecker : public RegionModelChecker<typename SparseModelType::ValueType> {
13 static_assert(storm::NumberTraits<PreciseType>::IsExact, "Specified type for exact computations is not exact.");
14
15 public:
18
19 virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel,
21
30 bool sampleVerticesOfRegion = false,
32 localMonotonicityResult = nullptr) override;
33
34 protected:
39
40 virtual void applyHintsToPreciseChecker() = 0;
41
42 private:
43 // Information for statistics
44 uint_fast64_t numOfWrongRegions;
45};
46} // namespace modelchecker
47} // namespace storm
storm::storage::ParameterRegion< ParametricType >::VariableType VariableType
Class to approximatively check a formula on a parametric model for all parameter valuations within a ...
virtual RegionResult analyzeRegion(Environment const &env, storm::storage::ParameterRegion< typename SparseModelType::ValueType > const &region, RegionResultHypothesis const &hypothesis=RegionResultHypothesis::Unknown, RegionResult const &initialResult=RegionResult::Unknown, bool sampleVerticesOfRegion=false, std::shared_ptr< storm::analysis::LocalMonotonicityResult< typename RegionModelChecker< typename SparseModelType::ValueType >::VariableType > > localMonotonicityResult=nullptr) override
Analyzes the given region by means of parameter lifting.
virtual SparseParameterLiftingModelChecker< SparseModelType, ImpreciseType > const & getImpreciseChecker() const =0
virtual SparseParameterLiftingModelChecker< SparseModelType, ImpreciseType > & getImpreciseChecker()=0
virtual SparseParameterLiftingModelChecker< SparseModelType, PreciseType > const & getPreciseChecker() const =0
virtual SparseParameterLiftingModelChecker< SparseModelType, PreciseType > & getPreciseChecker()=0
virtual bool canHandle(std::shared_ptr< storm::models::ModelBase > parametricModel, CheckTask< storm::logic::Formula, typename SparseModelType::ValueType > const &checkTask) const override
RegionResult
The results for a single Parameter Region.
@ Unknown
the result is unknown
RegionResultHypothesis
hypothesis for the result for a single Parameter Region
LabParser.cpp.
Definition cli.cpp:18