sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Started on support for constant failed/failsafe BEs

tempestpy_adaptions
Matthias Volk 6 years ago
parent
1f5d3b9479
commit
3183a141d6
5 changed files with 62 additions and 16 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      src/storm-dft/builder/DFTBuilder.cpp
  2. 37
      src/storm-dft/builder/DFTBuilder.h
  3. 13
      src/storm-dft/parser/DFTGalileoParser.cpp
  4. 3
      src/storm-dft/parser/DFTJsonParser.cpp
  5. 17
      src/storm-dft/storage/dft/elements/DFTConst.h

8
src/storm-dft/builder/DFTBuilder.cpp
View File

@ -273,14 +273,16 @@ namespace storm {
case storm::storage::DFTElementType::BE:
{
std::shared_ptr<storm::storage::DFTBE<ValueType>> be = std::static_pointer_cast<storm::storage::DFTBE<ValueType>>(element);
addBasicElement(be->name(), be->activeFailureRate(), be->dormancyFactor(), be->isTransient());
addBasicElementExponential(be->name(), be->activeFailureRate(), be->dormancyFactor(), be->isTransient());
break;
}
case storm::storage::DFTElementType::CONSTF:
case storm::storage::DFTElementType::CONSTS:
// TODO
STORM_LOG_ASSERT(false, "Const elements not supported.");
{
std::shared_ptr<storm::storage::DFTConst<ValueType>> be = std::static_pointer_cast<storm::storage::DFTConst<ValueType>>(element);
addBasicElementConst(be->name(), be->failed());
break;
}
case storm::storage::DFTElementType::PDEP:
{
DFTDependencyPointer dependency = std::static_pointer_cast<storm::storage::DFTDependency<ValueType>>(element);

37
src/storm-dft/builder/DFTBuilder.h
View File

@ -8,6 +8,8 @@
#include "storm-dft/storage/dft/DFTElements.h"
#include "storm-dft/storage/dft/elements/DFTRestriction.h"
#include "storm-dft/storage/dft/DFTLayoutInfo.h"
#include "storm/exceptions/NotSupportedException.h"
namespace storm {
namespace storage {
@ -109,7 +111,7 @@ namespace storm {
if (binaryDependencies && !storm::utility::isOne(probability) && children.size() > 2) {
// Introduce additional element for first capturing the probabilistic dependency
std::string nameAdditional = name + "_additional";
addBasicElement(nameAdditional, storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>(), false);
addBasicElementConst(nameAdditional, false);
// First consider probabilistic dependency
addDepElement(name + "_pdep", {children.front(), nameAdditional}, probability);
// Then consider dependencies to the children if probabilistic dependency failed
@ -167,15 +169,42 @@ namespace storm {
mChildNames[element] = children;
return true;
}
bool addBasicElement(std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) {
bool addBasicElementConst(std::string const& name, bool failed) {
if (nameInUse(name)) {
STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
return false;
}
mElements[name] = std::make_shared<storm::storage::DFTConst<ValueType>>(mNextId++, name, failed);
return true;
}
bool addBasicElementProbability(std::string const& name, ValueType probability, ValueType dormancyFactor, bool transient = false) {
//0 <= dormancyFactor <= 1
if (nameInUse(name)) {
STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
return false;
}
if (storm::utility::isZero<ValueType>(probability)) {
return addBasicElementConst(name, false);
} else if (storm::utility::isOne<ValueType>(probability)) {
return addBasicElementConst(name, true);
}
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Constant probability distribution is not supported for basic element '" << name << "'.");
return false;
}
bool addBasicElementExponential(std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) {
//TODO Matthias: collect constraints for SMT solving
//failureRate > 0
//0 <= dormancyFactor <= 1
if (nameInUse(name)) {
STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
return false;
}
if (storm::utility::isZero<ValueType>(failureRate)) {
return addBasicElementConst(name, false);
}
mElements[name] = std::make_shared<storm::storage::DFTBE<ValueType>>(mNextId++, name, failureRate, dormancyFactor, transient);
return true;
}

13
src/storm-dft/parser/DFTGalileoParser.cpp
View File

@ -297,26 +297,29 @@ namespace storm {
switch (distribution) {
case Constant:
if (storm::utility::isZero(firstValDistribution) || storm::utility::isOne(firstValDistribution)) {
return builder.addBasicElementProbability(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
}
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Constant distribution is not supported for basic element '" << name << "' in line " << lineNo << ".");
break;
case Exponential:
return builder.addBasicElement(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
return builder.addBasicElementExponential(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
break;
case Erlang:
if (erlangPhases == 1) {
// Erlang distribution reduces to exponential distribution
return builder.addBasicElement(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
return builder.addBasicElementExponential(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
} else {
// Model Erlang distribution by using SEQ over BEs instead.
// For each phase a BE is added, then the SEQ ensures the ordered failure.
STORM_LOG_WARN("Erlang distribution for basic element '" << name << "' in line " << lineNo << " is modelled by SEQ gate and BEs.");
std::string origName = parseName(name);
std::vector<std::string> childNames;
bool success = builder.addBasicElement(origName, firstValDistribution, dormancyFactor, false); // TODO set transient BEs
bool success = builder.addBasicElementExponential(origName, firstValDistribution, dormancyFactor, false); // TODO set transient BEs
for (size_t i = 0; i < erlangPhases - 1; ++i) {
std::string beName = origName + "_" + std::to_string(i);
childNames.push_back(beName);
success = success && builder.addBasicElement(beName, firstValDistribution, dormancyFactor, false); // TODO set transient BEs
success = success && builder.addBasicElementExponential(beName, firstValDistribution, dormancyFactor, false); // TODO set transient BEs
}
childNames.push_back(origName);
return success && builder.addSequenceEnforcer(origName + "_seq", childNames);
@ -325,7 +328,7 @@ namespace storm {
case Weibull:
if (storm::utility::isOne<ValueType>(secondValDistribution)) {
// Weibull distribution reduces to exponential distribution
return builder.addBasicElement(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
return builder.addBasicElementExponential(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Weibull distribution is not supported for basic element '" << name << "' in line " << lineNo << ".");
}

3
src/storm-dft/parser/DFTJsonParser.cpp
View File

@ -93,13 +93,14 @@ namespace storm {
ValueType probability = parseRationalExpression(parseJsonNumber(data.at("probability")));
success = builder.addDepElement(name, childNames, probability);
} else if (type == "be") {
// TODO support different distributions
ValueType failureRate = parseRationalExpression(parseJsonNumber(data.at("rate")));
ValueType dormancyFactor = parseRationalExpression(parseJsonNumber(data.at("dorm")));
bool transient = false;
if (data.count("transient") > 0) {
transient = data.at("transient");
}
success = builder.addBasicElement(name, failureRate, dormancyFactor, transient);
success = builder.addBasicElementExponential(name, failureRate, dormancyFactor, transient);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << type << " not recognized.");
success = false;

17
src/storm-dft/storage/dft/elements/DFTConst.h
View File

@ -27,15 +27,20 @@ namespace storm {
return mFailed;
}
virtual bool isConstant() const {
virtual bool isConstant() const override {
return true;
}
virtual size_t nrChildren() const override {
return 0;
}
std::string toString() const override {
std::stringstream stream;
stream << *this;
return stream.str();
}
bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
DFTConst<ValueType> const& otherCNST = static_cast<DFTConst<ValueType> const&>(other);
@ -43,5 +48,11 @@ namespace storm {
}
};
template<typename ValueType>
inline std::ostream& operator<<(std::ostream& os, DFTConst<ValueType> const& be) {
return os << "{" << be.name() << "} BE(const " << (be.failed() ? "failed" : "failsafe") << ")";
}
}
}
Write Preview
Loading…
Cancel
Save