From b7aaf1957e153734be532be2370a2704b1832106 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 26 Apr 2017 11:15:14 +0200 Subject: [PATCH] Replaced the StateDuplicator with the new memory structure product --- .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 2 +- .../pcaa/SparsePcaaPreprocessor.cpp | 199 ++++++++++-------- .../pcaa/SparsePcaaPreprocessor.h | 12 +- 3 files changed, 122 insertions(+), 91 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 8ae1c8498..e2cce333d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -108,7 +108,7 @@ namespace storm { result.toMS = this->model.getTransitionMatrix().getSubmatrix(true, result.states, this->model.getMarkovianStates(), createMS); result.toPS = this->model.getTransitionMatrix().getSubmatrix(true, result.states, probabilisticStates, false); STORM_LOG_ASSERT(result.getNumberOfStates() == result.states.getNumberOfSetBits() && result.getNumberOfStates() == result.toMS.getRowGroupCount() && result.getNumberOfStates() == result.toPS.getRowGroupCount(), "Invalid state count for subsystem"); - STORM_LOG_ASSERT(result.getNumberOfChoices() == result.choices.getNumberOfSetBits() && result.getNumberOfChoices() == result.toMS.getRowCount() && result.getNumberOfChoices() == result.toPS.getRowCount(), "Invalid state count for subsystem"); + STORM_LOG_ASSERT(result.getNumberOfChoices() == result.choices.getNumberOfSetBits() && result.getNumberOfChoices() == result.toMS.getRowCount() && result.getNumberOfChoices() == result.toPS.getRowCount(), "Invalid choice count for subsystem"); result.weightedRewardVector.resize(result.getNumberOfChoices()); storm::utility::vector::selectVectorValues(result.weightedRewardVector, result.choices, weightedRewardVector); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp index 9e5474362..506bb1ee8 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp @@ -6,7 +6,8 @@ #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/storage/MaximalEndComponentDecomposition.h" -#include "storm/transformer/StateDuplicator.h" +#include "storm/storage/memorystructure/MemoryStructureBuilder.h" +#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" #include "storm/transformer/SubsystemBuilder.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" @@ -26,12 +27,12 @@ namespace storm { result.newToOldStateIndexMapping = storm::utility::vector::buildVectorForRange(0, originalModel.getNumberOfStates()); //Invoke preprocessing on the individual objectives - for(auto const& subFormula : originalFormula.getSubformulas()){ + for (auto const& subFormula : originalFormula.getSubformulas()){ STORM_LOG_INFO("Preprocessing objective " << *subFormula<< "."); result.objectives.emplace_back(); PcaaObjective& currentObjective = result.objectives.back(); currentObjective.originalFormula = subFormula; - if(currentObjective.originalFormula->isOperatorFormula()) { + if (currentObjective.originalFormula->isOperatorFormula()) { preprocessOperatorFormula(currentObjective.originalFormula->asOperatorFormula(), result, currentObjective); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported"); @@ -40,11 +41,11 @@ namespace storm { // Set the query type. In case of a quantitative query, also set the index of the objective to be optimized. // Note: If there are only zero (or one) objectives left, we should not consider a pareto query! storm::storage::BitVector objectivesWithoutThreshold(result.objectives.size()); - for(uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) { + for (uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) { objectivesWithoutThreshold.set(objIndex, !result.objectives[objIndex].threshold); } uint_fast64_t numOfObjectivesWithoutThreshold = objectivesWithoutThreshold.getNumberOfSetBits(); - if(numOfObjectivesWithoutThreshold == 0) { + if (numOfObjectivesWithoutThreshold == 0) { result.queryType = ReturnType::QueryType::Achievability; } else if (numOfObjectivesWithoutThreshold == 1) { result.queryType = ReturnType::QueryType::Quantitative; @@ -64,9 +65,9 @@ namespace storm { //Get actions to which a positive or negative reward is assigned for at least one objective result.actionsWithPositiveReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); result.actionsWithNegativeReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); - for(uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) { - if(!result.objectives[objIndex].upperTimeBound) { - if(result.objectives[objIndex].rewardsArePositive) { + for (uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) { + if (!result.objectives[objIndex].upperTimeBound) { + if (result.objectives[objIndex].rewardsArePositive) { result.actionsWithPositiveReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); } else { result.actionsWithNegativeReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); @@ -77,7 +78,7 @@ namespace storm { // Analyze End components and ensure reward finiteness. // Note that this is only necessary if there is at least one objective with no upper time bound for (auto const& obj : result.objectives) { - if(!obj.upperTimeBound) { + if (!obj.upperTimeBound) { auto backwardTransitions = result.preprocessedModel.getBackwardTransitions(); analyzeEndComponents(result, backwardTransitions); ensureRewardFiniteness(result, backwardTransitions); @@ -89,13 +90,36 @@ namespace storm { template void SparsePcaaPreprocessor::updatePreprocessedModel(ReturnType& result, SparseModelType& newPreprocessedModel, std::vector& newToOldStateIndexMapping) { result.preprocessedModel = std::move(newPreprocessedModel); - // the given newToOldStateIndexMapping reffers to the indices of the former preprocessedModel as 'old indices' - for(auto & preprocessedModelStateIndex : newToOldStateIndexMapping){ + // the given newToOldStateIndexMapping refers to the indices of the former preprocessedModel as 'old indices' + for (auto & preprocessedModelStateIndex : newToOldStateIndexMapping){ preprocessedModelStateIndex = result.newToOldStateIndexMapping[preprocessedModelStateIndex]; } result.newToOldStateIndexMapping = std::move(newToOldStateIndexMapping); } + template + void SparsePcaaPreprocessor::addMemoryToPreprocessedModel(ReturnType& result, storm::storage::MemoryStructure& memory) { + storm::storage::SparseModelMemoryProduct product = memory.product(result.preprocessedModel); + auto newModel = product.build(); + + // update the newToOldStateIndexMapping + std::vector updatedMapping; + updatedMapping.reserve(newModel->getNumberOfStates()); + for (uint_fast64_t oldState = 0; oldState < result.preprocessedModel.getNumberOfStates(); ++oldState) { + for (uint_fast64_t memoryState = 0; memoryState < memory.getNumberOfStates(); ++memoryState) { + uint_fast64_t const& newState = product.getResultState(oldState, memoryState); + // Check if the state actually exists in the new model + if (newState < newModel->getNumberOfStates()) { + assert(newState == updatedMapping.size()); + updatedMapping.push_back(result.newToOldStateIndexMapping[oldState]); + } + } + } + + result.preprocessedModel = std::move(dynamic_cast(*newModel)); + result.newToOldStateIndexMapping = std::move(updatedMapping); + } + template void SparsePcaaPreprocessor::preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { @@ -110,7 +134,7 @@ namespace storm { currentObjective.rewardsArePositive = true; bool formulaMinimizes = false; - if(formula.hasBound()) { + if (formula.hasBound()) { currentObjective.threshold = formula.template getThresholdAs(); currentObjective.thresholdIsStrict = storm::logic::isStrict(formula.getBound().comparisonType); //Note that we minimize for upper bounds since we are looking for the EXISTENCE of a satisfying scheduler @@ -120,25 +144,25 @@ namespace storm { } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize"); } - if(formulaMinimizes) { + 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()){ + if (formula.isProbabilityOperatorFormula()){ preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), result, currentObjective); - } else if(formula.isRewardOperatorFormula()){ + } else if (formula.isRewardOperatorFormula()){ preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), result, currentObjective); - } else if(formula.isTimeOperatorFormula()){ + } else if (formula.isTimeOperatorFormula()){ preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), result, currentObjective); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported"); } // Transform the threshold for the preprocessed Model - if(currentObjective.threshold) { + if (currentObjective.threshold) { currentObjective.threshold = (currentObjective.threshold.get() - currentObjective.toOriginalValueTransformationOffset) / currentObjective.toOriginalValueTransformationFactor; } } @@ -146,13 +170,13 @@ namespace storm { template void SparsePcaaPreprocessor::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - if(formula.getSubformula().isUntilFormula()){ + if (formula.getSubformula().isUntilFormula()){ preprocessUntilFormula(formula.getSubformula().asUntilFormula(), result, currentObjective); - } else if(formula.getSubformula().isBoundedUntilFormula()){ + } else if (formula.getSubformula().isBoundedUntilFormula()){ preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), result, currentObjective); - } else if(formula.getSubformula().isGloballyFormula()){ + } else if (formula.getSubformula().isGloballyFormula()){ preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), result, currentObjective); - } else if(formula.getSubformula().isEventuallyFormula()){ + } else if (formula.getSubformula().isEventuallyFormula()){ preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); @@ -165,11 +189,11 @@ namespace storm { STORM_LOG_THROW((formula.hasRewardModelName() && result.preprocessedModel.hasRewardModel(formula.getRewardModelName())) || result.preprocessedModel.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "The reward model is not unique and the formula " << formula << " does not specify a reward model."); - if(formula.getSubformula().isEventuallyFormula()){ + if (formula.getSubformula().isEventuallyFormula()){ preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective, formula.getOptionalRewardModelName()); - } else if(formula.getSubformula().isCumulativeRewardFormula()) { + } else if (formula.getSubformula().isCumulativeRewardFormula()) { preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), result, currentObjective, formula.getOptionalRewardModelName()); - } else if(formula.getSubformula().isTotalRewardFormula()) { + } else if (formula.getSubformula().isTotalRewardFormula()) { preprocessTotalRewardFormula(result, currentObjective, formula.getOptionalRewardModelName()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); @@ -181,7 +205,7 @@ namespace storm { // Time formulas are only supported for Markov automata STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata."); - if(formula.getSubformula().isEventuallyFormula()){ + if (formula.getSubformula().isEventuallyFormula()){ preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); @@ -190,37 +214,39 @@ namespace storm { template void SparsePcaaPreprocessor::preprocessUntilFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - CheckTask phiTask(formula.getLeftSubformula()); - CheckTask psiTask(formula.getRightSubformula()); - storm::modelchecker::SparsePropositionalModelChecker mc(result.preprocessedModel); - STORM_LOG_THROW(mc.canHandle(phiTask) && mc.canHandle(psiTask), storm::exceptions::InvalidPropertyException, "The subformulas of " << formula << " should be propositional."); - storm::storage::BitVector phiStates = mc.check(phiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - storm::storage::BitVector psiStates = mc.check(psiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - if(!(psiStates & result.preprocessedModel.getInitialStates()).empty() && !currentObjective.lowerTimeBound) { + // Create a memory structure that stores whether a PhiState or a PsiState has already been reached + storm::storage::MemoryStructureBuilder builder(2); + // Get a unique label that is not already present in the model + std::string memoryLabel = "obj" + std::to_string(result.objectives.size()); + while (result.preprocessedModel.hasLabel(memoryLabel)) memoryLabel = "_" + memoryLabel; + builder.setLabel(0, memoryLabel); + 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, std::make_shared(true)); + storm::storage::MemoryStructure memory = builder.build(); + addMemoryToPreprocessedModel(result, memory); + + // build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from a memoryLabel-state to a psiState + storm::storage::BitVector const& statesWithMemoryLabel = result.preprocessedModel.getStates(memoryLabel); + if ((statesWithMemoryLabel & result.preprocessedModel.getInitialStates()).empty() && !currentObjective.lowerTimeBound) { // The probability is always one as the initial state is a target state. // For this special case, the transformation to an expected reward objective fails. - // We could handle this with further preprocessing steps but as this case is boring anyway, we simply reject the input. - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The Probability for the objective " << currentObjective.originalFormula << " is always one as the rhs of the until formula is true in the initial state. Please omit this objective."); - } - - auto duplicatorResult = storm::transformer::StateDuplicator::transform(result.preprocessedModel, ~phiStates | psiStates); - updatePreprocessedModel(result, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping); - - storm::storage::BitVector newPsiStates(result.preprocessedModel.getNumberOfStates(), false); - for(auto const& oldPsiState : psiStates){ - //note that psiStates are always located in the second copy - newPsiStates.set(duplicatorResult.secondCopyOldToNewStateIndexMapping[oldPsiState], true); + // We could handle this with further preprocessing steps but as this case is trivial anyway, we reject the input. + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The Probability for the objective " << *currentObjective.originalFormula << " is always one as the rhs of the until formula is true in the initial state. Please omit this objective."); } + storm::modelchecker::SparsePropositionalModelChecker mc(result.preprocessedModel); + storm::storage::BitVector psiStates = mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); - // build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from the firstCopy to a psiState std::vector objectiveRewards(result.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); - for (auto const& firstCopyState : duplicatorResult.firstCopy) { - for (uint_fast64_t row = result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[firstCopyState]; row < result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[firstCopyState + 1]; ++row) { - objectiveRewards[row] = result.preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, newPsiStates); + for (auto const& state : statesWithMemoryLabel) { + for (uint_fast64_t row = result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; row < result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) { + objectiveRewards[row] = result.preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, psiStates); } } - if(!currentObjective.rewardsArePositive) { + if (!currentObjective.rewardsArePositive) { storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one()); } result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards)); @@ -258,43 +284,48 @@ namespace storm { template void SparsePcaaPreprocessor::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { - if(formula.isReachabilityProbabilityFormula()){ + if (formula.isReachabilityProbabilityFormula()){ preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), result, currentObjective); 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 memoryLabel = "obj" + std::to_string(result.objectives.size()); + while (result.preprocessedModel.hasLabel(memoryLabel)) memoryLabel = "_" + memoryLabel; + builder.setLabel(0, memoryLabel); + 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 memory = builder.build(); + addMemoryToPreprocessedModel(result, memory); - CheckTask targetTask(formula.getSubformula()); - storm::modelchecker::SparsePropositionalModelChecker mc(result.preprocessedModel); - STORM_LOG_THROW(mc.canHandle(targetTask), storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " should be propositional."); - storm::storage::BitVector targetStates = mc.check(targetTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - - auto duplicatorResult = storm::transformer::StateDuplicator::transform(result.preprocessedModel, targetStates); - updatePreprocessedModel(result, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping); - - // Add a reward model that gives zero reward to the actions of states of the second copy. + // Add a reward model that only gives reward to states with the memory label RewardModelType objectiveRewards(boost::none); - if(formula.isReachabilityRewardFormula()) { + if (formula.isReachabilityRewardFormula()) { + storm::storage::BitVector statesWithoutMemoryLabel = ~result.preprocessedModel.getStates(memoryLabel); objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); - if(objectiveRewards.hasStateRewards()) { - storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), duplicatorResult.secondCopy, storm::utility::zero()); + if (objectiveRewards.hasStateRewards()) { + storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), statesWithoutMemoryLabel, storm::utility::zero()); } - if(objectiveRewards.hasStateActionRewards()) { - for(auto secondCopyState : duplicatorResult.secondCopy) { - std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[secondCopyState], result.preprocessedModel.getTransitionMatrix().getRowGroupSize(secondCopyState), storm::utility::zero()); + if (objectiveRewards.hasStateActionRewards()) { + for (auto state : statesWithoutMemoryLabel) { + std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state], result.preprocessedModel.getTransitionMatrix().getRowGroupSize(state), storm::utility::zero()); } } - } else if(formula.isReachabilityTimeFormula() && result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton)) { + } else if (formula.isReachabilityTimeFormula() && result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton)) { objectiveRewards = RewardModelType(std::vector(result.preprocessedModel.getNumberOfStates(), storm::utility::zero())); - storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), dynamic_cast*>(&result.preprocessedModel)->getMarkovianStates() & duplicatorResult.firstCopy, storm::utility::one()); + storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), dynamic_cast*>(&result.preprocessedModel)->getMarkovianStates() & result.preprocessedModel.getStates(memoryLabel), storm::utility::one()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported."); } - if(!currentObjective.rewardsArePositive){ - if(objectiveRewards.hasStateRewards()) { + if (!currentObjective.rewardsArePositive){ + if (objectiveRewards.hasStateRewards()) { storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one()); } - if(objectiveRewards.hasStateActionRewards()) { + if (objectiveRewards.hasStateActionRewards()) { storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one()); } } @@ -309,11 +340,11 @@ namespace storm { RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); - if(!currentObjective.rewardsArePositive){ - if(objectiveRewards.hasStateRewards()) { + if (!currentObjective.rewardsArePositive){ + if (objectiveRewards.hasStateRewards()) { storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one()); } - if(objectiveRewards.hasStateActionRewards()) { + if (objectiveRewards.hasStateActionRewards()) { storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one()); } } @@ -324,11 +355,11 @@ namespace storm { void SparsePcaaPreprocessor::preprocessTotalRewardFormula(ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); - if(!currentObjective.rewardsArePositive){ - if(objectiveRewards.hasStateRewards()) { + if (!currentObjective.rewardsArePositive){ + if (objectiveRewards.hasStateRewards()) { storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one()); } - if(objectiveRewards.hasStateActionRewards()) { + if (objectiveRewards.hasStateActionRewards()) { storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one()); } } @@ -344,9 +375,9 @@ namespace storm { auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition(result.preprocessedModel.getTransitionMatrix(), backwardTransitions); STORM_LOG_ASSERT(!mecDecomposition.empty(), "Empty maximal end component decomposition."); ecs.reserve(mecDecomposition.size()); - for(auto& mec : mecDecomposition) { - for(auto const& stateActionsPair : mec) { - for(auto const& action : stateActionsPair.second) { + for (auto& mec : mecDecomposition) { + for (auto const& stateActionsPair : mec) { + for (auto const& action : stateActionsPair.second) { result.ecActions.set(action); } } @@ -356,17 +387,17 @@ namespace storm { result.possiblyRecurrentStates = storm::storage::BitVector(result.preprocessedModel.getNumberOfStates(), false); storm::storage::BitVector neutralActions = ~(result.actionsWithNegativeReward | result.actionsWithPositiveReward); storm::storage::BitVector statesInCurrentECWithNeutralAction(result.preprocessedModel.getNumberOfStates(), false); - for(uint_fast64_t ecIndex = 0; ecIndex < ecs.size(); ++ecIndex) { //we will insert new ecs in the vector (thus no iterators for the loop) + for (uint_fast64_t ecIndex = 0; ecIndex < ecs.size(); ++ecIndex) { //we will insert new ecs in the vector (thus no iterators for the loop) bool currentECIsNeutral = true; - for(auto const& stateActionsPair : ecs[ecIndex]) { + for (auto const& stateActionsPair : ecs[ecIndex]) { bool stateHasNeutralActionWithinEC = false; - for(auto const& action : stateActionsPair.second) { + for (auto const& action : stateActionsPair.second) { stateHasNeutralActionWithinEC |= neutralActions.get(action); } statesInCurrentECWithNeutralAction.set(stateActionsPair.first, stateHasNeutralActionWithinEC); currentECIsNeutral &= stateHasNeutralActionWithinEC; } - if(currentECIsNeutral) { + if (currentECIsNeutral) { result.possiblyRecurrentStates |= statesInCurrentECWithNeutralAction; }else{ // Check if the ec contains neutral sub ecs. This is done by adding the subECs to our list of ECs @@ -374,7 +405,7 @@ namespace storm { statesInCurrentECWithNeutralAction = storm::utility::graph::performProb0E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions,statesInCurrentECWithNeutralAction, ~statesInCurrentECWithNeutralAction); auto subECs = storm::storage::MaximalEndComponentDecomposition(result.preprocessedModel.getTransitionMatrix(), backwardTransitions, statesInCurrentECWithNeutralAction); ecs.reserve(ecs.size() + subECs.size()); - for(auto& ec : subECs){ + for (auto& ec : subECs){ ecs.push_back(std::move(ec)); } } @@ -390,7 +421,7 @@ namespace storm { storm::storage::BitVector statesReachingNegativeRewardsFinitelyOftenForSomeScheduler = storm::utility::graph::performProb1E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions, storm::storage::BitVector(result.preprocessedModel.getNumberOfStates(), true), result.possiblyRecurrentStates); STORM_LOG_THROW(!(statesReachingNegativeRewardsFinitelyOftenForSomeScheduler & result.preprocessedModel.getInitialStates()).empty(), storm::exceptions::InvalidPropertyException, "Infinite Rewards: For every scheduler, the induced reward for one or more of the objectives that minimize rewards is infinity."); - if(!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) { + if (!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) { // Remove the states that for any scheduler have one objective with infinite expected reward. auto subsystemBuilderResult = storm::transformer::SubsystemBuilder::transform(result.preprocessedModel, statesReachingNegativeRewardsFinitelyOftenForSomeScheduler, storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), true)); updatePreprocessedModel(result, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h index fb35fa9d1..70e5a6018 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h @@ -6,6 +6,7 @@ #include "storm/logic/Formulas.h" #include "storm/storage/BitVector.h" #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h" +#include "storm/storage/memorystructure/MemoryStructure.h" namespace storm { namespace modelchecker { @@ -29,12 +30,6 @@ namespace storm { static ReturnType preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula); private: - /*! - * Initializes the returned Information - * @param originalModel The considered model - * @param originalFormula the considered formula - */ - static ReturnType initializeResult(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel); /*! * Updates the preprocessed model stored in the given result to the given model. @@ -43,6 +38,11 @@ namespace storm { */ static void updatePreprocessedModel(ReturnType& result, SparseModelType& newPreprocessedModel, std::vector& newToOldStateIndexMapping); + /*! + * Updates the preprocessed model stored in the given result to the product of the model and the given memory structure. + */ + static void addMemoryToPreprocessedModel(ReturnType& result, storm::storage::MemoryStructure& memory); + /*! * Apply the neccessary preprocessing for the given formula. * @param formula the current (sub)formula