Created attachment 311 [details] model showing the issue The following strategy: strategy Opt = minE (b) [<=1] : <> Proc.END || y>=1 should depend on concrete timing when Proc arrives at the decision and at least sometimes choose A.
I delegate this to Peter.