Parametric/exact Rmin: wrong result

[kleinj]

At https://groups.google.com/d/topic/prismmodelchecker/vQI-1srXSdk/discussion, Shalini Ghosh reported a small MDP with a strange result for an Rmin formula in the parametric engine. The model is attached.

The problematic formula is Rmin=?[ F "changed" ].

prism lanechange_mdp.prism -pf 'Rmin=?[F "changed" ]' --param p=0:1
Result (minimum expected reward): ([0.0,1.0]): { 1  | 2  }

prism lanechange_mdp.prism -pf 'Rmin=?[F "changed" ]' --exact --const p=0.626
Result (minimum expected reward): 1/2

prism lanechange_mdp_simple_parametric.prism -pf 'Rmin=?[F "changed" ]' --const p=0.626
Result: 1.002137421843802 (value in the initial state)

Manually restricting the MDP to the minimal strategy DTMC yields the expected results:

prism lanechange_dtmc.prism -pf 'R=?[F "changed" ]' --exact --param p=0:1
Result (expected reward): ([0.0,1.0]): { 2 p - 5  | 10 p - 10  }

prism lanechange_dtmc.prism -pf 'R=?[F "changed" ]' --exact --const p=0.626
Result (expected reward): 937/935

prism lanechange_dtmc.prism -pf 'R=?[F "changed" ]' --const p=0.626
Result: 1.0021390374331551 (value in the initial state)

Some preliminary debugging suggests that the precomputation for Rmin in the parametric/exact engine is the most probable culprit.

lanechange_mdp.prism.txt
lanechange_dtmc.prism.txt

[davexparker]

Fixed by the commit referenced above, now merged.