From 464a497093f821c37b5bb106afbc45c55cc65ae7 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sat, 29 Oct 2016 21:47:53 +0200 Subject: [PATCH] smt checker v1, and better error messages Former-commit-id: ab7391e85db4b7e94d9a6dfb2dfa383d570ff8c0 --- DFTASFChecker.cpp | 9 + DFTASFChecker.hpp | 14 + src/modelchecker/dft/DFTASFChecker.cpp | 413 +++++++++++++++++++++++++ src/modelchecker/dft/DFTASFChecker.h | 61 ++++ src/storage/dft/DFTBuilder.cpp | 2 +- src/storage/dft/DFTState.cpp | 2 +- src/storm-dyftee.cpp | 13 +- 7 files changed, 507 insertions(+), 7 deletions(-) create mode 100644 DFTASFChecker.cpp create mode 100644 DFTASFChecker.hpp create mode 100644 src/modelchecker/dft/DFTASFChecker.cpp create mode 100644 src/modelchecker/dft/DFTASFChecker.h diff --git a/DFTASFChecker.cpp b/DFTASFChecker.cpp new file mode 100644 index 000000000..de7a59428 --- /dev/null +++ b/DFTASFChecker.cpp @@ -0,0 +1,9 @@ +// +// DFTASFChecker.cpp +// storm +// +// Created by Sebastian Junges on 27/10/16. +// +// + +#include "DFTASFChecker.hpp" diff --git a/DFTASFChecker.hpp b/DFTASFChecker.hpp new file mode 100644 index 000000000..7920f026a --- /dev/null +++ b/DFTASFChecker.hpp @@ -0,0 +1,14 @@ +// +// DFTASFChecker.hpp +// storm +// +// Created by Sebastian Junges on 27/10/16. +// +// + +#ifndef DFTASFChecker_hpp +#define DFTASFChecker_hpp + +#include + +#endif /* DFTASFChecker_hpp */ diff --git a/src/modelchecker/dft/DFTASFChecker.cpp b/src/modelchecker/dft/DFTASFChecker.cpp new file mode 100644 index 000000000..ac28ba5cf --- /dev/null +++ b/src/modelchecker/dft/DFTASFChecker.cpp @@ -0,0 +1,413 @@ +#include "DFTASFChecker.h" +#include + +namespace storm { + + namespace modelchecker { + + /* + * Variable[VarIndex] is the maximum of the others + */ + class IsMaximum : public DFTConstraint { + public: + IsMaximum(uint64_t varIndex, std::vector const& varIndices) : varIndex(varIndex), varIndices(varIndices) { + + } + + virtual ~IsMaximum() { + + } + + std::string toSmtlib2(std::vector const& varNames) const override { + std::stringstream sstr; + sstr << "(and "; + // assert it is largereq than all values. + for (auto const& ovi : varIndices) { + sstr << "(>= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") "; + } + // assert it is one of the values. + sstr << "(or "; + for (auto const& ovi : varIndices) { + sstr << "(= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") "; + } + sstr << ")"; // end of the or + sstr << ")"; // end outer and. + return sstr.str(); + + } + + + private: + uint64_t varIndex; + std::vector varIndices; + }; + /* + * First is the minimum of the others + */ + class IsMinimum : public DFTConstraint { + public: + IsMinimum(uint64_t varIndex, std::vector const& varIndices) : varIndex(varIndex), varIndices(varIndices) { + + } + + + virtual ~IsMinimum() { + + } + + std::string toSmtlib2(std::vector const& varNames) const override { + std::stringstream sstr; + sstr << "(and "; + // assert it is smallereq than all values. + for (auto const& ovi : varIndices) { + sstr << "(<= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") "; + } + // assert it is one of the values. + sstr << "(or "; + for (auto const& ovi : varIndices) { + sstr << "(= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") "; + } + sstr << ")"; // end of the or + sstr << ")"; // end outer and. + return sstr.str(); + + } + + + private: + uint64_t varIndex; + std::vector varIndices; + }; + + class BetweenValues : public DFTConstraint { + public: + BetweenValues(uint64_t varIndex, uint64_t lower, uint64_t upper) : varIndex(varIndex), upperBound(upper) , lowerBound(lower) { + + } + virtual ~BetweenValues() { + + } + + std::string toSmtlib2(std::vector const& varNames) const override { + std::stringstream sstr; + sstr << "(and "; + sstr << "(>= " << varNames.at(varIndex) << " " << lowerBound << ")"; + sstr << "(<= " << varNames.at(varIndex) << " " << upperBound << ")"; + sstr << ")"; + return sstr.str(); + } + + private: + uint64_t varIndex; + uint64_t upperBound; + uint64_t lowerBound; + }; + + class And : public DFTConstraint { + public: + And(std::vector> const& constraints) : constraints(constraints) {} + + virtual ~And() { + + } + + std::string toSmtlib2(std::vector const& varNames) const override { + std::stringstream sstr; + sstr << "(and"; + for(auto const& c : constraints) { + sstr << " " << c->toSmtlib2(varNames); + } + sstr << ")"; + return sstr.str(); + } + private: + std::vector> constraints; + + }; + + class Iff : public DFTConstraint { + public: + Iff(std::shared_ptr l, std::shared_ptr r) : lhs(l), rhs(r) { + + } + + + std::string toSmtlib2(std::vector const& varNames) const override { + std::stringstream sstr; + sstr << "(= " << lhs->toSmtlib2(varNames) << " " << rhs->toSmtlib2(varNames) << ")"; + return sstr.str(); + } + + private: + std::shared_ptr lhs; + std::shared_ptr rhs; + }; + + class IsConstantValue : public DFTConstraint { + public: + IsConstantValue(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) { + + } + + virtual ~IsConstantValue() { + + } + + std::string toSmtlib2(std::vector const& varNames) const override { + std::stringstream sstr; + assert(varIndex < varNames.size()); + sstr << "(= " << varNames.at(varIndex) << " " << value << ")"; + return sstr.str(); + } + + private: + uint64_t varIndex; + uint64_t value; + }; + + class IsEqual : public DFTConstraint { + public: + IsEqual(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) { + + } + + virtual ~IsEqual() { + + } + + std::string toSmtlib2(std::vector const& varNames) const override { + return "(= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + " )"; + } + + private: + uint64_t var1Index; + uint64_t var2Index; + }; + + class IsLEqual : public DFTConstraint { + public: + IsLEqual(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) { + + } + + virtual ~IsLEqual() { + + } + + std::string toSmtlib2(std::vector const& varNames) const override { + return "(<= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + " )"; + } + + private: + uint64_t var1Index; + uint64_t var2Index; + }; + + class PairwiseDifferent : public DFTConstraint { + public: + PairwiseDifferent(std::vector const& indices) : varIndices(indices) { + + } + virtual ~PairwiseDifferent() { + + } + + std::string toSmtlib2(std::vector const& varNames) const override { + std::stringstream sstr; + sstr << "(distinct"; + // for(uint64_t i = 0; i < varIndices.size(); ++i) { + // for(uint64_t j = i + 1; j < varIndices.size(); ++j) { + // sstr << "()"; + // } + // } + for (auto const& varIndex : varIndices) { + sstr << " " << varNames.at(varIndex); + } + sstr << ")"; + return sstr.str(); + } + + private: + std::vector varIndices; + }; + + class Sorted : public DFTConstraint { + public: + Sorted(std::vector varIndices) : varIndices(varIndices) { + + } + + virtual ~Sorted() { + + } + + std::string toSmtlib2(std::vector const& varNames) const override { + std::stringstream sstr; + sstr << "(and "; + for(uint64_t i = 1; i < varIndices.size(); ++i) { + sstr << "(<= " << varNames.at(varIndices.at(i-1)) << " " << varNames.at(varIndices.at(i)) << ")"; + } + sstr << ") "; + return sstr.str(); + } + + + private: + std::vector varIndices; + }; + + class IfThenElse : public DFTConstraint { + public: + IfThenElse(std::shared_ptr ifC, std::shared_ptr thenC, std::shared_ptr elseC) : ifConstraint(ifC), thenConstraint(thenC), elseConstraint(elseC) { + + } + + std::string toSmtlib2(std::vector const& varNames) const override { + std::stringstream sstr; + sstr << "(ite " << ifConstraint->toSmtlib2(varNames) << " " << thenConstraint->toSmtlib2(varNames) << " " << elseConstraint->toSmtlib2(varNames) << ")"; + return sstr.str(); + } + + private: + std::shared_ptr ifConstraint; + std::shared_ptr thenConstraint; + std::shared_ptr elseConstraint; + }; + + + DFTASFChecker::DFTASFChecker(storm::storage::DFT const& dft) : dft(dft) { + // Intentionally left empty. + } + + uint64_t DFTASFChecker::getClaimVariableIndex(uint64_t spare, uint64_t child) const { + return claimVariables.at(SpareAndChildPair(spare, child)); + } + + void DFTASFChecker::convert() { + + std::vector beVariables; + // Convert all elements + for (size_t i = 0; i < dft.nrElements(); ++i) { + std::shared_ptr const> element = dft.getElement(i); + varNames.push_back("t_" + element->name()); + timePointVariables.emplace(i, varNames.size() - 1); + switch (element->type()) { + case storm::storage::DFTElementType::BE: + beVariables.push_back(varNames.size() - 1); + break; + case storm::storage::DFTElementType::SPARE: + { + auto spare = std::static_pointer_cast const>(element); + for( auto const& spareChild : spare->children()) { + varNames.push_back("c_" + element->name() + "_" + spareChild->name()); + claimVariables.emplace(SpareAndChildPair(element->id(), spareChild->id()), varNames.size() - 1); + } + break; + } + default: + break; + } + } + + // BE + constraints.push_back(std::make_shared(beVariables)); + constraints.back()->setDescription("No two BEs fail at the same time"); + for( auto const& beV : beVariables) { + constraints.push_back(std::make_shared(beV, 1, dft.nrBasicElements())); + } + + // Claim variables + for (auto const& csvV : claimVariables) { + constraints.push_back(std::make_shared(csvV.second, 0, dft.nrBasicElements() + 1)); + } + + for (size_t i = 0; i < dft.nrElements(); ++i) { + std::shared_ptr const> element = dft.getElement(i); + if(element->isSpareGate()) { + auto spare = std::static_pointer_cast const>(element); + auto const& spareChild = spare->children().front(); + constraints.push_back(std::make_shared(getClaimVariableIndex(spare->id(), spareChild->id()), 0)); + constraints.back()->setDescription("Spare " + spare->name() + " claims first child"); + + } + } + + + for (size_t i = 0; i < dft.nrElements(); ++i) { + std::vector childVarIndices; + if (dft.isGate(i)) { + std::shared_ptr const> gate = dft.getGate(i); + for (auto const& child : gate->children()) { + childVarIndices.push_back(timePointVariables.at(child->id())); + } + } + + std::shared_ptr const> element = dft.getElement(i); + switch (element->type()) { + case storm::storage::DFTElementType::AND: + constraints.push_back(std::make_shared(timePointVariables.at(i), childVarIndices)); + constraints.back()->setDescription("And gate"); + break; + case storm::storage::DFTElementType::OR: + constraints.push_back(std::make_shared(timePointVariables.at(i), childVarIndices)); + constraints.back()->setDescription("Or gate"); + break; + case storm::storage::DFTElementType::PAND: + constraints.push_back(std::make_shared(std::make_shared(childVarIndices), std::make_shared(timePointVariables.at(i), timePointVariables.at(childVarIndices.back())), std::make_shared(timePointVariables.at(i), dft.nrBasicElements()+1))); + constraints.back()->setDescription("Pand gate"); + case storm::storage::DFTElementType::SPARE: + { + auto spare = std::static_pointer_cast const>(element); + auto const& children = spare->children(); + + constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.back()->id()), childVarIndices.back()), std::make_shared(timePointVariables.at(i), childVarIndices.back()))); + constraints.back()->setDescription("Last child & claimed -> spare fails"); + std::vector> ifcs; + uint64_t xv = childVarIndices.at(childVarIndices.size()-2); // if v is the child, xv is the time x fails. + uint64_t csn = getClaimVariableIndex(spare->id(), children.back()->id()); // csn is the moment the spare claims the next child + uint64_t xn = childVarIndices.back(); // xn is the moment the next child fails + ifcs.push_back(std::make_shared(xv, xn)); + for(auto const& otherSpare : children.back()->parents()) { + if(otherSpare->id() == i) { continue; }// not a OTHER spare. + ifcs.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), children.back()->id()), dft.nrBasicElements()+1)); + } + std::shared_ptr ite = std::make_shared(std::make_shared(ifcs), std::make_shared(csn, xv), std::make_shared(timePointVariables.at(i), xv)); + constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.at(children.size()-2)->id()), xv), ite)); + constraints.back()->setDescription("1 but last child & claimed"); + + for( uint64_t j = 0; j < children.size() - 2; ++j) { + uint64_t currChild = children.size() - 1 - j; + + } + break; + } + default: + break; + } + } + + constraints.push_back(std::make_shared(dft.getTopLevelIndex(), dft.nrBasicElements()+1)); + } + + void DFTASFChecker::toFile(std::string const& filename) { + std::ofstream ofs; + std::cout << "Writing to " << filename << std::endl; + ofs.open(filename); + ofs << "; time point variables" << std::endl; + for (auto const& timeVarEntry : timePointVariables) { + ofs << "(declare-fun " << varNames[timeVarEntry.second] << "() Int)" << std::endl; + } + ofs << "; claim variables" << std::endl; + for (auto const& claimVarEntry : claimVariables) { + ofs << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl; + } + for (auto const& constraint : constraints) { + ofs << "; " << constraint->description() << std::endl; + ofs << "(assert " << constraint->toSmtlib2(varNames) << ")" << std::endl; + } + ofs << "(check-sat)" << std::endl; + ofs.close(); + + } + } +} \ No newline at end of file diff --git a/src/modelchecker/dft/DFTASFChecker.h b/src/modelchecker/dft/DFTASFChecker.h new file mode 100644 index 000000000..73a323b03 --- /dev/null +++ b/src/modelchecker/dft/DFTASFChecker.h @@ -0,0 +1,61 @@ +#pragma once + +#include +#include +#include +#include "src/storage/dft/DFT.h" + + +namespace storm { + namespace modelchecker { + class DFTConstraint { + public: + virtual ~DFTConstraint() { + + } + + virtual std::string toSmtlib2(std::vector const& varNames) const = 0; + virtual std::string description() const { return descript; } + + void setDescription(std::string const& descr) { + descript = descr; + } + + private: + std::string descript; + }; + + class SpareAndChildPair { + + public: + SpareAndChildPair(uint64_t spareIndex, uint64_t childIndex) : spareIndex(spareIndex), childIndex(childIndex) { + + } + + uint64_t spareIndex; + uint64_t childIndex; + }; + + bool operator<(SpareAndChildPair const& p1, SpareAndChildPair const& p2) { + return p1.spareIndex < p2.spareIndex || (p1.spareIndex == p2.spareIndex && p1.childIndex < p2.childIndex); + } + + class DFTASFChecker { + using ValueType = double; + + public: + DFTASFChecker(storm::storage::DFT const&); + void convert(); + void toFile(std::string const&); + + private: + uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; + + storm::storage::DFT const& dft; + std::vector varNames; + std::unordered_map timePointVariables; + std::vector> constraints; + std::map claimVariables; + }; + } +} \ No newline at end of file diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index 840f5b77b..55b430863 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -32,7 +32,7 @@ namespace storm { // Child not found -> find first dependent event to assure that child is dependency // TODO: Not sure whether this is the intended behaviour? auto itFind = mElements.find(child + "_1"); - STORM_LOG_ASSERT(itFind != mElements.end(), "Child not found."); + STORM_LOG_ASSERT(itFind != mElements.end(), "Child '" << child << "' for gate '" << gate->name() << "' not found."); STORM_LOG_ASSERT(itFind->second->isDependency(), "Child is no dependency."); STORM_LOG_TRACE("Ignore functional dependency " << child << " in gate " << gate->name()); } diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index f6bb692a7..6e2b80035 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -319,7 +319,7 @@ namespace storm { mCurrentlyFailableBE.push_back(elem); // Remove from not failable BEs auto it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), elem); - STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element not found."); + STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element " << mDft.getElement(elem)->name() << " not found."); mCurrentlyNotFailableBE.erase(it); } } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) { diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 51061050e..2c7418075 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -3,6 +3,8 @@ #include "src/utility/storm.h" #include "src/parser/DFTGalileoParser.h" #include "src/modelchecker/dft/DFTModelChecker.h" + +#include "src/modelchecker/dft/DFTASFChecker.h" #include "src/cli/cli.h" #include "src/exceptions/BaseException.h" #include "src/utility/macros.h" @@ -58,10 +60,11 @@ void analyzeWithSMT(std::string filename) { storm::parser::DFTGalileoParser parser; storm::storage::DFT dft = parser.parseDFT(filename); - storm::builder::DFTSMTBuilder dftSmtBuilder; - dftSmtBuilder.convertToSMT(dft); - bool sat = dftSmtBuilder.check(); - std::cout << "SMT result: " << sat << std::endl; + storm::modelchecker::DFTASFChecker asfChecker(dft); + asfChecker.convert(); + asfChecker.toFile("test.smt2"); + //bool sat = dftSmtBuilder.check(); + //std::cout << "SMT result: " << sat << std::endl; } /*! @@ -120,7 +123,7 @@ int main(const int argc, const char** argv) { if (dftSettings.solveWithSMT()) { // Solve with SMT if (parametric) { - analyzeWithSMT(dftSettings.getDftFilename()); + // analyzeWithSMT(dftSettings.getDftFilename()); } else { analyzeWithSMT(dftSettings.getDftFilename()); }