Browse Source

Fixed missing break in case distinction

tempestpy_adaptions
Matthias Volk 7 years ago
parent
commit
623ce0ccf1
  1. 1
      src/storm-dft/modelchecker/dft/DFTASFChecker.cpp

1
src/storm-dft/modelchecker/dft/DFTASFChecker.cpp

@ -388,6 +388,7 @@ namespace storm {
std::shared_ptr<DFTConstraint> elseC = std::make_shared<IsConstantValue>(timePointVariables.at(i), notFailed); std::shared_ptr<DFTConstraint> elseC = std::make_shared<IsConstantValue>(timePointVariables.at(i), notFailed);
constraints.push_back(std::make_shared<IfThenElse>(ifC, thenC, elseC)); constraints.push_back(std::make_shared<IfThenElse>(ifC, thenC, elseC));
constraints.back()->setDescription("PAND gate"); constraints.back()->setDescription("PAND gate");
break;
} }
case storm::storage::DFTElementType::SEQ: case storm::storage::DFTElementType::SEQ:
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "SMT encoding of SEQs is not implemented yet."); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "SMT encoding of SEQs is not implemented yet.");

Loading…
Cancel
Save