diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 8ce496426..beaae1814 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -42,12 +42,13 @@ namespace storm { // Build a subsystem of the preprocessor result model 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 maybeStates = preprocessorResult.rewardLessInfinityEStates.get() & ~preprocessorResult.reward0AStates; + storm::storage::BitVector finiteRewardChoices = preprocessorResult.preprocessedModel->getTransitionMatrix().getRowFilter(preprocessorResult.rewardLessInfinityEStates.get(), preprocessorResult.rewardLessInfinityEStates.get()); std::set relevantRewardModels; for (auto const& obj : this->objectives) { obj.formula->gatherReferencedRewardModels(relevantRewardModels); } storm::transformer::GoalStateMerger merger(*preprocessorResult.preprocessedModel); - auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, preprocessorResult.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end())); + auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, preprocessorResult.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end()), finiteRewardChoices); // Initialize data specific for the considered model type initializeModelTypeSpecificData(*mergerResult.model); diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index 49497237e..7707bd3f1 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -24,10 +24,10 @@ namespace storm { } template - typename GoalStateMerger::ReturnType GoalStateMerger::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector const& selectedRewardModels) const { + typename GoalStateMerger::ReturnType GoalStateMerger::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector const& selectedRewardModels, boost::optional const& choiceFilter) const { STORM_LOG_THROW(maybeStates.isDisjointFrom(targetStates) && targetStates.isDisjointFrom(sinkStates) && sinkStates.isDisjointFrom(maybeStates), storm::exceptions::InvalidArgumentException, "maybestates, targetstates, and sinkstates are assumed to be disjoint when creating the submodel. However, this is not the case."); - auto result = initialize(maybeStates, targetStates, sinkStates); + auto result = initialize(maybeStates, targetStates, sinkStates, choiceFilter); auto transitionMatrix = buildTransitionMatrix(maybeStates, result.first, result.second); auto labeling = buildStateLabeling(maybeStates, targetStates, sinkStates, result.first); @@ -39,7 +39,7 @@ namespace storm { } template - std::pair::ReturnType, uint_fast64_t> GoalStateMerger::initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const { + std::pair::ReturnType, uint_fast64_t> GoalStateMerger::initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional const& choiceFilter) const { storm::storage::SparseMatrix const& origMatrix = originalModel.getTransitionMatrix(); @@ -58,33 +58,35 @@ namespace storm { for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) { uint_fast64_t transitionsToMaybeStates = 0; bool keepThisRow(true), hasTransitionToTarget(false), hasTransitionToSink(false); - for (auto const& entry : origMatrix.getRow(row)) { - if (maybeStates.get(entry.getColumn())) { - ++transitionsToMaybeStates; - } else if (targetStates.get(entry.getColumn())) { - hasTransitionToTarget = true; - } else if (sinkStates.get(entry.getColumn())) { - hasTransitionToSink = true; - } else { - keepThisRow = false; - break; - } - } - if (keepThisRow) { - stateIsDeadlock = false; - result.keptChoices.set(row, true); - transitionCount += transitionsToMaybeStates; - if (hasTransitionToTarget) { - ++transitionCount; - targetStateRequired = true; + if (!choiceFilter || choiceFilter.get().get(row)) { + for (auto const& entry : origMatrix.getRow(row)) { + if (maybeStates.get(entry.getColumn())) { + ++transitionsToMaybeStates; + } else if (targetStates.get(entry.getColumn())) { + hasTransitionToTarget = true; + } else if (sinkStates.get(entry.getColumn())) { + hasTransitionToSink = true; + } else { + keepThisRow = false; + break; + } } - if (hasTransitionToSink) { - ++transitionCount; - sinkStateRequired = true; + if (keepThisRow) { + stateIsDeadlock = false; + result.keptChoices.set(row, true); + transitionCount += transitionsToMaybeStates; + if (hasTransitionToTarget) { + ++transitionCount; + targetStateRequired = true; + } + if (hasTransitionToSink) { + ++transitionCount; + sinkStateRequired = true; + } } } - STORM_LOG_THROW(!stateIsDeadlock, storm::exceptions::InvalidArgumentException, "Merging goal states leads to deadlocks!"); } + STORM_LOG_THROW(!stateIsDeadlock, storm::exceptions::InvalidArgumentException, "Merging goal states leads to deadlocks!"); ++stateCount; } diff --git a/src/storm/transformer/GoalStateMerger.h b/src/storm/transformer/GoalStateMerger.h index bc9dadcda..f79a127a6 100644 --- a/src/storm/transformer/GoalStateMerger.h +++ b/src/storm/transformer/GoalStateMerger.h @@ -35,6 +35,8 @@ namespace storm { * * one target state to which all transitions to a state selected by targetStates are redirected and * * one sink state to which all transitions to a state selected by sinkStates are redirected. * + * If a choiceFilter is given, choices on maybestates that are not selected by the filter will be removed. + * * Notes: * * the target (or sink) state is not created, if it is not reachable * * the target (or sink) state will get a label iff it is reachable and at least one of the given targetStates (sinkStates) have that label. @@ -43,7 +45,7 @@ namespace storm { * * It is assumed that maybeStates, targetStates, and sinkStates are pairwise disjoint. Otherwise an exception is thrown. * * The order of the maybeStates will not be affected (i.e. s_1 < s_2 in the input model implies s'_1 < s'_2 in the output model). */ - ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector const& selectedRewardModels = std::vector()) const; + ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector const& selectedRewardModels = std::vector(), boost::optional const& choiceFilter = boost::none) const; private: SparseModelType const& originalModel; @@ -53,7 +55,7 @@ namespace storm { * * @return The initialized result and the number of transitions of the result model */ - std::pair initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const; + std::pair initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional const& choiceFilter = boost::none) const; /*! * Builds the transition matrix of the resulting model