#import "@preview/cetz:0.4.0"
#import "@preview/finite:0.4.1"

#set page(paper: "a4")
#set par(justify: true)
#set raw(syntaxes: "zelus.sublime-syntax")
#show raw: set text(font: "CaskaydiaCove NF")

#let lustre = smallcaps[Lustre]
#let esterel = smallcaps[Esterel]
#let simulink = smallcaps[Simulink]
#let sundials = smallcaps[Sundials CVODE]
#let zelus = smallcaps[Zélus]
#let TODO(..what) = {
  let msg = if what.pos().len() == 0 { "" } else { ": " + what.pos().join("") }
  block(fill: red, width: 100%, inset: 5pt, align(center, raw("TODO" + msg)))
}
#let adot(s) = $accent(#s, dot)$
#let addot(s) = $accent(#s, dot.double)$

#align(center)[
  #text(16pt)[
    *Internship Report --- MPRI M2 \
    Hybrid System Models with Transparent Assertions*
  ]

  Henri Saudubray, supervised by Marc Pouzet, Inria PARKAS
]\

#heading(outlined: false)[General Context]
What is the report about? Where does the problem come from? What is the state of
the art in that area?

Hybrid systems modelers such as #simulink are essential tools in the development
of embedded systems evolving in physical environments. They allow for precise
descriptions of hybrid systems through both continuous-time behaviour defined
through Ordinary Differential Equations (ODEs) and discrete-time reactive
behaviour similar to what is found in the synchronous languages such as #lustre.
The #zelus language aims to reconcile synchronous languages with hybrid systems,
by taking a synchronous language kernel and extending it with continuous-time
constructs similar to what is found in tools like #simulink. Continuous-time
behaviour is computed through the use of an off-the-shelf ODE solver such as
#sundials.

#heading(outlined: false)[Research Problem]
What specific question(s) have you studied? What motivates the question? What
are the applications/consequences? Is it a new problem? Why did you choose this
problem?

The simulation of hybrid system models, as done in #simulink and #zelus, uses a
single ODE solver instance to simulate the entire model. This has various
advantages: it is less computationally intensive, and simplifies the work of the
compiler. Unfortunately, it also raises a difficult problem: sub-systems which
seemingly should not interfere with each other end up affecting each other's
results. This is due to the chosen integration method: an adaptive solver like
#sundials will vary its step length throughout the integration process, and the
addition of ODEs in the overall system can influence these step lengths,
affecting the results obtained for pre-existing ODEs. This is particularly
problematic in the case of runtime assertions, which are typically expected to
be transparent: they should not affect the final result of the computation.

#heading(outlined: false)[Proposed Contributions]
What is your answer to the research problem? Please remain at a high level;
technical details should be given in the main body of the report. Pay special
attention to the description of the _scientific_ approach.

To solve this, we propose a new runtime for the #zelus language, which simulates
assertions with their own solvers in order to maintain the separation between
assertions and the model they operate on.

#TODO()

#heading(outlined: false)[Arguments Supporting Their Validity]
What is the evidence that your solution is a good solution? (Experiments?
Proofs?) Comment on the robustness of your solution: does it rely on
assumptions, and if so, to what extent?

#TODO("Justify")

#heading(outlined: false)[Summary and Future Work]
What did you contribute to the area? What comes next? What is a good _next_ step
or question?

#TODO("Next steps")

#pagebreak()
#outline()
#pagebreak()

= Background

== Hybrid systems

Hybrid systems are dynamical systems whose behaviour evolves through both
continuous and discrete phases. They are used to model software interacting with
physical systems. Continuous phases are described using ordinary differential
equations (ODEs), while discrete phases can be represented as a reactive
program in a synchronous language such as #lustre or #esterel.

As a first example, say we wish to model a bouncing ball. We could start by
describing its distance from the ground $y$ with a second-order differential
equation
$ addot(y) = -9.81 $
where $addot(y)$ denotes the second order derivative of $y$ with
respect to time (the acceleration of the ball), and $9.81$ is the gravitational
constant $g$: the acceleration of the ball is its negation. We now give the
initial position and speed of the ball:
$ y(0) = 50 space space space adot(y)(0) = 0 $
We have just described an initial value problem: given an ODE and an initial
value for its dependent variable, its solution is a function $y(t)$ returning
the value of the variable at a given time $t$. We can find an approximation of
this function using an ODE solver, such as #sundials.

As of right now, our ball will fall until the end of time; we have not said
anything about how it bounces when it hits the floor. To do so, we need a notion
of discrete _events_. These are modelled by zero-crossings: we monitor a certain
value and stop when it goes from strictly negative to positive or null. For our
purposes, we choose $-y$ as the monitored value, and call the zero-crossing
event $z$. When $z$ occurs (i.e., when the ball touches the ground), we set the
speed $adot(y)$ to $-k dot "last"(adot(y))$, where $"last"(y)$ denotes the left
limit of $y$ (we cannot specify $adot(y)$ in terms of itself), and $k$ is a
factor modelling the loss of inertia due to the collision (say, $0.8$). We can
then resume the approximation of the solution.

@lst:ball.zls shows how such a model might be expressed in the concrete syntax
of #zelus.

#figure(placement: top, gap: 2em,
  ```zelus
  let hybrid ball () = y where
    rec der y = y' init 50.0
    and der y' = -9.81 init 0.0 reset z -> -0.8 *. (last y')
    and z = up (-. y)
  ```,
  caption: [The bouncing ball in #zelus]
) <lst:ball.zls>

More formally, a hybrid system can be described as an automaton

== Executing models

Executing such a model is quite simple. There are two modes of execution:
discrete and continuous. In continuous mode, we call the ODE solver in order to
obtain an approximation of the variables defined through ODEs, and monitor for
zero-crossings. If a zero-crossing occurs, we enter the discrete mode, in which
we perform computation steps as needed, until no other zero-crossing occurs, in
which case we go back to the continuous mode, and repeat, as seen in @automaton.

#figure(finite.automaton(
  (D: (D: "cascade", C: "no cascade"),
   C: (C: "no zero-crossing", D: "zero-crossing")),
  initial: "D", final: (), layout: finite.layout.linear.with(spacing: 3)
), caption: [High-level overview of the runtime], placement: top) <automaton>

= Runtime
To solve this issue, we need to redefine what the runtime of our hybrid system
models is. The runtime is the piece of software that handles the pairing of a
hybrid model with a solver and the different execution phases that need to take
place.

To allow for independent simulation of the assertions, we need to simulate them
with their own ODE solvers. Since assertions can themselves contain ODEs, they
can be viewed as hybrid systems themselves. Assertions can also contain their
own sub-assertions, and so recursively: our runtime needs to handle this
accordingly.

== Hybrid models with assertions
A hybrid model with assertions can be defined using a recursive data type:
```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, unit, 'y, 'yder, 'zin, 'zout) hnode_a list;
  } -> ('p, 'a, 'b, 'y, 'yder, 'zin, 'zout) hnode_a
```

Notice that the list of assertions takes as input the inner state of the parent
model: assertions are checked on the model state, and any variable which is
required by the assertion becomes a state variable.

== Solvers as synchronous nodes
== Simulations as synchronous nodes
#TODO("talk about the new runtime")

= Assertions
#TODO("talk about how assertions are done")

#pagebreak()
= Annex
#set heading(level: 2)
#bibliography("sources.bib", full: true)
#set heading(level: 1)