diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 3b1d9954b..e455e2308 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -779,8 +779,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 result. return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); } diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 193f6a5a5..6cd7ca91f 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -402,6 +402,8 @@ namespace storm { std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); for (auto const& state : states) { + bool setValue = false; + STORM_LOG_ASSERT(nondeterministicChoiceIndices[state+1] - nondeterministicChoiceIndices[state] > 0, "Expected at least one action enabled in state " << state); for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool allSuccessorsInStates = true; for (auto const& element : transitionMatrix.getRow(choice)) { @@ -414,9 +416,11 @@ namespace storm { for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { scheduler.setChoice(choice - nondeterministicChoiceIndices[state], state, memState); } + setValue = true; break; } } + STORM_LOG_ASSERT(setValue, "Expected that at least one action for state " << state << " stays within the selected state"); } }