refined computation of conditional probs a bit. Sebastian, if you're reading this: shouldn't you be working? :)

Former-commit-id: 83f6dbb8d2

src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp

@@ -238,26 +238,47 @@ namespace storm {
                 }
                 probabilitiesToReachConditionStates.resize(beforeStateIndex);
 
-                uint_fast64_t normalStatesOffset = beforeStates.getNumberOfSetBits();
+                // If there were any before states, we can compute their conditional probabilities. If not, the result
+                // is undefined for all states.
+                std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::infinity<ValueType>());
+                if (targetStates.empty()) {
+                    storm::utility::vector::setVectorValues(result, beforeStates, storm::utility::zero<ValueType>());
+                } else if (!beforeStates.empty()) {
+                    // If there are some states for which the conditional probability is defined and there are some
+                    // states that can reach the target states without visiting condition states first, we need to
+                    // do more work.
+
+                    // First, compute the relevant states and some offsets.
                     storm::storage::BitVector allStates(targetStates.size(), true);
+                    std::vector<uint_fast64_t> numberOfBeforeStatesUpToState = beforeStates.getNumberOfSetBitsBeforeIndices();
                     storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, allStates, targetStates);
                     statesWithProbabilityGreater0 &= storm::utility::graph::getReachableStates(transitionMatrix, conditionStates, allStates, targetStates);
+                    uint_fast64_t normalStatesOffset = beforeStates.getNumberOfSetBits();
                     std::vector<uint_fast64_t> numberOfNormalStatesUpToState = statesWithProbabilityGreater0.getNumberOfSetBitsBeforeIndices();
                     
+                    // All transitions going to states with probability zero, need to be redirected to a deadlock state.
+                    bool addDeadlockState = false;
+                    uint_fast64_t deadlockState = normalStatesOffset + statesWithProbabilityGreater0.getNumberOfSetBits();
+
                     // Now, we create the matrix of 'before' and 'normal' states.
-                std::vector<uint_fast64_t> numberOfBeforeStatesUpToState = beforeStates.getNumberOfSetBitsBeforeIndices();
                     storm::storage::SparseMatrixBuilder<ValueType> builder;
-                uint_fast64_t currentRow = 0;
                     
                     // Start by creating the transitions of the 'before' states.
+                    uint_fast64_t currentRow = 0;
                     for (auto beforeState : beforeStates) {
                         if (conditionStates.get(beforeState)) {
                             // For condition states, we move to the 'normal' states.
+                            ValueType zeroProbability = storm::utility::zero<ValueType>();
                             for (auto const& successorEntry : transitionMatrix.getRow(beforeState)) {
                                 if (statesWithProbabilityGreater0.get(successorEntry.getColumn())) {
                                     builder.addNextValue(currentRow, normalStatesOffset + numberOfNormalStatesUpToState[successorEntry.getColumn()], successorEntry.getValue());
+                                } else {
+                                    zeroProbability += successorEntry.getValue();
                                 }
                             }
+                            if (!storm::utility::isZero(zeroProbability)) {
+                                builder.addNextValue(currentRow, deadlockState, zeroProbability);
+                            }
                         } else {
                             // For non-condition states, we scale the probabilities going to other before states.
                             for (auto const& successorEntry : transitionMatrix.getRow(beforeState)) {
@@ -270,7 +291,6 @@ namespace storm {
                     }
                     
                     // Then, create the transitions of the 'normal' states.
-                uint_fast64_t deadlockState = normalStatesOffset + statesWithProbabilityGreater0.getNumberOfSetBits();
                     for (auto state : statesWithProbabilityGreater0) {
                         ValueType zeroProbability = storm::utility::zero<ValueType>();
                         for (auto const& successorEntry : transitionMatrix.getRow(state)) {
@@ -281,11 +301,14 @@ namespace storm {
                             }
                         }
                         if (!storm::utility::isZero(zeroProbability)) {
+                            addDeadlockState = true;
                             builder.addNextValue(currentRow, deadlockState, zeroProbability);
                         }
                         ++currentRow;
                     }
+                    if (addDeadlockState) {
                         builder.addNextValue(deadlockState, deadlockState, storm::utility::one<ValueType>());
+                    }
                     
                     // Build the new transition matrix and the new targets.
                     storm::storage::SparseMatrix<ValueType> newTransitionMatrix = builder.build();
@@ -297,10 +320,9 @@ namespace storm {
                     
                     // Finally, compute the conditional probabiltities by a reachability query.
                     std::vector<ValueType> conditionalProbabilities = computeUntilProbabilities(newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), newTargetStates, qualitative, linearEquationSolverFactory);
-
-                // Unpack and return result.
-                std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::infinity<ValueType>());
                     storm::utility::vector::setVectorValues(result, beforeStates, conditionalProbabilities);
+                }
+
                 return result;
             }