feat: start of assertions
This commit is contained in:
parent
65918ab59b
commit
883e5fff01
GPG key ID:
7065F57ED8856128
6 changed files with 341 additions and 93 deletions
195
doc/notes.typ
195
doc/notes.typ
|
|
@ -129,13 +129,11 @@ cases:
|
|||
#columns(4, [#align(center, {
|
||||
import cetz: *
|
||||
import cetz-plot.plot: *
|
||||
let p = palette.new(colors: (blue,blue, blue)).with(stroke: true, fill: true)
|
||||
canvas({
|
||||
plot(
|
||||
size: (2,2), axis-style: "left", x-tick-step: none, x-label: none,
|
||||
x-ticks: ((1,none),), x-grid: "both", y-tick-step: none, y-label: none,
|
||||
y-min: 1, y-ticks: ((4, none),), y-grid: "both",
|
||||
style: p, {
|
||||
y-min: 1, y-ticks: ((4, none),), y-grid: "both", {
|
||||
add(((0,2),(.3,2.1),(.7,2.9),(1,3)), line: "spline")
|
||||
add(((1,4),), mark: "o", mark-size: .03)
|
||||
add(((1,5),(1.3,4.7),(1.7,3.2),(2,3)), line: "spline")
|
||||
|
|
@ -180,7 +178,6 @@ interval `[now, now + h]`, and end in one of three possible cases:
|
|||
#columns(3, [#align(center, {
|
||||
import cetz: *
|
||||
import cetz-plot.plot: *
|
||||
let p = palette.new(colors: (blue,blue, blue)).with(stroke: true, fill: true)
|
||||
canvas({
|
||||
plot(
|
||||
size: (2,2), axis-style: "left", x-tick-step: none, x-label: none,
|
||||
|
|
@ -319,6 +316,71 @@ advantage of not needing/having optional values in the input and output streams,
|
|||
and the calling system does not need to guess how many steps the simulation will
|
||||
need to reach the requested horizon.
|
||||
|
||||
=== Composing simulations
|
||||
|
||||
The composition of two simulations must maintain the following invariant: the
|
||||
output is only ever absent if the solvers have finished integrating up to the
|
||||
requested horizon. This is because we need to keep providing absent values
|
||||
(`None`) to the first simulation until it reaches the requested horizon,
|
||||
otherwise we reset beforehand, and the only information we have on whether the
|
||||
simulation has reached its horizon is the nature of its output. Naïve
|
||||
composition breaks this:
|
||||
|
||||
#grid(columns: (1fr, 1fr), align: center + horizon, cetz.canvas({
|
||||
import cetz.draw: *
|
||||
rect((0, 0), (1, 1))
|
||||
rect((2, 0), (3, 1))
|
||||
content((0.5, 0.5), $M$)
|
||||
content((2.5, 0.5), $N$)
|
||||
line((-0.5, 0.5), (0, 0.5), mark: (end: "straight"))
|
||||
line((1, 0.5), (2, 0.5), mark: (end: "straight"))
|
||||
line((3, 0.5), (3.5, 0.5), mark: (end: "straight"))
|
||||
}),
|
||||
$ M_i & : & a_1 & | & bot & |
|
||||
\ M_o & : & b_1 & | & b_2 & |
|
||||
\ N_i & : & b_1 & | & b_2 & |
|
||||
\ N_o & : & c_1 & | & #text(fill: red, $c_2$) & |
|
||||
$)
|
||||
|
||||
Instead, we need to make sure we only provide $N$ with a new value when
|
||||
needed. This is done through the following composition:
|
||||
#grid(columns: (1fr, 1fr), align: center + horizon, cetz.canvas({
|
||||
import cetz.draw: *
|
||||
rect((0, 0), (1, 1))
|
||||
rect((2, 0), (3, 1))
|
||||
content((0.5, 0.5), $M$)
|
||||
content((2.5, 0.5), $N$)
|
||||
line((-0.5, 0.5), (0, 0.5), mark: (end: "straight"))
|
||||
line((1, 0.5), (2, 0.5), mark: (end: "straight"))
|
||||
line((3, 0.5), (3.5, 0.5), mark: (end: "straight"))
|
||||
}),
|
||||
$ I &: & a_1 & | & bot & | & bot & & & | & bot & | & bot & & & |
|
||||
\ M_i &: & a_1 & | & & | & & | & bot & | & & | & & | & bot & |
|
||||
\ M_o &: & b_1 & | & & | & & | & b_2 & | & & | & & | & bot & |
|
||||
\ N_i &: & b_1 & | & bot & | & bot & | & b_2 & | & bot & | & bot & | & bot & |
|
||||
\ N_o &: & c_1 & | & c_2 & | & bot & | & c_3 & | & c_4 & | & bot & | & bot & |
|
||||
\ O &: & c_1 & | & c_2 & | & & & c_3 & | & c_4 & | & & & bot & |
|
||||
$)
|
||||
|
||||
```ocaml
|
||||
let step (ms, ns) = function
|
||||
| Some i ->
|
||||
let v, ms = m.step ms (Some i) in
|
||||
let o, ns = n.step ns v in
|
||||
o, (ms, ns)
|
||||
| None ->
|
||||
let o, ns = n.step ns None in
|
||||
match o with
|
||||
| Some o -> Some o, (ms, ns)
|
||||
| None ->
|
||||
let v, ms = m.step ms None in
|
||||
match v with
|
||||
| None -> None, (ms, ns)
|
||||
| Some v ->
|
||||
let o, ns = n.step ns (Some v) in
|
||||
o, (ms, ns)
|
||||
```
|
||||
|
||||
=== Resets
|
||||
|
||||
==== Solver reset
|
||||
|
|
@ -411,6 +473,67 @@ Two possible options for the simulation reset:
|
|||
makes this impossible. We thus need reset parameters for both the model and
|
||||
solver.
|
||||
|
||||
=== Assertions
|
||||
|
||||
Assertions are themselves hybrid systems, with their own internal state, `fder`,
|
||||
`fzer`, `fout` and `reset` functions, etc.
|
||||
A hybrid model with assertions is then a recursive datatype
|
||||
```ocaml
|
||||
type ('p, 'a, 'b, 'y, 'yder, 'zin, 'zout) hnode_a =
|
||||
HNodeA : {
|
||||
body : ('s, 'p,' a, 'b, 'y, 'yder, 'zin, 'zout) hrec;
|
||||
assertions : ('p, 's, float, 'y, 'yder, 'zin, 'zout) hnode_a list;
|
||||
}
|
||||
```
|
||||
|
||||
Assertions in sub-models need to be "lifted" to the parent model in order to be
|
||||
visible for the simulation. Since the inner state of sub-models is contained in
|
||||
the state of the parent model, these assertions can be composed with projectors
|
||||
on the inner state of the parent model in order to provide them with the correct
|
||||
state.
|
||||
|
||||
What does it mean for an assertion to run in continuous time ?
|
||||
There are two possible approaches:
|
||||
- Sampling: take "snapshots" of the state at various timestamps and check the
|
||||
assertions at these snapshots.
|
||||
- Problems: expensive memory usage, and requires state copies for the model.
|
||||
Can also impact stop times for the parent model, which defeats the point of
|
||||
transparent assertions.
|
||||
- Real-time: consider the solution provided by the solver as a continuous
|
||||
function and use it as input to monitor for zero-crossings
|
||||
- Problems: limits the expressions we can use in continuous assertions to
|
||||
continuous functions; boolean expressions are inherently discontinuous. We
|
||||
can model inequalities using zero-crossing constructs like `up`
|
||||
(for instance, `a <= b` $-->$ `up(a -. b)`).
|
||||
|
||||
Building a continuous function of the entire state is possible. Since the entire
|
||||
state can be considered as the sum of a discrete and a continuous part, and that
|
||||
the discrete part is considered piecewise-constant, we can build a function
|
||||
`time -> 's` using the model's `cset` function (which updates the state's
|
||||
continuous part) as follows:
|
||||
#grid(columns: (1fr, 1fr), align: center + horizon, ```ocaml
|
||||
let f_st (ms : 's) (f : time -> 'y) =
|
||||
fun t -> cset ms (f t)
|
||||
```, cetz.canvas({
|
||||
import cetz-plot.plot: *
|
||||
plot(
|
||||
axis-style: "left", x-label: none, x-tick-step: none,
|
||||
y-label: none, y-tick-step: none, y-min: 0.1, {
|
||||
add(((0, 1), (1, 1)), style: (stroke: blue), label: $D$)
|
||||
add(((1, 2), (2.5, 2)), style: (stroke: blue))
|
||||
add(domain: (0, 1), t => - calc.sin(t + 1) + 1.5, style: (stroke: red))
|
||||
add(domain: (1, 2.5), t => calc.sin(t) + 2, style: (stroke: red), label: $C$)
|
||||
})
|
||||
}))
|
||||
|
||||
If `cset` is pure (that is, it returns a copy of the state, rather than modify
|
||||
it in-place), this function poses no problem. If `cset` is not pure and modifies
|
||||
the state in-place, this is still useable as long as `f_state` is never used in
|
||||
parallel: since `cset` only modifies the continuous part of the state, we can
|
||||
always recover the original state by calling `f_state` with the appropriate
|
||||
horizon. However, the model's continuous state needs to be re-updated to the
|
||||
reached horizon after all assertions/submodels have finished running.
|
||||
|
||||
== Mathematical model
|
||||
|
||||
#link("https://zelus.di.ens.fr/cc2015/fullpaper.pdf")[[CC'15]] defines the
|
||||
|
|
@ -497,6 +620,70 @@ simulation loop as follows:
|
|||
models has much in common with code generation for synchronous languages.
|
||||
])
|
||||
|
||||
In [Branicky, 1995b], dynamical systems are defined as follows:
|
||||
|
||||
#block(fill: rgb(230, 230, 230), stroke: black, inset: 5pt, [
|
||||
A continuous (resp. discrete) dynamical system defined on the topological
|
||||
space $X$ over the semigroup $bb(R)^+$ (resp. $bb(Z)^+$) is a function
|
||||
$f : X times bb(R)^+ -> X$ (resp. $f : X times bb(Z)^+ -> X$) with the
|
||||
following three properties:
|
||||
1. initial condition: $f(p, 0) = p$,
|
||||
2. continuity on both arguments,
|
||||
3. semigroup property: $f(f(p, t_1), t_2) = f(p, t_1 + t_2)$
|
||||
for any point $p in X$ and any $t_1, t_2 in bb(R)^+$ (resp $bb(Z)^+$).
|
||||
|
||||
Technically, such functions are referred to as semidynamical systems, with the
|
||||
term dynamical system reserved for those which the semigroups $bb(R)^+$,
|
||||
$bb(Z)^+$ above may be replaced by the groups $bb(R)$, $bb(Z)$. However, the
|
||||
more "popular" notion of dynamical system in math and engineering - and the
|
||||
one used here - requires only the semigroup property. Thus, the term
|
||||
_reversible_ dynamical system is used when it is necessary to distinguish the
|
||||
group from semigroup case.
|
||||
|
||||
The shorthand $[X, S, f]$ denotes the dynamical system $f$ defined on $X$ over
|
||||
the semigroup $S$; $X$ is referred to as its _state space_ and points in $X$
|
||||
are called _states_. If a dynamical system is defined on a subset of $X$, we
|
||||
say it is a dynamical system _in_ $X$.
|
||||
|
||||
For every fixed value of the parameter $s$, the function $f(dot, s)$ defines
|
||||
a mapping of the space $X$ into itself. Given $[X, bb(Z)^+, f]$, $f(dot, 1)$
|
||||
is its _transition function_. Thus if $[X, bb(Z)^+, f]$ is reversible, its
|
||||
transition function is invertible, with inverse given by $f(dot, -1)$.
|
||||
|
||||
The set $f(p, S) = { f(p, i) | i in S }$ is called the _orbit_ or _trajectory_
|
||||
of the point $p$. A _fixed point_ of $[X, S, f]$ is a point $p$ such that
|
||||
$f(p, s) = p$ for all $s in S$. A set $A subset X$ is _invariant w.r.t._ $f$,
|
||||
or simply _invariant_, if $f(A, s) subset A$ for all $s in S$.
|
||||
|
||||
The notions of equivalence and homomorphism are crucial. Two dynamical systems
|
||||
$[X, S, f]$, $[Y, S, g]$ are said to be _isomorphic_ (also
|
||||
_topologically equivalent_ or simply _equivalent_) if there exists a
|
||||
homeomorphism $psi : X -> Y$ such that
|
||||
$ psi(f(p, s)) = g(psi(p), s) $
|
||||
for all $p in X$ and $s in S$. If the mapping $psi$ is only continuous, then
|
||||
$[X, S, f]$ is said to be _homomorphic_ to $[Y, S, g]$. Homomorphisms preserve
|
||||
trajectories, fixed points, and invariant sets.
|
||||
|
||||
In this paper, the continuous dynamical systems dealt with are defined by the
|
||||
solutions of ordinary differential equations (ODEs):
|
||||
$ x'(t) = f(x(t)) $
|
||||
where $x(t) in X subset bb(R)^n$. The function $f : X -> bb(R)^n$ is called a
|
||||
_vector field_ on $bb(R)^n$. The resulting dynamical system is then given by
|
||||
$phi(x_0, t) = x(t)$ where $x(dot)$ is the solution to the above equation
|
||||
starting at $x_0$ at $t = 0$. (We assume existence and uniqueness of
|
||||
solutions; see [Hirsch, Smalle] for conditions). A system of ODEs is called
|
||||
_autonomous_ or _time-invariant_ if its vector field does not depend
|
||||
explicitly on time. Throughout, the shorthand _continuous_ (resp. _Lipschitz_)
|
||||
_ODEs_ denotes ODEs with continuous (resp. Lipschitz) vector fields.
|
||||
|
||||
An ODE _with input and outputs_ is given by
|
||||
$ x'(t) & = f(x(t), u(t)), \ y(t) & = h(x(t)) $
|
||||
where $x(t) in X subset bb(R)^n$, $u(t) in U subset bb(R)^m$,
|
||||
$y in Y subset bb(R)^p$, $f : bb(R)^n times bb(R)^m -> bb(R)^n$, and
|
||||
$h : bb(R)^n -> bb(R)^p$. The functions $u(dot)$ and $y(dot)$ are the _inputs_
|
||||
and _outputs_, respectively.
|
||||
])
|
||||
|
||||
== Miscellaneous
|
||||
|
||||
=== Signals
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue