HydLaWiki
HydLa(J)
Start:
* [[HydLa]]とは [#l7994977]
- HydLaとは, ハイブリッドシステムの為の宣言型言語である
- 与えられたシステムの数学的定義をできるだけそのままの形...
- HydLaプログラムは, 時間の推移に伴い連続的もしくは離散的...
* 記法 [#u40c53dc]
- まず, HydLaプログラムでは重要な制約という考え方がある
*** HydLaプログラムにおける制約とは何か? [#l7eceb06]
-- 等式(方程式など)や不等式で定義されている条件(連立方程...
-- さらにいくつかの条件を加えたもの(ガード条件, always)
-- これら制約の論理積のことも表す
** 基本的な記法 [#r2da58d9]
- HydLaプログラムは, 条件や制約等の宣言部分, その宣言され...
- まずは, 制約等の宣言部分の記法から説明する
>
constraint_name <=> constraint .
制約の定義・宣言 : 「<=>」記号は制約の定義・宣言におい...
<
- ここで制約において使用される記法や記号を説明する
>
constraint1 & constraint2 /\ constraint3
「&」記号や「/\」記号は論理積を表し, 例えばこれは３つの...
variable'
変数(variable)に「'」記号がついたものは, 変数(variable)...
variable-
変数(variable)に「-」記号がついたものは, 各時刻における...
[]( constraint )
「[]」記号は, その次に続く制約(constraint)が時刻t≧0以上...
逆に, この記号がついていない制約は時刻t=0においてのみ成...
ask => constraint
「=>」記号を含む式は条件付きの制約を表し, 左辺の論理式(...
右辺はガード条件がtrueとなる場合に有効となる制約を表す
exp
制約において使用される等式や不等式では, 「'」や「-」に...
また, 特殊な値として自然対数の底である「E」や円周率であ...
ask
ガード条件となる論理式においては, 「'」や「-」算術演算...
また, 論理式の評価結果はbool値となる
<
- これが制約の定義・宣言において用いられる基本的な記法と...
- 次にプログラムの本体となる制約階層の記法を説明する
>
constraint1 , constraint2 , constraint3 << constraint4.
プログラムは, 定義・宣言された各制約について, その関係...
ここで使用される記号は「,」と「<<」がありそれぞれについ...
constriant1 , constraint2
ここの「,」記号は二つの制約(constraint1,constraint2)間...
constraint3 << constraint4
ここの「<<」記号は左の制約(constraint3)より右の制約(con...
例えばconstraint3の制約とconstraint4の制約において矛盾...
constraint1 , constraint2 , constraint3 << constraint4.
また, 「,」記号と「<<」記号では「<<」記号の方が結合度が...
つまり,
「constraint1 , constraint2 , (constraint3 << constrain...
「(constraint1 , constraint2 , constraint3) << constrai...
<
- 最後にASSERT文の記法について説明する
>
ASSERT{ ask }.
ASSERT文では, HydLaプログラムが常に満たすべき条件(ask)...
この条件(ask)は「[]」記号を使用できないが, 常に全時刻に...
また, 条件(ask)はシミュレーション時間内において満たされ...
<
- この基本的な記法を用いて, 具体的にプログラムを記述する...
- また, 高度な記法についても説明する
** 例題 : 床を跳ねる質点 [#haead636]
- 具体的に床を跳ねる質点の例題を用いて記法の説明を行う
- 床を跳ねる質点の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, 質点の速...
- FALL : 質点の落下運動に関する制約
>
FALL <=> [](y'' = -10).
<
-- FALLでは, 時刻t≧0において重力加速度(-10)の影響で, 質点...
- BOUNCE : 質点の跳ね返りに関する制約
>
BOUNCE <=> [](y- = 0 => y' = -4/5*y'-).
<
-- BOUNCEでは, 質点が跳ね返る運動を表す制約を定義している
-- 時刻t≧0において質点の位置(y-)が床の位置となった場合(y-...
- プログラムの本体部分(制約階層)
>
INIT, FALL << BOUNCE.
<
-- プログラムの本体となる制約階層に関して記述している
-- ここでは, FALL と BOUNCE ではBOUNCEが優先順位が高く, I...
-- つまり, 床に衝突したとき(y- = 0)質点(y)の値に関しては,...
** 高度な記法 [#k8c62e97]
- ここでは, より高度な記法について説明する
*** 引数を用いた制約の定義・宣言 [#j660a34c]
>
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) ).
<
*** プログラム(制約階層)の定義と呼び出し [#v775c940]
>
~ 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), ...
<
*** 集合記法 [#eea12551]
>
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番目を取ってくる (要素の番...
-- sum(set) : 集合(set)の和を求める
-- |set| : 集合(set)の要素数を求める
-- { constarint(set[i]) | i in {1..|set|} }
-- { (constarint1(set[i]) , constarint1(set[i]) ) << cons...
-- { constraint(x) | x in set }
<
*** 利用可能な特殊関数 [#w69ae32d]
>
- 三角関数
-- 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 : 自然対数の底を表す定数
<
End:
* [[HydLa]]とは [#l7994977]
- HydLaとは, ハイブリッドシステムの為の宣言型言語である
- 与えられたシステムの数学的定義をできるだけそのままの形...
- HydLaプログラムは, 時間の推移に伴い連続的もしくは離散的...
* 記法 [#u40c53dc]
- まず, HydLaプログラムでは重要な制約という考え方がある
*** HydLaプログラムにおける制約とは何か? [#l7eceb06]
-- 等式(方程式など)や不等式で定義されている条件(連立方程...
-- さらにいくつかの条件を加えたもの(ガード条件, always)
-- これら制約の論理積のことも表す
** 基本的な記法 [#r2da58d9]
- HydLaプログラムは, 条件や制約等の宣言部分, その宣言され...
- まずは, 制約等の宣言部分の記法から説明する
>
constraint_name <=> constraint .
制約の定義・宣言 : 「<=>」記号は制約の定義・宣言におい...
<
- ここで制約において使用される記法や記号を説明する
>
constraint1 & constraint2 /\ constraint3
「&」記号や「/\」記号は論理積を表し, 例えばこれは３つの...
variable'
変数(variable)に「'」記号がついたものは, 変数(variable)...
variable-
変数(variable)に「-」記号がついたものは, 各時刻における...
[]( constraint )
「[]」記号は, その次に続く制約(constraint)が時刻t≧0以上...
逆に, この記号がついていない制約は時刻t=0においてのみ成...
ask => constraint
「=>」記号を含む式は条件付きの制約を表し, 左辺の論理式(...
右辺はガード条件がtrueとなる場合に有効となる制約を表す
exp
制約において使用される等式や不等式では, 「'」や「-」に...
また, 特殊な値として自然対数の底である「E」や円周率であ...
ask
ガード条件となる論理式においては, 「'」や「-」算術演算...
また, 論理式の評価結果はbool値となる
<
- これが制約の定義・宣言において用いられる基本的な記法と...
- 次にプログラムの本体となる制約階層の記法を説明する
>
constraint1 , constraint2 , constraint3 << constraint4.
プログラムは, 定義・宣言された各制約について, その関係...
ここで使用される記号は「,」と「<<」がありそれぞれについ...
constriant1 , constraint2
ここの「,」記号は二つの制約(constraint1,constraint2)間...
constraint3 << constraint4
ここの「<<」記号は左の制約(constraint3)より右の制約(con...
例えばconstraint3の制約とconstraint4の制約において矛盾...
constraint1 , constraint2 , constraint3 << constraint4.
また, 「,」記号と「<<」記号では「<<」記号の方が結合度が...
つまり,
「constraint1 , constraint2 , (constraint3 << constrain...
「(constraint1 , constraint2 , constraint3) << constrai...
<
- 最後にASSERT文の記法について説明する
>
ASSERT{ ask }.
ASSERT文では, HydLaプログラムが常に満たすべき条件(ask)...
この条件(ask)は「[]」記号を使用できないが, 常に全時刻に...
また, 条件(ask)はシミュレーション時間内において満たされ...
<
- この基本的な記法を用いて, 具体的にプログラムを記述する...
- また, 高度な記法についても説明する
** 例題 : 床を跳ねる質点 [#haead636]
- 具体的に床を跳ねる質点の例題を用いて記法の説明を行う
- 床を跳ねる質点の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, 質点の速...
- FALL : 質点の落下運動に関する制約
>
FALL <=> [](y'' = -10).
<
-- FALLでは, 時刻t≧0において重力加速度(-10)の影響で, 質点...
- BOUNCE : 質点の跳ね返りに関する制約
>
BOUNCE <=> [](y- = 0 => y' = -4/5*y'-).
<
-- BOUNCEでは, 質点が跳ね返る運動を表す制約を定義している
-- 時刻t≧0において質点の位置(y-)が床の位置となった場合(y-...
- プログラムの本体部分(制約階層)
>
INIT, FALL << BOUNCE.
<
-- プログラムの本体となる制約階層に関して記述している
-- ここでは, FALL と BOUNCE ではBOUNCEが優先順位が高く, I...
-- つまり, 床に衝突したとき(y- = 0)質点(y)の値に関しては,...
** 高度な記法 [#k8c62e97]
- ここでは, より高度な記法について説明する
*** 引数を用いた制約の定義・宣言 [#j660a34c]
>
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) ).
<
*** プログラム(制約階層)の定義と呼び出し [#v775c940]
>
~ 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), ...
<
*** 集合記法 [#eea12551]
>
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番目を取ってくる (要素の番...
-- sum(set) : 集合(set)の和を求める
-- |set| : 集合(set)の要素数を求める
-- { constarint(set[i]) | i in {1..|set|} }
-- { (constarint1(set[i]) , constarint1(set[i]) ) << cons...
-- { constraint(x) | x in set }
<
*** 利用可能な特殊関数 [#w69ae32d]
>
- 三角関数
-- 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 : 自然対数の底を表す定数
<
Page:
