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

Changed unordered_set to BitVectorHashMap for DFTState 

Former-commit-id: 35f57aa250
tempestpy_adaptions
Mavo 9 years ago
parent
dd17955a3e
commit
69a464d5ef
5 changed files with 63 additions and 52 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. 66
      src/builder/ExplicitDFTModelBuilder.cpp
  2. 11
      src/builder/ExplicitDFTModelBuilder.h
  3. 7
      src/storage/BitVectorHashMap.cpp
  4. 18
      src/storage/dft/DFT.cpp
  5. 13
      src/storage/dft/DFT.h

66
src/builder/ExplicitDFTModelBuilder.cpp
View File

@ -14,10 +14,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<ValueType> state(mDft, newIndex++);
mStates.insert(state);
DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, newIndex++);
mStates.findOrAdd(state->status(), state);
std::queue<storm::storage::DFTState<ValueType>> stateQueue;
std::queue<DFTStatePointer> stateQueue;
stateQueue.push(state);
bool deterministicModel = true;
@ -47,17 +47,18 @@ namespace storm {
modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
}
for (storm::storage::DFTState<ValueType> state : mStates) {
for (auto const& stateVectorPair : mStates) {
DFTStatePointer state = stateVectorPair.second;
if (mDft.hasFailed(state)) {
modelComponents.stateLabeling.addLabelToState("failed", state.getId());
modelComponents.stateLabeling.addLabelToState("failed", state->getId());
}
if (mDft.isFailsafe(state)) {
modelComponents.stateLabeling.addLabelToState("failsafe", state.getId());
modelComponents.stateLabeling.addLabelToState("failsafe", state->getId());
};
// Set fail status for each BE
for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
if (state.hasFailed(elem->id())) {
modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", state.getId());
if (state->hasFailed(elem->id())) {
modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", state->getId());
}
}
}
@ -69,7 +70,7 @@ namespace storm {
}
template<typename ValueType, typename RewardModelType, typename IndexType>
void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::exploreStates(std::queue<storm::storage::DFTState<ValueType>>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder) {
void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::exploreStates(std::queue<DFTStatePointer>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder) {
std::map<size_t, ValueType> outgoingTransitions;
@ -79,25 +80,26 @@ namespace storm {
ValueType sum = storm::utility::zero<ValueType>();
// Consider next state
storm::storage::DFTState<ValueType> state = stateQueue.front();
DFTStatePointer state = stateQueue.front();
stateQueue.pop();
size_t smallest = 0;
// Add self loop for target states
if (mDft.hasFailed(state) || mDft.isFailsafe(state)) {
transitionMatrixBuilder.addNextValue(state.getId(), state.getId(), storm::utility::one<ValueType>());
STORM_LOG_TRACE("Added self loop for " << state.getId());
transitionMatrixBuilder.addNextValue(state->getId(), state->getId(), storm::utility::one<ValueType>());
STORM_LOG_TRACE("Added self loop for " << state->getId());
// No further exploration required
continue;
}
// Let BE fail
while (smallest < state.nrFailableBEs()) {
while (smallest < state->nrFailableBEs()) {
STORM_LOG_TRACE("exploring from: " << mDft.getStateString(state));
storm::storage::DFTState<ValueType> newState(state);
std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType>>, bool> nextBEPair = newState.letNextBEFail(smallest++);
// Construct new state as copy from original one
DFTStatePointer newState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType>>, bool> nextBEPair = newState->letNextBEFail(smallest++);
std::shared_ptr<storm::storage::DFTBE<ValueType>> nextBE = nextBEPair.first;
if (nextBE == nullptr) {
break;
@ -107,57 +109,55 @@ namespace storm {
storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;
for (DFTGatePointer parent : nextBE->parents()) {
if (newState.isOperational(parent->id())) {
if (newState->isOperational(parent->id())) {
queues.propagateFailure(parent);
}
}
while (!queues.failurePropagationDone()) {
DFTGatePointer next = queues.nextFailurePropagation();
next->checkFails(newState, queues);
next->checkFails(*newState, queues);
}
while (!queues.failsafePropagationDone()) {
DFTGatePointer next = queues.nextFailsafePropagation();
next->checkFailsafe(newState, queues);
next->checkFailsafe(*newState, queues);
}
while (!queues.dontCarePropagationDone()) {
DFTElementPointer next = queues.nextDontCarePropagation();
next->checkDontCareAnymore(newState, queues);
next->checkDontCareAnymore(*newState, queues);
}
auto itState = mStates.find(newState);
if (itState == mStates.end()) {
if (mStates.contains(newState->status())) {
// State already exists
newState = mStates.findOrAdd(newState->status(), newState);
STORM_LOG_TRACE("State " << mDft.getStateString(newState) << " already exists");
} else {
// New state
newState.setId(newIndex++);
auto itInsert = mStates.insert(newState);
assert(itInsert.second);
itState = itInsert.first;
newState->setId(newIndex++);
mStates.findOrAdd(newState->status(), newState);
STORM_LOG_TRACE("New state " << mDft.getStateString(newState));
// Add state to search
stateQueue.push(newState);
} else {
// State already exists
STORM_LOG_TRACE("State " << mDft.getStateString(*itState) << " already exists");
}
// Set failure rate according to usage
bool isUsed = true;
if (mDft.hasRepresentant(nextBE->id())) {
DFTElementPointer representant = mDft.getRepresentant(nextBE->id());
isUsed = newState.isUsed(representant->id());
isUsed = newState->isUsed(representant->id());
}
STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used"));
ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
auto resultFind = outgoingTransitions.find(itState->getId());
auto resultFind = outgoingTransitions.find(newState->getId());
if (resultFind != outgoingTransitions.end()) {
// Add to existing transition
resultFind->second += rate;
} else {
// Insert new transition
outgoingTransitions.insert(std::make_pair(itState->getId(), rate));
outgoingTransitions.insert(std::make_pair(newState->getId(), rate));
}
sum += rate;
} // end while failing BE
@ -167,8 +167,8 @@ namespace storm {
{
// TODO Matthias: correct?
ValueType rate = it->second;// / sum;
transitionMatrixBuilder.addNextValue(state.getId(), it->first, rate);
STORM_LOG_TRACE("Added transition from " << state.getId() << " to " << it->first << " with " << rate);
transitionMatrixBuilder.addNextValue(state->getId(), it->first, rate);
STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << it->first << " with " << rate);
}
} // end while queue

11
src/builder/ExplicitDFTModelBuilder.h
View File

@ -7,6 +7,7 @@
#include <src/models/sparse/StandardRewardModel.h>
#include <src/models/sparse/Model.h>
#include <src/storage/SparseMatrix.h>
#include <src/storage/BitVectorHashMap.h>
#include <boost/container/flat_set.hpp>
#include <boost/optional/optional.hpp>
#include <stack>
@ -20,6 +21,7 @@ namespace storm {
using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
using DFTGatePointer = std::shared_ptr<storm::storage::DFTGate<ValueType>>;
using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
// A structure holding the individual components of a model.
struct ModelComponents {
@ -39,18 +41,19 @@ namespace storm {
};
storm::storage::DFT<ValueType> const &mDft;
std::unordered_set<storm::storage::DFTState<ValueType>> mStates;
storm::storage::BitVectorHashMap<DFTStatePointer> mStates;
size_t newIndex = 0;
public:
ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const &dft) : mDft(dft) {
ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const &dft) : mDft(dft), mStates(((mDft.stateSize() / 64) + 1) * 64, std::pow(2, mDft.nrBasicElements())) {
// stateSize is bound for size of bitvector
// 2^nrBE is upper bound for state space
}
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildCTMC();
private:
void exploreStates(std::queue<storm::storage::DFTState<ValueType>>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);
void exploreStates(std::queue<DFTStatePointer>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);
};
}

7
src/storage/BitVectorHashMap.cpp
View File

@ -4,6 +4,9 @@
#include "src/utility/macros.h"
#include "src/storage/dft/DFTState.h"
#include "src/adapters/CarlAdapter.h"
namespace storm {
namespace storage {
template<class ValueType, class Hash1, class Hash2>
@ -240,5 +243,9 @@ namespace storm {
template class BitVectorHashMap<uint_fast64_t>;
template class BitVectorHashMap<uint32_t>;
template class BitVectorHashMap<std::shared_ptr<DFTState<double>>>;
#ifdef STORM_HAVE_CARL
template class BitVectorHashMap<std::shared_ptr<DFTState<storm::RationalFunction>>>;
#endif
}
}

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

@ -109,17 +109,17 @@ namespace storm {
}
template<typename ValueType>
std::string DFT<ValueType>::getElementsWithStateString(DFTState<ValueType> const& state) const{
std::string DFT<ValueType>::getElementsWithStateString(DFTStatePointer const& state) const{
std::stringstream stream;
for (auto const& elem : mElements) {
stream << "[" << elem->id() << "]";
stream << elem->toString();
stream << "\t** " << state.getElementState(elem->id());
stream << "\t** " << state->getElementState(elem->id());
if(elem->isSpareGate()) {
if(state.isActiveSpare(elem->id())) {
if(state->isActiveSpare(elem->id())) {
stream << " actively";
}
stream << " using " << state.uses(elem->id());
stream << " using " << state->uses(elem->id());
}
stream << std::endl;
}
@ -127,16 +127,16 @@ namespace storm {
}
template<typename ValueType>
std::string DFT<ValueType>::getStateString(DFTState<ValueType> const& state) const{
std::string DFT<ValueType>::getStateString(DFTStatePointer const& state) const{
std::stringstream stream;
stream << "(" << state.getId() << ") ";
stream << "(" << state->getId() << ") ";
for (auto const& elem : mElements) {
stream << state.getElementStateInt(elem->id());
stream << state->getElementStateInt(elem->id());
if(elem->isSpareGate()) {
if(state.isActiveSpare(elem->id())) {
if(state->isActiveSpare(elem->id())) {
stream << " actively";
}
stream << " using " << state.uses(elem->id());
stream << " using " << state->uses(elem->id());
}
}
return stream.str();

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

@ -37,6 +37,7 @@ namespace storm {
using DFTElementVector = std::vector<DFTElementPointer>;
using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
using DFTGateVector = std::vector<DFTGatePointer>;
using DFTStatePointer = std::shared_ptr<DFTState<ValueType>>;
private:
DFTElementVector mElements;
@ -164,12 +165,12 @@ namespace storm {
return getElement(mRepresentants.find(id)->second);
}
bool hasFailed(DFTState<ValueType> const& state) const {
return state.hasFailed(mTopLevelIndex);
bool hasFailed(DFTStatePointer const& state) const {
return state->hasFailed(mTopLevelIndex);
}
bool isFailsafe(DFTState<ValueType> const& state) const {
return state.isFailsafe(mTopLevelIndex);
bool isFailsafe(DFTStatePointer const& state) const {
return state->isFailsafe(mTopLevelIndex);
}
std::string getElementsString() const;
@ -178,9 +179,9 @@ namespace storm {
std::string getSpareModulesString() const;
std::string getElementsWithStateString(DFTState<ValueType> const& state) const;
std::string getElementsWithStateString(DFTStatePointer const& state) const;
std::string getStateString(DFTState<ValueType> const& state) const;
std::string getStateString(DFTStatePointer const& state) const;
private:
bool elementIndicesCorrect() const {

Write Preview
Loading…
Cancel
Save