Interpretation of ProbUntil (Probability with U operator)

[lugino-emeritus]

Hello all,
I searched a lot and tested different models, but I'm not able to understand how ProbUntil works.

The following is a minimal example to see my problem:

minimal_test.zip

I want to get the probability that state ok is reached before state no. I thought this could be done with
Pr[<=100]((!Process.no) U (Process.ok))
while this works perfect in Prism (probability 0.7), in UPPAAL I have 72/72 successful runs with 5% CI. This does not makes sense as far as I understood the U operator defined in CTL.

Can someone explain me how UPPAAL interprets the U operator? I don't have Problems with <> or [].

Thanks in advance!

Note: I'm using UPPAAL 5.0.0 on Linux.