component ComponentIsNonDeterministic
{
  provides I pp;
  
  behaviour
  {
    [true] on pp.ia(): pp.oa();
    [true] on pp.ia(): pp.ob();
  }

  // Verifying model ComponentIsNonDeterministic =>
  //   Component ComponentIsNonDeterministic is non-deterministic due to overlapping guards
  // For trace
  //   pp.ia
}

interface I
{
  in void ia();
  out void oa();
  out void ob();
  
  behaviour
  {
    on ia: oa;
    on ia: ob;
  }
}