diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index d2db73a6a..69c317a21 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -426,9 +426,15 @@ namespace storm { storm::expressions::Variable FormulaParserGrammar::createQuantileBoundVariables(boost::optional const& dir, std::string const& variableName) { STORM_LOG_ASSERT(manager, "Mutable expression manager required to define quantile bound variable."); - STORM_LOG_THROW(!manager->hasVariable(variableName), storm::exceptions::WrongFormatException, "Invalid quantile variable name '" << variableName << "' in property: variable already exists."); + storm::expressions::Variable var; + if (manager->hasVariable(variableName)) { + var = manager->getVariable(variableName); + STORM_LOG_THROW(quantileFormulaVariables.count(var) > 0, storm::exceptions::WrongFormatException, "Invalid quantile variable name '" << variableName << "' in quantile formula: variable already exists."); + } else { + var = manager->declareRationalVariable(variableName); + quantileFormulaVariables.insert(var); + } STORM_LOG_WARN_COND(!dir.is_initialized(), "Optimization direction '" << dir.get() << "' for quantile variable " << variableName << " is ignored. This information will be derived from the subformula of the quantile."); - storm::expressions::Variable var = manager->declareRationalVariable(variableName); addIdentifierExpression(variableName, var); return var; } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 7f2bbf33c..64a38e4c1 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -245,6 +245,7 @@ namespace storm { uint64_t propertyCount; std::set undefinedConstants; + std::set quantileFormulaVariables; }; } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp index f4fd31d85..fefc20299 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp @@ -95,7 +95,19 @@ namespace storm { } return contains(infinityProjection); } - + + bool CostLimitClosure::empty() const { + return generator.empty(); + } + + bool CostLimitClosure::full() const { + CostLimits p(dimension(), CostLimit(0)); + for (auto const& dim : downwardDimensions) { + p[dim] = CostLimit::infinity(); + } + return contains(p); + } + bool CostLimitClosure::dominates(CostLimits const& lhs, CostLimits const& rhs) const { for (uint64_t i = 0; i < lhs.size(); ++i) { if (downwardDimensions.get(i)) { diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.h b/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.h index 579a33b5b..06abb4722 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.h +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.h @@ -38,6 +38,8 @@ namespace storm { bool contains(CostLimits const& costLimits) const; bool containsUpwardClosure(CostLimits const& costLimits) const; bool dominates(CostLimits const& lhs, CostLimits const& rhs) const; + bool empty() const; // True if there is no point in this + bool full() const; // True if all points lie in this. std::vector getDominatingCostLimits(CostLimits const& costLimits) const; GeneratorType const& getGenerator() const; uint64_t dimension() const; diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp index eefd43d95..c6bdda24e 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp @@ -21,6 +21,7 @@ #include "storm/logic/BoundedUntilFormula.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/UnexpectedException.h" namespace storm { namespace modelchecker { @@ -61,10 +62,6 @@ namespace storm { STORM_LOG_THROW(quantileVariables.count(boundVariable) == 1, storm::exceptions::NotSupportedException, "The formula contains undefined constant '" << boundExpression << "'."); } } - - // TODO - // Multiple quantile formulas in the same file yield constants def clash - // Test cases } enum class BoundTransformation { @@ -188,6 +185,7 @@ namespace storm { std::vector> QuantileHelper::computeQuantile(Environment const& env) { numCheckedEpochs = 0; numPrecisionRefinements = 0; + swEpochAnalysis.reset(); cachedSubQueryResults.clear(); std::vector> result; @@ -219,6 +217,7 @@ namespace storm { if (storm::settings::getModule().isShowStatisticsSet()) { std::cout << "Number of checked epochs: " << numCheckedEpochs << std::endl; std::cout << "Number of required precision refinements: " << numPrecisionRefinements << std::endl; + std::cout << "Time for epoch model analysis: " << swEpochAnalysis << " seconds." << std::endl; } return result; } @@ -302,30 +301,26 @@ namespace storm { } } - bool getNextCandidateCostLimit(CostLimit const& maxCostLimit, CostLimits& current) { - if (maxCostLimit.get() == 0) { + bool getNextCandidateCostLimit(CostLimit const& candidateCostLimitSum, CostLimits& current) { + if (current.size() == 0) { return false; } - storm::storage::BitVector nonMaxEntries = storm::utility::vector::filter(current, [&maxCostLimit] (CostLimit const& value) -> bool { return value < maxCostLimit; }); - bool allZero = true; - for (auto const& entry : nonMaxEntries) { - if (current[entry].get() > 0) { - --current[entry].get(); - allZero = false; - break; - } else { - current[entry] = CostLimit(maxCostLimit.get() - 1); - } + uint64_t iSum = current.front().get(); + if (iSum == candidateCostLimitSum.get()) { + return false; } - if (allZero) { - nonMaxEntries.increment(); - if (nonMaxEntries.full()) { - return false; + for (uint64_t i = 1; i < current.size(); ++i) { + iSum += current[i].get(); + if (iSum == candidateCostLimitSum.get()) { + ++current[i-1].get(); + uint64_t newVal = current[i].get() - 1; + current[i].get() = 0; + current.back().get() = newVal; + return true; } - current = CostLimits(current.size(), maxCostLimit); - storm::utility::vector::setVectorValues(current, nonMaxEntries, CostLimit(maxCostLimit.get() - 1)); } - return true; + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The entries of the current cost limit candidate do not sum up to the current candidate sum."); + return false; } bool translateEpochToCostLimits(EpochManager::Epoch const& epoch, EpochManager::Epoch const& startEpoch,storm::storage::BitVector const& consideredDimensions, storm::storage::BitVector const& lowerBoundedDimensions, EpochManager const& epochManager, CostLimits& epochAsCostLimits) { @@ -367,10 +362,14 @@ namespace storm { std::set checkedEpochs; bool progress = true; - for (CostLimit currentMaxCostLimit(0); progress; ++currentMaxCostLimit.get()) { - CostLimits currentCandidate(satCostLimits.dimension(), currentMaxCostLimit); - // We can only stop the exploration, if the upward closure of the point in the 'top right corner' is contained in the (un)satCostlLimits. - progress = !satCostLimits.containsUpwardClosure(currentCandidate) && !unsatCostLimits.containsUpwardClosure(currentCandidate); + for (CostLimit candidateCostLimitSum(0); progress; ++candidateCostLimitSum.get()) { + CostLimits currentCandidate(satCostLimits.dimension(), CostLimit(0)); + if (!currentCandidate.empty()) { + currentCandidate.back() = candidateCostLimitSum; + } + // We can still have progress if one of the closures is empty and the other is not full. + // This ensures that we do not terminate too early in case that the (un)satCostLimits are initially non-empty. + progress = (satCostLimits.empty() && !unsatCostLimits.full()) || (unsatCostLimits.empty() && !satCostLimits.full()); do { if (!satCostLimits.contains(currentCandidate) && !unsatCostLimits.contains(currentCandidate)) { progress = true; @@ -389,13 +388,16 @@ namespace storm { } ++costLimitIt; } + STORM_LOG_DEBUG("Checking start epoch " << rewardUnfolding.getEpochManager().toString(startEpoch) << "."); auto epochSequence = rewardUnfolding.getEpochComputationOrder(startEpoch); for (auto const& epoch : epochSequence) { if (checkedEpochs.count(epoch) == 0) { + ++numCheckedEpochs; + swEpochAnalysis.start(); checkedEpochs.insert(epoch); auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(env,boundedUntilOperator.getOptimalityType(), x, b, minMaxSolver, lowerBound, upperBound)); - ++numCheckedEpochs; + swEpochAnalysis.stop(); CostLimits epochAsCostLimits; if (translateEpochToCostLimits(epoch, startEpoch, consideredDimensions, lowerBoundedDimensions, rewardUnfolding.getEpochManager(), epochAsCostLimits)) { @@ -421,7 +423,7 @@ namespace storm { } } } - } while (getNextCandidateCostLimit(currentMaxCostLimit, currentCandidate)); + } while (getNextCandidateCostLimit(candidateCostLimitSum, currentCandidate)); } return true; } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h index e3bb5fd78..63a06e34e 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h @@ -8,6 +8,7 @@ #include "storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.h" #include "storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h" #include "storm/storage/BitVector.h" +#include "storm/utility/Stopwatch.h" namespace storm { class Environment; @@ -51,6 +52,7 @@ namespace storm { /// Statistics mutable uint64_t numCheckedEpochs; mutable uint64_t numPrecisionRefinements; + mutable storm::utility::Stopwatch swEpochAnalysis; }; } }