From ee54c6cdacd889e969906955a3555107b15ba587 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 30 Apr 2017 14:59:03 +0200 Subject: [PATCH] Towards refactoring multi-objective preprocessing --- .../modelchecker/multiobjective/Objective.h | 64 +++ .../SparseMultiObjectivePreprocessor.cpp | 448 ++++++++++++++++++ .../SparseMultiObjectivePreprocessor.h | 84 ++++ ...arseMultiObjectivePreprocessorReturnType.h | 73 +++ .../SparseMultiObjectivePreprocessorTask.h | 131 +++++ 5 files changed, 800 insertions(+) create mode 100644 src/storm/modelchecker/multiobjective/Objective.h create mode 100644 src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp create mode 100644 src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h create mode 100644 src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h create mode 100644 src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h diff --git a/src/storm/modelchecker/multiobjective/Objective.h b/src/storm/modelchecker/multiobjective/Objective.h new file mode 100644 index 000000000..6e7040fac --- /dev/null +++ b/src/storm/modelchecker/multiobjective/Objective.h @@ -0,0 +1,64 @@ +#pragma once + +#include + +#include "storm/logic/Formula.h" +#include "storm/logic/Bound.h" +#include "storm/logic/TimeBound.h" +#include "storm/solver/OptimizationDirection.h" + +namespace storm { + namespace modelchecker { + 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; + + // 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 bouds + boost::optional lowerTimeBound, upperTimeBound; + + 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 << " \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: " << *rewardModelName; + } + }; + } + } +} + diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp new file mode 100644 index 000000000..e85b41de6 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -0,0 +1,448 @@ +#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h" + +#include +#include + +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" +#include "storm/storage/memorystructure/MemoryStructureBuilder.h" +#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/transformer/SubsystemBuilder.h" +#include "storm/utility/macros.h" +#include "storm/utility/vector.h" +#include "storm/utility/graph.h" +#include "storm/utility/endComponents.h" + +#include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/NotImplementedException.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + template + typename SparseMultiObjectivePreprocessor::ReturnType SparseMultiObjectivePreprocessor::preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula) { + + PreprocessorData data(originalModel); + + //Invoke preprocessing on the individual objectives + for (auto const& subFormula : originalFormula.getSubformulas()) { + STORM_LOG_INFO("Preprocessing objective " << *subFormula<< "."); + data.objectives.push_back(std::make_shared>()); + data.objectives.back()->originalFormula = subFormula; + data.finiteRewardCheckObjectives.resize(data.objectives.size(), false); + if (data.objectives.back()->originalFormula->isOperatorFormula()) { + preprocessOperatorFormula(data.objectives.back()->originalFormula->asOperatorFormula(), data); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported"); + } + } + + storm::storage::SparseModelMemoryProduct product = data.memory->product(originalModel); + std::shared_ptr preprocessedModel = std::dynamic_pointer_cast(product.build()); + + auto backwardTransitions = preprocessedModel->getBackwardTransitions(); + + bool endComponentAnalysisRequired = false; + for (auto& task : data.tasks) { + endComponentAnalysisRequired = endComponentAnalysisRequired || task->requiresEndComponentAnalysis(); + } + if (endComponentAnalysisRequired) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "End component analysis required but currently not implemented."); + } + + for (auto& task : data.tasks) { + task->perform(*preprocessedModel); + } + + ReturnType result(originalFormula, originalModel); + for (auto& obj : data.objectives) { + result.objectives.push_back(std::move(*obj)); + } + result.preprocessedModel = std::move(preprocessedModel); + result.queryType = ReturnType::QueryType::Achievability; + + auto minMaxNonZeroRewardStates = getStatesWithNonZeroRewardMinMax(result, backwardTransitions); + auto finiteRewardStates = ensureRewardFiniteness(result, data.finiteRewardCheckObjectives, minMaxNonZeroRewardStates.first, backwardTransitions); + + std::set relevantRewardModels; + for (auto const& obj : result.objectives) { + relevantRewardModels.insert(*obj.rewardModelName); + } + + // Build a subsystem that discards states that yield infinite reward for all schedulers. + // We can also merge the states that will have reward zero anyway. + storm::storage::BitVector zeroRewardStates = ~minMaxNonZeroRewardStates.second; + storm::transformer::GoalStateMerger merger(*result.preprocessedModel); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = merger.mergeTargetAndSinkStates(finiteRewardStates, zeroRewardStates, storm::storage::BitVector(finiteRewardStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end())); + + result.preprocessedModel = mergerResult.model; + result.possibleBottomStates = (~minMaxNonZeroRewardStates.first) % finiteRewardStates; + if (mergerResult.targetState) { + storm::storage::BitVector targetStateAsVector(result.preprocessedModel->getNumberOfStates(), false); + targetStateAsVector.set(*mergerResult.targetState, true); + result.possibleECChoices = storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector); + result.possibleECChoices.set(result.preprocessedModel->getTransitionMatrix().getRowGroupIndices()[*mergerResult.targetState], true); + // There is an additional state in the result + result.possibleBottomStates.resize(result.possibleBottomStates.size() + 1, true); + } + assert(result.possibleBottomStates.size() == result.preprocessedModel->getNumberOfStates()); + + + return result; + } + + template + SparseMultiObjectivePreprocessor::PreprocessorData::PreprocessorData(SparseModelType const& model) : originalModel(model) { + storm::storage::MemoryStructureBuilder memoryBuilder(1); + memoryBuilder.setTransition(0,0, storm::logic::Formula::getTrueFormula()); + memory = std::make_shared(memoryBuilder.build()); + + // The memoryLabelPrefix should not be a prefix of a state label of the given model to ensure uniqueness of label names + memoryLabelPrefix = "mem"; + while (true) { + bool prefixIsUnique = true; + for (auto const& label : originalModel.getStateLabeling().getLabels()) { + if (memoryLabelPrefix.size() <= label.size()) { + if (std::mismatch(memoryLabelPrefix.begin(), memoryLabelPrefix.end(), label.begin()).first == memoryLabelPrefix.end()) { + prefixIsUnique = false; + memoryLabelPrefix = "_" + memoryLabelPrefix; + break; + } + } + } + if (prefixIsUnique) { + break; + } + } + + // The rewardModelNamePrefix should not be a prefix of a reward model name of the given model to ensure uniqueness of reward model names + rewardModelNamePrefix = "obj"; + while (true) { + bool prefixIsUnique = true; + for (auto const& label : originalModel.getStateLabeling().getLabels()) { + if (memoryLabelPrefix.size() <= label.size()) { + if (std::mismatch(memoryLabelPrefix.begin(), memoryLabelPrefix.end(), label.begin()).first == memoryLabelPrefix.end()) { + prefixIsUnique = false; + memoryLabelPrefix = "_" + memoryLabelPrefix; + break; + } + } + } + if (prefixIsUnique) { + break; + } + } + + + } + + template + void SparseMultiObjectivePreprocessor::preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data) { + + Objective& objective = *data.objectives.back(); + + objective.considersComplementaryEvent = false; + + 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; + objective.bound->comparisonType = storm::logic::invert(objective.bound->comparisonType); + } + objective.optimizationDirection = storm::solver::invert(objective.optimizationDirection); + } + + } + + template + void SparseMultiObjectivePreprocessor::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data) { + + if (formula.getSubformula().isUntilFormula()){ + preprocessUntilFormula(formula.getSubformula().asUntilFormula(), data); + } else if (formula.getSubformula().isBoundedUntilFormula()){ + preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), data); + } else if (formula.getSubformula().isGloballyFormula()){ + preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), data); + } else if (formula.getSubformula().isEventuallyFormula()){ + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), 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) { + + 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."); + + std::string rewardModelName; + if (formula.hasRewardModelName()) { + rewardModelName = formula.getRewardModelName(); + STORM_LOG_THROW(data.originalModel.hasRewardModel(rewardModelName), storm::exceptions::InvalidPropertyException, "The reward model specified by formula " << formula << " does not exist in the model"); + } else { + STORM_LOG_THROW(data.originalModel.hasUniqueRewardModel(), storm::exceptions::InvalidOperationException, "The formula " << formula << " does not specify a reward model name and the reward model is not unique."); + rewardModelName = data.originalModel.getRewardModels().begin()->first; + } + + if (formula.getSubformula().isEventuallyFormula()){ + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data, rewardModelName); + } else if (formula.getSubformula().isCumulativeRewardFormula()) { + preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), data, rewardModelName); + } else if (formula.getSubformula().isTotalRewardFormula()) { + preprocessTotalRewardFormula(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) { + // 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."); + + if (formula.getSubformula().isEventuallyFormula()){ + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), 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) { + + // 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) { + storm::modelchecker::SparsePropositionalModelChecker mc(data.originalModel); + if (!(data.originalModel.getInitialStates() & mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()).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."); + } + } + + // Create a memory structure that stores whether a non-PhiState or a PsiState has already been reached + storm::storage::MemoryStructureBuilder builder(2); + std::string relevantStatesLabel = data.memoryLabelPrefix + "_obj" + std::to_string(data.objectives.size()) + "_relevant"; + builder.setLabel(0, relevantStatesLabel); + auto negatedLeftSubFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getLeftSubformula().asSharedPointer()); + auto targetFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, negatedLeftSubFormula, formula.getRightSubformula().asSharedPointer()); + builder.setTransition(0, 0, std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, targetFormula)); + builder.setTransition(0, 1, targetFormula); + builder.setTransition(1, 1, storm::logic::Formula::getTrueFormula()); + 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()); + + auto relevantStatesFormula = std::make_shared(relevantStatesLabel); + data.tasks.push_back(std::make_shared>(data.objectives.back(), relevantStatesFormula, formula.getRightSubformula().asSharedPointer())); + + } + + template + void SparseMultiObjectivePreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data) { + STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); + + if (formula.hasLowerBound()) { + STORM_LOG_THROW(!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()); + } + } + 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; + + auto negatedSubformula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()); + + preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), data); + } + + template + void SparseMultiObjectivePreprocessor::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, boost::optional const& optionalRewardModelName) { + if (formula.isReachabilityProbabilityFormula()){ + preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), data); + return; + } + + // Create a memory structure that stores whether a target state has already been reached + storm::storage::MemoryStructureBuilder builder(2); + // Get a unique label that is not already present in the model + std::string relevantStatesLabel = data.memoryLabelPrefix + "_obj" + std::to_string(data.objectives.size()) + "_relevant"; + builder.setLabel(0, relevantStatesLabel); + builder.setTransition(0, 0, std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer())); + builder.setTransition(0, 1, formula.getSubformula().asSharedPointer()); + builder.setTransition(1, 1, std::make_shared(true)); + storm::storage::MemoryStructure objectiveMemory = builder.build(); + data.memory = std::make_shared(data.memory->product(objectiveMemory)); + + auto relevantStatesFormula = std::make_shared(relevantStatesLabel); + + data.objectives.back()->rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); + + if (formula.isReachabilityRewardFormula()) { + assert(optionalRewardModelName.is_initialized()); + data.tasks.push_back(std::make_shared>(data.objectives.back(), relevantStatesFormula, optionalRewardModelName.get())); + data.finiteRewardCheckObjectives.set(data.objectives.size() - 1); + } else if (formula.isReachabilityTimeFormula() && data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton)) { + data.finiteRewardCheckObjectives.set(data.objectives.size() - 1); + data.tasks.push_back(std::make_shared>(data.objectives.back(), relevantStatesFormula)); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported."); + } + } + + template + void SparseMultiObjectivePreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, 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()); + } + + + } + + template + void SparseMultiObjectivePreprocessor::preprocessTotalRewardFormula(PreprocessorData& data, boost::optional const& optionalRewardModelName) { + assert(optionalRewardModelName.is_initialized()); + data.objectives.back()->rewardModelName = *optionalRewardModelName; + data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); + } + + + template + std::pair SparseMultiObjectivePreprocessor::getStatesWithNonZeroRewardMinMax(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions) { + + uint_fast64_t stateCount = result.preprocessedModel->getNumberOfStates(); + auto const& transitions = result.preprocessedModel->getTransitionMatrix(); + std::vector const& groupIndices = transitions.getRowGroupIndices(); + storm::storage::BitVector allStates(stateCount, true); + + // 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); + } + + // Get the states that have reward for at least one (or for all) choices assigned to it. + storm::storage::BitVector statesWithRewardForOneChoice = storm::storage::BitVector(stateCount, false); + storm::storage::BitVector statesWithRewardForAllChoices = storm::storage::BitVector(stateCount, true); + for (uint_fast64_t state = 0; state < stateCount; ++state) { + bool stateHasChoiceWithReward = false; + bool stateHasChoiceWithoutReward = false; + uint_fast64_t const& groupEnd = groupIndices[state + 1]; + for (uint_fast64_t choice = groupIndices[state]; choice < groupEnd; ++choice) { + if (zeroRewardChoices.get(choice)) { + stateHasChoiceWithoutReward = true; + } else { + stateHasChoiceWithReward = true; + } + } + if (stateHasChoiceWithReward) { + statesWithRewardForOneChoice.set(state, true); + } + if (stateHasChoiceWithoutReward) { + statesWithRewardForAllChoices.set(state, false); + } + } + + // get the states from which the minimal/maximal expected reward is always non-zero + storm::storage::BitVector minStates = storm::utility::graph::performProbGreater0A(transitions, groupIndices, backwardTransitions, allStates, statesWithRewardForAllChoices, false, 0, zeroRewardChoices); + storm::storage::BitVector maxStates = storm::utility::graph::performProbGreater0E(backwardTransitions, allStates, statesWithRewardForOneChoice); + STORM_LOG_ASSERT(minStates.isSubsetOf(maxStates), "The computed set of states with minimal non-zero expected rewards is not a subset of the states with maximal non-zero rewards."); + return std::make_pair(std::move(minStates), std::move(maxStates)); + } + + template + storm::storage::BitVector SparseMultiObjectivePreprocessor::ensureRewardFiniteness(ReturnType& result, storm::storage::BitVector const& finiteRewardCheckObjectives, storm::storage::BitVector const& nonZeroRewardMin, storm::storage::SparseMatrix const& backwardTransitions) { + + auto const& transitions = result.preprocessedModel->getTransitionMatrix(); + std::vector const& groupIndices = transitions.getRowGroupIndices(); + + storm::storage::BitVector maxRewardsToCheck(result.preprocessedModel->getNumberOfChoices(), true); + bool hasMinRewardToCheck; + for (auto const& objIndex : finiteRewardCheckObjectives) { + auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].rewardModelName.get()); + if (storm::solver::minimize(result.objectives[objIndex].optimizationDirection)) { + hasMinRewardToCheck = true; + } else { + maxRewardsToCheck &= rewModel.getChoicesWithZeroReward(transitions); + } + } + maxRewardsToCheck.complement(); + + // Assert reward finitiness for maximizing objectives under all schedulers + storm::storage::BitVector allStates(result.preprocessedModel->getNumberOfStates(), true); + if (storm::utility::endComponents::checkIfECWithChoiceExists(transitions, backwardTransitions, allStates, maxRewardsToCheck)) { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "At least one of the maximizing objectives induces infinite expected reward (or time). This is not supported"); + } + + // Assert that there is one scheduler under which all rewards are finite. + // This only has to be done if there are minimizing expected rewards that potentially can be infinite + storm::storage::BitVector finiteRewardStates; + if (hasMinRewardToCheck) { + finiteRewardStates = storm::utility::graph::performProb1E(transitions, groupIndices, backwardTransitions, allStates, ~nonZeroRewardMin); + if ((finiteRewardStates & result.preprocessedModel->getInitialStates()).empty()) { + // There is no scheduler that induces finite reward for the initial state + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "For every scheduler, at least one objective gets infinite reward."); + } + } else { + finiteRewardStates = allStates; + } + return finiteRewardStates; + } + + template class SparseMultiObjectivePreprocessor>; + template class SparseMultiObjectivePreprocessor>; + + template class SparseMultiObjectivePreprocessor>; + template class SparseMultiObjectivePreprocessor>; + } + } +} diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h new file mode 100644 index 000000000..88727c504 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h @@ -0,0 +1,84 @@ +#pragma once + +#include +#include + +#include "storm/logic/Formulas.h" +#include "storm/storage/BitVector.h" +#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h" +#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h" +#include "storm/storage/memorystructure/MemoryStructure.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + /* + * This class invokes the necessary preprocessing for the constraint based multi-objective model checking algorithm + */ + template + class SparseMultiObjectivePreprocessor { + public: + typedef typename SparseModelType::ValueType ValueType; + typedef typename SparseModelType::RewardModelType RewardModelType; + typedef SparseMultiObjectivePreprocessorReturnType ReturnType; + + /*! + * Preprocesses the given model w.r.t. the given formulas + * @param originalModel The considered model + * @param originalFormula the considered formula. The subformulas should only contain one OperatorFormula at top level. + */ + static ReturnType preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula); + + private: + + struct PreprocessorData { + SparseModelType const& originalModel; + std::vector>> objectives; + std::vector>> tasks; + std::shared_ptr memory; + + // Indices of the objectives that require a check for finite reward + storm::storage::BitVector finiteRewardCheckObjectives; + + std::string memoryLabelPrefix; + std::string rewardModelNamePrefix; + + PreprocessorData(SparseModelType const& model); + }; + + /*! + * Apply the neccessary preprocessing for the given formula. + * @param formula the current (sub)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. + + + /*! + * Computes the set of states that have a non-zero reward w.r.t. all objectives, assuming that the objectives are all minimizing and maximizing, respectively. + */ + static std::pair getStatesWithNonZeroRewardMinMax(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions); + + + /*! + * Checks whether the occurring expected rewards are finite. If not, the input is rejected. + * Returns the set of states for which a scheduler exists that induces finite reward for all objectives + */ + static storm::storage::BitVector ensureRewardFiniteness(ReturnType& result, storm::storage::BitVector const& finiteRewardCheckObjectives, storm::storage::BitVector const& nonZeroRewardMin, storm::storage::SparseMatrix const& backwardTransitions); + + }; + } + } +} + diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h new file mode 100644 index 000000000..f9f71231f --- /dev/null +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h @@ -0,0 +1,73 @@ +#pragma once + +#include +#include +#include + +#include "storm/logic/Formulas.h" +#include "storm/modelchecker/multiobjective/constraintbased/CbObjective.h" + +#include "storm/exceptions/UnexpectedException.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + template + struct SparseCbPreprocessorReturnType { + + enum class QueryType { Achievability }; + + storm::logic::MultiObjectiveFormula const& originalFormula; + SparseModelType const& originalModel; + std::shared_ptr preprocessedModel; + QueryType queryType; + + // The (preprocessed) objectives + std::vector> objectives; + + // The states for which there is a scheduler such that all objectives have value zero + storm::storage::BitVector possibleBottomStates; + // Overapproximation of the set of choices that are part of an end component. + storm::storage::BitVector possibleECChoices; + + SparseCbPreprocessorReturnType(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) : originalFormula(originalFormula), originalModel(originalModel) { + // Intentionally left empty + } + + void printToStream(std::ostream& out) const { + out << std::endl; + out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; + out << " Multi-objective Query " << std::endl; + out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; + out << std::endl; + out << "Original Formula: " << std::endl; + out << "--------------------------------------------------------------" << std::endl; + out << "\t" << originalFormula << std::endl; + out << std::endl; + out << "Objectives:" << std::endl; + out << "--------------------------------------------------------------" << std::endl; + for (auto const& obj : objectives) { + obj.printToStream(out); + } + out << "--------------------------------------------------------------" << std::endl; + out << std::endl; + out << "Original Model Information:" << std::endl; + originalModel.printModelInformationToStream(out); + out << std::endl; + out << "Preprocessed Model Information:" << std::endl; + preprocessedModel.printModelInformationToStream(out); + out << std::endl; + out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; + } + + friend std::ostream& operator<<(std::ostream& out, SparseCbPreprocessorReturnType const& ret) { + ret.printToStream(out); + return out; + } + + }; + } + } +} + diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h new file mode 100644 index 000000000..e34e37584 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h @@ -0,0 +1,131 @@ +#pragma once + +#include +#include + +#include "storm/logic/Formula.h" +#include "storm/logic/Bound.h" +#include "storm/solver/OptimizationDirection.h" +#include "storm/modelchecker/multiobjective/Objective.h" +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/utility/vector.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + template + class SparseMultiObjectivePreprocessorTask { + public: + SparseMultiObjectivePreprocessorTask(std::shared_ptr> const& objective) : objective(objective) { + // intentionally left empty + } + + virtual void perform(SparseModelType& preprocessedModel) const = 0; + + virtual bool requiresEndComponentAnalysis() const { + return false; + } + + + protected: + std::shared_ptr> objective; + }; + + // Transforms reachability probabilities to total expected rewards by adding a rewardModel + // such that one reward is given whenever a goal state is reached from a relevant state + template + class SparseMultiObjectivePreprocessorReachProbToTotalRewTask : public SparseMultiObjectivePreprocessorTask { + public: + SparseMultiObjectivePreprocessorReachProbToTotalRewTask(std::shared_ptr> const& objective, std::shared_ptr const& relevantStateFormula, std::shared_ptr const& goalStateFormula) : SparseMultiObjectivePreprocessorTask(objective), relevantStateFormula(relevantStateFormula), goalStateFormula(goalStateFormula) { + // Intentionally left empty + } + + virtual void perform(SparseModelType& preprocessedModel) const override { + + // build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from a relevantState to a goalState + storm::modelchecker::SparsePropositionalModelChecker mc(preprocessedModel); + storm::storage::BitVector relevantStates = mc.check(*relevantStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector goalStates = mc.check(*goalStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + + std::vector objectiveRewards(preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); + for (auto const& state : relevantStates) { + for (uint_fast64_t row = preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; row < preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) { + 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))); + } + + private: + std::shared_ptr relevantStateFormula; + std::shared_ptr goalStateFormula; + }; + + // Transforms expected reachability rewards to total expected rewards by adding a rewardModel + // such that non-relevant states get reward zero + template + class SparseMultiObjectivePreprocessorReachRewToTotalRewTask : public SparseMultiObjectivePreprocessorTask { + public: + SparseMultiObjectivePreprocessorReachRewToTotalRewTask(std::shared_ptr> const& objective, std::shared_ptr const& relevantStateFormula, std::string const& originalRewardModelName) : SparseMultiObjectivePreprocessorTask(objective), relevantStateFormula(relevantStateFormula), originalRewardModelName(originalRewardModelName) { + // Intentionally left empty + } + + virtual void perform(SparseModelType& preprocessedModel) const override { + + // build stateAction reward vector that only gives reward for relevant states + storm::modelchecker::SparsePropositionalModelChecker mc(preprocessedModel); + storm::storage::BitVector nonRelevantStates = ~mc.check(*relevantStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + typename SparseModelType::RewardModelType objectiveRewards = preprocessedModel.getRewardModel(originalRewardModelName); + objectiveRewards.reduceToStateBasedRewards(preprocessedModel.getTransitionMatrix(), false); + if (objectiveRewards.hasStateRewards()) { + storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), nonRelevantStates, storm::utility::zero()); + } + if (objectiveRewards.hasStateActionRewards()) { + for (auto state : nonRelevantStates) { + 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)); + } + + private: + std::shared_ptr relevantStateFormula; + std::string originalRewardModelName; + }; + + // Transforms expected reachability time to total expected rewards by adding a rewardModel + // such that every time step done from a relevant state yields one reward + template + class SparseMultiObjectivePreprocessorReachTimeToTotalRewTask : public SparseMultiObjectivePreprocessorTask { + public: + SparseMultiObjectivePreprocessorReachTimeToTotalRewTask(std::shared_ptr> const& objective, std::shared_ptr const& relevantStateFormula) : SparseMultiObjectivePreprocessorTask(objective), relevantStateFormula(relevantStateFormula) { + // Intentionally left empty + } + + virtual void perform(SparseModelType& preprocessedModel) const override { + + // build stateAction reward vector that only gives reward for relevant states + storm::modelchecker::SparsePropositionalModelChecker mc(preprocessedModel); + storm::storage::BitVector relevantStates = mc.check(*relevantStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + + 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))); + } + + private: + std::shared_ptr relevantStateFormula; + }; + + } + } +} +