- The added line is THIS COLOR.
- The deleted line is THIS COLOR.
#author("2017-03-23T14:43:54+09:00","default:Uedalab","Uedalab")
#author("2021-02-25T15:51:23+09:00","default:Uedalab","Uedalab")
#noattach
#mathjax
#norelated
* Syntax [#r2da58d9]
- The abstract syntax of HydLa is given in the following BNF.
#ref(./HydLa_BNF.png, center);
- A HydLa program consists of definitions of constraints and declarations of constraint hierarchies.
//#ref(./HydLa_BNF.png, center);
#ref(./HydLa-syntax.png,center,80%);
~
- The concrete syntax uses the symbols in the following table.
#ref(./HydLa-symbols.png,center,50%);
~
- A HydLa program consists of '''definitions of constraints''' and '''declarations of constraint hierarchies''', each of which is described below.
** Definition [#s649ac18]
- In a definition, we define a named constraint or a named constraint hierarchies with arguments using the operator " ''<=>'' ".
- A definition allows us to define a named constraint with arguments using the operator "$\texttt{<=>}$". It allows us to define a named constraint hierarchies as well.
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.
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.
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$.
- '''Constraints''' allow conjunctions of constraints and implications.
- The antecedents of implications are called '''guards'''.
- "$\texttt{[]}$" (called '''box''' or '''always''') is a temporal operator which means that the constraint always holds from the time point at which the constraint is enabled.
- A variable name ($\textit{vname}$) starts with a lowercase letter.
- The notation $\textit{vname}′$ means the derivative of $\textit{vname}$, and $\textit{vname}\verb|−|$ means the left-hand limit of $\textit{vname}$.
** Declaration of Constraint Hierarchies [#oc2bb594]
- In a declaration, we declare constraints with priorities between them.
- The operator "$<<$" is a concrete notation of the operator "$\ll$" and it 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:~
- A constraint can be given higher or lower priority than another.
- The declaration $A \mathrel{\texttt{<<}} B$ states that the constraint A is weaker (i.e., of lower priority) than B. The relation $A \mathrel{\texttt{<<}} B$ is a strict partial order which is irreflexive, transitive and asymmetric.
-If we compose constraints with "$\texttt{,}$" instead of "$\texttt{<<}$", there is ordering between them.
- The operator "$\texttt{<<}$" has a higher precedence than "$,$", that is, $A, B \mathrel{\texttt{<<}} C$ is equivalent to $A, (B \mathrel{\texttt{<<}} C)$.
- The unit of constraints declared with a priority is called a '''module''' or a '''constraint module'''.
- The 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 the 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} \,)\]
\[\forall R (\neg \exists M( R \ll M ) \Rightarrow R \in {MS} \,)\]
** List Comprehension [#eea12551]
- In modeling of hybrid systems, we often come across necessity to introduce
- In the modeling of hybrid systems, we often come across necessity to introduce
multiple similar objects.
- HydLa allows a list comprehention to easily describe models with multiple objects.
- A list can be defined by the operator "$:=$", like $\texttt{X := {x0..x9}.}$
- There are a two types of lists: priority lists and expression lists.
- HydLa provides list comprehention to describe models with multiple objects.
- A list can be defined by the operator "$\texttt{:=}$", like $\texttt{X := {x0..x9}.}$
- There are two types of lists: priority lists and expression lists.
*** Priority List [#rb9d66d1]
- The first type of lists is priority lists.
-- A priority list can be denoted by an extensional notation of the following form.
>
$\{MP_1, MP_2, ..., MP_n\}$
<
-- It also can be denoted by an intensionally
>
$\{MP | LC_1, LC_2, ..., LC_n\}$
<
-- For example, $\{\texttt{INIT(i)}\ |\ \texttt{i in \{1,2,3,4\}}\}$ is equivalent to $\{\texttt{INIT(1),INIT(2),INIT(3),INIT(4)}\}$
-- If a HydLa program includes declarations of priority lists, the elements of the lists are expanded, that is, a declaration of $\{\texttt{A, B, C}\}$
is equivalent to $\texttt{A, B, C}$.
- The first type, priority lists, can be denoted by an extensional form
$\{\textit{MP}_1, \textit{MP}_2, ..., \textit{MP}_n\}$.
-- They also can be denoted intensionally as
$\{\textit{MP} \mid \textit{LC}_1, \textit{LC}_2, ..., \textit{LC}_n\}$.
-- For example, $\{\texttt{INIT(i)}\ |\ \texttt{i in \{1,2,3,4\}}\}$ is equivalent to $\{\texttt{INIT(1)}$, $\texttt{INIT(2)}$, $\texttt{INIT(3)}$, $\texttt{INIT(4)}\}$.
-- If a HydLa program includes declarations of priority lists, the elements of the lists are expanded, that is, a declaration of $\{A, B, C\}$
is equivalent to $A, B, C$.
*** Expression List [#c1744645]
- The second of list is expression lists, that is, lists of arithmetic expressions.
- The second type, expression lists, are lists of arithmetic expressions.
-- We can denote an expression list in an extensional or intensional notation
as well as a priority list.
-- In addition, we can use range expressions in the following form.
>
$\{RE .. RE\}$.
<
-- $RE$ is an arithmetic expression without variables or an arithmetic expression with a variable whose name terminates with a number such as x0 and y1.
*** Example of Lists [#b3820221]
- An expression list $\{1*2+1..5\}$ is equivalent to $\{3,4,5\}$.
- An expression list $\{\texttt{j | i in \{1,2\}, j in \{i+1..4\}}\}$ is equivalent to $\{2,3,4,3,
4\}$.
- An expression list $\{\texttt{x1..x3}\}$ is equivalent to $\{\texttt{x1, x2, x3}\}$.
-- In addition, we can use range expressions of the form $\{\textit{RE} \texttt{..} \textit{RE}\,\}$, where $\textit{RE}$ is an arithmetic expression without variables or an arithmetic expression with a variable whose name terminates with a number such as $\texttt{x0}$ and $\texttt{y1}$.
*** Examples [#b3820221]
- An expression list $\verb|{1*2 + 1..5}|$ is equivalent to $\verb|{3,4,5}|$.
- An expression list $\verb/{j | i in {1,2}, j in {i+1..4}}/$ is equivalent to $\verb|{2,3,4,3,4}|$.
- An expression list $\verb|{x1..x3}|$ is equivalent to $\verb|{x1,x2,x3}|$.
*** Other Notations [#mc029821]
- The n-th element of a list $\texttt{L}$ can be accessed by $\texttt{L[n]}$.
- The $n$-th $(n > 0)$ element of a list $L$ can be accessed by $L\texttt{[}n\texttt{]}$.
-- The index allows an arbitrary expression that results in an integer.
- The size of a list $\texttt{L}$ is denoted by $\texttt{|L|}$, which can be used as a constant value in a HydLa program.
- $\texttt{sum(L)}$ is a syntactic sugar of the sum of the elements in an expression list $\texttt{L}$
- The size of a list $L$ is denoted by $\texttt{|}L\texttt{|}$, which can be used as a constant value in a HydLa program.
- $\texttt{sum(}L\texttt{)}$ is a syntactic sugar of the sum of the elements in an expression list $L$
** Tips [#jb66d45b]
- Napier's constant "E" and the ratio of circumference to diameter "Pi" also can be used as constant values.
- The following trigonometric functions are available.
>
~ sin(x)
~ cos(x)
~ tan(x)
~ asin(x)
~ acos(x)
~ atan(x)
<
- Detailed syntax and semantics can be found [http://www.ueda.info.waseda.ac.jp/~matsusho/public/dissertation.pdf here].
** Built-in Constants and Functions [#jb66d45b]
- Napier's constant "$\texttt{E}$" and the ratio of circumference to diameter "$\texttt{Pi}$" can be used as constant values.
- The following mathematical functions are available. Note that $\texttt{Sqrt(}x\texttt{)}$ and $\texttt{Exp(}x\texttt{)}$ are missing because they can be expressed as $x\verb|^(1/2)|$ and $\verb|E^|x$, respectively.
\begin{align}
&\texttt{Log(}x\texttt{)}\\
&\texttt{Sin(}x\texttt{)}, \texttt{Cos(}x\texttt{)},
\texttt{Tan(}x\texttt{)}, \texttt{Asin(}x\texttt{)},
\texttt{Acos(}x\texttt{),} \texttt{Atan(}x\texttt{)}\\
&\texttt{Sinh(}x\texttt{)}, \texttt{Cosh(}x\texttt{)},
\texttt{Tanh(}x\texttt{)}, \texttt{Asinh(}x\texttt{)},
\texttt{Acosh(}x\texttt{)}, \texttt{Atanh(}x\texttt{)}\\
&\texttt{Floor(}x\texttt{)}
\end{align}
- Detailed syntax and semantics can be found in [https://doi.org/10.1007/978-3-030-41131-2_8 this comprehensive paper] and [http://www.ueda.info.waseda.ac.jp/~matsusho/public/dissertation.pdf this PhD thesis].
