From 22a19d68bae2b0740122857fa517b883fae8586f Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 23 Oct 2019 20:42:39 +0200 Subject: [PATCH] Fixed an issue with multi-objective model checking preprocessor not correctly preserving reachability rewards --- .../SparseMultiObjectivePreprocessor.cpp | 46 ++++++++++++------- .../SparseMultiObjectivePreprocessor.h | 5 +- src/storm/transformer/SubsystemBuilder.cpp | 6 +++ src/storm/transformer/SubsystemBuilder.h | 2 + 4 files changed, 42 insertions(+), 17 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp index a27025cf4..1888ab844 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp @@ -54,9 +54,11 @@ namespace storm { } // Remove states that are irrelevant for all properties (e.g. because they are only reachable via goal states - removeIrrelevantStates(model, originalFormula); + boost::optional deadlockLabel; + removeIrrelevantStates(model, deadlockLabel, originalFormula); PreprocessorData data(model); + data.deadlockLabel = deadlockLabel; //Invoke preprocessing on the individual objectives for (auto const& subFormula : originalFormula.getSubformulas()) { @@ -90,18 +92,7 @@ namespace storm { } template - storm::storage::BitVector getZeroRewardStates(SparseModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, typename SparseModelType::RewardModelType const& rewardModel, boost::optional const& rew0States) { - storm::storage::BitVector statesWithoutReward = rewardModel.getStatesWithZeroReward(model.getTransitionMatrix()); - if (rew0States) { - statesWithoutReward |= rew0States.get(); - } - storm::storage::BitVector result = storm::utility::graph::performProbGreater0E(model.getBackwardTransitions(), statesWithoutReward, ~statesWithoutReward); - result.complement(); - return result; - } - - template - void SparseMultiObjectivePreprocessor::removeIrrelevantStates(std::shared_ptr& model, storm::logic::MultiObjectiveFormula const& originalFormula) { + void SparseMultiObjectivePreprocessor::removeIrrelevantStates(std::shared_ptr& model, boost::optional& deadlockLabel, storm::logic::MultiObjectiveFormula const& originalFormula) { storm::storage::BitVector absorbingStates(model->getNumberOfStates(), true); storm::modelchecker::SparsePropositionalModelChecker mc(*model); @@ -161,9 +152,12 @@ namespace storm { if (pathFormula.isEventuallyFormula()) { auto rewardModel = storm::utility::createFilteredRewardModel(baseRewardModel, model->isDiscreteTimeModel(), pathFormula.asEventuallyFormula()); storm::storage::BitVector statesWithoutReward = rewardModel.get().getStatesWithZeroReward(model->getTransitionMatrix()); + // Make states that can not reach a state with non-zero reward absorbing absorbingStatesForSubformula = storm::utility::graph::performProb0A(backwardTransitions, statesWithoutReward, ~statesWithoutReward); auto phi = mc.check(pathFormula.asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + // Make states that reach phi with prob 1 while only visiting states with reward 0 absorbing absorbingStatesForSubformula |= storm::utility::graph::performProb1A(model->getTransitionMatrix(), model->getTransitionMatrix().getRowGroupIndices(), backwardTransitions, statesWithoutReward, phi); + // Make states that are only reachable via phi absorbing absorbingStatesForSubformula |= getOnlyReachableViaPhi(*model, phi); } else if (pathFormula.isCumulativeRewardFormula()) { auto rewardModel = storm::utility::createFilteredRewardModel(baseRewardModel, model->isDiscreteTimeModel(), pathFormula.asCumulativeRewardFormula()); @@ -205,6 +199,7 @@ namespace storm { auto const& submodel = storm::transformer::buildSubsystem(*model, storm::storage::BitVector(model->getNumberOfStates(), true), subsystemActions, false, options); STORM_LOG_INFO("Making states absorbing reduced the state space from " << model->getNumberOfStates() << " to " << submodel.model->getNumberOfStates() << "."); model = submodel.model->template as(); + deadlockLabel = submodel.deadlockLabel; } } @@ -489,13 +484,32 @@ namespace storm { } else { STORM_LOG_INFO("Objective " << *data.objectives.back()->originalFormula << " can not be transformed to an expected total/cumulative reward property."); if (formula.isReachabilityRewardFormula()) { + // TODO: this probably needs some better treatment regarding schedulers that do not reach the goal state allmost surely assert(optionalRewardModelName.is_initialized()); - data.objectives.back()->formula = std::make_shared(formula.asSharedPointer(), optionalRewardModelName.get(), opInfo); + if (data.deadlockLabel) { + // We made some states absorbing and created a new deadlock state. To make sure that this deadlock state gets value zero, we add it to the set of goal states of the formula. + std::shared_ptr newSubSubformula = std::make_shared(data.deadlockLabel.get()); + std::shared_ptr newSubformula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, formula.getSubformula().asSharedPointer(), newSubSubformula); + boost::optional newRewardAccumulation; + if (formula.hasRewardAccumulation()) { + newRewardAccumulation = formula.getRewardAccumulation(); + } + std::shared_ptr newFormula = std::make_shared(newSubformula, formula.getContext(), newRewardAccumulation); + data.objectives.back()->formula = std::make_shared(newFormula, optionalRewardModelName.get(), opInfo); + } else { + data.objectives.back()->formula = std::make_shared(formula.asSharedPointer(), optionalRewardModelName.get(), opInfo); + } } else if (formula.isReachabilityTimeFormula() && data.model->isOfType(storm::models::ModelType::MarkovAutomaton)) { // Reduce to reachability rewards so that time formulas do not have to be treated seperately later. std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); - auto newsubformula = std::make_shared(formula.getSubformula().asSharedPointer(), storm::logic::FormulaContext::Reward); - data.objectives.back()->formula = std::make_shared(newsubformula, rewardModelName, opInfo); + std::shared_ptr newSubformula = formula.getSubformula().asSharedPointer(); + if (data.deadlockLabel) { + // We made some states absorbing and created a new deadlock state. To make sure that this deadlock state gets value zero, we add it to the set of goal states of the formula. + std::shared_ptr newSubSubformula = std::make_shared(data.deadlockLabel.get()); + newSubformula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, formula.getSubformula().asSharedPointer(), newSubSubformula); + } + auto newFormula = std::make_shared(newSubformula, storm::logic::FormulaContext::Reward); + data.objectives.back()->formula = std::make_shared(newFormula, rewardModelName, opInfo); std::vector timeRewards(data.model->getNumberOfStates(), storm::utility::zero()); storm::utility::vector::setVectorValues(timeRewards, dynamic_cast const&>(*data.model).getMarkovianStates(), storm::utility::one()); data.model->addRewardModel(rewardModelName, typename SparseModelType::RewardModelType(std::move(timeRewards))); diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h index 60c692310..67f65b20a 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h @@ -47,13 +47,16 @@ namespace storm { std::string rewardModelNamePrefix; + // If set, some states have been merged to a deadlock state with this label. + boost::optional deadlockLabel; + PreprocessorData(std::shared_ptr model); }; /*! * Removes states that are irrelevant for all objectives, e.g., because they are only reachable via goal states. */ - static void removeIrrelevantStates(std::shared_ptr& model, storm::logic::MultiObjectiveFormula const& originalFormula); + static void removeIrrelevantStates(std::shared_ptr& model, boost::optional& deadlockLabel, storm::logic::MultiObjectiveFormula const& originalFormula); /*! * Apply the neccessary preprocessing for the given formula. diff --git a/src/storm/transformer/SubsystemBuilder.cpp b/src/storm/transformer/SubsystemBuilder.cpp index 44449c5ce..db700196f 100644 --- a/src/storm/transformer/SubsystemBuilder.cpp +++ b/src/storm/transformer/SubsystemBuilder.cpp @@ -168,6 +168,12 @@ namespace storm { components.choiceOrigins.get()->clearOriginOfChoice(choice); } } + // get a unique label for the deadlock states + result.deadlockLabel = "deadl"; + while (components.stateLabeling.containsLabel(result.deadlockLabel.get())) { + result.deadlockLabel->push_back('_'); + } + components.stateLabeling.addLabel(result.deadlockLabel.get(), std::move(subDeadlockStates)); } transformModelSpecificComponents(originalModel, subsystemStates, components); diff --git a/src/storm/transformer/SubsystemBuilder.h b/src/storm/transformer/SubsystemBuilder.h index cf7aefaaf..8418b09dc 100644 --- a/src/storm/transformer/SubsystemBuilder.h +++ b/src/storm/transformer/SubsystemBuilder.h @@ -21,6 +21,8 @@ namespace storm { std::vector newToOldActionIndexMapping; // marks the actions of the original model that are still available in the subsystem storm::storage::BitVector keptActions; + // If set, deadlock states have been introduced and have been assigned this label. + boost::optional deadlockLabel; }; struct SubsystemBuilderOptions {