From b3987b178cf757083a6601375b055d062804bdc2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 26 Oct 2018 16:09:27 +0200 Subject: [PATCH] Explicit model builder: Give an error if no initial state is found. --- src/storm/builder/ExplicitModelBuilder.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 6711c79f2..71a2681de 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -130,7 +130,8 @@ namespace storm { // Let the generator create all initial states. this->stateStorage.initialStateIndices = generator->getInitialStates(stateToIdCallback); - + STORM_LOG_THROW(!this->stateStorage.initialStateIndices.empty(), storm::exceptions::WrongFormatException, "The model does not have a single initial state."); + // Now explore the current state until there is no more reachable state. uint_fast64_t currentRowGroup = 0; uint_fast64_t currentRow = 0;