HydLa(J)

HydLaとは †

HydLaとは, ハイブリッドシステムの為の宣言型言語である
与えられたシステムの数学的定義をできるだけそのままの形で記述し, その実行や解析を目的とする
HydLaプログラムは, 時間の推移に伴い連続的もしくは離散的に変化する関数(軌道)の挙動に関する制約条件をあたえる

↑

記法 †

まず, HydLaプログラムでは重要な制約という考え方がある

↑

HydLaプログラムにおける制約とは何か? †

等式(方程式など)や不等式で定義されている条件(連立方程式とか連立不等式)
さらにいくつかの条件を加えたもの(ガード条件, always)
これら制約の論理積のことも表す

↑

基本的な記法 †

HydLaプログラムは, 条件や制約等の宣言部分, その宣言された制約を呼び出して制約階層(制約同士の関係)を記述するプログラムの本体部分, またはASSET文からなる

まずは, 制約等の宣言部分の記法から説明する

constraint_name <=> constraint .

 制約の定義・宣言  : 「<=>」記号は制約の定義・宣言において使用され, 右辺の「.」記号までの制約の内容に, 左辺の名前をつけて宣言することを表す

ここで制約において使用される記法や記号を説明する

constraint1 & constraint2 /\ constraint3

 「&」記号や「/\」記号は論理積を表し, 例えばこれは３つの制約(constraint1,constraint2,constraint3)の論理積を表す

variable'

 変数(variable)に「'」記号がついたものは, 変数(variable)の時間微分を表す

variable-

 変数(variable)に「-」記号がついたものは, 各時刻における変数(variable)の左極限値を表す

[]( constraint )

 「[]」記号は, その次に続く制約(constraint)が時刻t≧0以上で常に成り立つことを表している(always)
 逆に, この記号がついていない制約は時刻t=0においてのみ成り立つ

ask => constraint

 「=>」記号を含む式は条件付きの制約を表し, 左辺の論理式(結果がbool値となる)をガード条件とした制約のこと
 右辺はガード条件がtrueとなる場合に有効となる制約を表す

exp

 制約において使用される等式や不等式では, 「'」や「-」に加えて算術演算子である「+」「-」「*」「/」やべき乗「^」or「**」の演算子も使うことができる
 また, 特殊な値として自然対数の底である「E」や円周率である「Pi」も使用できる

ask

 ガード条件となる論理式においては, 「'」や「-」算術演算子などに加えて比較演算子となる「<」「>」「<=」「>=」「=」「!=」や「!」(not), また, andを表す「&」や「/\」, orを表す「|」「\/」の演算子を使うことができる
 また, 論理式の評価結果はbool値となる

これが制約の定義・宣言において用いられる基本的な記法となる

次にプログラムの本体となる制約階層の記法を説明する

constraint1 , constraint2 , constraint3 << constraint4.

 プログラムは, 定義・宣言された各制約について, その関係をふまえて記述する
 ここで使用される記号は「,」と「<<」がありそれぞれについて説明する

constriant1 , constraint2

 ここの「,」記号は二つの制約(constraint1,constraint2)間に優先順位がないことを表す

constraint3 << constraint4

 ここの「<<」記号は左の制約(constraint3)より右の制約(constraint4)が優先されることを表し, 
 例えばconstraint3の制約とconstraint4の制約において矛盾が発生した場合に, constraint4の制約が優先的に採用されることになる

constraint1 , constraint2 , constraint3 << constraint4.

 また, 「,」記号と「<<」記号では「<<」記号の方が結合度が強い
 つまり, 
 「constraint1 , constraint2 , (constraint3 << constraint4).」と同義であり
 「(constraint1 , constraint2 , constraint3) << constraint4.」ではない

最後にASSERT文の記法について説明する

ASSERT{ ask }.

 ASSERT文では, HydLaプログラムが常に満たすべき条件(ask)を記述する
 この条件(ask)は「[]」記号を使用できないが, 常に全時刻に対しての判定を行う
 また, 条件(ask)はシミュレーション時間内において満たされるかどうか判定しており, シミュレーション時間の終了後までは判定していない

この基本的な記法を用いて, 具体的にプログラムを記述すると次の例題のように掛ける
また, 高度な記法についても説明する

↑

例題 : 床を跳ねる質点 †

具体的に床を跳ねる質点の例題を用いて記法の説明を行う
床を跳ねる質点のHydLaプログラムは次のようになる

INIT <=> y=5 & y'=5.

FALL <=> [](y'' = -10).

BOUNCE <=> [](y- = 0 => y' = -4/5*y'-).

INIT, FALL << BOUNCE.
- 変数 y は質点の位置である
- 床は y=0 の位置にある
INIT : 質点の初期値に関する制約
INIT <=> y=5 & y'=5.
- INITでは, t=0の時刻において質点の位置(y)が5, 質点の速度(y')が5であることを定義している
FALL : 質点の落下運動に関する制約
FALL <=> [](y'' = -10).
- FALLでは, 時刻t≧0において重力加速度(-10)の影響で, 質点の加速度(y'')の値がどうなるのかを定義している
BOUNCE : 質点の跳ね返りに関する制約
BOUNCE <=> [](y- = 0 => y' = -4/5*y'-).
- BOUNCEでは, 質点が跳ね返る運動を表す制約を定義している
- 時刻t≧0において質点の位置(y-)が床の位置となった場合(y- = 0), 質点の速度(y')は跳ね返りによって(-4/5*y'-)の値となることを定義している
プログラムの本体部分(制約階層)
INIT, FALL << BOUNCE.
- プログラムの本体となる制約階層に関して記述している
- ここでは, FALL と BOUNCE ではBOUNCEが優先順位が高く, INITはそれらと並列であると定義している
- つまり, 床に衝突したとき(y- = 0)質点(y)の値に関しては, FALL(y''=-10)ではなくBOUNCE(y' = -4/5*y'-)の条件が採用される

↑

高度な記法 †

ここでは, より高度な記法について説明する

↑

引数を用いた制約の定義・宣言 †

constraint_name(arg) <=> constraint .

制約の定義・宣言において引数(arg)を用いることができる
制約階層を記述する際に引数(arg)を与えて, 制約を呼び出す
例 : 変数(x,y,z)がそれぞれ時間によって変化しないという制約を定義する
```
 CONST(a) <=> [](a'=0).
 ...
 CONST(x),CONST(y),CONST(z), ...
```
例 : 変数(x1,x2,x3)の初期値に関する制約をそれぞれ定義する
```
 INIT(x,xh,xv) <=> x=xh & x'=xv.
 ...
 INIT(x1,1,0),INIT(x2,2,3),INIT(x3,0,10), ...
```
例 : 一次元上(x軸上)における質点(x1,x2,x3)同士の完全弾性衝突を定義する
```
 COL(p,q) <=> []( (p- = q-) => p'=q'- & q'=p'- ).
 ...
 ... << ( COL(x1,x2),COL(x1,x3),COL(x2,x3) ).
```

↑

プログラム(制約階層)の定義と呼び出し †

program_name { program } .

program_name(arg) { program } .

名前(program_name)をつけて, 部分的な制約階層(program)を定義することができる
また, 引数(arg)を用いることも可能である
全体の制約階層の記述の際に, 制約と同様に呼び出すことができる
例 : 複数の初期値に関する制約の制約階層を一つにまとめる
```
 INITS { INIT(x1), INIT(x2), INIT(x3) }.
 ...
 INITS, ...
```
例 : 二つの制約に関する制約階層をまとめる
```
 CONSTMOVE { CONST << MOVE }.
 ...
 CONSTMOVE, ...
```
例 : お互いが干渉しない質点(y1,y2,y3)において, 地面を跳ねるプログラム(制約階層)をまとめて定義する
```
 ...
 BP(x,h,v) {INIT(x,h,v), FALL(x) << BOUNCE(x)}.
 ...
 BP(y1,1,1),BP(y2,2,3),BP(y3,3,5), ...
```

↑

集合記法 †

set_name := set .

複数の変数を集合として, より高度に扱うことができる
setの部分で集合を記述するには, さまざまな方法が可能であるので例を用いて説明する
- 集合に関する定義
  - es := {e1, e2, e3, e4}.
  - ten := { i | i in {0..9} }.
  - xten := {x1..x10} .
- 集合同士の演算
  - union := xten or es .
  - intersection := ten and xten .
- 集合, その要素の扱い方
  - set[i] : 集合(set)の要素のi番目を取ってくる (要素の番号 i は 0 から始まる)
  - sum(set) : 集合(set)の和を求める
  - |set| : 集合(set)の要素数を求める
  - { constarint(set[i]) | i in {1..|set|} }
  - { (constarint1(set[i]) , constarint1(set[i]) ) << constraint2(set[i], set[j]) | i in {1..|set|-1} , j in {i+1..|set|} }
  - { constraint(x) | x in set }

↑

利用可能な特殊関数 †

三角関数
sin(x) : xの正弦

cos(x) : xの余弦

tan(x) : xの正接

逆三角関数
asin(x) : xの逆正弦

acos(x) : xの逆余弦

atan(x) : xの逆正接

自然対数
ln(x) : xの自然対数

対数
log(a,x) : aを底とする対数

円周率
Pi : 円周率を表す定数

自然対数の底
E : 自然対数の底を表す定数

Last-modified: 2017-03-02 (Thu) 03:21:30 (2605d)