diff --git a/CHANGELOG.md b/CHANGELOG.md index eb2345e54..07b456a31 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,10 +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 - `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 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 - }; + } } } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 55d968a2c..41f688da0 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -1,22 +1,23 @@ #include "DFTASFChecker.h" #include #include "storm/utility/file.h" +#include "storm/utility/bitoperations.h" +#include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/NotSupportedException.h" 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 +35,734 @@ 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; + if (constraints.empty()) { + sstr << "true"; + } else { + sstr << "(and"; + for(auto const& c : constraints) { + sstr << " " << c->toSmtlib2(varNames); + } + sstr << ")"; + } + return sstr.str(); + } + + private: + std::vector> constraints; + + }; + + + 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) { + } + + 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) { + } + + 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 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) { + } + + 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) { + } + + 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 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 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: + 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 IsLess : public DFTConstraint { + public: + IsLess(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) { + } + + virtual ~IsLess() { + } + + 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; + }; + - 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) << ") "; + 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; + notFailed = dft.nrBasicElements()+1; // Value indicating the element is not failed + + // 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()); + 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); } - 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) { - + break; } - 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() { - + default: + break; + } + } + // Initialize variables indicating Markovian states + for (size_t i = 0; i < dft.nrBasicElements(); ++i) { + varNames.push_back("m_" + std::to_string(i)); + markovianVariables.emplace(i, varNames.size() - 1); + } + + + // Generate constraints + + // 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)); + } + + // 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; + 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::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - sstr << "(and"; - for(auto const& c : constraints) { - sstr << " " << c->toSmtlib2(varNames); + } + + 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 " + 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 " + element->name()); + break; + case storm::storage::DFTElementType::VOT: + { + // VOTs are implemented via OR over ANDs with all possible combinations + auto vot = std::static_pointer_cast const>(element); + std::vector tmpVars; + size_t k = 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(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(index, combinationChildren)); + constraints.back()->setDescription("VOT gate " + element->name() + ": AND no. " + std::to_string(k)); + // Generate next permutation + combination = nextBitPermutation(combination); + ++k; + } 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) + std::shared_ptr ifC = std::make_shared(childVarIndices); + 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 " + element->name()); + 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))); } - 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); + 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 " + element->name()); + break; + } + case storm::storage::DFTElementType::SEQ: + { + // 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())); } - 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)) << ")"; + + 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); + auto const& children = spare->children(); + uint64_t firstChild = children.front()->id(); + uint64_t lastChild = children.back()->id(); + + // 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 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()); + 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 + STORM_LOG_ASSERT(children.size() >= 2, "Spare has only one child"); + for (uint64_t currChild = 0; currChild < children.size() - 1; ++currChild) { + uint64_t timeCurrChild = childVarIndices.at(currChild); // Moment when current child fails + + // 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(currChild+2) + "th child"); } - 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. + break; + } + case storm::storage::DFTElementType::PDEP: + // 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."); + break; } - - 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; + } + + // 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 + for (auto const& parent : child->parents()) { + if (parent->isSpareGate() && parent->id() != spare->id()) { + // Different spare + additionalC.push_back(std::make_shared(getClaimVariableIndex(parent->id(), child->id()), notFailed)); } - 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"); - } + 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."); } - - - 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())); + } + } + + // 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"); + } + + 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; + // Child cannot be claimed. + 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::addMarkovianConstraints() { + uint64_t nrMarkovian = dft.nrBasicElements(); + // Vector containing (non-)Markovian constraints for each timepoint + 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 < nrMarkovian; ++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)); } } - - 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; + markovianC[i].push_back(std::make_shared(triggerFailed, std::make_shared(depFailed))); + } + } + } + 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."); + } + + // 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 < nrMarkovian -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)); } - default: - break; + nonMarkovianC[i].push_back(std::make_shared(nextFailure, std::make_shared(triggerFailed))); } } - - 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; + } + 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))); } - stream << "(check-sat)" << std::endl; - storm::utility::closeFile(stream); } + } + 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."); + } + + } + + + 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; + } + stream << "; Markovian variables" << std::endl; + 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; + } + 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 a4337bb58..ee53b152d 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -12,11 +12,13 @@ namespace storm { class DFTConstraint { public: virtual ~DFTConstraint() { - } - virtual std::string toSmtlib2(std::vector const& varNames) const = 0; - virtual std::string description() const { return descript; } + virtual std::string toSmtlib2(std::vector const& varNames) const = 0; + + virtual std::string description() const { + return descript; + } void setDescription(std::string const& descr) { descript = descr; @@ -27,10 +29,8 @@ namespace storm { }; class SpareAndChildPair { - public: SpareAndChildPair(uint64_t spareIndex, uint64_t childIndex) : spareIndex(spareIndex), childIndex(childIndex) { - } friend bool operator<(SpareAndChildPair const& p1, SpareAndChildPair const& p2) { @@ -45,7 +45,6 @@ namespace storm { class DFTASFChecker { using ValueType = double; - public: DFTASFChecker(storm::storage::DFT const&); void convert(); @@ -53,12 +52,33 @@ 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; + + /** + * 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; + std::vector tmpTimePointVariables; + uint64_t notFailed; }; } } diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index eba57d0dd..d38d8cd44 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") { @@ -829,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; @@ -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-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))); } 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/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) { diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index be2c74471..ca9bb2989 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; @@ -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; diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 79a37d384..bc8c687c7 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; @@ -633,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 401d1a54a..656003853 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 */ @@ -163,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. 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); } 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 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 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); } }