let between(inf, x, sup:real): bool = inf <= x and x <= sup
let delta = 2.0
node env() returns(t1,t2: real; tc: real [-100.0; 100.0]; v1,v2,on:bool) =
  exist t: real [-100.0; 100.0] in
  exist B1, B2: real [-0.5; 0.5] in
    t1=t+B1 and t2=t+B2 and on = ( t1<tc and t2<tc )
  fby
    loop {
      |9: t1 = t + B1 and t2 = t + B2 and on = ( t1<tc and t2<tc )  and
          v1=true and v2=true and between(pre t-delta, t, pre t+delta)
      |1: t1 = t + B1 and t2 = t + B2 and on = false  and
          v1=false and v2=false and between(pre t-delta, t, pre t+delta)
    }

node oracle(on:bool; t1, t2, tc: real; v1, v2: bool) returns (ok:bool) =
  exist bruitT1, bruitT2: real [-0.5; 0.5] in
  loop
     ok = ( ( v1 => on=((t1+bruitT1) < tc ) ) and
          ( v2 => on=((t2+bruitT2)  < tc )) )