- The added line is THIS COLOR.
- The deleted line is THIS COLOR.
#author("2017-03-17T11:49:00+09:00","default:Uedalab","Uedalab")
#author("2017-03-17T18:00:40+09:00","default:Uedalab","Uedalab")
#noattach
#mathjax
#norelated
* Syntax [#r2da58d9]
- A HydLa program consists of definitions of constraints and declaration of constraint hierarchies.
#ref(./HydLa_BNF.png);
* Syntax [#r2da58d9]
#ref(./HydLa_BNF.png, center);
- A HydLa program consists of definitions of constraints and declarations of constraint hierarchies.
** Definition [#s649ac18]
- One can define constraint using the operator " ''<=>'' ".
>
(name of the constraint) ''<=>'' (definition of constraint) .
<
- In a definition, we define a named constraint or a named constraint hierarchies with arguments using the operator " ''<=>'' ".
If the definition has no arguments, we can omit parentheses.
INIT <=> y = 0 & y' = 0. // definition of a constraint for the initial state of a ball.
FALL <=> [](y'' = -10). // definition of a constraint for falling of the ball.
BOUNCE(x) <=> [](x- = 0 => x' = -x'-). // definition of a constraint for bouncing of the ball.
BALL{FALL << BOUNCE}. // definition of a constraint hierarchy for the ball.
- $Constraints$ allow conjunctions of constraints and implications.
- The antecedents of implications are called $guards$.
- " ''[]'' " denotes a temporal operator which means that the constraint always holds from the time point at which the constraint is enabled.
- Each variable is denoted by a string starting with lower case($vname$).
- The notation $vname′$ means the derivative of $vname$, and $vname−$ means the left-hand limit of $vname$.
** Constraint [#a67e46ed]
*** Conjunction [#jd43749f]
>
~ (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
<
*** Derivative [#c106f801]
- The "'' ' ''" operator means a derivative of the variable with respect to time.
>
(variable | derivative of variable)'
<
*** Prev [#y9d604d8]
- The " - " operator means a left hand limit of a variable at each time point.
>
(variable | derivative of 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]
- Meaning of a HydLa program is a set of trajectories that satisfy maximal consistent sets of candidate constraint modules sets.
** Declaration of Constraint Hierarchies [#oc2bb594]
- In a declaration, we declare constraints with priorities between them.
- The operator ''$<<$'' describes a weak composition of constraints. For example,
$A << B$ means that the constraint A is weaker than B.
-If we declare a constraint without ''$<<$'', it means that there is no priority about the constraint.
- The operator ''$<<$'' has a higher precedence than ''$,$'', that is, $A, B << C$ is equivalent to $A, (B << C)$.
- The unit of constraints
that is declared with a priority is called a module or a constraint module.
- Meaning of a HydLa program is a set of trajectories that satisfy maximal consistent sets of candidate constraint modules sets at each time point.
- Each candidate constraint set must satisfy conditions below:~
#mathjax
\[\forall M_1, M_2((M_1 \ll M_2 \land M_1 \in {MS} \,) \Rightarrow M_2 \in {MS}\,)\]
\[\forall M (\neg \exists ( R \ll M ) \Rightarrow R \in {MS} \,)\]
#norelated
*** Equality [#i272cd72]
- The "," operator means that these two constraints(constraint1,constraint2) are equivalent.
>
constriant1 , 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
<
*** Precedence [#x04d90de]
- The "<<" operator has a higher precedence than the "," operator.
- Example:
>
constraint1 , constraint2 , constraint3 << constraint4.
<
- is equal to
>
constraint1 , constraint2 , (constraint3 << constraint4).
<
- not equal to
>
(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 }.
<
* 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.
<
- 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.
<
- 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).
<
- 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'-).
<
- 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.
<
* Advanced 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_definition .
<
example : Define the constraint that The variables(x,y,z) in constant
>
~ CONST(a) <=> [](a'=0).
~ ...
~ CONST(x),CONST(y),CONST(z),...
<
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 } .
<
example : Make some constraint together.
>
~ INITS { INIT(x1), INIT(x2), INIT(x3) }.
~ INITS, ...
<
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]
** List Comprehension [#eea12551]
- The set of some variables can be used.
- The syntax of the set is some way.
>
set_name := set .
<
- Example of Defining
>
~ es := {e1, e2, e3, e4}.
~ ten := { i | i in {0..9} }.
~ xten := {x1..x10} .
<
- The calculation of sets
>
~ 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 }
<
** Assert Statement[#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 }.
<
** Tips [#jb66d45b]
- As the special values , Napier's constant "E" and Pi "Pi"(the ratio of circumference to diameter) can be used too.
*** Special function [#w69ae32d]
- Trigonometric functions
>
~ sin(x)
~ cos(x)
~ tan(x)
~ asin(x)
~ acos(x)
~ atan(x)
<
