diff --git a/src/builder/DftSmtBuilder.cpp b/src/builder/DftSmtBuilder.cpp new file mode 100644 index 000000000..1d60b2c74 --- /dev/null +++ b/src/builder/DftSmtBuilder.cpp @@ -0,0 +1,120 @@ +#include "src/builder/DFTSMTBuilder.h" +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace builder { + + template + DFTSMTBuilder::DFTSMTBuilder() : manager(std::make_shared()) { + solver = storm::utility::solver::SmtSolverFactory().create(*manager); + } + + template + void DFTSMTBuilder::convertToSMT(storm::storage::DFT const& dft) { + std::cout << "Convert DFT to SMT" << std::endl; + timeMax = manager->integer(dft.nrBasicElements()); + timeFailSafe = manager->integer(dft.nrBasicElements() + 1); + timeZero = manager->integer(0); + + // Convert all elements + for (size_t i = 0; i < dft.nrElements(); ++i) { + std::shared_ptr const> element = dft.getElement(i); + std::cout << "Consider " << element->toString() << std::endl; + if (element->isBasicElement()) { + storm::expressions::Variable varBE = convert(std::static_pointer_cast const>(element)); + varsBE.push_back(varBE); + } else if (element->isGate()) { + storm::expressions::Variable varGate = convert(std::static_pointer_cast const>(element)); + if (dft.getTopLevelIndex() == i) { + topLevel = varGate; + } + } else if (element->isDependency()) { + convert(std::static_pointer_cast const>(element)); + } else if (element->isRestriction()) { + convert(std::static_pointer_cast const>(element)); + } + } + + // No simultaneous fails can occur + for (size_t i = 0; i < varsBE.size() - 1; ++i) { + storm::expressions::Expression be = varsBE[i]; + for (size_t j = i + 1; j < varsBE.size(); ++j) { + storm::expressions::Expression assertion = be != varsBE[j]; + solver->add(assertion); + } + } + + // For every time-point one BE must fail + for (size_t time = 1; time <= dft.nrBasicElements(); ++time) { + storm::expressions::Expression exprTime = manager->integer(time); + storm::expressions::Expression assertion = varsBE[0] == exprTime; + for (size_t i = 1; i < varsBE.size(); ++i) { + assertion = assertion || varsBE[i] == exprTime; + } + assertion = assertion || topLevel <= exprTime; + solver->add(assertion); + } + + } + + template + storm::expressions::Variable DFTSMTBuilder::convert(std::shared_ptr const> const& be) { + storm::expressions::Variable var = manager->declareIntegerVariable(be->name()); + storm::expressions::Expression assertion = timeZero < var && var < timeFailSafe; + solver->add(assertion); + return var; + } + + template + storm::expressions::Variable DFTSMTBuilder::convert(std::shared_ptr const> const& gate) { + storm::expressions::Variable var = manager->declareIntegerVariable(gate->name()); + storm::expressions::Expression assertion = timeZero < var && var <= timeFailSafe; + solver->add(assertion); + return var; + } + + template + storm::expressions::Variable DFTSMTBuilder::convert(std::shared_ptr const> const& dependency) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The dependency cannot be converted into SMT."); + } + + template + storm::expressions::Variable DFTSMTBuilder::convert(std::shared_ptr const> const& restriction) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The restriction cannot be converted into SMT."); + } + + template + bool DFTSMTBuilder::check() const { + std::cout << "Check" << std::endl; + storm::solver::SmtSolver::CheckResult result = solver->check(); + switch (result) { + case solver::SmtSolver::CheckResult::Sat: + { + std::cout << "SAT with model:" << std::endl; + std::shared_ptr model = solver->getModel(); + for (auto const& pair : *manager) { + std::cout << pair.first.getName() << "->" << model->getIntegerValue(pair.first) << std::endl; + } + return true; + } + case solver::SmtSolver::CheckResult::Unsat: + return false; + case solver::SmtSolver::CheckResult::Unknown: + default: + STORM_LOG_ASSERT(false, "Result is unknown."); + return false; + } + } + + + // Explicitly instantiate the class. + template class DFTSMTBuilder; + +#ifdef STORM_HAVE_CARL + template class DFTSMTBuilder; +#endif + + } // namespace builder +} // namespace storm + + diff --git a/src/builder/DftSmtBuilder.h b/src/builder/DftSmtBuilder.h new file mode 100644 index 000000000..596e8106f --- /dev/null +++ b/src/builder/DftSmtBuilder.h @@ -0,0 +1,49 @@ +#ifndef DFTSMTBUILDER_H +#define DFTSMTBUILDER_H + +#include "src/solver/SmtSolver.h" +#include "src/utility/solver.h" +#include "src/storage/dft/DFT.h" + +namespace storm { + namespace builder { + + template + class DFTSMTBuilder { + + public: + DFTSMTBuilder(); + + void convertToSMT(storm::storage::DFT const& dft); + + bool check() const; + + private: + + std::shared_ptr solver; + + std::shared_ptr manager; + + storm::expressions::Expression timeMax; + + storm::expressions::Expression timeFailSafe; + + storm::expressions::Expression timeZero; + + storm::expressions::Expression topLevel; + + std::vector varsBE; + + storm::expressions::Variable convert(std::shared_ptr const> const& be); + + storm::expressions::Variable convert(std::shared_ptr const> const& gate); + + storm::expressions::Variable convert(std::shared_ptr const> const& dependency); + + storm::expressions::Variable convert(std::shared_ptr const> const& restriction); + + }; + } +} + +#endif /* DFTSMTBUILDER_H */ diff --git a/src/settings/modules/DFTSettings.cpp b/src/settings/modules/DFTSettings.cpp index 365ba0271..4df95987c 100644 --- a/src/settings/modules/DFTSettings.cpp +++ b/src/settings/modules/DFTSettings.cpp @@ -27,7 +27,10 @@ namespace storm { const std::string DFTSettings::propTimeBoundOptionName = "timebound"; const std::string DFTSettings::minValueOptionName = "min"; const std::string DFTSettings::maxValueOptionName = "max"; - +#ifdef STORM_HAVE_Z3 + const std::string DFTSettings::solveWithSmtOptionName = "smt"; +#endif + DFTSettings::DFTSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); @@ -39,6 +42,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, propTimeBoundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorExcluding(0.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build()); +#ifdef STORM_HAVE_Z3 + this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); +#endif } bool DFTSettings::isDftFileSet() const { @@ -85,6 +91,12 @@ namespace storm { return this->getOption(maxValueOptionName).getHasOptionBeenSet(); } +#ifdef STORM_HAVE_Z3 + bool DFTSettings::solveWithSMT() const { + return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet(); + } +#endif + void DFTSettings::finalize() { } diff --git a/src/settings/modules/DFTSettings.h b/src/settings/modules/DFTSettings.h index 844953c2c..183e00eef 100644 --- a/src/settings/modules/DFTSettings.h +++ b/src/settings/modules/DFTSettings.h @@ -99,6 +99,15 @@ namespace storm { */ double getPropTimebound() const; +#ifdef STORM_HAVE_Z3 + /*! + * Retrieves whether the DFT should be checked via SMT. + * + * @return True iff the option was set. + */ + bool solveWithSMT() const; +#endif + bool check() const override; void finalize() override; @@ -119,6 +128,9 @@ namespace storm { static const std::string propTimeBoundOptionName; static const std::string minValueOptionName; static const std::string maxValueOptionName; +#ifdef STORM_HAVE_Z3 + static const std::string solveWithSmtOptionName; +#endif };