Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseCtmcInstantiationModelChecker.cpp
Go to the documentation of this file.
2
6
7namespace storm {
8namespace modelchecker {
9
10template<typename SparseModelType, typename ConstantType>
12 : SparseInstantiationModelChecker<SparseModelType, ConstantType>(parametricModel), modelInstantiator(parametricModel) {
13 // Intentionally left empty
14}
15
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);
22
23 return modelChecker.check(env, *this->currentCheckTask);
24}
25
28} // namespace modelchecker
29} // namespace storm
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
Class to efficiently check a formula on a parametric model with different parameter instantiations.
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
std::map< typename VariableType< FunctionType >::type, typename CoefficientType< FunctionType >::type > Valuation
Definition parametric.h:41
LabParser.cpp.
Definition cli.cpp:18