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

Use only state ids instead of complete data structure 

Former-commit-id: 0852cce6d7
main
Mavo 9 years ago
parent
20242e10e5
commit
d160bb1b13
7 changed files with 62 additions and 42 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 63
      src/builder/ExplicitDFTModelBuilder.cpp
  2. 4
      src/builder/ExplicitDFTModelBuilder.h
  3. 8
      src/storage/BitVectorHashMap.cpp
  4. 1
      src/storage/dft/DFT.cpp
  5. 8
      src/storage/dft/DFT.h
  6. 10
      src/storage/dft/DFTState.cpp
  7. 6
      src/storage/dft/DFTState.h

63
src/builder/ExplicitDFTModelBuilder.cpp
View File

@ -15,14 +15,13 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
ExplicitDFTModelBuilder<ValueType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, std::pow(2, mDft.nrBasicElements())) {
// stateSize is bound for size of bitvector
// 2^nrBE is upper bound for state space
ExplicitDFTModelBuilder<ValueType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, INITIAL_BUCKETSIZE) {
// stateVectorSize is bound for size of bitvector
// Find symmetries // Find symmetries
// TODO activate // TODO activate
// Currently using hack to test // Currently using hack to test
std::vector<std::vector<size_t>> symmetries;
std::vector<std::vector<size_t>> symmetriesTmp;
std::vector<size_t> vecB; std::vector<size_t> vecB;
std::vector<size_t> vecC; std::vector<size_t> vecC;
std::vector<size_t> vecD; std::vector<size_t> vecD;
@ -38,11 +37,11 @@ namespace storm {
vecD.push_back(id); vecD.push_back(id);
} }
} }
symmetries.push_back(vecB);
symmetries.push_back(vecC);
symmetries.push_back(vecD);
symmetriesTmp.push_back(vecB);
symmetriesTmp.push_back(vecC);
symmetriesTmp.push_back(vecD);
std::cout << "Found the following symmetries:" << std::endl; std::cout << "Found the following symmetries:" << std::endl;
for (auto const& symmetry : symmetries) {
for (auto const& symmetry : symmetriesTmp) {
for (auto const& elem : symmetry) { for (auto const& elem : symmetry) {
std::cout << elem << " -> "; std::cout << elem << " -> ";
} }
@ -51,7 +50,7 @@ namespace storm {
} else { } else {
vecB.push_back(mDft.getTopLevelIndex()); vecB.push_back(mDft.getTopLevelIndex());
} }
mStateGenerationInfo = std::make_shared<storm::storage::DFTStateGenerationInfo>(mDft.buildStateGenerationInfo(vecB, symmetries));
mStateGenerationInfo = std::make_shared<storm::storage::DFTStateGenerationInfo>(mDft.buildStateGenerationInfo(vecB, symmetriesTmp));
} }
@ -59,7 +58,7 @@ namespace storm {
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildModel() { std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildModel() {
// Initialize // Initialize
DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, *mStateGenerationInfo, newIndex++); DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, *mStateGenerationInfo, newIndex++);
mStates.findOrAdd(state->status(), state);
mStates.findOrAdd(state->status(), state->getId());
std::queue<DFTStatePointer> stateQueue; std::queue<DFTStatePointer> stateQueue;
stateQueue.push(state); stateQueue.push(state);
@ -97,18 +96,19 @@ namespace storm {
modelComponents.stateLabeling.addLabel(elem->name() + "_fail"); modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
} }
for (auto const& stateVectorPair : mStates) {
DFTStatePointer state = stateVectorPair.second;
if (mDft.hasFailed(state)) {
modelComponents.stateLabeling.addLabelToState("failed", state->getId());
for (auto const& stateIdPair : mStates) {
storm::storage::BitVector state = stateIdPair.first;
size_t stateId = stateIdPair.second;
if (mDft.hasFailed(state, *mStateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failed", stateId);
} }
if (mDft.isFailsafe(state)) {
modelComponents.stateLabeling.addLabelToState("failsafe", state->getId());
if (mDft.isFailsafe(state, *mStateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failsafe", stateId);
}; };
// Set fail status for each BE // Set fail status for each BE
for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) { for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
if (state->hasFailed(elem->id())) {
modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", state->getId());
if (storm::storage::DFTState<ValueType>::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id()))) {
modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId);
} }
} }
} }
@ -214,14 +214,15 @@ namespace storm {
// Update failable dependencies // Update failable dependencies
newState->updateFailableDependencies(nextBE->id()); newState->updateFailableDependencies(nextBE->id());
size_t newStateId;
if (mStates.contains(newState->status())) { if (mStates.contains(newState->status())) {
// State already exists // State already exists
newState = mStates.findOrAdd(newState->status(), newState);
newStateId = mStates.getValue(newState->status());
STORM_LOG_TRACE("State " << mDft.getStateString(newState) << " already exists"); STORM_LOG_TRACE("State " << mDft.getStateString(newState) << " already exists");
} else { } else {
// New state // New state
newState->setId(newIndex++); newState->setId(newIndex++);
mStates.findOrAdd(newState->status(), newState);
newStateId = mStates.findOrAdd(newState->status(), newState->getId());
STORM_LOG_TRACE("New state " << mDft.getStateString(newState)); STORM_LOG_TRACE("New state " << mDft.getStateString(newState));
// Add state to search queue // Add state to search queue
@ -232,22 +233,22 @@ namespace storm {
if (hasDependencies) { if (hasDependencies) {
// Failure is due to dependency -> add non-deterministic choice // Failure is due to dependency -> add non-deterministic choice
std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency = mDft.getDependency(state->getDependencyId(smallest-1)); std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency = mDft.getDependency(state->getDependencyId(smallest-1));
transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, newState->getId(), dependency->probability());
STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with probability " << dependency->probability());
transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, newStateId, dependency->probability());
STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newStateId << " with probability " << dependency->probability());
if (!storm::utility::isOne(dependency->probability())) { if (!storm::utility::isOne(dependency->probability())) {
// Add transition to state where dependency was unsuccessful // Add transition to state where dependency was unsuccessful
DFTStatePointer unsuccessfulState = std::make_shared<storm::storage::DFTState<ValueType>>(*state); DFTStatePointer unsuccessfulState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
unsuccessfulState->letDependencyBeUnsuccessful(smallest-1); unsuccessfulState->letDependencyBeUnsuccessful(smallest-1);
size_t unsuccessfulStateId;
if (mStates.contains(unsuccessfulState->status())) { if (mStates.contains(unsuccessfulState->status())) {
// Unsuccessful state already exists // Unsuccessful state already exists
unsuccessfulState = mStates.findOrAdd(unsuccessfulState->status(), unsuccessfulState);
unsuccessfulStateId = mStates.getValue(unsuccessfulState->status());
STORM_LOG_TRACE("State " << mDft.getStateString(unsuccessfulState) << " already exists"); STORM_LOG_TRACE("State " << mDft.getStateString(unsuccessfulState) << " already exists");
} else { } else {
// New unsuccessful state // New unsuccessful state
unsuccessfulState->setId(newIndex++); unsuccessfulState->setId(newIndex++);
mStates.findOrAdd(unsuccessfulState->status(), unsuccessfulState);
unsuccessfulStateId = mStates.findOrAdd(unsuccessfulState->status(), unsuccessfulState->getId());
STORM_LOG_TRACE("New state " << mDft.getStateString(unsuccessfulState)); STORM_LOG_TRACE("New state " << mDft.getStateString(unsuccessfulState));
// Add unsuccessful state to search queue // Add unsuccessful state to search queue
@ -255,11 +256,11 @@ namespace storm {
} }
ValueType remainingProbability = storm::utility::one<ValueType>() - dependency->probability(); ValueType remainingProbability = storm::utility::one<ValueType>() - dependency->probability();
transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, unsuccessfulState->getId(), remainingProbability);
STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << unsuccessfulState->getId() << " with probability " << remainingProbability);
transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, unsuccessfulStateId, remainingProbability);
STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << unsuccessfulStateId << " with probability " << remainingProbability);
} else { } else {
// Self-loop with probability one cannot be eliminated later one. // Self-loop with probability one cannot be eliminated later one.
assert(state->getId() != newState->getId());
assert(state->getId() != newStateId);
} }
++rowOffset; ++rowOffset;
@ -274,15 +275,15 @@ namespace storm {
} }
STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used")); STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used"));
ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
auto resultFind = outgoingTransitions.find(newState->getId());
auto resultFind = outgoingTransitions.find(newStateId);
if (resultFind != outgoingTransitions.end()) { if (resultFind != outgoingTransitions.end()) {
// Add to existing transition // Add to existing transition
resultFind->second += rate; resultFind->second += rate;
STORM_LOG_TRACE("Updated transition from " << state->getId() << " to " << resultFind->first << " with rate " << rate << " to new rate " << resultFind->second); STORM_LOG_TRACE("Updated transition from " << state->getId() << " to " << resultFind->first << " with rate " << rate << " to new rate " << resultFind->second);
} else { } else {
// Insert new transition // Insert new transition
outgoingTransitions.insert(std::make_pair(newState->getId(), rate));
STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with rate " << rate);
outgoingTransitions.insert(std::make_pair(newStateId, rate));
STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newStateId << " with rate " << rate);
} }
exitRate += rate; exitRate += rate;
} }

4
src/builder/ExplicitDFTModelBuilder.h
View File

@ -44,9 +44,11 @@ namespace storm {
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling; boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
}; };
const size_t INITIAL_BUCKETSIZE = 20000;
storm::storage::DFT<ValueType> const& mDft; storm::storage::DFT<ValueType> const& mDft;
std::shared_ptr<storm::storage::DFTStateGenerationInfo> mStateGenerationInfo; std::shared_ptr<storm::storage::DFTStateGenerationInfo> mStateGenerationInfo;
storm::storage::BitVectorHashMap<DFTStatePointer> mStates;
storm::storage::BitVectorHashMap<size_t> mStates;
size_t newIndex = 0; size_t newIndex = 0;
public: public:

8
src/storage/BitVectorHashMap.cpp
View File

@ -4,9 +4,6 @@
#include "src/utility/macros.h" #include "src/utility/macros.h"
#include "src/storage/dft/DFTState.h"
#include "src/adapters/CarlAdapter.h"
namespace storm { namespace storm {
namespace storage { namespace storage {
template<class ValueType, class Hash1, class Hash2> template<class ValueType, class Hash1, class Hash2>
@ -243,9 +240,6 @@ namespace storm {
template class BitVectorHashMap<uint_fast64_t>; template class BitVectorHashMap<uint_fast64_t>;
template class BitVectorHashMap<uint32_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
template class BitVectorHashMap<size_t>;
} }
} }

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

@ -204,6 +204,7 @@ namespace storm {
return stream.str(); return stream.str();
} }
// TODO rewrite to only use bitvector and id
template<typename ValueType> template<typename ValueType>
std::string DFT<ValueType>::getStateString(DFTStatePointer const& state) const{ std::string DFT<ValueType>::getStateString(DFTStatePointer const& state) const{
std::stringstream stream; std::stringstream stream;

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

@ -244,10 +244,18 @@ namespace storm {
return state->hasFailed(mTopLevelIndex); return state->hasFailed(mTopLevelIndex);
} }
bool hasFailed(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo) const {
return storm::storage::DFTState<ValueType>::hasFailed(state, stateGenerationInfo.getStateIndex(mTopLevelIndex));
}
bool isFailsafe(DFTStatePointer const& state) const { bool isFailsafe(DFTStatePointer const& state) const {
return state->isFailsafe(mTopLevelIndex); return state->isFailsafe(mTopLevelIndex);
} }
bool isFailsafe(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo) const {
return storm::storage::DFTState<ValueType>::isFailsafe(state, stateGenerationInfo.getStateIndex(mTopLevelIndex));
}
std::string getElementsString() const; std::string getElementsString() const;
std::string getInfoString() const; std::string getInfoString() const;

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

@ -64,11 +64,21 @@ namespace storm {
return mStatus[mStateGenerationInfo.getStateIndex(id)]; return mStatus[mStateGenerationInfo.getStateIndex(id)];
} }
template<typename ValueType>
bool DFTState<ValueType>::hasFailed(storm::storage::BitVector const& state, size_t indexId) {
return state[indexId];
}
template<typename ValueType> template<typename ValueType>
bool DFTState<ValueType>::isFailsafe(size_t id) const { bool DFTState<ValueType>::isFailsafe(size_t id) const {
return mStatus[mStateGenerationInfo.getStateIndex(id)+1]; return mStatus[mStateGenerationInfo.getStateIndex(id)+1];
} }
template<typename ValueType>
bool DFTState<ValueType>::isFailsafe(storm::storage::BitVector const& state, size_t indexId) {
return state[indexId+1];
}
template<typename ValueType> template<typename ValueType>
bool DFTState<ValueType>::dontCare(size_t id) const { bool DFTState<ValueType>::dontCare(size_t id) const {
return getElementState(id) == DFTElementState::DontCare; return getElementState(id) == DFTElementState::DontCare;

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

@ -51,7 +51,11 @@ namespace storm {
bool hasFailed(size_t id) const; bool hasFailed(size_t id) const;
bool isFailsafe(size_t id) const ;
static bool hasFailed(storm::storage::BitVector const& state, size_t indexId);
bool isFailsafe(size_t id) const;
static bool isFailsafe(storm::storage::BitVector const& state, size_t indexId);
bool dontCare(size_t id) const; bool dontCare(size_t id) const;

Write Preview
Loading…
Cancel
Save