9namespace modelchecker {
11template<
typename SparseModelType,
typename ImpreciseType,
typename PreciseType>
19 virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel,
30 bool sampleVerticesOfRegion =
false,
32 localMonotonicityResult =
nullptr)
override;
44 uint_fast64_t numOfWrongRegions;
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 ®ion, 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 ~ValidatingSparseParameterLiftingModelChecker()
virtual SparseParameterLiftingModelChecker< SparseModelType, ImpreciseType > & getImpreciseChecker()=0
virtual SparseParameterLiftingModelChecker< SparseModelType, PreciseType > const & getPreciseChecker() const =0
virtual SparseParameterLiftingModelChecker< SparseModelType, PreciseType > & getPreciseChecker()=0
ValidatingSparseParameterLiftingModelChecker()
virtual void applyHintsToPreciseChecker()=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