hms/hsim
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat (state): cleanup simulation state interface

Browse source
This commit is contained in:
Henri Saudubray 2025-04-23 10:47:46 +02:00
parent 200152b769
commit cc099c02e7
Signed by: hms
GPG key ID: 7065F57ED8856128
3 changed files with 118 additions and 128 deletions
Download patch file Download diff file Expand all files Collapse all files

2
hsim.opam
View file

@ -3,7 +3,7 @@ opam-version: "2.0"
synopsis: "An executable semantics for the simulation of hybrid systems" synopsis: "An executable semantics for the simulation of hybrid systems"
maintainer: ["henri.saudubray@proton.me"] maintainer: ["henri.saudubray@proton.me"]
authors: ["Henri Saudubray"] authors: ["Henri Saudubray"]
license: "GPL-3.0-or-later" license: "CeCILL-2.1-or-later"
homepage: "https://codeberg.org/17maiga/hsim" homepage: "https://codeberg.org/17maiga/hsim"
doc: "https://url/to/documentation" doc: "https://url/to/documentation"
bug-reports: "https://codeberg.org/17maiga/hsim/issues" bug-reports: "https://codeberg.org/17maiga/hsim/issues"

87
src/lib/hsim/sim.ml
View file

@ -26,27 +26,25 @@ module LazySim (S : SimState) =
(HNode model : ('p, 'a, 'b, 'y, 'yder, 'zin, 'zout) hnode) (HNode model : ('p, 'a, 'b, 'y, 'yder, 'zin, 'zout) hnode)
(DNode solver : ('y, 'yder, 'zin, 'zout) solver) (DNode solver : ('y, 'yder, 'zin, 'zout) solver)
: ('p, 'a, 'b) lazy_sim : ('p, 'a, 'b) lazy_sim
= let state = S.init ~mstate:model.state ~sstate:solver.state in = let state = S.get_init model.state solver.state in
let step state input = let step state input =
let mstate = S.mstate state and sstate = S.sstate state let mstate = S.get_mstate state and sstate = S.get_sstate state in
and status = S.status state in
match input, S.is_running state with match input, S.is_running state with
| Some input, _ -> | Some input, _ ->
let mode = Discrete and now = 0.0 and stop = input.length in let mode = Discrete and now = 0.0 and stop = input.length in
let status = S.running ~mode ~input ~now ~stop status in let state = S.set_running ~mode ~input ~now ~stop state in
let state = S.update ~status state in
None, state None, state
| None, false -> None, state | None, false -> None, state
| None, true -> | None, true ->
let input = S.input state and now = S.now state let input = S.get_input state and now = S.get_now state
and stop = S.stop state in and stop = S.get_stop state in
match S.mode state with match S.get_mode state with
| Discrete -> | Discrete ->
let o, mstate = model.step mstate (input.u now) in let o, mstate = model.step mstate (input.u now) in
let state = let state =
let h = model.horizon mstate in let h = model.horizon mstate in
if h <= 0.0 then S.update ~mstate state if h <= 0.0 then S.set_mstate state mstate
else if now >= stop then else if now >= stop then
(* TODO: Build an initial state with the initial states for (* TODO: Build an initial state with the initial states for
both the solver and model - an equivalent of [s] in both the solver and model - an equivalent of [s] in
@ -59,11 +57,9 @@ module LazySim (S : SimState) =
let ivp = { fder; stop = stop -. now; init = y } in let ivp = { fder; stop = stop -. now; init = y } in
let zc = { yc = y; fzer } in let zc = { yc = y; fzer } in
let sstate = solver.reset (ivp, zc) sstate in let sstate = solver.reset (ivp, zc) sstate in
let status = S.running ~mode:Continuous status in let state = S.set_running ~mode:Continuous state in
S.update ~status ~mstate ~sstate state S.update state mstate sstate
else else S.set_running ~mode:Continuous state in
let status = S.running ~mode:Continuous status in
S.update ~status state in
let start = input.start +. now in let start = input.start +. now in
Some { start; length = 0.0; u = fun _ -> o }, state Some { start; length = 0.0; u = fun _ -> o }, state
| Continuous -> | Continuous ->
@ -76,28 +72,27 @@ module LazySim (S : SimState) =
{ start = input.start +. now; length = h -. now; u = fout } in { start = input.start +. now; length = h -. now; u = fout } in
let state = match z with let state = match z with
| None -> | None ->
let status = let state =
if h >= stop then S.running ~mode:Discrete ~now:h' status if h >= stop then
else S.running ~now:h' status in S.set_running ~mode:Discrete ~now:h' state
S.update ~status ~mstate ~sstate state else S.set_running ~now:h' state in
S.update state mstate sstate
| Some z -> | Some z ->
let status = S.running ~mode:Discrete ~now:h' status in let state = S.set_running ~mode:Discrete ~now:h' state in
let mstate = model.zset mstate z in S.update state (model.zset mstate z) sstate in
S.update ~status ~mstate ~sstate state in
Some out, state in Some out, state in
let reset p s = let reset p s =
(* TODO: does [model.cget mstate] make sense before the first discrete (* TODO: does [model.cget mstate] make sense before the first discrete
step - can we use [mstate] to reinitialize [sstate] ? *) step - can we use [mstate] to reinitialize [sstate] ? *)
let mstate = model.reset p (S.mstate s) in let mstate = model.reset p (S.get_mstate s) in
let y = model.cget mstate in let y = model.cget mstate in
(* TODO: what initial stop time do we use ? *) (* TODO: what initial stop time do we use ? *)
let stop = raise Common.Utils.TODO in let stop = raise Common.Utils.TODO in
let ivp = { fder = model.fder mstate; stop; init = y } in let ivp = { fder = model.fder mstate; stop; init = y } in
let zc = { fzer = model.fzer mstate; yc = y } in let zc = { fzer = model.fzer mstate; yc = y } in
let sstate = solver.reset (ivp, zc) (S.sstate s) in let sstate = solver.reset (ivp, zc) (S.get_sstate s) in
let status = S.idle (S.status s) in S.update s mstate sstate in
S.update ~status ~mstate ~sstate s in
DNode { state; step; reset } DNode { state; step; reset }
@ -113,40 +108,37 @@ module GreedySim (S : SimState) =
(HNode model : ('p, 'a, 'b, 'y, 'yder, 'zin, 'zout) hnode) (HNode model : ('p, 'a, 'b, 'y, 'yder, 'zin, 'zout) hnode)
(DNode solver : ('y, 'yder, 'zin, 'zout) solver) (DNode solver : ('y, 'yder, 'zin, 'zout) solver)
: ('p, 'a, 'b) greedy_sim : ('p, 'a, 'b) greedy_sim
= let state = S.init ~mstate:model.state ~sstate:solver.state in = let state = S.get_init model.state solver.state in
let rec step state input = let rec step state input =
let status = S.status state and mstate = S.mstate state let mstate = S.get_mstate state and sstate = S.get_sstate state in
and sstate = S.sstate state in
if not (S.is_running state) then if not (S.is_running state) then
let mode = Discrete and now = 0.0 and stop = input.length in let mode = Discrete and now = 0.0 and stop = input.length in
let status = S.running ~mode ~input ~now ~stop (S.status state) in let state = S.set_running ~mode ~input ~now ~stop state in
let state = S.update ~status state in
step state input step state input
else let now = S.now state and stop = S.stop state in else let now = S.get_now state and stop = S.get_stop state in
match S.mode state with match S.get_mode state with
| Discrete -> | Discrete ->
let o, mstate = model.step mstate (input.u now) in let o, mstate = model.step mstate (input.u now) in
let h = model.horizon mstate in let h = model.horizon mstate in
let rest, state = let rest, state =
if h <= 0.0 then step (S.update ~mstate state) input if h <= 0.0 then step (S.set_mstate state mstate) input
else if now >= stop then [], state else if now >= stop then [], state
else if model.jump mstate then else if model.jump mstate then
let y = model.cget mstate in let y = model.cget mstate in
(* FIXME: copy the state here *)
let fder t = model.fder mstate (offset input now t) in let fder t = model.fder mstate (offset input now t) in
let fzer t = model.fzer mstate (offset input now t) in let fzer t = model.fzer mstate (offset input now t) in
let ivp = { fder; stop = stop -. now; init = y } in let ivp = { fder; stop = stop -. now; init = y } in
let zc = { yc = y; fzer } in let zc = { yc = y; fzer } in
let sstate = solver.reset (ivp, zc) sstate in let sstate = solver.reset (ivp, zc) sstate in
let status = S.running ~mode:Continuous status in let state = S.set_running ~mode:Continuous state in
step (S.update ~status ~mstate ~sstate state) input step (S.update state mstate sstate) input
else else step (S.set_running ~mode:Continuous state) input in
let status = S.running ~mode:Continuous status in
step (S.update ~status state) input in
let start = input.start +. now in let start = input.start +. now in
{ start; length = 0.0; u = fun _ -> o }::rest, state { start; length = 0.0; u = fun _ -> o }::rest, state
| Continuous -> | Continuous ->
let (h, f, z), _sstate = solver.step sstate stop in let (h, f, z), sstate = solver.step sstate stop in
let mstate = model.cset mstate (f h) in let mstate = model.cset mstate (f h) in
let h' = input.start +. h in let h' = input.start +. h in
let fout t = let fout t =
@ -156,22 +148,19 @@ module GreedySim (S : SimState) =
match z with match z with
| None -> | None ->
if h >= stop then if h >= stop then
let status = S.running ~mode:Discrete ~now:h' status in let state = S.set_running ~mode:Discrete ~now:h' state in
let rest, state = let rest, state = step (S.update state mstate sstate) input in
step (S.update ~status ~mstate ~sstate state) input in
out::rest, state out::rest, state
else else
let status = S.running ~now:h' status in let state = S.set_running ~now:h' state in
let rest, state = let rest, state = step (S.update state mstate sstate) input in
step (S.update ~status ~mstate ~sstate state) input in
(match rest with (match rest with
| [] -> [out], state | [] -> [out], state
| f::rest -> compose [out;f] :: rest, state) | f::rest -> compose [out;f] :: rest, state)
| Some z -> | Some z ->
let status = S.running ~mode:Discrete ~now:h' status in let state = S.set_running ~mode:Discrete ~now:h' state in
let mstate = model.zset mstate z in let mstate = model.zset mstate z in
let rest, state = let rest, state = step (S.update state mstate sstate) input in
step (S.update ~status ~mstate ~sstate state) input in
out::rest, state in out::rest, state in
let reset = assert false in let reset = assert false in

157
src/lib/hsim/state.ml
View file

@ -8,58 +8,59 @@ type mode = Discrete | Continuous
module type SimState = module type SimState =
sig sig
(** Simulation status:
- Idle: waiting for input
- Running: currently integrating; in this case, we have access to the
step mode, current input, timestamp and stop time. *)
type 'a status
(** Internal state of the simulation. This contains the state of the model (** Internal state of the simulation. This contains the state of the model
and solver, as well as the current simulation status. *) and solver, as well as the current simulation status.
The simulation status should take two forms:
- Idle: waiting for input;
- Running: currently integrating; in this case, we have access to the
step mode, current input, timestamp and stop time. *)
type ('a, 'ms, 'ss) state type ('a, 'ms, 'ss) state
(** Get the current simulation status. *)
val status : ('a, 'ms, 'ss) state -> 'a status
(** Get the model state. *) (** Get the model state. *)
val mstate : ('a, 'ms, 'ss) state -> 'ms val get_mstate : ('a, 'ms, 'ss) state -> 'ms
(** Get the solver state. *) (** Get the solver state. *)
val sstate : ('a, 'ms, 'ss) state -> 'ss val get_sstate : ('a, 'ms, 'ss) state -> 'ss
(** Get the current step mode.
⚠ Should only be called when running (see [is_running]). *)
val get_mode : ('a, 'ms, 'ss) state -> mode
(** Get the current input.
⚠ Should only be called when running (see [is_running]). *)
val get_input : ('a, 'ms, 'ss) state -> 'a value
(** Get the current timestamp.
⚠ Should only be called when running (see [is_running]). *)
val get_now : ('a, 'ms, 'ss) state -> time
(** Get the current stop time.
⚠ Should only be called when running (see [is_running]). *)
val get_stop : ('a, 'ms, 'ss) state -> time
(** Build an initial state. *)
val get_init : 'ms -> 'ss -> ('a, 'ms, 'ss) state
(** Is the simulation running or idle ? *) (** Is the simulation running or idle ? *)
val is_running : ('a, 'ms, 'ss) state -> bool val is_running : ('a, 'ms, 'ss) state -> bool
(** Update the state. *) (** Update the model state. *)
val update : ?status:'a status -> ?mstate:'ms -> ?sstate:'ss -> val set_mstate : ('a, 'ms, 'ss) state -> 'ms -> ('a, 'ms, 'ss) state
('a, 'ms, 'ss) state -> ('a, 'ms, 'ss) state
(** Update the status to idle. *) (** Update the solver state. *)
val idle : 'a status -> 'a status val set_sstate : ('a, 'ms, 'ss) state -> 'ss -> ('a, 'ms, 'ss) state
(** Update both the solver and model states. *)
val update : ('a, 'ms, 'ss) state -> 'ms -> 'ss -> ('a, 'ms, 'ss) state
(** Update the status to running. *) (** Update the status to running. *)
val running : val set_running :
?mode:mode -> ?input:'a value -> ?mode:mode -> ?input:'a value -> ?now:time -> ?stop:time ->
?now:time -> ?stop:time -> 'a status -> 'a status ('a, 'ms, 'ss) state -> ('a, 'ms, 'ss) state
(** Get the current step mode. (** Update the status to idle. *)
⚠ Should only be called when running (see [is_running]). *) val set_idle : ('a, 'ms, 'ss) state -> ('a, 'ms, 'ss) state
val mode : ('a, 'ms, 'ss) state -> mode
(** Get the current input.
⚠ Should only be called when running (see [is_running]). *)
val input : ('a, 'ms, 'ss) state -> 'a value
(** Get the current timestamp.
⚠ Should only be called when running (see [is_running]). *)
val now : ('a, 'ms, 'ss) state -> time
(** Get the current stop time.
⚠ Should only be called when running (see [is_running]). *)
val stop : ('a, 'ms, 'ss) state -> time
(** Build an initial state. *)
val init : mstate:'ms -> sstate:'ss -> ('a, 'ms, 'ss) state
end end
module FunctionalSimState : SimState = module FunctionalSimState : SimState =
@ -87,21 +88,20 @@ module FunctionalSimState : SimState =
exception Not_running exception Not_running
let status s = s.status let get_mstate state = state.mstate
let mstate s = s.mstate let get_sstate state = state.sstate
let sstate s = s.sstate
let is_running s = let is_running state =
match s.status with Running _ -> true | Idle -> false match state.status with Running _ -> true | Idle -> false
let idle _ = Idle let set_idle state = { state with status = Idle }
let running ?mode ?input ?now ?stop s = let set_running ?mode ?input ?now ?stop state =
match s with match state.status with
| Idle -> | Idle ->
begin match mode, input, now, stop with begin match mode, input, now, stop with
| Some mode, Some input, Some now, Some stop -> | Some mode, Some input, Some now, Some stop ->
Running { mode; input; now; stop } { state with status = Running { mode; input; now; stop } }
| _ -> raise (Invalid_argument "") | _ -> raise (Invalid_argument "")
end end
| Running { mode=m; input=i; now=n; stop=s } -> | Running { mode=m; input=i; now=n; stop=s } ->
@ -109,24 +109,23 @@ module FunctionalSimState : SimState =
let input = Option.value input ~default:i in let input = Option.value input ~default:i in
let now = Option.value now ~default:n in let now = Option.value now ~default:n in
let stop = Option.value stop ~default:s in let stop = Option.value stop ~default:s in
Running { mode; input; now; stop } { state with status = Running { mode; input; now; stop } }
let update ?status ?mstate ?sstate { status=st; mstate=ms; sstate=ss } = let set_mstate state mstate = { state with mstate }
let status = Option.value status ~default:st in let set_sstate state sstate = { state with sstate }
let mstate = Option.value mstate ~default:ms in
let sstate = Option.value sstate ~default:ss in
{ status; mstate; sstate }
let mode s = let update state mstate sstate = { state with mstate; sstate }
let get_mode s =
match s.status with Running r -> r.mode | Idle -> raise Not_running match s.status with Running r -> r.mode | Idle -> raise Not_running
let input s = let get_input s =
match s.status with Running r -> r.input | Idle -> raise Not_running match s.status with Running r -> r.input | Idle -> raise Not_running
let now s = let get_now s =
match s.status with Running r -> r.now | Idle -> raise Not_running match s.status with Running r -> r.now | Idle -> raise Not_running
let stop s = let get_stop s =
match s.status with Running r -> r.stop | Idle -> raise Not_running match s.status with Running r -> r.stop | Idle -> raise Not_running
let init ~mstate ~sstate = { status = Idle; mstate; sstate } let get_init mstate sstate = { status = Idle; mstate; sstate }
end end
module InPlaceSimState : SimState = module InPlaceSimState : SimState =
@ -147,21 +146,23 @@ module InPlaceSimState : SimState =
exception Not_running exception Not_running
let status s = s.status let get_mstate state = state.mstate
let mstate s = s.mstate let get_sstate state = state.sstate
let sstate s = s.sstate
let is_running s = let is_running state =
match s.status with Running _ -> true | Idle -> false match state.status with Running _ -> true | Idle -> false
let idle _ = Idle let set_idle state =
state.status <- Idle;
state
let running ?mode ?input ?now ?stop status = let set_running ?mode ?input ?now ?stop state =
match status with match state.status with
| Idle -> | Idle ->
begin match mode, input, now, stop with begin match mode, input, now, stop with
| Some mode, Some input, Some now, Some stop -> | Some mode, Some input, Some now, Some stop ->
Running { mode; input; now; stop } state.status <- Running { mode; input; now; stop };
state
| _ -> raise (Invalid_argument "") | _ -> raise (Invalid_argument "")
end end
| Running ({ mode=m; input=i; now=n; stop=s } as r) -> | Running ({ mode=m; input=i; now=n; stop=s } as r) ->
@ -169,23 +170,23 @@ module InPlaceSimState : SimState =
let input = Option.value input ~default:i in r.input <- input; let input = Option.value input ~default:i in r.input <- input;
let now = Option.value now ~default:n in r.now <- now; let now = Option.value now ~default:n in r.now <- now;
let stop = Option.value stop ~default:s in r.stop <- stop; let stop = Option.value stop ~default:s in r.stop <- stop;
status state
let update ?status ?mstate ?sstate let set_mstate state mstate = state.mstate <- mstate; state
({ status=st; mstate=ms; sstate=ss } as s) = let set_sstate state sstate = state.sstate <- sstate; state
let status = Option.value status ~default:st in
let mstate = Option.value mstate ~default:ms in
let sstate = Option.value sstate ~default:ss in
s.status <- status; s.mstate <- mstate; s.sstate <- sstate; s
let mode s = let update state mstate sstate =
state.mstate <- mstate; state.sstate <- sstate; state
let get_mode s =
match s.status with Running r -> r.mode | Idle -> raise Not_running match s.status with Running r -> r.mode | Idle -> raise Not_running
let input s = let get_input s =
match s.status with Running r -> r.input | Idle -> raise Not_running match s.status with Running r -> r.input | Idle -> raise Not_running
let now s = let get_now s =
match s.status with Running r -> r.now | Idle -> raise Not_running match s.status with Running r -> r.now | Idle -> raise Not_running
let stop s = let get_stop s =
match s.status with Running r -> r.stop | Idle -> raise Not_running match s.status with Running r -> r.stop | Idle -> raise Not_running
let init ~mstate ~sstate = { status = Idle; mstate; sstate } let get_init mstate sstate = { status = Idle; mstate; sstate }
end end