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

Decoupled preprocessing and SMT solving in commandline interface

tempestpy_adaptions
Alexander Bork 6 years ago
parent
449c513db2
commit
ec67166041
3 changed files with 60 additions and 45 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. 68
      src/storm-dft-cli/storm-dft.cpp
  2. 35
      src/storm-dft/api/storm-dft.cpp
  3. 2
      src/storm-dft/api/storm-dft.h

68
src/storm-dft-cli/storm-dft.cpp
View File

@ -28,7 +28,6 @@ void processOptions() {
storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();
storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule<storm::settings::modules::DftGspnSettings>();
auto const &debug = storm::settings::getModule<storm::settings::modules::DebugSettings>();
auto dftTransformator = storm::transformations::dft::DftTransformator<ValueType>();
@ -90,33 +89,72 @@ void processOptions() {
return;
}
// TODO introduce some flags
bool useSMT = false;
bool printOutput = false;
uint64_t solverTimeout = 10;
#ifdef STORM_HAVE_Z3
if (faultTreeSettings.solveWithSMT()) {
useSMT = true;
STORM_PRINT("Use SMT for preprocessing" << std::endl)
dft = dftTransformator.transformUniqueFailedBe(*dft);
if (dft->getDependencies().size() > 0) {
// Making the constantly failed BE unique may introduce non-binary FDEPs
dft = dftTransformator.transformBinaryFDEPs(*dft);
}
}
#endif
dft->setDynamicBehaviorInfo();
storm::api::PreprocessingResult preResults;
preResults.lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, useSMT,
solverTimeout);
preResults.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, useSMT,
solverTimeout);
if (printOutput) {
STORM_PRINT("BE FAILURE BOUNDS" << std::endl <<
"========================================" << std::endl <<
"Lower bound: " << std::to_string(preResults.lowerBEBound) << std::endl <<
"Upper bound: " << std::to_string(preResults.upperBEBound) << std::endl)
}
preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true,
solverTimeout);
if (printOutput) {
STORM_PRINT("========================================" << std::endl <<
"FDEP CONFLICTS" << std::endl <<
"========================================"
<< std::endl)
for (auto pair: preResults.fdepConflicts) {
STORM_PRINT("Conflict between " << dft->getElement(pair.first)->name() << " and "
<< dft->getElement(pair.second)->name() << std::endl)
}
}
// Set the conflict map of the dft
std::set<size_t> conflict_set;
for (auto conflict : preResults.fdepConflicts) {
conflict_set.insert(size_t(conflict.first));
conflict_set.insert(size_t(conflict.second));
}
for (size_t depId : dft->getDependencies()) {
if (!conflict_set.count(depId)) {
dft->setDependencyNotInConflict(depId);
}
}
#ifdef STORM_HAVE_Z3
if (faultTreeSettings.solveWithSMT()) {
// Solve with SMT
STORM_LOG_DEBUG("Running DFT analysis with use of SMT");
// Set dynamic behavior vector
dft->setDynamicBehaviorInfo();
auto smtResults = storm::api::analyzeDFTSMT(*dft, true);
// Set the conflict map of the dft
std::set<size_t> conflict_set;
for (auto conflict : smtResults.fdepConflicts) {
conflict_set.insert(size_t(conflict.first));
conflict_set.insert(size_t(conflict.second));
}
for (size_t depId : dft->getDependencies()) {
if (!conflict_set.count(depId)) {
dft->setDependencyNotInConflict(depId);
}
}
storm::api::analyzeDFTSMT(*dft, true);
}
#endif
//Proprocessing
// From now on we analyse DFT via model checking

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

@ -43,43 +43,20 @@ namespace storm {
}
template<>
storm::api::PreprocessingResult
void
analyzeDFTSMT(storm::storage::DFT<double> const &dft, bool printOutput) {
uint64_t solverTimeout = 10;
storm::modelchecker::DFTASFChecker smtChecker(dft);
smtChecker.toSolver();
storm::api::PreprocessingResult results;
results.lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(dft, true,
solverTimeout);
results.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(dft, true,
solverTimeout);
if (printOutput) {
STORM_PRINT("BE FAILURE BOUNDS" << std::endl <<
"========================================" << std::endl <<
"Lower bound: " << std::to_string(results.lowerBEBound) << std::endl <<
"Upper bound: " << std::to_string(results.upperBEBound) << std::endl)
}
results.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(dft, true,
solverTimeout);
if (printOutput) {
STORM_PRINT("========================================" << std::endl <<
"FDEP CONFLICTS" << std::endl <<
"========================================"
<< std::endl)
for (auto pair: results.fdepConflicts) {
STORM_PRINT("Conflict between " << dft.getElement(pair.first)->name() << " and "
<< dft.getElement(pair.second)->name() << std::endl)
}
}
return results;
// Removed bound computation etc. here
smtChecker.setSolverTimeout(solverTimeout);
smtChecker.checkTleNeverFailed();
smtChecker.unsetSolverTimeout();
}
template<>
storm::api::PreprocessingResult
void
analyzeDFTSMT(storm::storage::DFT<storm::RationalFunction> const &dft, bool printOutput) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
"Analysis by SMT not supported for this data type.");

2
src/storm-dft/api/storm-dft.h
View File

@ -108,7 +108,7 @@ namespace storm {
* @return Result result vector
*/
template<typename ValueType>
storm::api::PreprocessingResult
void
analyzeDFTSMT(storm::storage::DFT<ValueType> const &dft, bool printOutput);
/*!

Write Preview
Loading…
Cancel
Save