- The added line is THIS COLOR.
- The deleted line is THIS COLOR.
* 例題 [#gabe06d3]
-さまざまな例題について説明する
* bouncing_particle [#p560bc2f]
>
~ // bouncing particle
~
~ INIT <=> y = 10 & y' = 0.
~ FALL <=> [](y'' = -10).
~ BOUNCE <=> [](y- = 0 => y' = -4/5*y'-).
~
~ INIT, FALL << BOUNCE.
<
- このプログラムは, 床(y=0)で跳ね返る質点のモデルとなる
- 変数yは位置(高さ)を表し, 上向きを正とする
- 初期値は, 高さ10(y=10)で速度0(y'=0)から始まる(INIT)
- 重力加速度は-10となる(FALL)
- 床(y=0)に衝突すると跳ね返る(BOUNCE)
- 跳ね返る際は, 逆向きに4/5倍になる(y' = -4/5*y'-)
&ref(./bouncing_particle.png,50%);
#author("2017-03-17T17:42:45+09:00","default:Uedalab","Uedalab")
#noattach
* Bouncing particle [#p560bc2f]
// y stands for the height of the ball
INIT <=> y = 10 & y' = 0. // initial state
FALL <=> [](y'' = -10). // falling
BOUNCE <=> [](y- = 0 => y' = -4/5*y'-).
// if the ball reaches the ground, it bounces
INIT, FALL << BOUNCE. // FALL is weaker than BOUNCE
&ref(./Bouncing_Particle.png,50%);
----
* bouncing_particle_U [#j8167ade]
>
~ /**
~ * bouncing particle in f(x) = (1/2) * x^2
~ */
~
~ INIT <=> x = 1/2 & y = 10 & x' = 0 & y' = 0 & [](k = 1).
~ A <=> [](x" = 0 & y" = -98/10).
~ /**
~ * sin = f'(x) / (1+f'(x))^(1/2)
~ * cos = 1 / (1+f'(x))^(1/2)
~ * new x' = (-k * sin^2 + cos^2) * x' + (k+1) * sin * cos * y'
~ * new y' = (k+1) * sin * cos * x' + (sin^2 + (-k) * cos^2) * y'
~ */
~
~ SC <=> [](s = (x-)/(1+(x-)^2)^(1/2)
~ & c = 1 /(1+(x-)^2)^(1/2)).
~
~ BOUNCE <=> [](y- = (1/2) * (x-)^2 =>
~ x' = ( (-k) * s^2 + c^2 ) * x'-
~ + ( (k+1) * s * c ) * y'-
~ & y' = ( (k+1) * s * c ) * x'-
~ + ( s^2 + (-k) * c^2 ) * y'- ).
~
~ INIT, SC, A << BOUNCE.
<
- このプログラムは, U字型のハーフパイプのような床(f(x) = (1/2) * x^2)を跳ねる質点のモデルとなる
- 質点の位置は, xy座標で表される
&ref(./bouncing_particle_U.png,30%);
* Bouncing particle with a parametric initial height [#z5246173]
INIT <=> 5 < y < 15 & y' = 0. // the initial height is uncertain
FALL <=> [](y'' = -10).
BOUNCE <=> [](y- = 0 => y' = -4/5 * y'-).
INIT, FALL << BOUNCE.
&ref(./Bouncing_Particle_with_a_Parameter.png,100%);
----
* bouncing_particle_rp [#z5246173]
>
~ // bouncing particle with parameter
~
~ INIT <=> 5 < ht < 15 & v = 0 & e =4/5 & [](ht' = v & e'=0).
~ FALL <=> [](v' = -10).
~ BOUNCE <=> [](ht- = 0 => v = -e * v-).
~
~ INIT, FALL << BOUNCE.
<
- このプログラムは, 跳ねる質点のモデルだが初期位置が5~15のパラメータであるモデルとなる
- 質点の高さ(位置)はhtで表され, 速度はvで表される
- 跳ね返る反発係数はeとなり, 制約INITで4/5なっている
* Bouncing particle in a parabolic vase [#j8167ade]
/**
* bouncing particle on a curve of f(x) = (1/2) * x^2
*/
INIT <=> x = 1/2 & y = 10 & x' = 0 & y' = 0 & [](k = 1).
A <=> [](x'' = 0 & y'' = -98/10).
/**
* sin = f'(x) / (1+f'(x))^(1/2)
* cos = 1 / (1+f'(x))^(1/2)
* new x' = (-k * sin^2 + cos^2) * x' + (k+1) * sin * cos * y'
* new y' = (k+1) * sin * cos * x' + (sin^2 + (-k) * cos^2) * y'
*/
SC <=> [](s = (x-)/(1+(x-)^2)^(1/2)
& c = 1 /(1+(x-)^2)^(1/2)).
BOUNCE <=> [](y- = (1/2) * (x-)^2 =>
x' = ( (-k) * s^2 + c^2 ) * x'- + ( (k+1) * s * c ) * y'-
& y' = ( (k+1) * s * c ) * x'- + ( s^2 + (-k) * c^2 ) * y'- ).
INIT, SC, A << BOUNCE.
&ref(./Bouncing_Paticle_on_a_Curve.png,70%);
----
* bouncing_particles [#cd9b6075]
>
~ // many bouncing particles
~
~ INIT(y, y0) <=> y = y0 & y' = 0.
~ FALL(y) <=> [](y'' = -10).
~ BOUNCE(y) <=> [](y- = 0 => y' = -y'-).
~
~ BALL(yarg, y0){INIT(yarg, y0), FALL(yarg) << BOUNCE(yarg)}.
~
~ BALL(y1, 1), BALL(y2, 2),BALL(y3, 3), BALL(y4, 4),BALL(y5, 5),
~ BALL(y6, 6), BALL(y7, 7), BALL(y8, 8). BALL(y9, 9), BALL(y10, 10),
~ BALL(y11, 11),BALL(y12, 12), BALL(y13, 13), BALL(y14, 14).
~ BALL(y15, 15), BALL(y16, 16).
<
- このプログラムは, 複数の質点が跳ねるモデルとなる
- プログラム呼び出し(BALL(yarg, y0))によって16個の質点が定義されている
* Bouncing particle in a circle [#xbf24e18]
INIT <=> x = 0 /\ 0.5 < y < 0.6 /\ x' = 2 /\ y' = 1.
// the initial position is uncertain
RUN <=> [](x'' = 0 /\ y'' = 0).
BOUNCE <=> []((x-)^2 + (y-)^2 = 1 =>
x' = x'- - (x- * x'- + y- * y'-) * 2 * (x-)
/\ y' = y'- - (x- * x'- + y- * y'-) * 2 * (y-)
).
INIT, RUN<<BOUNCE.
&ref(./Bouncing_Particle_in_a_Circle.png,70%);
----
* circle [#xbf24e18]
>
~ //circle.hydla
~ //bouncing particle in a circle
~
~ INIT <=> x = 0 /\ 0.5 < y < 0.6 /\ x' = 2 /\ y' = 1.
~ RUN <=> [](x" = 0 /\ y" = 0).
~ BOUNCE <=> []((x-)^2 + (y-)^2 = 1 =>
~ x' = x'- - (x- * x'- + y- * y'-) * 2 * (x-) /\
~ y' = y'- - (x- * x'- + y- * y'-) * 2 * (y-)
~ ).
~ INIT, RUN<<BOUNCE.
<
- このプログラムは, 円の内部を跳ね返る質点のモデルとなる
- 質点の位置はxy座標で表される
* Hot-Air Balloon with multiple parameters [#tf906f5e]
/* A program for a hot-air balloon that repeats rising and falling */
// The initial condition of the balloon and the timer
// h: height of the balloon
// timer: timer variable to repeat rising and falling
INIT <=> h = 10 /\ h' = 0 /\ timer = 0.
// parameters
// duration: duration of falling
// riseT: duration of rising
PARAM<=> 1 < fallT < 4 /\ 1 < riseT < 3
/\ [](riseT' = 0 /\ fallT' = 0).
// increasing of timer
TIMER <=> [](timer' = 1).
// rising of the balloon
RISE <=> [](timer- < riseT =>h'' = 1).
// falling of the balloon
FALL <=> [](timer- >= riseT => h'' = -2).
// reset the timer to repeat rising and falling
RESET <=> [](timer- >= riseT + fallT => timer=0).
// assertion for bounded model checking
ASSERT(h > 0).
// constraint hierarchies
INIT, PARAM, FALL, RISE, TIMER<<RESET.
&ref(./Hot-Air_Balloon.png,70%);
----
* baloon_tank [#tf906f5e]
>
~ /* A program for a hot-air balloon rising by fuel tanks that are exchanged. */
~
~ INIT<=>h=10/\h'=0/\fuel=1/\timer=0
~ /\2<exT<4
~ ///\ exT = 3
~ /\ 1<volume<3.
~
~ CONS<=>[](exT'=0/\volume'=0).
~ TIME<=>[](timer'=1).
~
~ BURN<=>[](fuel=1=>h''=1).
~ FALL<=>[](fuel=0=>h''=-2).
~
~ VOID<=>[](timer->=volume=>fuel=0).
~ FULL<=>[](timer-<volume=>fuel=1).
~
~ COMP<=>
~ [](timer->=volume+exT=>timer=0).
~
~ ASSERT(h>0).
~
~ INIT,CONS,BURN,FALL,VOID,FULL,TIME<<COMP.
<
- このプログラムは, 燃料によって上下する気球のモデルとなる
- 気球の位置はy軸上で考えている
- 気球は動いている時刻(timer)によって, 燃料がある状態と燃料がない状態がある(VOID,FULL)
- 気球は燃料がある状態(fuel=1)なら上昇(h"=1)していき, 燃料がない状態(fuel=0)なら下降(h"=-2)する
- 燃料がなくなると新しい燃料に交換する, その際にある時間(exT)がかかり, 完了するともう一度燃料がある状態となる(COMP)
* Bouncing particle with magnetic force [#a6ea3f5c]
INIT <=> y=10 & y'=0 & mag=0 & timer=0.
FALL <=> [](y''=-10+mag).
BOUNCE <=> [](y-=0=>y'=-y'-).
TRUE <=> [](1=1).
TIMER <=> [](mag'=0&timer'=1).
SWITCHON <=> [](timer-=1=>mag=12&timer=0).
// The magnetic force may be switched on at every one second
SWITCHOFF <=> [](timer-=1=>mag=0&timer=0).
// The magnetic force may be switched off at every one second
INIT,TIMER<<(SWITCHOFF,SWITCHON)<<TRUE,FALL<<BOUNCE.
&ref(./Bouncing_Particle_with_Magnetic_Force.png,70%);
----
* magnet_ball [#a6ea3f5c]
>
~ /*
~ 重力と磁力の影響を考えたボールの動き
~ 磁力は重力と逆向きに働き、スイッチでＯＮ／ＯＦＦできる
~ スイッチは１秒ごとに切り替えられる可能性がある
~ */
~
~ INIT <=> y=10 & y'=0 & mag=0 & timer=0.
~ FALL <=> [](y''=-10+mag).
~ BOUNCE <=> [](y-=0=>y'=-y'-).
~ TRUE <=> [](1=1).
~ TIMER <=> [](mag'=0&timer'=1).
~ SWITCHON <=> [](timer-=1=>mag=12&timer=0).
~ SWITCHOFF <=> [](timer-=1=>mag=0&timer=0).
~ SWITCHW <=> [](timer-=1=>mag=100&timer=0).
~
~ INIT,TIMER<<(SWITCHOFF,SWITCHON,SWITCHW)<<TRUE,FALL.
<
- 一定時間(timer=1)ごとにスイッチが切り替わり, スイッチによって質点の運動がかわる
- どのスイッチに切り替わるのかは非決定である
* Bouncing particle thrown toward a ceiling [#e682ba1f]
INIT <=> 9 < y < 11 & y' = 10.
FALL <=> [](y'' = -10).
BOUNCE <=> [](y- = 15 => y' = -(4/5)*y'-).
INIT, FALL << BOUNCE.
#mathjax
- In this program, the trajectories change qualitatively dependent on the initial height \( y_0 \).
-- If \( 9 < y_0 < 10 \), the ball doesn't reach the ceiling.~
-- If \( y_0 = 10 \), the ball touches the ceiling, but the velocity remains continuous.~
-- If \( 10 < y_0 < 11 \), the ball bounces on the ceiling.~
- HyLaGI performs such a case analysis automatically.~
#norelated
&ref(./Bouncing_Particle_thrown_toward a_ceiling.png,100%);
----
* stadium [#oab94af0]
>
~ INIT <=> x=3/4 /\ y=0 /\ x'=2 /\ y'=1.
~ RUNX <=> [](x''=0).
~ RUNY <=> [](y''=0).
~ WALL1 <=> []( (x- - 1)^2+(y-)^2=1 & x > 1=>
~ x' = x'- - ( (x- -1)*x'- +y*y'-)*(1+1)*(x- -1) /\
~ y' = y'- - ( (x- -1)*x'- + y-*y'-)*(1+1)*(y-)).
~ WALL2 <=> []((x- + 1)^2+(y-)^2=1 & x < -1=>
~ x' = x'- - ( (x- +1)*x'- +y*y'-)*(1+1)*(x- +1) /\
~ y' = y'- - ( (x- +1)*x'- + y-*y'-)*(1+1)*(y-)).
~ WALL3 <=> [](y- = 1 => y' = -y'-).
~ WALL4 <=> [](y- =-1 => y' = -y'-).
~
~ INIT, (RUNX, RUNY)<<(WALL1,WALL2,WALL3,WALL4).
<
- このプログラムは, スタジアムのようなフィールドを運動する質点のモデルとなる
----
* throw_ball [#wd37993f]
>
~ // throwing ball against head wind
~
~ INIT <=> x = 0 & y = 10 & x' = 10 & y' = 10 & 5 <= y' <= 15.
~ FALL <=> [](y'' = -10).
~ WIND <=> []( (y- >= 15 => x" = -3) & (y- < 15 => x" = 0)).
~
~ INIT, FALL, WIND.
~
~ //ASSERT(!(x >= 25 & y > 0)).
<
- このプログラムは, 質点を投げ上げるモデルとなる
----
* roof_bouncing [#e682ba1f]
>
~ // bouncing particle to a roof
~
~ INIT <=> 9 < y < 11 & y' = 10.
~ FALL <=> [](y'' = -10).
~ BOUNCE <=> [](y- = 15 => y' = -(4/5)*y'-).
~
~ INIT, FALL << BOUNCE.
<
- このプログラムは, 天井に向かって投げ上げる質点のモデルとなる
----
