From 0b6d0a7e5e508d4b4b5baceb59be89402d5f5767 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 13 Jun 2016 19:13:53 +0200 Subject: [PATCH] improvements for preprocessor Former-commit-id: 99a3bc44a00e72c56c58a06a2eeaf0c3fc3c4b6e --- .../SparseMultiObjectivePreprocessor.cpp | 143 ++++++++---------- .../helper/SparseMultiObjectivePreprocessor.h | 14 +- ...arseMultiObjectivePreprocessorReturnType.h | 28 +++- 3 files changed, 82 insertions(+), 103 deletions(-) diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index 834977a4d..29f1b3edb 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp @@ -22,23 +22,21 @@ namespace storm { ReturnType data(std::move(originalModel)); //Initialize the state mapping. data.newToOldStateIndexMapping = storm::utility::vector::buildVectorForRange(0, data.preprocessedModel.getNumberOfStates()); - //Gather information regarding the individual objectives + //Invoke preprocessing on the individual objectives for(auto const& subFormula : originalFormula.getSubFormulas()){ - addObjective(subFormula, data); - } - //Invoke preprocessing on objectives - for (auto& obj : data.objectives){ - STORM_LOG_DEBUG("Preprocessing objective " << *obj.originalFormula << "."); - if(obj.originalFormula->isProbabilityOperatorFormula()){ - preprocessFormula(obj.originalFormula->asProbabilityOperatorFormula(), data, obj); - } else if(obj.originalFormula->isRewardOperatorFormula()){ - preprocessFormula(obj.originalFormula->asRewardOperatorFormula(), data, obj); + STORM_LOG_DEBUG("Preprocessing objective " << *subFormula<< "."); + data.objectives.emplace_back(); + ObjectiveInformation& currentObjective = data.objectives.back(); + currentObjective.originalFormula = subFormula; + if(currentObjective.originalFormula->isOperatorFormula()) { + preprocessFormula(currentObjective.originalFormula->asOperatorFormula(), data, currentObjective); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *obj.originalFormula << " of " << originalFormula << " because it is not supported"); + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported"); } } + //We can now remove all original reward models to save some memory - std::set origRewardModels = originalFormula.getReferencedRewardModels(); + std::set origRewardModels = originalFormula.getReferencedRewardModels(); for (auto const& rewModel : origRewardModels){ data.preprocessedModel.removeRewardModel(rewModel); } @@ -46,55 +44,51 @@ namespace storm { } template - void SparseMultiObjectivePreprocessor::addObjective(std::shared_ptr const& formula, ReturnType& data) { - STORM_LOG_THROW(formula->isOperatorFormula(), storm::exceptions::InvalidPropertyException, "Expected an OperatorFormula as subformula of multi-objective query but got " << *formula); + void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::OperatorFormula const& formula, ReturnType& data, ObjectiveInformation& currentObjective) { - ObjectiveInformation objective; - objective.originalFormula = formula; - objective.rewardModelName = "objective" + std::to_string(data.objectives.size()); - // Make sure the new reward model gets a unique name - while(data.preprocessedModel.hasRewardModel(objective.rewardModelName)){ - objective.rewardModelName = "_" + objective.rewardModelName; - } - data.objectives.push_back(std::move(objective)); - } - - template - void SparseMultiObjectivePreprocessor::setStepBoundOfObjective(ObjectiveInformation& objective){ - if(objective.originalFormula->isProbabilityOperatorFormula()){ - storm::logic::Formula const& f = objective.originalFormula->asProbabilityOperatorFormula().getSubformula(); - if(f.isBoundedUntilFormula()){ - STORM_LOG_THROW(f.asBoundedUntilFormula().hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with a discrete time bound but got " << f << "."); - objective.stepBound = f.asBoundedUntilFormula().getDiscreteTimeBound(); - } - } else if(objective.originalFormula->isRewardOperatorFormula()){ - storm::logic::Formula const& f = objective.originalFormula->asRewardOperatorFormula(); - if(f.isCumulativeRewardFormula()){ - STORM_LOG_THROW(f.asCumulativeRewardFormula().hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << f << "."); - objective.stepBound = f.asCumulativeRewardFormula().getDiscreteTimeBound(); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Expected a Probability or Reward OperatorFormula but got " << *objective.originalFormula << "."); + // Get a unique name for the new reward model. + currentObjective.rewardModelName = "objective" + std::to_string(data.objectives.size()); + while(data.preprocessedModel.hasRewardModel(currentObjective.rewardModelName)){ + currentObjective.rewardModelName = "_" + currentObjective.rewardModelName; } - } - - template - void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& data, ObjectiveInformation& currentObjective) { - //Set the information for the objective + + currentObjective.toOriginalValueTransformationFactor = storm::utility::one(); + currentObjective.toOriginalValueTransformationOffset = storm::utility::zero(); + currentObjective.rewardsArePositive = true; + + bool formulaMinimizes = false; if(formula.hasBound()) { - currentObjective.threshold = formula.getBound().threshold; + currentObjective.threshold = storm::utility::convertNumber(formula.getBound().threshold); currentObjective.thresholdIsStrict = storm::logic::isStrict(formula.getBound().comparisonType); - currentObjective.isNegative = !storm::logic::isLowerBound(formula.getBound().comparisonType); - if(currentObjective.isNegative) { - *currentObjective.threshold *= -storm::utility::one(); - } + //Note that we minimize for upper bounds since we are looking for the EXISTENCE of a satisfying scheduler + formulaMinimizes = !storm::logic::isLowerBound(formula.getBound().comparisonType); } else if (formula.hasOptimalityType()){ - currentObjective.isNegative = storm::solver::minimize(formula.getOptimalityType()); + formulaMinimizes = storm::solver::minimize(formula.getOptimalityType()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize"); } + if(formulaMinimizes) { + // We negate all the values so we can consider the maximum for this objective + // Thus, all objectives will be maximized. + currentObjective.rewardsArePositive = false; + currentObjective.toOriginalValueTransformationFactor = -storm::utility::one(); + } + + if(formula.isProbabilityOperatorFormula()){ + preprocessFormula(formula.asProbabilityOperatorFormula(), data, currentObjective); + } else if(formula.isRewardOperatorFormula()){ + preprocessFormula(formula.asRewardOperatorFormula(), data, currentObjective); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported"); + } - // Invoke preprocessing for subformula + if(currentObjective.threshold) { + currentObjective.threshold = (currentObjective.threshold.get() - currentObjective.toOriginalValueTransformationOffset) / currentObjective.toOriginalValueTransformationFactor; + } + } + + template + void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& data, ObjectiveInformation& currentObjective) { if(formula.getSubformula().isUntilFormula()){ preprocessFormula(formula.getSubformula().asUntilFormula(), data, currentObjective); } else if(formula.getSubformula().isBoundedUntilFormula()){ @@ -110,28 +104,9 @@ namespace storm { template void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& data, ObjectiveInformation& currentObjective) { - //TODO Make sure that our decision for negative rewards is consistent with the formula - // STORM_LOG_THROW(data.negatedRewardsConsidered == currentObjective.originalFormulaMinimizes, storm::exceptions::InvalidPropertyException, "Decided to consider " << (data.negatedRewardsConsidered ? "negated" : "non-negated") << "rewards, but the formula " << formula << (currentObjective.originalFormulaMinimizes ? " minimizes" : "maximizes") << ". Reward objectives should either all minimize or all maximize."); - // Check if the reward model is uniquely specified STORM_LOG_THROW((formula.hasRewardModelName() && data.preprocessedModel.hasRewardModel(formula.getRewardModelName())) || data.preprocessedModel.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "The reward model is not unique and the formula " << formula << " does not specify a reward model."); - - //Set the information for the objective - if(formula.hasBound()) { - currentObjective.threshold = formula.getBound().threshold; - currentObjective.thresholdIsStrict = storm::logic::isStrict(formula.getBound().comparisonType); - currentObjective.isNegative = !storm::logic::isLowerBound(formula.getBound().comparisonType); - if(currentObjective.isNegative) { - *currentObjective.threshold *= -storm::utility::one(); - } - } else if (formula.hasOptimalityType()){ - currentObjective.isNegative = storm::solver::minimize(formula.getOptimalityType()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize"); - } - - // Invoke preprocessing for subformula if(formula.getSubformula().isEventuallyFormula()){ preprocessFormula(formula.getSubformula().asEventuallyFormula(), data, currentObjective, formula.getOptionalRewardModelName()); } else if(formula.getSubformula().isCumulativeRewardFormula()) { @@ -171,7 +146,7 @@ namespace storm { objectiveRewards[row] = data.preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, newPsiStates); } } - if(currentObjective.isNegative){ + if(!currentObjective.rewardsArePositive) { storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one()); } data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards)); @@ -186,18 +161,17 @@ namespace storm { template void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::GloballyFormula const& formula, ReturnType& data, ObjectiveInformation& currentObjective) { - // The formula will be transformed to an until formula for the complementary event - currentObjective.isInverted = true; + // The formula will be transformed to an until formula for the complementary event. + // If the original formula minimizes, the complementary one will maximize and vice versa. + // Hence, the decision whether to consider positive or negative rewards flips. + currentObjective.rewardsArePositive = !currentObjective.rewardsArePositive; + // To transform from the value of the preprocessed model back to the value of the original model, we have to add 1 to the result. + // The transformation factor has already been set correctly + currentObjective.toOriginalValueTransformationOffset = storm::utility::one(); if(currentObjective.threshold) { - // the threshold changes from e.g. '> -p' to '>= 1-p' and '> p' to '>= p-1' - if(currentObjective.isNegative) { - *currentObjective.threshold += storm::utility::one(); - } else { - *currentObjective.threshold -= storm::utility::one(); - } + // Strict thresholds become non-strict and vice versa currentObjective.thresholdIsStrict = !currentObjective.thresholdIsStrict; } - currentObjective.isNegative = !currentObjective.isNegative; auto negatedSubformula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()); preprocessFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), data, currentObjective); } @@ -228,7 +202,10 @@ namespace storm { // Add a reward model that gives zero reward to the states of the second copy. std::vector objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "").getTotalRewardVector(data.preprocessedModel.getTransitionMatrix()); storm::utility::vector::setVectorValues(objectiveRewards, duplicatorResult.secondCopy, storm::utility::zero()); - if(currentObjective.isNegative){ + storm::storage::BitVector positiveRewards = storm::utility::vector::filterGreaterZero(objectiveRewards); + storm::storage::BitVector nonNegativeRewards = positiveRewards | storm::utility::vector::filterZero(objectiveRewards); + STORM_LOG_THROW(nonNegativeRewards.full() || positiveRewards.empty(), storm::exceptions::InvalidPropertyException, "The reward model for the formula " << formula << " has positive and negative rewards which is not supported."); + if(!currentObjective.rewardsArePositive){ storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one()); } data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards)); @@ -240,7 +217,7 @@ namespace storm { currentObjective.stepBound = formula.getDiscreteTimeBound(); std::vector objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "").getTotalRewardVector(data.preprocessedModel.getTransitionMatrix()); - if(currentObjective.isNegative){ + if(!currentObjective.rewardsArePositive){ storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one()); } data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards)); diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h index ee0575c04..8226d0dc0 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h @@ -30,19 +30,6 @@ namespace storm { private: - /*! - * Inserts the information regarding the given formula (i.e. objective) into info.objectives - * - * @param formula OperatorFormula representing the objective - * @param the information collected so far - */ - static void addObjective(std::shared_ptr const& formula, ReturnType& data); - - /*! - * Sets the timeBound for the given objective - */ - static void setStepBoundOfObjective(ObjectiveInformation& currentObjective); - /*! * Apply the neccessary preprocessing for the given formula. * @param formula the current (sub)formula @@ -50,6 +37,7 @@ namespace storm { * @param currentObjective the currently considered objective. The given formula should be a a (sub)formula of this objective * @param optionalRewardModelName the reward model name that is considered for the formula (if available) */ + static void preprocessFormula(storm::logic::OperatorFormula const& formula, ReturnType& info, ObjectiveInformation& currentObjective); static void preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& info, ObjectiveInformation& currentObjective); static void preprocessFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& info, ObjectiveInformation& currentObjective); static void preprocessFormula(storm::logic::UntilFormula const& formula, ReturnType& info, ObjectiveInformation& currentObjective); diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h index 4a5dcc367..3678bf416 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h @@ -21,19 +21,32 @@ namespace storm { typedef typename SparseModelType::RewardModelType RewardModelType; struct ObjectiveInformation { + // the original input formula std::shared_ptr originalFormula; + + // the name of the considered reward model in the preprocessedModel std::string rewardModelName; - bool isNegative = false; - bool isInverted = false; - boost::optional threshold; + + // true if all rewards for this objective are positive, false if all rewards are negative. + bool rewardsArePositive; + + // transformation from the values of the preprocessed model to the ones for the actual input model, i.e., + // x is achievable in the preprocessed model iff factor*x + offset is achievable in the original model + ValueType toOriginalValueTransformationFactor; + ValueType toOriginalValueTransformationOffset; + + // The probability/reward threshold for the preprocessed model (if originalFormula specifies one). + // This is always a lower bound. + boost::optional threshold; + // True iff the specified threshold is strict, i.e., > bool thresholdIsStrict = false; + + // The (discrete) stepBound for the formula (if given by the originalFormula) boost::optional stepBound; void printToStream(std::ostream& out) const { out << std::setw(30) << originalFormula->toString(); - out << " \t("; - out << (isNegative ? "-x, " : " "); - out << (isInverted ? "1-x, " : " "); + out << " \t(toOrigVal:" << std::setw(3) << toOriginalValueTransformationFactor << "*x +" << std::setw(3) << toOriginalValueTransformationOffset << ", \t"; out << "intern threshold:"; if(threshold){ out << (thresholdIsStrict ? " >" : ">="); @@ -42,7 +55,8 @@ namespace storm { out << " none,"; } out << " \t"; - out << "intern reward model: " << std::setw(10) << rewardModelName << ", \t"; + out << "intern reward model: " << std::setw(10) << rewardModelName; + out << (rewardsArePositive ? " (positive)" : " (negative)") << ", \t"; out << "step bound:"; if(stepBound) { out << std::setw(5) << (*stepBound);