From 4ac23d630ffbc6faff71a34a691596a8b5b08873 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 31 Jan 2019 11:53:05 +0100 Subject: [PATCH] quantiles: Added support for formulas with trivial bounds (i.e., >=0). --- .../prctl/helper/rewardbounded/Dimension.h | 4 ++-- .../prctl/helper/rewardbounded/EpochModel.cpp | 8 ++++---- .../MultiDimensionalRewardUnfolding.cpp | 18 ++++++++---------- .../helper/rewardbounded/ProductModel.cpp | 14 ++++++++------ src/storm/transformer/EndComponentEliminator.h | 2 +- 5 files changed, 23 insertions(+), 23 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/Dimension.h b/src/storm/modelchecker/prctl/helper/rewardbounded/Dimension.h index 256225616..34a3bef29 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/Dimension.h +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/Dimension.h @@ -21,8 +21,8 @@ namespace storm { /// A label that indicates the states where this dimension is still relevant (i.e., it is yet unknown whether the corresponding objective holds) boost::optional memoryLabel; - /// True iff the objective is not bounded at all (i.e., it has lower bound >= 0) - bool isNotBounded; + /// True iff the objective is bounded with either an upper bound or a lower bound which is not >= 0 + bool isBounded; /// True iff the objective is upper bounded, false if it has a lower bound or no bound at all. bool isUpperBounded; diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp index 37c39e691..e8b059f32 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp @@ -238,10 +238,10 @@ namespace storm { } } - template class EpochModel; - template class EpochModel; - template class EpochModel; - template class EpochModel; + template struct EpochModel; + template struct EpochModel; + template struct EpochModel; + template struct EpochModel; } } } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp index c31e64c80..902128890 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -95,11 +95,11 @@ namespace storm { if ((!subformula.hasLowerBound(dim) && !subformula.hasUpperBound(dim)) || (subformula.hasLowerBound(dim) && !subformula.isLowerBoundStrict(dim) && !subformula.getLowerBound(dim).containsVariables() && storm::utility::isZero(subformula.getLowerBound(dim).evaluateAsRational()))) { dimensionWiseEpochSteps.push_back(std::vector(model.getTransitionMatrix().getRowCount(), 0)); dimension.scalingFactor = storm::utility::zero(); - dimension.isNotBounded = true; + dimension.isBounded = false; } else if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) { dimensionWiseEpochSteps.push_back(std::vector(model.getTransitionMatrix().getRowCount(), 1)); dimension.scalingFactor = storm::utility::one(); - dimension.isNotBounded = false; + dimension.isBounded = true; } else { STORM_LOG_ASSERT(subformula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound."); std::string const& rewardName = subformula.getTimeBoundReference(dim).getRewardName(); @@ -110,7 +110,7 @@ namespace storm { auto discretizedRewardsAndFactor = storm::utility::vector::toIntegralVector(actionRewards); dimensionWiseEpochSteps.push_back(std::move(discretizedRewardsAndFactor.first)); dimension.scalingFactor = std::move(discretizedRewardsAndFactor.second); - dimension.isNotBounded = false; + dimension.isBounded = true; } dimensions.emplace_back(std::move(dimension)); } @@ -121,7 +121,7 @@ namespace storm { dimension.formula = subformula.restrictToDimension(dim); dimension.objectiveIndex = objIndex; dimension.isUpperBounded = true; - dimension.isNotBounded = false; + dimension.isBounded = true; if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) { dimensionWiseEpochSteps.push_back(std::vector(model.getTransitionMatrix().getRowCount(), 1)); dimension.scalingFactor = storm::utility::one(); @@ -229,7 +229,7 @@ namespace storm { ValueType discretizedBound = storm::utility::convertNumber(bound.evaluateAsRational()); // We always consider upper bounds to be non-strict and lower bounds to be strict. // Thus, >=N would become >N-1. However, note that the case N=0 needs extra treatment - if (!dimensions[dim].isNotBounded) { + if (dimensions[dim].isBounded) { discretizedBound /= dimensions[dim].scalingFactor; if (storm::utility::isInteger(discretizedBound)) { if (isStrict == dimensions[dim].isUpperBounded) { @@ -250,11 +250,11 @@ namespace storm { typename MultiDimensionalRewardUnfolding::Epoch MultiDimensionalRewardUnfolding::getStartEpoch() { Epoch startEpoch = epochManager.getZeroEpoch(); for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { - if (dimensions[dim].isNotBounded) { - epochManager.setBottomDimension(startEpoch, dim); - } else { + if (dimensions[dim].isBounded) { STORM_LOG_ASSERT(dimensions[dim].maxValue, "No max-value for dimension " << dim << " was given."); epochManager.setDimensionOfEpoch(startEpoch, dim, dimensions[dim].maxValue.get()); + } else { + epochManager.setBottomDimension(startEpoch, dim); } } STORM_LOG_TRACE("Start epoch is " << epochManager.toString(startEpoch)); @@ -745,7 +745,6 @@ namespace storm { } predecessorEpochs.erase(currentEpoch.get()); successorEpochs.erase(currentEpoch.get()); - STORM_LOG_ASSERT(!predecessorEpochs.empty(), "There are no predecessors for the epoch " << epochManager.toString(currentEpoch.get())); // clean up solutions that are not needed anymore for (auto const& successorEpoch : successorEpochs) { @@ -794,7 +793,6 @@ namespace storm { template typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getInitialStateResult(Epoch const& epoch) { STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "The model has multiple initial states."); - STORM_LOG_ASSERT(!epochManager.hasBottomDimension(epoch), "Tried to get the initial state result in an epoch that still contains at least one bottom dimension."); return getStateSolution(epoch, productModel->getInitialProductState(*model.getInitialStates().begin(), model.getInitialStates())); } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp index bc886afcd..5072082ee 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp @@ -460,11 +460,11 @@ namespace storm { Epoch startEpoch = epochManager.getZeroEpoch(); for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { - if (dimensions[dim].isNotBounded) { - epochManager.setBottomDimension(startEpoch, dim); - } else { + if (dimensions[dim].isBounded) { STORM_LOG_ASSERT(dimensions[dim].maxValue, "No max-value for dimension " << dim << " was given."); epochManager.setDimensionOfEpoch(startEpoch, dim, dimensions[dim].maxValue.get()); + } else { + epochManager.setBottomDimension(startEpoch, dim); } } @@ -491,22 +491,24 @@ namespace storm { void ProductModel::computeReachableStates(EpochClass const& epochClass, std::vector const& predecessors) { storm::storage::BitVector bottomDimensions(epochManager.getDimensionCount(), false); + bool considerInitialStates = true; for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { if (epochManager.isBottomDimensionEpochClass(epochClass, dim)) { bottomDimensions.set(dim, true); + if (dimensions[dim].isBounded) { + considerInitialStates = false; + } } } storm::storage::BitVector nonBottomDimensions = ~bottomDimensions; storm::storage::BitVector ecInStates(getProduct().getNumberOfStates(), false); - - if (!epochManager.hasBottomDimensionEpochClass(epochClass)) { + if (considerInitialStates) { for (auto const& initState : getProduct().getInitialStates()) { uint64_t transformedInitState = transformProductState(initState, epochClass, memoryStateManager.getInitialMemoryState()); ecInStates.set(transformedInitState, true); } } - for (auto const& predecessor : predecessors) { storm::storage::BitVector positiveStepDimensions(epochManager.getDimensionCount(), false); for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { diff --git a/src/storm/transformer/EndComponentEliminator.h b/src/storm/transformer/EndComponentEliminator.h index d2489eadc..c522e1987 100644 --- a/src/storm/transformer/EndComponentEliminator.h +++ b/src/storm/transformer/EndComponentEliminator.h @@ -53,7 +53,7 @@ namespace storm { keptStates.set(stateActionsPair.first, false); } } - STORM_LOG_DEBUG("Found " << ecs.size() << " end components to eliminate. Keeping " << keptStates.getNumberOfSetBits() << " of " << keptStates.size() << " original states."); + STORM_LOG_DEBUG("Found " << ecs.size() << " end components to eliminate. Keeping " << keptStates.getNumberOfSetBits() << " of " << keptStates.size() << " original states plus " << ecs.size() << "new end component states."); EndComponentEliminatorReturnType result; std::vector newRowGroupIndices;