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

Small refactoring 

Former-commit-id: 220d7408e7
main
Mavo 10 years ago
parent
8ecd75d0e9
commit
5da88d5d52
5 changed files with 25 additions and 19 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. 2
      src/CMakeLists.txt
  2. 2
      src/builder/ExplicitDFTModelBuilder.h
  3. 20
      src/storage/dft/DFT.cpp
  4. 15
      src/storage/dft/DFT.h
  5. 3
      src/storage/dft/DFTState.cpp

2
src/CMakeLists.txt
View File

@ -37,13 +37,13 @@ file(GLOB STORM_SOLVER_STATEELIMINATION_FILES ${PROJECT_SOURCE_DIR}/src/solver/s
file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp)
file(GLOB STORM_STORAGE_BISIMULATION_FILES ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.h ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.cpp) file(GLOB STORM_STORAGE_BISIMULATION_FILES ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.h ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.cpp)
file(GLOB STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp) file(GLOB STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp)
file(GLOB STORM_STORAGE_DFT_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/*.h ${PROJECT_SOURCE_DIR}/src/storage/dft/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_DD_CUDD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_CUDD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_DD_SYLVAN_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_SYLVAN_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp) file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp) file(GLOB_RECURSE STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp) file(GLOB_RECURSE STORM_STORAGE_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp)
file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_DFT_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp)
# Additional include files like the storm-config.h # Additional include files like the storm-config.h

2
src/builder/ExplicitDFTModelBuilder.h
View File

@ -49,7 +49,7 @@ namespace storm {
size_t newIndex = 0; size_t newIndex = 0;
public: public:
ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const &dft) : mDft(dft), mStates(((mDft.stateSize() / 64) + 1) * 64, std::pow(2, mDft.nrBasicElements())) {
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 // stateSize is bound for size of bitvector
// 2^nrBE is upper bound for state space // 2^nrBE is upper bound for state space
} }

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

@ -10,12 +10,11 @@ namespace storm {
namespace storage { namespace storage {
template<typename ValueType> template<typename ValueType>
DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0)
DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mTopLevelIndex(tle->id()), mNrOfBEs(0), mNrOfSpares(0)
{ {
assert(elementIndicesCorrect()); assert(elementIndicesCorrect());
size_t stateIndex = 0;
mUsageInfoBits = storm::utility::math::uint64_log2(mElements.size()-1)+1; mUsageInfoBits = storm::utility::math::uint64_log2(mElements.size()-1)+1;
size_t stateIndex = 0;
for (auto& elem : mElements) { for (auto& elem : mElements) {
mIdToFailureIndex.push_back(stateIndex); mIdToFailureIndex.push_back(stateIndex);
@ -25,6 +24,7 @@ namespace storm {
} }
else if (elem->isSpareGate()) { else if (elem->isSpareGate()) {
++mNrOfSpares; ++mNrOfSpares;
bool firstChild = true;
for(auto const& spareReprs : std::static_pointer_cast<DFTSpare<ValueType>>(elem)->children()) { for(auto const& spareReprs : std::static_pointer_cast<DFTSpare<ValueType>>(elem)->children()) {
if(mActivationIndex.count(spareReprs->id()) == 0) { if(mActivationIndex.count(spareReprs->id()) == 0) {
mActivationIndex[spareReprs->id()] = stateIndex++; mActivationIndex[spareReprs->id()] = stateIndex++;
@ -32,11 +32,9 @@ namespace storm {
std::set<size_t> module = {spareReprs->id()}; std::set<size_t> module = {spareReprs->id()};
spareReprs->extendSpareModule(module); spareReprs->extendSpareModule(module);
std::vector<size_t> sparesAndBes; std::vector<size_t> sparesAndBes;
bool secondSpare = false;
for(auto const& modelem : module) {
if (mElements[modelem]->isSpareGate()) {
STORM_LOG_THROW(!secondSpare, storm::exceptions::NotSupportedException, "Module for '" << spareReprs->name() << "' contains more than one spare.");
secondSpare = true;
for(size_t modelem : module) {
if (spareReprs->id() != modelem && (isRepresentative(modelem) || (!firstChild && mTopLevelIndex == modelem))) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Module for '" << spareReprs->name() << "' contains more than one representative.");
} }
if(mElements[modelem]->isSpareGate() || mElements[modelem]->isBasicElement()) { if(mElements[modelem]->isSpareGate() || mElements[modelem]->isBasicElement()) {
sparesAndBes.push_back(modelem); sparesAndBes.push_back(modelem);
@ -44,7 +42,7 @@ namespace storm {
} }
} }
mSpareModules.insert(std::make_pair(spareReprs->id(), sparesAndBes)); mSpareModules.insert(std::make_pair(spareReprs->id(), sparesAndBes));
firstChild = false;
} }
std::static_pointer_cast<DFTSpare<ValueType>>(elem)->setUseIndex(stateIndex); std::static_pointer_cast<DFTSpare<ValueType>>(elem)->setUseIndex(stateIndex);
mUsageIndex.insert(std::make_pair(elem->id(), stateIndex)); mUsageIndex.insert(std::make_pair(elem->id(), stateIndex));
@ -71,8 +69,8 @@ namespace storm {
} }
mTopModule = std::vector<size_t>(topModuleSet.begin(), topModuleSet.end()); mTopModule = std::vector<size_t>(topModuleSet.begin(), topModuleSet.end());
mStateSize = stateIndex;
mTopLevelIndex = tle->id();
mStateVectorSize = stateIndex;
}
} }

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

@ -53,7 +53,7 @@ namespace storm {
size_t mNrOfSpares; size_t mNrOfSpares;
size_t mTopLevelIndex; size_t mTopLevelIndex;
size_t mUsageInfoBits; size_t mUsageInfoBits;
size_t mStateSize;
size_t mStateVectorSize;
std::map<size_t, size_t> mActivationIndex; std::map<size_t, size_t> mActivationIndex;
std::map<size_t, std::vector<size_t>> mSpareModules; std::map<size_t, std::vector<size_t>> mSpareModules;
std::vector<size_t> mDependencies; std::vector<size_t> mDependencies;
@ -65,8 +65,8 @@ namespace storm {
public: public:
DFT(DFTElementVector const& elements, DFTElementPointer const& tle); DFT(DFTElementVector const& elements, DFTElementPointer const& tle);
size_t stateSize() const {
return mStateSize;
size_t stateVectorSize() const {
return mStateVectorSize;
} }
size_t nrElements() const { size_t nrElements() const {
@ -199,6 +199,15 @@ namespace storm {
return elements; return elements;
} }
bool isRepresentative(size_t id) const {
for (auto const& parent : getElement(id)->parents()) {
if (parent->isSpareGate()) {
return true;
}
}
return false;
}
bool hasRepresentant(size_t id) const { bool hasRepresentant(size_t id) const {
return mRepresentants.find(id) != mRepresentants.end(); return mRepresentants.find(id) != mRepresentants.end();
} }

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

@ -6,13 +6,12 @@ namespace storm {
namespace storage { namespace storage {
template<typename ValueType> template<typename ValueType>
DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, size_t id) : mStatus(dft.stateSize()), mId(id), mDft(dft) {
DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft) {
mInactiveSpares = dft.getSpareIndices(); mInactiveSpares = dft.getSpareIndices();
dft.initializeUses(*this); dft.initializeUses(*this);
dft.initializeActivation(*this); dft.initializeActivation(*this);
std::vector<size_t> alwaysActiveBEs = dft.nonColdBEs(); std::vector<size_t> alwaysActiveBEs = dft.nonColdBEs();
mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end()); mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end());
} }
template<typename ValueType> template<typename ValueType>

Write Preview
Loading…
Cancel
Save