diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 38a905999..aed36288c 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -13,6 +13,7 @@ #include "storm/utility/initialize.h" #include "storm-cli-utilities/cli.h" #include "storm-parsers/api/storm-parsers.h" +#include "storm-dft/transformations/DftTransformator.h" /*! @@ -29,6 +30,8 @@ void processOptions() { storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); auto const &debug = storm::settings::getModule(); + auto dftTransformator = storm::transformations::dft::DftTransformator(); + if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model given."); @@ -53,11 +56,8 @@ void processOptions() { storm::api::exportDFTToJsonFile(*dft, dftIOSettings.getExportJsonFilename()); } - if (dftIOSettings.isExportToSmt()) { - // Export to smtlib2 - storm::api::exportDFTToSMT(*dft, dftIOSettings.getExportSmtFilename(), debug.isTestSet()); - return; - } + // Eliminate non-binary dependencies + dft = dftTransformator.transformBinaryFDEPs(*dft); // Check well-formedness of DFT std::stringstream stream; @@ -79,6 +79,12 @@ void processOptions() { return; } + // SMT + if (dftIOSettings.isExportToSmt()) { + // Export to smtlib2 + storm::api::exportDFTToSMT(*dft, dftIOSettings.getExportSmtFilename(), debug.isTestSet()); + return; + } #ifdef STORM_HAVE_Z3 if (faultTreeSettings.solveWithSMT()) { diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index 9bb40a8b6..c02fb3364 100644 --- a/src/storm-dft/builder/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -77,7 +77,6 @@ namespace storm { childElement->addOutgoingDependency(elem.first); } } - STORM_LOG_ASSERT(!binaryDependencies || dependencies.size() == 1, "Dependency '" << elem.first->name() << "' should only have one dependent element."); for (auto& be : dependencies) { elem.first->addDependentEvent(be); be->addIngoingDependency(elem.first); diff --git a/src/storm-dft/builder/DFTBuilder.h b/src/storm-dft/builder/DFTBuilder.h index 9ce85db0f..31764e2b8 100644 --- a/src/storm-dft/builder/DFTBuilder.h +++ b/src/storm-dft/builder/DFTBuilder.h @@ -43,7 +43,8 @@ namespace storm { std::unordered_map mLayoutInfo; public: - DFTBuilder(bool defaultInclusive = true, bool binaryDependencies = true) : pandDefaultInclusive(defaultInclusive), porDefaultInclusive(defaultInclusive), binaryDependencies(binaryDependencies) { + DFTBuilder(bool defaultInclusive = true) : pandDefaultInclusive(defaultInclusive), + porDefaultInclusive(defaultInclusive) { } @@ -107,41 +108,13 @@ namespace storm { std::string trigger = children[0]; //TODO: collect constraints for SMT solving - //0 <= probability <= 1 - if (binaryDependencies && !storm::utility::isOne(probability) && children.size() > 2) { - // Introduce additional element for first capturing the probabilistic dependency - std::string nameAdditional = name + "_additional"; - addBasicElementConst(nameAdditional, false); - // First consider probabilistic dependency - addDepElement(name + "_pdep", {children.front(), nameAdditional}, probability); - // Then consider dependencies to the children if probabilistic dependency failed - std::vector newChildren = children; - newChildren[0] = nameAdditional; - addDepElement(name, newChildren, storm::utility::one()); - return true; - } else { - // Add dependencies - if(binaryDependencies) { - for (size_t i = 1; i < children.size(); ++i) { - std::string nameDep = name + "_" + std::to_string(i); - if (nameInUse(nameDep)) { - STORM_LOG_ERROR("Element with name '" << name << "' already exists."); - return false; - } - STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, "PDep with multiple children supported."); - DFTDependencyPointer element = std::make_shared>(mNextId++, nameDep, probability); - mElements[element->name()] = element; - mDependencyChildNames[element] = {trigger, children[i]}; - mDependencies.push_back(element); - } - } else { - DFTDependencyPointer element = std::make_shared>(mNextId++, name, probability); - mElements[element->name()] = element; - mDependencyChildNames[element] = children; - mDependencies.push_back(element); - } - return true; - } + DFTDependencyPointer element = std::make_shared>(mNextId++, + name, + probability); + mElements[element->name()] = element; + mDependencyChildNames[element] = children; + mDependencies.push_back(element); + return true; } bool addVotElement(std::string const& name, unsigned threshold, std::vector const& children) { @@ -268,8 +241,6 @@ namespace storm { bool pandDefaultInclusive; // If true, the standard gate adders make a pand inclusive, and exclusive otherwise. bool porDefaultInclusive; - - bool binaryDependencies; }; } diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index 8d44637f9..0062abce6 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -32,8 +32,9 @@ namespace storm { } template - storm::storage::DFT DFTGalileoParser::parseDFT(const std::string& filename, bool defaultInclusive, bool binaryDependencies) { - storm::builder::DFTBuilder builder(defaultInclusive, binaryDependencies); + storm::storage::DFT + DFTGalileoParser::parseDFT(const std::string &filename, bool defaultInclusive) { + storm::builder::DFTBuilder builder(defaultInclusive); ValueParser valueParser; // Regular expression to detect comments // taken from: https://stackoverflow.com/questions/9449887/removing-c-c-style-comments-using-boostregex diff --git a/src/storm-dft/parser/DFTGalileoParser.h b/src/storm-dft/parser/DFTGalileoParser.h index 0c280fd88..f5f259f5f 100644 --- a/src/storm-dft/parser/DFTGalileoParser.h +++ b/src/storm-dft/parser/DFTGalileoParser.h @@ -26,11 +26,10 @@ namespace storm { * * @param filename File. * @param defaultInclusive Flag indicating if priority gates are inclusive by default. - * @param binaryDependencies Flag indicating if dependencies should be converted to binary dependencies. * * @return DFT. */ - static storm::storage::DFT parseDFT(std::string const& filename, bool defaultInclusive = true, bool binaryDependencies = true); + static storm::storage::DFT parseDFT(std::string const &filename, bool defaultInclusive = true); private: /*! diff --git a/src/storm-dft/transformations/DftTransformator.cpp b/src/storm-dft/transformations/DftTransformator.cpp index d70c15ec0..a6ba46f17 100644 --- a/src/storm-dft/transformations/DftTransformator.cpp +++ b/src/storm-dft/transformations/DftTransformator.cpp @@ -5,16 +5,18 @@ namespace storm { namespace transformations { namespace dft { template - DftTransformator::DftTransformator(storm::storage::DFT const &dft) : mDft(dft) {} + DftTransformator::DftTransformator() { + } template - storm::storage::DFT DftTransformator::transformUniqueFailedBe() { - storm::builder::DFTBuilder builder = storm::builder::DFTBuilder(true, false); + std::shared_ptr> + DftTransformator::transformUniqueFailedBe(storm::storage::DFT const &dft) { + storm::builder::DFTBuilder builder = storm::builder::DFTBuilder(true); // NOTE: if probabilities for constant BEs are introduced, change this to vector of tuples (name, prob) std::vector failedBEs; - for (size_t i = 0; i < mDft.nrElements(); ++i) { - std::shared_ptr const> element = mDft.getElement(i); + for (size_t i = 0; i < dft.nrElements(); ++i) { + std::shared_ptr const> element = dft.getElement(i); switch (element->type()) { case storm::storage::DFTElementType::BE_EXP: { STORM_LOG_DEBUG("Transform " + element->name() + " [BE (exp)]"); @@ -75,13 +77,17 @@ namespace storm { } else { STORM_LOG_DEBUG("Transform " + element->name() + " [PDEP]"); } - builder.addDepElement(dep->name(), getChildrenVector(element), dep->probability()); + builder.addDepElement(dep->name(), getChildrenVector(dep), dep->probability()); break; } case storm::storage::DFTElementType::SEQ: STORM_LOG_DEBUG("Transform " + element->name() + " [SEQ]"); builder.addSequenceEnforcer(element->name(), getChildrenVector(element)); break; + case storm::storage::DFTElementType::MUTEX: + STORM_LOG_DEBUG("Transform " + element->name() + " [MUTEX]"); + builder.addMutex(element->name(), getChildrenVector(element)); + break; default: STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "DFT type '" << element->type() << "' not known."); @@ -96,10 +102,135 @@ namespace storm { builder.addDepElement("Failure_Trigger", failedBEs, storm::utility::one()); } - builder.setTopLevel(mDft.getTopLevelGate()->name()); + builder.setTopLevel(dft.getTopLevelGate()->name()); + + STORM_LOG_DEBUG("Transformation complete!"); + return std::make_shared>(builder.build()); + } + + template + std::shared_ptr> + DftTransformator::transformBinaryFDEPs(storm::storage::DFT const &dft) { + storm::builder::DFTBuilder builder = storm::builder::DFTBuilder(true); + + for (size_t i = 0; i < dft.nrElements(); ++i) { + std::shared_ptr const> element = dft.getElement(i); + switch (element->type()) { + case storm::storage::DFTElementType::BE_EXP: { + STORM_LOG_DEBUG("Transform " + element->name() + " [BE (exp)]"); + auto be_exp = std::static_pointer_cast const>( + element); + builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(), + be_exp->dormancyFactor()); + break; + } + case storm::storage::DFTElementType::BE_CONST: { + auto be_const = std::static_pointer_cast const>( + element); + STORM_LOG_DEBUG("Transform " + element->name() + " [BE (const)]"); + // All original constant BEs are set to failsafe, failed BEs are later triggered by a new element + builder.addBasicElementConst(be_const->name(), be_const->canFail()); + break; + } + case storm::storage::DFTElementType::AND: + STORM_LOG_DEBUG("Transform " + element->name() + " [AND]"); + builder.addAndElement(element->name(), getChildrenVector(element)); + break; + case storm::storage::DFTElementType::OR: + STORM_LOG_DEBUG("Transform " + element->name() + " [OR]"); + builder.addOrElement(element->name(), getChildrenVector(element)); + break; + case storm::storage::DFTElementType::VOT: { + STORM_LOG_DEBUG("Transform " + element->name() + " [VOT]"); + auto vot = std::static_pointer_cast const>(element); + builder.addVotElement(vot->name(), vot->threshold(), getChildrenVector(vot)); + break; + } + case storm::storage::DFTElementType::PAND: { + STORM_LOG_DEBUG("Transform " + element->name() + " [PAND]"); + auto pand = std::static_pointer_cast const>(element); + builder.addPandElement(pand->name(), getChildrenVector(pand), pand->isInclusive()); + break; + } + case storm::storage::DFTElementType::POR: { + STORM_LOG_DEBUG("Transform " + element->name() + " [POR]"); + auto por = std::static_pointer_cast const>(element); + builder.addPandElement(por->name(), getChildrenVector(por), por->isInclusive()); + break; + } + case storm::storage::DFTElementType::SPARE: + STORM_LOG_DEBUG("Transform " + element->name() + " [SPARE]"); + builder.addSpareElement(element->name(), getChildrenVector(element)); + break; + case storm::storage::DFTElementType::PDEP: { + auto dep = std::static_pointer_cast const>( + element); + auto children = getChildrenVector(dep); + if (!storm::utility::isOne(dep->probability())) { + STORM_LOG_DEBUG("Transform " + element->name() + " [PDEP]"); + if (children.size() > 2) { + // Introduce additional element for first capturing the probabilistic dependency + std::string nameAdditional = dep->name() + "_additional"; + builder.addBasicElementConst(nameAdditional, false); + // First consider probabilistic dependency + builder.addDepElement(dep->name() + "_pdep", {children.front(), nameAdditional}, + dep->probability()); + // Then consider dependencies to the children if probabilistic dependency failed + children.erase(children.begin()); + size_t i = 1; + for (auto const &child : children) { + std::string nameDep = dep->name() + "_" + std::to_string(i); + if (builder.nameInUse(nameDep)) { + STORM_LOG_ERROR("Element with name '" << nameDep << "' already exists."); + } + builder.addDepElement(nameDep, {dep->name() + "_additional", child}, + storm::utility::one()); + ++i; + } + } else { + builder.addDepElement(dep->name(), children, dep->probability()); + } + } else { + STORM_LOG_DEBUG("Transform " + element->name() + " [FDEP]"); + // Add dependencies + for (size_t i = 1; i < children.size(); ++i) { + std::string nameDep; + if (children.size() == 2) { + nameDep = dep->name(); + } else { + nameDep = dep->name() + "_" + std::to_string(i); + } + if (builder.nameInUse(nameDep)) { + STORM_LOG_ERROR("Element with name '" << nameDep << "' already exists."); + } + STORM_LOG_ASSERT(storm::utility::isOne(dep->probability()) || children.size() == 2, + "PDEP with multiple children supported."); + builder.addDepElement(nameDep, {children[0], children[i]}, + storm::utility::one()); + } + } + break; + } + case storm::storage::DFTElementType::SEQ: + STORM_LOG_DEBUG("Transform " + element->name() + " [SEQ]"); + builder.addSequenceEnforcer(element->name(), getChildrenVector(element)); + break; + case storm::storage::DFTElementType::MUTEX: + STORM_LOG_DEBUG("Transform " + element->name() + " [MUTEX]"); + builder.addMutex(element->name(), getChildrenVector(element)); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, + "DFT type '" << element->type() << "' not known."); + break; + } + + } + + builder.setTopLevel(dft.getTopLevelGate()->name()); STORM_LOG_DEBUG("Transformation complete!"); - return builder.build(); + return std::make_shared>(builder.build()); } template diff --git a/src/storm-dft/transformations/DftTransformator.h b/src/storm-dft/transformations/DftTransformator.h index 39dfa6acf..c8e832f1b 100644 --- a/src/storm-dft/transformations/DftTransformator.h +++ b/src/storm-dft/transformations/DftTransformator.h @@ -18,15 +18,17 @@ namespace storm { * * @param dft DFT */ - DftTransformator(storm::storage::DFT const &dft); + DftTransformator(); - storm::storage::DFT transformUniqueFailedBe(); + std::shared_ptr> + transformUniqueFailedBe(storm::storage::DFT const &dft); + + std::shared_ptr> + transformBinaryFDEPs(storm::storage::DFT const &dft); private: std::vector getChildrenVector(std::shared_ptr const> element); - - storm::storage::DFT const &mDft; }; } } diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 96f9263c6..bb37c29c7 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -2,6 +2,7 @@ #include "storm-config.h" #include "storm-dft/api/storm-dft.h" +#include "storm-dft/transformations/DftTransformator.h" #include "storm-parsers/api/storm-parsers.h" namespace { @@ -73,7 +74,9 @@ namespace { } double analyzeMTTF(std::string const& file) { - std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); + storm::transformations::dft::DftTransformator dftTransformator = storm::transformations::dft::DftTransformator(); + std::shared_ptr> dft = dftTransformator.transformBinaryFDEPs( + *(storm::api::loadDFTGalileoFile(file))); EXPECT_TRUE(storm::api::isWellFormed(*dft)); std::string property = "Tmin=? [F \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); @@ -87,7 +90,9 @@ namespace { } double analyzeReliability(std::string const &file, double bound) { - std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); + storm::transformations::dft::DftTransformator dftTransformator = storm::transformations::dft::DftTransformator(); + std::shared_ptr> dft = dftTransformator.transformBinaryFDEPs( + *(storm::api::loadDFTGalileoFile(file))); EXPECT_TRUE(storm::api::isWellFormed(*dft)); std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(