**Lelio Brun** • Christophe Garion • Pierre-Loïc Garoche • Xavier Thirioux

SCADE Suite

KCG Code Generator

` ````
node count() returns (out: bool)
var time, ptime: int;
init, b: bool;
let
init = true -> false;
b = (ptime = 3);
time = if init then 0
else if b then 0
else ptime + 1;
ptime = pre time;
out = (time = 2);
tel
```

` ````
node count() returns (out: bool)
var time, ptime: int;
init, b: bool;
let
out = (time = 2);
b = (ptime = 3);
ptime = pre time;
time = if init then 0
else if b then 0
else ptime + 1;
init = true -> false;
tel
```

` ````
node count() returns (out: bool)
var time, ptime: int;
init, b: bool;
let
init = true -> false;
b = (ptime = 3);
time = if init then 0
else if b then 0
else ptime + 1;
ptime = pre time;
out = (time = 2);
tel
```

```
// state initialization
n_reset(&self);
// execution loop
while (1) {
read_input(&x);
// execution step
n_step(x, &y, &self);
write_output(y);
}
```

```
node count() returns (out: bool)
var time, ptime: int; init, b: bool;
let
init = true -> false;
b = (ptime = 3);
time = if init then 0 else if b then 0 else ptime + 1;
ptime = pre time;
out = (time = 2);
tel
```

```
machine count {
state ptime: int;
instance a: _arrow;
step () => (out: bool) {
var time: int; init, b: bool;
init := a.step(true, false);
b := state(ptime) = 3;
if (init) { time := 0 } else { if (b) { time := 0 } else { time := state(ptime) + 1 } }
state(ptime) := time;
out := (time = 2);
}
}
```

```
machine count {
state ptime: int;
instance a: _arrow;
step () => (out: bool) {
var time: int; init, b: bool;
init := a.step(true, false);
b := state(ptime) = 3;
if (init) { time := 0 } else { if (b) { time := 0 } else { time := state(ptime) + 1 } }
state(ptime) := time;
out := (time = 2);
}
}
```

```
struct count_mem { _Bool _reset; int ptime; struct _arrow_mem *a; };
#define count_set_reset(self) { self->_reset = 1; }
void count_clear_reset(struct count_mem *self ) {
if (self->_reset) {
self->_reset = 0;
_arrow_reset(self->a);
}
}
void count_step(_Bool *out, struct count_mem *self) {
int time; _Bool init, b;
count_clear_reset(self);
init = _arrow_step(self->a);
b = self->ptime == 3;
if (init) { time = 0; } else { if (b) { time = 0; } else { time = self->ptime + 1; } }
self->ptime = time;
*out = time == 2;
}
```

```
node count() returns (out: bool)
var time, ptime: int;
init, b: bool;
let
init = true -> false;
b = (ptime = 3);
time = if init then 0
else if b then 0
else ptime + 1;
ptime = pre time;
out = (time = 2);
tel
```

\[
\newcommand\paren[1]{\left(#1\right)}
\newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}}
\newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}}
\newcommand\treel[2]{#1\!\paren{#2}}
\newcommand\treen[2]{#1\!\left[#2\right]}
\begin{split}
& \tr{} {count} S {out} {S'} \triangleq \\
& \quad \tr{5} {count} S {out} {S'} \\
& \quad\quad\begin{aligned}
& \phantom{\wedge \exists b,\, init,}\\
& \quad\quad\begin{aligned}
& \phantom{\wedge \tr{} {arrow} {\treen S a} {init} {\treen {S'} a}} \\
& \phantom{\wedge b = \left(\treel S {ptime} = 3\right)} \\
& \phantom{\wedge init \implies {time = 0}} \\
& \phantom{\wedge (\neg {init} \wedge b) \implies {time = 0}} \\
& \phantom{\wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1} \\
\end{aligned} \\
& \phantom{\wedge \treel {S'} {ptime} = time}\\
& \phantom{\wedge out = \left(time = 2\right)} \\
\end{aligned}
\end{split}
\]

```
node count() returns (out: bool)
var time, ptime: int;
init, b: bool;
let
init = true -> false;
b = (ptime = 3);
time = if init then 0
else if b then 0
else ptime + 1;
ptime = pre time;
out = (time = 2);
tel
```

\[
\newcommand\paren[1]{\left(#1\right)}
\newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}}
\newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}}
\newcommand\treel[2]{#1\!\paren{#2}}
\newcommand\treen[2]{#1\!\left[#2\right]}
\begin{split}
& \tr{} {count} S {out} {S'} \triangleq \\
& \quad \exists time,\\
& \quad\quad\begin{aligned}
& \phantom{\wedge} \tr{4} {count} S {time} {S'}\\
& \quad\quad\begin{aligned}
& \phantom{\wedge \tr{} {arrow} {\treen S a} {init} {\treen {S'} a}} \\
& \phantom{\wedge b = \left(\treel S {ptime} = 3\right)} \\
& \phantom{\wedge init \implies {time = 0}} \\
& \phantom{\wedge (\neg {init} \wedge b) \implies {time = 0}} \\
& \phantom{\wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1} \\
\end{aligned} \\
& \phantom{\wedge \treel {S'} {ptime} = time}\\
& \wedge out = \left(time = 2\right) \\
\end{aligned}
\end{split}
\]

```
node count() returns (out: bool)
var time, ptime: int;
init, b: bool;
let
init = true -> false;
b = (ptime = 3);
time = if init then 0
else if b then 0
else ptime + 1;
ptime = pre time;
out = (time = 2);
tel
```

\[
\newcommand\paren[1]{\left(#1\right)}
\newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}}
\newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}}
\newcommand\treel[2]{#1\!\paren{#2}}
\newcommand\treen[2]{#1\!\left[#2\right]}
\begin{split}
& \tr{} {count} S {out} {S'} \triangleq \\
& \quad \exists time,\\
& \quad\quad\begin{aligned}
& \phantom{\wedge}\tr{3} {count} S {time} {S'}\\
& \quad\quad\begin{aligned}
& \phantom{\wedge \tr{} {arrow} {\treen S a} {init} {\treen {S'} a}} \\
& \phantom{\wedge b = \left(\treel S {ptime} = 3\right)} \\
& \phantom{\wedge init \implies {time = 0}} \\
& \phantom{\wedge (\neg {init} \wedge b) \implies {time = 0}} \\
& \phantom{\wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1} \\
\end{aligned} \\
& \wedge \treel {S'} {ptime} = time\\
& \wedge out = \left(time = 2\right) \\
\end{aligned}
\end{split}
\]

```
node count() returns (out: bool)
var time, ptime: int;
init, b: bool;
let
init = true -> false;
b = (ptime = 3);
time = if init then 0
else if b then 0
else ptime + 1;
ptime = pre time;
out = (time = 2);
tel
```

\[
\newcommand\paren[1]{\left(#1\right)}
\newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}}
\newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}}
\newcommand\treel[2]{#1\!\paren{#2}}
\newcommand\treen[2]{#1\!\left[#2\right]}
\begin{split}
& \tr{} {count} S {out} {S'} \triangleq \\
& \quad \exists time,\\
& \quad\quad\begin{aligned}
& \phantom{\wedge}\exists b,\, init, \\
& \quad\quad\begin{aligned}
& \phantom{\wedge} \tr{2} {count} S {time} {S'} \\
& \phantom{\wedge b = \left(\treel S {ptime} = 3\right)} \\
& \wedge init \implies {time = 0} \\
& \wedge (\neg {init} \wedge b) \implies {time = 0} \\
& \wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1 \\
\end{aligned} \\
& \wedge \treel {S'} {ptime} = time\\
& \wedge out = \left(time = 2\right) \\
\end{aligned}
\end{split}
\]

```
node count() returns (out: bool)
var time, ptime: int;
init, b: bool;
let
init = true -> false;
b = (ptime = 3);
time = if init then 0
else if b then 0
else ptime + 1;
ptime = pre time;
out = (time = 2);
tel
```

\[
\newcommand\paren[1]{\left(#1\right)}
\newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}}
\newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}}
\newcommand\treel[2]{#1\!\paren{#2}}
\newcommand\treen[2]{#1\!\left[#2\right]}
\begin{split}
& \tr{} {count} S {out} {S'} \triangleq \\
& \quad \exists time,\\
& \quad\quad\begin{aligned}
& \phantom{\wedge}\exists b,\, init, \\
& \quad\quad\begin{aligned}
& \phantom{\wedge} \tr{1} {count} S {time} {S'} \\
& \wedge b = \left(\treel S {ptime} = 3\right) \\
& \wedge init \implies {time = 0} \\
& \wedge (\neg {init} \wedge b) \implies {time = 0} \\
& \wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1 \\
\end{aligned} \\
& \wedge \treel {S'} {ptime} = time\\
& \wedge out = \left(time = 2\right) \\
\end{aligned}
\end{split}
\]

```
node count() returns (out: bool)
var time, ptime: int;
init, b: bool;
let
init = true -> false;
b = (ptime = 3);
time = if init then 0
else if b then 0
else ptime + 1;
ptime = pre time;
out = (time = 2);
tel
```

\[
\newcommand\paren[1]{\left(#1\right)}
\newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}}
\newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}}
\newcommand\treel[2]{#1\!\paren{#2}}
\newcommand\treen[2]{#1\!\left[#2\right]}
\begin{split}
& \tr{} {count} S {out} {S'} \triangleq \\
& \quad \exists time,\\
& \quad\quad\begin{aligned}
& \phantom{\wedge} \exists b,\, init,\\
& \quad\quad\begin{aligned}
& \phantom{\wedge} \tr{} {arrow} {\treen S a} {init} {\treen {S'} a} \\
& \wedge b = \left(\treel S {ptime} = 3\right) \\
& \wedge init \implies {time = 0} \\
& \wedge (\neg {init} \wedge b) \implies {time = 0} \\
& \wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1 \\
\end{aligned} \\
& \wedge \treel {S'} {ptime} = time\\
& \wedge out = \left(time = 2\right) \\
\end{aligned}
\end{split}
\]

```
node count() returns (out: bool)
var time, ptime: int;
init, b: bool;
let
init = true -> false;
b = (ptime = 3);
time = if init then 0
else if b then 0
else ptime + 1;
ptime = pre time;
out = (time = 2);
tel
```

\[
\newcommand\paren[1]{\left(#1\right)}
\newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}}
\newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}}
\newcommand\treel[2]{#1\!\paren{#2}}
\newcommand\treen[2]{#1\!\left[#2\right]}
\begin{split}
& \tr{} {count} S {out} {S'} \triangleq \\
& \quad \exists time,\\
& \quad\quad\begin{aligned}
& \phantom{\wedge} \exists b,\, init,\\
& \quad\quad\begin{aligned}
& \phantom{\wedge} \tr{} {arrow} {\treen S a} {init} {\treen {S'} a} \\
& \wedge b = \left(\treel S {ptime} = 3\right) \\
& \wedge init \implies {time = 0} \\
& \wedge (\neg {init} \wedge b) \implies {time = 0} \\
& \wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1 \\
\end{aligned} \\
& \wedge \treel {S'} {ptime} = time\\
& \wedge out = \left(time = 2\right) \\
\end{aligned}
\end{split}
\]

```
/*@ requires count_pack(*mem, self);
ensures count_pack(*mem, self);
ensures count_tr(\old(*mem), *out, *mem); */
void count_step(_Bool *out, struct count_mem *self)
/*@ ghost (struct count_mem_ghost \ghost *mem) */ {
int time; _Bool init, b;
count_clear_reset(self);
init = _arrow_step(self->a) /*@ ghost (&mem->a) */;
//@ assert count_tr1(\at(*mem, Pre), b, *mem);
b = self->ptime == 3;
//@ assert count_tr2(\at(*mem, Pre), b, init, *mem);
if (init) { time = 0; } else { if (b) { time = 0; } else { time = self->ptime + 1; } }
//@ assert count_tr3(\at(*mem, Pre), time, *mem);
self->ptime = time;
//@ ghost mem->ptime = time;
//@ assert count_tr4(\at(*mem, Pre), time, *mem);
*out = time == 2;
//@ assert count_tr5(\at(*mem, Pre), *out, *mem);
}
```

~400 files | ✓ 92.7% |

~231 500 POs | ✓ 99.9% |

` ````
type en1 = enum { On, Off };
type en2 = enum { Up, Down };
node clocks (x: int) returns (y: int)
var c: en1 clock; d: en2 clock; b1, b2, b3, z: int; c1, c2: bool
let
c1 = (x >= 0);
d = if c1 then Up else Down;
c2 = (x = 0) when Up(d);
c = if c2 then Off else On;
b2 = 2 when Off(c);
b1 = 1 when On(c);
z = merge c (On -> b1) (Off -> b2);
b3 = 3 when Down(d);
y = merge d (Up -> z) (Down -> b3);
tel
```

` ````
type en1 = enum { On, Off };
type en2 = enum { Up, Down };
node clocks (x: int) returns (y: int)
var c: en1 clock; d: en2 clock; b1, b2, b3, z: int; c1, c2: bool
let
c1 = (x >= 0);
d = if c1 then Up else Down;
c2 = (x = 0) when Up(d);
c = if c2 then Off else On;
b2 = 2 when Off(c);
b1 = 1 when On(c);
z = merge c (On -> b1) (Off -> b2);
b3 = 3 when Down(d);
y = merge d (Up -> z) (Down -> b3);
tel
```

` ````
type en1 = enum { On, Off };
type en2 = enum { Up, Down };
node clocks (x: int) returns (y: int)
var c: en1 clock; d: en2 clock; b1, b2, b3, z: int; c1, c2: bool
let
c1 = (x >= 0);
d = if c1 then Up else Down;
c2 = (x = 0) when Up(d);
c = if c2 then Off else On;
b2 = 2 when Off(c);
b1 = 1 when On(c);
z = merge c (On -> b1) (Off -> b2);
b3 = 3 when Down(d);
y = merge d (Up -> z) (Down -> b3);
tel
```

` ````
type en1 = enum { On, Off };
type en2 = enum { Up, Down };
node clocks (x: int) returns (y: int)
var c: en1 clock; d: en2 clock; b1, b2, b3, z: int; c1, c2: bool
let
c1 = (x >= 0);
d = if c1 then Up else Down;
c2 = (x = 0) when Up(d);
c = if c2 then Off else On;
b2 = 2 when Off(c);
b1 = 1 when On(c);
z = merge c (On -> b1) (Off -> b2);
b3 = 3 when Down(d);
y = merge d (Up -> z) (Down -> b3);
tel
```

` ````
step (x: int) => (y: int) {
var c: en1; d: en2; b1, b2, b3, z: int; c1, c2: bool;
c1 := x >= 0;
//@ clocks_tr1(x, c1)
if (c1) { d := Up } else { d := Down }
//@ clocks_tr2(x, d)
case (d) { Up: c2 := x = 0 }
//@ clocks_tr3(x, d, c2)
case (d) { Up: if (c2) { c := Off } else { c := On } }
//@ clocks_tr4(x, d, c)
case (d) { Up: case (c) { Off: b2 := 2 } }
//@ clocks_tr5(x, d, c, b2)
case (d) { Up: case (c) { On: b1 := 1 } }
//@ clocks_tr6(x, d, c, b1, b2)
case (d) { Up: case (c) { On: z := b1 ; Off: z := b2 } }
//@ clocks_tr7(x, d, z)
case (d) { Down: b3 := 3 }
//@ clocks_tr8(x, d, b3, z)
case (d) { Up: y := z ; Down: y := b3 }
//@ clocks_tr9(x, y)
}
```

` ````
step (x: int) => (y: int) {
var c: en1; d: en2; b1, b2, b3, z: int; c1, c2: bool;
c1 := x >= 0;
//@ clocks_tr1(x, c1)
if (c1) { d := Up } else { d := Down }
//@ clocks_tr2(x, d)
case (d) { Up: c2 := x = 0 }
//@ clocks_tr3(x, d, c2)
case (d) { Up: if (c2) { c := Off } else { c := On } }
//@ clocks_tr4(x, d, c)
case (d) { Up: case (c) { Off: b2 := 2 } }
//@ clocks_tr5(x, d, c, b2)
case (d) { Up: case (c) { On: b1 := 1 } }
//@ clocks_tr6(x, d, c, b1, b2)
case (d) { Up: case (c) { On: z := b1 ; Off: z := b2 } }
//@ clocks_tr7(x, d, z)
case (d) { Down: b3 := 3 }
//@ clocks_tr8(x, d, b3, z)
case (d) { Up: y := z ; Down: y := b3 }
//@ clocks_tr9(x, y)
}
```

` ````
step (x: int) => (y: int) {
var c: en1; d: en2; b1, b2, b3, z: int; c1, c2: bool;
c1 := x >= 0;
//@ clocks_tr1(x, c1)
if (c1) { d := Up } else { d := Down }
//@ clocks_tr2(x, d)
case (d) {
Up:
c2 := x = 0;
if (c2) { c := Off } else { c := On }
case (c) {
On:
b1 := 1;
z := b1;
Off:
b2 := 2;
z := b2;
}
y := z;
Down:
b3 := 3;
y := b3;
}
//@ clocks_tr3(x, d, c2)
//@ clocks_tr4(x, d, c)
//@ clocks_tr5(x, d, c, b2)
//@ clocks_tr6(x, d, c, b1, b2)
//@ clocks_tr7(x, d, z)
//@ clocks_tr8(x, d, b3, z)
//@ clocks_tr9(x, y)
}
```

` ````
step (x: int) => (y: int) {
var c: en1; d: en2; b1, b2, b3, z: int; c1, c2: bool;
c1 := x >= 0;
//@ clocks_tr1(x, c1)
if (c1) { d := Up } else { d := Down }
//@ clocks_tr2(x, d)
case (d) {
Up:
c2 := x = 0;
if (c2) { c := Off } else { c := On }
case (c) {
On:
b1 := 1;
z := b1;
Off:
b2 := 2;
z := b2;
}
y := z;
Down:
b3 := 3;
y := b3;
}
//@ clocks_tr3(x, d, c2)
//@ clocks_tr4(x, d, c)
//@ clocks_tr5(x, d, c, b2)
//@ clocks_tr6(x, d, c, b1, b2)
//@ clocks_tr7(x, d, z)
//@ clocks_tr8(x, d, b3, z)
//@ clocks_tr9(x, y)
}
```

` ````
step (x: int) => (y: int) {
var c: en1; d: en2; z: int; //@ ghost b1, b2, b3: int; c1, c2: bool
//@ c1 := x >= 0
//@ clocks_tr1(x, c1)
if (x >= 0) { d := Up } else { d := Down }
//@ clocks_tr2(x, d)
case (d) {
Up:
//@ c2 := x = 0
if (x = 0) { c := Off } else { c := On }
case (c) {
On:
//@ b1 := 1
z := 1;
Off:
//@ b2 := 2
z := 2;
}
y := z;
Down:
//@ b3 := 3
y := 3;
}
//@ clocks_tr3(x, d, c2)
//@ clocks_tr4(x, d, c)
//@ clocks_tr5(x, d, c, b2)
//@ clocks_tr6(x, d, c, b1, b2)
//@ clocks_tr7(x, d, z)
//@ clocks_tr8(x, d, b3, z)
//@ clocks_tr9(x, y)
}
```

` ````
step (x: int) => (y: int) {
var c: en1; d: en2; z: int; //@ ghost b1, b2, b3: int; c1, c2: bool
//@ c1 := x >= 0
//@ clocks_tr1(x, c1)
if (x >= 0) { d := Up } else { d := Down }
//@ clocks_tr2(x, d)
case (d) {
Up:
//@ c2 := x = 0
if (x = 0) { c := Off } else { c := On }
case (c) {
On:
//@ b1 := 1
z := 1;
Off:
//@ b2 := 2
z := 2;
}
y := z;
Down:
//@ b3 := 3
y := 3;
}
//@ clocks_tr3(x, d, c2)
//@ clocks_tr4(x, d, c)
//@ clocks_tr5(x, d, c, b2)
//@ clocks_tr6(x, d, c, b1, b2)
//@ clocks_tr7(x, d, z)
//@ clocks_tr8(x, d, b3, z)
//@ clocks_tr9(x, y)
}
```

` ````
step (x: int) => (y: int) {
var c: en1; d: en2; //@ ghost b1, b2, b3, z: int; c1, c2: bool
//@ c1 := x >= 0
//@ clocks_tr1(x, c1)
if (x >= 0) { d := Up } else { d := Down }
//@ clocks_tr2(x, d)
case (d) {
Up:
//@ c2 := x = 0
if (x = 0) { c := Off } else { c := On }
case (c) {
On:
//@ b1 := 1
y := 1;
//@ z := y
Off:
//@ b2 := 2
y := 2;
//@ z := y
}
Down:
//@ b3 := 3
y := 3;
}
//@ clocks_tr3(x, d, c2)
//@ clocks_tr4(x, d, c)
//@ clocks_tr5(x, d, c, b2)
//@ clocks_tr6(x, d, c, b1, b2)
//@ clocks_tr7(x, d, z)
//@ clocks_tr8(x, d, b3, z)
//@ clocks_tr9(x, y)
}
```

` ````
step (x: int) => (y: int) {
var c: en1; d: en2; //@ ghost b1, b2, b3, z: int; c1, c2: bool
//@ c1 := x >= 0
//@ clocks_tr1(x, c1)
if (x >= 0) { d := Up } else { d := Down }
//@ clocks_tr2(x, d)
case (d) {
Up:
//@ c2 := x = 0
if (x = 0) { c := Off } else { c := On }
case (c) {
On:
//@ b1 := 1
y := 1;
//@ z := y
Off:
//@ b2 := 2
y := 2;
//@ z := y
}
Down:
//@ b3 := 3
y := 3;
}
//@ clocks_tr3(x, d, c2)
//@ clocks_tr4(x, d, c)
//@ clocks_tr5(x, d, c, b2)
//@ clocks_tr6(x, d, c, b1, b2)
//@ clocks_tr7(x, d, z)
//@ clocks_tr8(x, d, b3, z)
//@ clocks_tr9(x, y)
}
```

` ````
step (x: int) => (y: int) {
//@ ghost c: en1; d: en2; b1, b2, b3, z: int; c1, c2: bool
//@ c1 := x >= 0
//@ clocks_tr1(x, c1)
if (x >= 0) {
//@ d := Up
//@ c2 := x = 0
if (x = 0) {
//@ c := Off
//@ b2 := 2
y := 2;
//@ z := y
} else {
//@ c := On
//@ b1 := 1
y := 1;
//@ z := y
}
} else {
//@ d := Down
//@ b3 := 3
y := 3;
}
//@ clocks_tr2(x, d)
//@ clocks_tr3(x, d, c2)
//@ clocks_tr4(x, d, c)
//@ clocks_tr5(x, d, c, b2)
//@ clocks_tr6(x, d, c, b1, b2)
//@ clocks_tr7(x, d, z)
//@ clocks_tr8(x, d, b3, z)
//@ clocks_tr9(x, y)
}
```

- Extension of a Lustre compiler to support Translation Validation
- High automatic verification success rate
- Aggressive validated optimizations

- Functional contracts from Lustre to C
- Floats
- Arrays
- More optimizations