Incorrect minimal conditional probabilities.

When computing Pmin=? [F x=2 || x=1] for the following PRISM Program, with Storm we get 0, although 0.3 should be correct.

mdp
module main
    x : [0..2];
    [] x=0 -> 0.7 : (x'=1) + 0.3 : (x'=2);
    [] x=1 -> 1 : (x'=1);
    [] x=2 -> 1 : (x'=1);
endmodule

Storm 1.8.2 (dev)

Date: Wed Feb 28 12:55:15 2024
Command line arguments: --prism conditional.nm -prop 'Pmin=? [F x=2 || F x=1 ]'
Current working directory: 

Time for model input parsing: 0.000s.

Time for model construction: 0.010s.

-------------------------------------------------------------- 
Model type:     MDP (sparse)
States:     3
Transitions:    4
Choices:    3
Reward Models:  none
State Labels:   4 labels
   * init -> 1 item(s)
   * deadlock -> 0 item(s)
   * (x = 2) -> 1 item(s)
   * (x = 1) -> 1 item(s)
Choice Labels:  none
-------------------------------------------------------------- 

Model checking property "1": Pmin=? [(F (x = 2)) || (F (x = 1))] ...
Result (for initial states): 0
Time for model checking: 0.000s.

The problem seems to be an incorrect reduction from minimizing to maximizing queries.

moves-rwth / storm

Incorrect minimal conditional probabilities. #509