Created attachment 281 [details]
Model with wrong results
Open the attached model
Verify the probability of reaching Process.GOAL - this is >= 0.9..
Use the model checker to check if Process.GOAL is reachable - FALSE
As SMC has made runs that hit Process.GOAL, Process.GOAL must be reachable.
I think in this model the model checker is not capable of verifying the model, and it should give an error message.
Tested in UPPAAL stratego and Uppaal 4.1.19 - none of them works
"E<> Process.GOAL" should refuse to verify such model in the first place.