diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index 9ac504d7c..d6d4969d4 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -39,7 +39,7 @@ namespace storm { namespace api { - + template storm::modelchecker::CheckTask createTask(std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { return storm::modelchecker::CheckTask(*formula, onlyInitialStatesRelevant); @@ -53,7 +53,7 @@ namespace storm { AbstractionRefinementOptions(std::vector&& constraints, std::vector>&& injectedRefinementPredicates) : constraints(std::move(constraints)), injectedRefinementPredicates(std::move(injectedRefinementPredicates)) { // Intentionally left empty. } - + std::vector constraints; std::vector> injectedRefinementPredicates; }; @@ -228,13 +228,13 @@ namespace storm { template typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr> const& ma, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; - + // Close the MA, if it is not already closed. if (!ma->isClosed()) { STORM_LOG_WARN("Closing Markov automaton. Consider closing the MA before verification."); ma->close(); } - + storm::modelchecker::SparseMarkovAutomatonCslModelChecker> modelchecker(*ma); if (modelchecker.canHandle(task)) { result = modelchecker.check(env, task); @@ -299,7 +299,7 @@ namespace storm { Environment env; return verifyWithSparseEngine(env, model, task); } - + template std::unique_ptr computeSteadyStateDistributionWithSparseEngine(storm::Environment const& env, std::shared_ptr> const& dtmc) { std::unique_ptr result; @@ -326,7 +326,7 @@ namespace storm { } return result; } - + // // Verifying with Hybrid engine // @@ -485,6 +485,6 @@ namespace storm { Environment env; return verifyWithDdEngine(env, model, task); } - + } }