daily pastebin goal
78%
SHARE
TWEET

Untitled

a guest Apr 16th, 2018 47 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. let between(inf, x, sup:real): bool = inf <= x and x <= sup
  2. let delta = 2.0
  3. node env() returns(t1,t2: real; tc: real [-100.0; 100.0]; v1,v2,on:bool) =
  4.   exist t: real [-100.0; 100.0] in
  5.   exist B1, B2: real [-0.5; 0.5] in
  6.     t1=t+B1 and t2=t+B2 and on = ( t1<tc and t2<tc )
  7.   fby
  8.     loop {
  9.       |9: t1 = t + B1 and t2 = t + B2 and on = ( t1<tc and t2<tc )  and
  10.           v1=true and v2=true and between(pre t-delta, t, pre t+delta)
  11.       |1: t1 = t + B1 and t2 = t + B2 and on = false  and
  12.           v1=false and v2=false and between(pre t-delta, t, pre t+delta)
  13.     }
  14.  
  15. node oracle(on:bool; t1, t2, tc: real; v1, v2: bool) returns (ok:bool) =
  16.   exist bruitT1, bruitT2: real [-0.5; 0.5] in
  17.   loop
  18.      ok = ( ( v1 => on=((t1+bruitT1) < tc ) ) and
  19.           ( v2 => on=((t2+bruitT2)  < tc )) )
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top