Syntax

Syntax †

  • The abstract syntax of HydLa is given in the following BNF.
    HydLa-syntax.png

  • The concrete syntax uses the symbols in the following table.
    HydLa-symbols.png

  • A HydLa program consists of definitions of constraints and declarations of constraint hierarchies, each of which is described below.
↑

Definition †

  • 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.
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.
  • "$\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 †

  • 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 R (\neg \exists M( R \ll M ) \Rightarrow R \in {MS} \,)\]

↑

List Comprehension †

  • In the modeling of hybrid systems, we often come across necessity to introduce multiple similar objects.
  • 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 †

  • 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 †

  • 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 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 †

  • 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 †

  • 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 $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$
↑

Built-in Constants and Functions †

  • 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}

Last-modified: 2021-02-25 (Thu) 06:51:23 (1149d)