From e9bb791be10789698f7351015dae908d24fe528b Mon Sep 17 00:00:00 2001 From: Henri Saudubray Date: Thu, 2 Apr 2026 10:44:39 +0200 Subject: [PATCH] feat: final commit --- exm/main.zls | 55 ++++++++++++++++++++++++++++-------------------- justfile | 12 +++++++++++ lib/hsim/fill.ml | 24 ++++++++++++--------- 3 files changed, 58 insertions(+), 33 deletions(-) diff --git a/exm/main.zls b/exm/main.zls index 1cad532..cc17c0c 100644 --- a/exm/main.zls +++ b/exm/main.zls @@ -9,7 +9,7 @@ - Model discrete systems and their continuous environment - Research language, design space for hybrid system modelers - Compilation to OCaml, execution with an off-the-shelf ODE solver - - Developed by the Inria PARKAS team *) + - Developed by M. Pouzet and T. Bourke in the Inria PARKAS team *) @@ -20,6 +20,24 @@ + +(** Plan: + + - Zélus, the synchronous part + - Physical simulation, ODEs, and ODE solvers + - Zélus, the hybrid part + - Mixing discrete and continuous time, zero-crossing detection + - Informal operational semantics + - Low-level representation and runtime *) + + + + + + + + + (** Synchronous language kernel _à la_ Lustre: - programs are Mealy machines (outputs on each transition) - variables represent streams of values in time *) @@ -27,9 +45,9 @@ let node incr x = y where y = x + 1 -(* x │ 8 3 2 7 5 3 … - ───┼───────────────────── - y │ 9 4 3 8 6 4 … *) +(* x │ 8 3 2 7 5 3 … + ────────┼───────────────────── + incr x │ 9 4 3 8 6 4 … *) @@ -45,6 +63,7 @@ let node accumulate x = z where ──────────────┼───────────────────── pre x │ 1 2 5 2 5 … 0 -> x │ 0 2 5 2 5 3 … + 0 -> pre x │ 0 1 2 5 2 5 … accumulate x │ 1 3 8 10 15 18 … *) let node fib () = n where @@ -52,7 +71,6 @@ let node fib () = n where (** - causality loops are forbidden ([rec x = x]) *) - (** - we can reset streams at will *) let node stay x = y where (* output the first value forever *) @@ -77,11 +95,10 @@ let node loop x = y where -(** Math/physics reminder! +(** Calculus reminder: - Ordinary differential equations (ODEs), initial value problems - - Zero-crossing event basics - - Background on solvers *) + - A little background on solvers *) @@ -94,6 +111,7 @@ let node loop x = y where let dt = 0.01 (* 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) @@ -112,12 +130,11 @@ let node bouncing_ball (p0, v0) = p where - (** Cumbersome, and error-prone! *) let node sincos () = (sin, cos) where - rec sin = f_integr(0.0, cos) - and cos = f_integr(1.0, -. sin) + rec sin = f_integr (0.0, cos) (** [(dsin/dt) t = cos t, sin 0 = 0] *) + and cos = f_integr (1.0, -. sin) (** [(dcos/dt) t = -sin t, cos 0 = 1] *) @@ -136,10 +153,11 @@ let hybrid integr (x0, x') = x where let hybrid time () = t where der t = 1.0 init 0.0 -let hybrid position (p0, v0, a) = p where - rec der p = v init p0 - and der v = a init v0 +let hybrid falling_ball (p0, v0) = p where + rec der p = v init p0 + and der v = -. g init v0 +(** How do we mix discrete time and continuous time together? *) @@ -160,12 +178,3 @@ let hybrid time_bounces (p0, v0) = (p, b) where b = t -. last b done - - - - - - - - -(** - w FIXME e can mix discrete and continuous behaviours *) diff --git a/justfile b/justfile index 8ef5a92..45b91d3 100644 --- a/justfile +++ b/justfile @@ -2,10 +2,22 @@ exm1: timeout 1s dune exec exm_ball | \ feedgnuplot --stream --domain --lines +balld: + timeout 1s dune exec exm_ball | \ + feedgnuplot --stream --domain --lines + exm2: timeout 10s dune exec exm_sincos | \ feedgnuplot --stream --domain --lines +sincos: + timeout 10s dune exec exm_sincos | \ + feedgnuplot --stream --domain --lines + exm3: dune exec ballc.exe | \ feedgnuplot --stream --domain --lines + +ballc: + dune exec ballc.exe | \ + feedgnuplot --stream --domain --lines diff --git a/lib/hsim/fill.ml b/lib/hsim/fill.ml index ebe74b3..934fa03 100644 --- a/lib/hsim/fill.ml +++ b/lib/hsim/fill.ml @@ -1,19 +1,20 @@ [@@@warning "-27-50-69"] +let todo = assert false + + (* Little OCaml reminder: *) -type _s = A | B of int | C of float * string (* sum types *) -type _t = { a : int; b : int; } (* product types *) +type _t = { a : int; b : int; } let _f () = let x = { a = 0; b = 1 } in let y = { x with a = 2 } in (* same as "x", except field "a" *) assert (y = { a = 2; b = 1 }) -(* Everything is immutable, except explicitly declared record fields! *) -type _q = { c : int (* immutable *); mutable d : int; } +(* Everything is immutable (at least in this presentation)! *) + + -(* Types can be parameterized by other types: *) -type 'a _llist = Nil | Cons of { v : 'a; mutable next : 'a _llist } @@ -29,7 +30,7 @@ type ('i, 'o, 'r) dnode = (** Run a discrete node on a list of inputs *) let drun (DNode n : ('i, 'o, 'r) dnode) (i : 'i list) : 'o list = - snd (List.fold_left_map n.step n.state i) + todo @@ -153,7 +154,7 @@ let compose_solvers : ('y, 'yder) csolver -> let step (cstate, zstate) h = let cstate, y = csolver.step cstate h in let zstate, (h, z) = zsolver.step zstate y in - (cstate, zstate), ({ y with h }, z) in + (cstate, zstate), (todo (*?*), z) in let reset (cstate, zstate) (ivp, zcp) = (csolver.reset cstate ivp, zsolver.reset zstate zcp) in DNode { state; step; reset } @@ -206,12 +207,12 @@ let dstep (State ({ model = HNode m; solver = DNode s; _ } as state)) = else if state.time >= i.h then State { state with input = None; model; time = 0. } else - let y0 = m.cget ms and h = i.h -. state.time and ofs = (+.) state.time in + let y0 = todo (*?*) and h = i.h -. state.time and ofs = (+.) state.time in let ivp = { h; y0; fder = fun t y -> m.fder ms (ofs t) (i.f (ofs t)) y } in let zcp = { h; y0; fzer = fun t y -> m.fzer ms (ofs t) (i.f (ofs t)) y } in let solver = DNode { s with state = s.reset s.state (ivp, zcp) } in let input = Some { h; f = fun t -> i.f (ofs t) } in - State { model; solver; mode = C; time = 0.; input } in + State { model; solver; mode = todo (*?*); time = 0.; input } in state, Some { h = 0.; f = fun _ -> o } @@ -264,3 +265,6 @@ let hrun (model : ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode) if o = None then (sim, List.rev_map Option.get os) else step (o :: os) sim None in List.fold_left_map (step []) sim i |> snd |> List.flatten + + +