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

Fixed bound calculation for SMT encoding

tempestpy_adaptions
Alexander Bork 6 years ago
parent
d06cf59eba
commit
5d5487140f
5 changed files with 127 additions and 25 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. 6
      src/storm-dft/api/storm-dft.cpp
  2. 83
      src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
  3. 36
      src/storm-dft/modelchecker/dft/DFTASFChecker.h
  4. 25
      src/storm-dft/modelchecker/dft/SmtConstraint.cpp
  5. 2
      src/test/storm-dft/api/DftModelCheckerTest.cpp

6
src/storm-dft/api/storm-dft.cpp
View File

@ -46,12 +46,12 @@ namespace storm {
std::vector<storm::solver::SmtSolver::CheckResult>
analyzeDFTSMT(storm::storage::DFT<double> const &dft, bool printOutput) {
storm::modelchecker::DFTASFChecker smtChecker(dft);
smtChecker.convert();
smtChecker.toSolver();
std::vector<storm::solver::SmtSolver::CheckResult> results;
results.push_back(smtChecker.checkTleNeverFailedQuery());
results.push_back(smtChecker.checkTleNeverFailed());
uint64_t lower_bound = smtChecker.getLeastFailureBound();
uint64_t upper_bound = smtChecker.getAlwaysFailedBound();
if (printOutput) {
//TODO add suitable output function, maybe add query descriptions for better readability
for (size_t i = 0; i < results.size(); ++i) {
@ -61,9 +61,9 @@ namespace storm {
} else if (results.at(i) == storm::solver::SmtSolver::CheckResult::Unsat) {
tmp = "UNSAT";
}
std::cout << "Query " << std::to_string(i) << " : " << tmp << std::endl;
}
std::cout << "Lower bound: " << std::to_string(lower_bound) << std::endl;
std::cout << "Upper bound: " << std::to_string(upper_bound) << std::endl;
}
return results;
}

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

@ -242,6 +242,13 @@ namespace storm {
for (uint64_t currChild = 0; currChild < children.size() - 1; ++currChild) {
uint64_t timeCurrChild = childVarIndices.at(currChild); // Moment when current child fails
// If trying to claim (i+1)-th child, either child claimed before or never claimed by other spare
// (additional constraint)
std::shared_ptr<SmtConstraint> claimEarlyC = generateClaimEarlyConstraint(spare, currChild);
constraints.push_back(std::make_shared<Implies>(
std::make_shared<IsLess>(getClaimVariableIndex(spare->id(), children.at(currChild)->id()),
timeCurrChild), claimEarlyC));
constraints.back()->setDescription("Ensure earliest possible claiming");
// If i-th child fails after being claimed, then try to claim next child (constraint 6)
std::shared_ptr<SmtConstraint> tryClaimC = generateTryToClaimConstraint(spare, currChild + 1,
timeCurrChild);
@ -252,6 +259,28 @@ namespace storm {
}
}
std::shared_ptr<SmtConstraint>
DFTASFChecker::generateClaimEarlyConstraint(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> spare,
uint64_t childIndex) const {
auto child = spare->children().at(childIndex + 1);
std::vector<std::shared_ptr<SmtConstraint>> constraintAggregator;
for (auto const &otherSpare : child->parents()) {
if (otherSpare->id() == spare->id()) {
// not a different spare.
continue;
}
std::vector<std::shared_ptr<SmtConstraint>> OrAggregator;
// Other spare has claimed before
OrAggregator.push_back(std::make_shared<IsLessConstant>(
getClaimVariableIndex(otherSpare->id(), child->id()), timePointVariables.at(childIndex)));
// Other spare will never claim
OrAggregator.push_back(std::make_shared<IsConstantValue>(
getClaimVariableIndex(otherSpare->id(), child->id()), notFailed));
constraintAggregator.push_back(std::make_shared<Or>(OrAggregator));
}
return std::make_shared<And>(constraintAggregator);
}
std::shared_ptr<SmtConstraint>
DFTASFChecker::generateTryToClaimConstraint(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> spare,
uint64_t childIndex, uint64_t timepoint) const {
@ -458,14 +487,14 @@ namespace storm {
}
storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleNeverFailedQuery() {
// STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries");
storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleFailsWithEq(uint64_t bound) {
STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
// Set backtracking marker to check several properties without reconstructing DFT encoding
solver->push();
// Constraint that toplevel element will not fail (part of constraint 13)
// Constraint that toplevel element can fail with less or equal 'bound' failures
std::shared_ptr<SmtConstraint> tleNeverFailedConstr = std::make_shared<IsConstantValue>(
timePointVariables.at(dft.getTopLevelIndex()), notFailed);
timePointVariables.at(dft.getTopLevelIndex()), bound);
std::shared_ptr<storm::expressions::ExpressionManager> manager = solver->getManager().getSharedPointer();
solver->add(tleNeverFailedConstr->toExpression(varNames, manager));
storm::solver::SmtSolver::CheckResult res = solver->check();
@ -474,7 +503,7 @@ namespace storm {
}
storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleFailsWithLeq(uint64_t bound) {
//STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries");
STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
// Set backtracking marker to check several properties without reconstructing DFT encoding
solver->push();
@ -489,24 +518,25 @@ namespace storm {
}
void DFTASFChecker::setSolverTimeout(uint_fast64_t milliseconds) {
if (!solver) {
STORM_LOG_WARN("SMT Solver was not initialized, timeout setting ignored");
} else {
solver->setTimeout(milliseconds);
}
STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, timeout cannot be set");
solver->setTimeout(milliseconds);
}
void DFTASFChecker::unsetSolverTimeout() {
if (!solver) {
STORM_LOG_WARN("SMT Solver was not initialized, timeout unsetting ignored");
} else {
solver->unsetTimeout();
}
STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, timeout cannot be unset");
solver->unsetTimeout();
}
uint64_t DFTASFChecker::getLeastFailureBound() {
//STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries");
storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleNeverFailed() {
STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
return checkTleFailsWithEq(notFailed);
}
uint64_t DFTASFChecker::getLeastFailureBound() {
STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
if (checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) {
return notFailed;
}
uint64_t bound = 0;
while (bound < notFailed) {
setSolverTimeout(10000);
@ -520,5 +550,24 @@ namespace storm {
}
return bound;
}
uint64_t DFTASFChecker::getAlwaysFailedBound() {
STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
if (checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) {
return notFailed;
}
uint64_t bound = notFailed - 1;
while (bound >= 0) {
setSolverTimeout(10000);
storm::solver::SmtSolver::CheckResult tmp_res = checkTleFailsWithEq(bound);
unsetSolverTimeout();
if (tmp_res == storm::solver::SmtSolver::CheckResult::Sat ||
tmp_res == storm::solver::SmtSolver::CheckResult::Unknown) {
return bound;
}
--bound;
}
return bound;
}
}
}

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

@ -47,23 +47,38 @@ namespace storm {
*
* @return "Sat" if TLE never fails, "Unsat" if it does, otherwise "Unknown"
*/
storm::solver::SmtSolver::CheckResult checkTleNeverFailedQuery();
storm::solver::SmtSolver::CheckResult checkTleNeverFailed();
/**
* Check if there exists a sequence of BE failures of given length such that the TLE of the DFT fails
* Check if there exists a sequence of BE failures of exactly given length such that the TLE of the DFT fails
*
* @param bound the length of the sequene
* @return "Sat" if such a sequence exists, "Unsat" if it does not, otherwise "Unknown"
*/
storm::solver::SmtSolver::CheckResult checkTleFailsWithEq(uint64_t bound);
/**
* Check if there exists a sequence of BE failures of at least given length such that the TLE of the DFT fails
*
* @param bound the length of the sequence
* @return "Sat" if such a sequence exists, "Unsat" if it does not, otherwise "Unknown"
*/
storm::solver::SmtSolver::CheckResult checkTleFailsWithLeq(uint64_t bound);
/**
* Get the minimal number of BEs necessary for the TLE to fail
* Get the minimal number of BEs necessary for the TLE to fail (lower bound for number of failures to check)
*
* @return the minimal number
*/
uint64_t getLeastFailureBound();
/**
* Get the number of BE failures for which the TLE always fails (upper bound for number of failures to check)
*
* @return the number
*/
uint64_t getAlwaysFailedBound();
/**
* Set the timeout of the solver
*
@ -79,6 +94,19 @@ namespace storm {
private:
uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const;
/**
* Generate constraint for spares such that when trying to claim child (i+1), other spares either claimed it
* before or will never claim it
*
* @param spare Spare.
* @param childIndex Index of child to consider in spare children
* @param timepoint Timepoint to try to claim
* @return
*/
std::shared_ptr<SmtConstraint>
generateClaimEarlyConstraint(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> spare,
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.
@ -153,7 +181,7 @@ namespace storm {
void addMarkovianConstraints();
storm::storage::DFT<ValueType> const& dft;
std::shared_ptr<storm::solver::SmtSolver> solver = NULL;
std::shared_ptr<storm::solver::SmtSolver> solver = nullptr;
std::vector<std::string> varNames;
std::unordered_map<uint64_t, uint64_t> timePointVariables;
std::vector<std::shared_ptr<SmtConstraint>> constraints;

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

@ -395,6 +395,31 @@ namespace storm {
uint64_t value;
};
class IsGreaterEqualConstant : public SmtConstraint {
public:
IsGreaterEqualConstant(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) {
}
virtual ~IsGreaterEqualConstant() {
}
std::string toSmtlib2(std::vector<std::string> const &varNames) const override {
std::stringstream sstr;
assert(varIndex < varNames.size());
sstr << "(<= " << value << " " << varNames.at(varIndex) << ")";
return sstr.str();
}
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
return manager->getVariableExpression(varNames.at(varIndex)) >= value;
}
private:
uint64_t varIndex;
uint64_t value;
};
class IsEqual : public SmtConstraint {
public:

2
src/test/storm-dft/api/DftModelCheckerTest.cpp
View File

@ -80,7 +80,7 @@ namespace {
smtChecker.toSolver();
std::vector<storm::solver::SmtSolver::CheckResult> results;
return smtChecker.checkTleNeverFailedQuery();
return smtChecker.checkTleNeverFailed();
}
double analyzeReliability(std::string const &file, double bound) {

Write Preview
Loading…
Cancel
Save