8namespace modelchecker {
10template<
typename SparseModelType,
typename ConstantType>
16template<
typename SparseModelType,
typename ConstantType>
19 STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException,
"Checking has been invoked but no property has been specified before.");
20 auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
23 return modelChecker.
check(env, *this->currentCheckTask);
virtual std::unique_ptr< CheckResult > check(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
Checks the provided formula.
Class to efficiently check a formula on a parametric model with different parameter instantiations.
virtual std::unique_ptr< CheckResult > check(Environment const &env, storm::utility::parametric::Valuation< typename SparseModelType::ValueType > const &valuation) override
SparseCtmcInstantiationModelChecker(SparseModelType const ¶metricModel)
Class to efficiently check a formula on a parametric model with different parameter instantiations.
#define STORM_LOG_THROW(cond, exception, message)
std::map< typename VariableType< FunctionType >::type, typename CoefficientType< FunctionType >::type > Valuation