Incorrect minimal conditional probabilities.

[tquatmann]

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.