Browse Source

Fixed crucial bug marking all states as 'to expand'.

As a result no states were skipped during exploration and no approximation took place.
tempestpy_adaptions
Matthias Volk 6 years ago
parent
commit
6eb2795b68
  1. 2
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

2
src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@ -411,7 +411,7 @@ namespace storm {
} }
iter->second.second = heuristic; iter->second.second = heuristic;
if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->getFailableElements().hasDependencies() || (!state->getFailableElements().hasDependencies() && state->getFailableElements().hasBEs())) {
if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->getFailableElements().hasDependencies() || (!state->getFailableElements().hasDependencies() && !state->getFailableElements().hasBEs())) {
// Do not skip absorbing state or if reached by dependencies // Do not skip absorbing state or if reached by dependencies
iter->second.second->markExpand(); iter->second.second->markExpand();
} }

Loading…
Cancel
Save