HydLaWiki
Examples
Start:
#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 gro...
INIT, FALL << BOUNCE. // FALL is weaker than BOUNCE
&ref(./Bouncing_Particle.png,50%);
----
* Bouncing particle with a parametric initial height [#z5...
INIT <=> 5 < y < 15 & y' = 0. // the initial height is...
FALL <=> [](y'' = -10).
BOUNCE <=> [](y- = 0 => y' = -4/5 * y'-).
INIT, FALL << BOUNCE.
&ref(./Bouncing_Particle_with_a_Parameter.png,100%);
----
* 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 * c...
* new y' = (k+1) * sin * cos * x' + (sin^2 + (-k) *...
*/
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...
& y' = ( (k+1) * s * c ) * x'- + ( s^2 + (...
INIT, SC, A << BOUNCE.
&ref(./Bouncing_Paticle_on_a_Curve.png,70%);
----
* Bouncing particle in a circle [#xbf24e18]
INIT <=> x = 0 /\ 0.5 < y < 0.6 /\ x' = 2 /\ y' = 1.
// the initial pos...
RUN <=> [](x'' = 0 /\ y'' = 0).
BOUNCE <=> []((x-)^2 + (y-)^2 = 1 =>
x' = x'- - (x- * x'- + y- * y'-) * 2 *...
/\ y' = y'- - (x- * x'- + y- * y'-) * 2 *...
).
INIT, RUN<<BOUNCE.
&ref(./Bouncing_Particle_in_a_Circle.png,70%);
----
* Hot-Air Balloon with multiple parameters [#tf906f5e]
/* A program for a hot-air balloon that repeats rising a...
// 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%);
----
* 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 ...
SWITCHOFF <=> [](timer-=1=>mag=0&timer=0).
// The magnetic force may be switched off...
INIT,TIMER<<(SWITCHOFF,SWITCHON)<<TRUE,FALL<<BOUNCE.
&ref(./Bouncing_Particle_with_Magnetic_Force.png,70%);
----
* 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 ...
-- If \( 9 < y_0 < 10 \), the ball doesn't reach the ceil...
-- If \( y_0 = 10 \), the ball touches the ceiling, but t...
-- If \( 10 < y_0 < 11 \), the ball bounces on the ceilin...
- HyLaGI performs such a case analysis automatically.~
#norelated
&ref(./Bouncing_Particle_thrown_toward a_ceiling.png,100%);
----
End:
#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 gro...
INIT, FALL << BOUNCE. // FALL is weaker than BOUNCE
&ref(./Bouncing_Particle.png,50%);
----
* Bouncing particle with a parametric initial height [#z5...
INIT <=> 5 < y < 15 & y' = 0. // the initial height is...
FALL <=> [](y'' = -10).
BOUNCE <=> [](y- = 0 => y' = -4/5 * y'-).
INIT, FALL << BOUNCE.
&ref(./Bouncing_Particle_with_a_Parameter.png,100%);
----
* 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 * c...
* new y' = (k+1) * sin * cos * x' + (sin^2 + (-k) *...
*/
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...
& y' = ( (k+1) * s * c ) * x'- + ( s^2 + (...
INIT, SC, A << BOUNCE.
&ref(./Bouncing_Paticle_on_a_Curve.png,70%);
----
* Bouncing particle in a circle [#xbf24e18]
INIT <=> x = 0 /\ 0.5 < y < 0.6 /\ x' = 2 /\ y' = 1.
// the initial pos...
RUN <=> [](x'' = 0 /\ y'' = 0).
BOUNCE <=> []((x-)^2 + (y-)^2 = 1 =>
x' = x'- - (x- * x'- + y- * y'-) * 2 *...
/\ y' = y'- - (x- * x'- + y- * y'-) * 2 *...
).
INIT, RUN<<BOUNCE.
&ref(./Bouncing_Particle_in_a_Circle.png,70%);
----
* Hot-Air Balloon with multiple parameters [#tf906f5e]
/* A program for a hot-air balloon that repeats rising a...
// 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%);
----
* 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 ...
SWITCHOFF <=> [](timer-=1=>mag=0&timer=0).
// The magnetic force may be switched off...
INIT,TIMER<<(SWITCHOFF,SWITCHON)<<TRUE,FALL<<BOUNCE.
&ref(./Bouncing_Particle_with_Magnetic_Force.png,70%);
----
* 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 ...
-- If \( 9 < y_0 < 10 \), the ball doesn't reach the ceil...
-- If \( y_0 = 10 \), the ball touches the ceiling, but t...
-- If \( 10 < y_0 < 11 \), the ball bounces on the ceilin...
- HyLaGI performs such a case analysis automatically.~
#norelated
&ref(./Bouncing_Particle_thrown_toward a_ceiling.png,100%);
----
Page:
