Open
Description
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.