• The abstract syntax of HydLa is given in the following BNF.
  • A HydLa program consists of definitions of constraints and declarations of constraint hierarchies.


  • 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

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

\[\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

  • In 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.

Priority List

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

Expression List

  • The second of list is expression lists, that is, 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

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

Other Notations

  • The n-th $\texttt{(n > 0)}$ element of a list $\texttt{L}$ can be accessed by $\texttt{L[n]}$.
    • 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}$


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







  • Detailed syntax and semantics can be found here.
Last-modified: 2019-06-10 (Mon) 06:16:55 (468d)