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

Finished templating 

Former-commit-id: 7225717fdb
tempestpy_adaptions
Mavo 9 years ago
parent
7a0207637a
commit
6e2f5602e1
13 changed files with 453 additions and 357 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. 22
      src/builder/ExplicitDFTModelBuilder.cpp
  2. 7
      src/builder/ExplicitDFTModelBuilder.h
  3. 10
      src/storage/dft/DFT.cpp
  4. 42
      src/storage/dft/DFT.h
  5. 35
      src/storage/dft/DFTBuilder.cpp
  6. 20
      src/storage/dft/DFTBuilder.h
  7. 33
      src/storage/dft/DFTElements.cpp
  8. 438
      src/storage/dft/DFTElements.h
  9. 96
      src/storage/dft/DFTState.cpp
  10. 17
      src/storage/dft/DFTState.h
  11. 49
      src/storage/dft/DFTStateSpaceGenerationQueues.h
  12. 25
      src/storage/dft/OrderDFTElementsById.cpp
  13. 16
      src/storage/dft/OrderDFTElementsById.h

22
src/builder/ExplicitDFTModelBuilder.cpp
View File

@ -13,10 +13,10 @@ namespace storm {
template<typename ValueType, typename RewardModelType, typename IndexType>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::buildCTMC() {
// Initialize
storm::storage::DFTState state(mDft, newIndex++);
storm::storage::DFTState<ValueType> state(mDft, newIndex++);
mStates.insert(state);
std::queue<storm::storage::DFTState> stateQueue;
std::queue<storm::storage::DFTState<ValueType>> stateQueue;
stateQueue.push(state);
bool deterministicModel = true;
@ -46,7 +46,7 @@ namespace storm {
modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
}
for (storm::storage::DFTState state : mStates) {
for (storm::storage::DFTState<ValueType> state : mStates) {
if (mDft.hasFailed(state)) {
modelComponents.stateLabeling.addLabelToState("failed", state.getId());
}
@ -72,7 +72,7 @@ namespace storm {
}
template<typename ValueType, typename RewardModelType, typename IndexType>
void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::exploreStates(std::queue<storm::storage::DFTState>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder) {
void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::exploreStates(std::queue<storm::storage::DFTState<ValueType>>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder) {
std::vector<std::pair<size_t, ValueType>> outgoingTransitions;
@ -82,7 +82,7 @@ namespace storm {
ValueType sum = 0;
// Consider next state
storm::storage::DFTState state = stateQueue.front();
storm::storage::DFTState<ValueType> state = stateQueue.front();
stateQueue.pop();
size_t smallest = 0;
@ -99,7 +99,7 @@ namespace storm {
while (smallest < state.nrFailableBEs()) {
STORM_LOG_TRACE("exploring from: " << mDft.getStateString(state));
storm::storage::DFTState newState(state);
storm::storage::DFTState<ValueType> newState(state);
std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType>>, bool> nextBE = newState.letNextBEFail(smallest++);
if (nextBE.first == nullptr) {
std::cout << "break" << std::endl;
@ -108,26 +108,26 @@ namespace storm {
}
STORM_LOG_TRACE("with the failure of: " << nextBE.first->name() << " [" << nextBE.first->id() << "]");
storm::storage::DFTStateSpaceGenerationQueues queues;
storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;
for (std::shared_ptr<storm::storage::DFTGate> parent : nextBE.first->parents()) {
for (DFTGatePointer parent : nextBE.first->parents()) {
if (newState.isOperational(parent->id())) {
queues.propagateFailure(parent);
}
}
while (!queues.failurePropagationDone()) {
std::shared_ptr<storm::storage::DFTGate> next = queues.nextFailurePropagation();
DFTGatePointer next = queues.nextFailurePropagation();
next->checkFails(newState, queues);
}
while (!queues.failsafePropagationDone()) {
std::shared_ptr<storm::storage::DFTGate> next = queues.nextFailsafePropagation();
DFTGatePointer next = queues.nextFailsafePropagation();
next->checkFailsafe(newState, queues);
}
while (!queues.dontCarePropagationDone()) {
std::shared_ptr<storm::storage::DFTElement> next = queues.nextDontCarePropagation();
DFTElementPointer next = queues.nextDontCarePropagation();
next->checkDontCareAnymore(newState, queues);
}

7
src/builder/ExplicitDFTModelBuilder.h
View File

@ -18,6 +18,9 @@ namespace storm {
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename IndexType = uint32_t>
class ExplicitDFTModelBuilder {
using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
using DFTGatePointer = std::shared_ptr<storm::storage::DFTGate<ValueType>>;
// A structure holding the individual components of a model.
struct ModelComponents {
ModelComponents();
@ -36,7 +39,7 @@ namespace storm {
};
storm::storage::DFT<ValueType> const &mDft;
std::unordered_set<storm::storage::DFTState> mStates;
std::unordered_set<storm::storage::DFTState<ValueType>> mStates;
size_t newIndex = 0;
public:
@ -47,7 +50,7 @@ namespace storm {
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildCTMC();
private:
void exploreStates(std::queue<storm::storage::DFTState>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);
void exploreStates(std::queue<storm::storage::DFTState<ValueType>>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);
};
}

10
src/storage/dft/DFT.cpp
View File

@ -4,7 +4,7 @@ namespace storm {
namespace storage {
template<typename ValueType>
DFT<ValueType>::DFT(std::vector<std::shared_ptr<DFTElement>> const& elements, std::shared_ptr<DFTElement> const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0)
DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0)
{
assert(elementIndicesCorrect());
@ -19,7 +19,7 @@ namespace storm {
}
else if(elem->isSpareGate()) {
++mNrOfSpares;
for(auto const& spareReprs : std::static_pointer_cast<DFTSpare>(elem)->children()) {
for(auto const& spareReprs : std::static_pointer_cast<DFTSpare<ValueType>>(elem)->children()) {
if(mActivationIndex.count(spareReprs->id()) == 0) {
mActivationIndex[spareReprs->id()] = stateIndex++;
}
@ -34,7 +34,7 @@ namespace storm {
mSpareModules.insert(std::make_pair(spareReprs->id(), sparesAndBes));
}
std::static_pointer_cast<DFTSpare>(elem)->setUseIndex(stateIndex);
std::static_pointer_cast<DFTSpare<ValueType>>(elem)->setUseIndex(stateIndex);
mUsageIndex.insert(std::make_pair(elem->id(), stateIndex));
stateIndex += mUsageInfoBits;
@ -108,7 +108,7 @@ namespace storm {
}
template<typename ValueType>
std::string DFT<ValueType>::getElementsWithStateString(DFTState const& state) const{
std::string DFT<ValueType>::getElementsWithStateString(DFTState<ValueType> const& state) const{
std::stringstream stream;
for (auto const& elem : mElements) {
stream << "[" << elem->id() << "]";
@ -126,7 +126,7 @@ namespace storm {
}
template<typename ValueType>
std::string DFT<ValueType>::getStateString(DFTState const& state) const{
std::string DFT<ValueType>::getStateString(DFTState<ValueType> const& state) const{
std::stringstream stream;
stream << "(" << state.getId() << ") ";
for (auto const& elem : mElements) {

42
src/storage/dft/DFT.h
View File

@ -17,8 +17,9 @@
namespace storm {
namespace storage {
template<typename ValueType>
struct DFTElementSort {
bool operator()(std::shared_ptr<DFTElement> const& a, std::shared_ptr<DFTElement> const& b) const {
bool operator()(std::shared_ptr<DFTElement<ValueType>> const& a, std::shared_ptr<DFTElement<ValueType>> const& b) const {
if (a->rank() == 0 && b->rank() == 0) {
return a->isConstant();
} else {
@ -27,11 +28,18 @@ namespace storm {
}
};
template<typename ValueType>
class DFT {
using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
using DFTElementVector = std::vector<DFTElementPointer>;
using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
using DFTGateVector = std::vector<DFTGatePointer>;
private:
std::vector<std::shared_ptr<DFTElement>> mElements;
DFTElementVector mElements;
size_t mNrOfBEs;
size_t mNrOfSpares;
size_t mTopLevelIndex;
@ -44,9 +52,8 @@ namespace storm {
std::map<size_t, size_t> mUsageIndex;
public:
DFT(std::vector<std::shared_ptr<DFTElement>> const& elements, std::shared_ptr<DFTElement> const& tle);
DFT(DFTElementVector const& elements, DFTElementPointer const& tle);
size_t stateSize() const {
return mStateSize;
}
@ -72,15 +79,15 @@ namespace storm {
return mIdToFailureIndex[id];
}
void initializeUses(DFTState& state) const {
void initializeUses(DFTState<ValueType>& state) const {
for(auto const& elem : mElements) {
if(elem->isSpareGate()) {
std::static_pointer_cast<DFTSpare>(elem)->initializeUses(state);
std::static_pointer_cast<DFTSpare<ValueType>>(elem)->initializeUses(state);
}
}
}
void initializeActivation(DFTState& state) const {
void initializeActivation(DFTState<ValueType>& state) const {
state.activate(mTopLevelIndex);
for(auto const& elem : mTopModule) {
if(mElements[elem]->isSpareGate()) {
@ -108,8 +115,7 @@ namespace storm {
}
}
void propagateActivation(DFTState& state, size_t representativeId) const {
void propagateActivation(DFTState<ValueType>& state, size_t representativeId) const {
state.activate(representativeId);
for(size_t id : module(representativeId)) {
if(mElements[id]->isSpareGate()) {
@ -120,15 +126,15 @@ namespace storm {
std::vector<size_t> nonColdBEs() const {
std::vector<size_t> result;
for(std::shared_ptr<DFTElement> elem : mElements) {
for(DFTElementPointer elem : mElements) {
if(elem->isBasicElement() && !elem->isColdBasicElement()) {
result.push_back(elem->id());
}
}
return result;
}
std::shared_ptr<DFTElement> const& getElement(size_t index) const {
DFTElementPointer const& getElement(size_t index) const {
assert(index < nrElements());
return mElements[index];
}
@ -140,7 +146,7 @@ namespace storm {
std::vector<std::shared_ptr<DFTBE<ValueType>>> getBasicElements() const {
std::vector<std::shared_ptr<DFTBE<ValueType>>> elements;
for (std::shared_ptr<storm::storage::DFTElement> elem : mElements) {
for (DFTElementPointer elem : mElements) {
if (elem->isBasicElement()) {
elements.push_back(std::static_pointer_cast<DFTBE<ValueType>>(elem));
}
@ -149,11 +155,11 @@ namespace storm {
}
bool hasFailed(DFTState const& state) const {
bool hasFailed(DFTState<ValueType> const& state) const {
return state.hasFailed(mTopLevelIndex);
}
bool isFailsafe(DFTState const& state) const {
bool isFailsafe(DFTState<ValueType> const& state) const {
return state.isFailsafe(mTopLevelIndex);
}
@ -163,9 +169,9 @@ namespace storm {
std::string getSpareModulesString() const;
std::string getElementsWithStateString(DFTState const& state) const;
std::string getElementsWithStateString(DFTState<ValueType> const& state) const;
std::string getStateString(DFTState const& state) const;
std::string getStateString(DFTState<ValueType> const& state) const;
private:
bool elementIndicesCorrect() const {

35
src/storage/dft/DFTBuilder.cpp
View File

@ -17,7 +17,7 @@ namespace storm {
DFT<ValueType> DFTBuilder<ValueType>::build() {
for(auto& elem : mChildNames) {
for(auto const& child : elem.second) {
std::shared_ptr<DFTGate> gate = std::static_pointer_cast<DFTGate>(elem.first);
DFTGatePointer gate = std::static_pointer_cast<DFTGate<ValueType>>(elem.first);
gate->pushBackChild(mElements[child]);
mElements[child]->addParent(gate);
}
@ -30,25 +30,25 @@ namespace storm {
computeRank(elem.second);
}
std::vector<std::shared_ptr<DFTElement>> elems = topoSort();
DFTElementVector elems = topoSort();
size_t id = 0;
for(std::shared_ptr<DFTElement> e : elems) {
for(DFTElementPointer e : elems) {
e->setId(id++);
}
return DFT<ValueType>(elems, mElements[topLevelIdentifier]);
}
template<typename ValueType>
unsigned DFTBuilder<ValueType>::computeRank(std::shared_ptr<DFTElement> const& elem) {
unsigned DFTBuilder<ValueType>::computeRank(DFTElementPointer const& elem) {
if(elem->rank() == -1) {
if(elem->nrChildren() == 0) {
elem->setRank(0);
} else {
std::shared_ptr<DFTGate> gate = std::static_pointer_cast<DFTGate>(elem);
DFTGatePointer gate = std::static_pointer_cast<DFTGate<ValueType>>(elem);
unsigned maxrnk = 0;
unsigned newrnk = 0;
for (std::shared_ptr<DFTElement> const &child : gate->children()) {
for (DFTElementPointer const &child : gate->children()) {
newrnk = computeRank(child);
if (newrnk > maxrnk) {
maxrnk = newrnk;
@ -68,22 +68,22 @@ namespace storm {
// Element with that name already exists.
return false;
}
std::shared_ptr<DFTElement> element;
DFTElementPointer element;
switch(tp) {
case DFTElementTypes::AND:
element = std::make_shared<DFTAnd>(mNextId++, name);
element = std::make_shared<DFTAnd<ValueType>>(mNextId++, name);
break;
case DFTElementTypes::OR:
element = std::make_shared<DFTOr>(mNextId++, name);
element = std::make_shared<DFTOr<ValueType>>(mNextId++, name);
break;
case DFTElementTypes::PAND:
element = std::make_shared<DFTPand>(mNextId++, name);
element = std::make_shared<DFTPand<ValueType>>(mNextId++, name);
break;
case DFTElementTypes::POR:
element = std::make_shared<DFTPor>(mNextId++, name);
element = std::make_shared<DFTPor<ValueType>>(mNextId++, name);
break;
case DFTElementTypes::SPARE:
element = std::make_shared<DFTSpare>(mNextId++, name);
element = std::make_shared<DFTSpare<ValueType>>(mNextId++, name);
break;
case DFTElementTypes::BE:
case DFTElementTypes::VOT:
@ -102,13 +102,13 @@ namespace storm {
}
template<typename ValueType>
void DFTBuilder<ValueType>::topoVisit(std::shared_ptr<DFTElement> const& n, std::map<std::shared_ptr<DFTElement>, topoSortColour>& visited, std::vector<std::shared_ptr<DFTElement>>& L) {
void DFTBuilder<ValueType>::topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour>& visited, DFTElementVector& L) {
if(visited[n] == topoSortColour::GREY) {
throw storm::exceptions::WrongFormatException("DFT is cyclic");
} else if(visited[n] == topoSortColour::WHITE) {
if(n->isGate()) {
visited[n] = topoSortColour::GREY;
for(std::shared_ptr<DFTElement> const& c : std::static_pointer_cast<DFTGate>(n)->children()) {
for(DFTElementPointer const& c : std::static_pointer_cast<DFTGate<ValueType>>(n)->children()) {
topoVisit(c, visited, L);
}
}
@ -117,14 +117,15 @@ namespace storm {
}
}
// TODO Matthias: use typedefs
template<typename ValueType>
std::vector<std::shared_ptr<DFTElement>> DFTBuilder<ValueType>::topoSort() {
std::map<std::shared_ptr<DFTElement>, topoSortColour> visited;
std::vector<std::shared_ptr<DFTElement<ValueType>>> DFTBuilder<ValueType>::topoSort() {
std::map<std::shared_ptr<DFTElement<ValueType>>, topoSortColour> visited;
for(auto const& e : mElements) {
visited.insert(std::make_pair(e.second, topoSortColour::WHITE));
}
std::vector<std::shared_ptr<DFTElement>> L;
std::vector<std::shared_ptr<DFTElement<ValueType>>> L;
for(auto const& e : visited) {
topoVisit(e.first, visited, L);
}

20
src/storage/dft/DFTBuilder.h
View File

@ -14,11 +14,17 @@ namespace storm {
template<typename ValueType>
class DFTBuilder {
using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
using DFTElementVector = std::vector<DFTElementPointer>;
using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
using DFTGateVector = std::vector<DFTGatePointer>;
private:
std::size_t mNextId = 0;
std::string topLevelIdentifier;
std::unordered_map<std::string, std::shared_ptr<DFTElement>> mElements;
std::unordered_map<std::shared_ptr<DFTElement>, std::vector<std::string>> mChildNames;
std::unordered_map<std::string, DFTElementPointer> mElements;
std::unordered_map<DFTElementPointer, std::vector<std::string>> mChildNames;
public:
DFTBuilder() {
@ -64,7 +70,7 @@ namespace storm {
std::cerr << "Voting gates with threshold higher than the number of children is not supported." << std::endl;
return false;
}
std::shared_ptr<DFTElement> element = std::make_shared<DFTVot>(mNextId++, name, threshold);
DFTElementPointer element = std::make_shared<DFTVot<ValueType>>(mNextId++, name, threshold);
mElements[name] = element;
mChildNames[element] = children;
@ -96,15 +102,15 @@ namespace storm {
private:
unsigned computeRank(std::shared_ptr<DFTElement> const& elem);
unsigned computeRank(DFTElementPointer const& elem);
bool addStandardGate(std::string const& name, std::vector<std::string> const& children, DFTElementTypes tp);
enum class topoSortColour {WHITE, BLACK, GREY};
void topoVisit(std::shared_ptr<DFTElement> const& n, std::map<std::shared_ptr<DFTElement>, topoSortColour>& visited, std::vector<std::shared_ptr<DFTElement>>& L);
void topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour>& visited, DFTElementVector& L);
std::vector<std::shared_ptr<DFTElement>> topoSort();
DFTElementVector topoSort();
};
}

33
src/storage/dft/DFTElements.cpp
View File

@ -1,11 +1,15 @@
#include <src/exceptions/NotImplementedException.h>
#include <src/utility/macros.h>
#include "DFTElements.h"
namespace storm {
namespace storage {
bool DFTElement::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
template<typename ValueType>
bool DFTElement<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
if(!state.dontCare(mId))
{
for(std::shared_ptr<DFTGate> const& parent : mParents) {
for(DFTGatePointer const& parent : mParents) {
if(state.isOperational(parent->id())) {
return false;
}
@ -16,8 +20,9 @@ namespace storm {
}
return false;
}
void DFTElement::extendSpareModule(std::set<size_t>& elementsInModule) const {
template<typename ValueType>
void DFTElement<ValueType>::extendSpareModule(std::set<size_t>& elementsInModule) const {
for(auto const& parent : mParents) {
if(elementsInModule.count(parent->id()) == 0 && !parent->isSpareGate()) {
elementsInModule.insert(parent->id());
@ -25,8 +30,9 @@ namespace storm {
}
}
}
void DFTElement::extendUnit(std::set<size_t>& unit) const {
template<typename ValueType>
void DFTElement<ValueType>::extendUnit(std::set<size_t>& unit) const {
unit.insert(mId);
for(auto const& parent : mParents) {
if(unit.count(parent->id()) != 0) {
@ -34,20 +40,23 @@ namespace storm {
}
}
}
void DFTElement::checkForSymmetricChildren() const {
template<typename ValueType>
void DFTElement<ValueType>::checkForSymmetricChildren() const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not implemented.");
assert(false);
}
template<typename ValueType>
bool DFTBE<ValueType>::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
if(DFTElement::checkDontCareAnymore(state, queues)) {
state.beNoLongerFailable(mId);
bool DFTBE<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
if(DFTElement<ValueType>::checkDontCareAnymore(state, queues)) {
state.beNoLongerFailable(this->mId);
return true;
}
return false;
}
// Explicitly instantiate the class.
template class DFTBE<double>;

438
src/storage/dft/DFTElements.h
View File

@ -16,21 +16,28 @@ using std::size_t;
namespace storm {
namespace storage {
template<typename ValueType>
class DFTGate;
template<typename ValueType>
class DFTElement {
using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
using DFTGateVector = std::vector<DFTGatePointer>;
protected:
size_t mId;
std::string mName;
size_t mRank = -1;
std::vector<std::shared_ptr<DFTGate>> mParents;
DFTGateVector mParents;
public:
DFTElement(size_t id, std::string const& name) : mId(id), mName(name)
DFTElement(size_t id, std::string const& name) :
mId(id), mName(name)
{}
virtual ~DFTElement() {}
@ -74,7 +81,7 @@ namespace storm {
return mName;
}
bool addParent(std::shared_ptr<DFTGate> const& e) {
bool addParent(DFTGatePointer const& e) {
if(std::find(mParents.begin(), mParents.end(), e) != mParents.end()) {
return false;
}
@ -89,20 +96,21 @@ namespace storm {
return !mParents.empty();
}
std::vector<std::shared_ptr<DFTGate>> const& parents() const {
DFTGateVector const& parents() const {
return mParents;
}
virtual void extendSpareModule(std::set<size_t>& elementsInModule) const;
virtual size_t nrChildren() const = 0;
virtual std::string toString() const = 0;
virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const;
virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const;
virtual std::vector<size_t> independentUnit() const = 0;
virtual void extendUnit(std::set<size_t>& unit) const;
virtual void extendUnit(std::set<size_t>& unit) const;
void checkForSymmetricChildren() const;
};
@ -130,26 +138,34 @@ namespace storm {
assert(false);
}
}
class DFTGate : public DFTElement {
template<typename ValueType>
class DFTGate : public DFTElement<ValueType> {
using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
using DFTElementVector = std::vector<DFTElementPointer>;
protected:
std::vector<std::shared_ptr<DFTElement>> mChildren;
DFTElementVector mChildren;
public:
DFTGate(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children) :
DFTElement(id, name), mChildren(children)
DFTGate(size_t id, std::string const& name, DFTElementVector const& children) :
DFTElement<ValueType>(id, name), mChildren(children)
{}
virtual ~DFTGate() {}
void pushBackChild(std::shared_ptr<DFTElement> elem) {
void pushBackChild(DFTElementPointer elem) {
return mChildren.push_back(elem);
}
size_t nrChildren() const override {
return mChildren.size();
}
std::vector<std::shared_ptr<DFTElement>> const& children() const {
DFTElementVector const& children() const {
return mChildren;
}
@ -159,11 +175,13 @@ namespace storm {
virtual std::string typestring() const = 0;
virtual void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0;
virtual void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0;
virtual void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
virtual void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
virtual void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
DFTElement::extendSpareModule(elementsInSpareModule);
DFTElement<ValueType>::extendSpareModule(elementsInSpareModule);
for(auto const& child : mChildren) {
if(elementsInSpareModule.count(child->id()) == 0) {
elementsInSpareModule.insert(child->id());
@ -173,24 +191,22 @@ namespace storm {
}
virtual std::vector<size_t> independentUnit() const override {
std::set<size_t> unit = {mId};
std::set<size_t> unit = {this->mId};
for(auto const& child : mChildren) {
child->extendUnit(unit);
}
for(auto const& parent : mParents) {
for(auto const& parent : this->mParents) {
if(unit.count(parent->id()) != 0) {
return {};
}
}
return std::vector<size_t>(unit.begin(), unit.end());
}
return std::vector<size_t>(unit.begin(), unit.end());
}
virtual std::string toString() const override {
std::stringstream stream;
stream << "{" << name() << "} " << typestring() << "( ";
std::vector<std::shared_ptr<DFTElement>>::const_iterator it = mChildren.begin();
stream << "{" << this->name() << "} " << typestring() << "( ";
typename DFTElementVector::const_iterator it = mChildren.begin();
stream << (*it)->name();
++it;
while(it != mChildren.end()) {
@ -199,10 +215,10 @@ namespace storm {
}
stream << ")";
return stream.str();
}
virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override {
if(DFTElement::checkDontCareAnymore(state, queues)) {
}
virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
if(DFTElement<ValueType>::checkDontCareAnymore(state, queues)) {
childrenDontCare(state, queues);
return true;
}
@ -210,37 +226,37 @@ namespace storm {
}
virtual void extendUnit(std::set<size_t>& unit) const override {
DFTElement::extendUnit(unit);
DFTElement<ValueType>::extendUnit(unit);
for(auto const& child : mChildren) {
child->extendUnit(unit);
}
}
protected:
void fail(DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
for(std::shared_ptr<DFTGate> parent : mParents) {
void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
for(std::shared_ptr<DFTGate> parent : this->mParents) {
if(state.isOperational(parent->id())) {
queues.propagateFailure(parent);
}
}
state.setFailed(mId);
state.setFailed(this->mId);
}
void failsafe(DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
for(std::shared_ptr<DFTGate> parent : mParents) {
void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
for(std::shared_ptr<DFTGate> parent : this->mParents) {
if(state.isOperational(parent->id())) {
queues.propagateFailsafe(parent);
}
}
state.setFailsafe(mId);
state.setFailsafe(this->mId);
}
void childrenDontCare(DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
void childrenDontCare(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
queues.propagateDontCare(mChildren);
}
bool hasFailsafeChild(DFTState& state) const {
bool hasFailsafeChild(DFTState<ValueType>& state) const {
for(auto const& child : mChildren) {
if(state.isFailsafe(child->id()))
{
@ -249,9 +265,8 @@ namespace storm {
}
return false;
}
bool hasFailedChild(DFTState& state) const {
bool hasFailedChild(DFTState<ValueType>& state) const {
for(auto const& child : mChildren) {
if(state.hasFailed(child->id())) {
return true;
@ -265,17 +280,15 @@ namespace storm {
template<typename ValueType>
class DFTBE : public DFTElement {
class DFTBE : public DFTElement<ValueType> {
ValueType mActiveFailureRate;
ValueType mPassiveFailureRate;
public:
DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor) :
DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate)
{
}
DFTElement<ValueType>(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate)
{}
virtual size_t nrChildren() const {
return 0;
@ -304,9 +317,10 @@ namespace storm {
}
virtual std::vector<size_t> independentUnit() const {
return {mId};
return {this->mId};
}
virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const;
virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const;
};
template<typename ValueType>
@ -314,16 +328,17 @@ namespace storm {
return os << "{" << be.name() << "} BE(" << be.activeFailureRate() << ", " << be.passiveFailureRate() << ")";
}
class DFTConst : public DFTElement {
template<typename ValueType>
class DFTConst : public DFTElement<ValueType> {
bool mFailed;
public:
DFTConst(size_t id, std::string const& name, bool failed) : DFTElement(id, name), mFailed(failed)
{
}
DFTConst(size_t id, std::string const& name, bool failed) :
DFTElement<ValueType>(id, name), mFailed(failed)
{}
bool failed() const {
return mFailed;
@ -339,96 +354,96 @@ namespace storm {
};
class DFTAnd : public DFTGate {
template<typename ValueType>
class DFTAnd : public DFTGate<ValueType> {
public:
DFTAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
DFTGate(id, name, children)
DFTAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
DFTGate<ValueType>(id, name, children)
{}
void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
if(state.isOperational(mId)) {
for(auto const& child : mChildren)
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
if(state.isOperational(this->mId)) {
for(auto const& child : this->mChildren)
{
if(!state.hasFailed(child->id())) {
return;// false;
return;
}
}
fail(state, queues);
//return true;
}
//return false;
this->fail(state, queues);
}
}
void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
assert(hasFailsafeChild(state));
if(state.isOperational(mId)) {
failsafe(state, queues);
childrenDontCare(state, queues);
//return true;
void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const{
assert(this->hasFailsafeChild(state));
if(state.isOperational(this->mId)) {
this->failsafe(state, queues);
this->childrenDontCare(state, queues);
}
//return false;
}
std::string typestring() const {
return "AND";
}
};
inline std::ostream& operator<<(std::ostream& os, DFTAnd const& gate) {
template<typename ValueType>
inline std::ostream& operator<<(std::ostream& os, DFTAnd<ValueType> const& gate) {
return os << gate.toString();
}
class DFTOr : public DFTGate {
template<typename ValueType>
class DFTOr : public DFTGate<ValueType> {
public:
DFTOr(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
DFTGate(id, name, children)
DFTOr(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
DFTGate<ValueType>(id, name, children)
{}
void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
assert(hasFailedChild(state));
if(state.isOperational(mId)) {
fail(state, queues);
//return true;
}
// return false;
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
assert(this->hasFailedChild(state));
if(state.isOperational(this->mId)) {
this->fail(state, queues);
}
}
void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
for(auto const& child : mChildren) {
void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const{
for(auto const& child : this->mChildren) {
if(!state.isFailsafe(child->id())) {
return;// false;
return;
}
}
failsafe(state, queues);
//return true;
this->failsafe(state, queues);
}
std::string typestring() const {
return "OR";
}
private:
//static const std::string typestring = "or";
};
inline std::ostream& operator<<(std::ostream& os, DFTOr const& gate) {
template<typename ValueType>
inline std::ostream& operator<<(std::ostream& os, DFTOr<ValueType> const& gate) {
return os << gate.toString();
}
class DFTSeqAnd : public DFTGate {
template<typename ValueType>
class DFTSeqAnd : public DFTGate<ValueType> {
public:
DFTSeqAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
DFTGate(id, name, children)
DFTSeqAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
DFTGate<ValueType>(id, name, children)
{}
void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
if(!state.hasFailed(mId)) {
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
if(!state.hasFailed(this->mId)) {
bool childOperationalBefore = false;
for(auto const& child : mChildren)
for(auto const& child : this->mChildren)
{
if(!state.hasFailed(child->id())) {
childOperationalBefore = true;
@ -436,22 +451,20 @@ namespace storm {
else {
if(childOperationalBefore) {
state.markAsInvalid();
return; //false;
return;
}
}
}
if(!childOperationalBefore) {
fail(state, queues);
//return true;
}
}
//return false;
}
void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const{
assert(hasFailsafeChild(state));
if(state.isOperational(mId)) {
if(state.isOperational(this->mId)) {
failsafe(state, queues);
//return true;
}
@ -461,71 +474,74 @@ namespace storm {
std::string typestring() const {
return "SEQAND";
}
private:
//static const std::string typestring = "seqand";
};
inline std::ostream& operator<<(std::ostream& os, DFTSeqAnd const& gate) {
template<typename ValueType>
inline std::ostream& operator<<(std::ostream& os, DFTSeqAnd<ValueType> const& gate) {
return os << gate.toString();
}
class DFTPand : public DFTGate {
template<typename ValueType>
class DFTPand : public DFTGate<ValueType> {
public:
DFTPand(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
DFTGate(id, name, children)
DFTPand(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
DFTGate<ValueType>(id, name, children)
{}
void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
if(state.isOperational(mId)) {
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
if(state.isOperational(this->mId)) {
bool childOperationalBefore = false;
for(auto const& child : mChildren)
for(auto const& child : this->mChildren)
{
if(!state.hasFailed(child->id())) {
childOperationalBefore = true;
} else if(childOperationalBefore && state.hasFailed(child->id())){
failsafe(state, queues);
childrenDontCare(state, queues);
return; //false;
this->failsafe(state, queues);
this->childrenDontCare(state, queues);
return;
}
}
if(!childOperationalBefore) {
fail(state, queues);
//return true;
this->fail(state, queues);
}
}
// return false;
}
void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
assert(hasFailsafeChild(state));
if(state.isOperational(mId)) {
failsafe(state, queues);
childrenDontCare(state, queues);
//return true;
void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const{
assert(this->hasFailsafeChild(state));
if(state.isOperational(this->mId)) {
this->failsafe(state, queues);
this->childrenDontCare(state, queues);
}
//return false;
}
}
std::string typestring() const {
return "PAND";
}
};
inline std::ostream& operator<<(std::ostream& os, DFTPand const& gate) {
template<typename ValueType>
inline std::ostream& operator<<(std::ostream& os, DFTPand<ValueType> const& gate) {
return os << gate.toString();
}
class DFTPor : public DFTGate {
template<typename ValueType>
class DFTPor : public DFTGate<ValueType> {
public:
DFTPor(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
DFTGate(id, name, children)
DFTPor(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
DFTGate<ValueType>(id, name, children)
{}
void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
assert(false);
}
void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const{
assert(false);
}
@ -533,58 +549,60 @@ namespace storm {
return "POR";
}
};
inline std::ostream& operator<<(std::ostream& os, DFTPor const& gate) {
template<typename ValueType>
inline std::ostream& operator<<(std::ostream& os, DFTPor<ValueType> const& gate) {
return os << gate.toString();
}
class DFTVot : public DFTGate {
template<typename ValueType>
class DFTVot : public DFTGate<ValueType> {
private:
unsigned mThreshold;
public:
DFTVot(size_t id, std::string const& name, unsigned threshold, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
DFTGate(id, name, children), mThreshold(threshold)
DFTVot(size_t id, std::string const& name, unsigned threshold, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
DFTGate<ValueType>(id, name, children), mThreshold(threshold)
{}
void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
if(state.isOperational(mId)) {
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
if(state.isOperational(this->mId)) {
unsigned nrFailedChildren = 0;
for(auto const& child : mChildren)
for(auto const& child : this->mChildren)
{
if(state.hasFailed(child->id())) {
++nrFailedChildren;
if(nrFailedChildren >= mThreshold)
{
fail(state, queues);
return;// true;
this->fail(state, queues);
return;
}
}
}
}
// return false;
}
void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
assert(hasFailsafeChild(state));
if(state.isOperational(mId)) {
void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const{
assert(this->hasFailsafeChild(state));
if(state.isOperational(this->mId)) {
unsigned nrFailsafeChildren = 0;
for(auto const& child : mChildren)
for(auto const& child : this->mChildren)
{
if(state.isFailsafe(child->id())) {
++nrFailsafeChildren;
if(nrFailsafeChildren > nrChildren() - mThreshold)
if(nrFailsafeChildren > this->nrChildren() - mThreshold)
{
failsafe(state, queues);
childrenDontCare(state, queues);
return;// true;
this->failsafe(state, queues);
this->childrenDontCare(state, queues);
return;
}
}
}
}
//return false;
}
std::string typestring() const {
@ -593,21 +611,24 @@ namespace storm {
};
inline std::ostream& operator<<(std::ostream& os, DFTVot const& gate) {
template<typename ValueType>
inline std::ostream& operator<<(std::ostream& os, DFTVot<ValueType> const& gate) {
return os << gate.toString();
}
class DFTSpare : public DFTGate {
}
template<typename ValueType>
class DFTSpare : public DFTGate<ValueType> {
private:
size_t mUseIndex;
size_t mActiveIndex;
public:
DFTSpare(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
DFTGate(id, name, children)
{
}
DFTSpare(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
DFTGate<ValueType>(id, name, children)
{}
std::string typestring() const {
return "SPARE";
@ -624,39 +645,40 @@ namespace storm {
void setActiveIndex(size_t activeIndex) {
mActiveIndex = activeIndex;
}
void initializeUses(storm::storage::DFTState& state) {
assert(mChildren.size() > 0);
state.setUsesAtPosition(mUseIndex, mChildren[0]->id());
void initializeUses(storm::storage::DFTState<ValueType>& state) {
assert(this->mChildren.size() > 0);
state.setUsesAtPosition(mUseIndex, this->mChildren[0]->id());
}
void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
if(state.isOperational(mId)) {
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
if(state.isOperational(this->mId)) {
size_t uses = state.extractUses(mUseIndex);
if(!state.isOperational(uses)) {
// TODO compute children ids before.
std::vector<size_t> childrenIds;
for(auto const& child : mChildren) {
for(auto const& child : this->mChildren) {
childrenIds.push_back(child->id());
}
bool claimingSuccessful = state.claimNew(mId, mUseIndex, uses, childrenIds);
bool claimingSuccessful = state.claimNew(this->mId, mUseIndex, uses, childrenIds);
if(!claimingSuccessful) {
fail(state, queues);
this->fail(state, queues);
}
}
}
}
void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
if(state.isOperational(mId)) {
void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
if(state.isOperational(this->mId)) {
if(state.isFailsafe(state.extractUses((mUseIndex)))) {
failsafe(state, queues);
childrenDontCare(state, queues);
this->failsafe(state, queues);
this->childrenDontCare(state, queues);
}
}
}
};
}
}

96
src/storage/dft/DFTState.cpp
View File

@ -5,8 +5,8 @@
namespace storm {
namespace storage {
// TODO Matthias: template
DFTState::DFTState(DFT<double> const& dft, size_t id) : mStatus(dft.stateSize()), mId(id), mDft(dft) {
template<typename ValueType>
DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, size_t id) : mStatus(dft.stateSize()), mId(id), mDft(dft) {
mInactiveSpares = dft.getSpareIndices();
dft.initializeUses(*this);
dft.initializeActivation(*this);
@ -14,70 +14,83 @@ namespace storm {
mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end());
}
DFTElementState DFTState::getElementState(size_t id) const {
template<typename ValueType>
DFTElementState DFTState<ValueType>::getElementState(size_t id) const {
return static_cast<DFTElementState>(getElementStateInt(id));
}
int DFTState::getElementStateInt(size_t id) const {
template<typename ValueType>
int DFTState<ValueType>::getElementStateInt(size_t id) const {
return mStatus.getAsInt(mDft.failureIndex(id), 2);
}
size_t DFTState::getId() const {
template<typename ValueType>
size_t DFTState<ValueType>::getId() const {
return mId;
}
void DFTState::setId(size_t id) {
template<typename ValueType>
void DFTState<ValueType>::setId(size_t id) {
mId = id;
}
bool DFTState::isOperational(size_t id) const {
template<typename ValueType>
bool DFTState<ValueType>::isOperational(size_t id) const {
return getElementState(id) == DFTElementState::Operational;
}
bool DFTState::hasFailed(size_t id) const {
template<typename ValueType>
bool DFTState<ValueType>::hasFailed(size_t id) const {
return mStatus[mDft.failureIndex(id)];
}
bool DFTState::isFailsafe(size_t id) const {
template<typename ValueType>
bool DFTState<ValueType>::isFailsafe(size_t id) const {
return mStatus[mDft.failureIndex(id)+1];
}
bool DFTState::dontCare(size_t id) const {
template<typename ValueType>
bool DFTState<ValueType>::dontCare(size_t id) const {
return getElementState(id) == DFTElementState::DontCare;
}
void DFTState::setFailed(size_t id) {
template<typename ValueType>
void DFTState<ValueType>::setFailed(size_t id) {
mStatus.set(mDft.failureIndex(id));
}
void DFTState::setFailsafe(size_t id) {
template<typename ValueType>
void DFTState<ValueType>::setFailsafe(size_t id) {
mStatus.set(mDft.failureIndex(id)+1);
}
void DFTState::setDontCare(size_t id) {
template<typename ValueType>
void DFTState<ValueType>::setDontCare(size_t id) {
mStatus.setFromInt(mDft.failureIndex(id), 2, static_cast<uint_fast64_t>(DFTElementState::DontCare) );
}
void DFTState::beNoLongerFailable(size_t id) {
template<typename ValueType>
void DFTState<ValueType>::beNoLongerFailable(size_t id) {
auto it = std::find(mIsCurrentlyFailableBE.begin(), mIsCurrentlyFailableBE.end(), id);
if(it != mIsCurrentlyFailableBE.end()) {
mIsCurrentlyFailableBE.erase(it);
}
}
// TODO Matthias: template
std::pair<std::shared_ptr<DFTBE<double>>, bool> DFTState::letNextBEFail(size_t index)
template<typename ValueType>
std::pair<std::shared_ptr<DFTBE<ValueType>>, bool> DFTState<ValueType>::letNextBEFail(size_t index)
{
assert(index < mIsCurrentlyFailableBE.size());
STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString());
std::pair<std::shared_ptr<DFTBE<double>>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false);
std::pair<std::shared_ptr<DFTBE<ValueType>>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false);
mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index);
setFailed(res.first->id());
return res;
}
void DFTState::activate(size_t repr) {
template<typename ValueType>
void DFTState<ValueType>::activate(size_t repr) {
std::vector<size_t> const& module = mDft.module(repr);
for(size_t elem : module) {
if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) {
@ -89,33 +102,37 @@ namespace storm {
}
}
}
bool DFTState::isActiveSpare(size_t id) const {
template<typename ValueType>
bool DFTState<ValueType>::isActiveSpare(size_t id) const {
assert(mDft.getElement(id)->isSpareGate());
return (std::find(mInactiveSpares.begin(), mInactiveSpares.end(), id) == mInactiveSpares.end());
}
uint_fast64_t DFTState::uses(size_t id) const {
template<typename ValueType>
uint_fast64_t DFTState<ValueType>::uses(size_t id) const {
return extractUses(mDft.usageIndex(id));
}
uint_fast64_t DFTState::extractUses(size_t from) const {
template<typename ValueType>
uint_fast64_t DFTState<ValueType>::extractUses(size_t from) const {
assert(mDft.usageInfoBits() < 64);
return mStatus.getAsInt(from, mDft.usageInfoBits());
}
bool DFTState::isUsed(size_t child) {
template<typename ValueType>
bool DFTState<ValueType>::isUsed(size_t child) {
return (std::find(mUsedRepresentants.begin(), mUsedRepresentants.end(), child) != mUsedRepresentants.end());
}
void DFTState::setUsesAtPosition(size_t usageIndex, size_t child) {
template<typename ValueType>
void DFTState<ValueType>::setUsesAtPosition(size_t usageIndex, size_t child) {
mStatus.setFromInt(usageIndex, mDft.usageInfoBits(), child);
mUsedRepresentants.push_back(child);
}
bool DFTState::claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector<size_t> const& childIds) {
template<typename ValueType>
bool DFTState<ValueType>::claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector<size_t> const& childIds) {
auto it = find(childIds.begin(), childIds.end(), currentlyUses);
assert(it != childIds.end());
++it;
@ -132,5 +149,12 @@ namespace storm {
return false;
}
// Explicitly instantiate the class.
template class DFTState<double>;
#ifdef STORM_HAVE_CARL
template class DFTState<RationalFunction>;
#endif
}
}
}

17
src/storage/dft/DFTState.h
View File

@ -14,7 +14,7 @@ namespace storm {
template<typename ValueType>
class DFTBE;
template<typename ValueType>
class DFTState {
friend struct std::hash<DFTState>;
private:
@ -24,12 +24,10 @@ namespace storm {
std::vector<size_t> mIsCurrentlyFailableBE;
std::vector<size_t> mUsedRepresentants;
bool mValid = true;
// TODO Matthias: template
const DFT<double>& mDft;
const DFT<ValueType>& mDft;
public:
// TODO Matthias: template
DFTState(DFT<double> const& dft, size_t id);
DFTState(DFT<ValueType> const& dft, size_t id);
DFTElementState getElementState(size_t id) const;
@ -109,8 +107,7 @@ namespace storm {
return mIsCurrentlyFailableBE.size();
}
// TODO Matthias: template
std::pair<std::shared_ptr<DFTBE<double>>, bool> letNextBEFail(size_t smallestIndex = 0);
std::pair<std::shared_ptr<DFTBE<ValueType>>, bool> letNextBEFail(size_t smallestIndex = 0);
std::string getCurrentlyFailableString() {
std::stringstream stream;
@ -137,9 +134,9 @@ namespace storm {
}
namespace std {
template<>
struct hash<storm::storage::DFTState> {
size_t operator()(storm::storage::DFTState const& s) const {
template<typename ValueType>
struct hash<storm::storage::DFTState<ValueType>> {
size_t operator()(storm::storage::DFTState<ValueType> const& s) const {
return hash<storm::storage::BitVector>()(s.mStatus);
}
};

49
src/storage/dft/DFTStateSpaceGenerationQueues.h
View File

@ -10,19 +10,28 @@
namespace storm {
namespace storage {
template<typename ValueType>
class DFTGate;
template<typename ValueType>
class DFTElement;
template<typename ValueType>
class DFTStateSpaceGenerationQueues {
std::priority_queue<std::shared_ptr<DFTGate>, std::vector<std::shared_ptr<DFTGate>>, OrderElementsByRank> failurePropagation;
std::vector<std::shared_ptr<DFTGate>> failsafePropagation;
std::vector<std::shared_ptr<DFTElement>> dontcarePropagation;
std::vector<std::shared_ptr<DFTElement>> activatePropagation;
using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
using DFTElementVector = std::vector<DFTElementPointer>;
using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
using DFTGateVector = std::vector<DFTGatePointer>;
std::priority_queue<DFTGatePointer, DFTGateVector, OrderElementsByRank<ValueType>> failurePropagation;
DFTGateVector failsafePropagation;
DFTElementVector dontcarePropagation;
DFTElementVector activatePropagation;
public:
void propagateFailure(std::shared_ptr<DFTGate> const& elem) {
void propagateFailure(DFTGatePointer const& elem) {
failurePropagation.push(elem);
}
@ -30,8 +39,8 @@ namespace storm {
return failurePropagation.empty();
}
std::shared_ptr<DFTGate> nextFailurePropagation() {
std::shared_ptr<DFTGate> next = failurePropagation.top();
DFTGatePointer nextFailurePropagation() {
DFTGatePointer next = failurePropagation.top();
failurePropagation.pop();
return next;
}
@ -40,12 +49,12 @@ namespace storm {
return failsafePropagation.empty();
}
void propagateFailsafe(std::shared_ptr<DFTGate> const& gate) {
void propagateFailsafe(DFTGatePointer const& gate) {
failsafePropagation.push_back(gate);
}
std::shared_ptr<DFTGate> nextFailsafePropagation() {
std::shared_ptr<DFTGate> next = failsafePropagation.back();
DFTGatePointer nextFailsafePropagation() {
DFTGatePointer next = failsafePropagation.back();
failsafePropagation.pop_back();
return next;
}
@ -54,25 +63,23 @@ namespace storm {
return dontcarePropagation.empty();
}
void propagateDontCare(std::shared_ptr<DFTElement> const& elem) {
void propagateDontCare(DFTElementPointer const& elem) {
dontcarePropagation.push_back(elem);
}
void propagateDontCare(std::vector<std::shared_ptr<DFTElement>> const& elems) {
void propagateDontCare(DFTElementVector const& elems) {
dontcarePropagation.insert(dontcarePropagation.end(), elems.begin(), elems.end());
}
std::shared_ptr<DFTElement> nextDontCarePropagation() {
std::shared_ptr<DFTElement> next = dontcarePropagation.back();
DFTElementPointer nextDontCarePropagation() {
DFTElementPointer next = dontcarePropagation.back();
dontcarePropagation.pop_back();
return next;
}
};
}
}
#endif /* DFTSTATESPACEGENERATIONQUEUES_H */

25
src/storage/dft/OrderDFTElementsById.cpp
View File

@ -3,16 +3,31 @@
namespace storm {
namespace storage {
bool OrderElementsById::operator()(std::shared_ptr<DFTGate> const& a , std::shared_ptr<DFTGate> const& b) const {
template<typename ValueType>
bool OrderElementsById<ValueType>::operator()(std::shared_ptr<DFTGate<ValueType>> const& a , std::shared_ptr<DFTGate<ValueType>> const& b) const {
return a->id() < b->id();
}
bool OrderElementsById::operator ()(const std::shared_ptr<DFTElement>& a, const std::shared_ptr<DFTElement>& b) const {
template<typename ValueType>
bool OrderElementsById<ValueType>::operator ()(const std::shared_ptr<DFTElement<ValueType>>& a, const std::shared_ptr<DFTElement<ValueType>>& b) const {
return a->id() < b->id();
}
bool OrderElementsByRank::operator ()(const std::shared_ptr<DFTGate>& a, const std::shared_ptr<DFTGate>& b) const {
template<typename ValueType>
bool OrderElementsByRank<ValueType>::operator ()(const std::shared_ptr<DFTGate<ValueType>>& a, const std::shared_ptr<DFTGate<ValueType>>& b) const {
return a->rank() < b->rank();
}
// Explicitly instantiate the class.
template class OrderElementsById<double>;
template class OrderElementsByRank<double>;
#ifdef STORM_HAVE_CARL
template class OrderElementsById<RationalFunction>;
template class OrderElementsByRank<RationalFunction>;
#endif
}
}

16
src/storage/dft/OrderDFTElementsById.h
View File

@ -5,16 +5,22 @@
namespace storm {
namespace storage {
template<typename ValueType>
class DFTGate;
template<typename ValueType>
class DFTElement;
template<typename ValueType>
struct OrderElementsById {
bool operator()(std::shared_ptr<DFTGate> const& a , std::shared_ptr<DFTGate> const& b) const;
bool operator()(std::shared_ptr<DFTElement> const& a, std::shared_ptr<DFTElement> const& b) const;
bool operator()(std::shared_ptr<DFTGate<ValueType>> const& a , std::shared_ptr<DFTGate<ValueType>> const& b) const;
bool operator()(std::shared_ptr<DFTElement<ValueType>> const& a, std::shared_ptr<DFTElement<ValueType>> const& b) const;
};
template<typename ValueType>
struct OrderElementsByRank {
bool operator()(std::shared_ptr<DFTGate> const& a, std::shared_ptr<DFTGate> const& b) const;
bool operator()(std::shared_ptr<DFTGate<ValueType>> const& a, std::shared_ptr<DFTGate<ValueType>> const& b) const;
};
}

Write Preview
Loading…
Cancel
Save