diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/EpochManager.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/EpochManager.cpp index 4431e00e4..8a196627c 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/EpochManager.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/EpochManager.cpp @@ -28,6 +28,15 @@ namespace storm { } } + typename EpochManager::Epoch EpochManager::getBottomEpoch() const { + return relevantBitsMask; + } + + typename EpochManager::Epoch EpochManager::getZeroEpoch() const { + return 0; + } + + uint64_t const& EpochManager::getDimensionCount() const { STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); return dimensionCount; @@ -50,13 +59,14 @@ namespace storm { typename EpochManager::EpochClass EpochManager::getEpochClass(Epoch const& epoch) const { STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); EpochClass result = 0; - uint64_t mask = dimensionBitMask; + uint64_t dimensionMask = dimensionBitMask; + uint64_t classMask = 1; for (uint64_t d = 0; d < dimensionCount; ++d) { - if ((epoch & mask) == mask) { - ++result; + if ((epoch & dimensionMask) == dimensionMask) { + result |= classMask; } - result = result << 1; - mask = mask << bitsPerDimension; + classMask = classMask << 1; + dimensionMask = dimensionMask << bitsPerDimension; } return result; } @@ -151,6 +161,16 @@ namespace storm { } return false; } + + bool EpochManager::hasBottomDimensionEpochClass(EpochClass const& epochClass) const { + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); + uint64_t mask = (1 << dimensionCount) - 1; + return (epochClass & mask) != 0; + } + + bool EpochManager::isPredecessorEpochClass(EpochClass const& epochClass1, EpochClass const& epochClass2) const { + return (epochClass1 & epochClass2) == epochClass1; + } void EpochManager::setBottomDimension(Epoch& epoch, uint64_t const& dimension) const { STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); @@ -169,6 +189,11 @@ namespace storm { return (epoch | (dimensionBitMask << (dimension * bitsPerDimension))) == epoch; } + bool EpochManager::isBottomDimensionEpochClass(EpochClass const& epochClass, uint64_t const& dimension) const { + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); + return (epochClass | (1 << dimension)) == epochClass; + } + uint64_t EpochManager::getDimensionOfEpoch(Epoch const& epoch, uint64_t const& dimension) const { STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); return (epoch >> (dimension * bitsPerDimension)) & dimensionBitMask; @@ -190,32 +215,9 @@ namespace storm { // Return true iff epoch 1 has to be computed before epoch 2 - // Check whether the number of bottom dimensions is not equal - uint64_t e1Count = 0; - uint64_t e2Count = 0; - for (uint64_t dim = 0; dim < dimensionCount; ++dim) { - if (isBottomDimension(epoch1, dim)) { - ++e1Count; - } - if (isBottomDimension(epoch2, dim)) { - ++e2Count; - } - } - if (e1Count > e2Count) { - return true; - } else if (e1Count < e2Count) { - return false; - } - - // Check the epoch classes - EpochClass e1Class = getEpochClass(epoch1); - uint64_t e2Class = getEpochClass(epoch2); - if (e1Class < e2Class) { - return true; - } else if (e1Class > e2Class) { - return false; + if (!compareEpochClass(epoch1, epoch2)) { + return epochClassOrder(getEpochClass(epoch1), getEpochClass(epoch2)); } - assert(compareEpochClass(epoch1, epoch2)); // check whether the sum of dimensions is the same uint64_t e1Sum = 0; @@ -265,6 +267,34 @@ namespace storm { return false; } + + bool EpochManager::epochClassOrder(EpochClass const& epochClass1, EpochClass const& epochClass2) const { + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); + + if (epochClass1 == epochClass2) { + return false; + } + + // Return true iff epochClass 1 is a successor class of epochClass 2 + + // Check whether the number of bottom dimensions is not equal + int64_t count; + EpochClass ec = epochClass1; + for (count = 0; ec; ++count) { + ec &= ec - 1; + } + ec = epochClass2; + for (; ec; --count) { + ec &= ec - 1; + } + if (count > 0) { + return true; + } else if (count < 0) { + return false; + } + + return epochClass1 < epochClass2; + } } } } \ No newline at end of file diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/EpochManager.h b/src/storm/modelchecker/multiobjective/rewardbounded/EpochManager.h index c0fe6694d..e168e1877 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/EpochManager.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/EpochManager.h @@ -20,6 +20,9 @@ namespace storm { uint64_t const& getDimensionCount() const; + Epoch getBottomEpoch() const; + Epoch getZeroEpoch() const; + bool compareEpochClass(Epoch const& epoch1, Epoch const& epoch2) const; EpochClass getEpochClass(Epoch const& epoch) const; @@ -30,6 +33,8 @@ namespace storm { bool isZeroEpoch(Epoch const& epoch) const; bool isBottomEpoch(Epoch const& epoch) const; bool hasBottomDimension(Epoch const& epoch) const; + bool hasBottomDimensionEpochClass(EpochClass const& epochClass) const; + bool isPredecessorEpochClass(EpochClass const& epochClass1, EpochClass const& epochClass2) const; bool isValidDimensionValue(uint64_t const& value) const; @@ -37,11 +42,13 @@ namespace storm { void setDimensionOfEpoch(Epoch& epoch, uint64_t const& dimension, uint64_t const& value) const; // assumes that the value is valid, i.e., small enough bool isBottomDimension(Epoch const& epoch, uint64_t const& dimension) const; + bool isBottomDimensionEpochClass(EpochClass const& epochClass, uint64_t const& dimension) const; uint64_t getDimensionOfEpoch(Epoch const& epoch, uint64_t const& dimension) const; // assumes that the dimension is not bottom std::string toString(Epoch const& epoch) const; bool epochClassZigZagOrder(Epoch const& epoch1, Epoch const& epoch2) const; + bool epochClassOrder(EpochClass const& epochClass1, EpochClass const& epochClass2) const; private: