diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 871502586..38a905999 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -27,6 +27,7 @@ void processOptions() { storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule(); storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule(); storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); + auto const &debug = storm::settings::getModule(); if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) { @@ -53,8 +54,8 @@ void processOptions() { } if (dftIOSettings.isExportToSmt()) { - // Export to json - storm::api::exportDFTToSMT(*dft, dftIOSettings.getExportSmtFilename()); + // Export to smtlib2 + storm::api::exportDFTToSMT(*dft, dftIOSettings.getExportSmtFilename(), debug.isTestSet()); return; } @@ -81,7 +82,6 @@ void processOptions() { #ifdef STORM_HAVE_Z3 if (faultTreeSettings.solveWithSMT()) { - auto const& debug = storm::settings::getModule(); // Solve with SMT STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); storm::api::analyzeDFTSMT(*dft, true, debug.isTestSet()); diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index ed20e5c69..2cb36853f 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -31,14 +31,18 @@ namespace storm { } template<> - void exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file) { + void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file, bool experimentalMode) { storm::modelchecker::DFTASFChecker asfChecker(dft); + if (experimentalMode) { + asfChecker.activateExperimentalMode(); + } asfChecker.convert(); asfChecker.toFile(file); } template<> - void exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file) { + void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file, + bool experimentalMode) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to SMT does not support this data type."); } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index fcaab98b1..2af6a43e1 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -134,7 +134,7 @@ namespace storm { * @param file File. */ template - void exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file); + void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file, bool experimentalMode); /*! * Transform DFT to GSPN. diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 4ea6ba0aa..f6c955d56 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -29,6 +29,8 @@ namespace storm { void DFTASFChecker::convert() { std::vector beVariables; + std::vector failedBeVariables; + std::vector failsafeBeVariables; notFailed = dft.nrBasicElements() + 1; // Value indicating the element is not failed // Initialize variables @@ -40,11 +42,19 @@ namespace storm { case storm::storage::DFTElementType::BE_EXP: beVariables.push_back(varNames.size() - 1); break; - case storm::storage::DFTElementType::BE_CONST: + case storm::storage::DFTElementType::BE_CONST: { STORM_LOG_THROW(experimentalMode, storm::exceptions::NotSupportedException, "Constant BEs are not supported in SMT translation."); STORM_LOG_WARN("Constant BEs are only experimentally supported"); + // Constant BEs are initially either failed or failsafe, treat them differently + auto be = std::static_pointer_cast const>(element); + if (be->failed()) { + failedBeVariables.push_back(varNames.size() - 1); + } else { + failsafeBeVariables.push_back(varNames.size() - 1); + } break; + } case storm::storage::DFTElementType::SPARE: { auto spare = std::static_pointer_cast const>(element); @@ -73,13 +83,29 @@ namespace storm { // Generate constraints - // All BEs have to fail (first part of constraint 12) + // All exponential BEs have to fail (first part of constraint 12) for (auto const &beV : beVariables) { constraints.push_back(std::make_shared(beV, 1, dft.nrBasicElements())); } + // Constantly failsafe BEs may also be fail-safe + for (auto const &beV : failsafeBeVariables) { + constraints.push_back(std::make_shared(beV, 1, notFailed)); + } + + // Constantly failed BEs fail before other types + for (auto const &beV : failedBeVariables) { + constraints.push_back(std::make_shared(beV, 1, failedBeVariables.size())); + } + + std::vector allBeVariables; + allBeVariables.insert(std::end(allBeVariables), std::begin(beVariables), std::end(beVariables)); + allBeVariables.insert(std::end(allBeVariables), std::begin(failedBeVariables), std::end(failedBeVariables)); + allBeVariables.insert(std::end(allBeVariables), std::begin(failsafeBeVariables), + std::end(failsafeBeVariables)); + // No two BEs fail at the same time (second part of constraint 12) - constraints.push_back(std::make_shared(beVariables)); + constraints.push_back(std::make_shared(allBeVariables)); constraints.back()->setDescription("No two BEs fail at the same time"); // Initialize claim variables in [1, |BE|+1] @@ -142,6 +168,44 @@ namespace storm { // Handle dependencies addMarkovianConstraints(); + + // Failsafe BEs may only fail in non-Markovian states (i.e. if they were triggered) + std::vector> failsafeNotIConstr; + for (uint64_t i = 0; i < dft.nrBasicElements(); ++i) { + failsafeNotIConstr.clear(); + for (auto const &beV : failsafeBeVariables) { + failsafeNotIConstr.push_back(std::make_shared(beV, i)); + } + constraints.push_back( + std::make_shared(std::make_shared(markovianVariables.at(i), true), + std::make_shared(failsafeNotIConstr))); + if (i == 0) { + constraints.back()->setDescription("Failsafe BEs fail only if they are triggered"); + } + } + + + // A failsafe BE only stays failsafe if no trigger has been triggered + std::vector> triggerConstraints; + for (size_t i = 0; i < dft.nrElements(); ++i) { + std::shared_ptr const> element = dft.getElement(i); + if (element->type() == storm::storage::DFTElementType::BE_CONST) { + auto be = std::static_pointer_cast const>(element); + triggerConstraints.clear(); + for (auto const &dependency : be->ingoingDependencies()) { + triggerConstraints.push_back(std::make_shared( + timePointVariables.at(dependency->triggerEvent()->id()), notFailed)); + } + if (!triggerConstraints.empty()) { + constraints.push_back(std::make_shared( + std::make_shared(timePointVariables.at(be->id()), notFailed), + std::make_shared(triggerConstraints))); + constraints.back()->setDescription( + "Failsafe BE " + be->name() + " stays failsafe if no trigger fails"); + } + } + } + } // Constraint Generator Functions diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index ef16d580a..b2b367893 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -344,6 +344,31 @@ namespace storm { uint64_t value; }; + class IsNotConstantValue : public SmtConstraint { + public: + IsNotConstantValue(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) { + } + + virtual ~IsNotConstantValue() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + assert(varIndex < varNames.size()); + sstr << "(distinct " << varNames.at(varIndex) << " " << value << ")"; + return sstr.str(); + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + return manager->getVariableExpression(varNames.at(varIndex)) != manager->integer(value); + } + + private: + uint64_t varIndex; + uint64_t value; + }; + class IsLessConstant : public SmtConstraint { public: