#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 note(color, prefix, ..what) = {
  let msg = if what.pos().len() == 0 { "" } else { ": " + what.pos().join("") }
  block(fill: color, width: 100%, inset: 5pt, align(center, raw(prefix + msg)))
}
#let TODO(..what) = note(red, "TODO", ..what)
#let MENTION(..what) = note(gray, "MENTION", ..what)
#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 an illustration, say we wished to model an extensively studied system: a
bouncing ball. We could start by describing its distance from the ground $y$ as
a function of time, with a second-order differential equation
$ addot(y) = -9.81, $
where $addot(y)$ denotes the second order derivative of $y$ with
respect to time $(d^2y)/(d t^2)$ (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 _events_: we need to identify exactly when the ball hits the ground, so that
we may take action to make it bounce. These events 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 #raw(lang: "zelus", "last")\(adot(y))$, where
$#raw(lang: "zelus", "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 @cit:zelus_sync_lng_with_ode.

#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, and as done in @cit:alg_ana_hyb_sys, a hybrid system $cal(H)$ can
be defined as a graph whose nodes represent continuous behaviour, and whose
edges represent discrete transitions:
$ cal(H) = (L o c, V a r, E d g, A c t, I n v, I n i) $
where:
- $L o c$ is a finite set of _locations_;
- $V a r$ is a finite set of _variables_;
- $E d g subset.eq L o c times F times L o c$ is a finite set of _transitions_


== Executing models

To execute such a model, we first compile it into a synchronous function, as
described in @cit:sync_based_codegen_hyb_sys_lng. The details of this
compilation step are not particularly relevant to our purposes, and can be
ignored. What is more interesting is the output of this compilation step: a
single synchronous function. The simulation loop is then itself described as a
synchronous function operating on

#MENTION("Use of a single solver")

#pagebreak()

// The compilation of a hybrid model into a synchronous function is described in
// detail in @cit:sync_based_codegen_hyb_sys_lng, but can be summarized quite
// succintly as follows. By pairing this synchronous function with an
// off-the-shelf ODE solver like #sundials, we can then simulate the dynamics of
// the system. This is done by repeatedly performing execution steps according to
// two different modes: discrete and continuous.

// The continuous mode operates as follows: we first call the ODE solver in order
// to approximate the dynamics of the model's continuous state.

// Continuous steps first call the ODE solver to approximate the dynamics of the
// model's continuous variables. The solver will return a function defined on a
// time interval, which we then provide as input to the zero-crossing solver, which
// will monitor the evolution of zero-crossing values along this interval. After
// both solvers have been called, we choose what the next step's mode will be:
// - if no zero-crossings have been detected, we output the entire solution
//   provided by the ODE solver, and the next step remains continuous;
// - if a zero-crossing occurs, we return the solution provided by the ODE solver
//   up to the zero-crossing instant, and the next step becomes a discrete step.

// Discrete steps perform state changes and side effects. We first call the model's
// step function, which updates the state and outputs a value. We then decide what
// the next step is. If a zero-crossing event occured due to the current step, the
// next step is another discrete step. If no new event occured, we perform a
// continuous step.

// 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
#MENTION("the new runtime")

= Assertions
#MENTION("how assertions are done")

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