形式手法の１つである LUSTRE に関する情報

ミッションクリティカルなシステムへの適用を考えています。

0. 言語設計
　同期型言語は、リアクティブなシステム向けの高級言語です。
　LUSTRE は、Esterel-Technologies社の SCADE に中心的な言語として使われています。
　　適用例
　　　・原子力発電所の制御ソフトウェア
　　　・エアバス社の飛行機の制御ソフトウェア

1. 言語の基本
　LUSTRE のプログラムまたは、サブプログラムは、ノード と呼びます（関数や、ブロックと考えたほうがわかりやすいでしょう）。
　LUSTRE は ストリーム による関数型言語です。
　さしあたって、"ストリーム" は、有限または無限のシーケンス上の値だと解釈してください（信号と考えても良いです）。１つのストリームは、常に同じ型です。プログラムは、周期的に動きます（クロックによる演算周期を持ちます）。ｎサイクル目のプログラム実行では、全てのストリームはｎサイクル目の値を持ちます。
　１つのノードは、１つまたは複数のパラメータを入力して、１つまたは複数のパラメータを出力します。これらのパラメータが、ストリームです。

　早い話が、多入力／多出力のシステムをノードと呼びます。MATLAB/Simulinkを使ったことがある人は、ブロックと思えばよいです。プログラムの得意な人は、関数と思えばよいです。

1.1 シンプルな制御デバイス
1.1.1 ２値のノード
　最初の例として、Figure1のようなノードを考えます。



　入力はboolean型のストリームX=(x1,x2,...,xn,...)とします。出力は、boolean型のストリームY=(xy,y2,...,yn,...)とします。XとYの関係は、Xの立ち上がりエッジを検出してYのエッジが立ち上がるものとします。yn+1は、xnがfalseでxn+1がtrueのときにtrueとなります（Xはn+1サイクルのときにfalseからtrueになります）。
　このノードのインタフェースは、次のように表現できます。

node EDGE (X: bool) returns (Y: bool);

出力Yの定義は、1つの式で表現できます。

Y = X and not pre(X);

"Y"と"X and not pre(X)"は、常に等しくなります。
この式は、3つのオペレータを含んでいます。

・"and"と"not"はbool型のオペレータで、データオペレータと呼んでいる。
　　"xor"や"or"も定義されている。"int"や"real"は型変換のオペレータである。
・"pre"は、nサイクル目のときに、1サイクル前の値を示す。
　　A=(a1,a2,...an,...)の時、pre(A)は(nil,a1,a2,...,an-1,...)となる。
　　初期値は、未定義(nil)となる。
・"->"は、ストリームの初期化を示す。
　　A=(a1,a2,...an,...)、B=(b1,b2,...bn,...)で同じ型とした場合、"A->B"は、(a1,b2,...bn,...)となる。
　　初期値は、Aと等しくなり、それ以降はBと等しくなる。このオペレータは、"pre"オペレータによる"nil"値を防ぐ目的で使用される。

"nil"値を防ぐために、"->"を使用すると、Figure.1のEDGEは、次式となる。

　node EDGE (X: bool) returns (Y: bool);
　let
　　Y = false -> X and not pre(X);
　tel

1.2 オペレータの一覧

　　　and　　or　　xor　　not　　#

　　　if...then...else...　+　　 -

　　　*　　　/　　 div　　mod　　=

　　　<>　　 <　　 <=　　 >　　　>=

　　　int　　real　bool

1.3 ２値の平均

２値の平均を算出するノードは、次にように表現できます。

　　　　　　　　　　　　　　　Figure 2：平均値

node　Average(X, Y : int)
returns (A : int);
let
　　A = (X + Y)/2;
tel

別な表現もあります。ローカル変数を使ってみましょう。

node　Average(X, Y : int)
returns (A : int);
var S : int;
let
　　A = S/2;
　　S = X + Y;　　-(order does not matter)
tel

2. その他

2.1 基本

・基本型　：
　　　bool, int, real

・定数　　：
　　　2 ≡ 2,2,2,...
　　　true ≡ true,true,true,...

・変数　　：
　　　X ≡ x0,x1,x2,...　Y ≡ y0,y1,y2,...
　　　X + Y ≡ x0+y0, x1+y1, x2+y2,...

・if　　　：
　　　node　Max(A,B : real) returns (M : real);
　　　let
　　　　　M = if (A >= B) then A else B;
　　　tel

2.2 メモリ操作

• ディレイ

・前回値　：　pre
　　　　　 X　　　x0　x1　x2　x3　x4　・・・
　　　pre X　　　nil　x0　x1　x2　x3　・・・
　　　i.e. (pre X)0は未定義 and ∀i≠0の時、(pre X)i = Xi-1

・初期化　：　->
　　　　X　　　x0　x1　x2　x3　x4　・・・
　　　　Y　　　y0　y1　y2　y3　y4　・・・
　　 X->Y　　x0　y1　y2　y3　y4　・・・
　　　i.e. (X->Y)0 = X0 and ∀i≠0の時、(X->Y)i = Yi

• メモリを含んだノード

・Booleanの例　：　ポジティブエッジ
　　node　Edge (X : bool) returns (E : bool);
　　let
　　　　E = false -> X and not pre X;
　　tel

・数値演算の例　：　min and max
　　node　MinMax(X : int)
　　returns (min, max : int);
　　let
　　　min = X -> if (X < pre min) then X else pre min;
　　　max = X -> if (X > pre max) then X else pre max;
　　tel

2.3 帰納的定義

• 例

・N = 0 -> pre N + 1
　　　　N = 0,1,2,3,・・・

・A = false -> not pre A
　　　　　A = false, true, false, true, ・・・

2.4 構文的ループと意味論的ループ

・例：
　　　X = if C then Y else A;
　　　Y = if C then B else X;
　　構文的には、ループする。
　　意味論的には？： X = Y = if C then B else A

・LUSTREでの正しい定義では、構文的ループは排除する。

3. 演習

3.1 Fibonacci

・Q.
　　　A flow F = 1,1,2,3,5,8,・・・?

・A.
　　　f = 1 -> pre(f + (0 -> pre f));

3.2 Bistable

・Q.
　　　A node Switch(on, off : bool) returns (s : bool);
　　　★onの時、s はfalseからtrueへ立ち上がる。offの時、s はtrueからfalseに立ち下がる。
　　　★sの初期値はfalse
　　　★offでもonでも適切に動く

・A.
　　　node Switch(on, off : bool) returns (s : bool);
　　　let
　　　 　　s = if(false -> pre s) then not off else on;
　　　tel

3.3 counter

・Q.
　　　A node Count(reset,x : bool) returns (c : int);
　　　★resetが真ならば、cは0にリセットされ、それ以外ならば、xが真の場合にインクリメントする。
　　　★cの初期値は、0とする。

・A.
　　　node Count(reset,x : bool) returns (c : int);
　　　let
　　　　　c = if reset then 0
　　　　　　　　else if x then (0 -> pre c) + 1
　　　　　　　　else (0 -> pre c);
　　　tel

4. モジュール化

4.1 再利用

・既にユーザが定義したノードは、オペレータとして利用可能。

・関数のように、インスタンス化される。

・例　(出力はいくつになるでしょうか？)
　　　A = Count(true -> (pre A = 3), true)

・複数の出力
　　node MinMaxAverage(x: bool) returns (a: int);
　　var min,max: int;
　　let
　　　　a = average(min, max);
　　　　　min, max = MinMax(x);
　　　tel

4. ストップウォッチの例

• 出力：時刻（整数型）
• 入力：on_off, reset, freeze

　　★on_offは、ストップウォッチのSTARTとSTOPボタンである。
　　★resetは、リセットボタンである。
　　★freezeは、表示している時刻を止める。

• ローカル変数

　　★runningは、bool型のswitch
　　★freezedは、bool型のswitch
　　★cptは、int型のカウンタ

node Stopwatch(on_off, reset, freeze: bool)
returns (time: int);
var running, freezed:bool, cpt:int;
let
　　running = Switch(on_off, on_off);
　　freezed = Switch(freeze and running, freeze or on_off);
　　cpt = Count(reset and not running, running);
　　time = if freezed then (0 -> pre time) else cpt;
tel

5. クロック

・サンプリング　：　when
　　　X　　　　　　4　 　　1　　　-3　 　0　 　　2　　　 7　　　8
　　　C　　　　　 true 　false　false　true　 true　 false　true
　　X when C　　 4　　　 　　　　　　　0　　　　2　　　　　　　 8

※ Cがfalseの時は常に、"X when C"は、存在しない。

・現在値　：　current
　　　X　　　　　　　　4　 　　1　　　-3　 　0　 　　2　　　 7　　　8
　　　C　　　　　　　 true 　false　false　true　 true　 false　true
　Y = X when C　 　4　　　 　　　　　　　　0　　 　2　　　　　　　8
　Z = current(Y)　　4　　　 4 　　　 4　 　0　 　　2　　 　2　　　8

・ノードとクロック
　　　　　　　C　　　　　　　　 true 　true 　false　false　true　 false　true
　Count((r,true) when C)　 　1　　　2　 　　　　　　 　　　3　　 　　　　　4
　 Count(r,true) when C　　　1　　　2　　　　　　　 　　　 5　　　　　 　　7

・クロックを用いたストップウォッチの例
node Stopwatch(on_off,reset,freeze: bool)
returns (time: int);
var running, freezed: bool;
　　cpt_ena, tim_ena: bool;
　　(cpt:int) when cpt_ena;
let
　　running = Switch(on_off, on_off);
　　freezed = Switch(freeze and running, freeze or on_off);
　　cpt_ena = true -> reset or running;
　　cpt = Count((not running, true) when cpt_ena);
　　tim_ena = true -> not freezed;
　　time = current(current(cpt) when tim_ena);
tel

・クロックのチェック
　★型のチェックと同様
　★クロックには名前をつける必要がある（同じ変数名のクロックは、同じ値を持つ）
　★クロックの変数は、それぞれを宣言する必要がある
　★clk(exp when C) = C ⇔ clk(exp) = clk (c)
　★clk (current exp) = clk (clk (exp))
　★clk (e1 op e2) = C ⇔ clk (e1) = clk (e2) = C

●クロックを用いたプログラミング

・クロックは、意味論的に正しい解決策
・しかし、クロックの使用は、トリッキーである
・初期化の問題
　　current(X when C)は存在するが、Cが最初にtrueになるまで値が未定義になる
・解決策：activation condition
　　★オペレータではなく、マクロのようなもの
　　★X = CONDACT(OP, clk, args, dflt) は、次式と等価
　　　X = if clk then current(OP(args when clk)) else (dflt -> pre X)
　　★SCADEで実装されている

すべてここにあるか？

専用言語　対　汎用言語

• 同期型言語は、リアクティブシステムの中心となる専用言語
• 構造体の操作は実装していない
• 抽象的な型は、ホストの言語からインポートされる（C言語等）

しかしながら・・・

• 静的な配列は提供されている
• 静的な再帰は可能（Lustre V4, 回路専用）
• モジュールとテンプレートの提供（Lustre V6, ソフトウェア専用）