Closed kleinj closed 7 years ago
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" ].
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
Fixed by the commit referenced above, now merged.
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" ]
.Manually restricting the MDP to the minimal strategy DTMC yields the expected results:
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