121 lines
2.5 KiB
Text
121 lines
2.5 KiB
Text
|
|
|
|
|
|
(** Zélus
|
|
|
|
Synchronous language kernel _à la_ Lustre:
|
|
- programs are Mealy machines (outputs on each transition)
|
|
- variables represent streams of values in time *)
|
|
|
|
let node incr x = y where
|
|
y = x + 1
|
|
|
|
(* x │ 8 3 2 7 5 3 …
|
|
───┼─────────────────────
|
|
y │ 9 4 3 8 6 4 … *)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** - we can use values of the previous instants (using [pre]) and
|
|
initialize streams (using [->]) *)
|
|
|
|
let node accumulate x = z where
|
|
rec w = pre x
|
|
and y = 0 -> pre x
|
|
and z = x -> (pre z) + x
|
|
|
|
(* x │ 1 2 5 2 5 3 …
|
|
───┼─────────────────────
|
|
w │ 1 2 5 2 5 …
|
|
y │ 0 1 2 5 2 5 …
|
|
z │ 1 3 8 10 15 18 … *)
|
|
|
|
|
|
|
|
(** - we can reset streams at will *)
|
|
|
|
let node stay x = y where (* output the first value forever *)
|
|
rec y = x -> pre y
|
|
|
|
let node from x = y where (* count up from the first value *)
|
|
rec y = x -> pre y + 1
|
|
|
|
let node loop x = y where
|
|
rec y = reset from 0 every z
|
|
and z = false -> pre y >= w
|
|
and w = stay x
|
|
|
|
(* x │ 2 _ _ _ _ _ …
|
|
────────┼─────────────────────
|
|
loop x │ 0 1 2 0 1 2 … *)
|
|
|
|
|
|
(** Already able to model physical behaviours! *)
|
|
|
|
let dt = 0.001 (* Integration step *)
|
|
let g = 9.81 (* Gravitational constant *)
|
|
let node f_integr (x0, x') = x where (* Forward Euler integrator *)
|
|
rec x = x0 -> pre (x +. x' *. dt)
|
|
let node b_integr (x0, x') = x where (* Backward Euler integrator *)
|
|
rec x = x0 -> (pre x) +. x' *. dt
|
|
|
|
let node bouncing_ball (p0, v0) = p where
|
|
rec p = reset f_integr (q, v) every z
|
|
and v = reset b_integr (w, -. g) every z
|
|
and q = p0 -> 0.0 and w = v0 -> -0.8 *. (pre v)
|
|
and z = false -> (pre p) < 0.0
|
|
|
|
(** Quite cumbersome. *)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** Enter continuous-time constructs:
|
|
- express values with initial value problems with [der] and [init] *)
|
|
|
|
let hybrid integr (x0, x') = x where
|
|
der x = x' init x0
|
|
|
|
let hybrid position (p0, v0, a) = p where
|
|
rec der p = v init p0
|
|
and der v = a init v0
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** We can intermingle discrete and continuous behaviours: *)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** We can now express physical systems much more precisely: *)
|
|
|
|
let hybrid bouncing_ball (p0, v0) = p where
|
|
rec der p = v init p0 reset z -> 0.0
|
|
and der v = -. g init v0 reset z -> -0.8 *. last v
|
|
and z = up(-. p)
|