# Backup diff of Syntax (No. 1)

- List of Backups
- View the diff current.
- View the source.
- Go to Syntax.
*1 (2016-06-29 (Wed) 05:13:03)*- 2 (2017-03-02 (Thu) 03:21:30)
- 3 (2017-03-17 (Fri) 02:49:00)
- 4 (2017-03-17 (Fri) 09:00:40)
- 5 (2017-03-23 (Thu) 05:43:54)

- The added line is THIS COLOR.
- The deleted line is THIS COLOR.

// 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) < *** 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. - Each candidate constraint set must satisfy conditions below.~ -- ∀M1, ∀M2(M1<< M2 ∧ M1 ∈ MS ⇒ M2 ∈ MS) -- ∀M(¬(∃S.M << S) ⇒ M ∈ MS) *** 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] - 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 } < *** Special function [#w69ae32d] - The trigonometric function > ~ sin(x) ~ cos(x) ~ tan(x) < - inverse trigonometric function > ~ asin(x) ~ acos(x) ~ atan(x) <