Browse Source
Untangled creating of DFT successor state and refactored FailableElements
tempestpy_adaptions
Untangled creating of DFT successor state and refactored FailableElements
tempestpy_adaptions
Matthias Volk
4 years ago
No known key found for this signature in database
GPG Key ID: 83A57678F739FCD3
7 changed files with 518 additions and 233 deletions
-
5src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
-
124src/storm-dft/generator/DftNextStateGenerator.cpp
-
11src/storm-dft/generator/DftNextStateGenerator.h
-
29src/storm-dft/storage/dft/DFTState.cpp
-
178src/storm-dft/storage/dft/DFTState.h
-
163src/storm-dft/storage/dft/FailableElements.cpp
-
241src/storm-dft/storage/dft/FailableElements.h
@ -0,0 +1,163 @@ |
|||||
|
#include "storm-dft/storage/dft/FailableElements.h"
|
||||
|
|
||||
|
#include <sstream>
|
||||
|
|
||||
|
#include "storm-dft/storage/dft/DFT.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace dft { |
||||
|
namespace storage { |
||||
|
|
||||
|
FailableElements::const_iterator::const_iterator(bool dependency, bool conflicting, storm::storage::BitVector::const_iterator const& iterBE, std::list<size_t>::const_iterator const& iterDependency, std::list<size_t>::const_iterator nonConflictEnd, std::list<size_t>::const_iterator conflictBegin) |
||||
|
: dependency(dependency), conflicting(conflicting), itBE(iterBE), itDep(iterDependency), nonConflictEnd(nonConflictEnd), conflictBegin(conflictBegin) { |
||||
|
STORM_LOG_ASSERT(conflicting || itDep != nonConflictEnd, "No non-conflicting dependencies present."); |
||||
|
} |
||||
|
|
||||
|
FailableElements::const_iterator& FailableElements::const_iterator::operator++() { |
||||
|
if (dependency) { |
||||
|
++itDep; |
||||
|
if (!conflicting && itDep == nonConflictEnd) { |
||||
|
// All non-conflicting dependencies considered -> start with conflicting ones
|
||||
|
conflicting = true; |
||||
|
itDep = conflictBegin; |
||||
|
} |
||||
|
} else { |
||||
|
++itBE; |
||||
|
} |
||||
|
return *this; |
||||
|
} |
||||
|
|
||||
|
uint_fast64_t FailableElements::const_iterator::operator*() const { |
||||
|
if (dependency) { |
||||
|
return *itDep; |
||||
|
} else { |
||||
|
return *itBE; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
bool FailableElements::const_iterator::operator!=(const_iterator const& other) const { |
||||
|
if (dependency != other.dependency || conflicting != other.conflicting) { |
||||
|
return true; |
||||
|
} |
||||
|
if (dependency) { |
||||
|
return itDep != other.itDep; |
||||
|
} else { |
||||
|
return itBE != other.itBE; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
bool FailableElements::const_iterator::operator==(const_iterator const& other) const { |
||||
|
if (dependency != other.dependency || conflicting != other.conflicting) { |
||||
|
return false; |
||||
|
} |
||||
|
if (dependency) { |
||||
|
return itDep == other.itDep; |
||||
|
} else { |
||||
|
return itBE == other.itBE; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
bool FailableElements::const_iterator::isFailureDueToDependency() const { |
||||
|
return dependency; |
||||
|
} |
||||
|
|
||||
|
bool FailableElements::const_iterator::isConflictingDependency() const { |
||||
|
return conflicting; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, std::shared_ptr<storm::storage::DFTDependency<ValueType> const>> FailableElements::const_iterator::getFailBE(storm::storage::DFT<ValueType> const& dft) const { |
||||
|
size_t nextFailId = **this; |
||||
|
if (isFailureDueToDependency()) { |
||||
|
// Consider failure due to dependency
|
||||
|
std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency = dft.getDependency(nextFailId); |
||||
|
STORM_LOG_ASSERT(dependency->dependentEvents().size() == 1, "More than one dependent event"); |
||||
|
return std::make_pair(dft.getBasicElement(dependency->dependentEvents()[0]->id()), dependency); |
||||
|
} else { |
||||
|
// Consider "normal" failure
|
||||
|
return std::make_pair(dft.getBasicElement(nextFailId), nullptr); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
void FailableElements::addBE(size_t id) { |
||||
|
currentlyFailableBE.set(id); |
||||
|
} |
||||
|
|
||||
|
void FailableElements::addDependency(size_t id, bool isConflicting) { |
||||
|
std::list<size_t>& failableList = (isConflicting ? failableConflictingDependencies : failableNonconflictingDependencies); |
||||
|
for (auto it = failableList.begin(); it != failableList.end(); ++it) { |
||||
|
if (*it > id) { |
||||
|
failableList.insert(it, id); |
||||
|
return; |
||||
|
} else if (*it == id) { |
||||
|
// Dependency already contained
|
||||
|
return; |
||||
|
} |
||||
|
} |
||||
|
failableList.push_back(id); |
||||
|
} |
||||
|
|
||||
|
void FailableElements::removeBE(size_t id) { |
||||
|
currentlyFailableBE.set(id, false); |
||||
|
} |
||||
|
|
||||
|
void FailableElements::removeDependency(size_t id) { |
||||
|
auto iter = std::find(failableConflictingDependencies.begin(), failableConflictingDependencies.end(), id); |
||||
|
if (iter != failableConflictingDependencies.end()) { |
||||
|
failableConflictingDependencies.erase(iter); |
||||
|
return; |
||||
|
} |
||||
|
iter = std::find(failableNonconflictingDependencies.begin(), failableNonconflictingDependencies.end(), id); |
||||
|
if (iter != failableNonconflictingDependencies.end()) { |
||||
|
failableNonconflictingDependencies.erase(iter); |
||||
|
return; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
void FailableElements::clear() { |
||||
|
currentlyFailableBE.clear(); |
||||
|
failableConflictingDependencies.clear(); |
||||
|
failableNonconflictingDependencies.clear(); |
||||
|
} |
||||
|
|
||||
|
FailableElements::const_iterator FailableElements::begin(bool forceBE) const { |
||||
|
bool dependency = hasDependencies() && !forceBE; |
||||
|
bool conflicting = failableNonconflictingDependencies.empty(); |
||||
|
auto itDep = conflicting ? failableConflictingDependencies.begin() : failableNonconflictingDependencies.begin(); |
||||
|
return FailableElements::const_iterator(dependency, conflicting, currentlyFailableBE.begin(), itDep, failableNonconflictingDependencies.end(), failableConflictingDependencies.begin()); |
||||
|
} |
||||
|
|
||||
|
FailableElements::const_iterator FailableElements::end(bool forceBE) const { |
||||
|
bool dependency = hasDependencies() && !forceBE; |
||||
|
return FailableElements::const_iterator(dependency, true, currentlyFailableBE.end(), failableConflictingDependencies.end(), failableNonconflictingDependencies.end(), failableConflictingDependencies.begin()); |
||||
|
} |
||||
|
|
||||
|
bool FailableElements::hasDependencies() const { |
||||
|
return !failableConflictingDependencies.empty() || !failableNonconflictingDependencies.empty(); |
||||
|
} |
||||
|
|
||||
|
bool FailableElements::hasBEs() const { |
||||
|
return !currentlyFailableBE.empty(); |
||||
|
} |
||||
|
|
||||
|
std::string FailableElements::getCurrentlyFailableString() const { |
||||
|
std::stringstream stream; |
||||
|
stream << "{"; |
||||
|
if (hasDependencies()) { |
||||
|
stream << "Dependencies: "; |
||||
|
} |
||||
|
for (auto it = begin(); it != end(); ++it) { |
||||
|
stream << *it << ", "; |
||||
|
} |
||||
|
stream << "}"; |
||||
|
return stream.str(); |
||||
|
} |
||||
|
|
||||
|
// Explicit instantiations.
|
||||
|
template std::pair<std::shared_ptr<storm::storage::DFTBE<double> const>, std::shared_ptr<storm::storage::DFTDependency<double> const>> FailableElements::const_iterator::getFailBE(storm::storage::DFT<double> const& dft) const; |
||||
|
|
||||
|
template std::pair<std::shared_ptr<storm::storage::DFTBE<storm::RationalFunction> const>, std::shared_ptr<storm::storage::DFTDependency<storm::RationalFunction> const>> FailableElements::const_iterator::getFailBE(storm::storage::DFT<storm::RationalFunction> const& dft) const; |
||||
|
|
||||
|
} // namespace storage
|
||||
|
} // namespace dft
|
||||
|
} // namespace storm
|
||||
@ -0,0 +1,241 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include <list> |
||||
|
#include <memory> |
||||
|
|
||||
|
#include "storm/storage/BitVector.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace storage { |
||||
|
// Forward declarations |
||||
|
template<typename ValueType> |
||||
|
class DFT; |
||||
|
template<typename ValueType> |
||||
|
class DFTBE; |
||||
|
template<typename ValueType> |
||||
|
class DFTDependency; |
||||
|
} |
||||
|
|
||||
|
namespace dft { |
||||
|
namespace storage { |
||||
|
|
||||
|
/*! |
||||
|
* Handling of currently failable elements (BEs) either due to their own failure or because of dependencies. |
||||
|
* |
||||
|
* We distinguish between failures of BEs and failures of dependencies. |
||||
|
* For dependencies, we further distinguish between non-conflicting and conflicting dependencies. |
||||
|
* Non-conflicting dependencies will lead to spurious non-determinsm. |
||||
|
* |
||||
|
* The class supports iterators for all failable elements (either BE or dependencies). |
||||
|
* |
||||
|
*/ |
||||
|
class FailableElements { |
||||
|
|
||||
|
public: |
||||
|
/*! |
||||
|
* Iterator for failable elements. |
||||
|
* |
||||
|
*/ |
||||
|
class const_iterator : public std::iterator<std::input_iterator_tag, size_t> { |
||||
|
|
||||
|
public: |
||||
|
/*! |
||||
|
* Construct a new iterator. |
||||
|
* We either iterate over all failable BEs or over all dependencies (if dependency is true). |
||||
|
* For dependencies, we start with non-conflicting dependencies before iterating over conflicting ones. |
||||
|
* For dependencies, we start with non-conflicting dependencies if they are present. |
||||
|
* |
||||
|
* @param dependency Whether dependencies should be iterated (or BEs if false). |
||||
|
* @param conflicting Whether conflicting dependencies should be iterated (or non-conflicting if false). |
||||
|
* @param iterBE Iterator for BEs. |
||||
|
* @param iterDependency Iterator for Dependencies. |
||||
|
* @param nonConflictEnd Iterator to end of non-conflicting dependencies. |
||||
|
* @param conflictBegin Iterator to begin of conflicting dependencies. |
||||
|
*/ |
||||
|
const_iterator(bool dependency, bool conflicting, storm::storage::BitVector::const_iterator const& iterBE, std::list<size_t>::const_iterator const& iterDependency, std::list<size_t>::const_iterator nonConflictEnd, std::list<size_t>::const_iterator conflictBegin); |
||||
|
|
||||
|
/*! |
||||
|
* Constructs an iterator by copying the given iterator. |
||||
|
* |
||||
|
* @param other The iterator to copy. |
||||
|
*/ |
||||
|
const_iterator(const_iterator const& other) = default; |
||||
|
|
||||
|
/*! |
||||
|
* Assigns the contents of the given iterator to the current one via copying the former's contents. |
||||
|
* |
||||
|
* @param other The iterator from which to copy-assign. |
||||
|
*/ |
||||
|
const_iterator& operator=(const_iterator const& other) = default; |
||||
|
|
||||
|
/*! |
||||
|
* Increment the iterator. |
||||
|
* |
||||
|
* @return A reference to this iterator. |
||||
|
*/ |
||||
|
const_iterator& operator++(); |
||||
|
|
||||
|
/*! |
||||
|
* Returns the id of the current failable element. |
||||
|
* |
||||
|
* @return Element id. |
||||
|
*/ |
||||
|
uint_fast64_t operator*() const; |
||||
|
|
||||
|
/*! |
||||
|
* Compares the iterator with another iterator for inequality. |
||||
|
* |
||||
|
* @param other The iterator with respect to which inequality is checked. |
||||
|
* @return True if the two iterators are unequal. |
||||
|
*/ |
||||
|
bool operator!=(const_iterator const& other) const; |
||||
|
|
||||
|
/*! |
||||
|
* Compares the iterator with another iterator for equality. |
||||
|
* |
||||
|
* @param other The iterator with respect to which equality is checked. |
||||
|
* @return True if the two iterators are equal. |
||||
|
*/ |
||||
|
bool operator==(const_iterator const& other) const; |
||||
|
|
||||
|
/*! |
||||
|
* Return whether the current failure is due to a dependency (or the BE itself). |
||||
|
* |
||||
|
* @return true iff current failure is due to dependency. |
||||
|
*/ |
||||
|
bool isFailureDueToDependency() const; |
||||
|
|
||||
|
/*! |
||||
|
* Return whether the current dependency failure is conflicting. |
||||
|
* |
||||
|
* @return true iff current dependency failure is conflicting. |
||||
|
*/ |
||||
|
bool isConflictingDependency() const; |
||||
|
|
||||
|
/*! |
||||
|
* Obtain the BE which fails from the current iterator. |
||||
|
* Optionally returns the dependency which triggered the BE failure. |
||||
|
* |
||||
|
* @tparam ValueType Value type. |
||||
|
* @param dft DFT. |
||||
|
* @return Pair of the BE which fails and the dependency which triggered the failure (or nullptr if the BE fails on its own). |
||||
|
*/ |
||||
|
template<typename ValueType> |
||||
|
std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, std::shared_ptr<storm::storage::DFTDependency<ValueType> const>> getFailBE(storm::storage::DFT<ValueType> const& dft) const; |
||||
|
|
||||
|
private: |
||||
|
// Whether dependencies are currently considered. |
||||
|
bool dependency; |
||||
|
// Whether the iterator currently points to a conflicting dependency. |
||||
|
bool conflicting; |
||||
|
// Iterators for underlying data structures |
||||
|
storm::storage::BitVector::const_iterator itBE; |
||||
|
std::list<size_t>::const_iterator itDep; |
||||
|
|
||||
|
// Pointers marking end of non-conflict list and beginning of conflict list |
||||
|
// Used for sequential iteration over all dependencies |
||||
|
std::list<size_t>::const_iterator nonConflictEnd; |
||||
|
std::list<size_t>::const_iterator conflictBegin; |
||||
|
}; |
||||
|
|
||||
|
/*! |
||||
|
* Creator. |
||||
|
* |
||||
|
* @param maxBEId Maximal id of a BE. |
||||
|
*/ |
||||
|
FailableElements(size_t maxBEId) : currentlyFailableBE(maxBEId) { |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Add failable BE. |
||||
|
* Note that this invalidates the iterator. |
||||
|
* |
||||
|
* @param id Id of BE. |
||||
|
*/ |
||||
|
void addBE(size_t id); |
||||
|
|
||||
|
/*! |
||||
|
* Add failable dependency. |
||||
|
* Note that this invalidates the iterator. |
||||
|
* |
||||
|
* @param id Id of dependency. |
||||
|
* @param isConflicting Whether the dependency is in conflict to other dependencies. In this case |
||||
|
* the conflict needs to be resolved non-deterministically. |
||||
|
*/ |
||||
|
void addDependency(size_t id, bool isConflicting); |
||||
|
|
||||
|
/*! |
||||
|
* Remove BE from list of failable elements. |
||||
|
* Note that this invalidates the iterator. |
||||
|
* |
||||
|
* @param id Id of BE. |
||||
|
*/ |
||||
|
void removeBE(size_t id); |
||||
|
|
||||
|
/*! |
||||
|
* Remove dependency from list of failable elements. |
||||
|
* Note that this invalidates the iterator. |
||||
|
* |
||||
|
* @param id Id of dependency. |
||||
|
*/ |
||||
|
void removeDependency(size_t id); |
||||
|
|
||||
|
/*! |
||||
|
* Clear list of currently failable elements. |
||||
|
* Note that this invalidates the iterator. |
||||
|
*/ |
||||
|
void clear(); |
||||
|
|
||||
|
/*! |
||||
|
* Iterator to first failable element. |
||||
|
* If dependencies are present, the iterator is for dependencies. Otherwise it is for BEs. |
||||
|
* For dependencies, the iterator considers non-conflicting dependencies first. |
||||
|
* |
||||
|
* @param forceBE If true, failable dependencies are ignored and only BEs are considered. |
||||
|
* @return Iterator. |
||||
|
*/ |
||||
|
FailableElements::const_iterator begin(bool forceBE = false) const; |
||||
|
|
||||
|
/*! |
||||
|
* Iterator after last failable element. |
||||
|
* |
||||
|
* @param forceBE If true, failable dependencies are ignored and only BEs are considered. |
||||
|
* @return Iterator. |
||||
|
*/ |
||||
|
FailableElements::const_iterator end(bool forceBE = false) const; |
||||
|
|
||||
|
/*! |
||||
|
* Whether failable dependencies are present. |
||||
|
* |
||||
|
* @return true iff dependencies can fail. |
||||
|
*/ |
||||
|
bool hasDependencies() const; |
||||
|
|
||||
|
/*! |
||||
|
* Whether failable BEs are present. |
||||
|
* |
||||
|
* @return true iff BEs can fail. |
||||
|
*/ |
||||
|
bool hasBEs() const; |
||||
|
|
||||
|
/*! |
||||
|
* Get a string representation of the currently failable elements. |
||||
|
* |
||||
|
* @return std::string Enumeration of currently failable elements. |
||||
|
*/ |
||||
|
std::string getCurrentlyFailableString() const; |
||||
|
|
||||
|
private: |
||||
|
|
||||
|
// We use a BitVector for BEs but a list for dependencies, because usually only a few dependencies are failable at the same time. |
||||
|
// In contrast, usually most BEs are failable. |
||||
|
// The lists of failable elements are sorted by increasing id. |
||||
|
storm::storage::BitVector currentlyFailableBE; |
||||
|
std::list<size_t> failableConflictingDependencies; |
||||
|
std::list<size_t> failableNonconflictingDependencies; |
||||
|
|
||||
|
}; |
||||
|
|
||||
|
} // namespace storage |
||||
|
} // namespace dft |
||||
|
} // namespace storm |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue