by Timothy Bourke, Jean-Louis Colaço, Bruno Pagano, Cédric Pasteur, and Marc Pouzet.
This page contains source code in support of our CC 2015 submission.
Models are given for Zélus and Scade 6.
This example demonstrates a simple discrete node that increments an internal
counter whenever a tick
input is true and resets it whenever a res
input
is true.
To test the program, we set tick
to false at the second, and then every 6
instants, and res
to true when the counter became 4
at the last
reaction.
open Dump
let node counting(tick, res) = c where
rec reset
init c = 0
and match tick with
| true -> do c = last c + 1 done
| false -> do done
every res
let floatb x = if x then 1.0 else 0.0
let node main () = window("counting", 5.0, t, s) where
(* Run counting *)
rec c = counting(tick, false fby (c = 4))
and tick = let rec x = (0 fby x + 1) mod 6 in x <> 2
(* Plot the results *)
and t = 0. fby (t +. 1.)
and s = scope2(0., 10., ("c", points true, float c),
("tick", points true, floatb tick))
The program text above differs from that given in the paper: it is written in Zélus, not the kernel language. The program also contains additional commands to produce the plot shown below.
This program compiles with the version of Zélus available from this site. We simulate the true (1.0)/false(0.0) tick input (the red dots) and reset the counter (the green dots) when it reaches 5.
The same program expressed in the graphical syntax of Scade is shown below. A single state automaton with a self-loop is used to implement the reset.
Compiling this program with the standard version of KCG produces, amongst others, the two files included below.
#ifndef _counting_H_ #define _counting_H_ #include "kcg_types.h" /* ======================== input structure ====================== */ typedef struct { kcg_bool /* counting::tick */ tick; kcg_bool /* counting::res */ res; } inC_counting; /* ======================== context type ========================= */ typedef struct { /* --------------------------- outputs --------------------------- */ kcg_int /* counting::o */ o; /* ----------------------- no local probes ----------------------- */ /* -------------------- initialization variables ------------------ */ kcg_bool init; /* ----------------------- no local memory ----------------------- */ /* -------------------- no sub nodes' contexts -------------------- */ /* ----------------- no clocks of observable data ------------------ */ } outC_counting; /* =========== node initialization and cycle functions =========== */ /* counting */ extern void counting(inC_counting *inC, outC_counting *outC); extern void counting_reset(outC_counting *outC); #endif /* _counting_H_ */
This header file defines the state record for the counting
node. There is
a state variable of type kcg_bool
that records whether or not the node has
been initialized, and a variable of type kcg_int
to store the counter
value.
#include "kcg_consts.h" #include "kcg_sensors.h" #include "counting.h" void counting_reset(outC_counting *outC) { outC->init = kcg_true; } /* counting */ void counting(inC_counting *inC, outC_counting *outC) { /* counting::SM1::S1::c */ kcg_int last_c_SM1_S1; if (inC->res) { outC->init = kcg_true; } if (outC->init) { last_c_SM1_S1 = 0; } else { last_c_SM1_S1 = outC->o; } if (inC->tick) { outC->o = last_c_SM1_S1 + 1; } else { outC->o = last_c_SM1_S1; } outC->init = kcg_false; }
The counting.c
source declares two functions: one to reset the node, and
another to calculate its behaviour at a discrete step.
This example demonstrates the hello world of hybrid modelers: a bouncing ball that loses energy at each impact.
open Dump
let g = 9.81
let hybrid bouncing(y0, y'0) = y where
rec der y = y' init y0
and der y' = -. g init y'0 reset z -> (-0.8 *. last y')
and z = up(-. last y)
let node plot (t, y) =
let rec s = scope (-0.5, 10.0, ("y", linear, y)) in
window ("bouncing", 50.0, t, s)
let hybrid main () = () where
rec y = bouncing(9.0, 0.0)
and der t = 1.0 init 0.0
and _ = present (period (0.04)) -> plot(t, y)
The Zélus source code above has three nodes: bouncing
, the model from the
paper, plot
, a discrete node for generating the plot shown below, and
main
, for connecting everything together.
A collision of the ball with the ground is detected using the up
operator,
which watches for rising zero-crossings. The resulting event z
triggers a
reset of the y'
continuous state variable. The results are shown in the
graph below.
The bouncing
node is expressed in the textual syntax of Scade below.
const g:real = 9.81; hybrid bouncing(y0,y_v0:real) returns (y:real last = y0) var y_v:real last = y_v0; let der y = y_v; activate if down y then y_v = - 0.8 * last 'y_v; else der y_v = - g; returns ..; tel
In this version, the continuous variable y_v
is defined over two branches
of the activate
operator. The first one gives its value at instants when a
falling zero-crossing is detected via down y
. The second defines its
derivative at other instants.
Compiling this program with a prototype version of KCG produces, amongst others, the two files included below.
#ifndef _bouncing_H_ #define _bouncing_H_ #include "kcg_types.h" /* ======================== input structure ====================== */ typedef struct { kcg_real /* bouncing::y0 */ y0; kcg_real /* bouncing::y_v0 */ y_v0; } inC_bouncing; /* ===================== no output structure ====================== */ /* ======================== context type ========================= */ typedef struct { /* --------------------------- outputs --------------------------- */ kcg_real /* bouncing::y */ y; /* ----------------------- no local probes ----------------------- */ /* -------------------- initialization variables ------------------ */ kcg_bool init; /* ----------------------- no local memory ----------------------- */ /* -------------------- no sub nodes' contexts -------------------- */ /* ----------------- no clocks of observable data ------------------ */ kcg_cstate /* bouncing::y_v */ y_v; kcg_cstate /* bouncing */ der_out; kcg_zc zc_cb_clock; kcg_real horizon; } outC_bouncing; /* =========== node initialization and cycle functions =========== */ /* bouncing */ extern void bouncing(inC_bouncing *inC, outC_bouncing *outC); extern void bouncing_cont(inC_bouncing *inC, outC_bouncing *outC); extern kcg_real bouncing_horizon(outC_bouncing *outC); #ifndef KCG_NO_EXTERN_CALL_TO_RESET extern void bouncing_reset(outC_bouncing *outC); #endif /* KCG_NO_EXTERN_CALL_TO_RESET */ #ifndef KCG_USER_DEFINED_INIT extern void bouncing_init(outC_bouncing *outC); #endif /* KCG_USER_DEFINED_INIT */ #endif /* _bouncing_H_ */
This header file defines the state record for the bouncing
node. There are
two continous variables of type kcg_cstate
, one zero-crossing expression
of type kcg_zc
and a discrete state variable of type kcg_bool
.
#include "kcg_consts.h" #include "kcg_sensors.h" #include "bouncing.h" #ifndef KCG_USER_DEFINED_INIT void bouncing_init(outC_bouncing *outC) { outC->init = kcg_true; outC->y = 0.0; } #endif /* KCG_USER_DEFINED_INIT */ #ifndef KCG_NO_EXTERN_CALL_TO_RESET void bouncing_reset(outC_bouncing *outC) { outC->init = kcg_true; } #endif /* KCG_NO_EXTERN_CALL_TO_RESET */ /* bouncing */ void bouncing(inC_bouncing *inC, outC_bouncing *outC) { /* bouncing::y_v */ kcg_real last_y_v; /* bouncing::?? */ kcg_bool cb_clock; /* last_init_ck_y */ if (outC->init) { outC->init = kcg_false; last_y_v = inC->y_v0; outC->der_out.val = inC->y0; } else { last_y_v = outC->y_v.last; outC->der_out.val = outC->der_out.last; } outC->y = outC->der_out.val; outC->zc_cb_clock.out = outC->y; cb_clock = outC->zc_cb_clock.up | kcg_down( outC->zc_cb_clock.last, outC->zc_cb_clock.out); /* ck_anon_activ */ if (cb_clock) { outC->y_v.val = - 0.8 * last_y_v; } else { outC->y_v.val = last_y_v; } outC->horizon = kcg_infinity; } void bouncing_cont(inC_bouncing *inC, outC_bouncing *outC) { outC->y = outC->der_out.last; outC->zc_cb_clock.out = outC->y; outC->y_v.der = - g; outC->der_out.der = outC->y_v.last; } kcg_real bouncing_horizon(outC_bouncing *outC) { /* bouncing */ kcg_real horizon_acc; /* bouncing */ kcg_real _1_horizon_acc; horizon_acc = kcg_infinity; horizon_acc = kcg_min(horizon_acc, outC->horizon); outC->horizon = kcg_infinity; return horizon_acc; }
The bouncing.c
source includes separate functions for initializing and
resetting the bouncing
node, for calculating its behaviour at discrete
instants, for calculating its derivatives at continuous ones, and also for
calculating the next horizon.
This model is a reimplementation of the Mathworks Simulink example [Bang-Bang Control Using Temporal Logic]( http://www.mathworks.com/help/simulink/examples/bang-bang-control-using-temporal-logic.html).
The main differences with the original model are:
Zélus does not have fixed-point data types, so we have to manually track bias and slope for integers representing rational values.
We use int for the integer values rather than int8.
The top level of this example comprises three nodes:
The controller is discrete. It takes two inputs:
reference temperature
This value is a constant 20°C, but it is encoded as a fixed-point integer so that it can be compared directly with the digital temperature value from the environment model. The reference temperature has a value between 0 (-15°C) and 255 (84.609375°C), i.e., a resolution of 0.390625 per bit (0.390625 = 5 / 256 / 0.05).
feedback temperature
A digital temperature measurement.
And provides two outputs:
led: the colour of a light emitting diode on the outside of the controller:
0
= off
,1
= red
(not heating),2
= green
(heating).boiler: a signal that switches the boiler on (1
) or off (0
).
The main part of the controller is an automaton with two top-level states:
Off
: The boiler is off. The LED is flashed red at 0.1 Hz (5 secs off, 5
secs red).
On
: The boiler is on. The LED is flashed red at 0.5 Hz (1 sec off, 1 sec
green).
The controller always remains in the Off
state for at least 40 seconds,
after which it will switch to the On
state if the temperature is less than
the reference temperature.
The controller may not remain in the On
state for more than 20 seconds. It
will switch to the Off
state if the temperature becomes greater than the
reference temperature.
The on state contains an internal automaton that stays in a High
state from
t = 0
until the very first time that the measured temperature exceeds the
reference temperature (this is ensured by entry-by-history from Off
). The
reason for this additional complication in the original Stateflow controller
is not clear; perhaps the intent was to heat at a faster rate the first time
the system is switched on? In our model, the effect is to delay an exit from
the On
state by one reaction the first time the reference temperature is
attained.
Boiler is a hybrid model of the boiler temperature and a digital thermometer.
The boiler temperature is modeled by a single integrator with an initial value of 15°C. This value (cools) at a rate of -0.1 / 25 when the boiler is off. It changes (heats) at a rate of 1.0 / 25 when the boiler is on.
The digital thermometer is modelled in some detail. Effectively, it takes a floating point temperature value in degrees centigrade and returns an integer between 0 and 255 representing that value (see the discussion above for the reference temperature).
The sensor itself has a bias of 0.75 and and a precision of 0.05, i.e., the
output voltage V is a function of the temperature T: V = 0.05 * T + 0.75
. An
analog-to-digital converter (ADC) converts this voltage into an integer. By
scaling, quantization, and limiting.
Scope is a discrete node. It is triggered every sample_period
to plot the
LED output, the boiler command, and the actual temperature against time.
Note that, even though all of these signals are continuous, they are plotted at discrete instants (as plotting is a side-effect) and the graph is thus (linearly) interpolated.
The simulation output shows a staircased increase in temperature from 15°C
at t = 0
to the 20°C just before t = 500
. The initial rising edges have a
slope of 1.0/25 (the heating rate) and a duration of 20 seconds (the maximum
amount of time in the On
state). The initial falling edges have a slope of
0.1/25 (the cooling rate) and a duration of 40 seconds (the minimum amount
of time in the Off
state). After reaching the reference temperature, the
controller switches on and off to oscillate around the set-point.
The LED will flash green (2
) during periods of heating, and red (1
) during
periods of cooling, i.e., when not heating.
(*
Version of the Mathworks Simulink example:
Bang-Bang Control Using Temporal Logic
*)
(* ** library functions ** *)
let hybrid integrator (i, u) = y where
der y = u init i
let node round x = floor (x +. 0.5)
(* ** model of analog-to-digital convertor ** *)
let node quantize (q, u) = q *. round(u /. q)
(* limiting without zero-crossings *)
let node limit (min, max, x) =
if x >= max then max
else if x <= min then min
else x
let node adc (v) = pcm where
rec vs = v *. (256.0 /. 5.0)
and pcm = quantize (1.0, limit (0.0, 255.0, vs))
(* ** model of digital thermometer ** *)
let node digital_thermometer (temp) = int_of_float(adv) where
rec voltage = 0.05 *. temp +. 0.75
and adv = adc (voltage)
(* signed fixed-point int from scale and bias *)
let discrete fixdt (s, b, v) = int_of_float ((v -. b) /. s)
(* ** model of boiler plant with an exponential ** *)
let hybrid boiler_exponential(k1, k2, is_on) = actual_temp where
rec der actual_temp =
(* two modes. [is_on] is a boolean and will only change *)
(* at a zero-crossing instant. *)
if is_on then k1 -. k2 *. actual_temp
else -. k2 *. actual_temp
init 15.0
(* the one below is the Simulink version with an approximation by a *)
(* linear function *)
let hybrid boiler(is_on) = actual_temp where
rec der actual_temp =
(* two modes. [is_on] is a boolean and will only change *)
(* at a zero-crossing instant. *)
(if is_on then 1.0 else -0.1) /. 25.0
init 15.0
(* ** Bang-Bang Controller ** *)
let off = 0
let red = 1
let green = 2
let b_off = false
let b_on = true
let node after (x) =
let rec c = x fby max (0, c - 1) in
c = 0
let node at (x) =
let rec c = 0 fby ((c + 1) mod x) in
false -> (c = 0)
let node flash_led (color, delay) = led where
automaton
| Off -> do led = off until (after delay) then On
| On -> do led = color until (after delay) then Off
let node controller (ref, temp) = (led, boiler) where
rec cold = temp <= ref
and automaton
| Off ->
do boiler = b_off
and led = flash_led (red, 5)
until (after 40) & cold then On
| On ->
do boiler = b_on
and led = flash_led (green, 1)
until (not cold) then Off
else (at 20) then Off
(* ** main ** *)
let reference = fixdt (5.0 /. 256.0 /. 0.05, -. 0.75 /. 0.05, 20.0)
let hybrid model () = (led, on_off, actual_temp) where
rec trigger = period (1.0)
and (led, on_off) =
present trigger -> controller(reference, last digital_temp)
init (red, false)
and actual_temp = boiler(on_off)
and digital_temp =
present trigger -> digital_thermometer (actual_temp)
init 0
open Scope (* Dump *)
let sample_period = 1.0
let node bool_to_float(x) = if x then 1.0 else 0.0
let node plot (led, boiler, temp) =
let s1 =
scope (0.0, 2.0, ("led (0=OFF, 1=RED, 2=GREEN)", points true, float(led))) in
let s2 =
scope (0.0, 1.0, ("boiler (0=OFF, 1=ON)", points true, bool_to_float(boiler))) in
let s3 =
scope (11.0, 25.0, ("temperature (degC)", linear, temp)) in
let rec t = 0.0 fby t +. sample_period in
window3 ("bangbang", 600.0, t, s1, s2, s3)
let hybrid main () =
let (led, on_off, actual_temp) = model () in
let trigger = period (0.5) in
present trigger -> plot (led, on_off, actual_temp) else ()
The Zélus program is readily transcribed into the extended (with ODEs) textual syntax of Scade:
-- Version of the Mathworks Simulink example: -- Bang-Bang Control Using Temporal Logic -- library functions function max (x1,x2:'a) returns (o:'a) where 'a numeric o = if x1 > x2 then x1 else x2; hybrid integrator (i, u:real) returns (y:real last=i) der y = u; function round (x:real) returns (o:real) -- o = floor (x +. 0.5); o = real (int (x+0.5)); function quantize (q, u:real) returns (o:real) o = q * round(u / q); -- limiting without zero-crossings function limit (min, max, x:real) returns (o:real) o = if x >= max then max else if x <= min then min else x; -- model of analog-to-digital convertor function adc (v:real) returns (pcm:real) var vs:real; let vs = v * (256.0 / 5.0); pcm = quantize (1.0, limit (0.0, 255.0, vs)); tel -- model of digital thermometer function digital_thermometer (temp:real) returns (adv:int) var voltage:real; let voltage = 0.05 * temp + 0.75; adv = int (adc (voltage)); tel -- signed fixed-point int from scale and bias function fixdt (s, b, v:real) returns (o:int) o = int ((v - b) / s); -- model of boiler plant with an exponential hybrid boiler_exponential(k1, k2:real; is_on:bool) returns (actual_temp:real last=15.0) let der actual_temp = -- two modes. [is_on] is a boolean and will only change -- at a zero-crossing instant. if is_on then k1 - k2 * actual_temp else - k2 * actual_temp; tel -- the one below is the Simulink version with an approximation by a -- linear function hybrid boiler(is_on:bool) returns (actual_temp:real last=15.0) der actual_temp = -- two modes. [is_on] is a boolean and will only change *) -- at a zero-crossing instant. *) (if is_on then 1.0 else -0.1) / 25.0; -- Bang-Bang Controller -- const off:int = 0; const red:int = 1; const green:int = 2; const b_off:bool = false; const b_on:bool = true; node after (x:int) returns (res:bool) var c:int; let c = fby(max (0, c - 1); 1; x); res = (c = 0); tel node at(x:int) returns (res:bool) var c:int; let c = fby ((c + 1) mod x; 1; 0); res = false -> (c = 0); tel node flash_led (color:int; delay:int) returns (led:int) let automaton initial state Off led = off; until if after(delay) restart On; state On led = color; until if after(delay) restart Off; returns ..; tel node controller (ref, temp:int) returns (led:int; boiler:bool) var cold:bool; let cold = temp <= ref; automaton initial state Off let boiler = b_off; led = flash_led (red, 5); tel until if after(40) and cold restart On; state On let boiler = b_on; led = flash_led (green, 1); tel until if not cold restart Off; if at (20) restart Off; returns ..; tel -- main hybrid reference() returns (o:int) o = fixdt (5.0 / 256.0 / 0.05, - 0.75 / 0.05, 20.0); hybrid bangbang () returns (led:int last=red; on_off:bool last=false; actual_temp:real) var trigger:zero; digital_temp:int last=0; ref:int; let trigger = period 1.0 .(1.0); ref = reference(); actual_temp = boiler(on_off); activate if trigger then let led, on_off = controller(ref, last 'digital_temp); digital_temp = digital_thermometer(actual_temp); tel else let tel returns ..; tel
This program is compiled with the prototype KCG compiler to give (amongst other files—one for each node):
#ifndef _bangbang_H_ #define _bangbang_H_ #include "kcg_types.h" #include "digital_thermometer.h" #include "boiler.h" #include "controller.h" #include "reference.h" #include "period.h" /* ===================== no input structure ====================== */ /* ===================== no output structure ====================== */ /* ======================== context type ========================= */ typedef struct { /* --------------------------- outputs --------------------------- */ kcg_int /* bangbang::led */ led; kcg_bool /* bangbang::on_off */ on_off; kcg_real /* bangbang::actual_temp */ actual_temp; /* ----------------------- no local probes ----------------------- */ /* -------------------- initialization variables ------------------ */ kcg_bool init; /* ----------------------- local memories ------------------------- */ kcg_int /* bangbang::digital_temp */ digital_temp; /* --------------------- sub nodes' contexts --------------------- */ outC_boiler /* boiler */ Context_boiler; outC_controller /* controller */ Context_controller; outC_reference /* reference */ Context_reference; outC_period Context; /* ----------------- no clocks of observable data ------------------ */ kcg_real horizon; } outC_bangbang; /* =========== node initialization and cycle functions =========== */ /* bangbang */ extern void bangbang(outC_bangbang *outC); extern void bangbang_cont(outC_bangbang *outC); extern kcg_real bangbang_horizon(outC_bangbang *outC); #ifndef KCG_NO_EXTERN_CALL_TO_RESET extern void bangbang_reset(outC_bangbang *outC); #endif /* KCG_NO_EXTERN_CALL_TO_RESET */ #ifndef KCG_USER_DEFINED_INIT extern void bangbang_init(outC_bangbang *outC); #endif /* KCG_USER_DEFINED_INIT */ #endif /* _bangbang_H_ */
#include "kcg_consts.h" #include "kcg_sensors.h" #include "bangbang.h" #ifndef KCG_USER_DEFINED_INIT void bangbang_init(outC_bangbang *outC) { outC->on_off = kcg_true; outC->init = kcg_true; outC->digital_temp = 0; outC->actual_temp = 0.0; outC->led = 0; /* boiler */ boiler_init(&outC->Context_boiler); /* controller */ controller_init(&outC->Context_controller); /* reference */ reference_init(&outC->Context_reference); period_init(&outC->Context); } #endif /* KCG_USER_DEFINED_INIT */ #ifndef KCG_NO_EXTERN_CALL_TO_RESET void bangbang_reset(outC_bangbang *outC) { outC->init = kcg_true; /* boiler */ boiler_reset(&outC->Context_boiler); /* controller */ controller_reset(&outC->Context_controller); /* reference */ reference_reset(&outC->Context_reference); period_reset(&outC->Context); } #endif /* KCG_NO_EXTERN_CALL_TO_RESET */ /* bangbang */ void bangbang(outC_bangbang *outC) { /* bangbang::led */ kcg_int led; /* bangbang::digital_temp */ kcg_int last_digital_temp; /* last_init_ck_digital_temp */ if (outC->init) { last_digital_temp = 0; } else { last_digital_temp = outC->digital_temp; } period(1.0, 1.0, &outC->Context); /* ck_trigger */ if (outC->Context.period_evt) { /* reference */ reference(&outC->Context_reference); /* controller */ controller( outC->Context_reference.o, last_digital_temp, &outC->Context_controller); led = outC->Context_controller.led; outC->on_off = outC->Context_controller.boiler; } else /* last_init_ck_on_off */ if (outC->init) { outC->on_off = kcg_false; } /* boiler */ boiler(outC->on_off, &outC->Context_boiler); outC->actual_temp = outC->Context_boiler.actual_temp; /* ck_trigger */ if (outC->Context.period_evt) { outC->digital_temp = /* digital_thermometer */ digital_thermometer(outC->actual_temp); outC->led = led; } else { outC->digital_temp = last_digital_temp; /* last_init_ck_led */ if (outC->init) { outC->led = red; } } outC->init = kcg_false; outC->horizon = kcg_infinity; } void bangbang_cont(outC_bangbang *outC) { period_cont(1.0, 1.0, &outC->Context); /* boiler */ boiler_cont(outC->on_off, &outC->Context_boiler); outC->actual_temp = outC->Context_boiler.actual_temp; } kcg_real bangbang_horizon(outC_bangbang *outC) { /* bangbang */ kcg_real horizon_acc; /* bangbang */ kcg_real _1_horizon_acc; horizon_acc = kcg_infinity; horizon_acc = kcg_min(horizon_acc, outC->horizon); outC->horizon = kcg_infinity; _1_horizon_acc = period_horizon(&outC->Context); horizon_acc = kcg_min(horizon_acc, _1_horizon_acc); _1_horizon_acc = /* reference */ reference_horizon(&outC->Context_reference); horizon_acc = kcg_min(horizon_acc, _1_horizon_acc); _1_horizon_acc = /* boiler */ boiler_horizon(&outC->Context_boiler); horizon_acc = kcg_min(horizon_acc, _1_horizon_acc); return horizon_acc; }
#ifndef _boiler_H_ #define _boiler_H_ #include "kcg_types.h" /* ===================== no input structure ====================== */ /* ===================== no output structure ====================== */ /* ======================== context type ========================= */ typedef struct { /* --------------------------- outputs --------------------------- */ kcg_real /* boiler::actual_temp */ actual_temp; /* ----------------------- no local probes ----------------------- */ /* -------------------- initialization variables ------------------ */ kcg_bool init; /* ----------------------- no local memory ----------------------- */ /* -------------------- no sub nodes' contexts -------------------- */ /* ----------------- no clocks of observable data ------------------ */ kcg_cstate /* boiler */ der_out; kcg_real horizon; } outC_boiler; /* =========== node initialization and cycle functions =========== */ /* boiler */ extern void boiler(/* boiler::is_on */ kcg_bool is_on, outC_boiler *outC); extern void boiler_cont(/* boiler::is_on */ kcg_bool is_on, outC_boiler *outC); extern kcg_real boiler_horizon(outC_boiler *outC); #ifndef KCG_NO_EXTERN_CALL_TO_RESET extern void boiler_reset(outC_boiler *outC); #endif /* KCG_NO_EXTERN_CALL_TO_RESET */ #ifndef KCG_USER_DEFINED_INIT extern void boiler_init(outC_boiler *outC); #endif /* KCG_USER_DEFINED_INIT */ #endif /* _boiler_H_ */
#include "kcg_consts.h" #include "kcg_sensors.h" #include "boiler.h" #ifndef KCG_USER_DEFINED_INIT void boiler_init(outC_boiler *outC) { outC->init = kcg_true; outC->actual_temp = 0.0; } #endif /* KCG_USER_DEFINED_INIT */ #ifndef KCG_NO_EXTERN_CALL_TO_RESET void boiler_reset(outC_boiler *outC) { outC->init = kcg_true; } #endif /* KCG_NO_EXTERN_CALL_TO_RESET */ /* boiler */ void boiler(/* boiler::is_on */ kcg_bool is_on, outC_boiler *outC) { /* last_init_ck_actual_temp */ if (outC->init) { outC->init = kcg_false; outC->der_out.val = 15.0; } else { outC->der_out.val = outC->der_out.last; } outC->actual_temp = outC->der_out.val; outC->horizon = kcg_infinity; } void boiler_cont(/* boiler::is_on */ kcg_bool is_on, outC_boiler *outC) { outC->actual_temp = outC->der_out.last; if (is_on) { outC->der_out.der = 1.0 / 25.0; } else { outC->der_out.der = - 0.1 / 25.0; } } kcg_real boiler_horizon(outC_boiler *outC) { /* boiler */ kcg_real horizon_acc; /* boiler */ kcg_real _1_horizon_acc; horizon_acc = kcg_infinity; horizon_acc = kcg_min(horizon_acc, outC->horizon); outC->horizon = kcg_infinity; return horizon_acc; }
#ifndef _controller_H_ #define _controller_H_ #include "kcg_types.h" #include "after.h" #include "at.h" #include "flash_led.h" /* ===================== no input structure ====================== */ /* ===================== no output structure ====================== */ /* ======================== context type ========================= */ typedef struct { /* --------------------------- outputs --------------------------- */ kcg_int /* controller::led */ led; kcg_bool /* controller::boiler */ boiler; /* ----------------------- no local probes ----------------------- */ /* -------------------- initialization variables ------------------ */ kcg_bool init; /* ----------------------- local memories ------------------------- */ SSM_ST /* controller::?? */ state_nxt; kcg_bool /* controller::?? */ reset_nxt; /* --------------------- sub nodes' contexts --------------------- */ outC_flash_led /* flash_led */ _1_Context_flash_led; outC_after /* after */ Context_after; outC_flash_led /* flash_led */ Context_flash_led; outC_at /* at */ Context_at; /* ----------------- no clocks of observable data ------------------ */ kcg_real horizon; } outC_controller; /* =========== node initialization and cycle functions =========== */ /* controller */ extern void controller( /* controller::ref */ kcg_int ref, /* controller::temp */ kcg_int temp, outC_controller *outC); #ifndef KCG_NO_EXTERN_CALL_TO_RESET extern void controller_reset(outC_controller *outC); #endif /* KCG_NO_EXTERN_CALL_TO_RESET */ #ifndef KCG_USER_DEFINED_INIT extern void controller_init(outC_controller *outC); #endif /* KCG_USER_DEFINED_INIT */ #endif /* _controller_H_ */
#include "kcg_consts.h" #include "kcg_sensors.h" #include "controller.h" #ifndef KCG_USER_DEFINED_INIT void controller_init(outC_controller *outC) { outC->boiler = kcg_true; outC->reset_nxt = kcg_true; outC->init = kcg_true; outC->state_nxt = SSM_st_Off; outC->led = 0; /* flash_led */ flash_led_init(&outC->_1_Context_flash_led); /* after */ after_init(&outC->Context_after); /* flash_led */ flash_led_init(&outC->Context_flash_led); /* at */ at_init(&outC->Context_at); } #endif /* KCG_USER_DEFINED_INIT */ #ifndef KCG_NO_EXTERN_CALL_TO_RESET void controller_reset(outC_controller *outC) { outC->init = kcg_true; /* flash_led */ flash_led_reset(&outC->_1_Context_flash_led); /* after */ after_reset(&outC->Context_after); /* flash_led */ flash_led_reset(&outC->Context_flash_led); /* at */ at_reset(&outC->Context_at); } #endif /* KCG_NO_EXTERN_CALL_TO_RESET */ /* controller */ void controller( /* controller::ref */ kcg_int ref, /* controller::temp */ kcg_int temp, outC_controller *outC) { /* controller::??::Off */ kcg_bool br_1_guard_Off; /* controller::??::On */ kcg_bool br_1_guard_On; /* controller::?? */ SSM_ST state_act; /* controller::?? */ kcg_bool reset_sel; /* controller::cold */ kcg_bool cold; /* init_anon_sm */ if (outC->init) { outC->init = kcg_false; reset_sel = kcg_false; state_act = SSM_st_Off; } else { state_act = outC->state_nxt; reset_sel = outC->reset_nxt; } cold = temp <= ref; /* act_anon_sm */ switch (state_act) { case SSM_st_On : if (reset_sel) { /* at */ at_reset(&outC->Context_at); /* flash_led */ flash_led_reset(&outC->Context_flash_led); } /* at */ at(20, &outC->Context_at); br_1_guard_On = !cold; /* flash_led */ flash_led(green, 1, &outC->Context_flash_led); if (br_1_guard_On) { outC->reset_nxt = kcg_true; outC->state_nxt = SSM_st_Off; } else { outC->reset_nxt = outC->Context_at.res; if (outC->Context_at.res) { outC->state_nxt = SSM_st_Off; } else { outC->state_nxt = SSM_st_On; } } outC->boiler = b_on; outC->led = outC->Context_flash_led.led; break; case SSM_st_Off : if (reset_sel) { /* after */ after_reset(&outC->Context_after); /* flash_led */ flash_led_reset(&outC->_1_Context_flash_led); } /* after */ after(40, &outC->Context_after); br_1_guard_Off = outC->Context_after.res & cold; /* flash_led */ flash_led(red, 5, &outC->_1_Context_flash_led); outC->reset_nxt = br_1_guard_Off; if (br_1_guard_Off) { outC->state_nxt = SSM_st_On; } else { outC->state_nxt = SSM_st_Off; } outC->boiler = b_off; outC->led = outC->_1_Context_flash_led.led; break; } outC->horizon = kcg_infinity; }
#include "stddef.h" #include "bangbang.h" #define MODEL_IDENTIFIER bangbang #define SCADE_OUT_CTX outC_bangbang #define INIT_FUN bangbang_init #define RESET_FUN bangbang_reset #define STEP_FUN bangbang #define CONT_FUN bangbang_cont #define HORIZON_FUN bangbang_horizon #include "fmu_wrapper.h" static const size_t vars_offsets[3] = { SCADE_CTX_OFFSET + offsetof (outC_bangbang, led), SCADE_CTX_OFFSET + offsetof (outC_bangbang, on_off), SCADE_CTX_OFFSET + offsetof (outC_bangbang, actual_temp) }; #define NB_CSTATE 1 static const size_t cstates_offsets[1] = { SCADE_CTX_OFFSET + offsetof (outC_bangbang, Context_boiler.der_out) }; #define NB_ZC 0 #include "fmu_wrapper.c"
This example is based on example 6.8 in Edward A. Lee and Pravin Varaiya, Structure and Interpretation of Signals and Systems, Second Edition, and the Ptolemy II model by Jie Liu, Haiyang Zheng, and Edward A. Lee.
The model comprises two sticky round masses, each on the end of a spring. The other ends of the springs are tied to opposing walls. After the springs are compressed (or extended) and released the masses oscillate back and forth, and may collide. After a collision, the masses remain stuck together until the pulling forces from the springs are greater than a stickiness value (which decreases exponentially after a collision).
We program this model in Zélus using automata:
(* ** Parameters ** *)
(* neutral positions of the two masses *)
let p1 = 1.25
let p2 = 1.75
(* initial positions of the two masses: y1_i < y2_i *)
let x1_i = 0.0
let x2_i = 3.0
(* spring constants *)
(* let k1 = 4.0 (* exhibits problem *) *)
let k1 = 1.0
let k2 = 2.5 (* 2.0 *)
(* masses *)
let m1 = 1.5
let m2 = 1.0
(* stickyness *)
let stickiness_max = 10.0
let tau = 0.5
(* ** Model ** *)
let hybrid sticky () =
((x1, v1), (x2, v2), pull, stickiness_out, total) where
rec der x1 = v1 init x1_i
and der x2 = v2 init x2_i
and init v1 = 0.0
and init v2 = 0.0
and total = 0.5 *. m1 *. v1 *. v1 +. 0.5 *. m2 *. v2 *. v2 +.
0.5 *. k1 *. (x1 -. p1) *. (x1 -. p1) +.
0.5 *. k2 *. (x2 -. p2) *. (x2 -. p2)
and automaton
| Apart ->
local mediant in
do der v1 = k1 *. (p1 -. x1) /. m1
and der v2 = k2 *. (p2 -. x2) /. m2
and mediant = (v1 *. m1 +. v2 *. m2) /. (m1 +. m2)
and pull = 0.0
and stickiness_out = 0.0
until up (x1 -. x2) then
do next v1 = mediant
and next v2 = mediant in Together
| Together ->
local y_dot_dot, stickiness in
do pull =
abs_float (-. last x1 *. (k1 +. k2) +. (k2 *. p2 -. k1 *. p1))
and y_dot_dot =
(k1 *. p1 +. k2 *. p2 -. (k1 +. k2) *. last x1) /. (m1 +. m2)
and der v1 = y_dot_dot
and der v2 = y_dot_dot
and der stickiness = -. stickiness /. tau init stickiness_max
and stickiness_out = stickiness
until up (pull -. stickiness) then Apart
(* ** plotting ** *)
open Scope
let node plot (t, (y1, y1_dot), (y2, y2_dot), pull_force, stickiness, total) =
let s1 = scope2 (0.0, 3.0, ("p1", linear, y1), ("p2", linear, y2)) in
let s2 = scope2 (-1.5, 1.5, ("v1", linear, y1_dot), ("v2", linear, y2_dot)) in
let s3 = scope2 (0.0, stickiness_max, ("Pulling force", linear, pull_force),
("Stickiness", linear, stickiness)) in
let s4 = scope (0.0, 3.0, ("Total Energy", linear, total)) in
window4 ("sticky springs", 30.0, t, s1, s2, s3, s4)
(* ** main ** *)
let hybrid main () =
let der t = 1.0 init 0.0 in
let ((y1, y1_dot), (y2, y2_dot), pull_force, stickiness, total) = sticky () in
present
(period (0.10)) ->
plot (t, (y1, y1_dot), (y2, y2_dot), pull_force, stickiness, total);
()
We program this model in Scade (extended with ODEs) using automata:
-- Parameters -- -- neutral positions of the two masses const p1:real = 1.25; const p2:real = 1.75; -- initial positions of the two masses: y1_i < y2_i const x1_i:real = 0.0; const x2_i:real = 3.0; -- spring constants const k1:real = 1.0; const k2:real = 2.5; -- masses const m1:real = 1.5; const m2:real = 1.0; -- stickyness const stickiness_max:real = 10.0; const tau:real = 0.5; function abs_float(i:real) returns (o:real) o = if i < 0.0 then -i else i; hybrid stickysprings () returns(x1:real last=x1_i; v1:real last = 0.0; x2:real last=x2_i; v2:real last=0.0; pull, stickiness_out, total:real) let der x1 = v1; der x2 = v2; total = 0.5 * m1 * v1 * v1 + 0.5 * m2 * v2 * v2 + 0.5 * k1 * (x1 - p1) * (x1 - p1) + 0.5 * k2 * (x2 - p2) * (x2 - p2); automaton initial state Apart var mediant:real last=0.0; let der v1 = k1 * (p1 - x1) / m1; der v2 = k2 * (p2 - x2) / m2; mediant = (v1 * m1 + v2 * m2) / (m1 + m2); pull = 0.0; stickiness_out = 0.0; tel until if up (x1 - x2) do let v1 = last 'mediant; v2 = last 'mediant; tel restart Together; state Together var y_dot_dot:real; stickiness:real last = stickiness_max; let pull = abs_float (- last 'x1 * (k1 + k2) + (k2 * p2 - k1 * p1)); y_dot_dot = (k1 * p1 + k2 * p2 - (k1 + k2) * last 'x1) / (m1 + m2); der v1 = y_dot_dot; der v2 = y_dot_dot; der stickiness = - stickiness / tau; stickiness_out = stickiness; tel until if up (pull - stickiness) restart Apart; returns ..; tel
Compilation with the prototype KCG compiler gives, amongst others, these files:
#ifndef _stickysprings_H_ #define _stickysprings_H_ #include "kcg_types.h" #include "abs_float.h" /* ===================== no input structure ====================== */ /* ===================== no output structure ====================== */ /* ======================== context type ========================= */ typedef struct { /* --------------------------- outputs --------------------------- */ kcg_real /* stickysprings::x1 */ x1; kcg_real /* stickysprings::v1 */ v1; kcg_real /* stickysprings::x2 */ x2; kcg_real /* stickysprings::v2 */ v2; kcg_real /* stickysprings::pull */ pull; kcg_real /* stickysprings::stickiness_out */ stickiness_out; kcg_real /* stickysprings::total */ total; /* ----------------------- no local probes ----------------------- */ /* -------------------- initialization variables ------------------ */ kcg_bool init5; kcg_bool init4; kcg_bool init; /* ----------------------- local memories ------------------------- */ kcg_real /* stickysprings::??::Apart::mediant */ mediant_Apart; SSM_ST /* stickysprings::?? */ state_nxt; kcg_bool /* stickysprings::?? */ reset_nxt; /* -------------------- no sub nodes' contexts -------------------- */ /* ----------------- no clocks of observable data ------------------ */ kcg_cstate /* stickysprings::??::Together::stickiness */ stickiness_Together; kcg_cstate /* stickysprings */ _3_der_out; kcg_cstate /* stickysprings */ _2_der_out; kcg_cstate /* stickysprings */ _1_der_out; kcg_cstate /* stickysprings */ der_out; kcg_zc zc_br_1_guard_Together; kcg_zc zc_br_1_guard_Apart; kcg_real horizon; } outC_stickysprings; /* =========== node initialization and cycle functions =========== */ /* stickysprings */ extern void stickysprings(outC_stickysprings *outC); extern void stickysprings_cont(outC_stickysprings *outC); extern kcg_real stickysprings_horizon(outC_stickysprings *outC); #ifndef KCG_NO_EXTERN_CALL_TO_RESET extern void stickysprings_reset(outC_stickysprings *outC); #endif /* KCG_NO_EXTERN_CALL_TO_RESET */ #ifndef KCG_USER_DEFINED_INIT extern void stickysprings_init(outC_stickysprings *outC); #endif /* KCG_USER_DEFINED_INIT */ #endif /* _stickysprings_H_ */
#include "kcg_consts.h" #include "kcg_sensors.h" #include "stickysprings.h" #ifndef KCG_USER_DEFINED_INIT void stickysprings_init(outC_stickysprings *outC) { outC->reset_nxt = kcg_true; outC->init5 = kcg_true; outC->init4 = kcg_true; outC->init = kcg_true; outC->state_nxt = SSM_st_Apart; outC->mediant_Apart = 0.0; outC->total = 0.0; outC->stickiness_out = 0.0; outC->pull = 0.0; outC->v2 = 0.0; outC->x2 = 0.0; outC->v1 = 0.0; outC->x1 = 0.0; } #endif /* KCG_USER_DEFINED_INIT */ #ifndef KCG_NO_EXTERN_CALL_TO_RESET void stickysprings_reset(outC_stickysprings *outC) { outC->init5 = kcg_true; outC->init4 = kcg_true; outC->init = kcg_true; } #endif /* KCG_NO_EXTERN_CALL_TO_RESET */ /* stickysprings */ void stickysprings(outC_stickysprings *outC) { /* stickysprings */ kcg_bool tmp; /* stickysprings::??::Apart */ kcg_bool br_1_guard_Apart; /* stickysprings::??::Apart::mediant */ kcg_real last_mediant_Apart; /* stickysprings::??::Together */ kcg_bool br_1_guard_Together; /* stickysprings::v2 */ kcg_real last_v2; /* stickysprings::v1 */ kcg_real last_v1; /* stickysprings::?? */ SSM_ST state_act; /* stickysprings::?? */ kcg_bool reset_sel; /* init_anon_sm */ if (outC->init5) { last_v2 = 0.0; outC->_1_der_out.val = x2_i; last_v1 = 0.0; outC->_3_der_out.val = x1_i; outC->init5 = kcg_false; reset_sel = kcg_false; state_act = SSM_st_Apart; } else { last_v2 = outC->der_out.last; outC->_1_der_out.val = outC->_1_der_out.last; last_v1 = outC->_2_der_out.last; outC->_3_der_out.val = outC->_3_der_out.last; state_act = outC->state_nxt; reset_sel = outC->reset_nxt; } outC->x2 = outC->_1_der_out.val; outC->x1 = outC->_3_der_out.val; /* act_anon_sm */ switch (state_act) { case SSM_st_Together : if (reset_sel) { outC->init4 = kcg_true; } /* last_init_ck_stickiness */ if (outC->init4) { outC->stickiness_Together.val = stickiness_max; } else { outC->stickiness_Together.val = outC->stickiness_Together.last; } outC->pull = /* abs_float */ abs_float(- outC->x1 * (k1 + k2) + (k2 * p2 - k1 * p1)); outC->zc_br_1_guard_Together.out = outC->pull - outC->stickiness_Together.val; br_1_guard_Together = outC->zc_br_1_guard_Together.up | kcg_up( outC->zc_br_1_guard_Together.last, outC->zc_br_1_guard_Together.out); outC->stickiness_out = outC->stickiness_Together.val; outC->der_out.val = last_v2; outC->_2_der_out.val = last_v1; /* guard_Together */ if (br_1_guard_Together) { outC->reset_nxt = kcg_true; outC->state_nxt = SSM_st_Apart; tmp = kcg_true; } else { outC->reset_nxt = kcg_false; outC->state_nxt = SSM_st_Together; tmp = kcg_false; } outC->init4 = kcg_false; break; case SSM_st_Apart : if (reset_sel) { outC->init = kcg_true; } /* last_init_ck_mediant */ if (outC->init) { last_mediant_Apart = 0.0; } else { last_mediant_Apart = outC->mediant_Apart; } outC->zc_br_1_guard_Apart.out = outC->x1 - outC->x2; br_1_guard_Apart = outC->zc_br_1_guard_Apart.up | kcg_up( outC->zc_br_1_guard_Apart.last, outC->zc_br_1_guard_Apart.out); /* guard_Apart */ if (br_1_guard_Apart) { outC->der_out.val = last_mediant_Apart; outC->_2_der_out.val = last_mediant_Apart; outC->reset_nxt = kcg_true; outC->state_nxt = SSM_st_Together; tmp = kcg_true; } else { outC->der_out.val = last_v2; outC->_2_der_out.val = last_v1; outC->reset_nxt = kcg_false; outC->state_nxt = SSM_st_Apart; tmp = kcg_false; } outC->mediant_Apart = (outC->_2_der_out.val * m1 + outC->der_out.val * m2) / (m1 + m2); outC->stickiness_out = 0.0; outC->pull = 0.0; outC->init = kcg_false; break; } outC->v2 = outC->der_out.val; outC->v1 = outC->_2_der_out.val; outC->total = 0.5 * m1 * outC->v1 * outC->v1 + 0.5 * m2 * outC->v2 * outC->v2 + 0.5 * k1 * (outC->x1 - p1) * (outC->x1 - p1) + 0.5 * k2 * (outC->x2 - p2) * (outC->x2 - p2); /* horizon */ if (tmp) { outC->horizon = 0.0; } else { outC->horizon = kcg_infinity; } } void stickysprings_cont(outC_stickysprings *outC) { outC->x2 = outC->_1_der_out.last; outC->x1 = outC->_3_der_out.last; outC->v2 = outC->der_out.last; outC->v1 = outC->_2_der_out.last; /* act_anon_sm */ switch (outC->state_nxt) { case SSM_st_Together : outC->pull = /* abs_float */ abs_float(- outC->x1 * (k1 + k2) + (k2 * p2 - k1 * p1)); outC->zc_br_1_guard_Together.out = outC->pull - outC->stickiness_Together.last; outC->stickiness_Together.der = - outC->stickiness_Together.last / tau; outC->_2_der_out.der = (k1 * p1 + k2 * p2 - (k1 + k2) * outC->x1) / (m1 + m2); outC->stickiness_out = outC->stickiness_Together.last; outC->der_out.der = outC->_2_der_out.der; break; case SSM_st_Apart : outC->zc_br_1_guard_Apart.out = outC->x1 - outC->x2; outC->mediant_Apart = (outC->_2_der_out.last * m1 + outC->der_out.last * m2) / (m1 + m2); outC->stickiness_out = 0.0; outC->pull = 0.0; outC->der_out.der = k2 * (p2 - outC->x2) / m2; outC->_2_der_out.der = k1 * (p1 - outC->x1) / m1; break; } outC->total = 0.5 * m1 * outC->v1 * outC->v1 + 0.5 * m2 * outC->v2 * outC->v2 + 0.5 * k1 * (outC->x1 - p1) * (outC->x1 - p1) + 0.5 * k2 * (outC->x2 - p2) * (outC->x2 - p2); outC->_1_der_out.der = outC->v2; outC->_3_der_out.der = outC->v1; } kcg_real stickysprings_horizon(outC_stickysprings *outC) { /* stickysprings */ kcg_real horizon_acc; /* stickysprings */ kcg_real _1_horizon_acc; horizon_acc = kcg_infinity; horizon_acc = kcg_min(horizon_acc, outC->horizon); outC->horizon = kcg_infinity; return horizon_acc; }
#include "stddef.h" #include "stickysprings.h" #define MODEL_IDENTIFIER stickysprings #define SCADE_OUT_CTX outC_stickysprings #define INIT_FUN stickysprings_init #define RESET_FUN stickysprings_reset #define STEP_FUN stickysprings #define CONT_FUN stickysprings_cont #define HORIZON_FUN stickysprings_horizon #include "fmu_wrapper.h" static const size_t vars_offsets[7] = { SCADE_CTX_OFFSET + offsetof (outC_stickysprings, x1), SCADE_CTX_OFFSET + offsetof (outC_stickysprings, v1), SCADE_CTX_OFFSET + offsetof (outC_stickysprings, x2), SCADE_CTX_OFFSET + offsetof (outC_stickysprings, v2), SCADE_CTX_OFFSET + offsetof (outC_stickysprings, pull), SCADE_CTX_OFFSET + offsetof (outC_stickysprings, stickiness_out), SCADE_CTX_OFFSET + offsetof (outC_stickysprings, total) }; #define NB_CSTATE 5 static const size_t cstates_offsets[5] = { SCADE_CTX_OFFSET + offsetof (outC_stickysprings, stickiness_Together), SCADE_CTX_OFFSET + offsetof (outC_stickysprings, _3_der_out), SCADE_CTX_OFFSET + offsetof (outC_stickysprings, _2_der_out), SCADE_CTX_OFFSET + offsetof (outC_stickysprings, _1_der_out), SCADE_CTX_OFFSET + offsetof (outC_stickysprings, der_out) }; #define NB_ZC 2 static const size_t zc_offsets[2] = { SCADE_CTX_OFFSET + offsetof (outC_stickysprings, zc_br_1_guard_Together), SCADE_CTX_OFFSET + offsetof (outC_stickysprings, zc_br_1_guard_Apart) }; static const zc_dir zc_dirs[2] = { UP, UP }; #include "fmu_wrapper.c"