diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 8c7b93738..eb90df88d 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -1277,7 +1277,11 @@ namespace storm { } // Sanity check for created scheduler. - STORM_LOG_ASSERT((!produceScheduler && !scheduler) || (!scheduler->isPartialScheduler() && scheduler->isDeterministicScheduler() && scheduler->isMemorylessScheduler()), "Unexpected format of obtained scheduler."); + STORM_LOG_ASSERT(!produceScheduler || scheduler, "Expected that a scheduler was obtained."); + STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(), "Expected a fully defined scheduler"); + STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isDeterministicScheduler(), "Expected a deterministic scheduler"); + STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler"); + return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); }