// Bug fixed in SVN rev 11215
// Probabilities that reference state variables were not correctly
// translated in the transformation to a location-based model

pta

module M
  s : [0..2];
  x : clock;

  invariant
    true => x<=1
  endinvariant

  // ITE for probabilities
  [a] true & x=1 -> (s=0 ? 0.5 : 0.25):(s'=0)&(x'=0) + (s=0 ? 0.5 : 0.75):(s'=2)&(x'=0);

  // direct reference to state variable values in probabilities
  [b] s<=1 & x=1 -> (1-s):(s'=1)&(x'=0) + s:(s'=0)&(x'=0);

  // implicit probability (checks that 'null' probability is properly handled)
  [c] s=2 & x=1 -> (s'=2)&(x'=0);
endmodule