#author("2017-03-17T18:00:40+09:00","default:Uedalab","Uedalab")
#noattach
#mathjax
#norelated
* Syntax [#r2da58d9]
#ref(./HydLa_BNF.png, center);
- A HydLa program consists of definitions of constraints and declarations of constraint hierarchies.
** Definition [#s649ac18]
- 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$.
** 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:~
\[\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} \,)\]
** 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)
<
