HydLaWiki
Syntax
Start:
#noattach
#mathjax
#norelated
* Syntax [#r2da58d9]
- The abstract syntax of HydLa is given in the following ...
//#ref(./HydLa_BNF.png, center);
#ref(./HydLa-syntax.png,center,80%);
~
- The concrete syntax uses the symbols in the following t...
#ref(./HydLa-symbols.png,center,50%);
~
- A HydLa program consists of '''definitions of constrain...
** Definition [#s649ac18]
- A definition allows us to define a named constraint wit...
If the definition has no arguments, we can omit parenthes...
INIT <=> y = 0 & y' = 0. // definition of a constraint ...
FALL <=> [](y'' = -10). // definition of a constraint ...
BOUNCE(x) <=> [](x- = 0 => x' = -x'-). // definition of...
BALL{FALL << BOUNCE}. // definition of a constraint hier...
- '''Constraints''' allow conjunctions of constraints and...
- The antecedents of implications are called '''guards'''.
- "$\texttt{[]}$" (called '''box''' or '''always''') is a...
- A variable name ($\textit{vname}$) starts with a lowerc...
- The notation $\textit{vname}′$ means the derivative of ...
** Declaration of Constraint Hierarchies [#oc2bb594]
- A constraint can be given higher or lower priority than...
- The declaration $A \mathrel{\texttt{<<}} B$ states that...
-If we compose constraints with "$\texttt{,}$" instead of...
- The operator "$\texttt{<<}$" has a higher precedence th...
- The unit of constraints declared with a priority is cal...
- The meaning of a HydLa program is a set of trajectories...
- Each candidate constraint set must satisfy the conditio...
\[\forall M_1, M_2((M_1 \ll M_2 \land M_1 \in {MS} \,) \R...
\[\forall R (\neg \exists M( R \ll M ) \Rightarrow R \i...
** List Comprehension [#eea12551]
- In the modeling of hybrid systems, we often come across...
multiple similar objects.
- HydLa provides list comprehention to describe models wi...
- A list can be defined by the operator "$\texttt{:=}$", ...
- There are two types of lists: priority lists and expres...
*** Priority List [#rb9d66d1]
- The first type, priority lists, can be denoted by an ex...
$\{\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, ..., \t...
-- For example, $\{\texttt{INIT(i)}\ |\ \texttt{i in \{1,...
-- If a HydLa program includes declarations of priority l...
is equivalent to $A, B, C$.
*** Expression List [#c1744645]
- The second type, expression lists, are lists of arithme...
-- We can denote an expression list in an extensional or...
as well as a priority list.
-- In addition, we can use range expressions of the form ...
*** Examples [#b3820221]
- An expression list $\verb|{1*2 + 1..5}|$ is equivalent ...
- An expression list $\verb/{j | i in {1,2}, j in {i+1..4...
- An expression list $\verb|{x1..x3}|$ is equivalent to $...
*** Other Notations [#mc029821]
- The $n$-th $(n > 0)$ element of a list $L$ can be acces...
-- The index allows an arbitrary expression that results ...
- The size of a list $L$ is denoted by $\texttt{|}L\textt...
- $\texttt{sum(}L\texttt{)}$ is a syntactic sugar of the ...
** Built-in Constants and Functions [#jb66d45b]
- Napier's constant "$\texttt{E}$" and the ratio of circu...
- The following mathematical functions are available. No...
\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://...
End:
#noattach
#mathjax
#norelated
* Syntax [#r2da58d9]
- The abstract syntax of HydLa is given in the following ...
//#ref(./HydLa_BNF.png, center);
#ref(./HydLa-syntax.png,center,80%);
~
- The concrete syntax uses the symbols in the following t...
#ref(./HydLa-symbols.png,center,50%);
~
- A HydLa program consists of '''definitions of constrain...
** Definition [#s649ac18]
- A definition allows us to define a named constraint wit...
If the definition has no arguments, we can omit parenthes...
INIT <=> y = 0 & y' = 0. // definition of a constraint ...
FALL <=> [](y'' = -10). // definition of a constraint ...
BOUNCE(x) <=> [](x- = 0 => x' = -x'-). // definition of...
BALL{FALL << BOUNCE}. // definition of a constraint hier...
- '''Constraints''' allow conjunctions of constraints and...
- The antecedents of implications are called '''guards'''.
- "$\texttt{[]}$" (called '''box''' or '''always''') is a...
- A variable name ($\textit{vname}$) starts with a lowerc...
- The notation $\textit{vname}′$ means the derivative of ...
** Declaration of Constraint Hierarchies [#oc2bb594]
- A constraint can be given higher or lower priority than...
- The declaration $A \mathrel{\texttt{<<}} B$ states that...
-If we compose constraints with "$\texttt{,}$" instead of...
- The operator "$\texttt{<<}$" has a higher precedence th...
- The unit of constraints declared with a priority is cal...
- The meaning of a HydLa program is a set of trajectories...
- Each candidate constraint set must satisfy the conditio...
\[\forall M_1, M_2((M_1 \ll M_2 \land M_1 \in {MS} \,) \R...
\[\forall R (\neg \exists M( R \ll M ) \Rightarrow R \i...
** List Comprehension [#eea12551]
- In the modeling of hybrid systems, we often come across...
multiple similar objects.
- HydLa provides list comprehention to describe models wi...
- A list can be defined by the operator "$\texttt{:=}$", ...
- There are two types of lists: priority lists and expres...
*** Priority List [#rb9d66d1]
- The first type, priority lists, can be denoted by an ex...
$\{\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, ..., \t...
-- For example, $\{\texttt{INIT(i)}\ |\ \texttt{i in \{1,...
-- If a HydLa program includes declarations of priority l...
is equivalent to $A, B, C$.
*** Expression List [#c1744645]
- The second type, expression lists, are lists of arithme...
-- We can denote an expression list in an extensional or...
as well as a priority list.
-- In addition, we can use range expressions of the form ...
*** Examples [#b3820221]
- An expression list $\verb|{1*2 + 1..5}|$ is equivalent ...
- An expression list $\verb/{j | i in {1,2}, j in {i+1..4...
- An expression list $\verb|{x1..x3}|$ is equivalent to $...
*** Other Notations [#mc029821]
- The $n$-th $(n > 0)$ element of a list $L$ can be acces...
-- The index allows an arbitrary expression that results ...
- The size of a list $L$ is denoted by $\texttt{|}L\textt...
- $\texttt{sum(}L\texttt{)}$ is a syntactic sugar of the ...
** Built-in Constants and Functions [#jb66d45b]
- Napier's constant "$\texttt{E}$" and the ratio of circu...
- The following mathematical functions are available. No...
\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://...
Page:
