From 2e01c8b137ad0afe41722194797139eb6b0f43d5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 12 Apr 2017 16:45:08 +0200 Subject: [PATCH] Fixed time bounds containing constant variables for multi objective formulas. --- .../multiobjective/pcaa/PcaaObjective.h | 12 ++- .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 92 +++++++------------ .../pcaa/SparseMaPcaaWeightVectorChecker.h | 8 +- .../pcaa/SparseMdpPcaaWeightVectorChecker.cpp | 53 +++++------ .../pcaa/SparsePcaaPreprocessor.cpp | 29 ++---- 5 files changed, 71 insertions(+), 123 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h b/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h index 84f04ec62..ac0043fae 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h +++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h @@ -32,8 +32,10 @@ namespace storm { bool thresholdIsStrict = false; // The time bound(s) for the formula (if given by the originalFormula) - boost::optional lowerTimeBound; - boost::optional upperTimeBound; + boost::optional lowerTimeBound; + boost::optional upperTimeBound; + bool lowerTimeBoundStrict = false; + bool upperTimeBoundStrict = false; void printToStream(std::ostream& out) const { out << std::setw(30) << originalFormula->toString(); @@ -51,12 +53,12 @@ namespace storm { out << "time bounds:"; if(lowerTimeBound) { if(upperTimeBound) { - out << "[" << *lowerTimeBound << ", " << *upperTimeBound << "]"; + out << (lowerTimeBoundStrict ? "(" : "[") << *lowerTimeBound << ", " << *upperTimeBound << (upperTimeBoundStrict ? ")" : "]"); } else { - out << ">=" << std::setw(5) << *lowerTimeBound; + out << (lowerTimeBoundStrict ? " >" : ">=") << std::setw(5) << *lowerTimeBound; } } else if (upperTimeBound) { - out << "<=" << std::setw(5) << *upperTimeBound; + out << (upperTimeBoundStrict ? " <" : "<=") << std::setw(5) << *upperTimeBound; } else { out << " none"; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index df2864b34..8ae1c8498 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -9,6 +9,7 @@ #include "storm/utility/vector.h" #include "storm/exceptions/InvalidOperationException.h" +#include "storm/exceptions/InvalidPropertyException.h" namespace storm { namespace modelchecker { @@ -48,9 +49,8 @@ namespace storm { digitize(MS, digitizationConstant); // Get for each occurring (digitized) timeBound the indices of the objectives with that bound. - TimeBoundMap lowerTimeBounds; TimeBoundMap upperTimeBounds; - digitizeTimeBounds(lowerTimeBounds, upperTimeBounds, digitizationConstant); + digitizeTimeBounds(upperTimeBounds, digitizationConstant); // Initialize a minMaxSolver to compute an optimal scheduler (w.r.t. PS) for each epoch // No EC elimination is necessary as we assume non-zenoness @@ -66,12 +66,11 @@ namespace storm { // Stores the objectives for which we need to compute values in the current time epoch. storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound; - auto lowerTimeBoundIt = lowerTimeBounds.begin(); auto upperTimeBoundIt = upperTimeBounds.begin(); - uint_fast64_t currentEpoch = std::max(lowerTimeBounds.empty() ? 0 : lowerTimeBoundIt->first, upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first); - while(true) { + uint_fast64_t currentEpoch = upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first; + while (true) { // Update the objectives that are considered at the current time epoch as well as the (weighted) reward vectors. - updateDataToCurrentEpoch(MS, PS, *minMax, consideredObjectives, currentEpoch, weightVector, lowerTimeBoundIt, lowerTimeBounds, upperTimeBoundIt, upperTimeBounds); + updateDataToCurrentEpoch(MS, PS, *minMax, consideredObjectives, currentEpoch, weightVector, upperTimeBoundIt, upperTimeBounds); // Compute the values that can be obtained at probabilistic states in the current time epoch performPSStep(PS, MS, *minMax, *linEq, optimalChoicesAtCurrentEpoch, consideredObjectives, weightVector); @@ -156,20 +155,19 @@ namespace storm { // Initialize some data for fast and easy access VT const maxRate = this->model.getMaximalExitRate(); - std::vector> eToPowerOfMinusMaxRateTimesBound; + std::vector timeBounds; + std::vector eToPowerOfMinusMaxRateTimesBound; VT smallestNonZeroBound = storm::utility::zero(); for(auto const& obj : this->objectives) { - eToPowerOfMinusMaxRateTimesBound.emplace_back(); - if(obj.lowerTimeBound){ - STORM_LOG_ASSERT(!storm::utility::isZero(*obj.lowerTimeBound), "Got zero-valued lower bound."); // should have been handled in preprocessing - STORM_LOG_ASSERT(!obj.upperTimeBound || *obj.lowerTimeBound < *obj.upperTimeBound, "Got point intervall or empty intervall on time bounded property which is not supported"); // should also have been handled in preprocessing - eToPowerOfMinusMaxRateTimesBound.back().first = std::exp(-maxRate * (*obj.lowerTimeBound)); - smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? *obj.lowerTimeBound : std::min(smallestNonZeroBound, *obj.lowerTimeBound); - } if(obj.upperTimeBound){ - STORM_LOG_ASSERT(!storm::utility::isZero(*obj.upperTimeBound), "Got zero-valued upper bound."); // should have been handled in preprocessing - eToPowerOfMinusMaxRateTimesBound.back().second = std::exp(-maxRate * (*obj.upperTimeBound)); - smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? *obj.upperTimeBound : std::min(smallestNonZeroBound, *obj.upperTimeBound); + STORM_LOG_THROW(!obj.upperTimeBound->containsVariables(), storm::exceptions::InvalidOperationException, "The time bound '" << *obj.upperTimeBound << " contains undefined variables"); + timeBounds.push_back(storm::utility::convertNumber(obj.upperTimeBound->evaluateAsRational())); + STORM_LOG_ASSERT(!storm::utility::isZero(timeBounds.back()), "Got zero-valued upper time bound."); + eToPowerOfMinusMaxRateTimesBound.push_back(std::exp(-maxRate * timeBounds.back())); + smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? timeBounds.back() : std::min(smallestNonZeroBound, timeBounds.back()); + } else { + timeBounds.push_back(storm::utility::zero()); + eToPowerOfMinusMaxRateTimesBound.push_back(storm::utility::zero()); } } if(storm::utility::isZero(smallestNonZeroBound)) { @@ -181,13 +179,14 @@ namespace storm { // We brute-force a delta, since a direct computation is apparently not easy. // Also note that the number of times this loop runs is a lower bound for the number of minMaxSolver invocations. // Hence, this brute-force approach will most likely not be a bottleneck. + storm::storage::BitVector objectivesWithTimeBound = ~this->objectivesWithNoUpperTimeBound; uint_fast64_t smallestStepBound = 1; VT delta = smallestNonZeroBound / smallestStepBound; while(true) { bool deltaValid = true; - for(auto const& obj : this->objectives) { - if((obj.lowerTimeBound && *obj.lowerTimeBound/delta != std::floor(*obj.lowerTimeBound/delta)) || - (obj.upperTimeBound && *obj.upperTimeBound/delta != std::floor(*obj.upperTimeBound/delta))) { + for(auto const& objIndex : objectivesWithTimeBound) { + auto const& timeBound = timeBounds[objIndex]; + if(timeBound/delta != std::floor(timeBound/delta)) { deltaValid = false; break; } @@ -195,14 +194,9 @@ namespace storm { if(deltaValid) { VT weightedPrecisionForCurrentDelta = storm::utility::zero(); for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - auto const& obj = this->objectives[objIndex]; VT precisionOfObj = storm::utility::zero(); - if(obj.lowerTimeBound) { - precisionOfObj += storm::utility::one() - (eToPowerOfMinusMaxRateTimesBound[objIndex].first * storm::utility::pow(storm::utility::one() + maxRate * delta, *obj.lowerTimeBound / delta) ) - + storm::utility::one() - std::exp(-maxRate * delta); - } - if(obj.upperTimeBound) { - precisionOfObj += storm::utility::one() - (eToPowerOfMinusMaxRateTimesBound[objIndex].second * storm::utility::pow(storm::utility::one() + maxRate * delta, *obj.upperTimeBound / delta) ); + if (objectivesWithTimeBound.get(objIndex)) { + precisionOfObj += storm::utility::one() - (eToPowerOfMinusMaxRateTimesBound[objIndex] * storm::utility::pow(storm::utility::one() + maxRate * delta, timeBounds[objIndex] / delta) ); } weightedPrecisionForCurrentDelta += weightVector[objIndex] * precisionOfObj; } @@ -256,31 +250,21 @@ namespace storm { template template ::SupportsExponential, int>::type> - void SparseMaPcaaWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { + void SparseMaPcaaWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { VT const maxRate = this->model.getMaximalExitRate(); for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { auto const& obj = this->objectives[objIndex]; - VT errorTowardsZero; - VT errorAwayFromZero; - if(obj.lowerTimeBound) { - uint_fast64_t digitizedBound = storm::utility::convertNumber((*obj.lowerTimeBound)/digitizationConstant); - auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->objectives.size(), false))).first; - timeBoundIt->second.set(objIndex); - VT digitizationError = storm::utility::one(); - digitizationError -= std::exp(-maxRate * (*obj.lowerTimeBound)) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); - errorTowardsZero = -digitizationError; - errorAwayFromZero = storm::utility::one() - std::exp(-maxRate * digitizationConstant);; - } else { - errorTowardsZero = storm::utility::zero(); - errorAwayFromZero = storm::utility::zero(); - } + STORM_LOG_THROW(!obj.lowerTimeBound, storm::exceptions::InvalidPropertyException, "Lower time bounds are not supported by this model checker"); + VT errorTowardsZero = storm::utility::zero(); + VT errorAwayFromZero = storm::utility::zero(); if(obj.upperTimeBound) { - uint_fast64_t digitizedBound = storm::utility::convertNumber((*obj.upperTimeBound)/digitizationConstant); + VT timeBound = storm::utility::convertNumber(obj.upperTimeBound->evaluateAsRational()); + uint_fast64_t digitizedBound = storm::utility::convertNumber(timeBound/digitizationConstant); auto timeBoundIt = upperTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->objectives.size(), false))).first; timeBoundIt->second.set(objIndex); VT digitizationError = storm::utility::one(); - digitizationError -= std::exp(-maxRate * (*obj.upperTimeBound)) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); + digitizationError -= std::exp(-maxRate * timeBound) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); errorAwayFromZero += digitizationError; } if (obj.rewardsArePositive) { @@ -295,7 +279,7 @@ namespace storm { template template ::SupportsExponential, int>::type> - void SparseMaPcaaWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { + void SparseMaPcaaWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type."); } @@ -324,19 +308,7 @@ namespace storm { } template - void SparseMaPcaaWeightVectorChecker::updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& lowerTimeBoundIt, TimeBoundMap const& lowerTimeBounds, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds) { - - //Note that lower time bounds are always strict. Hence, we need to react when the current epoch equals the stored bound. - if(lowerTimeBoundIt != lowerTimeBounds.end() && currentEpoch == lowerTimeBoundIt->first) { - for(auto objIndex : lowerTimeBoundIt->second) { - // No more reward is earned for this objective. - storm::utility::vector::addScaledVector(MS.weightedRewardVector, MS.objectiveRewardVectors[objIndex], -weightVector[objIndex]); - storm::utility::vector::addScaledVector(PS.weightedRewardVector, PS.objectiveRewardVectors[objIndex], -weightVector[objIndex]); - MS.objectiveRewardVectors[objIndex] = std::vector(MS.objectiveRewardVectors[objIndex].size(), storm::utility::zero()); - PS.objectiveRewardVectors[objIndex] = std::vector(PS.objectiveRewardVectors[objIndex].size(), storm::utility::zero()); - } - ++lowerTimeBoundIt; - } + void SparseMaPcaaWeightVectorChecker::updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds) { if(upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) { consideredObjectives |= upperTimeBoundIt->second; @@ -420,12 +392,12 @@ namespace storm { template class SparseMaPcaaWeightVectorChecker>; template double SparseMaPcaaWeightVectorChecker>::getDigitizationConstant(std::vector const& direction) const; template void SparseMaPcaaWeightVectorChecker>::digitize(SparseMaPcaaWeightVectorChecker>::SubModel& subModel, double const& digitizationConstant) const; - template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds(SparseMaPcaaWeightVectorChecker>::TimeBoundMap& lowerTimeBounds, SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, double const& digitizationConstant); + template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds( SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, double const& digitizationConstant); #ifdef STORM_HAVE_CARL // template class SparseMaPcaaWeightVectorChecker>; // template storm::RationalNumber SparseMaPcaaWeightVectorChecker>::getDigitizationConstant(std::vector const& direction) const; // template void SparseMaPcaaWeightVectorChecker>::digitize(SparseMaPcaaWeightVectorChecker>::SubModel& subModel, storm::RationalNumber const& digitizationConstant) const; -// template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds(SparseMaPcaaWeightVectorChecker>::TimeBoundMap& lowerTimeBounds, SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, storm::RationalNumber const& digitizationConstant); +// template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds(SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, storm::RationalNumber const& digitizationConstant); #endif } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h index a757ccf0a..1ac363c4d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h @@ -105,13 +105,13 @@ namespace storm { void digitize(SubModel& subModel, VT const& digitizationConstant) const; /* - * Fills the given maps with the digitized time bounds. Also sets the offsetsToLowerBound / offsetsToUpperBound values + * Fills the given map with the digitized time bounds. Also sets the offsetsToLowerBound / offsetsToUpperBound values * according to the digitization error */ template ::SupportsExponential, int>::type = 0> - void digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant); + void digitizeTimeBounds(TimeBoundMap& upperTimeBounds, VT const& digitizationConstant); template ::SupportsExponential, int>::type = 0> - void digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant); + void digitizeTimeBounds(TimeBoundMap& upperTimeBounds, VT const& digitizationConstant); /*! @@ -129,7 +129,7 @@ namespace storm { * the reward vector of the reduced PStoPS model, and * objectives that are considered at the current time epoch. */ - void updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& lowerTimeBoundIt, TimeBoundMap const& lowerTimeBounds, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds); + void updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds); /* * Performs a step for the probabilistic states, that is diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp index cb5c92e34..a6dc7a3b4 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp @@ -5,6 +5,7 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" +#include "storm/exceptions/InvalidPropertyException.h" namespace storm { @@ -19,7 +20,7 @@ namespace storm { storm::storage::BitVector const& possiblyRecurrentStates) : SparsePcaaWeightVectorChecker(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates) { // set the state action rewards - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { typename SparseMdpModelType::RewardModelType const& rewModel = this->model.getRewardModel(this->objectives[objIndex].rewardModelName); STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Reward model has transition rewards which is not expected."); this->discreteActionRewards[objIndex] = rewModel.getTotalRewardVector(this->model.getTransitionMatrix()); @@ -34,19 +35,18 @@ namespace storm { std::vector temporaryResult(this->model.getNumberOfStates()); std::vector zeroReward(weightedRewardVector.size(), storm::utility::zero()); // Get for each occurring timeBound the indices of the objectives with that bound. - std::map> lowerTimeBounds; - std::map> upperTimeBounds; - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + std::map> stepBounds; + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { auto const& obj = this->objectives[objIndex]; - if(obj.lowerTimeBound) { - auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(storm::utility::convertNumber(*obj.lowerTimeBound), storm::storage::BitVector(this->objectives.size(), false))).first; - STORM_LOG_WARN_COND(storm::utility::convertNumber(timeBoundIt->first) == (*obj.lowerTimeBound), "Rounded non-integral bound " << *obj.lowerTimeBound << " to " << timeBoundIt->first << "."); - timeBoundIt->second.set(objIndex); - } - if(obj.upperTimeBound) { - auto timeBoundIt = upperTimeBounds.insert(std::make_pair(storm::utility::convertNumber(*obj.upperTimeBound), storm::storage::BitVector(this->objectives.size(), false))).first; - STORM_LOG_WARN_COND(storm::utility::convertNumber(timeBoundIt->first) == (*obj.upperTimeBound), "Rounded non-integral bound " << *obj.upperTimeBound << " to " << timeBoundIt->first << "."); - timeBoundIt->second.set(objIndex); + STORM_LOG_THROW(!obj.lowerTimeBound, storm::exceptions::InvalidPropertyException, "Lower step bounds are not supported by this model checker"); + if (obj.upperTimeBound) { + STORM_LOG_THROW(!obj.upperTimeBound->containsVariables(), storm::exceptions::InvalidPropertyException, "The step bound '" << * obj.upperTimeBound << " contains undefined variables"); + uint_fast64_t stepBound = (uint_fast64_t) obj.upperTimeBound->evaluateAsInt(); + if (obj.upperTimeBoundStrict) { + --stepBound; + } + auto stepBoundIt = stepBounds.insert(std::make_pair(stepBound, storm::storage::BitVector(this->objectives.size(), false))).first; + stepBoundIt->second.set(objIndex); // There is no error for the values of these objectives. this->offsetsToLowerBound[objIndex] = storm::utility::zero(); @@ -60,29 +60,18 @@ namespace storm { // Stores objectives for which the current epoch passed their lower bound storm::storage::BitVector lowerBoundViolatedObjectives(consideredObjectives.size(), false); - auto lowerTimeBoundIt = lowerTimeBounds.begin(); - auto upperTimeBoundIt = upperTimeBounds.begin(); - uint_fast64_t currentEpoch = std::max(lowerTimeBounds.empty() ? 0 : lowerTimeBoundIt->first - 1, upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first); // consider lowerBound - 1 since we are interested in the first epoch that passes the bound + auto stepBoundIt = stepBounds.begin(); + uint_fast64_t currentEpoch = stepBounds.empty() ? 0 : stepBoundIt->first; - while(currentEpoch > 0) { - //For lower time bounds we need to react when the currentEpoch passed the bound - // Hence, we substract 1 from the lower time bounds. - if(lowerTimeBoundIt != lowerTimeBounds.end() && currentEpoch == lowerTimeBoundIt->first - 1) { - lowerBoundViolatedObjectives |= lowerTimeBoundIt->second; - for(auto objIndex : lowerTimeBoundIt->second) { - // No more reward is earned for this objective. - storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], -weightVector[objIndex]); - } - ++lowerTimeBoundIt; - } + while (currentEpoch > 0) { - if(upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) { - consideredObjectives |= upperTimeBoundIt->second; - for(auto objIndex : upperTimeBoundIt->second) { + if (stepBoundIt != stepBounds.end() && currentEpoch == stepBoundIt->first) { + consideredObjectives |= stepBoundIt->second; + for(auto objIndex : stepBoundIt->second) { // This objective now plays a role in the weighted sum storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], weightVector[objIndex]); } - ++upperTimeBoundIt; + ++stepBoundIt; } // Get values and scheduler for weighted sum of objectives @@ -92,7 +81,7 @@ namespace storm { // get values for individual objectives // TODO we could compute the result for one of the objectives from the weighted result, the given weight vector, and the remaining objective results. - for(auto objIndex : consideredObjectives) { + for (auto objIndex : consideredObjectives) { std::vector& objectiveResult = this->objectiveResults[objIndex]; std::vector const& objectiveRewards = lowerBoundViolatedObjectives.get(objIndex) ? zeroReward : this->discreteActionRewards[objIndex]; auto rowGroupIndexIt = this->model.getTransitionMatrix().getRowGroupIndices().begin(); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp index 36f4a961b..9e5474362 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp @@ -228,30 +228,16 @@ namespace storm { template void SparsePcaaPreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support step-bounded properties for Markov automata."); + STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); if (formula.hasLowerBound()) { - STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::Mdp) || formula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Expected discrete lower time-bound in formula."); - // FIXME: really convert formula bound to value type? - if (formula.hasIntegerLowerBound()) { - currentObjective.lowerTimeBound = storm::utility::convertNumber(formula.getLowerBound()); - } else { - currentObjective.lowerTimeBound = storm::utility::convertNumber(formula.getLowerBound()); - } + currentObjective.lowerTimeBound = formula.getLowerBound(); + currentObjective.lowerTimeBoundStrict = formula.isLowerBoundStrict(); } if (formula.hasUpperBound()) { - STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::Mdp) || formula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Expected discrete lower time-bound in formula."); - // FIXME: really convert formula bound to value type? - if (formula.hasIntegerUpperBound()) { - currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getUpperBound()); - } else { - currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getUpperBound()); - } - } else { - currentObjective.upperTimeBound = storm::utility::infinity(); + currentObjective.upperTimeBound = formula.getUpperBound(); + currentObjective.upperTimeBoundStrict = formula.isUpperBoundStrict(); } - STORM_LOG_THROW(currentObjective.lowerTimeBound < currentObjective.upperTimeBound, storm::exceptions::InvalidPropertyException, "Empty or point time intervals are currently not supported by multi-objective model checking."); - preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), result, currentObjective); } @@ -318,9 +304,8 @@ namespace storm { template void SparsePcaaPreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); - STORM_LOG_THROW(formula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << "."); - // FIXME: really convert to value type? - currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getBound()); + currentObjective.upperTimeBound = formula.getBound(); + currentObjective.upperTimeBoundStrict = formula.isBoundStrict(); RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false);