#import "@preview/cetz:0.3.2"
#import "@preview/cetz-plot:0.1.1"
#import "@preview/finite:0.4.1"
#import "@preview/touying:0.6.1": *
#import themes.simple: *

// Notes
//
// Shorten: too long on the explanation
// Instead, rely on a simple, two-axes presentation: We need
// - continuously described variables: IVP, ODEs
// - scheduling discrete-time signals with continuous ones: solution in simulink
//   is zc events
// Need an introduction: what the problem is, what are we doing
// - Executable assertions: before any kind of formal methods, a programmer's
//   tool
// - Explaining the simulation as succintly as possible
//
// Zélus:
// - Cite Simulink
//
// Discrete nodes:
// - remove some stuff
// - show signals
// - "redge" -> "rising_edge"
// - "true, false" -> "T, F"
// - cite Mealy
// - OCaml datatype
// - "Given i : I as input stream, simulation defines o : O [...]"
//
// Van der Pol: 
// - show the math and oscillator
//
// Continuous nodes:
// - remove some stuff
// - the other way around: model first, low-level representation later (as for
//   the discrete)
// - does not typecheck!
// - remind the audience of the vdp oscillator math
// - f_der, f_out
//
// Hybrid nodes:
// - the other way around, too: model first, low-level representation later
// - f_zero
//
// Synthesis: new constructs for continuous time (hybrid, der, up...)
//
// Assertions:
// - Shorter, explain as a programmer's tool
//
// Now, my work:
// - define the runtime as precisely and succintly as possible;
//
// ODE/ZC solvers
// - Too "hand-wavy"

#show: simple-theme.with(
  config-common(show-bibliography-as-footnote: bibliography("sources.bib")))
#set raw(syntaxes: "zelus.sublime-syntax")
#show raw: set text(font: "CaskaydiaCove NF")
#let zelus = smallcaps[Zélus]
#let lustre = smallcaps[Lustre]
#let simulink = smallcaps[Simulink]
#let ocaml = smallcaps[OCaml]
#let Time = math.italic[Time]

// 20 mins presentation - 10 mins questions
 
= Internship Defense --- MPRI M2 \ Hybrid System Models with Transparent Assertions

Henri #smallcaps[Saudubray]#footnote(
  [All code accessible at #link("https://codeberg.org/17maiga/hsim").],
  numbering: "*"
), supervised by Marc #smallcaps[Pouzet], #smallcaps[Inria PARKAS]

10/09/2025

= Context: #zelus and Hybrid System Models

== The #zelus Programming Language

- Language@cit:zelus_sync_lng_with_ode for description of hybrid system models
- Synchronous language kernel _à la_ #lustre@cit:lustre
- Extension to continuous-time behaviour
- Compilation to #ocaml code
- Execution using an off-the-shelf numerical solver@cit:sundials@cit:sundialsml

== Discrete-Time Systems

Programs (nodes) are functions on streams

#align(center + horizon, [
  ```zelus
  let node rising_edge(x: bool) =
    x -> (x && not(pre(x)))
  ```
  #linebreak()
  #table(
    columns: (auto, auto, auto, auto, auto, auto, auto),
    align: center + horizon, stroke: (x, y) => (
      left: if x == 0 { 0pt } else { 1pt },
      top: if y == 0 { 0pt } else { 1pt },
    ),
    `x`,                                 $F$,   $T$, $T$, $F$, $T$, [...],
    ```zelus pre(x)```,                  $bot$, $F$, $T$, $T$, $F$, [...],
    ```zelus x && not(pre(x))```,        $bot$, $T$, $F$, $F$, $T$, [...],
    ```zelus x -> (x && not(pre(x)))```, $F$,   $T$, $F$, $F$, $T$, [...],
  )
])

// Prononcer les suites, "front montant", `fby` ?

#pagebreak()

Compiled down to Mealy machines@cit:mealy@cit:sync_based_codegen_hyb_sys_lng:
$ s_0 : S wide wide f_"step" : S times I -> O times S $
#pause
With input $i : NN -> I$, simulation defines output $o : NN -> O$
$ (o_n, s_(n+1)) = f_"step" (s_n, i_n) $

== Physical Simulation in Discrete Time

// Mention initial values in vdp

The Van der Pol oscillator:
$ (d x)/(d t) = y wide (d y)/(d t) = mu(1 - x^2)y - x wide x(0) = y(0) = 1 $
#pause
#align(center, cetz.canvas({
  cetz-plot.plot.plot(size: (20, 4), axis-style: "school-book",
    x-tick-step: 10, y-tick-step: 5, x-label: $t$, y-label: none,
    y-grid: "both", legend: (19, 4.5), {
    let d = csv("data/vdp.csv")
    let x = d.map(r => (r.at(0), r.at(1)).map(v => float(v.trim())))
    let y = d.map(r => (r.at(0), r.at(2)).map(v => float(v.trim())))
    cetz-plot.plot.add(x, line: "spline", label: $x$)
    cetz-plot.plot.add(y, line: "spline", label: $y$)
  })
}))

#pagebreak()

#only((1,2))[
  ```zelus
  let h = 0.001
  (* Euler integrators. *)
  let node f_euler(x0, x') = x where
    rec x = x0 -> pre(x + x' * h)
  let node b_euler(x0, x') = x where
    rec x = x0 -> pre(x) + x' * h
  
  (* Van der Pol oscillator. *)
  let node vdp(μ) = (x, y) where
    rec x = b_euler(1.0, y)
    and y = f_euler(1.0, (μ * (1.0 - (x * x)) * y) - x)
  ```
]
#only(2)[
  #place(dx: 55%, dy: -70%, cetz.canvas({
    let d = csv("data/xsmall.csv")
    let x = d.map(r => (r.at(0), r.at(1)).map(v => float(v.trim())))
    let y = d.map(r => (r.at(0), r.at(2)).map(v => float(v.trim())))
    cetz-plot.plot.plot(size: (10, 5), axis-style: "school-book",
      x-tick-step: 10, y-tick-step: 5, x-grid: "both", y-grid: "both",
      y-min: -8, y-max: 8, legend: (9, 5.5), y-label: none, x-label: none, {
      cetz-plot.plot.add(x, label: $x$)
      cetz-plot.plot.add(y, label: $y$)
    })
  }))
]
#only(3)[
  ```zelus
  let h = 0.1
  (* Euler integrators. *)
  let node f_euler(x0, x') = x where
    rec x = x0 -> pre(x + x' * h)
  let node b_euler(x0, x') = x where
    rec x = x0 -> pre(x) + x' * h
  
  (* Van der Pol oscillator. *)
  let node vdp(μ) = (x, y) where
    rec x = b_euler(1.0, y)
    and y = f_euler(1.0, (μ * (1.0 - (x * x)) * y) - x)
  ```
  #place(dx: 55%, dy: -70%, cetz.canvas({
    let d = csv("data/middle.csv")
    let x = d.map(r => (r.at(0), r.at(1)).map(v => float(v.trim())))
    let y = d.map(r => (r.at(0), r.at(2)).map(v => float(v.trim())))
    cetz-plot.plot.plot(size: (10, 5), axis-style: "school-book",
      x-tick-step: 10, y-tick-step: 5, x-grid: "both", y-grid: "both",
      y-min: -8, y-max: 8, legend: (9, 5.5), y-label: none, x-label: none, {
      cetz-plot.plot.add(x, label: $x$)
      cetz-plot.plot.add(y, label: $y$)
    })
  }))
]

== Continuous-Time Systems

Extension to continuous time. \ #pause
New constructs: ```zelus hybrid```, ```zelus der```, ```zelus init```

$ (d x)/(d t) = y wide (d y)/(d t) = mu(1 - x^2)y - x wide x(0) = y(0) = 1 $

```zelus
let hybrid vdp(μ) = (x, y) where
  rec der x = y init 1.0
  and der y = (μ * (1.0 - (x * x)) * y) - x) init 1.0
```

#pagebreak()

Programs are compiled down to initial value problems (IVPs)
$ y_0 : Y wide f_"der" : Time times I times Y -> Y'
          wide f_"out" : Time times I times Y -> O $
#pause
Use a numerical solver to compute an approximation of $y : Time -> Y$
$ y(0) = y_0 wide (d y)/(d t)(t) = f_"der" (t, i(t), y(t)) $
#pause
With input $i : Time -> I$, simulation defines output
$o : Time -> O$
$ o(t) = f_"out" (t, i(t), y(t)) $

== Hybrid Systems

- Mixing discrete and continuous behaviours #pause
- Discrete steps are scheduled with _zero-crossing events_
  #grid(align: horizon + center, columns: (1fr, 4fr), {
    let p(b) = cetz.canvas({
      cetz-plot.plot.plot(
        axis-style: "left", size: (5, 3),
        y-tick-step: none, y-label: none,
        x-tick-step: none, x-label: none, b
      )
    })
    let data = csv("data/ball.csv").map(r => r.map(float))
    alternatives-match((
      "1-3": p({
        cetz-plot.plot.add(data, line: "spline")
      }),
      "4-": p({
        cetz-plot.plot.add(data, line: "spline")
        cetz-plot.plot.add((
          (3.2, 0), (8.3, 0), (12.4, 0), (15.6, 0), (18.2, 0), (20.3, 0),
          (22.0, 0), (23.2, 0), (24, 0), (24.5, 0), (24.8, 0), (25, 0),
          (25.1, 0), (25.2, 0), (25.3, 0), (25.4, 0), (25.5, 0), (25.6, 0),
          (25.7, 0), (25.8, 0), (25.9, 0), (26.0, 0), (26.1, 0), (26.2, 0),
          (26.3, 0), (26.4, 0), (26.5, 0), (26.6, 0), (26.7, 0), (26.8, 0),
          (26.9, 0), (27.0, 0), (27.1, 0), (27.2, 0), (27.3, 0), (27.4, 0),
          (27.5, 0), (27.6, 0), (27.7, 0), (27.8, 0), (27.9, 0), (28.0, 0),
        ), mark: "o", mark-size: .1)
      })
    ))
  }, [
    #pause $ (d y)/(d t) = y' wide (d y')/(d t) = -g $
    #pause "When $y < 0$ at time $t$, $y'(t) = -k times (lim_(h -> t^-) y'(h))$"
  ])
  #pause
  ```zelus
  let hybrid bouncing_ball(y0, y'0) = y where
    rec der y  = y' init y0
    and der y' = -g init y'0 reset up(-y) -> -k * (last y')
  ```

#pagebreak()

Compiled down to both a Mealy machine and an IVP \ #pause
Use of a zero-crossing detection mechanism@cit:illinois to monitor for events

$ f_"zero" : Time times I times Y -> Z $

== Models with assertions

// Observers rather than sub-nodes...
// Mention more clearly that they are executable
- In #lustre, assertions are observers on the parent state@cit:assertion_lustre
#only(2)[
- Hybrid assertions are the same!
  ```zelus
  let hybrid sincos() = (sin, cos) where
    rec der sin = cos init 0.0
    and der cos = -sin init 1.0
    and assert(
      let der neg_cos = sin init -1.0 in
      abs(neg_cos + cos) <= ε
    )
  ```
]

== Interferences

Simultaneous simulation of independent systems causes interferences
#{
  let code1 = ```zelus
    let hybrid ball() = p where
      rec der p = v           init 0.0
      and der v = a * (cos p) init 2.953
      and a = g * (sin p) - 5.0 * v / (cos p)
    
    let hybrid main() = p where
      p = ball()
    ```
  let code2 = ```zelus
    let hybrid ball() = p where
      rec der p = v           init 0.0
      and der v = a * (cos p) init 2.953
      and a = g * (sin p) - 5.0 * v / (cos p)
    
    let hybrid main() = p where
      p = ball() and _ = vdp(10.0)
    ```
  let plot(file, x-step) = cetz.canvas({
    let x = csv(file).map(
      row => (float(row.at(0).trim()), float(row.at(1).trim())))
    cetz-plot.plot.plot(axis-style: "left", size: (7, 2), y-tick-step: none,
    y-max: calc.pi * 2, y-min: 0, x-grid: "major",
    x-tick-step: none, x-label: none, y-label: none, legend: (6, 2),
    x-ticks: ((x-step, ""),), {
      cetz-plot.plot.add(x, label: `p`)
    })
  })
  let plot1(t) = plot("data/0000001.csv", t)
  let plot2(t) = plot("data/10.csv", t)
  let plot_ball(coords) = cetz.canvas({
    cetz-plot.plot.plot(
      size: (7, 2), axis-style: "left",
      x-label: `p`, y-label: [~~~], x-tick-step: none, y-tick-step: none, {
      cetz-plot.plot.add(t => calc.cos(t), domain: (0, 13), samples: 500)
    })
    cetz.draw.circle(coords, radius: .15)
  })
  let anim1 = (
    ((0.2, 2.10), 00.0), ((1.0, 1.10), 00.5), ((1.8, 0.20), 01.0),
    ((2.5, 1.30), 01.5), ((3.1, 2.10), 02.5), ((3.2, 2.15), 03.5),
    ((3.1, 2.10), 04.5), ((2.5, 1.30), 06.0), ((1.8, 0.20), 07.5),
    ((1.0, 1.10), 08.0), ((1.7, 0.15), 09.0), ((1.9, 0.30), 10.0),
    ((1.7, 0.15), 12.0), ((1.5, 0.30), 14.0), ((1.7, 0.15), 18.0),
    ((1.7, 0.15), 20.0), ((1.7, 0.15), 30.0), ((1.7, 0.15), 50.0),
    ((1.7, 0.15), 60.0),
  ).map(coords => grid(columns: (7fr, 3fr), align: center, code1, [
    #plot_ball(coords.at(0))
    #v(-10%)
    #plot1(coords.at(1) / 2)
  ]))
  let anim2 = (
    ((0.2, 2.10), 00.0), ((1.0, 1.10), 00.5), ((1.8, 0.20), 01.0),
    ((2.5, 1.30), 01.5), ((3.1, 2.10), 02.0), ((3.4, 2.15), 03.5),
    ((3.7, 2.05), 05.5), ((4.3, 1.20), 07.0), ((5.1, 0.15), 07.5),
    ((5.8, 1.15), 08.2), ((6.5, 2.05), 08.5), ((6.6, 2.15), 08.6),
    ((6.5, 2.10), 09.2), ((5.9, 1.30), 09.8), ((5.2, 0.20), 10.2),
    ((4.4, 1.10), 11.0), ((5.1, 0.15), 12.5), ((5.3, 0.30), 13.0),
    ((5.1, 0.15), 14.0), ((4.9, 0.30), 16.0), ((5.1, 0.15), 20.0),
    ((5.1, 0.15), 22.0), ((5.1, 0.15), 30.0), ((5.1, 0.15), 50.0),
    ((5.1, 0.15), 60.0),
  ).map(coords => grid(columns: (7fr, 3fr), align: center, code2, [
    #plot_ball(coords.at(0))
    #v(-10%)
    #plot2(coords.at(1) / 2)
  ]))
  alternatives(
    align(center, cetz.canvas({
      cetz-plot.plot.plot(size: (15, 5), x-tick-step: none, y-tick-step: none,
        axis-style: "left", y-label: none, x-label: `p`, {
        cetz-plot.plot.add(t => calc.cos(t), domain: (0, 13), samples: 500)
      })
      cetz.draw.circle((0.4, 5.25), radius: 0.3)
      cetz.draw.line((0.8, 5), (1.5, 4.5), mark: (end: "straight"))
    })),
    grid(columns: (7fr, 3fr), align: center, code1, []), ..anim1,
    grid(columns: (7fr, 3fr), align: center, code2, []), ..anim2,
  )
}
#only(47)[This is the main issue with assertions]

== Summary

- Extension of a synchronous kernel to continuous time (```zelus der```,
  ```zelus init```, ...)
- Scheduling of discrete steps using zero-crossing events (```zelus up```, ...)
- Execution using a numerical solver
- Simultaneous simulation causes interferences

= Formalizing the Runtime

== Numerical Solvers

- Used to solve the model's initial value problem
- Integration is done _sequentially_ on successive intervals

$ italic("csolve")(italic("ivp")) :
    (h : Time) -> (h' : [0, h]) times (u : [0, h'] -> Y) $

#pause

#align(center, {
  import cetz-plot.plot: *
  
  let p(b, t) = cetz.canvas(plot(
    size: (10, 2), axis-style: "school-book", legend: (9.2, 2.5),
    y-tick-step: none, y-label: none, y-min: 0, y-max: 5, x-tick-step: none,
    x-label: none, x-min: 0, x-max: 5.5, x-ticks: t, b
  ))
  alternatives(
    p({
      add(domain: (0, 2), t => calc.sin(t) + t, label: $u$)
    }, ((2, $h'$), (5, $h$))),
    p({
      add(domain: (2, 4), t => calc.sin(t) + t, label: $u$)
      add(domain: (0, 2), t => calc.sin(t) + t)
    }, ((2, ""), (4, $h'$), (5, $h$))),
    p({
      add(domain: (4, 5), t => calc.sin(t) + t, label: $u$)
      add(domain: (0, 4), t => calc.sin(t) + t)
    }, ((2, ""), (4, ""), (5, $h', h$)))
  )
}) #pause #pause #pause
#only("5-")[- Solvers maintain their own internal state]
#only("6-")[- Viewed as discrete nodes]

== Zero-crossing Detection

- Detection of zero-crossing events using the integration results \
  $ italic("zsolve")(f_"zero") : (h : Time) times ([0, h] -> Y) -> (h' : [0, h]) times italic("Option")(Z_i) $
#pause
#align(center, alternatives(
  cetz.canvas({
    cetz-plot.plot.plot(
      size: (10, 2), axis-style: "school-book", legend: (9, 2.5),
      y-tick-step: none, y-label: none, y-min: -2, y-max: 5,
      x-tick-step: none, x-label: none, x-min: 0, x-max: 2.2,
      x-ticks: ((2/3, $h', h$),), {
      cetz-plot.plot.add(domain: (0, 2/3), t => t * t - 1)
    })
  }),
  cetz.canvas({
    cetz-plot.plot.plot(
      size: (10, 2), axis-style: "school-book", legend: (9, 2.5),
      y-tick-step: none, y-label: none, y-min: -2, y-max: 5,
      x-tick-step: none, x-label: none, x-min: 0, x-max: 2.2,
      x-ticks: ((1, $h'$), (4/3, $h$)), {
      cetz-plot.plot.add(domain: (2/3, 4/3), t => t * t - 1)
      cetz-plot.plot.add(domain: (0, 2/3), t => t * t - 1)
    })
    cetz.draw.line((4.55, 2.5), (4.55, 1.5), mark: (end: "straight"))
  }),
  cetz.canvas({
    cetz-plot.plot.plot(
      size: (10, 2), axis-style: "school-book", legend: (9, 2.5),
      y-tick-step: none, y-label: none, y-min: -2, y-max: 5,
      x-tick-step: none, x-label: none, x-min: 0, x-max: 2.2,
      x-ticks: ((1, ""), (2, $h', h$),), {
      cetz-plot.plot.add(domain: (1, 2), t => -t * t + 3.5 * t)
      cetz-plot.plot.add(domain: (0, 1), t => t * t - 1)
    })
  })
))
#pause
- Discrete steps are performed when a zero-crossing event is detected #pause
- State changes may occur during discrete steps
#pause
- Viewed as discrete nodes

== Full simulation

- Simulations are discrete nodes on streams of functions
- Two step modes: discrete and continuous

#align(center + horizon, grid(columns: (1fr, 1fr), {
  let a(s) = finite.automaton(
    (D: (D: "", C: ""),
     C: (C: "", D: "zero-crossing")),
    initial: "D", final: (), layout: finite.layout.linear.with(spacing: 6),
    style: s
  )
  alternatives(
    a((D: (fill: gray))),
    a((C: (fill: gray), D-C: (stroke: red))),
    a((C: (fill: gray), C-C: (stroke: red))),
    a((D: (fill: gray), C-D: (stroke: red))),
    a((C: (fill: gray), D-C: (stroke: red))),
    a((C: (fill: gray), C-C: (stroke: red))),
    a((D: (fill: gray), C-D: (stroke: red))),
    a((D: (fill: gray), D-D: (stroke: red))),
    a((C: (fill: gray), D-C: (stroke: red))),
  )
}, {
  let p(b, t: ()) = cetz.canvas(cetz-plot.plot.plot(
    size: (8, 5), axis-style: "school-book",
    x-tick-step: none, x-label: none, x-min: 0, x-max: 10,
    y-tick-step: none, y-label: none, y-min: -3, y-max: 10, b,
    x-ticks: t, x-grid: "both"
  ))
  alternatives[#p({
    cetz-plot.plot.add(t => calc.sin(t - 1/(0.1*t+0.1)) + 8 + 0.1 * t,
        domain: (0, 10), label: "in", samples: 500, style: (stroke: 2pt + blue))
    cetz-plot.plot.add(((0, 4),), label: "out", style: (stroke: 2pt + red))
    cetz-plot.plot.add(((0, -1),), label: "zero", style: (stroke: 2pt + green))
  })][#p({
    cetz-plot.plot.add(t => calc.sin(t - 1/(0.1*t+0.1)) + 8 + 0.1 * t,
        domain: (0, 10), label: "in", samples: 500, style: (stroke: 2pt + blue))
    cetz-plot.plot.add(t => calc.cos(t) + 3, domain: (0, 2), label: "out", style: (stroke: 2pt + red))
    cetz-plot.plot.add(t => 0.2 * t * t - 1, domain: (0, 2), label: "zero", style: (stroke: 2pt + green))
  })][#p({
    cetz-plot.plot.add(t => calc.sin(t - 1/(0.1*t+0.1)) + 8 + 0.1 * t,
        domain: (0, 10), label: "in", samples: 500, style: (stroke: 2pt + blue))
    cetz-plot.plot.add(t => calc.cos(t) + 3, domain: (0, 3), label: "out", style: (stroke: 2pt + red))
    cetz-plot.plot.add(t => 0.2 * t * t - 1, domain: (0, 3), label: "zero", style: (stroke: 2pt + green))
  }, t: ((2.25, ""),))][#p({
    cetz-plot.plot.add(t => calc.sin(t - 1/(0.1*t+0.1)) + 8 + 0.1 * t,
        domain: (0, 10), label: "in", samples: 500, style: (stroke: 2pt + blue))
    cetz-plot.plot.add(t => calc.cos(t) + 3, domain: (0, 2.25), label: "out", style: (stroke: 2pt + red))
    cetz-plot.plot.add(t => 0.2 * t * t - 1, domain: (0, 2.25), label: "zero", style: (stroke: 2pt + green))
    cetz-plot.plot.add(((2.25, 3),), mark-style: (stroke: red + 2pt), mark: "+", mark-size: .04)
    cetz-plot.plot.add(((2.25, -1),), mark-style: (stroke: green + 2pt), mark: "+", mark-size: .04)
  })][#p({
    cetz-plot.plot.add(t => calc.sin(t - 1/(0.1*t+0.1)) + 8 + 0.1 * t,
        domain: (0, 10), label: "in", samples: 500, style: (stroke: 2pt + blue))
    cetz-plot.plot.add(t => calc.cos(t) + 3, domain: (0, 2.25), label: "out", style: (stroke: 2pt + red))
    cetz-plot.plot.add(t => 0.2 * t * t - 1, domain: (0, 2.25), label: "zero", style: (stroke: 2pt + green))
    cetz-plot.plot.add(t => calc.cos(t) + 3.65, domain: (2.25, 6), style: (stroke: red + 2pt))
    cetz-plot.plot.add(t => calc.sin(t) + (0.2 * (t - 2.25)) - 1.8, domain: (2.25, 6), style: (stroke: green + 2pt))
  })][#p({
    cetz-plot.plot.add(t => calc.sin(t - 1/(0.1*t+0.1)) + 8 + 0.1 * t,
        domain: (0, 10), label: "in", samples: 500, style: (stroke: 2pt + blue))
    cetz-plot.plot.add(t => calc.cos(t) + 3, domain: (0, 2.25), label: "out", style: (stroke: 2pt + red))
    cetz-plot.plot.add(t => 0.2 * t * t - 1, domain: (0, 2.25), label: "zero", style: (stroke: 2pt + green))
    cetz-plot.plot.add(t => calc.cos(t) + 3.65, domain: (2.25, 8), style: (stroke: red + 2pt))
    cetz-plot.plot.add(t => calc.sin(t) + (0.2 * (t - 2.25)) - 1.8, domain: (2.25, 8), style: (stroke: green + 2pt))
  }, t: ((7.2, ""),))][#p({
    cetz-plot.plot.add(t => calc.sin(t - 1/(0.1*t+0.1)) + 8 + 0.1 * t,
        domain: (0, 10), label: "in", samples: 500, style: (stroke: 2pt + blue))
    cetz-plot.plot.add(t => calc.cos(t) + 3, domain: (0, 2.25), label: "out", style: (stroke: 2pt + red))
    cetz-plot.plot.add(t => 0.2 * t * t - 1, domain: (0, 2.25), label: "zero", style: (stroke: 2pt + green))
    cetz-plot.plot.add(t => calc.cos(t) + 3.65, domain: (2.25, 7.2), style: (stroke: red + 2pt))
    cetz-plot.plot.add(t => calc.sin(t) + (0.2 * (t - 2.25)) - 1.8, domain: (2.25, 7.2), style: (stroke: green + 2pt))
    cetz-plot.plot.add(((7.2, 5),), mark-style: (stroke: red + 2pt), mark: "+", mark-size: .04)
    cetz-plot.plot.add(((7.2, 1),), mark-style: (stroke: green + 2pt), mark: "+", mark-size: .04)
  })][#p({
    cetz-plot.plot.add(t => calc.sin(t - 1/(0.1*t+0.1)) + 8 + 0.1 * t,
        domain: (0, 10), label: "in", samples: 500, style: (stroke: 2pt + blue))
    cetz-plot.plot.add(t => calc.cos(t) + 3, domain: (0, 2.25), label: "out", style: (stroke: 2pt + red))
    cetz-plot.plot.add(t => 0.2 * t * t - 1, domain: (0, 2.25), label: "zero", style: (stroke: 2pt + green))
    cetz-plot.plot.add(t => calc.cos(t) + 3.65, domain: (2.25, 7.2), style: (stroke: red + 2pt))
    cetz-plot.plot.add(t => calc.sin(t) + (0.2 * (t - 2.25)) - 1.8, domain: (2.25, 7.2), style: (stroke: green + 2pt))
    cetz-plot.plot.add(((7.2, 5),), mark-style: (stroke: red + 2pt), mark: "+", mark-size: .04)
    cetz-plot.plot.add(((7.2, 1),), mark-style: (stroke: green + 2pt), mark: "+", mark-size: .04)
    cetz-plot.plot.add(((7.2, 6),), mark-style: (stroke: red + 2pt), mark: "+", mark-size: .04)
    cetz-plot.plot.add(((7.2, -1),), mark-style: (stroke: green + 2pt), mark: "+", mark-size: .04)
  })][#p({
    cetz-plot.plot.add(t => calc.sin(t - 1/(0.1*t+0.1)) + 8 + 0.1 * t,
        domain: (0, 10), label: "in", samples: 500, style: (stroke: 2pt + blue))
    cetz-plot.plot.add(t => calc.cos(t) + 3, domain: (0, 2.25), label: "out", style: (stroke: 2pt + red))
    cetz-plot.plot.add(t => 0.2 * t * t - 1, domain: (0, 2.25), label: "zero", style: (stroke: 2pt + green))
    cetz-plot.plot.add(t => calc.cos(t) + 3.65, domain: (2.25, 7.2), style: (stroke: red + 2pt))
    cetz-plot.plot.add(t => calc.sin(t) + (0.2 * (t - 2.25)) - 1.8, domain: (2.25, 7.2), style: (stroke: green + 2pt))
    cetz-plot.plot.add(((7.2, 5),), mark-style: (stroke: red + 2pt), mark: "+", mark-size: .04)
    cetz-plot.plot.add(((7.2, 1),), mark-style: (stroke: green + 2pt), mark: "+", mark-size: .04)
    cetz-plot.plot.add(t => t * (0.04 * calc.cos(t)) - 0.2 * (1 / t * t) + 6, domain: (7.2, 10), style: (stroke: red + 2pt))
    cetz-plot.plot.add(t => calc.sin(t) + (0.2 * (t - 2.25)) - 2.8, domain: (7.2, 10), style: (stroke: green + 2pt))
  })]
}))

== Lifting simulations

- We can manipulate simulations directly in #zelus

```zelus
type 'a dense  = time * (time -> 'a)
type 'a signal = 'a dense option
val solve : ('a -C-> 'b) -S-> ('a signal -D-> 'b signal)
```
#pause
- Running part of the model with its own solver instance is possible #pause
- This is exactly what we need for assertions!

== Simulating assertions

- Compile models with assertions down to two separate models
#pause
- Simulate the assertion independently with `solve`
#pause
- At each step of the parent model, run the assertion up to the horizon

#align(center, {
  let p(b, t) = cetz.canvas(cetz-plot.plot.plot(
    size: (10, 4), axis-style: "left",
    x-label: none, y-label: none, x-tick-step: none, y-tick-step: none,
    y-min: 0, x-min: 0.1, x-max: 10, x-ticks: t,
    b
  ))
  import cetz-plot.plot: add
  alternatives(
    p({
      add(t => calc.sin(t) + 5, domain: (0, 5), label: "Parent", samples: 500)
      add(((0, 0),), label: "Assertion", samples: 500)
    }, ((5, ""),)),
    p({
      add(t => calc.sin(t) + 5, domain: (0, 5), label: "Parent", samples: 500)
      add(t => calc.cos(2 * t) + 2, domain: (0, 2), label: "Assertion", samples: 500)
    }, ((5, ""), (2, ""))),
    p({
      add(t => calc.sin(t) + 5, domain: (0, 5), label: "Parent", samples: 500)
      add(t => calc.cos(2 * t) + 2, domain: (0, 5), label: "Assertion", samples: 500)
    }, ((5, ""), (2, ""))),
    p({
      add(t => calc.sin(t) + 5, domain: (0, 10), label: "Parent", samples: 500)
      add(t => calc.cos(2 * t) + 2, domain: (0, 5), label: "Assertion", samples: 500)
    }, ((5, ""), (2, ""), (10, ""))),
    p({
      add(t => calc.sin(t) + 5, domain: (0, 10), label: "Parent", samples: 500)
      add(t => calc.cos(2 * t) + 2, domain: (0, 7), label: "Assertion", samples: 500)
    }, ((5, ""), (2, ""), (10, ""), (7, ""))),
    p({
      add(t => calc.sin(t) + 5, domain: (0, 10), label: "Parent", samples: 500)
      add(t => calc.cos(2 * t) + 2, domain: (0, 9), label: "Assertion", samples: 500)
    }, ((5, ""), (2, ""), (10, ""), (7, ""), (9, ""))),
    p({
      add(t => calc.sin(t) + 5, domain: (0, 10), label: "Parent", samples: 500)
      add(t => calc.cos(2 * t) + 2, domain: (0, 10), label: "Assertion", samples: 500)
    }, ((5, ""), (2, ""), (10, ""), (7, ""), (9, ""))),
  )
})

= Conclusion

== Conclusion

*Results*
- Efficient implementation of a hybrid system simulation runtime
- Primitives to allow manipulation of simulations directly in #zelus
- Assertions representable as continuous observers
#pause

*Future Work*
- Implementation of a compilation pass (in progress)
- Support for _nested assertions_
- Concerns related to lifting simulations (can we use ```zelus pre```)?