From defcd7d5d72a6649ecbf786a5ae1569bfbd384c6 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 19 Jul 2017 11:42:06 +0200 Subject: [PATCH] Multi-objective model checking: adapted data structures to allow more general objectives --- .../modelchecker/multiobjective/Objective.h | 48 +---- .../SparseMultiObjectivePreprocessor.cpp | 196 +++++++++--------- .../SparseMultiObjectivePreprocessor.h | 19 +- .../SparseMultiObjectivePreprocessorTask.h | 16 +- .../SparseCbAchievabilityQuery.cpp | 56 +++-- .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 96 ++++----- .../pcaa/SparseMdpPcaaWeightVectorChecker.cpp | 31 ++- .../pcaa/SparsePcaaAchievabilityQuery.cpp | 15 +- .../pcaa/SparsePcaaQuantitativeQuery.cpp | 22 +- .../multiobjective/pcaa/SparsePcaaQuery.cpp | 6 +- .../pcaa/SparsePcaaWeightVectorChecker.cpp | 39 ++-- 11 files changed, 260 insertions(+), 284 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/Objective.h b/src/storm/modelchecker/multiobjective/Objective.h index d5d269775..6b1f44f1f 100644 --- a/src/storm/modelchecker/multiobjective/Objective.h +++ b/src/storm/modelchecker/multiobjective/Objective.h @@ -13,57 +13,27 @@ namespace storm { namespace multiobjective { template struct Objective { + // the original input formula std::shared_ptr originalFormula; - // the name of the considered reward model in the preprocessedModel - boost::optional rewardModelName; + // The preprocessed (simplified) formula + std::shared_ptr formula; // True iff the complementary event is considered. // E.g. if we consider P<1-t [F !"safe"] instead of P>=t [ G "safe"] bool considersComplementaryEvent; - // The probability/reward threshold for the preprocessed model (if originalFormula specifies one). - boost::optional bound; - // The optimization direction for the preprocessed model - // if originalFormula does ot specifies one, the direction is derived from the bound. - storm::solver::OptimizationDirection optimizationDirection; - - // Lower and upper time/step/reward bouds - boost::optional lowerTimeBound, upperTimeBound; - boost::optional timeBoundReference; - + // Limitations for the quantitative objective value (e.g. 0 <= value <= 1 for probabilities). + // Can be used to guide the underlying solver boost::optional lowerResultBound, upperResultBound; void printToStream(std::ostream& out) const { - out << originalFormula->toString(); - out << " \t"; - out << "direction: "; - out << optimizationDirection; - out << " \t"; - out << "intern bound: "; - if (bound){ - out << *bound; - } else { - out << " -none- "; - } + out << "Original: " << *originalFormula; out << " \t"; - out << "time bounds: "; - if (lowerTimeBound && upperTimeBound) { - out << (lowerTimeBound->isStrict() ? "(" : "[") << lowerTimeBound->getBound() << "," << upperTimeBound->getBound() << (upperTimeBound->isStrict() ? ")" : "]"); - } else if (lowerTimeBound) { - out << (lowerTimeBound->isStrict() ? ">" : ">=") << lowerTimeBound->getBound(); - } else if (upperTimeBound) { - out << (upperTimeBound->isStrict() ? "<" : "<=") << upperTimeBound->getBound(); - } else { - out << " -none- "; - } - out << " \t"; - out << "intern reward model: "; - if (rewardModelName) { - out << *rewardModelName; - } else { - out << " -none- "; + out << "Preprocessed: " << *formula; + if (considersComplementaryEvent) { + out << " (Complementary event)"; } out << " \t"; out << "result bounds: "; diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index 09f0fdc6a..7d359a5ab 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -113,80 +113,81 @@ namespace storm { Objective& objective = *data.objectives.back(); - objective.considersComplementaryEvent = false; + // Check whether the complementary event is considered + objective.considersComplementaryEvent = formula.isProbabilityOperatorFormula() && formula.getSubformula().isGloballyFormula(); + storm::logic::OperatorInformation opInfo; if (formula.hasBound()) { - STORM_LOG_THROW(!formula.getBound().threshold.containsVariables(), storm::exceptions::InvalidPropertyException, "The formula " << formula << "considers a non-constant threshold"); - objective.bound = formula.getBound(); - if (storm::logic::isLowerBound(formula.getBound().comparisonType)) { - objective.optimizationDirection = storm::solver::OptimizationDirection::Maximize; - } else { - objective.optimizationDirection = storm::solver::OptimizationDirection::Minimize; - } - STORM_LOG_WARN_COND(!formula.hasOptimalityType() || formula.getOptimalityType() == objective.optimizationDirection, "Optimization direction of formula " << formula << " ignored as the formula also specifies a threshold."); - } else if (formula.hasOptimalityType()){ - objective.optimizationDirection = formula.getOptimalityType(); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize"); - } - - if (formula.isProbabilityOperatorFormula()){ - preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), data); - } else if (formula.isRewardOperatorFormula()){ - preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), data); - } else if (formula.isTimeOperatorFormula()){ - preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), data); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported"); - } - - // Invert the bound and optimization direction (if necessary) - if (objective.considersComplementaryEvent) { - if (objective.bound) { - objective.bound->threshold = objective.bound->threshold.getManager().rational(storm::utility::one()) - objective.bound->threshold; - switch (objective.bound->comparisonType) { + opInfo.bound = formula.getBound(); + // Invert the bound (if necessary) + if (objective.considersComplementaryEvent) { + opInfo.bound->threshold = opInfo.bound->threshold.getManager().rational(storm::utility::one()) - opInfo.bound->threshold; + switch (opInfo.bound->comparisonType) { case storm::logic::ComparisonType::Greater: - objective.bound->comparisonType = storm::logic::ComparisonType::Less; + opInfo.bound->comparisonType = storm::logic::ComparisonType::Less; break; case storm::logic::ComparisonType::GreaterEqual: - objective.bound->comparisonType = storm::logic::ComparisonType::LessEqual; + opInfo.bound->comparisonType = storm::logic::ComparisonType::LessEqual; break; case storm::logic::ComparisonType::Less: - objective.bound->comparisonType = storm::logic::ComparisonType::Greater; + opInfo.bound->comparisonType = storm::logic::ComparisonType::Greater; break; case storm::logic::ComparisonType::LessEqual: - objective.bound->comparisonType = storm::logic::ComparisonType::GreaterEqual; + opInfo.bound->comparisonType = storm::logic::ComparisonType::GreaterEqual; break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " has unexpected comparison type"); } } - objective.optimizationDirection = storm::solver::invert(objective.optimizationDirection); + if (storm::logic::isLowerBound(opInfo.bound->comparisonType)) { + opInfo.optimalityType = storm::solver::OptimizationDirection::Maximize; + } else { + opInfo.optimalityType = storm::solver::OptimizationDirection::Minimize; + } + STORM_LOG_WARN_COND(!formula.hasOptimalityType(), "Optimization direction of formula " << formula << " ignored as the formula also specifies a threshold."); + } else if (formula.hasOptimalityType()){ + opInfo.optimalityType = formula.getOptimalityType(); + // Invert the optimality type (if necessary) + if (objective.considersComplementaryEvent) { + opInfo.optimalityType = storm::solver::invert(opInfo.optimalityType.get()); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Objective " << formula << " does not specify whether to minimize or maximize"); + } + + if (formula.isProbabilityOperatorFormula()){ + preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), opInfo, data); + } else if (formula.isRewardOperatorFormula()){ + preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), opInfo, data); + } else if (formula.isTimeOperatorFormula()){ + preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), opInfo, data); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported"); } } template - void SparseMultiObjectivePreprocessor::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data) { + void SparseMultiObjectivePreprocessor::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { // Probabilities are between zero and one data.objectives.back()->lowerResultBound = storm::utility::zero(); data.objectives.back()->upperResultBound = storm::utility::one(); if (formula.getSubformula().isUntilFormula()){ - preprocessUntilFormula(formula.getSubformula().asUntilFormula(), data); + preprocessUntilFormula(formula.getSubformula().asUntilFormula(), opInfo, data); } else if (formula.getSubformula().isBoundedUntilFormula()){ - preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), data); + preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), opInfo, data); } else if (formula.getSubformula().isGloballyFormula()){ - preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), data); + preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), opInfo, data); } else if (formula.getSubformula().isEventuallyFormula()){ - preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data); + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), opInfo, data); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); } } template - void SparseMultiObjectivePreprocessor::preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data) { + void SparseMultiObjectivePreprocessor::preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { STORM_LOG_THROW((formula.hasRewardModelName() && data.originalModel.hasRewardModel(formula.getRewardModelName())) || (!formula.hasRewardModelName() && data.originalModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model is not unique or the formula " << formula << " does not specify an existing reward model."); @@ -203,43 +204,39 @@ namespace storm { data.objectives.back()->lowerResultBound = storm::utility::zero(); if (formula.getSubformula().isEventuallyFormula()){ - preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data, rewardModelName); + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), opInfo, data, rewardModelName); } else if (formula.getSubformula().isCumulativeRewardFormula()) { - preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), data, rewardModelName); + preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), opInfo, data, rewardModelName); } else if (formula.getSubformula().isTotalRewardFormula()) { - preprocessTotalRewardFormula(data, rewardModelName); + preprocessTotalRewardFormula(opInfo, data, rewardModelName); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); } } template - void SparseMultiObjectivePreprocessor::preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data) { + void SparseMultiObjectivePreprocessor::preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { // Time formulas are only supported for Markov automata STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata."); data.objectives.back()->lowerResultBound = storm::utility::zero(); if (formula.getSubformula().isEventuallyFormula()){ - preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data); + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), opInfo, data); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); } } template - void SparseMultiObjectivePreprocessor::preprocessUntilFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data) { + void SparseMultiObjectivePreprocessor::preprocessUntilFormula(storm::logic::UntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, std::shared_ptr subformula) { storm::modelchecker::SparsePropositionalModelChecker mc(data.originalModel); storm::storage::BitVector rightSubformulaResult = mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector leftSubformulaResult = mc.check(formula.getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); // Check if the formula is already satisfied in the initial state because then the transformation to expected rewards will fail. - if (!data.objectives.back()->lowerTimeBound) { - if (!(data.originalModel.getInitialStates() & rightSubformulaResult).empty()) { - // TODO: Handle this case more properly - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The Probability for the objective " << *data.objectives.back()->originalFormula << " is always one as the rhs of the until formula is true in the initial state. This (trivial) case is currently not implemented."); - } - } + // TODO: Handle this case more properly + STORM_LOG_THROW((data.originalModel.getInitialStates() & rightSubformulaResult).empty(), storm::exceptions::NotImplementedException, "The Probability for the objective " << *data.objectives.back()->originalFormula << " is always one as the rhs of the until formula is true in the initial state. This (trivial) case is currently not implemented."); // Create a memory structure that stores whether a non-PhiState or a PsiState has already been reached storm::storage::MemoryStructureBuilder builder(2, data.originalModel); @@ -255,7 +252,11 @@ namespace storm { storm::storage::MemoryStructure objectiveMemory = builder.build(); data.memory = std::make_shared(data.memory->product(objectiveMemory)); - data.objectives.back()->rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + if (subformula == nullptr) { + subformula = std::make_shared(); + } + data.objectives.back()->formula = std::make_shared(subformula, rewardModelName, opInfo); auto relevantStatesFormula = std::make_shared(relevantStatesLabel); data.tasks.push_back(std::make_shared>(data.objectives.back(), relevantStatesFormula, formula.getRightSubformula().asSharedPointer())); @@ -263,38 +264,37 @@ namespace storm { } template - void SparseMultiObjectivePreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data) { - if (formula.hasLowerBound()) { - STORM_LOG_THROW(!formula.getLowerBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The lower time bound for the formula " << formula << " still contains variables"); - if (!storm::utility::isZero(formula.getLowerBound()) || formula.isLowerBoundStrict()) { - data.objectives.back()->lowerTimeBound = storm::logic::TimeBound(formula.isLowerBoundStrict(), formula.getLowerBound()); - } - } - if (formula.hasUpperBound()) { - STORM_LOG_THROW(!formula.getUpperBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The Upper time bound for the formula " << formula << " still contains variables"); - if (!storm::utility::isInfinity(formula.getUpperBound())) { - data.objectives.back()->upperTimeBound = storm::logic::TimeBound(formula.isUpperBoundStrict(), formula.getUpperBound()); + void SparseMultiObjectivePreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { + + // Check how to handle this query + if (!formula.getTimeBoundReference().isRewardBound() && (!formula.hasLowerBound() || (!formula.isLowerBoundStrict() && storm::utility::isZero(formula.template getLowerBound())))) { + std::shared_ptr subformula; + if (!formula.hasUpperBound()) { + // The formula is actually unbounded + subformula = std::make_shared(); + } else { + STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || formula.getTimeBoundReference().isTimeBound(), storm::exceptions::InvalidPropertyException, "Bounded until formulas for Markov Automata are only allowed when time bounds are considered."); + storm::logic::TimeBound bound(formula.isUpperBoundStrict(), formula.getUpperBound()); + subformula = std::make_shared(bound, formula.getTimeBoundReference().getType()); } + preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), opInfo, data, subformula); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Property " << formula << "is not supported"); } - - data.objectives.back()->timeBoundReference = formula.getTimeBoundReference(); - preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data); } template - void SparseMultiObjectivePreprocessor::preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data) { - // The formula will be transformed to an until formula for the complementary event. - data.objectives.back()->considersComplementaryEvent = true; - + void SparseMultiObjectivePreprocessor::preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { + // The formula is transformed to an until formula for the complementary event. auto negatedSubformula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()); - preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), data); + preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), opInfo, data); } template - void SparseMultiObjectivePreprocessor::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, boost::optional const& optionalRewardModelName) { + void SparseMultiObjectivePreprocessor::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName) { if (formula.isReachabilityProbabilityFormula()){ - preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), data); + preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), opInfo, data); return; } @@ -318,7 +318,9 @@ namespace storm { auto relevantStatesFormula = std::make_shared(relevantStatesLabel); - data.objectives.back()->rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + std::string auxRewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + auto totalRewardFormula = std::make_shared(); + data.objectives.back()->formula = std::make_shared(totalRewardFormula, auxRewardModelName, opInfo); data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); if (formula.isReachabilityRewardFormula()) { @@ -334,23 +336,19 @@ namespace storm { } template - void SparseMultiObjectivePreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, boost::optional const& optionalRewardModelName) { + void SparseMultiObjectivePreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName) { STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); - STORM_LOG_THROW(!formula.getBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The time bound for the formula " << formula << " still contains variables"); - if (!storm::utility::isInfinity(formula.getBound())) { - data.objectives.back()->upperTimeBound = storm::logic::TimeBound(formula.isBoundStrict(), formula.getBound()); - } - - assert(optionalRewardModelName.is_initialized()); - data.objectives.back()->rewardModelName = *optionalRewardModelName; - + storm::logic::TimeBound bound(formula.isBoundStrict(), formula.getBound()); + auto cumulativeRewardFormula = std::make_shared(bound, storm::logic::TimeBoundType::Steps); + data.objectives.back()->formula = std::make_shared(cumulativeRewardFormula, *optionalRewardModelName, opInfo); } template - void SparseMultiObjectivePreprocessor::preprocessTotalRewardFormula(PreprocessorData& data, boost::optional const& optionalRewardModelName) { - assert(optionalRewardModelName.is_initialized()); - data.objectives.back()->rewardModelName = *optionalRewardModelName; + void SparseMultiObjectivePreprocessor::preprocessTotalRewardFormula(storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName) { + + auto totalRewardFormula = std::make_shared(); + data.objectives.back()->formula = std::make_shared(totalRewardFormula, *optionalRewardModelName, opInfo); data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); } @@ -372,9 +370,10 @@ namespace storm { std::set relevantRewardModels; for (auto const& obj : result.objectives) { - relevantRewardModels.insert(*obj.rewardModelName); - if (obj.timeBoundReference && obj.timeBoundReference->isRewardBound()) { - relevantRewardModels.insert(obj.timeBoundReference->getRewardName()); + if (obj.formula->isRewardOperatorFormula()) { + relevantRewardModels.insert(obj.formula->asRewardOperatorFormula().getRewardModelName()); + } else { + STORM_LOG_ASSERT(false, "Unknown formula type."); } } @@ -407,7 +406,7 @@ namespace storm { typename SparseMultiObjectivePreprocessor::ReturnType::QueryType SparseMultiObjectivePreprocessor::getQueryType(std::vector> const& objectives) { uint_fast64_t numOfObjectivesWithThreshold = 0; for (auto& obj : objectives) { - if (obj.bound) { + if (obj.formula->hasBound()) { ++numOfObjectivesWithThreshold; } } @@ -434,8 +433,12 @@ namespace storm { // Get the choices that yield non-zero reward storm::storage::BitVector zeroRewardChoices(result.preprocessedModel->getNumberOfChoices(), true); for (auto const& obj : result.objectives) { - auto const& rewModel = result.preprocessedModel->getRewardModel(*obj.rewardModelName); - zeroRewardChoices &= rewModel.getChoicesWithZeroReward(transitions); + if (obj.formula->isRewardOperatorFormula()) { + auto const& rewModel = result.preprocessedModel->getRewardModel(obj.formula->asRewardOperatorFormula().getRewardModelName()); + zeroRewardChoices &= rewModel.getChoicesWithZeroReward(transitions); + } else { + STORM_LOG_ASSERT(false, "Unknown formula type."); + } } // Get the states that have reward for at least one (or for all) choices assigned to it. @@ -476,8 +479,9 @@ namespace storm { storm::storage::BitVector maxRewardsToCheck(result.preprocessedModel->getNumberOfChoices(), true); bool hasMinRewardToCheck = false; for (auto const& objIndex : finiteRewardCheckObjectives) { - auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].rewardModelName.get()); - if (storm::solver::minimize(result.objectives[objIndex].optimizationDirection)) { + STORM_LOG_ASSERT(result.objectives[objIndex].formula->isRewardOperatorFormula(), "Objective needs to be checked for finite reward but has no reward operator."); + auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName()); + if (storm::solver::minimize(result.objectives[objIndex].formula->getOptimalityType())) { hasMinRewardToCheck = true; } else { maxRewardsToCheck &= rewModel.getChoicesWithZeroReward(transitions); diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h index 318433575..505431e62 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h @@ -50,19 +50,20 @@ namespace storm { /*! * Apply the neccessary preprocessing for the given formula. * @param formula the current (sub)formula + * @param opInfo the information of the resulting operator formula * @param data the current data. The currently processed objective is located at data.objectives.back() * @param optionalRewardModelName the reward model name that is considered for the formula (if available) */ static void preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data); - static void preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data); - static void preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data); - static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data); - static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data); - static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data); - static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data); - static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); - static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); - static void preprocessTotalRewardFormula(PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique. + static void preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); + static void preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); + static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); + static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, std::shared_ptr subformula = nullptr); + static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); + static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); + static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); + static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); + static void preprocessTotalRewardFormula(storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique. /*! diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h index e34e37584..f84b935b6 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h @@ -58,8 +58,9 @@ namespace storm { objectiveRewards[row] = preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, goalStates); } } - STORM_LOG_ASSERT(this->objective->rewardModelName.is_initialized(), "No reward model name has been specified"); - preprocessedModel.addRewardModel(this->objective->rewardModelName.get(), typename SparseModelType::RewardModelType(boost::none, std::move(objectiveRewards))); + STORM_LOG_ASSERT(this->objective->formula->isRewardOperatorFormula(), "No reward operator formula."); + STORM_LOG_ASSERT(this->objective->formula->asRewardOperatorFormula().hasRewardModelName(), "No reward model name has been specified"); + preprocessedModel.addRewardModel(this->objective->formula->asRewardOperatorFormula().getRewardModelName(), typename SparseModelType::RewardModelType(boost::none, std::move(objectiveRewards))); } private: @@ -91,8 +92,9 @@ namespace storm { std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state], preprocessedModel.getTransitionMatrix().getRowGroupSize(state), storm::utility::zero()); } } - STORM_LOG_ASSERT(this->objective->rewardModelName.is_initialized(), "No reward model name has been specified"); - preprocessedModel.addRewardModel(this->objective->rewardModelName.get(), std::move(objectiveRewards)); + STORM_LOG_ASSERT(this->objective->formula->isRewardOperatorFormula(), "No reward operator formula."); + STORM_LOG_ASSERT(this->objective->formula->asRewardOperatorFormula().hasRewardModelName(), "No reward model name has been specified"); + preprocessedModel.addRewardModel(this->objective->formula->asRewardOperatorFormula().getRewardModelName(), std::move(objectiveRewards)); } private: @@ -117,8 +119,10 @@ namespace storm { std::vector timeRewards(preprocessedModel.getNumberOfStates(), storm::utility::zero()); storm::utility::vector::setVectorValues(timeRewards, dynamic_cast const&>(preprocessedModel).getMarkovianStates() & relevantStates, storm::utility::one()); - STORM_LOG_ASSERT(this->objective->rewardModelName.is_initialized(), "No reward model name has been specified"); - preprocessedModel.addRewardModel(this->objective->rewardModelName.get(), typename SparseModelType::RewardModelType(std::move(timeRewards))); + + STORM_LOG_ASSERT(this->objective->formula->isRewardOperatorFormula(), "No reward operator formula."); + STORM_LOG_ASSERT(this->objective->formula->asRewardOperatorFormula().hasRewardModelName(), "No reward model name has been specified"); + preprocessedModel.addRewardModel(this->objective->formula->asRewardOperatorFormula().getRewardModelName(), typename SparseModelType::RewardModelType(std::move(timeRewards))); } private: diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp index 86faf88a7..628fbb687 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp @@ -26,7 +26,7 @@ namespace storm { template SparseCbAchievabilityQuery::SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : SparseCbQuery(preprocessorResult) { - STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorReturnType::QueryType::Achievability, "Invalid query Type"); + STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorReturnType::QueryType::Achievability, "Invalid query Type"); solver = storm::utility::solver::SmtSolverFactory().create(*this->expressionManager); } @@ -134,36 +134,34 @@ namespace storm { void SparseCbAchievabilityQuery::addObjectiveConstraints() { storm::expressions::Expression zero = this->expressionManager->rational(storm::utility::zero()); for (Objective const& obj : this->objectives) { - if (obj.rewardModelName) { - STORM_LOG_THROW(obj.bound, storm::exceptions::InvalidOperationException, "Invoked achievability query but no bound was specified for at least one objective."); - STORM_LOG_THROW(!obj.lowerTimeBound && !obj.upperTimeBound, storm::exceptions::NotSupportedException, "Constraint based method currently does not support step bounds"); - std::vector rewards = getActionBasedExpectedRewards(*obj.rewardModelName); - storm::expressions::Expression objValue = zero; - for (uint_fast64_t choice = 0; choice < rewards.size(); ++choice) { - if (!storm::utility::isZero(rewards[choice])) { - objValue = objValue + (this->expressionManager->rational(rewards[choice]) * expectedChoiceVariables[choice].getExpression()); - } - } - // We need to actually evaluate the threshold as rational number. Otherwise a threshold like '<=16/9' might be considered as 1 due to integer division - STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "The threshold for one objective still contains undefined variables"); - storm::expressions::Expression threshold = this->expressionManager->rational(obj.bound->threshold.evaluateAsRational()); - switch (obj.bound->comparisonType) { - case storm::logic::ComparisonType::Greater: - solver->add( objValue > threshold); - break; - case storm::logic::ComparisonType::GreaterEqual: - solver->add( objValue >= threshold); - break; - case storm::logic::ComparisonType::Less: - solver->add( objValue < threshold); - break; - case storm::logic::ComparisonType::LessEqual: - solver->add( objValue <= threshold); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "One or more objectives have an invalid comparison type"); + STORM_LOG_THROW(obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isTotalRewardFormula(), storm::exceptions::InvalidOperationException, "Constraint-based solver only supports total-reward objectives. Got " << *obj.formula << " instead."); + STORM_LOG_THROW(obj.formula->hasBound(), storm::exceptions::InvalidOperationException, "Invoked achievability query but no bound was specified for at least one objective."); + STORM_LOG_THROW(obj.formula->asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::InvalidOperationException, "Expected reward operator with a reward model name. Got " << *obj.formula << " instead."); + std::vector rewards = getActionBasedExpectedRewards(obj.formula->asRewardOperatorFormula().getRewardModelName()); + storm::expressions::Expression objValue = zero; + for (uint_fast64_t choice = 0; choice < rewards.size(); ++choice) { + if (!storm::utility::isZero(rewards[choice])) { + objValue = objValue + (this->expressionManager->rational(rewards[choice]) * expectedChoiceVariables[choice].getExpression()); } } + // We need to actually evaluate the threshold as rational number. Otherwise a threshold like '<=16/9' might be considered as 1 due to integer division + storm::expressions::Expression threshold = this->expressionManager->rational(obj.formula->getThreshold().evaluateAsRational()); + switch (obj.formula->getBound().comparisonType) { + case storm::logic::ComparisonType::Greater: + solver->add( objValue > threshold); + break; + case storm::logic::ComparisonType::GreaterEqual: + solver->add( objValue >= threshold); + break; + case storm::logic::ComparisonType::Less: + solver->add( objValue < threshold); + break; + case storm::logic::ComparisonType::LessEqual: + solver->add( objValue <= threshold); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "One or more objectives have an invalid comparison type"); + } } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index e65aa6325..e695fa8db 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -8,9 +8,11 @@ #include "storm/utility/macros.h" #include "storm/utility/vector.h" #include "storm/solver/GmmxxLinearEquationSolver.h" +#include "storm/logic/Formulas.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/UnexpectedException.h" namespace storm { namespace modelchecker { @@ -25,13 +27,17 @@ namespace storm { SparsePcaaWeightVectorChecker(model, objectives, possibleECActions, possibleBottomStates) { // Set the (discretized) state action rewards. this->discreteActionRewards.resize(objectives.size()); - for(auto objIndex : this->objectivesWithNoUpperTimeBound) { - typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName); + for (auto objIndex : this->objectivesWithNoUpperTimeBound) { + auto const& formula = *objectives[objIndex].formula; + STORM_LOG_THROW(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::UnexpectedException, "Unexpected type of operator formula: " << formula); + STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula() || (formula.getSubformula().isCumulativeRewardFormula() && formula.getSubformula().asCumulativeRewardFormula().isTimeBounded()), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula()); + STORM_LOG_WARN_COND(!formula.getSubformula().isCumulativeRewardFormula() || (objectives[objIndex].originalFormula->isProbabilityOperatorFormula() && objectives[objIndex].originalFormula->asProbabilityOperatorFormula().getSubformula().isBoundedUntilFormula()), "Objective " << objectives[objIndex].originalFormula << " was simplified to a cumulative reward formula. Correctness of the algorithm is unknown for this type of property."); + typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()); STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); this->discreteActionRewards[objIndex] = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector(this->model.getTransitionMatrix().getRowCount(), storm::utility::zero()); - if(rewModel.hasStateRewards()) { + if (rewModel.hasStateRewards()) { // Note that state rewards are earned over time and thus play no role for probabilistic states - for(auto markovianState : this->model.getMarkovianStates()) { + for (auto markovianState : this->model.getMarkovianStates()) { this->discreteActionRewards[objIndex][this->model.getTransitionMatrix().getRowGroupIndices()[markovianState]] += rewModel.getStateReward(markovianState) / this->model.getExitRate(markovianState); } } @@ -41,10 +47,6 @@ namespace storm { template void SparseMaPcaaWeightVectorChecker::boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) { - for (auto const& obj : this->objectives) { - STORM_LOG_THROW(!obj.timeBoundReference || obj.timeBoundReference->isTimeBound(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking of Markov automata is only supported for time-bounded formulass."); - } - // Split the preprocessed model into transitions from/to probabilistic/Markovian states. SubModel MS = createSubModel(true, weightedRewardVector); SubModel PS = createSubModel(false, weightedRewardVector); @@ -82,7 +84,7 @@ namespace storm { // Compute values that can be obtained at Markovian states after letting one (digitized) time unit pass. // Only perform such a step if there is time left. - if(currentEpoch>0) { + if (currentEpoch>0) { performMSStep(MS, PS, consideredObjectives, weightVector); --currentEpoch; } else { @@ -93,7 +95,7 @@ namespace storm { // compose the results from MS and PS storm::utility::vector::setVectorValues(this->weightedResult, MS.states, MS.weightedSolutionVector); storm::utility::vector::setVectorValues(this->weightedResult, PS.states, PS.weightedSolutionVector); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { storm::utility::vector::setVectorValues(this->objectiveResults[objIndex], MS.states, MS.objectiveSolutionVectors[objIndex]); storm::utility::vector::setVectorValues(this->objectiveResults[objIndex], PS.states, PS.objectiveSolutionVectors[objIndex]); } @@ -118,16 +120,16 @@ namespace storm { result.weightedRewardVector.resize(result.getNumberOfChoices()); storm::utility::vector::selectVectorValues(result.weightedRewardVector, result.choices, weightedRewardVector); result.objectiveRewardVectors.resize(this->objectives.size()); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { std::vector& objVector = result.objectiveRewardVectors[objIndex]; objVector = std::vector(result.weightedRewardVector.size(), storm::utility::zero()); - if(this->objectivesWithNoUpperTimeBound.get(objIndex)) { + if (this->objectivesWithNoUpperTimeBound.get(objIndex)) { storm::utility::vector::selectVectorValues(objVector, result.choices, this->discreteActionRewards[objIndex]); } else { - typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName); + typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(this->objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName()); STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); STORM_LOG_ASSERT(!rewModel.hasStateRewards(), "State rewards for bounded objectives for MAs are not expected (bounded rewards are not supported)."); - if(rewModel.hasStateActionRewards()) { + if (rewModel.hasStateActionRewards()) { storm::utility::vector::selectVectorValues(objVector, result.choices, rewModel.getStateActionRewardVector()); } } @@ -136,7 +138,7 @@ namespace storm { result.weightedSolutionVector.resize(result.getNumberOfStates()); storm::utility::vector::selectVectorValues(result.weightedSolutionVector, result.states, this->weightedResult); result.objectiveSolutionVectors.resize(this->objectives.size()); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { result.objectiveSolutionVectors[objIndex].resize(result.weightedSolutionVector.size()); storm::utility::vector::selectVectorValues(result.objectiveSolutionVectors[objIndex], result.states, this->objectiveResults[objIndex]); } @@ -163,11 +165,10 @@ namespace storm { std::vector timeBounds; std::vector eToPowerOfMinusMaxRateTimesBound; VT smallestNonZeroBound = storm::utility::zero(); - for(auto const& obj : this->objectives) { - if(obj.upperTimeBound){ - STORM_LOG_THROW(!obj.upperTimeBound->getBound().containsVariables(), storm::exceptions::InvalidOperationException, "The time bound '" << obj.upperTimeBound->getBound() << " contains undefined variables"); - timeBounds.push_back(storm::utility::convertNumber(obj.upperTimeBound->getBound().evaluateAsRational())); - STORM_LOG_ASSERT(!storm::utility::isZero(timeBounds.back()), "Got zero-valued upper time bound."); + for (auto const& obj : this->objectives) { + if (obj.formula->getSubformula().isCumulativeRewardFormula()) { + timeBounds.push_back(obj.formula->getSubformula().asCumulativeRewardFormula().template getBound()); + STORM_LOG_THROW(!storm::utility::isZero(timeBounds.back()), storm::exceptions::InvalidPropertyException, "Got zero-valued upper time bound. This is not suppoted."); eToPowerOfMinusMaxRateTimesBound.push_back(std::exp(-maxRate * timeBounds.back())); smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? timeBounds.back() : std::min(smallestNonZeroBound, timeBounds.back()); } else { @@ -175,7 +176,7 @@ namespace storm { eToPowerOfMinusMaxRateTimesBound.push_back(storm::utility::zero()); } } - if(storm::utility::isZero(smallestNonZeroBound)) { + if (storm::utility::isZero(smallestNonZeroBound)) { // There are no time bounds. In this case, one is a valid digitization constant. return storm::utility::one(); } @@ -189,16 +190,16 @@ namespace storm { VT delta = smallestNonZeroBound / smallestStepBound; while(true) { bool deltaValid = true; - for(auto const& objIndex : objectivesWithTimeBound) { + for (auto const& objIndex : objectivesWithTimeBound) { auto const& timeBound = timeBounds[objIndex]; - if(timeBound/delta != std::floor(timeBound/delta)) { + if (timeBound/delta != std::floor(timeBound/delta)) { deltaValid = false; break; } } - if(deltaValid) { + if (deltaValid) { VT weightedPrecisionForCurrentDelta = storm::utility::zero(); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { VT precisionOfObj = storm::utility::zero(); if (objectivesWithTimeBound.get(objIndex)) { precisionOfObj += storm::utility::one() - (eToPowerOfMinusMaxRateTimesBound[objIndex] * storm::utility::pow(storm::utility::one() + maxRate * delta, timeBounds[objIndex] / delta) ); @@ -207,7 +208,7 @@ namespace storm { } deltaValid &= weightedPrecisionForCurrentDelta <= goalPrecisionTimesNorm; } - if(deltaValid) { + if (deltaValid) { break; } ++smallestStepBound; @@ -229,19 +230,19 @@ namespace storm { void SparseMaPcaaWeightVectorChecker::digitize(SubModel& MS, VT const& digitizationConstant) const { std::vector rateVector(MS.getNumberOfChoices()); storm::utility::vector::selectVectorValues(rateVector, MS.states, this->model.getExitRates()); - for(uint_fast64_t row = 0; row < rateVector.size(); ++row) { + for (uint_fast64_t row = 0; row < rateVector.size(); ++row) { VT const eToMinusRateTimesDelta = std::exp(-rateVector[row] * digitizationConstant); - for(auto& entry : MS.toMS.getRow(row)) { + for (auto& entry : MS.toMS.getRow(row)) { entry.setValue((storm::utility::one() - eToMinusRateTimesDelta) * entry.getValue()); - if(entry.getColumn() == row) { + if (entry.getColumn() == row) { entry.setValue(entry.getValue() + eToMinusRateTimesDelta); } } - for(auto& entry : MS.toPS.getRow(row)) { + for (auto& entry : MS.toPS.getRow(row)) { entry.setValue((storm::utility::one() - eToMinusRateTimesDelta) * entry.getValue()); } MS.weightedRewardVector[row] *= storm::utility::one() - eToMinusRateTimesDelta; - for(auto& objVector : MS.objectiveRewardVectors) { + for (auto& objVector : MS.objectiveRewardVectors) { objVector[row] *= storm::utility::one() - eToMinusRateTimesDelta; } } @@ -258,13 +259,12 @@ namespace storm { 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) { + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { auto const& obj = this->objectives[objIndex]; - 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) { - VT timeBound = storm::utility::convertNumber(obj.upperTimeBound->getBound().evaluateAsRational()); + if (obj.formula->getSubformula().isCumulativeRewardFormula()) { + VT timeBound = obj.formula->getSubformula().asCumulativeRewardFormula().template getBound(); 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); @@ -272,7 +272,7 @@ namespace storm { digitizationError -= std::exp(-maxRate * timeBound) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); errorAwayFromZero += digitizationError; } - if (storm::solver::maximize(obj.optimizationDirection)) { + if (storm::solver::maximize(obj.formula->getOptimalityType())) { this->offsetsToUnderApproximation[objIndex] = -errorTowardsZero; this->offsetsToOverApproximation[objIndex] = errorAwayFromZero; } else { @@ -324,11 +324,11 @@ 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& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds) { - if(upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) { + if (upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) { consideredObjectives |= upperTimeBoundIt->second; - for(auto objIndex : upperTimeBoundIt->second) { + for (auto objIndex : upperTimeBoundIt->second) { // This objective now plays a role in the weighted sum - ValueType factor = storm::solver::minimize(this->objectives[objIndex].optimizationDirection) ? -weightVector[objIndex] : weightVector[objIndex]; + ValueType factor = storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex]; storm::utility::vector::addScaledVector(MS.weightedRewardVector, MS.objectiveRewardVectors[objIndex], factor); storm::utility::vector::addScaledVector(PS.weightedRewardVector, PS.objectiveRewardVectors[objIndex], factor); } @@ -345,16 +345,16 @@ namespace storm { // compute a choice vector for the probabilistic states that is optimal w.r.t. the weighted reward vector minMax.solver->solveEquations(PS.weightedSolutionVector, minMax.b); auto const& newChoices = minMax.solver->getSchedulerChoices(); - if(consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { + if (consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { // In this case there is no need to perform the computation on the individual objectives optimalChoicesAtCurrentEpoch = newChoices; PS.objectiveSolutionVectors[*consideredObjectives.begin()] = PS.weightedSolutionVector; - if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].optimizationDirection)) { + if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].formula->getOptimalityType())) { storm::utility::vector::scaleVectorInPlace(PS.objectiveSolutionVectors[*consideredObjectives.begin()], -storm::utility::one()); } } else { // check whether the linEqSolver needs to be updated, i.e., whether the scheduler has changed - if(linEq.solver == nullptr || newChoices != optimalChoicesAtCurrentEpoch) { + if (linEq.solver == nullptr || newChoices != optimalChoicesAtCurrentEpoch) { optimalChoicesAtCurrentEpoch = newChoices; linEq.solver = nullptr; storm::storage::SparseMatrix linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true); @@ -365,17 +365,17 @@ namespace storm { // Get the results for the individual objectives. // Note that we do not consider an estimate for each objective (as done in the unbounded phase) since the results from the previous epoch are already pretty close - for(auto objIndex : consideredObjectives) { + for (auto objIndex : consideredObjectives) { auto const& objectiveRewardVectorPS = PS.objectiveRewardVectors[objIndex]; auto const& objectiveSolutionVectorMS = MS.objectiveSolutionVectors[objIndex]; // compute rhs of equation system, i.e., PS.toMS * x + Rewards // To safe some time, only do this for the obtained optimal choices auto itGroupIndex = PS.toPS.getRowGroupIndices().begin(); auto itChoiceOffset = optimalChoicesAtCurrentEpoch.begin(); - for(auto& bValue : linEq.b) { + for (auto& bValue : linEq.b) { uint_fast64_t row = (*itGroupIndex) + (*itChoiceOffset); bValue = objectiveRewardVectorPS[row]; - for(auto const& entry : PS.toMS.getRow(row)){ + for (auto const& entry : PS.toMS.getRow(row)){ bValue += entry.getValue() * objectiveSolutionVectorMS[entry.getColumn()]; } ++itGroupIndex; @@ -393,14 +393,14 @@ namespace storm { storm::utility::vector::addVectors(MS.weightedRewardVector, MS.auxChoiceValues, MS.weightedSolutionVector); MS.toPS.multiplyWithVector(PS.weightedSolutionVector, MS.auxChoiceValues); storm::utility::vector::addVectors(MS.weightedSolutionVector, MS.auxChoiceValues, MS.weightedSolutionVector); - if(consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { + if (consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { // In this case there is no need to perform the computation on the individual objectives MS.objectiveSolutionVectors[*consideredObjectives.begin()] = MS.weightedSolutionVector; - if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].optimizationDirection)) { + if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].formula->getOptimalityType())) { storm::utility::vector::scaleVectorInPlace(MS.objectiveSolutionVectors[*consideredObjectives.begin()], -storm::utility::one()); } } else { - for(auto objIndex : consideredObjectives) { + for (auto objIndex : consideredObjectives) { MS.toMS.multiplyWithVector(MS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues); storm::utility::vector::addVectors(MS.objectiveRewardVectors[objIndex], MS.auxChoiceValues, MS.objectiveSolutionVectors[objIndex]); MS.toPS.multiplyWithVector(PS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp index 0916fd94c..0744f1d7d 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/logic/Formulas.h" #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/IllegalArgumentException.h" #include "storm/exceptions/NotSupportedException.h" @@ -21,24 +22,22 @@ namespace storm { storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) : SparsePcaaWeightVectorChecker(model, objectives, possibleECActions, possibleBottomStates) { - // set the state action rewards + // set the state action rewards. Also do some sanity checks on the objectives. 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."); + auto const& formula = *objectives[objIndex].formula; + STORM_LOG_THROW(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::UnexpectedException, "Unexpected type of operator formula: " << formula); + STORM_LOG_THROW(formula.getSubformula().isCumulativeRewardFormula() || formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula()); + typename SparseMdpModelType::RewardModelType const& rewModel = this->model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()); + STORM_LOG_THROW(!rewModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Reward model has transition rewards which is not expected."); this->discreteActionRewards[objIndex] = rewModel.getTotalRewardVector(this->model.getTransitionMatrix()); } } template void SparseMdpPcaaWeightVectorChecker::boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) { - // Check whether reward bounded objectives occur. + // Currently, only step bounds are considered. + // TODO: Check whether reward bounded objectives occur. bool containsRewardBoundedObjectives = false; - for (auto const& obj : this->objectives) { - if (obj.timeBoundReference && obj.timeBoundReference->isRewardBound()) { - containsRewardBoundedObjectives = true; - break; - } - } if (containsRewardBoundedObjectives) { boundedPhaseWithRewardBounds(weightVector, weightedRewardVector); @@ -56,12 +55,10 @@ namespace storm { // Get for each occurring timeBound the indices of the objectives with that bound. std::map> stepBounds; for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - auto const& obj = this->objectives[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->getBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The step bound '" << obj.upperTimeBound->getBound() << " contains undefined variables"); - uint_fast64_t stepBound = (uint_fast64_t) obj.upperTimeBound->getBound().evaluateAsInt(); - if (obj.upperTimeBound->isStrict()) { + if (this->objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula()) { + auto const& subformula = this->objectives[objIndex].formula->getSubformula().asCumulativeRewardFormula(); + uint_fast64_t stepBound = subformula.template getBound(); + if (subformula.isBoundStrict()) { --stepBound; } auto stepBoundIt = stepBounds.insert(std::make_pair(stepBound, storm::storage::BitVector(this->objectives.size(), false))).first; @@ -85,7 +82,7 @@ namespace storm { consideredObjectives |= stepBoundIt->second; for(auto objIndex : stepBoundIt->second) { // This objective now plays a role in the weighted sum - ValueType factor = storm::solver::minimize(this->objectives[objIndex].optimizationDirection) ? -weightVector[objIndex] : weightVector[objIndex]; + ValueType factor = storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex]; storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], factor); } ++stepBoundIt; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp index 74e646103..a1d457c11 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp @@ -31,18 +31,17 @@ namespace storm { void SparsePcaaAchievabilityQuery::initializeThresholdData() { thresholds.reserve(this->objectives.size()); strictThresholds = storm::storage::BitVector(this->objectives.size(), false); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - auto const& obj = this->objectives[objIndex]; - STORM_LOG_ASSERT(obj.bound.is_initialized(), "Achievability query invoked but there is an objective without bound."); - STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "There is an objective whose bound contains undefined variables."); - thresholds.push_back(storm::utility::convertNumber(obj.bound->threshold.evaluateAsRational())); - if (storm::solver::minimize(obj.optimizationDirection)) { - STORM_LOG_ASSERT(!storm::logic::isLowerBound(obj.bound->comparisonType), "Minimizing objective should not specify an upper bound."); + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + auto const& formula = *this->objectives[objIndex].formula; + STORM_LOG_ASSERT(formula.hasBound(), "Achievability query invoked but there is an objective without bound."); + thresholds.push_back(formula.template getThresholdAs()); + if (storm::solver::minimize(formula.getOptimalityType())) { + STORM_LOG_ASSERT(!storm::logic::isLowerBound(formula.getBound().comparisonType), "Minimizing objective should not specify an upper bound."); // Values for minimizing objectives will be negated in order to convert them to maximizing objectives. // Hence, we also negate the threshold thresholds.back() *= -storm::utility::one(); } - strictThresholds.set(objIndex, storm::logic::isStrict(obj.bound->comparisonType)); + strictThresholds.set(objIndex, storm::logic::isStrict(formula.getBound().comparisonType)); } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index c459ce7df..0405a6022 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -24,7 +24,7 @@ namespace storm { STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorReturnType::QueryType::Quantitative, "Invalid query Type"); for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - if (!this->objectives[objIndex].bound.is_initialized()) { + if (!this->objectives[objIndex].formula->hasBound()) { indexOfOptimizingObjective = objIndex; break; } @@ -41,19 +41,19 @@ namespace storm { thresholds.reserve(this->objectives.size()); strictThresholds = storm::storage::BitVector(this->objectives.size(), false); std::vector> thresholdConstraints; - thresholdConstraints.reserve(this->objectives.size()-1); + thresholdConstraints.reserve(this->objectives.size() - 1); for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - auto const& obj = this->objectives[objIndex]; - if (obj.bound) { - STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "There is an objective whose bound contains undefined variables."); - thresholds.push_back(storm::utility::convertNumber(obj.bound->threshold.evaluateAsRational())); - if (storm::solver::minimize(obj.optimizationDirection)) { - STORM_LOG_ASSERT(!storm::logic::isLowerBound(obj.bound->comparisonType), "Minimizing objective should not specify an upper bound."); + auto const& formula = *this->objectives[objIndex].formula; + + if (formula.hasBound()) { + thresholds.push_back(formula.template getThresholdAs()); + if (storm::solver::minimize(formula.getOptimalityType())) { + STORM_LOG_ASSERT(!storm::logic::isLowerBound(formula.getBound().comparisonType), "Minimizing objective should not specify an upper bound."); // Values for minimizing objectives will be negated in order to convert them to maximizing objectives. // Hence, we also negate the threshold thresholds.back() *= -storm::utility::one(); } - strictThresholds.set(objIndex, storm::logic::isStrict(obj.bound->comparisonType)); + strictThresholds.set(objIndex, storm::logic::isStrict(formula.getBound().comparisonType)); WeightVector normalVector(this->objectives.size(), storm::utility::zero()); normalVector[objIndex] = -storm::utility::one(); thresholdConstraints.emplace_back(std::move(normalVector), -thresholds.back()); @@ -74,7 +74,7 @@ namespace storm { // transform the obtained result for the preprocessed model to a result w.r.t. the original model and return the checkresult auto const& obj = this->objectives[indexOfOptimizingObjective]; - if (storm::solver::maximize(obj.optimizationDirection)) { + if (storm::solver::maximize(obj.formula->getOptimalityType())) { if (obj.considersComplementaryEvent) { result = storm::utility::one() - result; } @@ -95,7 +95,7 @@ namespace storm { template bool SparsePcaaQuantitativeQuery::checkAchievability() { - if (this->objectives.size()>1) { + if (this->objectives.size() > 1) { // We don't care for the optimizing objective at this point this->diracWeightVectorsToBeChecked.set(indexOfOptimizingObjective, false); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index 9276613b1..a978dc53c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -107,7 +107,7 @@ namespace storm { step.upperBoundPoint = storm::utility::vector::convertNumericVector(weightVectorChecker->getOverApproximationOfInitialStateResults()); // For the minimizing objectives, we need to scale the corresponding entries with -1 as we want to consider the downward closure for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - if (storm::solver::minimize(this->objectives[objIndex].optimizationDirection)) { + if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) { step.lowerBoundPoint[objIndex] *= -storm::utility::one(); step.upperBoundPoint[objIndex] *= -storm::utility::one(); } @@ -161,7 +161,7 @@ namespace storm { result.reserve(point.size()); for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { auto const& obj = this->objectives[objIndex]; - if (storm::solver::maximize(obj.optimizationDirection)) { + if (storm::solver::maximize(obj.formula->getOptimalityType())) { if (obj.considersComplementaryEvent) { result.push_back(storm::utility::one() - point[objIndex]); } else { @@ -192,7 +192,7 @@ namespace storm { transformationVector.reserve(numObjectives); for(uint_fast64_t objIndex = 0; objIndex < numObjectives; ++objIndex) { auto const& obj = this->objectives[objIndex]; - if (storm::solver::maximize(obj.optimizationDirection)) { + if (storm::solver::maximize(obj.formula->getOptimalityType())) { if (obj.considersComplementaryEvent) { transformationMatrix[objIndex][objIndex] = -storm::utility::one(); transformationVector.push_back(storm::utility::one()); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index be8727462..452254107 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -12,6 +12,7 @@ #include "storm/utility/graph.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" +#include "storm/logic/Formulas.h" #include "storm/exceptions/IllegalFunctionCallException.h" #include "storm/exceptions/UnexpectedException.h" @@ -42,10 +43,11 @@ namespace storm { // set data for unbounded objectives for(uint_fast64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { - auto const& obj = objectives[objIndex]; - if (!obj.upperTimeBound) { + auto const& formula = *objectives[objIndex].formula; + if (formula.getSubformula().isTotalRewardFormula()) { objectivesWithNoUpperTimeBound.set(objIndex, true); - actionsWithoutRewardInUnboundedPhase &= model.getRewardModel(*obj.rewardModelName).getChoicesWithZeroReward(model.getTransitionMatrix()); + STORM_LOG_ASSERT(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), "Unexpected type of operator formula."); + actionsWithoutRewardInUnboundedPhase &= model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()).getChoicesWithZeroReward(model.getTransitionMatrix()); } } } @@ -59,26 +61,27 @@ namespace storm { boost::optional weightedLowerResultBound = storm::utility::zero(); boost::optional weightedUpperResultBound = storm::utility::zero(); for (auto objIndex : objectivesWithNoUpperTimeBound) { - if (storm::solver::minimize(objectives[objIndex].optimizationDirection)) { - if (objectives[objIndex].lowerResultBound && weightedUpperResultBound) { - weightedUpperResultBound.get() -= weightVector[objIndex] * objectives[objIndex].lowerResultBound.get(); + auto const& obj = objectives[objIndex]; + if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) { + if (obj.lowerResultBound && weightedUpperResultBound) { + weightedUpperResultBound.get() -= weightVector[objIndex] * obj.lowerResultBound.get(); } else { weightedUpperResultBound = boost::none; } - if (objectives[objIndex].upperResultBound && weightedLowerResultBound) { - weightedLowerResultBound.get() -= weightVector[objIndex] * objectives[objIndex].upperResultBound.get(); + if (obj.upperResultBound && weightedLowerResultBound) { + weightedLowerResultBound.get() -= weightVector[objIndex] * obj.upperResultBound.get(); } else { weightedLowerResultBound = boost::none; } storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], -weightVector[objIndex]); } else { - if (objectives[objIndex].lowerResultBound && weightedLowerResultBound) { - weightedLowerResultBound.get() += weightVector[objIndex] * objectives[objIndex].lowerResultBound.get(); + if (obj.lowerResultBound && weightedLowerResultBound) { + weightedLowerResultBound.get() += weightVector[objIndex] * obj.lowerResultBound.get(); } else { weightedLowerResultBound = boost::none; } - if (objectives[objIndex].upperResultBound && weightedUpperResultBound) { - weightedUpperResultBound.get() += weightVector[objIndex] * objectives[objIndex].upperResultBound.get(); + if (obj.upperResultBound && weightedUpperResultBound) { + weightedUpperResultBound.get() += weightVector[objIndex] * obj.upperResultBound.get(); } else { weightedUpperResultBound = boost::none; } @@ -90,8 +93,8 @@ namespace storm { unboundedIndividualPhase(weightVector); // Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound - for(auto const& obj : this->objectives) { - if(obj.lowerTimeBound || obj.upperTimeBound) { + for (auto const& obj : this->objectives) { + if (!obj.formula->getSubformula().isTotalRewardFormula()) { boundedPhase(weightVector, weightedRewardVector); break; } @@ -140,8 +143,8 @@ namespace storm { template storm::storage::Scheduler::ValueType> SparsePcaaWeightVectorChecker::computeScheduler() const { STORM_LOG_THROW(this->checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); - for(auto const& obj : this->objectives) { - STORM_LOG_THROW(!obj.lowerTimeBound && !obj.upperTimeBound, storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for timeBounded objectives."); + for (auto const& obj : this->objectives) { + STORM_LOG_THROW(obj.formula->getSubformula().isTotalRewardFormula(), storm::exceptions::NotImplementedException, "Scheduler retrival is only implemented for objectives without time-bound."); } storm::storage::Scheduler result(this->optimalChoices.size()); @@ -202,7 +205,7 @@ namespace storm { if (objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) { uint_fast64_t objIndex = *objectivesWithNoUpperTimeBound.begin(); objectiveResults[objIndex] = weightedResult; - if (storm::solver::minimize(objectives[objIndex].optimizationDirection)) { + if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) { storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], -storm::utility::one()); } for (uint_fast64_t objIndex2 = 0; objIndex2 < objectives.size(); ++objIndex2) { @@ -235,7 +238,7 @@ namespace storm { if (!storm::utility::isZero(weightVector[objIndex])) { objectiveResults[objIndex] = weightedSumOfUncheckedObjectives; ValueType scalingFactor = storm::utility::one() / sumOfWeightsOfUncheckedObjectives; - if (storm::solver::minimize(obj.optimizationDirection)) { + if (storm::solver::minimize(obj.formula->getOptimalityType())) { scalingFactor *= -storm::utility::one(); } storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], scalingFactor);