637 lines
24 KiB
Typst
637 lines
24 KiB
Typst
|
|
#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```)?
|