From 8051912147ec4915812d5bed1e03140a2b097fc0 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 22 Nov 2017 13:50:34 +0100 Subject: [PATCH 01/38] Correct indentation --- .../modelchecker/dft/DFTASFChecker.cpp | 718 +++++++++--------- .../modelchecker/dft/DFTASFChecker.h | 6 +- 2 files changed, 351 insertions(+), 373 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 55d968a2c..b1a37aa90 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -7,16 +7,14 @@ namespace storm { namespace modelchecker { /* - * Variable[VarIndex] is the maximum of the others + * 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 { @@ -34,383 +32,367 @@ namespace storm { 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. + + 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; + }; - uint64_t DFTASFChecker::getClaimVariableIndex(uint64_t spare, uint64_t child) const { - return claimVariables.at(SpareAndChildPair(spare, child)); + + 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; + }; + - 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; + 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; } - - // 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"); - - } + 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())); } - - - 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::shared_ptr elseCase = nullptr; + for (uint64_t j = 0; j < children.size(); ++j) { + uint64_t currChild = children.size() - 2 - j; + std::vector> ifcs; + uint64_t xv = childVarIndices.at(currChild); // if v is the child, xv is the time x fails. + uint64_t csn = getClaimVariableIndex(spare->id(), childVarIndices.at(currChild+1)); // csn is the moment the spare claims the next child + uint64_t xn = childVarIndices.at(currChild+1); // xn is the moment the next child fails + if (j == 0) { + elseCase = std::make_shared(timePointVariables.at(i), xv); } - } - - 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::shared_ptr elseCase = nullptr; - for( uint64_t j = 0; j < children.size(); ++j) { - uint64_t currChild = children.size() - 2 - j; - std::vector> ifcs; - uint64_t xv = childVarIndices.at(currChild); // if v is the child, xv is the time x fails. - uint64_t csn = getClaimVariableIndex(spare->id(), childVarIndices.at(currChild+1)); // csn is the moment the spare claims the next child - uint64_t xn = childVarIndices.at(currChild+1); // xn is the moment the next child fails - if (j == 0) { - elseCase = std::make_shared(timePointVariables.at(i), xv); - } - ifcs.push_back(std::make_shared(xv, xn)); - for(auto const& otherSpare : children.at(currChild+1)->parents()) { - if(otherSpare->id() == i) { continue; }// not a OTHER spare. - ifcs.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), children.at(currChild+1)->id()), dft.nrBasicElements()+1)); - } - std::shared_ptr ite = std::make_shared(std::make_shared(ifcs), std::make_shared(csn, xv), elseCase); - elseCase = ite; - constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), xv), ite)); - constraints.back()->setDescription(std::to_string(j+1) + " but last child & claimed"); - } - break; + ifcs.push_back(std::make_shared(xv, xn)); + for (auto const& otherSpare : children.at(currChild+1)->parents()) { + if (otherSpare->id() == i) { continue; }// not a OTHER spare. + ifcs.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), children.at(currChild+1)->id()), dft.nrBasicElements()+1)); } - default: - break; + std::shared_ptr ite = std::make_shared(std::make_shared(ifcs), std::make_shared(csn, xv), elseCase); + elseCase = ite; + constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), xv), ite)); + constraints.back()->setDescription(std::to_string(j+1) + " but last child & claimed"); } + break; } - - constraints.push_back(std::make_shared(dft.getTopLevelIndex(), dft.nrBasicElements()+1)); - } - - void DFTASFChecker::toFile(std::string const& filename) { - std::ofstream stream; - storm::utility::openFile(filename, stream); - stream << "; time point variables" << std::endl; - for (auto const& timeVarEntry : timePointVariables) { - stream << "(declare-fun " << varNames[timeVarEntry.second] << "() Int)" << std::endl; - } - stream << "; claim variables" << std::endl; - for (auto const& claimVarEntry : claimVariables) { - stream << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl; - } - for (auto const& constraint : constraints) { - stream << "; " << constraint->description() << std::endl; - stream << "(assert " << constraint->toSmtlib2(varNames) << ")" << std::endl; - } - stream << "(check-sat)" << std::endl; - storm::utility::closeFile(stream); + default: + break; } + } + constraints.push_back(std::make_shared(dft.getTopLevelIndex(), dft.nrBasicElements()+1)); + } + + void DFTASFChecker::toFile(std::string const& filename) { + std::ofstream stream; + storm::utility::openFile(filename, stream); + stream << "; time point variables" << std::endl; + for (auto const& timeVarEntry : timePointVariables) { + stream << "(declare-fun " << varNames[timeVarEntry.second] << "() Int)" << std::endl; + } + stream << "; claim variables" << std::endl; + for (auto const& claimVarEntry : claimVariables) { + stream << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl; + } + for (auto const& constraint : constraints) { + stream << "; " << constraint->description() << std::endl; + stream << "(assert " << constraint->toSmtlib2(varNames) << ")" << std::endl; + } + stream << "(check-sat)" << std::endl; + storm::utility::closeFile(stream); + } } } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index c4a47116d..e38c5ed91 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -12,10 +12,9 @@ namespace storm { class DFTConstraint { public: virtual ~DFTConstraint() { - } - virtual std::string toSmtlib2(std::vector const& varNames) const = 0; + virtual std::string toSmtlib2(std::vector const& varNames) const = 0; virtual std::string description() const { return descript; } void setDescription(std::string const& descr) { @@ -27,10 +26,8 @@ namespace storm { }; class SpareAndChildPair { - public: SpareAndChildPair(uint64_t spareIndex, uint64_t childIndex) : spareIndex(spareIndex), childIndex(childIndex) { - } uint64_t spareIndex; @@ -43,7 +40,6 @@ namespace storm { class DFTASFChecker { using ValueType = double; - public: DFTASFChecker(storm::storage::DFT const&); void convert(); From 34911003e016ba55d19aca939569382a88fcea2d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 22 Nov 2017 15:06:55 +0100 Subject: [PATCH 02/38] Better comments for SMT generation --- .../modelchecker/dft/DFTASFChecker.cpp | 65 +++++++++++++++---- 1 file changed, 51 insertions(+), 14 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index b1a37aa90..ec0bcd4f9 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -271,7 +271,8 @@ namespace storm { void DFTASFChecker::convert() { std::vector beVariables; - // Convert all elements + + // Initialize variables for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); varNames.push_back("t_" + element->name()); @@ -294,21 +295,28 @@ namespace storm { } } - // BE + + // Generate constraints + + // No two BEs fail at the same time (first part of constraint 12) constraints.push_back(std::make_shared(beVariables)); constraints.back()->setDescription("No two BEs fail at the same time"); + + // All BEs have to fail (second part of constraint 12) 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)); + + // Initialize claim variables in [1, |BE|+1] + for (auto const& claimVariable : claimVariables) { + constraints.push_back(std::make_shared(claimVariable.second, 0, dft.nrBasicElements() + 1)); } + // First child of each spare is claimed in the beginning for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); - if(element->isSpareGate()) { + 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)); @@ -317,7 +325,9 @@ namespace storm { } } + // Encoding for specific gates for (size_t i = 0; i < dft.nrElements(); ++i) { + // Get indices for gate children std::vector childVarIndices; if (dft.isGate(i)) { std::shared_ptr const> gate = dft.getGate(i); @@ -328,25 +338,39 @@ namespace storm { std::shared_ptr const> element = dft.getElement(i); switch (element->type()) { + case storm::storage::DFTElementType::BE: + // BEs were already considered before + break; case storm::storage::DFTElementType::AND: + // Constraint for AND gate (constraint 1) constraints.push_back(std::make_shared(timePointVariables.at(i), childVarIndices)); constraints.back()->setDescription("And gate"); break; case storm::storage::DFTElementType::OR: + // Constraint for OR gate (constraint 2) 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))); + { + + // Constraint for PAND gate (constraint 3) + std::shared_ptr ifC = std::make_shared(childVarIndices); + std::shared_ptr thenC = std::make_shared(timePointVariables.at(i), timePointVariables.at(childVarIndices.back())); + std::shared_ptr elseC = std::make_shared(timePointVariables.at(i), dft.nrBasicElements()+1); + constraints.push_back(std::make_shared(ifC, thenC, elseC)); 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()))); + // If last child is claimed before failure the spare fails when the last child fails (constraint 5) + std::shared_ptr leftC = std::make_shared(getClaimVariableIndex(spare->id(), children.back()->id()), childVarIndices.back()); + constraints.push_back(std::make_shared(leftC, std::make_shared(timePointVariables.at(i), childVarIndices.back()))); constraints.back()->setDescription("Last child & claimed -> spare fails"); + // Construct constraint for claiming std::shared_ptr elseCase = nullptr; for (uint64_t j = 0; j < children.size(); ++j) { uint64_t currChild = children.size() - 2 - j; @@ -354,22 +378,35 @@ namespace storm { uint64_t xv = childVarIndices.at(currChild); // if v is the child, xv is the time x fails. uint64_t csn = getClaimVariableIndex(spare->id(), childVarIndices.at(currChild+1)); // csn is the moment the spare claims the next child uint64_t xn = childVarIndices.at(currChild+1); // xn is the moment the next child fails + + // Generate constraint for trying to claim next child if (j == 0) { - elseCase = std::make_shared(timePointVariables.at(i), xv); + // Last child: spare fails at same point as xv (otherwise case in constraint 7) + elseCase = std::make_shared(timePointVariables.at(i), xv); } + // Next child is not yet failed ifcs.push_back(std::make_shared(xv, xn)); + + // Child is not yet claimed by a different spare (first part of case distinction for constraint 7) for (auto const& otherSpare : children.at(currChild+1)->parents()) { - if (otherSpare->id() == i) { continue; }// not a OTHER spare. + if (otherSpare->id() == i) { + // not an OTHER spare. + continue; + } ifcs.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), children.at(currChild+1)->id()), dft.nrBasicElements()+1)); } - std::shared_ptr ite = std::make_shared(std::make_shared(ifcs), std::make_shared(csn, xv), elseCase); - elseCase = ite; - constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), xv), ite)); + // Claim next child (constraint 7) + // elseCase contains the constraints for the recursive call to phi^s_{i+1} + std::shared_ptr tryClaimC = std::make_shared(std::make_shared(ifcs), std::make_shared(csn, xv), elseCase); + elseCase = tryClaimC; + // If i-th child fails after being claimed, then try to claim (i+1)-th child (constraint 6) + constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), xv), tryClaimC)); constraints.back()->setDescription(std::to_string(j+1) + " but last child & claimed"); } break; } default: + STORM_LOG_WARN("DFT element of type '" << element->type() << "' is ignored for SMT encoding."); break; } } From cf7c09584b68974f80f5e838ad42a756f02d0e40 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 22 Nov 2017 15:42:54 +0100 Subject: [PATCH 03/38] Use implication instead off iff in constraint 5 --- .../modelchecker/dft/DFTASFChecker.cpp | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index ec0bcd4f9..10b3cdf2c 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -119,6 +119,23 @@ namespace storm { }; + class Implies : public DFTConstraint { + public: + Implies(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 Iff : public DFTConstraint { public: Iff(std::shared_ptr l, std::shared_ptr r) : lhs(l), rhs(r) { @@ -367,7 +384,7 @@ namespace storm { auto const& children = spare->children(); // If last child is claimed before failure the spare fails when the last child fails (constraint 5) std::shared_ptr leftC = std::make_shared(getClaimVariableIndex(spare->id(), children.back()->id()), childVarIndices.back()); - constraints.push_back(std::make_shared(leftC, std::make_shared(timePointVariables.at(i), childVarIndices.back()))); + constraints.push_back(std::make_shared(leftC, std::make_shared(timePointVariables.at(i), childVarIndices.back()))); constraints.back()->setDescription("Last child & claimed -> spare fails"); // Construct constraint for claiming From 3df80c338919997858d4200d4d4f1abed8034f8d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 22 Nov 2017 17:03:34 +0100 Subject: [PATCH 04/38] Better comments for SMT encoding --- .../modelchecker/dft/DFTASFChecker.cpp | 102 +++++++++--------- .../modelchecker/dft/DFTASFChecker.h | 5 +- 2 files changed, 55 insertions(+), 52 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 10b3cdf2c..f59fb3455 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -192,12 +192,12 @@ namespace storm { }; - class IsLEqual : public DFTConstraint { + class IsLessEqual : public DFTConstraint { public: - IsLEqual(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) { + IsLessEqual(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) { } - virtual ~IsLEqual() { + virtual ~IsLessEqual() { } std::string toSmtlib2(std::vector const& varNames) const override { @@ -288,6 +288,7 @@ namespace storm { void DFTASFChecker::convert() { std::vector beVariables; + uint64_t notFailed = dft.nrBasicElements()+1; // Value indicating the element is not failed // Initialize variables for (size_t i = 0; i < dft.nrElements(); ++i) { @@ -324,36 +325,24 @@ namespace storm { constraints.push_back(std::make_shared(beV, 1, dft.nrBasicElements())); } - // Initialize claim variables in [1, |BE|+1] for (auto const& claimVariable : claimVariables) { - constraints.push_back(std::make_shared(claimVariable.second, 0, dft.nrBasicElements() + 1)); + constraints.push_back(std::make_shared(claimVariable.second, 0, notFailed)); } - // First child of each spare is claimed in the beginning + // Encoding for gates 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"); - - } - } - // Encoding for specific gates - for (size_t i = 0; i < dft.nrElements(); ++i) { // Get indices for gate children std::vector childVarIndices; - if (dft.isGate(i)) { + if (element->isGate()) { 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::BE: // BEs were already considered before @@ -361,64 +350,71 @@ namespace storm { case storm::storage::DFTElementType::AND: // Constraint for AND gate (constraint 1) constraints.push_back(std::make_shared(timePointVariables.at(i), childVarIndices)); - constraints.back()->setDescription("And gate"); + constraints.back()->setDescription("AND gate"); break; case storm::storage::DFTElementType::OR: // Constraint for OR gate (constraint 2) constraints.push_back(std::make_shared(timePointVariables.at(i), childVarIndices)); - constraints.back()->setDescription("Or gate"); + constraints.back()->setDescription("OR gate"); break; case storm::storage::DFTElementType::PAND: { - // Constraint for PAND gate (constraint 3) std::shared_ptr ifC = std::make_shared(childVarIndices); std::shared_ptr thenC = std::make_shared(timePointVariables.at(i), timePointVariables.at(childVarIndices.back())); - std::shared_ptr elseC = std::make_shared(timePointVariables.at(i), dft.nrBasicElements()+1); + std::shared_ptr elseC = std::make_shared(timePointVariables.at(i), notFailed); constraints.push_back(std::make_shared(ifC, thenC, elseC)); - constraints.back()->setDescription("Pand gate"); + constraints.back()->setDescription("PAND gate"); } case storm::storage::DFTElementType::SPARE: { auto spare = std::static_pointer_cast const>(element); auto const& children = spare->children(); - // If last child is claimed before failure the spare fails when the last child fails (constraint 5) - std::shared_ptr leftC = std::make_shared(getClaimVariableIndex(spare->id(), children.back()->id()), childVarIndices.back()); - constraints.push_back(std::make_shared(leftC, std::make_shared(timePointVariables.at(i), childVarIndices.back()))); - constraints.back()->setDescription("Last child & claimed -> spare fails"); + uint64_t firstChild = children.front()->id(); + uint64_t lastChild = children.back()->id(); - // Construct constraint for claiming - std::shared_ptr elseCase = nullptr; - for (uint64_t j = 0; j < children.size(); ++j) { + // First child of each spare is claimed in the beginning + constraints.push_back(std::make_shared(getClaimVariableIndex(spare->id(), firstChild), 0)); + constraints.back()->setDescription("SPARE " + spare->name() + " claims first child"); + + // If last child is claimed before failure, then the spare fails when the last child fails (constraint 5) + std::shared_ptr leftC = std::make_shared(getClaimVariableIndex(spare->id(), lastChild), childVarIndices.back()); + constraints.push_back(std::make_shared(leftC, std::make_shared(timePointVariables.at(i), childVarIndices.back()))); + constraints.back()->setDescription("Last child & claimed -> SPARE fails"); + + // Construct constraint for trying to claim next child + // We recursively build the function phi^s_i + // Last child: spare fails at same point as second to last child (otherwise case in constraint 7) + std::shared_ptr oldPhi = std::make_shared(timePointVariables.at(i), childVarIndices.at(children.size() - 2)); + STORM_LOG_ASSERT(children.size() >= 2, "Spare has only one child"); + for (uint64_t j = 0; j+1 < children.size(); ++j) { uint64_t currChild = children.size() - 2 - j; + uint64_t nextChild = currChild + 1; + uint64_t timeCurrChild = childVarIndices.at(currChild); // Moment when current child fails + uint64_t timeNextChild = childVarIndices.at(nextChild); // Moment when next child fails + uint64_t claimNextChild = getClaimVariableIndex(spare->id(), childVarIndices.at(nextChild)); // Moment the spare claims the next child + + // Check if next child is availble (first part of case distinction for constraint 7) std::vector> ifcs; - uint64_t xv = childVarIndices.at(currChild); // if v is the child, xv is the time x fails. - uint64_t csn = getClaimVariableIndex(spare->id(), childVarIndices.at(currChild+1)); // csn is the moment the spare claims the next child - uint64_t xn = childVarIndices.at(currChild+1); // xn is the moment the next child fails - - // Generate constraint for trying to claim next child - if (j == 0) { - // Last child: spare fails at same point as xv (otherwise case in constraint 7) - elseCase = std::make_shared(timePointVariables.at(i), xv); - } // Next child is not yet failed - ifcs.push_back(std::make_shared(xv, xn)); - - // Child is not yet claimed by a different spare (first part of case distinction for constraint 7) - for (auto const& otherSpare : children.at(currChild+1)->parents()) { + ifcs.push_back(std::make_shared(timeCurrChild, timeNextChild)); + // Child is not yet claimed by a different spare + for (auto const& otherSpare : children.at(nextChild)->parents()) { if (otherSpare->id() == i) { // not an OTHER spare. continue; } - ifcs.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), children.at(currChild+1)->id()), dft.nrBasicElements()+1)); + ifcs.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), children.at(nextChild)->id()), notFailed)); } + // Claim next child (constraint 7) - // elseCase contains the constraints for the recursive call to phi^s_{i+1} - std::shared_ptr tryClaimC = std::make_shared(std::make_shared(ifcs), std::make_shared(csn, xv), elseCase); - elseCase = tryClaimC; + // oldPhi contains the constraints for the recursive call to phi^s_{i+1} + std::shared_ptr tryClaimC = std::make_shared(std::make_shared(ifcs), std::make_shared(claimNextChild, timeCurrChild), oldPhi); + // Next iteration of phi + oldPhi = tryClaimC; // If i-th child fails after being claimed, then try to claim (i+1)-th child (constraint 6) - constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), xv), tryClaimC)); - constraints.back()->setDescription(std::to_string(j+1) + " but last child & claimed"); + constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), timeCurrChild), tryClaimC)); + constraints.back()->setDescription("Try to claim " + std::to_string(nextChild+1) + "th child"); } break; } @@ -427,7 +423,9 @@ namespace storm { break; } } - constraints.push_back(std::make_shared(dft.getTopLevelIndex(), dft.nrBasicElements()+1)); + // Toplevel element will not fail (part of constraint 13) + constraints.push_back(std::make_shared(dft.getTopLevelIndex(), notFailed)); + constraints.back()->setDescription("Toplevel element should not fail"); } void DFTASFChecker::toFile(std::string const& filename) { @@ -442,7 +440,9 @@ namespace storm { stream << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl; } for (auto const& constraint : constraints) { - stream << "; " << constraint->description() << std::endl; + if (!constraint->description().empty()) { + stream << "; " << constraint->description() << std::endl; + } stream << "(assert " << constraint->toSmtlib2(varNames) << ")" << std::endl; } stream << "(check-sat)" << std::endl; diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index e38c5ed91..f05bd6595 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -15,7 +15,10 @@ namespace storm { } virtual std::string toSmtlib2(std::vector const& varNames) const = 0; - virtual std::string description() const { return descript; } + + virtual std::string description() const { + return descript; + } void setDescription(std::string const& descr) { descript = descr; From b567aa0de924c00fe7df26da1138fa14dcde4567 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 22 Nov 2017 17:26:54 +0100 Subject: [PATCH 05/38] Added encoding for constraint 8 --- .../modelchecker/dft/DFTASFChecker.cpp | 64 ++++++++++++++++--- 1 file changed, 55 insertions(+), 9 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index f59fb3455..246065266 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -174,6 +174,27 @@ namespace storm { }; + class IsLessConstant : public DFTConstraint { + public: + IsLessConstant(uint64_t varIndex, uint64_t val) :varIndex(varIndex), value(val) { + } + + virtual ~IsLessConstant() { + } + + 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) { @@ -183,7 +204,7 @@ namespace storm { } std::string toSmtlib2(std::vector const& varNames) const override { - return "(= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + " )"; + return "(= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")"; } private: @@ -192,16 +213,16 @@ namespace storm { }; - class IsLessEqual : public DFTConstraint { + class IsLess : public DFTConstraint { public: - IsLessEqual(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) { + IsLess(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) { } - virtual ~IsLessEqual() { + virtual ~IsLess() { } std::string toSmtlib2(std::vector const& varNames) const override { - return "(<= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + " )"; + return "(< " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")"; } private: @@ -378,7 +399,7 @@ namespace storm { constraints.back()->setDescription("SPARE " + spare->name() + " claims first child"); // If last child is claimed before failure, then the spare fails when the last child fails (constraint 5) - std::shared_ptr leftC = std::make_shared(getClaimVariableIndex(spare->id(), lastChild), childVarIndices.back()); + std::shared_ptr leftC = std::make_shared(getClaimVariableIndex(spare->id(), lastChild), childVarIndices.back()); constraints.push_back(std::make_shared(leftC, std::make_shared(timePointVariables.at(i), childVarIndices.back()))); constraints.back()->setDescription("Last child & claimed -> SPARE fails"); @@ -397,11 +418,11 @@ namespace storm { // Check if next child is availble (first part of case distinction for constraint 7) std::vector> ifcs; // Next child is not yet failed - ifcs.push_back(std::make_shared(timeCurrChild, timeNextChild)); + ifcs.push_back(std::make_shared(timeCurrChild, timeNextChild)); // Child is not yet claimed by a different spare for (auto const& otherSpare : children.at(nextChild)->parents()) { if (otherSpare->id() == i) { - // not an OTHER spare. + // not a different spare. continue; } ifcs.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), children.at(nextChild)->id()), notFailed)); @@ -413,7 +434,7 @@ namespace storm { // Next iteration of phi oldPhi = tryClaimC; // If i-th child fails after being claimed, then try to claim (i+1)-th child (constraint 6) - constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), timeCurrChild), tryClaimC)); + constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), timeCurrChild), tryClaimC)); constraints.back()->setDescription("Try to claim " + std::to_string(nextChild+1) + "th child"); } break; @@ -423,6 +444,31 @@ namespace storm { break; } } + + // Only one spare can claim a child (constraint 8) + 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); + for (auto const& child : spare->children()) { + // No other spare claims this child + std::vector> noOtherClaims; + for (auto const& otherSpare : child->parents()) { + if (otherSpare->id() == spare->id()) { + // original spare + continue; + } + noOtherClaims.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), child->id()), notFailed)); + } + if (!noOtherClaims.empty()) { + std::shared_ptr leftC = std::make_shared(getClaimVariableIndex(spare->id(), child->id()), notFailed); + constraints.push_back(std::make_shared(leftC, std::make_shared(noOtherClaims))); + constraints.back()->setDescription("Only one spare claims the child " + child->name()); + } + } + } + } + // Toplevel element will not fail (part of constraint 13) constraints.push_back(std::make_shared(dft.getTopLevelIndex(), notFailed)); constraints.back()->setDescription("Toplevel element should not fail"); From d1d2925044b20d7734c1a4c28df1e3ca60e84ce9 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 22 Nov 2017 17:37:58 +0100 Subject: [PATCH 06/38] Throw exceptions for missing SMT encodings --- .../modelchecker/dft/DFTASFChecker.cpp | 20 +++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 246065266..4289dba8a 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -1,6 +1,8 @@ #include "DFTASFChecker.h" #include #include "storm/utility/file.h" +#include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/NotSupportedException.h" namespace storm { @@ -337,15 +339,15 @@ namespace storm { // Generate constraints - // No two BEs fail at the same time (first part of constraint 12) - constraints.push_back(std::make_shared(beVariables)); - constraints.back()->setDescription("No two BEs fail at the same time"); - - // All BEs have to fail (second part of constraint 12) + // All BEs have to fail (first part of constraint 12) for (auto const& beV : beVariables) { constraints.push_back(std::make_shared(beV, 1, dft.nrBasicElements())); } + // No two BEs fail at the same time (second part of constraint 12) + constraints.push_back(std::make_shared(beVariables)); + constraints.back()->setDescription("No two BEs fail at the same time"); + // Initialize claim variables in [1, |BE|+1] for (auto const& claimVariable : claimVariables) { constraints.push_back(std::make_shared(claimVariable.second, 0, notFailed)); @@ -387,6 +389,9 @@ namespace storm { constraints.push_back(std::make_shared(ifC, thenC, elseC)); constraints.back()->setDescription("PAND gate"); } + case storm::storage::DFTElementType::SEQ: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "SMT encoding of SEQs is not implemented yet."); + break; case storm::storage::DFTElementType::SPARE: { auto spare = std::static_pointer_cast const>(element); @@ -439,8 +444,11 @@ namespace storm { } break; } + case storm::storage::DFTElementType::PDEP: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "SMT encoding of FDEPs and PDEPs is not implemented yet."); + break; default: - STORM_LOG_WARN("DFT element of type '" << element->type() << "' is ignored for SMT encoding."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "SMT encoding for type '" << element->type() << "' is not supported."); break; } } From 1affccbf81d1596c25dc5abbec3edac9a481bc34 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 23 Nov 2017 16:35:40 +0100 Subject: [PATCH 07/38] Fixed encoding of PAND --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 4289dba8a..7f26ed62d 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -384,7 +384,7 @@ namespace storm { { // Constraint for PAND gate (constraint 3) std::shared_ptr ifC = std::make_shared(childVarIndices); - std::shared_ptr thenC = std::make_shared(timePointVariables.at(i), timePointVariables.at(childVarIndices.back())); + std::shared_ptr thenC = std::make_shared(timePointVariables.at(i), childVarIndices.back()); std::shared_ptr elseC = std::make_shared(timePointVariables.at(i), notFailed); constraints.push_back(std::make_shared(ifC, thenC, elseC)); constraints.back()->setDescription("PAND gate"); From 623ce0ccf1d3a89ac0754df4998da240f61843d1 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 23 Nov 2017 17:19:04 +0100 Subject: [PATCH 08/38] Fixed missing break in case distinction --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 7f26ed62d..f99cc23aa 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -388,6 +388,7 @@ namespace storm { std::shared_ptr elseC = std::make_shared(timePointVariables.at(i), notFailed); constraints.push_back(std::make_shared(ifC, thenC, elseC)); constraints.back()->setDescription("PAND gate"); + break; } case storm::storage::DFTElementType::SEQ: STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "SMT encoding of SEQs is not implemented yet."); From b6d3b0242f56213f689eeec55e1226505583550c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 23 Nov 2017 17:38:10 +0100 Subject: [PATCH 09/38] Fixed encoding for toplevel element --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index f99cc23aa..fd1db1421 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -479,7 +479,7 @@ namespace storm { } // Toplevel element will not fail (part of constraint 13) - constraints.push_back(std::make_shared(dft.getTopLevelIndex(), notFailed)); + constraints.push_back(std::make_shared(timePointVariables.at(dft.getTopLevelIndex()), notFailed)); constraints.back()->setDescription("Toplevel element should not fail"); } From 7d56572ebac68210f0f6b42cd796c2de02bf2d60 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Nov 2017 10:13:49 +0100 Subject: [PATCH 10/38] Recursive method for generating constrainst for 'trying to claim' --- .../modelchecker/dft/DFTASFChecker.cpp | 68 +++++++++++-------- .../modelchecker/dft/DFTASFChecker.h | 13 ++++ 2 files changed, 52 insertions(+), 29 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index fd1db1421..f112d2436 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -311,7 +311,7 @@ namespace storm { void DFTASFChecker::convert() { std::vector beVariables; - uint64_t notFailed = dft.nrBasicElements()+1; // Value indicating the element is not failed + notFailed = dft.nrBasicElements()+1; // Value indicating the element is not failed // Initialize variables for (size_t i = 0; i < dft.nrElements(); ++i) { @@ -410,38 +410,14 @@ namespace storm { constraints.back()->setDescription("Last child & claimed -> SPARE fails"); // Construct constraint for trying to claim next child - // We recursively build the function phi^s_i - // Last child: spare fails at same point as second to last child (otherwise case in constraint 7) - std::shared_ptr oldPhi = std::make_shared(timePointVariables.at(i), childVarIndices.at(children.size() - 2)); STORM_LOG_ASSERT(children.size() >= 2, "Spare has only one child"); - for (uint64_t j = 0; j+1 < children.size(); ++j) { - uint64_t currChild = children.size() - 2 - j; - uint64_t nextChild = currChild + 1; + for (uint64_t currChild = 0; currChild < children.size() - 1; ++currChild) { uint64_t timeCurrChild = childVarIndices.at(currChild); // Moment when current child fails - uint64_t timeNextChild = childVarIndices.at(nextChild); // Moment when next child fails - uint64_t claimNextChild = getClaimVariableIndex(spare->id(), childVarIndices.at(nextChild)); // Moment the spare claims the next child - - // Check if next child is availble (first part of case distinction for constraint 7) - std::vector> ifcs; - // Next child is not yet failed - ifcs.push_back(std::make_shared(timeCurrChild, timeNextChild)); - // Child is not yet claimed by a different spare - for (auto const& otherSpare : children.at(nextChild)->parents()) { - if (otherSpare->id() == i) { - // not a different spare. - continue; - } - ifcs.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), children.at(nextChild)->id()), notFailed)); - } - // Claim next child (constraint 7) - // oldPhi contains the constraints for the recursive call to phi^s_{i+1} - std::shared_ptr tryClaimC = std::make_shared(std::make_shared(ifcs), std::make_shared(claimNextChild, timeCurrChild), oldPhi); - // Next iteration of phi - oldPhi = tryClaimC; - // If i-th child fails after being claimed, then try to claim (i+1)-th child (constraint 6) + // If i-th child fails after being claimed, then try to claim next child (constraint 6) + std::shared_ptr tryClaimC = generateTryToClaimConstraint(spare, currChild + 1, timeCurrChild); constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), timeCurrChild), tryClaimC)); - constraints.back()->setDescription("Try to claim " + std::to_string(nextChild+1) + "th child"); + constraints.back()->setDescription("Try to claim " + std::to_string(currChild+2) + "th child"); } break; } @@ -483,6 +459,40 @@ namespace storm { constraints.back()->setDescription("Toplevel element should not fail"); } + std::shared_ptr DFTASFChecker::generateTryToClaimConstraint(std::shared_ptr const> spare, uint64_t childIndex, uint64_t timepoint) const { + auto child = spare->children().at(childIndex); + uint64_t timeChild = timePointVariables.at(child->id()); // Moment when the child fails + uint64_t claimChild = getClaimVariableIndex(spare->id(), child->id()); // Moment the spare claims the child + + std::vector> noClaimingPossible; + if (childIndex + 1 < spare->children().size()) { + // Consider next child for claiming (second case in constraint 7) + noClaimingPossible.push_back(generateTryToClaimConstraint(spare, childIndex+1, timepoint)); + } else { + // Last child: spare fails at same point as this child (third case in constraint 7) + noClaimingPossible.push_back(std::make_shared(timePointVariables.at(spare->id()), timepoint)); + } + std::shared_ptr elseCaseC = std::make_shared(noClaimingPossible); + + // Check if next child is availble (first case in constraint 7) + std::vector> claimingPossibleC; + // Next child is not yet failed + claimingPossibleC.push_back(std::make_shared(timepoint, timeChild)); + // Child is not yet claimed by a different spare + for (auto const& otherSpare : child->parents()) { + if (otherSpare->id() == spare->id()) { + // not a different spare. + continue; + } + claimingPossibleC.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), child->id()), notFailed)); + } + + // Claim child if available + std::shared_ptr firstCaseC = std::make_shared(std::make_shared(claimingPossibleC), std::make_shared(claimChild, timepoint), elseCaseC); + return firstCaseC; + } + + void DFTASFChecker::toFile(std::string const& filename) { std::ofstream stream; storm::utility::openFile(filename, stream); diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index f05bd6595..d9331511b 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -50,12 +50,25 @@ namespace storm { private: uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; + + /** + * Generate constraint for 'spare (s) tries to claim the child (i) at the given timepoint (t)'. + * This corresponds to the function \phi^s_i(t) in constraint 7. + * + * @param spare Spare. + * @param childIndex Index of child to consider in spare children. + * @param timepoint Timepoint to try to claim. + * + * @return Constraint encoding the claiming. + */ + std::shared_ptr generateTryToClaimConstraint(std::shared_ptr const> spare, uint64_t childIndex, uint64_t timepoint) const; storm::storage::DFT const& dft; std::vector varNames; std::unordered_map timePointVariables; std::vector> constraints; std::map claimVariables; + uint64_t notFailed; }; } } From 275a191b0840df847a8f40f4b361e028fde605e8 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Nov 2017 10:17:41 +0100 Subject: [PATCH 11/38] Fixed spare claiming by adding missing constraint 'if the child is not claimed at the moment, it will never be claimed'. --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index f112d2436..ae70b1317 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -465,6 +465,8 @@ namespace storm { uint64_t claimChild = getClaimVariableIndex(spare->id(), child->id()); // Moment the spare claims the child std::vector> noClaimingPossible; + // Child cannot be claimed. + noClaimingPossible.push_back(std::make_shared(claimChild, notFailed)); if (childIndex + 1 < spare->children().size()) { // Consider next child for claiming (second case in constraint 7) noClaimingPossible.push_back(generateTryToClaimConstraint(spare, childIndex+1, timepoint)); From f675d60cccfaf7758041ff93e5e0a651b1b9cc81 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Nov 2017 10:32:24 +0100 Subject: [PATCH 12/38] Added assertion --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index ae70b1317..fa5ada44c 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -356,6 +356,7 @@ namespace storm { // Encoding for gates for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); + STORM_LOG_ASSERT(i == element->id(), "Id and index should match."); // Get indices for gate children std::vector childVarIndices; From 89984abdaf1750aec6f96f4ce9ae03b9282e8f66 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Nov 2017 17:50:27 +0100 Subject: [PATCH 13/38] Fixed spare claiming problem by asserting that only operational elements can be claimed --- .../modelchecker/dft/DFTASFChecker.cpp | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index fa5ada44c..98ccc8ae4 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -432,25 +432,26 @@ namespace storm { } // Only one spare can claim a child (constraint 8) + // and only not failed childs can be claimed (addition to constrain 8) 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); for (auto const& child : spare->children()) { + std::vector> additionalC; + uint64_t timeClaiming = getClaimVariableIndex(spare->id(), child->id()); + std::shared_ptr leftC = std::make_shared(timeClaiming, notFailed); + // Child must be operational at time of claiming + additionalC.push_back(std::make_shared(timeClaiming, timePointVariables.at(child->id()))); // No other spare claims this child - std::vector> noOtherClaims; for (auto const& otherSpare : child->parents()) { - if (otherSpare->id() == spare->id()) { - // original spare - continue; + if (otherSpare->id() != spare->id()) { + // Different spare + additionalC.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), child->id()), notFailed)); } - noOtherClaims.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), child->id()), notFailed)); - } - if (!noOtherClaims.empty()) { - std::shared_ptr leftC = std::make_shared(getClaimVariableIndex(spare->id(), child->id()), notFailed); - constraints.push_back(std::make_shared(leftC, std::make_shared(noOtherClaims))); - constraints.back()->setDescription("Only one spare claims the child " + child->name()); } + constraints.push_back(std::make_shared(leftC, std::make_shared(additionalC))); + constraints.back()->setDescription("Child " + child->name() + " must be operational at time of claiming by spare " + spare->name() + " and can only be claimed by one spare."); } } } @@ -467,7 +468,6 @@ namespace storm { std::vector> noClaimingPossible; // Child cannot be claimed. - noClaimingPossible.push_back(std::make_shared(claimChild, notFailed)); if (childIndex + 1 < spare->children().size()) { // Consider next child for claiming (second case in constraint 7) noClaimingPossible.push_back(generateTryToClaimConstraint(spare, childIndex+1, timepoint)); From 0efa16876b50064b379100e04c08a99310813b6b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Nov 2017 18:08:01 +0100 Subject: [PATCH 14/38] Started on encoding for FDEPs by implementing constraint (9) --- .../modelchecker/dft/DFTASFChecker.cpp | 65 ++++++++++++++++++- .../modelchecker/dft/DFTASFChecker.h | 7 ++ 2 files changed, 71 insertions(+), 1 deletion(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 98ccc8ae4..94b6c308c 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -155,6 +155,31 @@ namespace storm { }; + class IsBoolValue : public DFTConstraint { + public: + IsBoolValue(uint64_t varIndex, bool val) : varIndex(varIndex), value(val) { + } + + virtual ~IsBoolValue() { + } + + std::string toSmtlib2(std::vector const& varNames) const override { + std::stringstream sstr; + assert(varIndex < varNames.size()); + if (value) { + sstr << varNames.at(varIndex); + } else { + sstr << "(not " << varNames.at(varIndex) << ")"; + } + return sstr.str(); + } + + private: + uint64_t varIndex; + bool value; + }; + + class IsConstantValue : public DFTConstraint { public: IsConstantValue(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) { @@ -335,6 +360,11 @@ namespace storm { break; } } + // Initialize variables indicating Markovian states + for (size_t i = 0; i < dft.nrBasicElements() - 1; ++i) { + varNames.push_back("m_" + std::to_string(i)); + markovianVariables.emplace(i, varNames.size() - 1); + } // Generate constraints @@ -423,7 +453,7 @@ namespace storm { break; } case storm::storage::DFTElementType::PDEP: - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "SMT encoding of FDEPs and PDEPs is not implemented yet."); + // FDEPs are considered later in the Markovian constraints break; default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "SMT encoding for type '" << element->type() << "' is not supported."); @@ -456,6 +486,9 @@ namespace storm { } } + // Handle dependencies + addMarkovianConstraints(); + // Toplevel element will not fail (part of constraint 13) constraints.push_back(std::make_shared(timePointVariables.at(dft.getTopLevelIndex()), notFailed)); constraints.back()->setDescription("Toplevel element should not fail"); @@ -495,6 +528,32 @@ namespace storm { return firstCaseC; } + void DFTASFChecker::addMarkovianConstraints() { + // This vector contains Markovian constraints for each timepoint + std::vector>> markovianC(dft.nrBasicElements() -1); + + for (size_t j = 0; j < dft.nrElements(); ++j) { + std::shared_ptr const> element = dft.getElement(j); + if (element->hasOutgoingDependencies()) { + for (uint64_t i = 0; i < dft.nrBasicElements() -1; ++i) { + // All dependent events of a failed trigger have failed as well (constraint 9) + std::shared_ptr triggerFailed = std::make_shared(timePointVariables.at(j), i); + std::vector> depFailed; + for (auto const& dependency : element->outgoingDependencies()) { + for (auto const& depElement : dependency->dependentEvents()) { + depFailed.push_back(std::make_shared(timePointVariables.at(depElement->id()), i)); + } + } + markovianC[i].push_back(std::make_shared(triggerFailed, std::make_shared(depFailed))); + } + } + } + for (uint64_t i = 0; i < dft.nrBasicElements() - 1; ++i) { + constraints.push_back(std::make_shared(std::make_shared(markovianVariables.at(i), true), std::make_shared(markovianC[i]))); + constraints.back()->setDescription("Markovian (" + std::to_string(i) + ") iff all dependent events which trigger failed also failed."); + } + } + void DFTASFChecker::toFile(std::string const& filename) { std::ofstream stream; @@ -507,6 +566,10 @@ namespace storm { for (auto const& claimVarEntry : claimVariables) { stream << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl; } + stream << "; Markovian variables" << std::endl; + for (auto const& markovianVarEntry : markovianVariables) { + stream << "(declare-fun " << varNames[markovianVarEntry.second] << "() Bool)" << std::endl; + } for (auto const& constraint : constraints) { if (!constraint->description().empty()) { stream << "; " << constraint->description() << std::endl; diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index d9331511b..af4f257ca 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -62,12 +62,19 @@ namespace storm { * @return Constraint encoding the claiming. */ std::shared_ptr generateTryToClaimConstraint(std::shared_ptr const> spare, uint64_t childIndex, uint64_t timepoint) const; + + /** + * Add constraints encoding Markovian states. + * This corresponds to constraints (9), (10) and (11) + */ + void addMarkovianConstraints(); storm::storage::DFT const& dft; std::vector varNames; std::unordered_map timePointVariables; std::vector> constraints; std::map claimVariables; + std::unordered_map markovianVariables; uint64_t notFailed; }; } From e8a950d9d77b17b7dad0aac6d6780fd10d689882 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Nov 2017 18:27:32 +0100 Subject: [PATCH 15/38] Support for conjunction over empty set --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 94b6c308c..35afa7cb8 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -107,11 +107,15 @@ namespace storm { std::string toSmtlib2(std::vector const& varNames) const override { std::stringstream sstr; - sstr << "(and"; - for(auto const& c : constraints) { - sstr << " " << c->toSmtlib2(varNames); + if (constraints.empty()) { + sstr << "true"; + } else { + sstr << "(and"; + for(auto const& c : constraints) { + sstr << " " << c->toSmtlib2(varNames); + } + sstr << ")"; } - sstr << ")"; return sstr.str(); } From 1c90f3829fd9c1e42b837e187dc5d2ecb4fcc60c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Nov 2017 18:46:50 +0100 Subject: [PATCH 16/38] Added constraints 10 --- .../modelchecker/dft/DFTASFChecker.cpp | 84 +++++++++++++++++-- 1 file changed, 79 insertions(+), 5 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 35afa7cb8..c5ebcef2e 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -101,7 +101,8 @@ namespace storm { class And : public DFTConstraint { public: - And(std::vector> const& constraints) : constraints(constraints) {} + And(std::vector> const& constraints) : constraints(constraints) { + } virtual ~And() { } @@ -125,6 +126,34 @@ namespace storm { }; + class Or : public DFTConstraint { + public: + Or(std::vector> const& constraints) : constraints(constraints) { + } + + virtual ~Or() { + } + + std::string toSmtlib2(std::vector const& varNames) const override { + std::stringstream sstr; + if (constraints.empty()) { + sstr << "false"; + } else { + sstr << "(or"; + for(auto const& c : constraints) { + sstr << " " << c->toSmtlib2(varNames); + } + sstr << ")"; + } + return sstr.str(); + } + + private: + std::vector> constraints; + + }; + + class Implies : public DFTConstraint { public: Implies(std::shared_ptr l, std::shared_ptr r) : lhs(l), rhs(r) { @@ -225,6 +254,26 @@ namespace storm { uint64_t value; }; + class IsLessEqualConstant : public DFTConstraint { + public: + IsLessEqualConstant(uint64_t varIndex, uint64_t val) :varIndex(varIndex), value(val) { + } + + virtual ~IsLessEqualConstant() { + } + + 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: @@ -533,19 +582,20 @@ namespace storm { } void DFTASFChecker::addMarkovianConstraints() { - // This vector contains Markovian constraints for each timepoint + // Vector containing (non-)Markovian constraints for each timepoint std::vector>> markovianC(dft.nrBasicElements() -1); + std::vector>> nonMarkovianC(dft.nrBasicElements() -1); + // All dependent events of a failed trigger have failed as well (constraint 9) for (size_t j = 0; j < dft.nrElements(); ++j) { std::shared_ptr const> element = dft.getElement(j); if (element->hasOutgoingDependencies()) { for (uint64_t i = 0; i < dft.nrBasicElements() -1; ++i) { - // All dependent events of a failed trigger have failed as well (constraint 9) - std::shared_ptr triggerFailed = std::make_shared(timePointVariables.at(j), i); + std::shared_ptr triggerFailed = std::make_shared(timePointVariables.at(j), i); std::vector> depFailed; for (auto const& dependency : element->outgoingDependencies()) { for (auto const& depElement : dependency->dependentEvents()) { - depFailed.push_back(std::make_shared(timePointVariables.at(depElement->id()), i)); + depFailed.push_back(std::make_shared(timePointVariables.at(depElement->id()), i)); } } markovianC[i].push_back(std::make_shared(triggerFailed, std::make_shared(depFailed))); @@ -556,6 +606,30 @@ namespace storm { constraints.push_back(std::make_shared(std::make_shared(markovianVariables.at(i), true), std::make_shared(markovianC[i]))); constraints.back()->setDescription("Markovian (" + std::to_string(i) + ") iff all dependent events which trigger failed also failed."); } + + // In non-Markovian steps the next failed element is a dependent BE (constraint 10) + for (size_t j = 0; j < dft.nrElements(); ++j) { + std::shared_ptr const> element = dft.getElement(j); + if (element->isBasicElement()) { + auto be = std::static_pointer_cast const>(element); + + if (be->hasIngoingDependencies()) { + for (uint64_t i = 0; i < dft.nrBasicElements() -1; ++i) { + std::shared_ptr nextFailure = std::make_shared(timePointVariables.at(j), i+1); + std::vector> triggerFailed; + for (auto const& dependency : be->ingoingDependencies()) { + triggerFailed.push_back(std::make_shared(timePointVariables.at(dependency->triggerEvent()->id()), i)); + } + nonMarkovianC[i].push_back(std::make_shared(nextFailure, std::make_shared(triggerFailed))); + } + } + } + } + for (uint64_t i = 0; i < dft.nrBasicElements() - 1; ++i) { + constraints.push_back(std::make_shared(std::make_shared(markovianVariables.at(i), false), std::make_shared(nonMarkovianC[i]))); + constraints.back()->setDescription("Non-Markovian (" + std::to_string(i) + ") -> next failure is dependent BE."); + } + } From ccee1bb007f51cf955f47cdebfe81a5244f7f014 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Nov 2017 19:21:35 +0100 Subject: [PATCH 17/38] Added last constraint 11 for Fdeps --- .../modelchecker/dft/DFTASFChecker.cpp | 54 ++++++++++++++++--- 1 file changed, 47 insertions(+), 7 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index c5ebcef2e..da968b7a9 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -188,6 +188,25 @@ namespace storm { }; + class IsTrue : public DFTConstraint { + public: + IsTrue(bool val) :value(val) { + } + + virtual ~IsTrue() { + } + + std::string toSmtlib2(std::vector const& varNames) const override { + std::stringstream sstr; + sstr << (value ? "true" : "false"); + return sstr.str(); + } + + private: + bool value; + }; + + class IsBoolValue : public DFTConstraint { public: IsBoolValue(uint64_t varIndex, bool val) : varIndex(varIndex), value(val) { @@ -414,7 +433,7 @@ namespace storm { } } // Initialize variables indicating Markovian states - for (size_t i = 0; i < dft.nrBasicElements() - 1; ++i) { + for (size_t i = 0; i < dft.nrBasicElements(); ++i) { varNames.push_back("m_" + std::to_string(i)); markovianVariables.emplace(i, varNames.size() - 1); } @@ -582,15 +601,17 @@ namespace storm { } void DFTASFChecker::addMarkovianConstraints() { + uint64_t nrMarkovian = dft.nrBasicElements(); // Vector containing (non-)Markovian constraints for each timepoint - std::vector>> markovianC(dft.nrBasicElements() -1); - std::vector>> nonMarkovianC(dft.nrBasicElements() -1); + std::vector>> markovianC(nrMarkovian); + std::vector>> nonMarkovianC(nrMarkovian); + std::vector>> notColdC(nrMarkovian); // All dependent events of a failed trigger have failed as well (constraint 9) for (size_t j = 0; j < dft.nrElements(); ++j) { std::shared_ptr const> element = dft.getElement(j); if (element->hasOutgoingDependencies()) { - for (uint64_t i = 0; i < dft.nrBasicElements() -1; ++i) { + for (uint64_t i = 0; i < nrMarkovian; ++i) { std::shared_ptr triggerFailed = std::make_shared(timePointVariables.at(j), i); std::vector> depFailed; for (auto const& dependency : element->outgoingDependencies()) { @@ -602,7 +623,7 @@ namespace storm { } } } - for (uint64_t i = 0; i < dft.nrBasicElements() - 1; ++i) { + for (uint64_t i = 0; i < nrMarkovian; ++i) { constraints.push_back(std::make_shared(std::make_shared(markovianVariables.at(i), true), std::make_shared(markovianC[i]))); constraints.back()->setDescription("Markovian (" + std::to_string(i) + ") iff all dependent events which trigger failed also failed."); } @@ -614,7 +635,7 @@ namespace storm { auto be = std::static_pointer_cast const>(element); if (be->hasIngoingDependencies()) { - for (uint64_t i = 0; i < dft.nrBasicElements() -1; ++i) { + for (uint64_t i = 0; i < nrMarkovian -1; ++i) { std::shared_ptr nextFailure = std::make_shared(timePointVariables.at(j), i+1); std::vector> triggerFailed; for (auto const& dependency : be->ingoingDependencies()) { @@ -625,11 +646,30 @@ namespace storm { } } } - for (uint64_t i = 0; i < dft.nrBasicElements() - 1; ++i) { + for (uint64_t i = 0; i < nrMarkovian; ++i) { constraints.push_back(std::make_shared(std::make_shared(markovianVariables.at(i), false), std::make_shared(nonMarkovianC[i]))); constraints.back()->setDescription("Non-Markovian (" + std::to_string(i) + ") -> next failure is dependent BE."); } + // In Markovian steps the failure rate is positive (constraint 11) + for (size_t j = 0; j < dft.nrElements(); ++j) { + std::shared_ptr const> element = dft.getElement(j); + if (element->isBasicElement()) { + auto be = std::static_pointer_cast const>(element); + for (uint64_t i = 0; i < nrMarkovian; ++i) { + std::shared_ptr nextFailure = std::make_shared(timePointVariables.at(j), i+1); + // BE is not cold + // TODO: implement use of activation variables here + bool cold = storm::utility::isZero(be->activeFailureRate()); + notColdC[i].push_back(std::make_shared(nextFailure, std::make_shared(!cold))); + } + } + } + for (uint64_t i = 0; i < nrMarkovian; ++i) { + constraints.push_back(std::make_shared(std::make_shared(markovianVariables.at(i), true), std::make_shared(notColdC[i]))); + constraints.back()->setDescription("Markovian (" + std::to_string(i) + ") -> positive failure rate."); + } + } From b31aa5d463c0090eed6378e414b49f0c2bcab26b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Nov 2017 19:41:19 +0100 Subject: [PATCH 18/38] SMT support for POR gate --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index da968b7a9..364d6743a 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -493,6 +493,22 @@ namespace storm { constraints.back()->setDescription("PAND gate"); break; } + case storm::storage::DFTElementType::POR: + { + // Constraint for POR gate + // First child fails before all others + std::vector> firstSmallestC; + uint64_t timeFirstChild = childVarIndices.front(); + for (uint64_t i = 1; i < childVarIndices.size(); ++i) { + firstSmallestC.push_back(std::make_shared(timeFirstChild, childVarIndices.at(i))); + } + std::shared_ptr ifC = std::make_shared(firstSmallestC); + std::shared_ptr thenC = std::make_shared(timePointVariables.at(i), childVarIndices.front()); + std::shared_ptr elseC = std::make_shared(timePointVariables.at(i), notFailed); + constraints.push_back(std::make_shared(ifC, thenC, elseC)); + constraints.back()->setDescription("POR gate"); + break; + } case storm::storage::DFTElementType::SEQ: STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "SMT encoding of SEQs is not implemented yet."); break; From 0b4c093e81a1e801b5185737d8df8f2eb8cce104 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Nov 2017 19:46:01 +0100 Subject: [PATCH 19/38] Throw exception for VOT gates --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 364d6743a..60f6976d6 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -483,6 +483,10 @@ namespace storm { constraints.push_back(std::make_shared(timePointVariables.at(i), childVarIndices)); constraints.back()->setDescription("OR gate"); break; + case storm::storage::DFTElementType::VOT: + //TODO implement via and/or construction + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "SMT encoding of VOTs is not implemented yet."); + break; case storm::storage::DFTElementType::PAND: { // Constraint for PAND gate (constraint 3) From 3987458ed84b94ddc7399928a761683314fa6198 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Nov 2017 20:00:45 +0100 Subject: [PATCH 20/38] Fixed bug in claiming by only considering spare parents --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 60f6976d6..06bfd1cca 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -566,10 +566,10 @@ namespace storm { // Child must be operational at time of claiming additionalC.push_back(std::make_shared(timeClaiming, timePointVariables.at(child->id()))); // No other spare claims this child - for (auto const& otherSpare : child->parents()) { - if (otherSpare->id() != spare->id()) { + for (auto const& parent : child->parents()) { + if (parent->isSpareGate() && parent->id() != spare->id()) { // Different spare - additionalC.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), child->id()), notFailed)); + additionalC.push_back(std::make_shared(getClaimVariableIndex(parent->id(), child->id()), notFailed)); } } constraints.push_back(std::make_shared(leftC, std::make_shared(additionalC))); From 7d464f580715227b4694d3ed70856a2714a6b9a2 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 27 Nov 2017 18:54:43 +0100 Subject: [PATCH 21/38] SMT encoding for voting gate via or/and construction --- .../modelchecker/dft/DFTASFChecker.cpp | 50 ++++++++++++++++--- .../modelchecker/dft/DFTASFChecker.h | 1 + 2 files changed, 44 insertions(+), 7 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 06bfd1cca..8704febe3 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -1,6 +1,7 @@ #include "DFTASFChecker.h" #include #include "storm/utility/file.h" +#include "storm/utility/bitoperations.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/NotSupportedException.h" @@ -476,17 +477,46 @@ namespace storm { case storm::storage::DFTElementType::AND: // Constraint for AND gate (constraint 1) constraints.push_back(std::make_shared(timePointVariables.at(i), childVarIndices)); - constraints.back()->setDescription("AND gate"); + constraints.back()->setDescription("AND gate " + element->name()); break; case storm::storage::DFTElementType::OR: // Constraint for OR gate (constraint 2) constraints.push_back(std::make_shared(timePointVariables.at(i), childVarIndices)); - constraints.back()->setDescription("OR gate"); + constraints.back()->setDescription("OR gate " + element->name()); break; case storm::storage::DFTElementType::VOT: - //TODO implement via and/or construction - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "SMT encoding of VOTs is not implemented yet."); + { + // VOTs are implemented via OR over ANDs with all possible combinations + auto vot = std::static_pointer_cast const>(element); + std::vector tmpVars; + size_t i = 0; + // Generate all permutations of k out of n + size_t combination = smallestIntWithNBitsSet(static_cast(vot->threshold())); + do { + // Construct selected children from combination + std::vector combinationChildren; + for (size_t j = 0; j < vot->nrChildren(); ++j) { + if (combination & (1 << j)) { + combinationChildren.push_back(childVarIndices.at(j)); + } + } + // Introduce temporary variable for this AND + varNames.push_back("v_" + vot->name() + "_" + std::to_string(i)); + tmpVars.push_back(varNames.size() - 1); + tmpTimePointVariables.push_back(varNames.size() - 1); + // AND over the selected children + constraints.push_back(std::make_shared(tmpVars.at(i), combinationChildren)); + constraints.back()->setDescription("VOT gate " + element->name() + ": AND no. " + std::to_string(i)); + // Generate next permutation + combination = nextBitPermutation(combination); + ++i; + } while(combination < (1 << vot->nrChildren()) && combination != 0); + + // Constraint is OR over all possible combinations + constraints.push_back(std::make_shared(timePointVariables.at(i), tmpVars)); + constraints.back()->setDescription("VOT gate " + element->name() + ": OR"); break; + } case storm::storage::DFTElementType::PAND: { // Constraint for PAND gate (constraint 3) @@ -494,7 +524,7 @@ namespace storm { std::shared_ptr thenC = std::make_shared(timePointVariables.at(i), childVarIndices.back()); std::shared_ptr elseC = std::make_shared(timePointVariables.at(i), notFailed); constraints.push_back(std::make_shared(ifC, thenC, elseC)); - constraints.back()->setDescription("PAND gate"); + constraints.back()->setDescription("PAND gate " + element->name()); break; } case storm::storage::DFTElementType::POR: @@ -510,7 +540,7 @@ namespace storm { std::shared_ptr thenC = std::make_shared(timePointVariables.at(i), childVarIndices.front()); std::shared_ptr elseC = std::make_shared(timePointVariables.at(i), notFailed); constraints.push_back(std::make_shared(ifC, thenC, elseC)); - constraints.back()->setDescription("POR gate"); + constraints.back()->setDescription("POR gate " + element->name()); break; } case storm::storage::DFTElementType::SEQ: @@ -525,7 +555,7 @@ namespace storm { // First child of each spare is claimed in the beginning constraints.push_back(std::make_shared(getClaimVariableIndex(spare->id(), firstChild), 0)); - constraints.back()->setDescription("SPARE " + spare->name() + " claims first child"); + constraints.back()->setDescription("SPARE gate " + spare->name() + " claims first child"); // If last child is claimed before failure, then the spare fails when the last child fails (constraint 5) std::shared_ptr leftC = std::make_shared(getClaimVariableIndex(spare->id(), lastChild), childVarIndices.back()); @@ -708,6 +738,12 @@ namespace storm { for (auto const& markovianVarEntry : markovianVariables) { stream << "(declare-fun " << varNames[markovianVarEntry.second] << "() Bool)" << std::endl; } + if (!tmpTimePointVariables.empty()) { + stream << "; Temporary variables" << std::endl; + for (auto const& tmpVar : tmpTimePointVariables) { + stream << "(declare-fun " << varNames[tmpVar] << "() Int)" << std::endl; + } + } for (auto const& constraint : constraints) { if (!constraint->description().empty()) { stream << "; " << constraint->description() << std::endl; diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index af4f257ca..33f209957 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -75,6 +75,7 @@ namespace storm { std::vector> constraints; std::map claimVariables; std::unordered_map markovianVariables; + std::vector tmpTimePointVariables; uint64_t notFailed; }; } From e99e5bf6bfd66292b1acde051a7046bae83d716c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 28 Nov 2017 15:56:50 +0100 Subject: [PATCH 22/38] Fixed typo leading to wrong variables in SMT encoding --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 8704febe3..56e7671b5 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -505,7 +505,7 @@ namespace storm { tmpVars.push_back(varNames.size() - 1); tmpTimePointVariables.push_back(varNames.size() - 1); // AND over the selected children - constraints.push_back(std::make_shared(tmpVars.at(i), combinationChildren)); + constraints.push_back(std::make_shared(timePointVariables.at(i), combinationChildren)); constraints.back()->setDescription("VOT gate " + element->name() + ": AND no. " + std::to_string(i)); // Generate next permutation combination = nextBitPermutation(combination); From 09797dae5a5c883de0903c46afc844b83b81131d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 30 May 2018 17:17:31 +0200 Subject: [PATCH 23/38] SMT encoding for SEQ gate --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 56e7671b5..de653752d 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -544,8 +544,18 @@ namespace storm { break; } case storm::storage::DFTElementType::SEQ: - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "SMT encoding of SEQs is not implemented yet."); + { + // Constraint for SEQ gate (constraint 4) + // As the restriction is not a gate we have to enumerate its children here + auto seq = std::static_pointer_cast const>(element); + for (auto const& child : seq->children()) { + childVarIndices.push_back(timePointVariables.at(child->id())); + } + + constraints.push_back(std::make_shared(childVarIndices)); + constraints.back()->setDescription("SEQ gate " + element->name()); break; + } case storm::storage::DFTElementType::SPARE: { auto spare = std::static_pointer_cast const>(element); From 1461ba9073d4431f12d603697770e3feeccd36fd Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 5 Jun 2018 22:49:58 +0200 Subject: [PATCH 24/38] Fixed SMT encoding of voting gate --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index de653752d..41f688da0 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -489,7 +489,7 @@ namespace storm { // VOTs are implemented via OR over ANDs with all possible combinations auto vot = std::static_pointer_cast const>(element); std::vector tmpVars; - size_t i = 0; + size_t k = 0; // Generate all permutations of k out of n size_t combination = smallestIntWithNBitsSet(static_cast(vot->threshold())); do { @@ -501,15 +501,16 @@ namespace storm { } } // Introduce temporary variable for this AND - varNames.push_back("v_" + vot->name() + "_" + std::to_string(i)); - tmpVars.push_back(varNames.size() - 1); - tmpTimePointVariables.push_back(varNames.size() - 1); + varNames.push_back("v_" + vot->name() + "_" + std::to_string(k)); + size_t index = varNames.size() - 1; + tmpVars.push_back(index); + tmpTimePointVariables.push_back(index); // AND over the selected children - constraints.push_back(std::make_shared(timePointVariables.at(i), combinationChildren)); - constraints.back()->setDescription("VOT gate " + element->name() + ": AND no. " + std::to_string(i)); + constraints.push_back(std::make_shared(index, combinationChildren)); + constraints.back()->setDescription("VOT gate " + element->name() + ": AND no. " + std::to_string(k)); // Generate next permutation combination = nextBitPermutation(combination); - ++i; + ++k; } while(combination < (1 << vot->nrChildren()) && combination != 0); // Constraint is OR over all possible combinations From fef4b694d443cf6dabd49095bf02ba57f499facf Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 1 Oct 2018 16:36:24 +0200 Subject: [PATCH 25/38] topo sort: add first states --- src/storm/utility/graph.cpp | 103 ++++++++++++++++++++---------------- src/storm/utility/graph.h | 2 +- 2 files changed, 57 insertions(+), 48 deletions(-) diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 63dd4e592..193f6a5a5 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1554,9 +1554,56 @@ namespace storm { return SymbolicGameProb01Result(maybePlayer1States, maybePlayer2States, player1StrategyBdd, player2StrategyBdd); } - + + + template + void topologicalSortHelper(storm::storage::SparseMatrix const& matrix, uint64_t state, std::vector& topologicalSort, std::vector& recursionStack, std::vector::const_iterator>& iteratorRecursionStack, storm::storage::BitVector& visitedStates) { + if (!visitedStates.get(state)) { + recursionStack.push_back(state); + iteratorRecursionStack.push_back(matrix.begin(state)); + + recursionStepForward: + while (!recursionStack.empty()) { + uint_fast64_t currentState = recursionStack.back(); + typename storm::storage::SparseMatrix::const_iterator successorIterator = iteratorRecursionStack.back(); + + visitedStates.set(currentState, true); + + recursionStepBackward: + for (; successorIterator != matrix.end(currentState); ++successorIterator) { + if (!visitedStates.get(successorIterator->getColumn())) { + // Put unvisited successor on top of our recursion stack and remember that. + recursionStack.push_back(successorIterator->getColumn()); + + // Also, put initial value for iterator on corresponding recursion stack. + iteratorRecursionStack.push_back(matrix.begin(successorIterator->getColumn())); + + goto recursionStepForward; + } + } + + topologicalSort.push_back(currentState); + + // If we reach this point, we have completed the recursive descent for the current state. + // That is, we need to pop it from the recursion stacks. + recursionStack.pop_back(); + iteratorRecursionStack.pop_back(); + + // If there is at least one state under the current one in our recursion stack, we need + // to restore the topmost state as the current state and jump to the part after the + // original recursive call. + if (recursionStack.size() > 0) { + currentState = recursionStack.back(); + successorIterator = iteratorRecursionStack.back(); + + goto recursionStepBackward; + } + } + } + } + template - std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) { + std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, std::vector const& firstStates) { if (matrix.getRowCount() != matrix.getColumnCount()) { STORM_LOG_ERROR("Provided matrix is required to be square."); throw storm::exceptions::InvalidArgumentException() << "Provided matrix is required to be square."; @@ -1576,49 +1623,11 @@ namespace storm { // Perform a depth-first search over the given transitions and record states in the reverse order they were visited. storm::storage::BitVector visitedStates(numberOfStates); + for (auto const state : firstStates ) { + topologicalSortHelper(matrix, state, topologicalSort, recursionStack, iteratorRecursionStack, visitedStates); + } for (uint_fast64_t state = 0; state < numberOfStates; ++state) { - if (!visitedStates.get(state)) { - recursionStack.push_back(state); - iteratorRecursionStack.push_back(matrix.begin(state)); - - recursionStepForward: - while (!recursionStack.empty()) { - uint_fast64_t currentState = recursionStack.back(); - typename storm::storage::SparseMatrix::const_iterator successorIterator = iteratorRecursionStack.back(); - - visitedStates.set(currentState, true); - - recursionStepBackward: - for (; successorIterator != matrix.end(currentState); ++successorIterator) { - if (!visitedStates.get(successorIterator->getColumn())) { - // Put unvisited successor on top of our recursion stack and remember that. - recursionStack.push_back(successorIterator->getColumn()); - - // Also, put initial value for iterator on corresponding recursion stack. - iteratorRecursionStack.push_back(matrix.begin(successorIterator->getColumn())); - - goto recursionStepForward; - } - } - - topologicalSort.push_back(currentState); - - // If we reach this point, we have completed the recursive descent for the current state. - // That is, we need to pop it from the recursion stacks. - recursionStack.pop_back(); - iteratorRecursionStack.pop_back(); - - // If there is at least one state under the current one in our recursion stack, we need - // to restore the topmost state as the current state and jump to the part after the - // original recursive call. - if (recursionStack.size() > 0) { - currentState = recursionStack.back(); - successorIterator = iteratorRecursionStack.back(); - - goto recursionStepBackward; - } - } - } + topologicalSortHelper(matrix, state, topologicalSort, recursionStack, iteratorRecursionStack, visitedStates); } return topologicalSort; @@ -1696,7 +1705,7 @@ namespace storm { template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, boost::optional const& player1Candidates); - template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, std::vector const& firstStates) ; // Instantiations for storm::RationalNumber. #ifdef STORM_HAVE_CARL @@ -1752,7 +1761,7 @@ namespace storm { template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, boost::optional const& player1Candidates); - template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix); + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, std::vector const& firstStates); // End of instantiations for storm::RationalNumber. template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps, boost::optional const& choiceFilter); @@ -1804,7 +1813,7 @@ namespace storm { template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix); + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, std::vector const& firstStates); #endif diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 36b86ff69..d42a6be2f 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -683,7 +683,7 @@ namespace storm { * @return A vector of indices that is a topological sort of the states. */ template - std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; + std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, std::vector const& firstStates = {}) ; } // namespace graph } // namespace utility From 035bbd0952b4849ee0cc3e57b02fcf1cc5e07851 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 2 Oct 2018 18:53:44 +0200 Subject: [PATCH 26/38] removed spurious debugging output --- src/storm-parsers/parser/PrismParser.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index 68d8d77fb..4c0edbb34 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -561,7 +561,6 @@ namespace storm { bool observable = this->observables.count(variableName) > 0; if(observable) { this->observables.erase(variableName); - std::cout << variableName << " is observable." << std::endl; } return storm::prism::BooleanVariable(manager->getVariable(variableName), initialValueExpression, observable, this->getFilename()); } @@ -582,7 +581,6 @@ namespace storm { bool observable = this->observables.count(variableName) > 0; if(observable) { this->observables.erase(variableName); - std::cout << variableName << " is observable." << std::endl; } return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, observable, this->getFilename()); @@ -613,7 +611,6 @@ namespace storm { this->identifiers_.add(renamingPair->second, renamedVariable.getExpression()); if(this->observables.count(renamingPair->second) > 0) { this->observables.erase(renamingPair->second); - std::cout << renamingPair->second << " is observable." << std::endl; } } for (auto const& variable : moduleToRename.getIntegerVariables()) { @@ -623,7 +620,6 @@ namespace storm { this->identifiers_.add(renamingPair->second, renamedVariable.getExpression()); if(this->observables.count(renamingPair->second) > 0) { this->observables.erase(renamingPair->second); - std::cout << renamingPair->second << " is observable." << std::endl; } } @@ -666,7 +662,6 @@ namespace storm { bool observable = this->observables.count(renamingPair->second) > 0; if(observable) { this->observables.erase(renamingPair->second); - std::cout << renamingPair->second << " is observable." << std::endl; } booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), get_line(qi::_1))); } @@ -679,7 +674,6 @@ namespace storm { bool observable = this->observables.count(renamingPair->second) > 0; if(observable) { this->observables.erase(renamingPair->second); - std::cout << renamingPair->second << " is observable." << std::endl; } integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), get_line(qi::_1))); } From cc78629ddad7235f8aad1967373efa07af0d9635 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 2 Oct 2018 18:58:52 +0200 Subject: [PATCH 27/38] refer to storm-pomdp in changelog --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index eb2345e54..63f102b4d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,7 @@ Version 1.2.x - Added support for expected time properties for discrete time models - Bug fix in the parser for DRN (MDPs and MAs might have been affected). - Several bug fixes related to jani +- New binary `storm-pomdp` that handles the translation of POMDPs to pMCs. - `storm-gspn`: Improved .pnpro parser - `storm-gspn`: Added support for single/infinite/k-server semantics for GSPNs given in the .pnpro format - `storm-gspn`: Added option to set a global capacity for all places From 6102fd27ae469990bfaed50888c80011b7aba635 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 4 Oct 2018 10:26:32 +0200 Subject: [PATCH 28/38] Subsystembuilder can now handle deadlock states --- src/storm/transformer/SubsystemBuilder.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/storm/transformer/SubsystemBuilder.cpp b/src/storm/transformer/SubsystemBuilder.cpp index b8ba5f0e3..cfeba6b0e 100644 --- a/src/storm/transformer/SubsystemBuilder.cpp +++ b/src/storm/transformer/SubsystemBuilder.cpp @@ -65,7 +65,6 @@ namespace storm { result.keptActions = storm::storage::BitVector(originalModel.getTransitionMatrix().getRowCount(), false); for (auto subsysState : subsystemStates) { result.newToOldStateIndexMapping.push_back(subsysState); - bool stateHasOneChoiceLeft = false; for (uint_fast64_t row = subsystemActions.getNextSetIndex(originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState]); row < originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState+1]; row = subsystemActions.getNextSetIndex(row+1)) { bool allRowEntriesStayInSubsys = true; for (auto const& entry : originalModel.getTransitionMatrix().getRow(row)) { @@ -74,10 +73,8 @@ namespace storm { break; } } - stateHasOneChoiceLeft |= allRowEntriesStayInSubsys; result.keptActions.set(row, allRowEntriesStayInSubsys); } - STORM_LOG_THROW(stateHasOneChoiceLeft, storm::exceptions::InvalidArgumentException, "The subsystem would contain a deadlock state."); } // Transform the components of the model From 03c80f3ae1845e8f8d2034d5033309c0a4c33281 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 4 Oct 2018 10:27:43 +0200 Subject: [PATCH 29/38] correct treatment of non-trivial reward expressions --- src/storm-parsers/parser/JaniParser.cpp | 24 ++++++++++--- .../RewardAccumulationEliminationVisitor.cpp | 36 +++++++++++++------ src/storm/storage/jani/JSONExporter.cpp | 2 +- 3 files changed, 45 insertions(+), 17 deletions(-) diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index eba57d0dd..52677bfb0 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -205,7 +205,11 @@ namespace storm { STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array"); for(auto const& propertyEntry : parsedStructure.at("properties")) { try { + nonTrivialRewardModelExpressions.clear(); auto prop = this->parseProperty(propertyEntry, scope.refine("property[" + std::to_string(properties.size()) + "]")); + for (auto const& nonTrivRewExpr : nonTrivialRewardModelExpressions) { + model.addNonTrivialRewardExpression(nonTrivRewExpr.first, nonTrivRewExpr.second); + } // Eliminate reward accumulations as much as possible rewAccEliminator.eliminateRewardAccumulations(prop); properties.push_back(prop); @@ -321,7 +325,10 @@ namespace storm { STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a step-instant and a reward-instant in " + scope.description); storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), scope.refine("Step instant")); - if(rewardAccumulation.isEmpty()) { + if (!rewExpr.isVariable()) { + nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + } + if (rewardAccumulation.isEmpty()) { return std::make_shared(std::make_shared(stepInstantExpr, storm::logic::TimeBoundType::Steps), rewardName, opInfo); } else { return std::make_shared(std::make_shared(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps), rewardAccumulation), rewardName, opInfo); @@ -329,7 +336,10 @@ namespace storm { } else if (propertyStructure.count("time-instant") > 0) { STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a time-instant and a reward-instant in " + scope.description); storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), scope.refine("time instant")); - if(rewardAccumulation.isEmpty()) { + if (!rewExpr.isVariable()) { + nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + } + if (rewardAccumulation.isEmpty()) { return std::make_shared(std::make_shared(timeInstantExpr, storm::logic::TimeBoundType::Time), rewardName, opInfo); } else { return std::make_shared(std::make_shared(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time), rewardAccumulation), rewardName, opInfo); @@ -349,6 +359,9 @@ namespace storm { storm::expressions::Expression rewInstantExpr = parseExpression(rewInst.at("instant"), scope.refine("reward instant")); bounds.emplace_back(false, rewInstantExpr); } + if (!rewExpr.isVariable()) { + nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + } return std::make_shared(std::make_shared(bounds, boundReferences, rewardAccumulation), rewardName, opInfo); } else { time = !rewExpr.containsVariables() && storm::utility::isOne(rewExpr.evaluateAsRational()); @@ -363,12 +376,12 @@ namespace storm { assert(subformula->isTotalRewardFormula() || subformula->isTimePathFormula()); return std::make_shared(subformula, opInfo); } else { + if (!rewExpr.isVariable()) { + nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + } return std::make_shared(subformula, rewardName, opInfo); } } - if (!time && !rewExpr.isVariable()) { - nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); - } } else if (opString == "Smin" || opString == "Smax") { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported"); } else if (opString == "U" || opString == "F") { @@ -1403,6 +1416,7 @@ namespace storm { STORM_LOG_THROW(edgeEntry.at("rate").count("exp") == 1, storm::exceptions::InvalidJaniException, "Rate in edge from '" << sourceLoc << "' in automaton '" << name << "' must have a defing expression."); rateExpr = parseExpression(edgeEntry.at("rate").at("exp"), scope.refine("rate expression in edge from '" + sourceLoc)); STORM_LOG_THROW(rateExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Rate '" << rateExpr << "' has not a numerical type"); + STORM_LOG_THROW(rateExpr.containsVariables() || rateExpr.evaluateAsRational() > storm::utility::zero(), storm::exceptions::InvalidJaniException, "Only positive rates are allowed but rate '" << rateExpr << " was found."); } // guard STORM_LOG_THROW(edgeEntry.count("guard") <= 1, storm::exceptions::InvalidJaniException, "Guard can be given at most once in edge from '" << sourceLoc << "' in automaton '" << name << "'"); diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp index 34f911da7..11b99dabe 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp @@ -3,6 +3,7 @@ #include "storm/storage/jani/Model.h" #include "storm/storage/jani/traverser/AssignmentsFinder.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" #include "storm/utility/macros.h" #include "storm/exceptions/UnexpectedException.h" @@ -126,20 +127,33 @@ namespace storm { } bool RewardAccumulationEliminationVisitor::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional rewardModelName) const { - STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with for unique reward model."); - storm::jani::AssignmentsFinder::ResultType assignmentKinds; - STORM_LOG_THROW(model.hasGlobalVariable(rewardModelName.get()), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with name " << rewardModelName.get() << "."); - storm::jani::Variable const& transientVar = model.getGlobalVariable(rewardModelName.get()); - if (transientVar.getInitExpression().containsVariables() || !storm::utility::isZero(transientVar.getInitExpression().evaluateAsRational())) { - assignmentKinds.hasLocationAssignment = true; - assignmentKinds.hasEdgeAssignment = true; - assignmentKinds.hasEdgeDestinationAssignment = true; + STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable for unique reward model."); + storm::expressions::Expression rewardExpression = model.getRewardModelExpression(rewardModelName.get()); + bool hasStateRewards = false; + bool hasActionOrTransitionRewards = false; + auto variablesInRewardExpression = rewardExpression.getVariables(); + std::map initialSubstitution; + for (auto const& v : variablesInRewardExpression) { + STORM_LOG_ASSERT(model.hasGlobalVariable(v.getName()), "Unable to find global variable " << v.getName() << " occurring in a reward expression."); + auto const& janiVar = model.getGlobalVariable(v.getName()); + if (janiVar.hasInitExpression()) { + initialSubstitution.emplace(v, janiVar.getInitExpression()); + } + auto assignmentKinds = storm::jani::AssignmentsFinder().find(model, v); + hasActionOrTransitionRewards = hasActionOrTransitionRewards || assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment; + hasStateRewards = hasStateRewards || assignmentKinds.hasLocationAssignment; + } + rewardExpression = storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution); + if (rewardExpression.containsVariables() || !storm::utility::isZero(rewardExpression.evaluateAsRational())) { + hasStateRewards = true; + hasActionOrTransitionRewards = true; } - assignmentKinds = storm::jani::AssignmentsFinder().find(model, transientVar); - if ((assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment) && !accumulation.isStepsSet()) { + + + if (hasActionOrTransitionRewards && !accumulation.isStepsSet()) { return false; } - if (assignmentKinds.hasLocationAssignment) { + if (hasStateRewards) { if (model.isDiscreteTimeModel()) { if (!accumulation.isExitSet()) { return false; diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index be2c74471..8259229fc 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -183,7 +183,7 @@ namespace storm { time = time || (!model.isDeterministicModel() && assignmentKinds.hasLocationAssignment); exit = exit || assignmentKinds.hasLocationAssignment; } - storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution); + rewardExpression = storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution); if (rewardExpression.containsVariables() || !storm::utility::isZero(rewardExpression.evaluateAsRational())) { steps = true; time = true; From 97b248ec8f7a17a8d9f66887387108fda8cf9a6a Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 4 Oct 2018 10:28:03 +0200 Subject: [PATCH 30/38] Updated changelog --- CHANGELOG.md | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 63f102b4d..07b456a31 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,11 +8,15 @@ Version 1.2.x ------------- ### Version 1.2.4 (2018/08) -- New binary `storm-conv` that handles conversions between model files (currently: prism to jani) +- Heavily extended JANI support, in particular: + * arrays, functions, state-exit-rewards (all engines) + * indexed assignments, complex reward expressions (sparse engine) + * several jani-related bug fixes +- New binary `storm-conv` that handles conversions between model files +- New binary `storm-pomdp` that handles the translation of POMDPs to pMCs. +- Closing a Markov automaton now removes unreachable states - Added support for expected time properties for discrete time models - Bug fix in the parser for DRN (MDPs and MAs might have been affected). -- Several bug fixes related to jani -- New binary `storm-pomdp` that handles the translation of POMDPs to pMCs. - `storm-gspn`: Improved .pnpro parser - `storm-gspn`: Added support for single/infinite/k-server semantics for GSPNs given in the .pnpro format - `storm-gspn`: Added option to set a global capacity for all places From d417c9ecbe7a31ced64dabc99c0e317d38f0376f Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 4 Oct 2018 22:14:14 +0200 Subject: [PATCH 31/38] Fix assertion. assert(x < y < z) is not the same as assert(x < y and y < z). --- src/storm/utility/shortestPaths.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/storm/utility/shortestPaths.h b/src/storm/utility/shortestPaths.h index ad344f1aa..60b206bca 100644 --- a/src/storm/utility/shortestPaths.h +++ b/src/storm/utility/shortestPaths.h @@ -235,7 +235,8 @@ namespace storm { // only non-zero entries (i.e. true transitions) are added to the map if (probEntry != 0) { - assert(0 < probEntry <= 1); + assert(0 < probEntry); + assert(probEntry <= 1); stateProbMap.emplace(i, probEntry); } } From 7f5d1591541d6431955b6d3eda4a57c46f14dbb2 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 4 Oct 2018 22:35:03 +0200 Subject: [PATCH 32/38] fix spurious semicolon warning --- src/storm-conv/converter/options/JaniConversionOptions.cpp | 4 ++-- .../converter/options/PrismToJaniConverterOptions.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm-conv/converter/options/JaniConversionOptions.cpp b/src/storm-conv/converter/options/JaniConversionOptions.cpp index 9c1bc1b04..50a5a568c 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.cpp +++ b/src/storm-conv/converter/options/JaniConversionOptions.cpp @@ -5,7 +5,7 @@ namespace storm { JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { // Intentionally left empty - }; + } JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { if (settings.isEliminateFunctionsSet()) { @@ -14,7 +14,7 @@ namespace storm { if (settings.isEliminateArraysSet()) { allowedModelFeatures.remove(storm::jani::ModelFeature::Arrays); } - }; + } } } diff --git a/src/storm-conv/converter/options/PrismToJaniConverterOptions.cpp b/src/storm-conv/converter/options/PrismToJaniConverterOptions.cpp index a64f9edbc..4be7abf2c 100644 --- a/src/storm-conv/converter/options/PrismToJaniConverterOptions.cpp +++ b/src/storm-conv/converter/options/PrismToJaniConverterOptions.cpp @@ -6,7 +6,7 @@ namespace storm { PrismToJaniConverterOptions::PrismToJaniConverterOptions() : allVariablesGlobal(false), suffix("") { // Intentionally left empty - }; + } } } From 41e7932b18c8f33bcbca362c5e5e586dc8b9e513 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 4 Oct 2018 22:47:19 +0200 Subject: [PATCH 33/38] jani exporter: dont write null if no properties are given --- src/storm/storage/jani/JSONExporter.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 8259229fc..ca9bb2989 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -1118,7 +1118,11 @@ namespace storm { // Unset model-features that only relate to properties. These are only set if such properties actually exist. modelFeatures.remove(storm::jani::ModelFeature::StateExitRewards); - + if (formulas.empty()) { + jsonStruct["properties"] = modernjson::json(modernjson::json::value_t::array); + return; + } + uint64_t index = 0; for(auto const& f : formulas) { modernjson::json propDecl; From 9d78c8d22c5188d8d4bc20e8870356e5ce26ff63 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 4 Oct 2018 22:48:05 +0200 Subject: [PATCH 34/38] jani set model type, useful to change from dtmc to mdp semantics -- be careful in usage though --- src/storm/storage/jani/Model.cpp | 4 ++++ src/storm/storage/jani/Model.h | 8 +++++++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 79a37d384..1f219a60d 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -117,6 +117,10 @@ namespace storm { ModelType const& Model::getModelType() const { return modelType; } + + void Model::setModelType(ModelType const& newModelType) { + modelType = newModelType; + } ModelFeatures const& Model::getModelFeatures() const { return modelFeatures; diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 401d1a54a..36cae30ca 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -79,7 +79,13 @@ namespace storm { * Retrieves the type of the model. */ ModelType const& getModelType() const; - + + /*! + * Changes (only) the type declaration of the model. Notice that this operation should be applied with great care, as it may break several algorithms. + * The operation is useful to e.g. make a deterministic model into a non-deterministic one. + */ + void setModelType(ModelType const&); + /*! * Retrieves the enabled model features */ From 98f14684799a387db425d239b9ab29338088739d Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 4 Oct 2018 22:49:03 +0200 Subject: [PATCH 35/38] remove constant from model, e.g. for constants that do not appear in the model --- src/storm/storage/jani/Model.cpp | 16 ++++++++++++++++ src/storm/storage/jani/Model.h | 5 +++++ 2 files changed, 21 insertions(+) diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 1f219a60d..bc8c687c7 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -637,6 +637,22 @@ namespace storm { bool Model::hasConstant(std::string const& name) const { return constantToIndex.find(name) != constantToIndex.end(); } + + + void Model::removeConstant(std::string const& name) { + auto pos = constantToIndex.find(name); + if (pos != constantToIndex.end()) { + uint64_t index = pos->second; + constants.erase(constants.begin() + index); + constantToIndex.erase(pos); + for (auto& entry : constantToIndex) { + if(entry.second > index) { + entry.second--; + } + } + } + + } Constant const& Model::getConstant(std::string const& name) const { auto it = constantToIndex.find(name); diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 36cae30ca..656003853 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -169,6 +169,11 @@ namespace storm { * Retrieves whether the model has a constant with the given name. */ bool hasConstant(std::string const& name) const; + + /*! + * Removes (without checks) a constant from the model. + */ + void removeConstant(std::string const& name); /*! * Retrieves the constants of the model. From 4e9ae0823eb171ab6904e7a95fe78851c8e7b84a Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 5 Oct 2018 15:05:09 +0200 Subject: [PATCH 36/38] JaniParser: fixed parsing of integer variables without initial value --- src/storm-parsers/parser/JaniParser.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 52677bfb0..d38d8cd44 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -842,9 +842,9 @@ namespace storm { } } else { if (type.bounds) { - return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar); - } else { return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), boost::none, false, type.bounds->first, type.bounds->second); + } else { + return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName)); } } break; From a48f90a523c07b0f7346749891a8d3bf6479fe44 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 5 Oct 2018 17:29:11 +0200 Subject: [PATCH 37/38] Guard setInitialStates with hasInitialStatesRestriction --- src/storm/storage/jani/Automaton.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 08cec4105..37924c221 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -444,9 +444,11 @@ namespace storm { for (auto& location : this->getLocations()) { location.substitute(substitution); } - - this->setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), substitution)); - + + if (hasInitialStatesRestriction()) { + this->setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), substitution)); + } + edges.substitute(substitution); } void Automaton::registerTemplateEdge(std::shared_ptr const& te) { From 5bafcbe816126f2aa0402f1e9116b04c6b21446b Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 5 Oct 2018 17:59:46 +0200 Subject: [PATCH 38/38] prism to jani: return properties also in simple cases --- src/storm/storage/prism/Program.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 332bef0fd..e9f6f8ecb 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -1820,6 +1820,8 @@ namespace storm { std::vector newProperties; if (converter.labelsWereRenamed() || converter.rewardModelsWereRenamed()) { newProperties = converter.applyRenaming(properties); + } else { + newProperties = properties; // Nothing to be done here. Notice that the copy operation is suboptimal. } return std::make_pair(janiModel, newProperties); }