- The added line is THIS COLOR.
- The deleted line is THIS COLOR.
* HydLa, A Hybrid Constraint Language [#l7994977]
- HydLa is a modeling language for hybrid systems.
- HydLa is based on constraints, which inclue ordinary differential equations, temporarl operators and logical operators.
// TODO: link to formal syntax written in BNF.
* Basic Syntax [#r2da58d9]
- A basic hydLa program consists of definitions of constraints and declaration of constraint hierarchies.
** Definition [#s649ac18]
- One can define constraint using the operator " ''<=>'' ".
>
(name of the constraint) ''<=>'' (definition of constraint) .
<
** Constraint [#a67e46ed]
*** Conjunction [#jd43749f]
>
(constraint1) ''&'' (constraint2)
or
(constraint1) ''/\'' (constraint2)
~ (constraint1) ''&'' (constraint2)
~ or
~ (constraint1) ''/\'' (constraint2)
<
*** Always [#e8fd1135]
- ''Always'' operator in temporal logic is denoted by "''[]''"
- This operator means the constraint is effective forever from the time when this constraint is in maximal module sets.
// TODO: link to maximal module set
>
''[]''( constraint )
<
*** Guard Condition [#tdd5bc86]
- The "''=>''" operator means the left-hand side is the guard condition of the right-hand side.
- The constraint on right-hand side is effective only when the left-hand side is entailed.
>
guard ''=>'' constraint
<
*** Differential [#c106f801]
- The ' operator means the differential of the variable with respect to time.
>
variable'
変数(variable)に「'」記号がついたものは, 変数(variable)の時間微分を表す
variable-
変数(variable)に「-」記号がついたものは, 各時刻における変数(variable)の左極限値を表す
逆に, この記号がついていない制約は時刻t=0においてのみ成り立つ
exp
制約において使用される等式や不等式では, 「'」や「-」に加えて算術演算子である「+」「-」「*」「/」やべき乗「^」or「**」の演算子も使うことができる
また, 特殊な値として自然対数の底である「E」や円周率である「Pi」も使用できる
ask
ガード条件となる論理式においては, 「'」や「-」算術演算子などに加えて比較演算子となる「<」「>」「<=」「>=」「=」「!=」や「!」(not), また, andを表す「&」や「/\」, orを表す「|」「\/」の演算子を使うことができる
また, 論理式の評価結果はbool値となる
<
- これが制約の定義・宣言において用いられる基本的な記法となる
- 次にプログラムの本体となる制約階層の記法を説明する
*** Prev [#y9d604d8]
- The "-" operator means the just before value of the variable in every time point.
>
constraint1 , constraint2 , constraint3 << constraint4.
プログラムは, 定義・宣言された各制約について, その関係をふまえて記述する
ここで使用される記号は「,」と「<<」がありそれぞれについて説明する
variable'-'
<
*** exp [#r04a0562]
- In describing equality or inequality as the constraint, not only the '(differential) , -(prev) operators, but also the arithmetic operators (+,-(minus),*,/,^(power),**(power) )can be used.
- As the special values , Napier's constant "E" and Pi "Pi"(the ratio of circumference to diameter) can be used too.
*** ask [#b9a84175]
- In describing formula as guard condition, these (',-,arithmetic operators) , the relational operatprs (>,<,<=,>=,=,!=) and the logical operators (!(not),&(and),/\(and),|(or),\/(or)) can be used.
- The evaluation result of formula is boolean value.
** Hierarchy [#oc2bb594]
- The program is described as the defined constraints and these relations.
- In describing programs, the "," operator and the "<<" operator can be used.
*** Equality [#i272cd72]
- The "," operator means that these two constraints(constraint1,constraint2) are equivalent.
>
constriant1 , constraint2
ここの「,」記号は二つの制約(constraint1,constraint2)間に優先順位がないことを表す
<
*** Superiority [#s5ec52f8]
- The "<<" operator means right-hand side constraint(constraint4) is superior to left-hand side constraint(constraint3)
- If there is contradictions between constraint3 and constraint4, constraint4 is adopted and constraint3 is excluded.
>
constraint3 << constraint4
ここの「<<」記号は左の制約(constraint3)より右の制約(constraint4)が優先されることを表し,
例えばconstraint3の制約とconstraint4の制約において矛盾が発生した場合に, constraint4の制約が優先的に採用されることになる
<
*** Bonding [#p96713f4]
- The "<<" operator is more strong bonding strength than the "," operator.
- Example:
>
constraint1 , constraint2 , constraint3 << constraint4.
また, 「,」記号と「<<」記号では「<<」記号の方が結合度が強い
つまり,
「constraint1 , constraint2 , (constraint3 << constraint4).」と同義であり
「(constraint1 , constraint2 , constraint3) << constraint4.」ではない
<
- 最後にASSERT文の記法について説明する
- This example means
not
>
(constraint1 , constraint2 , constraint3) << constraint4.
<
but
>
constraint1 , constraint2 , (constraint3 << constraint4).
<
** Assert [#m5d52a83]
- The condition(ask) is described in the assert sentence.
- The condition(ask) must be always satisfied in the simulation of HydLa program.
- In the condition(ask), the always operator("[]") can't be used. But the condition is always judged for all the time of simulation.
- The condition is judged within simulating time and is not judged over simulating time.
>
ASSERT{ ask }.
ASSERT文では, HydLaプログラムが常に満たすべき条件(ask)を記述する
この条件(ask)は「[]」記号を使用できないが, 常に全時刻に対しての判定を行う
また, 条件(ask)はシミュレーション時間内において満たされるかどうか判定しており, シミュレーション時間の終了後までは判定していない
<
- この基本的な記法を用いて, 具体的にプログラムを記述すると次の例題のように掛ける
- また, 高度な記法についても説明する
** 例題 : 床を跳ねる質点 [#haead636]
- 具体的に床を跳ねる質点の例題を用いて記法の説明を行う
- 床を跳ねる質点のHydLaプログラムは次のようになる
* Example : Bouncing Particle [#haead636]
- This program is the model that a particle is falling down into floor, bounces at collision of particle and floor and repeat these movement.
- The variable "y" is the position(height) of the particle.
- The floor is at "y=0".
>
~ INIT <=> y=5 & y'=5.
~ FALL <=> [](y'' = -10).
~ BOUNCE <=> [](y- = 0 => y' = -4/5*y'-).
~
~ INIT, FALL << BOUNCE.
<
-- 変数 y は質点の位置である
-- 床は y=0 の位置にある
- INIT : 質点の初期値に関する制約
- INIT : The constraint about the beginning value of the particle.
- By "INIT", the position(y) of the particle is 5 and the speed(y') of the particle is 5 at the starting time.
>
INIT <=> y=5 & y'=5.
<
-- INITでは, t=0の時刻において質点の位置(y)が5, 質点の速度(y')が5であることを定義している
- FALL : 質点の落下運動に関する制約
- FALL : The constraint about the falling movement of the particle.
- By "FALL", the acceleration(y'') of particle is -10 in that the time is over 0.
>
FALL <=> [](y'' = -10).
<
-- FALLでは, 時刻t≧0において重力加速度(-10)の影響で, 質点の加速度(y'')の値がどうなるのかを定義している
- BOUNCE : 質点の跳ね返りに関する制約
- BOUNCE : The constraint about the bouncing movement of the particle
- By "BOUNCE", in that the time is over 0, if the position(y) of the particle become 0, the speed(y') of the particle becomes the value of "-4/5*y'-".
- This is the bouncing movement. And the coefficient of rebound is 4/5.
>
BOUNCE <=> [](y- = 0 => y' = -4/5*y'-).
<
-- BOUNCEでは, 質点が跳ね返る運動を表す制約を定義している
-- 時刻t≧0において質点の位置(y-)が床の位置となった場合(y- = 0), 質点の速度(y')は跳ね返りによって(-4/5*y'-)の値となることを定義している
- プログラムの本体部分(制約階層)
- The core part of HydLa program (constraint hierarchy)
- This part is describing the hierarchy of the constraints(INIT,FALL,BOUNCE).
- BOUNCE is superior than FALL, and INIT is equal to them.
- In other words, when the particle collide with the floor, not FALL but BOUNCE is adopted as the value of the variable y.
>
INIT, FALL << BOUNCE.
<
-- プログラムの本体となる制約階層に関して記述している
-- ここでは, FALL と BOUNCE ではBOUNCEが優先順位が高く, INITはそれらと並列であると定義している
-- つまり, 床に衝突したとき(y- = 0)質点(y)の値に関しては, FALL(y''=-10)ではなくBOUNCE(y' = -4/5*y'-)の条件が採用される
** 高度な記法 [#k8c62e97]
- ここでは, より高度な記法について説明する
*** 引数を用いた制約の定義・宣言 [#j660a34c]
* Difficult syntax [#k8c62e97]
*** Definition using args [#j660a34c]
- The argument can be used in defining constraint.
- In constraint hierarchy, the constraint is called by applying arguments.
>
constraint_name(arg) <=> constraint .
constraint_name(arg) <=> constraint_definition .
<
- 制約の定義・宣言において引数(arg)を用いることができる
- 制約階層を記述する際に引数(arg)を与えて, 制約を呼び出す
example : Define the constraint that The variables(x,y,z) in constant
>
例 : 変数(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) ).
~ CONST(a) <=> [](a'=0).
~ ...
~ CONST(x),CONST(y),CONST(z),...
<
*** プログラム(制約階層)の定義と呼び出し [#v775c940]
example : Define the beginning values of the variables(x1,x2,x3)
>
~ INIT(x,xh,xv) <=> x=xh & x'=xv.
~ ...
~ INIT(x1,1,0),INIT(x2,2,3),INIT(x3,0,10),...
<
example : Define the collision constraint of the particles(x1,x2,x3) in one dimension
>
~ COL(p,q) <=> []( (p- = q-) => p'=q'- & q'=p'- ).
~ ...
~ ... << ( COL(x1,x2),COL(x1,x3),COL(x2,x3) ).
<
*** Subprogram of Constraint Hierarchy [#zd88597b]
- The subprogram(the part of constraint hierarchy) can be used by naming program name.
- The argument can be used too.
- In describing the constraint hierarchy, this subprogram is called.
>
~ program_name { program } .
~ program_name(arg) { program } .
<
- 名前(program_name)をつけて, 部分的な制約階層(program)を定義することができる
- また, 引数(arg)を用いることも可能である
- 全体の制約階層の記述の際に, 制約と同様に呼び出すことができる
example : Make some constraint together.
>
例 : 複数の初期値に関する制約の制約階層を一つにまとめる
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), ...
~ INITS { INIT(x1), INIT(x2), INIT(x3) }.
~ INITS, ...
<
*** 集合記法 [#eea12551]
example : Make the hierarchy of two constraint together
>
~ CONSTMOVE { CONST << MOVE }.
~ CONSTMOVE, ...
<
example : Define bouncing program of the particles(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 [#eea12551]
- The set of some variables can be used.
- The syntax of the set is some way.
>
set_name := set .
<
- 複数の変数を集合として, より高度に扱うことができる
- setの部分で集合を記述するには, さまざまな方法が可能であるので例を用いて説明する
- Example of Defining
>
- 集合に関する定義
-- 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 }
~ es := {e1, e2, e3, e4}.
~ ten := { i | i in {0..9} }.
~ xten := {x1..x10} .
<
*** 利用可能な特殊関数 [#w69ae32d]
- The calculation of sets
>
- 三角関数
-- sin(x) : xの正弦
-- cos(x) : xの余弦
-- tan(x) : xの正接
- 逆三角関数
-- asin(x) : xの逆正弦
-- acos(x) : xの逆余弦
-- atan(x) : xの逆正接
~ union := xten or es .
~ intersection := ten and xten .
<
- The element of sets
>
~ set[i] : The i'th element of the "set" (element is start 0)
~ sum(set) : The sum of the "set"
~ |set| : The number of the "set"
<
- Examples:
>
~ { 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 }
<
*** Special function [#w69ae32d]
- The trigonometric function
>
~ sin(x)
~ cos(x)
~ tan(x)
<
- inverse trigonometric function
>
~ asin(x)
~ acos(x)
~ atan(x)
<
