Browse Source

No DC propagation for failed toplevel

Former-commit-id: a2cf30e071
tempestpy_adaptions
Mavo 9 years ago
parent
commit
2c15c89751
  1. 12
      src/builder/ExplicitDFTModelBuilder.cpp

12
src/builder/ExplicitDFTModelBuilder.cpp

@ -212,21 +212,23 @@ namespace storm {
if(newState->isInvalid()) { if(newState->isInvalid()) {
continue; continue;
} }
while (!queues.failsafePropagationDone()) {
bool dftFailed = newState->hasFailed(mDft.getTopLevelIndex());
while (!dftFailed && !queues.failsafePropagationDone()) {
DFTGatePointer next = queues.nextFailsafePropagation(); DFTGatePointer next = queues.nextFailsafePropagation();
next->checkFailsafe(*newState, queues); next->checkFailsafe(*newState, queues);
} }
while (enableDC && !queues.dontCarePropagationDone()) {
while (!dftFailed && enableDC && !queues.dontCarePropagationDone()) {
DFTElementPointer next = queues.nextDontCarePropagation(); DFTElementPointer next = queues.nextDontCarePropagation();
next->checkDontCareAnymore(*newState, queues); next->checkDontCareAnymore(*newState, queues);
} }
// Update failable dependencies // Update failable dependencies
newState->updateFailableDependencies(nextBE->id());
if (!dftFailed) {
newState->updateFailableDependencies(nextBE->id());
}
bool dftFailed = newState->hasFailed(mDft.getTopLevelIndex());
uint_fast64_t newStateId; uint_fast64_t newStateId;
if(dftFailed && mergeFailedStates) { if(dftFailed && mergeFailedStates) {
newStateId = failedIndex; newStateId = failedIndex;

Loading…
Cancel
Save