Browse Source

refined error message wrt unexpected type of scheduler

tempestpy_adaptions
Sebastian Junges 6 years ago
parent
commit
9a0794fca1
  1. 6
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

6
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@ -1277,7 +1277,11 @@ namespace storm {
} }
// Sanity check for created scheduler. // 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<ValueType>(std::move(result), std::move(scheduler)); return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(scheduler));
} }

Loading…
Cancel
Save