Browse Source

Explicit model builder: Give an error if no initial state is found.

tempestpy_adaptions
TimQu 6 years ago
parent
commit
b3987b178c
  1. 3
      src/storm/builder/ExplicitModelBuilder.cpp

3
src/storm/builder/ExplicitModelBuilder.cpp

@ -130,7 +130,8 @@ namespace storm {
// Let the generator create all initial states. // Let the generator create all initial states.
this->stateStorage.initialStateIndices = generator->getInitialStates(stateToIdCallback); 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. // Now explore the current state until there is no more reachable state.
uint_fast64_t currentRowGroup = 0; uint_fast64_t currentRowGroup = 0;
uint_fast64_t currentRow = 0; uint_fast64_t currentRow = 0;

Loading…
Cancel
Save