# Backup diff of Examples (No. 6)

• The added line is THIS COLOR.
• The deleted line is THIS COLOR.
```* A 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
// 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 with a Parameter [#z5246173]
>
~
~ INIT   <=> 5 < y < 15 & y' = 0. // the initial height is uncertain
~ FALL   <=> [](y''  = -10).
~ BOUNCE <=> [](y- = 0 => y' = -4/5 * vy'-).
~
~ INIT, FALL << BOUNCE.
* A Bouncing Particle with a Parameter [#z5246173]
>
INIT   <=> 5 < y < 15 & y' = 0. // the initial height is uncertain
FALL   <=> [](y''  = -10).
BOUNCE <=> [](y- = 0 => y' = -4/5 * vy'-).

INIT, FALL << BOUNCE.
<
&ref(./bouncing_particle_rp.png,50%);
----
* A Bouncing Paticle on a Curve [#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.
/**
*  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_particle_U.png,30%);
----
* A 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.
>
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(./circle.png,30%);
----
* A hot-air balloon [#tf906f5e]
* A Hot-Air Balloon with multiple parameters [#tf906f5e]
>
- An example with multiple parameters.
~/* 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.
/* 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(./balloon_tank.png,25%);
----
* A 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.
>
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.
<
----
* A 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.
INIT  <=> 9 < y < 11 & y' = 10.
FALL  <=> [](y'' = -10).
BOUNCE <=> [](y- = 15 => y' = -(4/5)*y'-).

INIT, FALL << BOUNCE.
<
- In this program, the trajectories change qualitatively dependent on the initial height y0.
-- If 9 < y0 < 10, the ball doesn't reaches the ceiling.~
-- If y0 = 10, the ball touches the ceiling, but the velocity remains continuous.~
-- If 10 < t < 11, the ball bounces on the ceiling.~
- HyLaGI performs such a case analysis automatically.~
&ref(./roof_bouncing.png,40%);
----

```