Browse Source

Failed spares set use index to own id

Former-commit-id: e4da5bd5d8
tempestpy_adaptions
Mavo 9 years ago
parent
commit
2e8460548b
  1. 4
      src/storage/dft/DFT.cpp
  2. 4
      src/storage/dft/DFTElements.h

4
src/storage/dft/DFT.cpp

@ -263,7 +263,7 @@ namespace storm {
stream << "\t** " << storm::storage::toChar(state->getElementState(elem->id())); stream << "\t** " << storm::storage::toChar(state->getElementState(elem->id()));
if(elem->isSpareGate()) { if(elem->isSpareGate()) {
size_t useId = state->uses(elem->id()); size_t useId = state->uses(elem->id());
if(state->isActive(useId)) {
if(useId == elem->id() || state->isActive(useId)) {
stream << "actively "; stream << "actively ";
} }
stream << "using " << useId; stream << "using " << useId;
@ -287,7 +287,7 @@ namespace storm {
if(elem->isSpareGate()) { if(elem->isSpareGate()) {
stream << "["; stream << "[";
size_t useId = state->uses(elem->id()); size_t useId = state->uses(elem->id());
if(state->isActive(useId)) {
if(useId == elem->id() || state->isActive(useId)) {
stream << "actively "; stream << "actively ";
} }
stream << "using " << useId << "]"; stream << "using " << useId << "]";

4
src/storage/dft/DFTElements.h

@ -412,12 +412,12 @@ namespace storm {
} }
/** /**
* Finish failed/failsafe spare gate by activating the children and setting the useIndex to zero.
* Finish failed/failsafe spare gate by activating the children and setting the useIndex to the spare id.
* This prevents multiple fail states with different usages or activations. * This prevents multiple fail states with different usages or activations.
* @param state The current state. * @param state The current state.
*/ */
void finalizeSpare(DFTState<ValueType>& state) const { void finalizeSpare(DFTState<ValueType>& state) const {
state.setUses(this->mId, 0);
state.setUses(this->mId, this->mId);
for (auto child : this->children()) { for (auto child : this->children()) {
if (!state.isActive(child->id())) { if (!state.isActive(child->id())) {
state.activate(child->id()); state.activate(child->id());

Loading…
Cancel
Save