Alexander Bork
6 years ago
7 changed files with 340 additions and 237 deletions
-
13src/storm-dft/api/storm-dft.cpp
-
4src/storm-dft/api/storm-dft.h
-
185src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
-
50src/storm-dft/modelchecker/dft/DFTASFChecker.h
-
241src/storm-dft/utility/FailureBoundFinder.cpp
-
73src/storm-dft/utility/FailureBoundFinder.h
-
11src/test/storm-dft/api/DftSmtTest.cpp
@ -0,0 +1,241 @@ |
|||
#include "FailureBoundFinder.h"
|
|||
|
|||
namespace storm { |
|||
namespace dft { |
|||
namespace utility { |
|||
uint64_t |
|||
FailureBoundFinder::correctLowerBound(std::shared_ptr<storm::modelchecker::DFTASFChecker> smtchecker, |
|||
uint64_t bound, uint_fast64_t timeout) { |
|||
STORM_LOG_DEBUG("Lower bound correction - try to correct bound " << std::to_string(bound)); |
|||
uint64_t boundCandidate = bound; |
|||
uint64_t nrDepEvents = 0; |
|||
uint64_t nrNonMarkovian = 0; |
|||
auto dft = smtchecker->getDFT(); |
|||
|
|||
// Count dependent events
|
|||
for (size_t i = 0; i < dft.nrElements(); ++i) { |
|||
std::shared_ptr<storm::storage::DFTElement<double> const> element = dft.getElement(i); |
|||
if (element->type() == storm::storage::DFTElementType::BE_EXP || |
|||
element->type() == storm::storage::DFTElementType::BE_CONST) { |
|||
auto be = std::static_pointer_cast<storm::storage::DFTBE<double> const>(element); |
|||
if (be->hasIngoingDependencies()) { |
|||
++nrDepEvents; |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Only need to check as long as bound candidate + nr of non-Markovians to check is smaller than number of dependent events
|
|||
while (nrNonMarkovian <= nrDepEvents && boundCandidate >= 0) { |
|||
if (nrNonMarkovian == 0 and boundCandidate == 0) { |
|||
nrNonMarkovian = 1; |
|||
} |
|||
STORM_LOG_TRACE( |
|||
"Lower bound correction - check possible bound " << std::to_string(boundCandidate) |
|||
<< " with " |
|||
<< std::to_string(nrNonMarkovian) |
|||
<< " non-Markovian states"); |
|||
// The uniqueness transformation for constantly failed BEs guarantees that a DFT never fails
|
|||
// in step 0 without intermediate non-Markovians, thus forcibly set nrNonMarkovian
|
|||
smtchecker->setSolverTimeout(timeout * 1000); |
|||
storm::solver::SmtSolver::CheckResult tmp_res = |
|||
smtchecker->checkFailsLeqWithEqNonMarkovianState(boundCandidate + nrNonMarkovian, |
|||
nrNonMarkovian); |
|||
smtchecker->unsetSolverTimeout(); |
|||
switch (tmp_res) { |
|||
case storm::solver::SmtSolver::CheckResult::Sat: |
|||
/* If SAT, there is a sequence where only boundCandidate-many BEs fail directly and rest is nonMarkovian.
|
|||
* Bound candidate is vaild, therefore check the next one */ |
|||
STORM_LOG_TRACE("Lower bound correction - SAT"); |
|||
// Prevent integer underflow
|
|||
if (boundCandidate == 0) { |
|||
STORM_LOG_DEBUG("Lower bound correction - corrected bound to 0"); |
|||
return 0; |
|||
} |
|||
--boundCandidate; |
|||
break; |
|||
case storm::solver::SmtSolver::CheckResult::Unknown: |
|||
// If any query returns unknown, we cannot be sure about the bound and fall back to the naive one
|
|||
STORM_LOG_DEBUG("Lower bound correction - Solver returned 'Unknown', corrected to 1"); |
|||
return 1; |
|||
default: |
|||
// if query is UNSAT, increase number of non-Markovian states and try again
|
|||
STORM_LOG_TRACE("Lower bound correction - UNSAT"); |
|||
++nrNonMarkovian; |
|||
break; |
|||
} |
|||
} |
|||
// if for one candidate all queries are UNSAT, it is not valid. Return last valid candidate
|
|||
STORM_LOG_DEBUG("Lower bound correction - corrected bound to " << std::to_string(boundCandidate + 1)); |
|||
return boundCandidate + 1; |
|||
} |
|||
|
|||
uint64_t |
|||
FailureBoundFinder::correctUpperBound(std::shared_ptr<storm::modelchecker::DFTASFChecker> smtchecker, |
|||
uint64_t bound, uint_fast64_t timeout) { |
|||
STORM_LOG_DEBUG("Upper bound correction - try to correct bound " << std::to_string(bound)); |
|||
uint64_t boundCandidate = bound; |
|||
uint64_t nrDepEvents = 0; |
|||
uint64_t nrNonMarkovian = 0; |
|||
uint64_t currentTimepoint = 0; |
|||
auto dft = smtchecker->getDFT(); |
|||
// Count dependent events
|
|||
for (size_t i = 0; i < dft.nrElements(); ++i) { |
|||
std::shared_ptr<storm::storage::DFTElement<double> const> element = dft.getElement(i); |
|||
if (element->type() == storm::storage::DFTElementType::BE_EXP || |
|||
element->type() == storm::storage::DFTElementType::BE_CONST) { |
|||
auto be = std::static_pointer_cast<storm::storage::DFTBE<double> const>(element); |
|||
if (be->hasIngoingDependencies()) { |
|||
++nrDepEvents; |
|||
} |
|||
} |
|||
} |
|||
while (boundCandidate >= 0) { |
|||
currentTimepoint = bound + 1; |
|||
while (currentTimepoint - boundCandidate > 0) { |
|||
--currentTimepoint; |
|||
nrNonMarkovian = currentTimepoint - boundCandidate; |
|||
STORM_LOG_TRACE( |
|||
"Upper bound correction - candidate " << std::to_string(boundCandidate) |
|||
<< " check split " |
|||
<< |
|||
std::to_string(currentTimepoint) << "|" |
|||
<< std::to_string(nrNonMarkovian)); |
|||
smtchecker->setSolverTimeout(timeout * 1000); |
|||
storm::solver::SmtSolver::CheckResult tmp_res = |
|||
smtchecker->checkFailsAtTimepointWithEqNonMarkovianState(currentTimepoint, |
|||
nrNonMarkovian); |
|||
smtchecker->unsetSolverTimeout(); |
|||
switch (tmp_res) { |
|||
case storm::solver::SmtSolver::CheckResult::Sat: |
|||
STORM_LOG_TRACE("Upper bound correction - SAT"); |
|||
STORM_LOG_DEBUG("Upper bound correction - corrected to bound " << boundCandidate << |
|||
" (TLE can fail at sequence point " |
|||
<< std::to_string( |
|||
currentTimepoint) |
|||
<< " with " |
|||
<< std::to_string( |
|||
nrNonMarkovian) |
|||
<< " non-Markovian states)"); |
|||
return boundCandidate; |
|||
case storm::solver::SmtSolver::CheckResult::Unknown: |
|||
// If any query returns unknown, we cannot be sure about the bound and fall back to the naive one
|
|||
STORM_LOG_DEBUG( |
|||
"Upper bound correction - Solver returned 'Unknown', corrected to bound " |
|||
<< bound); |
|||
return bound; |
|||
default: |
|||
// if query is UNSAT, increase number of non-Markovian states and try again
|
|||
STORM_LOG_TRACE("Lower bound correction - UNSAT"); |
|||
break; |
|||
} |
|||
} |
|||
--boundCandidate; |
|||
} |
|||
|
|||
// if for one candidate all queries are UNSAT, it is not valid. Return last valid candidate
|
|||
STORM_LOG_DEBUG("Upper bound correction - corrected bound to " << std::to_string(boundCandidate)); |
|||
return boundCandidate; |
|||
} |
|||
|
|||
uint64_t FailureBoundFinder::getLeastFailureBound(storm::storage::DFT<double> const &dft, |
|||
bool useSMT, uint_fast64_t timeout) { |
|||
if (useSMT) { |
|||
STORM_LOG_TRACE("Compute lower bound for number of BE failures necessary for the DFT to fail"); |
|||
|
|||
storm::modelchecker::DFTASFChecker smtchecker(dft); |
|||
smtchecker.activateExperimentalMode(); |
|||
smtchecker.toSolver(); |
|||
|
|||
uint64_t bound = 0; |
|||
while (bound < dft.nrBasicElements() + 1) { |
|||
smtchecker.setSolverTimeout(timeout * 1000); |
|||
storm::solver::SmtSolver::CheckResult tmp_res = smtchecker.checkTleFailsWithLeq(bound); |
|||
smtchecker.unsetSolverTimeout(); |
|||
switch (tmp_res) { |
|||
case storm::solver::SmtSolver::CheckResult::Sat: |
|||
if (!dft.getDependencies().empty()) { |
|||
return correctLowerBound( |
|||
std::make_shared<storm::modelchecker::DFTASFChecker>(smtchecker), bound, |
|||
timeout); |
|||
} else { |
|||
return bound; |
|||
} |
|||
case storm::solver::SmtSolver::CheckResult::Unknown: |
|||
STORM_LOG_DEBUG("Lower bound: Solver returned 'Unknown'"); |
|||
return bound; |
|||
default: |
|||
++bound; |
|||
break; |
|||
} |
|||
|
|||
} |
|||
|
|||
return bound; |
|||
} else { |
|||
// naive bound
|
|||
return 1; |
|||
} |
|||
} |
|||
|
|||
uint64_t FailureBoundFinder::getLeastFailureBound(storm::storage::DFT<RationalFunction> const &dft, |
|||
bool useSMT, uint_fast64_t timeout) { |
|||
if (useSMT) { |
|||
STORM_LOG_WARN("SMT encoding does not support rational functions"); |
|||
} |
|||
return 1; |
|||
} |
|||
|
|||
uint64_t FailureBoundFinder::getAlwaysFailedBound(storm::storage::DFT<double> const &dft, bool useSMT, |
|||
uint_fast64_t timeout) { |
|||
STORM_LOG_TRACE("Compute bound for number of BE failures such that the DFT always fails"); |
|||
if (useSMT) { |
|||
|
|||
storm::modelchecker::DFTASFChecker smtchecker(dft); |
|||
smtchecker.activateExperimentalMode(); |
|||
smtchecker.toSolver(); |
|||
|
|||
if (smtchecker.checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) { |
|||
return dft.nrBasicElements() + 1; |
|||
} |
|||
uint64_t bound = dft.nrBasicElements(); |
|||
while (bound >= 0) { |
|||
smtchecker.setSolverTimeout(timeout * 1000); |
|||
storm::solver::SmtSolver::CheckResult tmp_res = smtchecker.checkTleFailsWithEq(bound); |
|||
smtchecker.unsetSolverTimeout(); |
|||
switch (tmp_res) { |
|||
case storm::solver::SmtSolver::CheckResult::Sat: |
|||
if (!dft.getDependencies().empty()) { |
|||
return correctUpperBound( |
|||
std::make_shared<storm::modelchecker::DFTASFChecker>(smtchecker), bound, |
|||
timeout); |
|||
} else { |
|||
return bound; |
|||
} |
|||
case storm::solver::SmtSolver::CheckResult::Unknown: |
|||
STORM_LOG_DEBUG("Upper bound: Solver returned 'Unknown'"); |
|||
return bound; |
|||
default: |
|||
--bound; |
|||
break; |
|||
} |
|||
} |
|||
return bound; |
|||
} else { |
|||
// naive bound
|
|||
return dft.nrBasicElements() + 1; |
|||
} |
|||
} |
|||
|
|||
uint64_t |
|||
FailureBoundFinder::getAlwaysFailedBound(storm::storage::DFT<RationalFunction> const &dft, bool useSMT, |
|||
uint_fast64_t timeout) { |
|||
if (useSMT) { |
|||
STORM_LOG_WARN("SMT encoding does not support rational functions"); |
|||
} |
|||
return dft.nrBasicElements() + 1; |
|||
} |
|||
|
|||
class FailureBoundFinder; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,73 @@ |
|||
#include <vector> |
|||
#include "storm-dft/storage/dft/DFT.h" |
|||
#include "storm-dft/modelchecker/dft/DFTASFChecker.h" |
|||
|
|||
namespace storm { |
|||
namespace dft { |
|||
namespace utility { |
|||
class FailureBoundFinder { |
|||
public: |
|||
/** |
|||
* Get the minimal number of BEs necessary for the TLE to fail (lower bound for number of failures to check) |
|||
* |
|||
* @param dft the DFT to check |
|||
* @param useSMT if set, an SMT solver is used to improve the bounds |
|||
* @param timeout timeout for each query in seconds, defaults to 10 seconds |
|||
* @return the minimal number |
|||
*/ |
|||
static uint64_t getLeastFailureBound(storm::storage::DFT<double> const &dft, |
|||
bool useSMT = false, |
|||
uint_fast64_t timeout = 10); |
|||
|
|||
static uint64_t getLeastFailureBound(storm::storage::DFT<storm::RationalFunction> const &dft, |
|||
bool useSMT = false, |
|||
uint_fast64_t timeout = 10); |
|||
|
|||
/** |
|||
* Get the number of BE failures for which the TLE always fails (upper bound for number of failures to check). |
|||
* |
|||
* @param dft the DFT to check |
|||
* @param useSMT if set, an SMT solver is used to improve the bounds |
|||
* @param timeout timeout for each query in seconds, defaults to 10 seconds |
|||
* @return the number |
|||
*/ |
|||
static uint64_t getAlwaysFailedBound(storm::storage::DFT<double> const &dft, |
|||
bool useSMT = false, |
|||
uint_fast64_t timeout = 10); |
|||
|
|||
static uint64_t getAlwaysFailedBound(storm::storage::DFT<storm::RationalFunction> const &dft, |
|||
bool useSMT = false, |
|||
uint_fast64_t timeout = 10); |
|||
|
|||
private: |
|||
/** |
|||
* Helper function for correction of least failure bound when dependencies are present. |
|||
* The main idea is to check if a later point of failure for the TLE than the pre-computed bound exists, but |
|||
* up until that point the number of non-Markovian states visited is so large, that less than the pre-computed bound BEs fail by themselves. |
|||
* The corrected bound is then (newTLEFailureTimepoint)-(nrNonMarkovianStatesVisited). This term is minimized. |
|||
* |
|||
* @param smtchecker the SMT checker to use |
|||
* @param bound known lower bound to be corrected |
|||
* @param timeout timeout timeout for each query in seconds |
|||
* @return the corrected bound |
|||
*/ |
|||
static uint64_t |
|||
correctLowerBound(std::shared_ptr<storm::modelchecker::DFTASFChecker> smtchecker, uint64_t bound, |
|||
uint_fast64_t timeout); |
|||
|
|||
/** |
|||
* Helper function for correction of bound for number of BEs such that the DFT always fails when dependencies are present |
|||
* |
|||
* @param smtchecker the SMT checker to use |
|||
* @param bound known bound to be corrected |
|||
* @param timeout timeout timeout for each query in seconds |
|||
* @return the corrected bound |
|||
*/ |
|||
static uint64_t |
|||
correctUpperBound(std::shared_ptr<storm::modelchecker::DFTASFChecker> smtchecker, uint64_t bound, |
|||
uint_fast64_t timeout); |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
Reference in new issue
xxxxxxxxxx