fixes for new goal state merger

src/storm/transformer/GoalStateMerger.cpp

@@ -75,11 +75,11 @@ namespace storm {
                         stateIsDeadlock = false;
                         result.keptChoices.set(row, true);
                         transitionCount += transitionsToMaybeStates;
-                        if(hasTransitionToTarget) {
+                        if (hasTransitionToTarget) {
                             ++transitionCount;
                             targetStateRequired = true;
                         }
-                        if(hasTransitionToSink) {
+                        if (hasTransitionToSink) {
                             ++transitionCount;
                             sinkStateRequired = true;
                         }
@@ -90,14 +90,14 @@ namespace storm {
             }
             
             // Treat the target and sink states (if these states will exist)
-            if(targetStateRequired) {
+            if (targetStateRequired) {
                 result.targetState = stateCount;
                 ++stateCount;
                 ++transitionCount;
                 storm::utility::vector::setVectorValues(result.oldToNewStateIndexMapping, targetStates, *result.targetState);
             }
             
-            if(sinkStateRequired) {
+            if (sinkStateRequired) {
                 result.sinkState = stateCount;
                 ++stateCount;
                 ++transitionCount;
@@ -116,7 +116,7 @@ namespace storm {
             uint_fast64_t rowCount = resultData.keptChoices.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0);
             uint_fast64_t maybeStateCount = maybeStates.getNumberOfSetBits();
             uint_fast64_t stateCount = maybeStateCount + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0);
-            storm::storage::SparseMatrixBuilder<typename SparseModelType::ValueType> builder(rowCount, stateCount, transitionCount, true, origMatrix.hasTrivialRowGrouping(), origMatrix.hasTrivialRowGrouping() ? 0 : stateCount);
+             storm::storage::SparseMatrixBuilder<typename SparseModelType::ValueType> builder(rowCount, stateCount, transitionCount, true, !origMatrix.hasTrivialRowGrouping(), origMatrix.hasTrivialRowGrouping() ? 0 : stateCount);
             
             uint_fast64_t currRow = 0;
             for (auto state : maybeStates) {
@@ -138,10 +138,10 @@ namespace storm {
                             STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "There is a transition originating from a maybestate that does not lead to a maybe-, target-, or sinkstate.");
                         }
                     }
-                    if(targetValue) {
+                    if (targetValue) {
                         builder.addNextValue(currRow, *resultData.targetState, storm::utility::simplify(*targetValue));
                     }
-                    if(sinkValue) {
+                    if (sinkValue) {
                         builder.addNextValue(currRow, *resultData.sinkState, storm::utility::simplify(*sinkValue));
                     }
                     ++currRow;
@@ -149,13 +149,17 @@ namespace storm {
             }
             
             // Add the selfloops at target and sink
-            if(resultData.targetState) {
-                builder.newRowGroup(currRow);
+            if (resultData.targetState) {
+                if (!origMatrix.hasTrivialRowGrouping()) {
+                    builder.newRowGroup(currRow);
+                }
                 builder.addNextValue(currRow, *resultData.targetState, storm::utility::one<typename SparseModelType::ValueType>());
                 ++currRow;
             }
-            if(resultData.sinkState) {
-                builder.newRowGroup(currRow);
+            if (resultData.sinkState) {
+                if (!origMatrix.hasTrivialRowGrouping()) {
+                    builder.newRowGroup(currRow);
+                }
                 builder.addNextValue(currRow, *resultData.sinkState, storm::utility::one<typename SparseModelType::ValueType>());
                 ++currRow;
             }
@@ -173,10 +177,10 @@ namespace storm {
                 storm::storage::BitVector const& oldStatesWithLabel = originalModel.getStates(label);
                 storm::storage::BitVector newStatesWithLabel = oldStatesWithLabel % maybeStates;
                 newStatesWithLabel.resize(stateCount, false);
-                if (!oldStatesWithLabel.isDisjointFrom(targetStates)) {
+                if (!oldStatesWithLabel.isDisjointFrom(targetStates) && resultData.targetState.is_initialized()) {
                     newStatesWithLabel.set(*resultData.targetState, true);
                 }
-                if (!oldStatesWithLabel.isDisjointFrom(sinkStates)) {
+                if (!oldStatesWithLabel.isDisjointFrom(sinkStates) && resultData.sinkState.is_initialized()) {
                     newStatesWithLabel.set(*resultData.sinkState, true);
                 }
                 labeling.addLabel(label, std::move(newStatesWithLabel));
@@ -227,10 +231,10 @@ namespace storm {
                                 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "There is a transition reward originating from a maybestate that does not lead to a maybe-, target-, or sinkstate.");
                             }
                         }
-                        if(targetValue) {
+                        if (targetValue) {
                             builder.addNextValue(row, *resultData.targetState, storm::utility::simplify(*targetValue));
                         }
-                        if(sinkValue) {
+                        if (sinkValue) {
                             builder.addNextValue(row, *resultData.sinkState, storm::utility::simplify(*sinkValue));
                         }
                     }

src/storm/transformer/GoalStateMerger.h

@@ -37,7 +37,7 @@ namespace storm {
              *
              *  Notes:
              *  * the target (or sink) state is not created, if it is not reachable
-             *  * the target (or sink) state will get a label iff at least one of the given targetStates (sinkStates) have that label.
+             *  * 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.
              *  * Only the selected reward models will be kept. The target and sink states will not get any reward.
              *  * Choices that lead from a maybeState to a ~(target | sink) state will be removed. An exception is thrown if this leads to deadlocks.
              *  * It is assumed that maybeStates, targetStates, and sinkStates are pairwise disjoint. Otherwise an exception is thrown.

src/storm/transformer/SparseParametricDtmcSimplifier.cpp

@@ -42,7 +42,7 @@ namespace storm {
             this->simplifiedModel = mergerResult.model;
             statesWithProbability01.second = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
             if (mergerResult.targetState) {
-                statesWithProbability01.first.set(mergerResult.targetState.get(), true);
+                statesWithProbability01.second.set(mergerResult.targetState.get(), true);
             }
             std::string targetLabel = "target";
             while (this->simplifiedModel->hasLabel(targetLabel)) {
@@ -56,7 +56,14 @@ namespace storm {
             this->simplifiedFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(eventuallyFormula, formula.getOperatorInformation());
             
             // Eliminate all states for which all outgoing transitions are constant
-            this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel);
+            storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates();
+            if (mergerResult.targetState) {
+                considerForElimination.set(*mergerResult.targetState, false);
+            }
+            if (mergerResult.sinkState) {
+                considerForElimination.set(*mergerResult.sinkState, false);
+            }
+            this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination);
                 
             return true;
         }
@@ -90,7 +97,7 @@ namespace storm {
             
             // obtain the resulting subsystem
             storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
-            typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates);
+            typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, psiStates, prob0States);
             this->simplifiedModel = mergerResult.model;
             psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
             if (mergerResult.targetState) {
@@ -150,7 +157,14 @@ namespace storm {
             this->simplifiedFormula = std::make_shared<storm::logic::RewardOperatorFormula const>(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation);
             
             // Eliminate all states for which all outgoing transitions are constant
-            this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, rewardModelNameAsVector.front());
+            storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates();
+            if (mergerResult.targetState) {
+                considerForElimination.set(*mergerResult.targetState, false);
+            }
+            if (mergerResult.sinkState) {
+                considerForElimination.set(*mergerResult.sinkState, false);
+            }
+            this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination, rewardModelNameAsVector.front());
                 
             return true;
         }

src/storm/transformer/SparseParametricMdpSimplifier.cpp

@@ -47,9 +47,18 @@ namespace storm {
             storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
             typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first);
             this->simplifiedModel = mergerResult.model;
+            statesWithProbability01.first = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
+            if (mergerResult.sinkState) {
+                statesWithProbability01.first.set(mergerResult.sinkState.get(), true);
+            }
+            std::string sinkLabel = "sink";
+            while (this->simplifiedModel->hasLabel(sinkLabel)) {
+                sinkLabel = "_" + sinkLabel;
+            }
+            this->simplifiedModel->getStateLabeling().addLabel(sinkLabel, std::move(statesWithProbability01.first));
             statesWithProbability01.second = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
             if (mergerResult.targetState) {
-                statesWithProbability01.first.set(mergerResult.targetState.get(), true);
+                statesWithProbability01.second.set(mergerResult.targetState.get(), true);
             }
             std::string targetLabel = "target";
             while (this->simplifiedModel->hasLabel(targetLabel)) {
@@ -63,11 +72,18 @@ namespace storm {
             this->simplifiedFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(eventuallyFormula, formula.getOperatorInformation());
             
             // Eliminate all states for which all outgoing transitions are constant
-            this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel);
+            storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates();
+            if (mergerResult.targetState) {
+                considerForElimination.set(*mergerResult.targetState, false);
+            }
+            if (mergerResult.sinkState) {
+                considerForElimination.set(*mergerResult.sinkState, false);
+            }
+            this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination);
                         
             // Eliminate the end components that do not contain a target or a sink state (only required if the probability is maximized)
             if(!minimizing) {
-                this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates("target") | this->simplifiedModel->getStates("sink"));
+                this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates(targetLabel) | this->simplifiedModel->getStates(sinkLabel));
             }
             
             return true;
@@ -105,7 +121,7 @@ namespace storm {
             
             // obtain the resulting subsystem
             storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
-            typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates);
+            typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, psiStates, prob0States);
             this->simplifiedModel = mergerResult.model;
             psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
             if (mergerResult.targetState) {
@@ -156,6 +172,16 @@ namespace storm {
             storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
             typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector);
             this->simplifiedModel = mergerResult.model;
+            infinityStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
+            if (mergerResult.sinkState) {
+                infinityStates.set(mergerResult.sinkState.get(), true);
+            }
+            std::string sinkLabel = "sink";
+            while (this->simplifiedModel->hasLabel(sinkLabel)) {
+                sinkLabel = "_" + sinkLabel;
+            }
+            this->simplifiedModel->getStateLabeling().addLabel(sinkLabel, std::move(infinityStates));
+
             targetStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
             if (mergerResult.targetState) {
                 targetStates.set(mergerResult.targetState.get(), true);
@@ -172,11 +198,18 @@ namespace storm {
             this->simplifiedFormula = std::make_shared<storm::logic::RewardOperatorFormula const>(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation);
             
             // Eliminate all states for which all outgoing transitions are constant
-            this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, rewardModelNameAsVector.front());
+            storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates();
+            if (mergerResult.targetState) {
+                considerForElimination.set(*mergerResult.targetState, false);
+            }
+            if (mergerResult.sinkState) {
+                considerForElimination.set(*mergerResult.sinkState, false);
+            }
+            this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination, rewardModelNameAsVector.front());
             
             // Eliminate the end components in which no reward is collected (only required if rewards are minimized)
             if (minimizing) {
-                this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates("target") | this->simplifiedModel->getStates("sink"), rewardModelNameAsVector.front());
+                this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates(targetLabel) | this->simplifiedModel->getStates(sinkLabel), rewardModelNameAsVector.front());
             }
             return true;
         }

src/storm/transformer/SparseParametricModelSimplifier.cpp

@@ -97,15 +97,9 @@ namespace storm {
         }
         
         template<typename SparseModelType>
-         std::shared_ptr<SparseModelType> SparseParametricModelSimplifier<SparseModelType>::eliminateConstantDeterministicStates(SparseModelType const& model, boost::optional<std::string> const& rewardModelName) {
+         std::shared_ptr<SparseModelType> SparseParametricModelSimplifier<SparseModelType>::eliminateConstantDeterministicStates(SparseModelType const& model, storm::storage::BitVector const& consideredStates, boost::optional<std::string> const& rewardModelName) {
             storm::storage::SparseMatrix<typename SparseModelType::ValueType> const& sparseMatrix = model.getTransitionMatrix();
             
-            // Get the states without any label
-            storm::storage::BitVector considerForElimination(model.getNumberOfStates(), false);
-            for(auto const& label : model.getStateLabeling().getLabels()) {
-                considerForElimination |= model.getStateLabeling().getStates(label);
-            }
-            considerForElimination.complement();
                             
             // get the action-based reward values
             std::vector<typename SparseModelType::ValueType> actionRewards;
@@ -116,8 +110,8 @@ namespace storm {
             }
             
             // Find the states that are to be eliminated
-            storm::storage::BitVector selectedStates = considerForElimination;
-            for (auto state : considerForElimination) {
+            storm::storage::BitVector selectedStates = consideredStates;
+            for (auto state : consideredStates) {
                 if (sparseMatrix.getRowGroupSize(state) == 1 && (!rewardModelName.is_initialized() || storm::utility::isConstant(actionRewards[sparseMatrix.getRowGroupIndices()[state]]))) {
                     for (auto const& entry : sparseMatrix.getRowGroup(state)) {
                         if(!storm::utility::isConstant(entry.getValue())) {

src/storm/transformer/SparseParametricModelSimplifier.h

@@ -56,9 +56,10 @@ namespace storm {
              * * there is no statelabel defined, and
              * * (if rewardModelName is given) the reward collected at the state is constant.
              *
-             * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given)
+             * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given).
+             * Labelings of eliminated states will be lost
              */
-            static std::shared_ptr<SparseModelType> eliminateConstantDeterministicStates(SparseModelType const& model, boost::optional<std::string> const& rewardModelName = boost::none);
+            static std::shared_ptr<SparseModelType> eliminateConstantDeterministicStates(SparseModelType const& model,  storm::storage::BitVector const& consideredStates, boost::optional<std::string> const& rewardModelName = boost::none);
             
             SparseModelType const& originalModel;