• API
• FAQ
• Tools
• Archive
daily pastebin goal
24%
SHARE
TWEET

# Untitled

a guest Apr 16th, 2018 48 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.

Top