Fix phiStates ignored in computeAllTransientProbabilities

[Copilot]

phiStates was passed to computeAllTransientProbabilities but never applied, causing probability mass to flow through states that violate the φ U ψ path condition. All states outside φ should be absorbing — only paths staying within phiStates until reaching psiStates are valid.

Changes

• SparseCtmcCslHelper::computeAllTransientProbabilities: Compute absorbingStates = ~phiStates | psiStates and call makeRowsAbsorbing on those states before uniformization. Also set their exit rates to 1, consistent with how psiStates were previously handled.

// Before: only psiStates made absorbing; phiStates unused
transposedMatrix.makeRowsAbsorbing(psiStates);

// After: non-phi states also absorbing, enforcing the phi U psi path condition
storm::storage::BitVector absorbingStates = ~phiStates | psiStates;
transposedMatrix.makeRowsAbsorbing(absorbingStates);
for (auto state : absorbingStates) {
    newRates[state] = storm::utility::one<ValueType>();
}

This matches the pattern already used in computeBoundedUntilProbabilities.

• Fixes Phistates never used: Is this a bug #542

[sjunges]

@copilot Add a test that failed without this change and does not fail with this change!

[Copilot]

@copilot Add a test that failed without this change and does not fail with this change!

Added TransientProbabilitiesWithPhiStates test in CtmcCslModelCheckerTest.cpp: it uses a 3-state chain (0→1→2→0) and verifies that when state 1 is excluded from phiStates, no probability reaches state 2 (since state 1 becomes absorbing). Without the fix, probability would flow freely to state 2. Also fixed the existing TransientProbabilities test to use phiStates=all — the old empty phiStates would have caused all states to be absorbing under the fixed code.

[sjunges]

I've reviewed this. Looks good. @volkm can you have a quick look?

[volkm]

Looks okay to me.

There is still the issue that all goal states are made absorbing, so only the "first front" of goal states will be considered. If there is a goal state s with successor s', then the probabilities for s' will be set to zero instead of the correct value. So maybe the function should just take absorbing states as argument anyway.
But this was originally used for only one paper anyway, so I think improving a bit is good.

[sjunges]

Should we instead remove this if there are still issues with this? I must say that I have a hard time to understand "all transient probabilities".

[volkm]

The goal was originally to compute the probability $P_{=?} [F^{= t} s]$ from the initial state but for all $s \in S$ in one go. For goal states we would compute $\leq t$ instead of $=t$ by making them absorbing.

My suggestion would be to replace phiStates and psiStates by absorbingStates in the function header. Then it should be correct.

[sjunges]

with an assertion that the states are in fact absorbing?

[volkm]

No, I would still make them absorbing in the function (as we currently do). The name "absorbing" is not a good name then, maybe use "goalStates" instead?

[tquatmann]

implicitlyAbsorbingStates maybe?