diff --git a/hsim.opam b/hsim.opam index 316a89c..c68849c 100644 --- a/hsim.opam +++ b/hsim.opam @@ -3,7 +3,7 @@ opam-version: "2.0" synopsis: "An executable semantics for the simulation of hybrid systems" maintainer: ["henri.saudubray@proton.me"] authors: ["Henri Saudubray"] -license: "GPL-3.0-or-later" +license: "CeCILL-2.1-or-later" homepage: "https://codeberg.org/17maiga/hsim" doc: "https://url/to/documentation" bug-reports: "https://codeberg.org/17maiga/hsim/issues" diff --git a/src/lib/hsim/sim.ml b/src/lib/hsim/sim.ml index 6c05702..7381160 100644 --- a/src/lib/hsim/sim.ml +++ b/src/lib/hsim/sim.ml @@ -26,27 +26,25 @@ module LazySim (S : SimState) = (HNode model : ('p, 'a, 'b, 'y, 'yder, 'zin, 'zout) hnode) (DNode solver : ('y, 'yder, 'zin, 'zout) solver) : ('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 mstate = S.mstate state and sstate = S.sstate state - and status = S.status state in + let mstate = S.get_mstate state and sstate = S.get_sstate state in match input, S.is_running state with | Some input, _ -> - 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.update ~status state in + let mode = Discrete and now = 0.0 and stop = input.length in + let state = S.set_running ~mode ~input ~now ~stop state in None, state | None, false -> None, state | None, true -> - let input = S.input state and now = S.now state - and stop = S.stop state in - match S.mode state with + let input = S.get_input state and now = S.get_now state + and stop = S.get_stop state in + match S.get_mode state with | Discrete -> let o, mstate = model.step mstate (input.u now) in let state = 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 (* TODO: Build an initial state with the initial states for 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 zc = { yc = y; fzer } in let sstate = solver.reset (ivp, zc) sstate in - let status = S.running ~mode:Continuous status in - S.update ~status ~mstate ~sstate state - else - let status = S.running ~mode:Continuous status in - S.update ~status state in + let state = S.set_running ~mode:Continuous state in + S.update state mstate sstate + else S.set_running ~mode:Continuous state in let start = input.start +. now in Some { start; length = 0.0; u = fun _ -> o }, state | Continuous -> @@ -76,28 +72,27 @@ module LazySim (S : SimState) = { start = input.start +. now; length = h -. now; u = fout } in let state = match z with | None -> - let status = - if h >= stop then S.running ~mode:Discrete ~now:h' status - else S.running ~now:h' status in - S.update ~status ~mstate ~sstate state + let state = + if h >= stop then + S.set_running ~mode:Discrete ~now:h' state + else S.set_running ~now:h' state in + S.update state mstate sstate | Some z -> - let status = S.running ~mode:Discrete ~now:h' status in - let mstate = model.zset mstate z in - S.update ~status ~mstate ~sstate state in + let state = S.set_running ~mode:Discrete ~now:h' state in + S.update state (model.zset mstate z) sstate in Some out, state in let reset p s = (* TODO: does [model.cget mstate] make sense before the first discrete 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 (* TODO: what initial stop time do we use ? *) let stop = raise Common.Utils.TODO in let ivp = { fder = model.fder mstate; stop; init = y } in let zc = { fzer = model.fzer mstate; yc = y } in - let sstate = solver.reset (ivp, zc) (S.sstate s) in - let status = S.idle (S.status s) in - S.update ~status ~mstate ~sstate s in + let sstate = solver.reset (ivp, zc) (S.get_sstate s) in + S.update s mstate sstate in DNode { state; step; reset } @@ -113,40 +108,37 @@ module GreedySim (S : SimState) = (HNode model : ('p, 'a, 'b, 'y, 'yder, 'zin, 'zout) hnode) (DNode solver : ('y, 'yder, 'zin, 'zout) solver) : ('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 status = S.status state and mstate = S.mstate state - and sstate = S.sstate state in + let mstate = S.get_mstate state and sstate = S.get_sstate state in if not (S.is_running state) then 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.update ~status state in + let state = S.set_running ~mode ~input ~now ~stop state in step state input - else let now = S.now state and stop = S.stop state in - match S.mode state with + else let now = S.get_now state and stop = S.get_stop state in + match S.get_mode state with | Discrete -> let o, mstate = model.step mstate (input.u now) in let h = model.horizon mstate in 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 model.jump mstate then let y = model.cget mstate in + (* FIXME: copy the state here *) let fder t = model.fder 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 zc = { yc = y; fzer } in let sstate = solver.reset (ivp, zc) sstate in - let status = S.running ~mode:Continuous status in - step (S.update ~status ~mstate ~sstate state) input - else - let status = S.running ~mode:Continuous status in - step (S.update ~status state) input in + let state = S.set_running ~mode:Continuous state in + step (S.update state mstate sstate) input + else step (S.set_running ~mode:Continuous state) input in let start = input.start +. now in { start; length = 0.0; u = fun _ -> o }::rest, state | 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 h' = input.start +. h in let fout t = @@ -156,22 +148,19 @@ module GreedySim (S : SimState) = match z with | None -> if h >= stop then - let status = S.running ~mode:Discrete ~now:h' status in - let rest, state = - step (S.update ~status ~mstate ~sstate state) input in + let state = S.set_running ~mode:Discrete ~now:h' state in + let rest, state = step (S.update state mstate sstate) input in out::rest, state else - let status = S.running ~now:h' status in - let rest, state = - step (S.update ~status ~mstate ~sstate state) input in + let state = S.set_running ~now:h' state in + let rest, state = step (S.update state mstate sstate) input in (match rest with | [] -> [out], state | f::rest -> compose [out;f] :: rest, state) | 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 rest, state = - step (S.update ~status ~mstate ~sstate state) input in + let rest, state = step (S.update state mstate sstate) input in out::rest, state in let reset = assert false in diff --git a/src/lib/hsim/state.ml b/src/lib/hsim/state.ml index 28a8856..2cacc40 100644 --- a/src/lib/hsim/state.ml +++ b/src/lib/hsim/state.ml @@ -8,58 +8,59 @@ type mode = Discrete | Continuous module type SimState = 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 - 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 - (** Get the current simulation status. *) - val status : ('a, 'ms, 'ss) state -> 'a status - (** Get the model state. *) - val mstate : ('a, 'ms, 'ss) state -> 'ms + val get_mstate : ('a, 'ms, 'ss) state -> 'ms (** 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 ? *) val is_running : ('a, 'ms, 'ss) state -> bool - (** Update the state. *) - val update : ?status:'a status -> ?mstate:'ms -> ?sstate:'ss -> - ('a, 'ms, 'ss) state -> ('a, 'ms, 'ss) state + (** Update the model state. *) + val set_mstate : ('a, 'ms, 'ss) state -> 'ms -> ('a, 'ms, 'ss) state - (** Update the status to idle. *) - val idle : 'a status -> 'a status + (** Update the solver state. *) + 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. *) - val running : - ?mode:mode -> ?input:'a value -> - ?now:time -> ?stop:time -> 'a status -> 'a status + val set_running : + ?mode:mode -> ?input:'a value -> ?now:time -> ?stop:time -> + ('a, 'ms, 'ss) state -> ('a, 'ms, 'ss) state - (** Get the current step mode. - ⚠ Should only be called when running (see [is_running]). *) - 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 + (** Update the status to idle. *) + val set_idle : ('a, 'ms, 'ss) state -> ('a, 'ms, 'ss) state end module FunctionalSimState : SimState = @@ -87,21 +88,20 @@ module FunctionalSimState : SimState = exception Not_running - let status s = s.status - let mstate s = s.mstate - let sstate s = s.sstate + let get_mstate state = state.mstate + let get_sstate state = state.sstate - let is_running s = - match s.status with Running _ -> true | Idle -> false + let is_running state = + 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 = - match s with + let set_running ?mode ?input ?now ?stop state = + match state.status with | Idle -> begin match mode, input, now, stop with | Some mode, Some input, Some now, Some stop -> - Running { mode; input; now; stop } + { state with status = Running { mode; input; now; stop } } | _ -> raise (Invalid_argument "") end | 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 now = Option.value now ~default:n 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 status = Option.value status ~default:st in - let mstate = Option.value mstate ~default:ms in - let sstate = Option.value sstate ~default:ss in - { status; mstate; sstate } + let set_mstate state mstate = { state with mstate } + let set_sstate state sstate = { state with 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 - let input s = + let get_input s = 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 - let stop s = + let get_stop s = 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 module InPlaceSimState : SimState = @@ -147,21 +146,23 @@ module InPlaceSimState : SimState = exception Not_running - let status s = s.status - let mstate s = s.mstate - let sstate s = s.sstate + let get_mstate state = state.mstate + let get_sstate state = state.sstate - let is_running s = - match s.status with Running _ -> true | Idle -> false + let is_running state = + 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 = - match status with + let set_running ?mode ?input ?now ?stop state = + match state.status with | Idle -> begin match mode, input, now, stop with | Some mode, Some input, Some now, Some stop -> - Running { mode; input; now; stop } + state.status <- Running { mode; input; now; stop }; + state | _ -> raise (Invalid_argument "") end | 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 now = Option.value now ~default:n in r.now <- now; let stop = Option.value stop ~default:s in r.stop <- stop; - status + state - let update ?status ?mstate ?sstate - ({ status=st; mstate=ms; sstate=ss } as s) = - 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 set_mstate state mstate = state.mstate <- mstate; state + let set_sstate state sstate = state.sstate <- sstate; state - 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 - let input s = + let get_input s = 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 - let stop s = + let get_stop s = 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 +