sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Refactoring of constraint generation

main
Alexander Bork 6 years ago
parent
be86014007
commit
33b6ba6d8f
4 changed files with 689 additions and 548 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 625
      src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
  2. 87
      src/storm-dft/modelchecker/dft/DFTASFChecker.h
  3. 407
      src/storm-dft/modelchecker/dft/SmtConstraint.cpp
  4. 24
      src/storm-dft/modelchecker/dft/SmtConstraint.h

625
src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
View File

@ -1,4 +1,5 @@
#include "DFTASFChecker.h"
#include "SmtConstraint.cpp"
#include <string>
#include "storm/utility/file.h"
#include "storm/utility/bitoperations.h"
@ -8,397 +9,6 @@
namespace storm {
namespace modelchecker {
/*
* Variable[VarIndex] is the maximum of the others
*/
class IsMaximum : public DFTConstraint {
public:
IsMaximum(uint64_t varIndex, std::vector<uint64_t> const& varIndices) : varIndex(varIndex), varIndices(varIndices) {
}
virtual ~IsMaximum() {
}
std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
std::stringstream sstr;
sstr << "(and ";
// assert it is largereq than all values.
for (auto const& ovi : varIndices) {
sstr << "(>= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") ";
}
// assert it is one of the values.
sstr << "(or ";
for (auto const& ovi : varIndices) {
sstr << "(= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") ";
}
sstr << ")"; // end of the or
sstr << ")"; // end outer and.
return sstr.str();
}
private:
uint64_t varIndex;
std::vector<uint64_t> varIndices;
};
/*
* First is the minimum of the others
*/
class IsMinimum : public DFTConstraint {
public:
IsMinimum(uint64_t varIndex, std::vector<uint64_t> const& varIndices) : varIndex(varIndex), varIndices(varIndices) {
}
virtual ~IsMinimum() {
}
std::string toSmtlib2(std::vector<std::string> 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<uint64_t> 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<std::string> 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<std::shared_ptr<DFTConstraint>> const& constraints) : constraints(constraints) {
}
virtual ~And() {
}
std::string toSmtlib2(std::vector<std::string> 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<std::shared_ptr<DFTConstraint>> constraints;
};
class Or : public DFTConstraint {
public:
Or(std::vector<std::shared_ptr<DFTConstraint>> const& constraints) : constraints(constraints) {
}
virtual ~Or() {
}
std::string toSmtlib2(std::vector<std::string> 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<std::shared_ptr<DFTConstraint>> constraints;
};
class Implies : public DFTConstraint {
public:
Implies(std::shared_ptr<DFTConstraint> l, std::shared_ptr<DFTConstraint> r) : lhs(l), rhs(r) {
}
std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
std::stringstream sstr;
sstr << "(=> " << lhs->toSmtlib2(varNames) << " " << rhs->toSmtlib2(varNames) << ")";
return sstr.str();
}
private:
std::shared_ptr<DFTConstraint> lhs;
std::shared_ptr<DFTConstraint> rhs;
};
class Iff : public DFTConstraint {
public:
Iff(std::shared_ptr<DFTConstraint> l, std::shared_ptr<DFTConstraint> r) : lhs(l), rhs(r) {
}
std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
std::stringstream sstr;
sstr << "(= " << lhs->toSmtlib2(varNames) << " " << rhs->toSmtlib2(varNames) << ")";
return sstr.str();
}
private:
std::shared_ptr<DFTConstraint> lhs;
std::shared_ptr<DFTConstraint> rhs;
};
class IsTrue : public DFTConstraint {
public:
IsTrue(bool val) :value(val) {
}
virtual ~IsTrue() {
}
std::string toSmtlib2(std::vector<std::string> 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<std::string> 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<std::string> 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<std::string> 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<std::string> 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<std::string> 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<std::string> 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<uint64_t> const& indices) : varIndices(indices) {
}
virtual ~PairwiseDifferent() {
}
std::string toSmtlib2(std::vector<std::string> 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<uint64_t> varIndices;
};
class Sorted : public DFTConstraint {
public:
Sorted(std::vector<uint64_t> varIndices) : varIndices(varIndices) {
}
virtual ~Sorted() {
}
std::string toSmtlib2(std::vector<std::string> 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<uint64_t> varIndices;
};
class IfThenElse : public DFTConstraint {
public:
IfThenElse(std::shared_ptr<DFTConstraint> ifC, std::shared_ptr<DFTConstraint> thenC, std::shared_ptr<DFTConstraint> elseC) : ifConstraint(ifC), thenConstraint(thenC), elseConstraint(elseC) {
}
std::string toSmtlib2(std::vector<std::string> 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<DFTConstraint> ifConstraint;
std::shared_ptr<DFTConstraint> thenConstraint;
std::shared_ptr<DFTConstraint> elseConstraint;
};
DFTASFChecker::DFTASFChecker(storm::storage::DFT<double> const& dft) : dft(dft) {
// Intentionally left empty.
}
@ -475,19 +85,68 @@ namespace storm {
// BEs were already considered before
break;
case storm::storage::DFTElementType::AND:
generateAndConstraint(i, childVarIndices, element);
break;
case storm::storage::DFTElementType::OR:
generateOrConstraint(i, childVarIndices, element);
break;
case storm::storage::DFTElementType::VOT:
generateVotConstraint(i, childVarIndices, element);
break;
case storm::storage::DFTElementType::PAND:
generatePandConstraint(i, childVarIndices, element);
break;
case storm::storage::DFTElementType::POR:
generatePorConstraint(i, childVarIndices, element);
break;
case storm::storage::DFTElementType::SEQ:
generateSeqConstraint(childVarIndices, element);
break;
case storm::storage::DFTElementType::SPARE:
generateSpareConstraint(i, childVarIndices, element);
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;
}
}
// Constraint (8)
addClaimingConstraints();
// Handle dependencies
addMarkovianConstraints();
//TODO Move this out of convert method
// Toplevel element will not fail (part of constraint 13)
constraints.push_back(std::make_shared<IsConstantValue>(timePointVariables.at(dft.getTopLevelIndex()), notFailed));
constraints.back()->setDescription("Toplevel element should not fail");
}
// Constraint Generator Functions
void DFTASFChecker::generateAndConstraint(size_t i, std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element) {
// Constraint for AND gate (constraint 1)
constraints.push_back(std::make_shared<IsMaximum>(timePointVariables.at(i), childVarIndices));
constraints.back()->setDescription("AND gate " + element->name());
break;
case storm::storage::DFTElementType::OR:
}
void DFTASFChecker::generateOrConstraint(size_t i, std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element) {
// Constraint for OR gate (constraint 2)
constraints.push_back(std::make_shared<IsMinimum>(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
}
void DFTASFChecker::generateVotConstraint(size_t i, std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element) {
auto vot = std::static_pointer_cast<storm::storage::DFTVot<double> const>(element);
// VOTs are implemented via OR over ANDs with all possible combinations
std::vector<uint64_t> tmpVars;
size_t k = 0;
// Generate all permutations of k out of n
@ -511,56 +170,60 @@ namespace storm {
// Generate next permutation
combination = nextBitPermutation(combination);
++k;
} while(combination < (1 << vot->nrChildren()) && combination != 0);
} while (combination < (1 << vot->nrChildren()) && combination != 0);
// Constraint is OR over all possible combinations
constraints.push_back(std::make_shared<IsMinimum>(timePointVariables.at(i), tmpVars));
constraints.back()->setDescription("VOT gate " + element->name() + ": OR");
break;
}
case storm::storage::DFTElementType::PAND:
{
void DFTASFChecker::generatePandConstraint(size_t i, std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element) {
// Constraint for PAND gate (constraint 3)
std::shared_ptr<DFTConstraint> ifC = std::make_shared<Sorted>(childVarIndices);
std::shared_ptr<DFTConstraint> thenC = std::make_shared<IsEqual>(timePointVariables.at(i), childVarIndices.back());
std::shared_ptr<DFTConstraint> elseC = std::make_shared<IsConstantValue>(timePointVariables.at(i), notFailed);
std::shared_ptr<SmtConstraint> ifC = std::make_shared<Sorted>(childVarIndices);
std::shared_ptr<SmtConstraint> thenC = std::make_shared<IsEqual>(timePointVariables.at(i),
childVarIndices.back());
std::shared_ptr<SmtConstraint> elseC = std::make_shared<IsConstantValue>(timePointVariables.at(i),
notFailed);
constraints.push_back(std::make_shared<IfThenElse>(ifC, thenC, elseC));
constraints.back()->setDescription("PAND gate " + element->name());
break;
}
case storm::storage::DFTElementType::POR:
{
void DFTASFChecker::generatePorConstraint(size_t i, std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element) {
// Constraint for POR gate
// First child fails before all others
std::vector<std::shared_ptr<DFTConstraint>> firstSmallestC;
std::vector<std::shared_ptr<SmtConstraint>> firstSmallestC;
uint64_t timeFirstChild = childVarIndices.front();
for (uint64_t i = 1; i < childVarIndices.size(); ++i) {
firstSmallestC.push_back(std::make_shared<IsLess>(timeFirstChild, childVarIndices.at(i)));
}
std::shared_ptr<DFTConstraint> ifC = std::make_shared<And>(firstSmallestC);
std::shared_ptr<DFTConstraint> thenC = std::make_shared<IsEqual>(timePointVariables.at(i), childVarIndices.front());
std::shared_ptr<DFTConstraint> elseC = std::make_shared<IsConstantValue>(timePointVariables.at(i), notFailed);
std::shared_ptr<SmtConstraint> ifC = std::make_shared<And>(firstSmallestC);
std::shared_ptr<SmtConstraint> thenC = std::make_shared<IsEqual>(timePointVariables.at(i),
childVarIndices.front());
std::shared_ptr<SmtConstraint> elseC = std::make_shared<IsConstantValue>(timePointVariables.at(i),
notFailed);
constraints.push_back(std::make_shared<IfThenElse>(ifC, thenC, elseC));
constraints.back()->setDescription("POR gate " + element->name());
break;
}
case storm::storage::DFTElementType::SEQ:
{
void DFTASFChecker::generateSeqConstraint(std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element) {
// 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<storm::storage::DFTRestriction<double> const>(element);
for (auto const& child : seq->children()) {
for (auto const &child : seq->children()) {
childVarIndices.push_back(timePointVariables.at(child->id()));
}
constraints.push_back(std::make_shared<Sorted>(childVarIndices));
constraints.back()->setDescription("SEQ gate " + element->name());
break;
}
case storm::storage::DFTElementType::SPARE:
{
void DFTASFChecker::generateSpareConstraint(size_t i, std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element) {
auto spare = std::static_pointer_cast<storm::storage::DFTSpare<double> const>(element);
auto const& children = spare->children();
auto const &children = spare->children();
uint64_t firstChild = children.front()->id();
uint64_t lastChild = children.back()->id();
@ -569,8 +232,10 @@ namespace storm {
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<DFTConstraint> leftC = std::make_shared<IsLess>(getClaimVariableIndex(spare->id(), lastChild), childVarIndices.back());
constraints.push_back(std::make_shared<Implies>(leftC, std::make_shared<IsEqual>(timePointVariables.at(i), childVarIndices.back())));
std::shared_ptr<SmtConstraint> leftC = std::make_shared<IsLess>(
getClaimVariableIndex(spare->id(), lastChild), childVarIndices.back());
constraints.push_back(std::make_shared<Implies>(leftC, std::make_shared<IsEqual>(timePointVariables.at(i),
childVarIndices.back())));
constraints.back()->setDescription("Last child & claimed -> SPARE fails");
// Construct constraint for trying to claim next child
@ -579,60 +244,23 @@ namespace storm {
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<DFTConstraint> tryClaimC = generateTryToClaimConstraint(spare, currChild + 1, timeCurrChild);
constraints.push_back(std::make_shared<Iff>(std::make_shared<IsLess>(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), timeCurrChild), tryClaimC));
constraints.back()->setDescription("Try to claim " + std::to_string(currChild+2) + "th child");
}
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;
std::shared_ptr<SmtConstraint> tryClaimC = generateTryToClaimConstraint(spare, currChild + 1,
timeCurrChild);
constraints.push_back(std::make_shared<Iff>(
std::make_shared<IsLess>(getClaimVariableIndex(spare->id(), children.at(currChild)->id()),
timeCurrChild), tryClaimC));
constraints.back()->setDescription("Try to claim " + std::to_string(currChild + 2) + "th child");
}
}
// 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<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
if (element->isSpareGate()) {
auto spare = std::static_pointer_cast<storm::storage::DFTSpare<double> const>(element);
for (auto const& child : spare->children()) {
std::vector<std::shared_ptr<DFTConstraint>> additionalC;
uint64_t timeClaiming = getClaimVariableIndex(spare->id(), child->id());
std::shared_ptr<DFTConstraint> leftC = std::make_shared<IsLessConstant>(timeClaiming, notFailed);
// Child must be operational at time of claiming
additionalC.push_back(std::make_shared<IsLess>(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<IsConstantValue>(getClaimVariableIndex(parent->id(), child->id()), notFailed));
}
}
constraints.push_back(std::make_shared<Implies>(leftC, std::make_shared<And>(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.");
}
}
}
// Handle dependencies
addMarkovianConstraints();
// Toplevel element will not fail (part of constraint 13)
constraints.push_back(std::make_shared<IsConstantValue>(timePointVariables.at(dft.getTopLevelIndex()), notFailed));
constraints.back()->setDescription("Toplevel element should not fail");
}
std::shared_ptr<DFTConstraint> DFTASFChecker::generateTryToClaimConstraint(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> spare, uint64_t childIndex, uint64_t timepoint) const {
std::shared_ptr<SmtConstraint>
DFTASFChecker::generateTryToClaimConstraint(std::shared_ptr<storm::storage::DFTSpare<ValueType> 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<std::shared_ptr<DFTConstraint>> noClaimingPossible;
std::vector<std::shared_ptr<SmtConstraint>> noClaimingPossible;
// Child cannot be claimed.
if (childIndex + 1 < spare->children().size()) {
// Consider next child for claiming (second case in constraint 7)
@ -641,10 +269,10 @@ namespace storm {
// Last child: spare fails at same point as this child (third case in constraint 7)
noClaimingPossible.push_back(std::make_shared<IsEqual>(timePointVariables.at(spare->id()), timepoint));
}
std::shared_ptr<DFTConstraint> elseCaseC = std::make_shared<And>(noClaimingPossible);
std::shared_ptr<SmtConstraint> elseCaseC = std::make_shared<And>(noClaimingPossible);
// Check if next child is availble (first case in constraint 7)
std::vector<std::shared_ptr<DFTConstraint>> claimingPossibleC;
// Check if next child is available (first case in constraint 7)
std::vector<std::shared_ptr<SmtConstraint>> claimingPossibleC;
// Next child is not yet failed
claimingPossibleC.push_back(std::make_shared<IsLess>(timepoint, timeChild));
// Child is not yet claimed by a different spare
@ -657,24 +285,59 @@ namespace storm {
}
// Claim child if available
std::shared_ptr<DFTConstraint> firstCaseC = std::make_shared<IfThenElse>(std::make_shared<And>(claimingPossibleC), std::make_shared<IsEqual>(claimChild, timepoint), elseCaseC);
std::shared_ptr<SmtConstraint> firstCaseC = std::make_shared<IfThenElse>(
std::make_shared<And>(claimingPossibleC), std::make_shared<IsEqual>(claimChild, timepoint),
elseCaseC);
return firstCaseC;
}
void DFTASFChecker::addClaimingConstraints() {
// Only one spare can claim a child (constraint 8)
// and only not failed children can be claimed (addition to constrain 8)
for (size_t i = 0; i < dft.nrElements(); ++i) {
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
if (element->isSpareGate()) {
auto spare = std::static_pointer_cast<storm::storage::DFTSpare<double> const>(element);
for (auto const &child : spare->children()) {
std::vector<std::shared_ptr<SmtConstraint>> additionalC;
uint64_t timeClaiming = getClaimVariableIndex(spare->id(), child->id());
std::shared_ptr<SmtConstraint> leftC = std::make_shared<IsLessConstant>(timeClaiming,
notFailed);
// Child must be operational at time of claiming
additionalC.push_back(
std::make_shared<IsLess>(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<IsConstantValue>(
getClaimVariableIndex(parent->id(), child->id()), notFailed));
}
}
constraints.push_back(std::make_shared<Implies>(leftC, std::make_shared<And>(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.");
}
}
}
}
void DFTASFChecker::addMarkovianConstraints() {
uint64_t nrMarkovian = dft.nrBasicElements();
// Vector containing (non-)Markovian constraints for each timepoint
std::vector<std::vector<std::shared_ptr<DFTConstraint>>> markovianC(nrMarkovian);
std::vector<std::vector<std::shared_ptr<DFTConstraint>>> nonMarkovianC(nrMarkovian);
std::vector<std::vector<std::shared_ptr<DFTConstraint>>> notColdC(nrMarkovian);
std::vector<std::vector<std::shared_ptr<SmtConstraint>>> markovianC(nrMarkovian);
std::vector<std::vector<std::shared_ptr<SmtConstraint>>> nonMarkovianC(nrMarkovian);
std::vector<std::vector<std::shared_ptr<SmtConstraint>>> 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<storm::storage::DFTElement<ValueType> const> element = dft.getElement(j);
if (element->hasOutgoingDependencies()) {
for (uint64_t i = 0; i < nrMarkovian; ++i) {
std::shared_ptr<DFTConstraint> triggerFailed = std::make_shared<IsLessEqualConstant>(timePointVariables.at(j), i);
std::vector<std::shared_ptr<DFTConstraint>> depFailed;
std::shared_ptr<SmtConstraint> triggerFailed = std::make_shared<IsLessEqualConstant>(
timePointVariables.at(j), i);
std::vector<std::shared_ptr<SmtConstraint>> depFailed;
for (auto const& dependency : element->outgoingDependencies()) {
for (auto const& depElement : dependency->dependentEvents()) {
depFailed.push_back(std::make_shared<IsLessEqualConstant>(timePointVariables.at(depElement->id()), i));
@ -697,8 +360,9 @@ namespace storm {
if (be->hasIngoingDependencies()) {
for (uint64_t i = 0; i < nrMarkovian -1; ++i) {
std::shared_ptr<DFTConstraint> nextFailure = std::make_shared<IsConstantValue>(timePointVariables.at(j), i+1);
std::vector<std::shared_ptr<DFTConstraint>> triggerFailed;
std::shared_ptr<SmtConstraint> nextFailure = std::make_shared<IsConstantValue>(
timePointVariables.at(j), i + 1);
std::vector<std::shared_ptr<SmtConstraint>> triggerFailed;
for (auto const& dependency : be->ingoingDependencies()) {
triggerFailed.push_back(std::make_shared<IsLessEqualConstant>(timePointVariables.at(dependency->triggerEvent()->id()), i));
}
@ -718,7 +382,8 @@ namespace storm {
if (element->isBasicElement()) {
auto be = std::static_pointer_cast<storm::storage::DFTBE<double> const>(element);
for (uint64_t i = 0; i < nrMarkovian; ++i) {
std::shared_ptr<DFTConstraint> nextFailure = std::make_shared<IsConstantValue>(timePointVariables.at(j), i+1);
std::shared_ptr<SmtConstraint> nextFailure = std::make_shared<IsConstantValue>(
timePointVariables.at(j), i + 1);
// BE is not cold
// TODO: implement use of activation variables here
bool cold = storm::utility::isZero<ValueType>(be->activeFailureRate());

87
src/storm-dft/modelchecker/dft/DFTASFChecker.h
View File

@ -4,30 +4,12 @@
#include <vector>
#include <unordered_map>
#include "SmtConstraint.h"
#include "storm-dft/storage/dft/DFT.h"
namespace storm {
namespace modelchecker {
class DFTConstraint {
public:
virtual ~DFTConstraint() {
}
virtual std::string toSmtlib2(std::vector<std::string> const& varNames) const = 0;
virtual std::string description() const {
return descript;
}
void setDescription(std::string const& descr) {
descript = descr;
}
private:
std::string descript;
};
class SpareAndChildPair {
public:
SpareAndChildPair(uint64_t spareIndex, uint64_t childIndex) : spareIndex(spareIndex), childIndex(childIndex) {
@ -47,9 +29,16 @@ namespace storm {
using ValueType = double;
public:
DFTASFChecker(storm::storage::DFT<ValueType> const&);
/**
* Generate general variables and constraints for the DFT and store them in the corresponding maps and vectors
*
*/
void convert();
void toFile(std::string const&);
void toSolver();
private:
uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const;
@ -63,7 +52,63 @@ namespace storm {
*
* @return Constraint encoding the claiming.
*/
std::shared_ptr<DFTConstraint> generateTryToClaimConstraint(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> spare, uint64_t childIndex, uint64_t timepoint) const;
std::shared_ptr<SmtConstraint>
generateTryToClaimConstraint(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> spare,
uint64_t childIndex, uint64_t timepoint) const;
/**
* Add constraints encoding AND gates.
* This corresponds to constraint (1)
*/
void generateAndConstraint(size_t i, std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element);
/**
* Add constraints encoding OR gates.
* This corresponds to constraint (2)
*/
void generateOrConstraint(size_t i, std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element);
/**
* Add constraints encoding VOT gates.
*/
void generateVotConstraint(size_t i, std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element);
/**
* Add constraints encoding PAND gates.
* This corresponds to constraint (3)
*/
void generatePandConstraint(size_t i, std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element);
/**
* Add constraints encoding POR gates.
*/
void generatePorConstraint(size_t i, std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element);
/**
* Add constraints encoding SEQ gates.
* This corresponds to constraint (4)
*/
void generateSeqConstraint(std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element);
/**
* Add constraints encoding SPARE gates.
* This corresponds to constraints (5),(6),(7)
*/
void generateSpareConstraint(size_t i, std::vector<uint64_t> childVarIndices,
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element);
/**
* Add constraints encoding claiming rules.
* This corresponds to constraint (8) and addition
*/
void addClaimingConstraints();
/**
* Add constraints encoding Markovian states.
@ -74,7 +119,7 @@ namespace storm {
storm::storage::DFT<ValueType> const& dft;
std::vector<std::string> varNames;
std::unordered_map<uint64_t, uint64_t> timePointVariables;
std::vector<std::shared_ptr<DFTConstraint>> constraints;
std::vector<std::shared_ptr<SmtConstraint>> constraints;
std::map<SpareAndChildPair, uint64_t> claimVariables;
std::unordered_map<uint64_t, uint64_t> markovianVariables;
std::vector<uint64_t> tmpTimePointVariables;

407
src/storm-dft/modelchecker/dft/SmtConstraint.cpp
View File

@ -0,0 +1,407 @@
#include "DFTASFChecker.h"
#include <string>
namespace storm {
namespace modelchecker {
/*
* Variable[VarIndex] is the maximum of the others
*/
class IsMaximum : public SmtConstraint {
public:
IsMaximum(uint64_t varIndex, std::vector<uint64_t> const &varIndices) : varIndex(varIndex),
varIndices(varIndices) {
}
virtual ~IsMaximum() {
}
std::string toSmtlib2(std::vector<std::string> const &varNames) const override {
std::stringstream sstr;
sstr << "(and ";
// assert it is largereq than all values.
for (auto const &ovi : varIndices) {
sstr << "(>= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") ";
}
// assert it is one of the values.
sstr << "(or ";
for (auto const &ovi : varIndices) {
sstr << "(= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") ";
}
sstr << ")"; // end of the or
sstr << ")"; // end outer and.
return sstr.str();
}
private:
uint64_t varIndex;
std::vector<uint64_t> varIndices;
};
/*
* First is the minimum of the others
*/
class IsMinimum : public SmtConstraint {
public:
IsMinimum(uint64_t varIndex, std::vector<uint64_t> const &varIndices) : varIndex(varIndex),
varIndices(varIndices) {
}
virtual ~IsMinimum() {
}
std::string toSmtlib2(std::vector<std::string> 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<uint64_t> varIndices;
};
class BetweenValues : public SmtConstraint {
public:
BetweenValues(uint64_t varIndex, uint64_t lower, uint64_t upper) : varIndex(varIndex), upperBound(upper),
lowerBound(lower) {
}
virtual ~BetweenValues() {
}
std::string toSmtlib2(std::vector<std::string> 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 SmtConstraint {
public:
And(std::vector<std::shared_ptr<SmtConstraint>> const &constraints) : constraints(constraints) {
}
virtual ~And() {
}
std::string toSmtlib2(std::vector<std::string> 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<std::shared_ptr<SmtConstraint>> constraints;
};
class Or : public SmtConstraint {
public:
Or(std::vector<std::shared_ptr<SmtConstraint>> const &constraints) : constraints(constraints) {
}
virtual ~Or() {
}
std::string toSmtlib2(std::vector<std::string> 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<std::shared_ptr<SmtConstraint>> constraints;
};
class Implies : public SmtConstraint {
public:
Implies(std::shared_ptr<SmtConstraint> l, std::shared_ptr<SmtConstraint> r) : lhs(l), rhs(r) {
}
std::string toSmtlib2(std::vector<std::string> const &varNames) const override {
std::stringstream sstr;
sstr << "(=> " << lhs->toSmtlib2(varNames) << " " << rhs->toSmtlib2(varNames) << ")";
return sstr.str();
}
private:
std::shared_ptr<SmtConstraint> lhs;
std::shared_ptr<SmtConstraint> rhs;
};
class Iff : public SmtConstraint {
public:
Iff(std::shared_ptr<SmtConstraint> l, std::shared_ptr<SmtConstraint> r) : lhs(l), rhs(r) {
}
std::string toSmtlib2(std::vector<std::string> const &varNames) const override {
std::stringstream sstr;
sstr << "(= " << lhs->toSmtlib2(varNames) << " " << rhs->toSmtlib2(varNames) << ")";
return sstr.str();
}
private:
std::shared_ptr<SmtConstraint> lhs;
std::shared_ptr<SmtConstraint> rhs;
};
class IsTrue : public SmtConstraint {
public:
IsTrue(bool val) : value(val) {
}
virtual ~IsTrue() {
}
std::string toSmtlib2(std::vector<std::string> const &varNames) const override {
std::stringstream sstr;
sstr << (value ? "true" : "false");
return sstr.str();
}
private:
bool value;
};
class IsBoolValue : public SmtConstraint {
public:
IsBoolValue(uint64_t varIndex, bool val) : varIndex(varIndex), value(val) {
}
virtual ~IsBoolValue() {
}
std::string toSmtlib2(std::vector<std::string> 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 SmtConstraint {
public:
IsConstantValue(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) {
}
virtual ~IsConstantValue() {
}
std::string toSmtlib2(std::vector<std::string> 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 SmtConstraint {
public:
IsLessConstant(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) {
}
virtual ~IsLessConstant() {
}
std::string toSmtlib2(std::vector<std::string> 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 SmtConstraint {
public:
IsLessEqualConstant(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) {
}
virtual ~IsLessEqualConstant() {
}
std::string toSmtlib2(std::vector<std::string> 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 SmtConstraint {
public:
IsEqual(uint64_t varIndex1, uint64_t varIndex2) : var1Index(varIndex1), var2Index(varIndex2) {
}
virtual ~IsEqual() {
}
std::string toSmtlib2(std::vector<std::string> const &varNames) const override {
return "(= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")";
}
private:
uint64_t var1Index;
uint64_t var2Index;
};
class IsLess : public SmtConstraint {
public:
IsLess(uint64_t varIndex1, uint64_t varIndex2) : var1Index(varIndex1), var2Index(varIndex2) {
}
virtual ~IsLess() {
}
std::string toSmtlib2(std::vector<std::string> const &varNames) const override {
return "(< " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")";
}
private:
uint64_t var1Index;
uint64_t var2Index;
};
class PairwiseDifferent : public SmtConstraint {
public:
PairwiseDifferent(std::vector<uint64_t> const &indices) : varIndices(indices) {
}
virtual ~PairwiseDifferent() {
}
std::string toSmtlib2(std::vector<std::string> 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<uint64_t> varIndices;
};
class Sorted : public SmtConstraint {
public:
Sorted(std::vector<uint64_t> varIndices) : varIndices(varIndices) {
}
virtual ~Sorted() {
}
std::string toSmtlib2(std::vector<std::string> 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<uint64_t> varIndices;
};
class IfThenElse : public SmtConstraint {
public:
IfThenElse(std::shared_ptr<SmtConstraint> ifC, std::shared_ptr<SmtConstraint> thenC,
std::shared_ptr<SmtConstraint> elseC) : ifConstraint(ifC), thenConstraint(thenC),
elseConstraint(elseC) {
}
std::string toSmtlib2(std::vector<std::string> 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<SmtConstraint> ifConstraint;
std::shared_ptr<SmtConstraint> thenConstraint;
std::shared_ptr<SmtConstraint> elseConstraint;
};
}
}

24
src/storm-dft/modelchecker/dft/SmtConstraint.h
View File

@ -0,0 +1,24 @@
#include <string>
namespace storm {
namespace modelchecker {
class SmtConstraint {
public:
virtual ~SmtConstraint() {
}
virtual std::string toSmtlib2(std::vector<std::string> const &varNames) const = 0;
virtual std::string description() const {
return descript;
}
void setDescription(std::string const &descr) {
descript = descr;
}
private:
std::string descript;
};
}
}
Write Preview
Loading…
Cancel
Save