module_ident |
UIDENT |
|
IDENT |
tag_ident |
UIDENT |
|
TRUE |
|
FALSE |
node_ident |
UIDENT |
|
IDENT |
node_ident_decl |
node_ident |
vdecl_ident |
UIDENT |
|
IDENT |
const_ident |
UIDENT |
|
IDENT |
type_ident |
IDENT |
prog |
open_lusi
typ_def_prog
top_decl
EOF |
typ_def_prog |
typ_def
SCOL |
header |
open_lusi
typ_def_header
top_decl_header
EOF |
typ_def_header |
typ_def
SCOL |
open_lusi |
OPEN
QUOTE
module_ident
QUOTE |
|
OPEN
LT
module_ident
GT |
state_annot |
FUNCTION |
|
NODE |
top_decl_header |
CONST
cdecl_list |
|
NODESPEC
state_annot
node_ident
LPAR
vdecl+SCOL
SCOL
RPAR
RETURNS
LPAR
vdecl+SCOL
SCOL
RPAR
PROTOTYPE
node_ident
LIB
module_ident
SCOL |
top_decl |
CONST
cdecl_list |
|
NODESPEC
state_annot
node_ident_decl
LPAR
vdecl+SCOL
SCOL
RPAR
RETURNS
LPAR
vdecl+SCOL
SCOL
RPAR
SCOL
VAR
local_vdecl_list
SCOL
LET
stmt_list
TEL |
typ_def |
TYPE
type_ident
EQ
typ_def_rhs |
typ_def_rhs |
typeconst |
|
ENUM
LCUR
UIDENT+COMMA
RCUR |
|
STRUCT
LCUR
IDENT
COL
typeconst
SCOL
RCUR |
typeconst |
TINT
POWER
dim |
|
TBOOL
POWER
dim |
|
TREAL
POWER
dim |
|
type_ident
POWER
dim |
|
TBOOL
TCLOCK |
|
IDENT
TCLOCK |
stmt_list |
epsilon
|
|
eq
stmt_list |
|
assert_
stmt_list |
|
ANNOT
stmt_list |
|
automaton
stmt_list |
automaton |
AUTOMATON
type_ident
handler |
handler |
STATE
UIDENT
COL
unless
VAR
local_vdecl_list
SCOL
LET
stmt_list
TEL
until |
unless |
UNLESS
expr
RESTART
UIDENT |
|
UNLESS
expr
RESUME
UIDENT |
until |
UNTIL
expr
RESTART
UIDENT |
|
UNTIL
expr
RESUME
UIDENT |
assert_ |
ASSERT
expr
SCOL |
eq |
vdecl_ident+COMMA
EQ
expr
SCOL |
|
LPAR
vdecl_ident+COMMA
RPAR
EQ
expr
SCOL |
lustre_spec |
contract
EOF |
contract |
REQUIRES
qexpr
SCOL
ensures
BEHAVIOR
IDENT
COL
assumes
ensures |
ensures |
epsilon
|
|
ENSURES
qexpr
SCOL
ensures |
|
OBSERVER
node_ident
LPAR
tuple_expr
RPAR
SCOL
ensures |
tuple_qexpr |
qexpr
COMMA
qexpr |
|
tuple_qexpr
COMMA
qexpr |
qexpr |
expr |
|
EXISTS
vdecl
SCOL
qexpr |
|
FORALL
vdecl
SCOL
qexpr |
tuple_expr |
expr
COMMA
expr |
|
tuple_expr
COMMA
expr |
expr |
INT |
|
REAL |
|
STRING |
|
IDENT |
|
tag_ident |
|
LPAR
ANNOT
expr
RPAR |
|
LPAR
expr
RPAR |
|
LPAR
tuple_expr
RPAR |
|
LBRACKET
expr+COMMA
RBRACKET |
|
expr
POWER
dim |
|
expr
LBRACKET
dim
RBRACKET+LBRACKET |
|
PRE
expr |
|
expr
ARROW
expr |
|
expr
FBY
expr |
|
expr
WHEN
vdecl_ident |
|
expr
WHENNOT
vdecl_ident |
|
expr
WHEN
tag_ident
LPAR
vdecl_ident
RPAR |
|
MERGE
vdecl_ident
handler_expr |
|
node_ident
LPAR
expr
RPAR |
|
node_ident
LPAR
expr
RPAR
EVERY
expr |
|
node_ident
LPAR
tuple_expr
RPAR |
|
node_ident
LPAR
tuple_expr
RPAR
EVERY
expr |
|
expr
AND
expr |
|
expr
AMPERAMPER
expr |
|
expr
OR
expr |
|
expr
BARBAR
expr |
|
expr
XOR
expr |
|
NOT
expr |
|
expr
IMPL
expr |
|
expr
EQ
expr |
|
expr
LT
expr |
|
expr
LTE
expr |
|
expr
GT
expr |
|
expr
GTE
expr |
|
expr
NEQ
expr |
|
expr
PLUS
expr |
|
expr
MINUS
expr |
|
expr
MULT
expr |
|
expr
DIV
expr |
|
MINUS
expr |
|
expr
MOD
expr |
|
IF
expr
THEN
expr
ELSE
expr |
handler_expr |
LPAR
tag_ident
ARROW
expr
RPAR |
signed_const |
INT |
|
REAL |
|
tag_ident |
|
MINUS
INT |
|
MINUS
REAL |
|
LCUR
IDENT
EQ
signed_const+COMMA
RCUR |
|
LBRACKET
signed_const+COMMA
RBRACKET |
dim |
INT |
|
LPAR
dim
RPAR |
|
UIDENT |
|
IDENT |
|
dim
AND
dim |
|
dim
AMPERAMPER
dim |
|
dim
OR
dim |
|
dim
BARBAR
dim |
|
dim
XOR
dim |
|
NOT
dim |
|
dim
IMPL
dim |
|
dim
EQ
dim |
|
dim
LT
dim |
|
dim
LTE
dim |
|
dim
GT
dim |
|
dim
GTE
dim |
|
dim
NEQ
dim |
|
dim
PLUS
dim |
|
dim
MINUS
dim |
|
dim
MULT
dim |
|
dim
DIV
dim |
|
MINUS
dim |
|
dim
MOD
dim |
|
IF
dim
THEN
dim
ELSE
dim |
vdecl |
vdecl_ident+COMMA
COL
typeconst
when_cond*epsilon
|
|
CONST
vdecl_ident+COMMA |
|
CONST
vdecl_ident+COMMA
COL
typeconst |
local_vdecl |
vdecl_ident+COMMA |
|
vdecl_ident+COMMA
COL
typeconst
when_cond*epsilon
|
|
CONST
vdecl_ident
EQ
expr |
|
CONST
vdecl_ident
COL
typeconst
EQ
expr |
cdecl_list |
cdecl
SCOL |
|
cdecl
cdecl_list
SCOL |
cdecl |
const_ident
EQ
signed_const |
when_cond |
WHEN
IDENT |
|
WHENNOT
IDENT |
|
WHEN
tag_ident
LPAR
IDENT
RPAR |
lustre_annot |
lustre_annot_list
EOF |
lustre_annot_list |
epsilon
|
|
DIV+IDENT
COL
qexpr
SCOL
lustre_annot_list |
|
IDENT
COL
qexpr
SCOL
lustre_annot_list |
|
INVARIANT
COL
qexpr
SCOL
lustre_annot_list |
|
OBSERVER
COL
qexpr
SCOL
lustre_annot_list |
|
CCODE
COL
qexpr
SCOL
lustre_annot_list |
|
MATLAB
COL
qexpr
SCOL
lustre_annot_list |