Matthias Volk
7 years ago
44 changed files with 2409 additions and 435 deletions
-
8resources/examples/testfiles/dft/const_be_test.dft
-
12resources/examples/testfiles/dft/seq_conflict_test.dft
-
12resources/examples/testfiles/dft/spare_conflict_test.dft
-
26src/storm-cli-utilities/model-handling.h
-
82src/storm-dft-cli/storm-dft.cpp
-
33src/storm-dft/api/storm-dft.cpp
-
21src/storm-dft/api/storm-dft.h
-
1src/storm-dft/builder/DFTBuilder.cpp
-
49src/storm-dft/builder/DFTBuilder.h
-
25src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
-
144src/storm-dft/generator/DftNextStateGenerator.cpp
-
20src/storm-dft/generator/DftNextStateGenerator.h
-
299src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
-
60src/storm-dft/modelchecker/dft/DFTASFChecker.h
-
189src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
-
15src/storm-dft/modelchecker/dft/DFTModelChecker.h
-
94src/storm-dft/modelchecker/dft/SmtConstraint.cpp
-
23src/storm-dft/parser/DFTGalileoParser.cpp
-
3src/storm-dft/parser/DFTGalileoParser.h
-
2src/storm-dft/settings/DftSettings.cpp
-
7src/storm-dft/settings/modules/FaultTreeSettings.cpp
-
8src/storm-dft/settings/modules/FaultTreeSettings.h
-
156src/storm-dft/storage/dft/DFT.cpp
-
21src/storm-dft/storage/dft/DFT.h
-
4src/storm-dft/storage/dft/DFTState.cpp
-
54src/storm-dft/storage/dft/DFTState.h
-
253src/storm-dft/transformations/DftTransformator.cpp
-
35src/storm-dft/transformations/DftTransformator.h
-
111src/storm-dft/utility/FDEPConflictFinder.cpp
-
29src/storm-dft/utility/FDEPConflictFinder.h
-
239src/storm-dft/utility/FailureBoundFinder.cpp
-
73src/storm-dft/utility/FailureBoundFinder.h
-
14src/storm-pars-cli/storm-pars.cpp
-
26src/storm/api/transformation.h
-
62src/storm/models/sparse/MarkovAutomaton.cpp
-
1src/storm/models/sparse/MarkovAutomaton.h
-
2src/storm/settings/SettingsManager.cpp
-
49src/storm/settings/modules/TransformationSettings.cpp
-
56src/storm/settings/modules/TransformationSettings.h
-
299src/storm/transformer/NonMarkovianChainTransformer.cpp
-
46src/storm/transformer/NonMarkovianChainTransformer.h
-
67src/test/storm-dft/api/DftModelCheckerTest.cpp
-
45src/test/storm-dft/api/DftSmtTest.cpp
-
69src/test/storm-dft/api/DftTransformatorTest.cpp
@ -0,0 +1,8 @@ |
|||
toplevel "A"; |
|||
"A" and "I" "J" "K" "L"; |
|||
"DEP1" fdep "I" "J" "K"; |
|||
|
|||
"I" prob=1; |
|||
"J" prob=1; |
|||
"K" prob=1; |
|||
"L" lambda=1.0 dorm=0.5; |
|||
@ -0,0 +1,12 @@ |
|||
toplevel "A"; |
|||
"A" and "I" "B"; |
|||
"SEQ_dynamic" seq "I" "B"; |
|||
"B" or "J" "K"; |
|||
"DEP1_1" fdep "T1" "I"; |
|||
"DEP1_2" fdep "T1" "J"; |
|||
"DEP1_3" fdep "T1" "K"; |
|||
|
|||
"I" lambda=0.5 dorm=0; |
|||
"J" lambda=0.5 dorm=0; |
|||
"K" lambda=0.5 dorm=0; |
|||
"T1" lambda=0.5 dorm=0; |
|||
@ -0,0 +1,12 @@ |
|||
toplevel "A"; |
|||
"A" pand "SP1" "SP2"; |
|||
"SP1" wsp "I" "J"; |
|||
"SP2" wsp "J" "K"; |
|||
"DEP1" fdep "T1" "I"; |
|||
"DEP2" fdep "T2" "K"; |
|||
|
|||
"I" lambda=0.5 dorm=0; |
|||
"J" lambda=0.5 dorm=0; |
|||
"K" lambda=0.5 dorm=0; |
|||
"T1" lambda=0.5 dorm=0; |
|||
"T2" lambda=0.5 dorm=0; |
|||
@ -0,0 +1,253 @@ |
|||
#include "DftTransformator.h"
|
|||
#include "storm/exceptions/NotImplementedException.h"
|
|||
|
|||
namespace storm { |
|||
namespace transformations { |
|||
namespace dft { |
|||
template<typename ValueType> |
|||
DftTransformator<ValueType>::DftTransformator() { |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::shared_ptr<storm::storage::DFT<ValueType>> |
|||
DftTransformator<ValueType>::transformUniqueFailedBe(storm::storage::DFT<ValueType> const &dft) { |
|||
STORM_LOG_DEBUG("Start transformation UniqueFailedBe"); |
|||
storm::builder::DFTBuilder<ValueType> builder = storm::builder::DFTBuilder<ValueType>(true); |
|||
// NOTE: if probabilities for constant BEs are introduced, change this to vector of tuples (name, prob)
|
|||
std::vector<std::string> failedBEs; |
|||
|
|||
for (size_t i = 0; i < dft.nrElements(); ++i) { |
|||
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i); |
|||
switch (element->type()) { |
|||
case storm::storage::DFTElementType::BE_EXP: { |
|||
auto be_exp = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>( |
|||
element); |
|||
builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(), |
|||
be_exp->dormancyFactor()); |
|||
break; |
|||
} |
|||
case storm::storage::DFTElementType::BE_CONST: { |
|||
auto be_const = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>( |
|||
element); |
|||
if (be_const->canFail()) { |
|||
STORM_LOG_TRACE("Transform " + element->name() + " [BE (const failed)]"); |
|||
failedBEs.push_back(be_const->name()); |
|||
} |
|||
// All original constant BEs are set to failsafe, failed BEs are later triggered by a new element
|
|||
builder.addBasicElementConst(be_const->name(), false); |
|||
break; |
|||
} |
|||
case storm::storage::DFTElementType::AND: |
|||
builder.addAndElement(element->name(), getChildrenVector(element)); |
|||
break; |
|||
case storm::storage::DFTElementType::OR: |
|||
builder.addOrElement(element->name(), getChildrenVector(element)); |
|||
break; |
|||
case storm::storage::DFTElementType::VOT: { |
|||
auto vot = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(element); |
|||
builder.addVotElement(vot->name(), vot->threshold(), getChildrenVector(vot)); |
|||
break; |
|||
} |
|||
case storm::storage::DFTElementType::PAND: { |
|||
auto pand = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(element); |
|||
builder.addPandElement(pand->name(), getChildrenVector(pand), pand->isInclusive()); |
|||
break; |
|||
} |
|||
case storm::storage::DFTElementType::POR: { |
|||
auto por = std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(element); |
|||
builder.addPandElement(por->name(), getChildrenVector(por), por->isInclusive()); |
|||
break; |
|||
} |
|||
case storm::storage::DFTElementType::SPARE: |
|||
builder.addSpareElement(element->name(), getChildrenVector(element)); |
|||
break; |
|||
case storm::storage::DFTElementType::PDEP: { |
|||
auto dep = std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>( |
|||
element); |
|||
builder.addDepElement(dep->name(), getChildrenVector(dep), dep->probability()); |
|||
break; |
|||
} |
|||
case storm::storage::DFTElementType::SEQ: |
|||
builder.addSequenceEnforcer(element->name(), getChildrenVector(element)); |
|||
break; |
|||
case storm::storage::DFTElementType::MUTEX: |
|||
builder.addMutex(element->name(), getChildrenVector(element)); |
|||
break; |
|||
default: |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, |
|||
"DFT type '" << element->type() << "' not known."); |
|||
break; |
|||
} |
|||
|
|||
} |
|||
// At this point the DFT is an exact copy of the original, except for all constant failure probabilities being 0
|
|||
|
|||
// Introduce new constantly failed BE and FDEPs to trigger all failures
|
|||
if (!failedBEs.empty()) { |
|||
STORM_LOG_TRACE("Add Unique_Constant_Failure [BE (const failed)]"); |
|||
builder.addBasicElementConst("Unique_Constant_Failure", true); |
|||
failedBEs.insert(std::begin(failedBEs), "Unique_Constant_Failure"); |
|||
STORM_LOG_TRACE("Add Failure_Trigger [FDEP]"); |
|||
builder.addDepElement("Failure_Trigger", failedBEs, storm::utility::one<ValueType>()); |
|||
} |
|||
|
|||
builder.setTopLevel(dft.getTopLevelGate()->name()); |
|||
|
|||
STORM_LOG_DEBUG("Transformation UniqueFailedBe complete"); |
|||
return std::make_shared<storm::storage::DFT<ValueType>>(builder.build()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::shared_ptr<storm::storage::DFT<ValueType>> |
|||
DftTransformator<ValueType>::transformBinaryFDEPs(storm::storage::DFT<ValueType> const &dft) { |
|||
STORM_LOG_DEBUG("Start transformation BinaryFDEPs"); |
|||
storm::builder::DFTBuilder<ValueType> builder = storm::builder::DFTBuilder<ValueType>(true); |
|||
|
|||
for (size_t i = 0; i < dft.nrElements(); ++i) { |
|||
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i); |
|||
switch (element->type()) { |
|||
case storm::storage::DFTElementType::BE_EXP: { |
|||
auto be_exp = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>( |
|||
element); |
|||
builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(), |
|||
be_exp->dormancyFactor()); |
|||
break; |
|||
} |
|||
case storm::storage::DFTElementType::BE_CONST: { |
|||
auto be_const = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>( |
|||
element); |
|||
// All original constant BEs are set to failsafe, failed BEs are later triggered by a new element
|
|||
builder.addBasicElementConst(be_const->name(), be_const->canFail()); |
|||
break; |
|||
} |
|||
case storm::storage::DFTElementType::AND: |
|||
builder.addAndElement(element->name(), getChildrenVector(element)); |
|||
break; |
|||
case storm::storage::DFTElementType::OR: |
|||
builder.addOrElement(element->name(), getChildrenVector(element)); |
|||
break; |
|||
case storm::storage::DFTElementType::VOT: { |
|||
auto vot = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(element); |
|||
builder.addVotElement(vot->name(), vot->threshold(), getChildrenVector(vot)); |
|||
break; |
|||
} |
|||
case storm::storage::DFTElementType::PAND: { |
|||
auto pand = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(element); |
|||
builder.addPandElement(pand->name(), getChildrenVector(pand), pand->isInclusive()); |
|||
break; |
|||
} |
|||
case storm::storage::DFTElementType::POR: { |
|||
auto por = std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(element); |
|||
builder.addPandElement(por->name(), getChildrenVector(por), por->isInclusive()); |
|||
break; |
|||
} |
|||
case storm::storage::DFTElementType::SPARE: |
|||
builder.addSpareElement(element->name(), getChildrenVector(element)); |
|||
break; |
|||
case storm::storage::DFTElementType::PDEP: { |
|||
auto dep = std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>( |
|||
element); |
|||
auto children = getChildrenVector(dep); |
|||
if (!storm::utility::isOne(dep->probability())) { |
|||
if (children.size() > 2) { |
|||
STORM_LOG_TRACE("Transform " + element->name() + " [PDEP]"); |
|||
// Introduce additional element for first capturing the probabilistic dependency
|
|||
std::string nameAdditional = dep->name() + "_additional"; |
|||
STORM_LOG_TRACE("Add auxilliary BE " << nameAdditional); |
|||
builder.addBasicElementConst(nameAdditional, false); |
|||
STORM_LOG_TRACE("Add " << dep->name() << "_pdep [PDEP]"); |
|||
// First consider probabilistic dependency
|
|||
builder.addDepElement(dep->name() + "_pdep", {children.front(), nameAdditional}, |
|||
dep->probability()); |
|||
// Then consider dependencies to the children if probabilistic dependency failed
|
|||
children.erase(children.begin()); |
|||
size_t i = 1; |
|||
for (auto const &child : children) { |
|||
std::string nameDep = dep->name() + "_" + std::to_string(i); |
|||
if (builder.nameInUse(nameDep)) { |
|||
STORM_LOG_ERROR("Element with name '" << nameDep << "' already exists."); |
|||
} |
|||
STORM_LOG_TRACE("Add " << nameDep << " [FDEP]"); |
|||
builder.addDepElement(nameDep, {dep->name() + "_additional", child}, |
|||
storm::utility::one<ValueType>()); |
|||
++i; |
|||
} |
|||
} else { |
|||
builder.addDepElement(dep->name(), children, dep->probability()); |
|||
} |
|||
} else { |
|||
// Add dependencies
|
|||
for (size_t i = 1; i < children.size(); ++i) { |
|||
std::string nameDep; |
|||
if (children.size() == 2) { |
|||
nameDep = dep->name(); |
|||
} else { |
|||
nameDep = dep->name() + "_" + std::to_string(i); |
|||
STORM_LOG_TRACE("Transform " + element->name() + " [FDEP]"); |
|||
STORM_LOG_TRACE("Add " + nameDep + " [FDEP]"); |
|||
} |
|||
if (builder.nameInUse(nameDep)) { |
|||
STORM_LOG_ERROR("Element with name '" << nameDep << "' already exists."); |
|||
} |
|||
STORM_LOG_ASSERT(storm::utility::isOne(dep->probability()) || children.size() == 2, |
|||
"PDEP with multiple children supported."); |
|||
builder.addDepElement(nameDep, {children[0], children[i]}, |
|||
storm::utility::one<ValueType>()); |
|||
} |
|||
} |
|||
break; |
|||
} |
|||
case storm::storage::DFTElementType::SEQ: |
|||
builder.addSequenceEnforcer(element->name(), getChildrenVector(element)); |
|||
break; |
|||
case storm::storage::DFTElementType::MUTEX: |
|||
builder.addMutex(element->name(), getChildrenVector(element)); |
|||
break; |
|||
default: |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, |
|||
"DFT type '" << element->type() << "' not known."); |
|||
break; |
|||
} |
|||
|
|||
} |
|||
|
|||
builder.setTopLevel(dft.getTopLevelGate()->name()); |
|||
|
|||
STORM_LOG_DEBUG("Transformation BinaryFDEPs complete"); |
|||
return std::make_shared<storm::storage::DFT<ValueType>>(builder.build()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::vector<std::string> DftTransformator<ValueType>::getChildrenVector( |
|||
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element) { |
|||
std::vector<std::string> res; |
|||
if (element->isDependency()) { |
|||
// Dependencies have to be handled separately
|
|||
auto dependency = std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(element); |
|||
res.push_back(dependency->triggerEvent()->name()); |
|||
for (auto const &depEvent : dependency->dependentEvents()) { |
|||
res.push_back(depEvent->name()); |
|||
} |
|||
} else { |
|||
auto elementWithChildren = std::static_pointer_cast<storm::storage::DFTChildren<ValueType> const>( |
|||
element); |
|||
for (auto const &child : elementWithChildren->children()) { |
|||
res.push_back(child->name()); |
|||
} |
|||
} |
|||
return res; |
|||
} |
|||
|
|||
// Explicitly instantiate the class.
|
|||
template |
|||
class DftTransformator<double>; |
|||
|
|||
#ifdef STORM_HAVE_CARL
|
|||
|
|||
template |
|||
class DftTransformator<RationalFunction>; |
|||
|
|||
#endif
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,35 @@ |
|||
#include "storm-dft/storage/dft/DFT.h" |
|||
#include "storm-dft/builder/DFTBuilder.h" |
|||
#include "storm/utility/macros.h" |
|||
|
|||
namespace storm { |
|||
namespace transformations { |
|||
namespace dft { |
|||
|
|||
/*! |
|||
* Transformator for DFT -> DFT. |
|||
*/ |
|||
template<typename ValueType> |
|||
class DftTransformator { |
|||
|
|||
public: |
|||
/*! |
|||
* Constructor. |
|||
* |
|||
* @param dft DFT |
|||
*/ |
|||
DftTransformator(); |
|||
|
|||
std::shared_ptr<storm::storage::DFT<ValueType>> |
|||
transformUniqueFailedBe(storm::storage::DFT<ValueType> const &dft); |
|||
|
|||
std::shared_ptr<storm::storage::DFT<ValueType>> |
|||
transformBinaryFDEPs(storm::storage::DFT<ValueType> const &dft); |
|||
|
|||
private: |
|||
std::vector<std::string> |
|||
getChildrenVector(std::shared_ptr<storm::storage::DFTElement<ValueType> const> element); |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,111 @@ |
|||
#include "FDEPConflictFinder.h"
|
|||
|
|||
namespace storm { |
|||
namespace dft { |
|||
namespace utility { |
|||
|
|||
std::vector<std::pair<uint64_t, uint64_t>> |
|||
FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT<double> const &dft, |
|||
bool useSMT, |
|||
uint_fast64_t timeout) { |
|||
|
|||
std::shared_ptr<storm::modelchecker::DFTASFChecker> smtChecker = nullptr; |
|||
if (useSMT) { |
|||
storm::modelchecker::DFTASFChecker checker(dft); |
|||
smtChecker = std::make_shared<storm::modelchecker::DFTASFChecker>(checker); |
|||
smtChecker->toSolver(); |
|||
} |
|||
|
|||
std::vector<std::pair<uint64_t, uint64_t>> res; |
|||
uint64_t dep1Index; |
|||
uint64_t dep2Index; |
|||
for (size_t i = 0; i < dft.getDependencies().size(); ++i) { |
|||
dep1Index = dft.getDependencies().at(i); |
|||
for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) { |
|||
dep2Index = dft.getDependencies().at(j); |
|||
if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) { |
|||
if (useSMT) { // if an SMT solver is to be used
|
|||
if (dft.getDependency(dep1Index)->triggerEvent() == |
|||
dft.getDependency(dep2Index)->triggerEvent()) { |
|||
STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " |
|||
<< dft.getElement(dep2Index)->name() |
|||
<< ": Same trigger"); |
|||
res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index)); |
|||
} else { |
|||
switch (smtChecker->checkDependencyConflict(dep1Index, dep2Index, timeout)) { |
|||
case storm::solver::SmtSolver::CheckResult::Sat: |
|||
STORM_LOG_DEBUG( |
|||
"Conflict between " << dft.getElement(dep1Index)->name() << " and " |
|||
<< dft.getElement(dep2Index)->name()); |
|||
res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index)); |
|||
break; |
|||
case storm::solver::SmtSolver::CheckResult::Unknown: |
|||
STORM_LOG_DEBUG( |
|||
"Unknown: Conflict between " << dft.getElement(dep1Index)->name() |
|||
<< " and " |
|||
<< dft.getElement(dep2Index)->name()); |
|||
res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index)); |
|||
break; |
|||
default: |
|||
STORM_LOG_DEBUG( |
|||
"No conflict between " << dft.getElement(dep1Index)->name() |
|||
<< " and " |
|||
<< dft.getElement(dep2Index)->name()); |
|||
break; |
|||
} |
|||
} |
|||
} else { |
|||
STORM_LOG_DEBUG( |
|||
"Conflict between " << dft.getElement(dep1Index)->name() << " and " |
|||
<< dft.getElement(dep2Index)->name()); |
|||
res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index)); |
|||
} |
|||
} else { |
|||
STORM_LOG_DEBUG( |
|||
"Static behavior: No conflict between " << dft.getElement(dep1Index)->name() |
|||
<< " and " |
|||
<< dft.getElement(dep2Index)->name()); |
|||
break; |
|||
} |
|||
} |
|||
} |
|||
return res; |
|||
} |
|||
|
|||
std::vector<std::pair<uint64_t, uint64_t>> |
|||
FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT<storm::RationalFunction> const &dft, |
|||
bool useSMT, |
|||
uint_fast64_t timeout) { |
|||
if (useSMT) { |
|||
STORM_LOG_WARN("SMT encoding for rational functions is not supported"); |
|||
} |
|||
|
|||
std::vector<std::pair<uint64_t, uint64_t>> res; |
|||
uint64_t dep1Index; |
|||
uint64_t dep2Index; |
|||
for (size_t i = 0; i < dft.getDependencies().size(); ++i) { |
|||
dep1Index = dft.getDependencies().at(i); |
|||
for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) { |
|||
dep2Index = dft.getDependencies().at(j); |
|||
if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) { |
|||
STORM_LOG_DEBUG( |
|||
"Conflict between " << dft.getElement(dep1Index)->name() << " and " |
|||
<< dft.getElement(dep2Index)->name()); |
|||
res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index)); |
|||
} else { |
|||
STORM_LOG_DEBUG( |
|||
"Static behavior: No conflict between " << dft.getElement(dep1Index)->name() |
|||
<< " and " |
|||
<< dft.getElement(dep2Index)->name()); |
|||
break; |
|||
} |
|||
} |
|||
} |
|||
return res; |
|||
} |
|||
|
|||
class FDEPConflictFinder; |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,29 @@ |
|||
#include <vector> |
|||
#include "storm-dft/storage/dft/DFT.h" |
|||
#include "storm-dft/modelchecker/dft/DFTASFChecker.h" |
|||
|
|||
namespace storm { |
|||
namespace dft { |
|||
namespace utility { |
|||
class FDEPConflictFinder { |
|||
public: |
|||
/** |
|||
* Get a vector of index pairs of FDEPs in the DFT which are conflicting. Two FDEPs are conflicting if |
|||
* their simultaneous triggering may cause unresolvable non-deterministic behavior. |
|||
* |
|||
* @param dft the DFT |
|||
* @param useSMT if set, an SMT solver is used to refine the conflict set |
|||
* @param timeout timeout for each query in seconds, defaults to 10 seconds |
|||
* @return a vector of pairs of indices. The indices in a pair refer to FDEPs which are conflicting |
|||
*/ |
|||
static std::vector<std::pair<uint64_t, uint64_t>> |
|||
getDependencyConflicts(storm::storage::DFT<double> const &dft, |
|||
bool useSMT = false, uint_fast64_t timeout = 10); |
|||
|
|||
static std::vector<std::pair<uint64_t, uint64_t>> |
|||
getDependencyConflicts(storm::storage::DFT<storm::RationalFunction> const &dft, |
|||
bool useSMT = false, uint_fast64_t timeout = 10); |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,239 @@ |
|||
#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.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.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); |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
@ -0,0 +1,49 @@ |
|||
#include "TransformationSettings.h"
|
|||
|
|||
#include "storm/settings/Option.h"
|
|||
#include "storm/settings/OptionBuilder.h"
|
|||
#include "storm/exceptions/InvalidSettingsException.h"
|
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
|
|||
const std::string TransformationSettings::moduleName = "transformation"; |
|||
|
|||
const std::string TransformationSettings::chainEliminationOptionName = "eliminate-chains"; |
|||
const std::string TransformationSettings::ignoreLabelingOptionName = "ec-ignore-labeling"; |
|||
|
|||
|
|||
TransformationSettings::TransformationSettings() : ModuleSettings(moduleName) { |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, chainEliminationOptionName, false, |
|||
"If set, chains of non-Markovian states are eliminated if the resulting model is a Markov Automaton.").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, ignoreLabelingOptionName, false, |
|||
"If set, the elimination of chains ignores the labels for all non-Markovian states. This may cause wrong results.").build()); |
|||
} |
|||
|
|||
bool TransformationSettings::isChainEliminationSet() const { |
|||
return this->getOption(chainEliminationOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool TransformationSettings::isIgnoreLabelingSet() const { |
|||
return this->getOption(ignoreLabelingOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
|
|||
bool TransformationSettings::check() const { |
|||
// Ensure that labeling preservation is only set if chain elimination is set
|
|||
STORM_LOG_THROW(isChainEliminationSet() || !isIgnoreLabelingSet(), |
|||
storm::exceptions::InvalidSettingsException, |
|||
"Label preservation can only be chosen if chain elimination is applied."); |
|||
|
|||
return true; |
|||
} |
|||
|
|||
void TransformationSettings::finalize() { |
|||
//Intentionally left empty
|
|||
} |
|||
|
|||
|
|||
} // namespace modules
|
|||
} // namespace settings
|
|||
} // namespace storm
|
|||
@ -0,0 +1,56 @@ |
|||
#ifndef STORM_TRANSFORMATIONSETTINGS_H |
|||
#define STORM_TRANSFORMATIONSETTINGS_H |
|||
|
|||
#include "storm-config.h" |
|||
#include "storm/settings/modules/ModuleSettings.h" |
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
|
|||
/*! |
|||
* This class represents the model transformer settings |
|||
*/ |
|||
class TransformationSettings : public ModuleSettings { |
|||
public: |
|||
|
|||
/*! |
|||
* Creates a new set of transformer settings. |
|||
*/ |
|||
TransformationSettings(); |
|||
|
|||
/*! |
|||
* Retrieves whether the option to eliminate chains of non-Markovian states was set. |
|||
* |
|||
* @return True if the option to eliminate chains of non-Markovian states was set. |
|||
*/ |
|||
bool isChainEliminationSet() const; |
|||
|
|||
|
|||
/*! |
|||
* Retrieves whether the preserve-labeling option for jani was set. |
|||
* |
|||
* @return True if the preserve-labeling option was set. |
|||
*/ |
|||
bool isIgnoreLabelingSet() const; |
|||
|
|||
|
|||
bool check() const override; |
|||
|
|||
void finalize() override; |
|||
|
|||
// The name of the module. |
|||
static const std::string moduleName; |
|||
|
|||
private: |
|||
// Define the string names of the options as constants. |
|||
static const std::string chainEliminationOptionName; |
|||
static const std::string ignoreLabelingOptionName; |
|||
|
|||
}; |
|||
|
|||
} // namespace modules |
|||
} // namespace settings |
|||
} // namespace storm |
|||
|
|||
#endif //STORM_TRANSFORMATIONSETTINGS_H |
|||
@ -0,0 +1,299 @@ |
|||
#include <queue>
|
|||
|
|||
#include "NonMarkovianChainTransformer.h"
|
|||
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/logic/FragmentSpecification.h"
|
|||
|
|||
#include "storm/storage/sparse/ModelComponents.h"
|
|||
#include "storm/adapters/RationalFunctionAdapter.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/utility/constants.h"
|
|||
#include "storm/utility/ConstantsComparator.h"
|
|||
#include "storm/utility/vector.h"
|
|||
#include "storm/utility/macros.h"
|
|||
#include "storm/utility/graph.h"
|
|||
|
|||
namespace storm { |
|||
namespace transformer { |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::shared_ptr<models::sparse::Model<ValueType, RewardModelType>> |
|||
NonMarkovianChainTransformer<ValueType, RewardModelType>::eliminateNonmarkovianStates( |
|||
std::shared_ptr<models::sparse::MarkovAutomaton<ValueType, RewardModelType>> ma, |
|||
bool preserveLabels) { |
|||
// TODO reward models
|
|||
|
|||
STORM_LOG_WARN_COND(preserveLabels, "Labels are not preserved! Results may be incorrect."); |
|||
STORM_LOG_WARN("Reward Models and Choice Labelings are ignored!"); |
|||
if (ma->isClosed() && ma->getMarkovianStates().full()) { |
|||
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> components( |
|||
ma->getTransitionMatrix(), ma->getStateLabeling(), ma->getRewardModels(), false); |
|||
components.exitRates = ma->getExitRates(); |
|||
if (ma->hasChoiceLabeling()) { |
|||
components.choiceLabeling = ma->getChoiceLabeling(); |
|||
} |
|||
if (ma->hasStateValuations()) { |
|||
components.stateValuations = ma->getStateValuations(); |
|||
} |
|||
if (ma->hasChoiceOrigins()) { |
|||
components.choiceOrigins = ma->getChoiceOrigins(); |
|||
} |
|||
return std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>>( |
|||
std::move(components)); |
|||
} |
|||
|
|||
std::map<uint_fast64_t, uint_fast64_t> eliminationMapping; |
|||
std::set<uint_fast64_t> statesToKeep; |
|||
std::queue<uint_fast64_t> changedStates; |
|||
std::queue<uint_fast64_t> queue; |
|||
|
|||
storm::storage::SparseMatrix<ValueType> backwards = ma->getBackwardTransitions(); |
|||
|
|||
// Determine the state remapping
|
|||
for (uint_fast64_t base_state = 0; base_state < ma->getNumberOfStates(); ++base_state) { |
|||
STORM_LOG_ASSERT(!ma->isHybridState(base_state), "Base state is hybrid."); |
|||
if (ma->isMarkovianState(base_state)) { |
|||
queue.push(base_state); |
|||
|
|||
while (!queue.empty()) { |
|||
auto currState = queue.front(); |
|||
queue.pop(); |
|||
|
|||
auto currLabels = ma->getLabelsOfState(currState); |
|||
|
|||
// Get predecessors from matrix
|
|||
typename storm::storage::SparseMatrix<ValueType>::rows entriesInRow = backwards.getRow( |
|||
currState); |
|||
for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); |
|||
entryIt != entryIte; ++entryIt) { |
|||
uint_fast64_t predecessor = entryIt->getColumn(); |
|||
if (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { |
|||
if (!preserveLabels || currLabels == ma->getLabelsOfState(predecessor)) { |
|||
// If labels are not to be preserved or states are labeled the same
|
|||
if (!eliminationMapping.count(predecessor)) { |
|||
eliminationMapping[predecessor] = base_state; |
|||
queue.push(predecessor); |
|||
} else if (eliminationMapping[predecessor] != base_state) { |
|||
eliminationMapping.erase(predecessor); |
|||
statesToKeep.insert(predecessor); |
|||
changedStates.push(predecessor); |
|||
} |
|||
} else { |
|||
// Labels are to be preserved and states have different labels
|
|||
if (eliminationMapping.count(predecessor)) { |
|||
eliminationMapping.erase(predecessor); |
|||
} |
|||
statesToKeep.insert(predecessor); |
|||
changedStates.push(predecessor); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Correct the mapping with the states which have to be kept
|
|||
while (!changedStates.empty()) { |
|||
uint_fast64_t base_state = changedStates.front(); |
|||
queue.push(base_state); |
|||
|
|||
while (!queue.empty()) { |
|||
auto currState = queue.front(); |
|||
queue.pop(); |
|||
|
|||
auto currLabels = ma->getLabelsOfState(currState); |
|||
|
|||
// Get predecessors from matrix
|
|||
typename storm::storage::SparseMatrix<ValueType>::rows entriesInRow = backwards.getRow( |
|||
currState); |
|||
for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); |
|||
entryIt != entryIte; ++entryIt) { |
|||
uint_fast64_t predecessor = entryIt->getColumn(); |
|||
if (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { |
|||
if (!preserveLabels || currLabels == ma->getLabelsOfState(predecessor)) { |
|||
// If labels are not to be preserved or states are labeled the same
|
|||
if (!eliminationMapping.count(predecessor)) { |
|||
eliminationMapping[predecessor] = base_state; |
|||
queue.push(predecessor); |
|||
} else if (eliminationMapping[predecessor] != base_state) { |
|||
eliminationMapping.erase(predecessor); |
|||
statesToKeep.insert(predecessor); |
|||
changedStates.push(predecessor); |
|||
} |
|||
} else { |
|||
// Labels are to be preserved and states have different labels
|
|||
if (eliminationMapping.count(predecessor)) { |
|||
eliminationMapping.erase(predecessor); |
|||
} |
|||
statesToKeep.insert(predecessor); |
|||
changedStates.push(predecessor); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
changedStates.pop(); |
|||
} |
|||
|
|||
// At this point, we hopefully have a valid mapping which eliminates a lot of states
|
|||
|
|||
STORM_LOG_TRACE("Elimination Mapping" << std::endl); |
|||
for (auto entry : eliminationMapping) { |
|||
STORM_LOG_TRACE(std::to_string(entry.first) << " -> " << std::to_string(entry.second) << std::endl); |
|||
} |
|||
STORM_LOG_INFO("Eliminating " << eliminationMapping.size() << " states" << std::endl); |
|||
|
|||
// TODO explore if one can construct elimination mapping and state remapping in one step
|
|||
|
|||
// Construct a mapping of old state space to new one
|
|||
std::vector<uint_fast64_t> stateRemapping(ma->getNumberOfStates(), -1); |
|||
uint_fast64_t currentNewState = 0; |
|||
for (uint_fast64_t state = 0; state < ma->getNumberOfStates(); ++state) { |
|||
if (eliminationMapping.count(state) > 0) { |
|||
if (stateRemapping[eliminationMapping[state]] == uint_fast64_t(-1)) { |
|||
stateRemapping[eliminationMapping[state]] = currentNewState; |
|||
stateRemapping[state] = currentNewState; |
|||
++currentNewState; |
|||
queue.push(eliminationMapping[state]); |
|||
} else { |
|||
stateRemapping[state] = stateRemapping[eliminationMapping[state]]; |
|||
} |
|||
} else if (stateRemapping[state] == uint_fast64_t(-1)) { |
|||
stateRemapping[state] = currentNewState; |
|||
queue.push(state); |
|||
++currentNewState; |
|||
} |
|||
} |
|||
|
|||
uint64_t newStateCount = ma->getNumberOfStates() - eliminationMapping.size(); |
|||
// Build the new MA
|
|||
storm::storage::SparseMatrix<ValueType> newTransitionMatrix; |
|||
storm::models::sparse::StateLabeling newStateLabeling( |
|||
newStateCount); |
|||
storm::storage::BitVector newMarkovianStates(ma->getNumberOfStates() - eliminationMapping.size(), |
|||
false); |
|||
std::vector<ValueType> newExitRates; |
|||
//TODO choice labeling
|
|||
boost::optional<storm::models::sparse::ChoiceLabeling> newChoiceLabeling; |
|||
|
|||
// Initialize the matrix builder and helper variables
|
|||
storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>( |
|||
0, 0, 0, false, true, 0); |
|||
uint_fast64_t currentRow = 0; |
|||
uint_fast64_t state = 0; |
|||
while (!queue.empty()) { |
|||
state = queue.front(); |
|||
queue.pop(); |
|||
|
|||
for (auto const &label : ma->getLabelsOfState(state)) { |
|||
if (!newStateLabeling.containsLabel(label)) { |
|||
newStateLabeling.addLabel(label); |
|||
} |
|||
|
|||
newStateLabeling.addLabelToState(label, stateRemapping[state]); |
|||
} |
|||
|
|||
// Use a set to not include redundant rows
|
|||
std::set<std::map<uint_fast64_t, ValueType>> rowSet; |
|||
for (uint_fast64_t row = 0; row < ma->getTransitionMatrix().getRowGroupSize(state); ++row) { |
|||
std::map<uint_fast64_t, ValueType> transitions; |
|||
for (typename storm::storage::SparseMatrix<ValueType>::const_iterator itEntry = ma->getTransitionMatrix().getRow( |
|||
state, row).begin(); |
|||
itEntry != ma->getTransitionMatrix().getRow(state, row).end(); ++itEntry) { |
|||
uint_fast64_t newId = stateRemapping[itEntry->getColumn()]; |
|||
if (transitions.count(newId) == 0) { |
|||
transitions[newId] = itEntry->getValue(); |
|||
} else { |
|||
transitions[newId] += itEntry->getValue(); |
|||
} |
|||
} |
|||
rowSet.insert(transitions); |
|||
} |
|||
|
|||
// correctly set rates
|
|||
auto rate = storm::utility::zero<ValueType>(); |
|||
|
|||
if (ma->isMarkovianState(state)) { |
|||
newMarkovianStates.set(stateRemapping[state], true); |
|||
rate = ma->getExitRates().at(state); |
|||
} |
|||
|
|||
newExitRates.push_back(rate); |
|||
// Build matrix
|
|||
matrixBuilder.newRowGroup(currentRow); |
|||
for (auto const &row : rowSet) { |
|||
for (auto const &transition : row) { |
|||
matrixBuilder.addNextValue(currentRow, transition.first, transition.second); |
|||
STORM_LOG_TRACE(stateRemapping[state] << "->" << transition.first << " : " << transition.second |
|||
<< std::endl); |
|||
} |
|||
++currentRow; |
|||
} |
|||
} |
|||
// explicitly force dimensions of the matrix in case a column is missing
|
|||
newTransitionMatrix = matrixBuilder.build(newStateCount, newStateCount, newStateCount); |
|||
|
|||
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> newComponents = storm::storage::sparse::ModelComponents<ValueType, RewardModelType>( |
|||
std::move(newTransitionMatrix), std::move(newStateLabeling)); |
|||
|
|||
newComponents.rateTransitions = false; |
|||
newComponents.markovianStates = std::move(newMarkovianStates); |
|||
newComponents.exitRates = std::move(newExitRates); |
|||
auto model = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType >>( |
|||
std::move(newComponents)); |
|||
if (model->isConvertibleToCtmc()) { |
|||
return model->convertToCtmc(); |
|||
} else { |
|||
return model; |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
bool NonMarkovianChainTransformer<ValueType, RewardModelType>::preservesFormula( |
|||
storm::logic::Formula const &formula) { |
|||
storm::logic::FragmentSpecification fragment = storm::logic::propositional(); |
|||
|
|||
fragment.setProbabilityOperatorsAllowed(true); |
|||
fragment.setGloballyFormulasAllowed(true); |
|||
fragment.setReachabilityProbabilityFormulasAllowed(true); |
|||
fragment.setUntilFormulasAllowed(true); |
|||
fragment.setTimeBoundedUntilFormulasAllowed(true); |
|||
|
|||
return formula.isInFragment(fragment); |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<std::shared_ptr<storm::logic::Formula const>> |
|||
NonMarkovianChainTransformer<ValueType, RewardModelType>::checkAndTransformFormulas( |
|||
std::vector<std::shared_ptr<storm::logic::Formula const>> const &formulas) { |
|||
std::vector<std::shared_ptr<storm::logic::Formula const>> result; |
|||
|
|||
for (auto const &f : formulas) { |
|||
if (preservesFormula(*f)) { |
|||
result.push_back(f); |
|||
} else { |
|||
STORM_LOG_INFO("Non-Markovian chain elimination does not preserve formula " << *f); |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
|
|||
template |
|||
class NonMarkovianChainTransformer<double>; |
|||
|
|||
template |
|||
class NonMarkovianChainTransformer<double, storm::models::sparse::StandardRewardModel<storm::Interval>>; |
|||
#ifdef STORM_HAVE_CARL
|
|||
|
|||
template |
|||
class NonMarkovianChainTransformer<storm::RationalFunction>; |
|||
|
|||
template |
|||
class NonMarkovianChainTransformer<storm::RationalNumber>; |
|||
|
|||
#endif
|
|||
} |
|||
} |
|||
|
|||
@ -0,0 +1,46 @@ |
|||
#include "storm/models/sparse/MarkovAutomaton.h" |
|||
#include "storm/logic/Formula.h" |
|||
|
|||
namespace storm { |
|||
namespace transformer { |
|||
/** |
|||
* Transformer for eliminating chains of non-Markovian states (instantaneous path fragment leading to the same outcome) from Markov Automata |
|||
*/ |
|||
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>> |
|||
class NonMarkovianChainTransformer { |
|||
public: |
|||
|
|||
/** |
|||
* Generates a model with the same basic behavior as the input, but eliminates non-Markovian chains. |
|||
* If no non-determinism occurs, a CTMC is generated. |
|||
* |
|||
* @param ma the input Markov Automaton |
|||
* @param preserveLabels if set, the procedure considers the labels of non-Markovian states when eliminating states |
|||
* @return a reference to the new Mmodel after eliminating non-Markovian states |
|||
*/ |
|||
static std::shared_ptr< |
|||
models::sparse::Model < ValueType, RewardModelType>> eliminateNonmarkovianStates(std::shared_ptr< |
|||
models::sparse::MarkovAutomaton < ValueType, RewardModelType>> ma, |
|||
bool preserveLabels = true |
|||
); |
|||
|
|||
/** |
|||
* Check if the property specified by the given formula is preserved by the transformation. |
|||
* |
|||
* @param formula the formula to check |
|||
* @return true, if the property is preserved |
|||
*/ |
|||
static bool preservesFormula(storm::logic::Formula const &formula); |
|||
|
|||
/** |
|||
* Checks for the given formulae if the specified properties are preserved and removes formulae of properties which are not preserved. |
|||
* |
|||
* @param formulas |
|||
* @return vector containing all fomulae which are valid for the transformed model |
|||
*/ |
|||
static std::vector<std::shared_ptr<storm::logic::Formula const>> |
|||
checkAndTransformFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> const &formulas); |
|||
}; |
|||
} |
|||
} |
|||
|
|||
@ -0,0 +1,69 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "storm-dft/api/storm-dft.h"
|
|||
#include "storm-dft/transformations/DftTransformator.h"
|
|||
|
|||
namespace { |
|||
|
|||
TEST(DftTransformatorTest, UniqueConstantFailedTest) { |
|||
std::string file = STORM_TEST_RESOURCES_DIR "/dft/const_be_test.dft"; |
|||
std::shared_ptr<storm::storage::DFT<double>> originalDft = storm::api::loadDFTGalileoFile<double>(file); |
|||
auto dftTransformator = storm::transformations::dft::DftTransformator<double>(); |
|||
std::shared_ptr<storm::storage::DFT<double>> transformedDft = dftTransformator.transformUniqueFailedBe( |
|||
*originalDft); |
|||
|
|||
auto bes = transformedDft->getBasicElements(); |
|||
uint64_t constBeFailedCount = 0; |
|||
uint64_t constBeFailsafeCount = 0; |
|||
for (auto &be : bes) { |
|||
if (be->type() == storm::storage::DFTElementType::BE_CONST) { |
|||
if (be->canFail()) { |
|||
++constBeFailedCount; |
|||
} else { |
|||
++constBeFailsafeCount; |
|||
} |
|||
} |
|||
} |
|||
|
|||
EXPECT_EQ(1ul, constBeFailedCount); |
|||
EXPECT_EQ(3ul, constBeFailsafeCount); |
|||
} |
|||
|
|||
TEST(DftTransformatorTest, BinaryFDEPTest) { |
|||
std::string file = STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft"; |
|||
std::shared_ptr<storm::storage::DFT<double>> originalDft = storm::api::loadDFTGalileoFile<double>(file); |
|||
auto dftTransformator = storm::transformations::dft::DftTransformator<double>(); |
|||
std::shared_ptr<storm::storage::DFT<double>> transformedDft = dftTransformator.transformBinaryFDEPs( |
|||
*originalDft); |
|||
|
|||
uint64_t dependencyCount = transformedDft->getDependencies().size(); |
|||
|
|||
EXPECT_EQ(2ul, dependencyCount); |
|||
} |
|||
|
|||
TEST(DftTransformatorTest, PDEPTransformTest) { |
|||
std::string file = STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft"; |
|||
std::shared_ptr<storm::storage::DFT<double>> originalDft = storm::api::loadDFTGalileoFile<double>(file); |
|||
auto dftTransformator = storm::transformations::dft::DftTransformator<double>(); |
|||
std::shared_ptr<storm::storage::DFT<double>> transformedDft = dftTransformator.transformBinaryFDEPs( |
|||
*originalDft); |
|||
|
|||
uint64_t fdepCount = 0; |
|||
uint64_t pdepCount = 0; |
|||
|
|||
for (auto depIndex : transformedDft->getDependencies()) { |
|||
auto dep = transformedDft->getDependency(depIndex); |
|||
if (dep->probability() == 1) { |
|||
++fdepCount; |
|||
} else { |
|||
++pdepCount; |
|||
} |
|||
} |
|||
|
|||
EXPECT_EQ(1ul, pdepCount); |
|||
EXPECT_EQ(2ul, fdepCount); |
|||
EXPECT_EQ(4ul, transformedDft->nrBasicElements()); |
|||
} |
|||
|
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue