diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index 0062abce6..1c97653af 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -302,6 +302,24 @@ namespace storm { case Constant: if (storm::utility::isZero(firstValDistribution) || storm::utility::isOne(firstValDistribution)) { return builder.addBasicElementProbability(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs + } else { + // Model constant BEs with probability 0 < p < 1 + bool success = true; + if (!builder.nameInUse("constantBeTrigger")) { + // Use a unique constantly failed element that triggers failsafe elements probabilistically + success = success && builder.addBasicElementProbability("constantBeTrigger", + storm::utility::one(), + storm::utility::one(), + false); + } + std::vector childNames; + childNames.push_back("constantBeTrigger"); + success = success && + builder.addBasicElementProbability(parseName(name), storm::utility::zero(), + storm::utility::one(), false); + childNames.push_back(parseName(name)); + return success && + builder.addDepElement(parseName(name) + "_pdep", childNames, firstValDistribution); } STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Constant distribution is not supported for basic element '" << name << "' in line " << lineNo << "."); break;