1 files changed, 36 insertions, 5 deletions

diff --git a/frontend/parser.mly b/frontend/parser.mly
index 51974d1..fb00478 100644
--- a/frontend/parser.mly
+++ b/frontend/parser.mly
@@ -1,5 +1,6 @@
 %{
 open Ast
+open Util
 %}
 
 %token BOOL INT REAL
@@ -12,6 +13,7 @@ open Ast
 %token VAR LET TEL
 %token PRE
 %token ASSUME GUARANTEE
+%token AUTOMATON STATE INITIAL UNTIL UNLESS RESUME
 
 %token LPAREN RPAREN
 %token LCURLY RCURLY
@@ -57,12 +59,12 @@ primary_expr:
 | TRUE                      { AST_bool_const true }
 | FALSE                     { AST_bool_const false }
 | e=ext(IDENT) LPAREN l=separated_list(COMMA,ext(expr)) RPAREN 
-                            { AST_instance (e, l) }
+                            { AST_instance (e, l, fst e ^ uid ()) }
 
 unary_expr:
 | e=primary_expr                   { e }
 | NOT e=ext(unary_expr)            { AST_not(e) }
-| PRE e=ext(unary_expr)            { AST_pre(e) }
+| PRE e=ext(unary_expr)            { AST_pre(e, "pre"^uid()) }
 | o=unary_op e=ext(unary_expr)     { AST_unary (o, e) }
 
 %inline unary_op:
@@ -103,23 +105,52 @@ expr:
 
 
 (* Equations (can be asserts, automata, ...) *)
+automaton:
+| AUTOMATON a=IDENT? s=list(ext(state)) RETURNS r=separated_list(COMMA, IDENT)
+    { ((match a with Some n -> n | None -> "aut") ^ uid (), s, r) }
+
+state:
+| i=boption(INITIAL) STATE n=IDENT
+  unless=trans(UNLESS)
+  v=option(var_decl)
+  b=body
+  until=trans(UNTIL)
+{ if unless <> [] then failwith "UNLESS transitions not supported.";
+  { initial = i;
+    name = n;
+    locals = (match v with Some v -> v | None -> []);
+    body = b;
+    until = until;
+} }
+
+trans(TT):
+| TT t=nonempty_list(terminated(transition, SEMICOLON))   { t }
+|                                                         { [] }
+
+transition:
+| IF e=ext(expr) RESUME s=ext(IDENT)                      { (e, s) }
+
+
 eqn:
 | i=separated_list(COMMA, ext(IDENT)) EQUAL e=ext(expr)         
                                                 { AST_assign(i, e) }
 | ASSUME i=ext(IDENT) COLON e=ext(expr)         { AST_assume(i, e) }
 | GUARANTEE i=ext(IDENT) COLON e=ext(expr)      { AST_guarantee(i, e) }
+| a=automaton                                   { AST_automaton(a) }
 
 typ:
 | INT                                           { AST_TINT }
 | BOOL                                          { AST_TBOOL }
 | REAL                                          { AST_TREAL }
-| LPAREN l=separated_list(COMMA, typ) RPAREN    { AST_TGROUP(l) }
 
 (* Declarations *)
 dbody:
 | e=ext(eqn) SEMICOLON                          { [e] }
+| l=body                                        { l }
+
+body:
 | LET l=nonempty_list(terminated(ext(eqn), SEMICOLON)) TEL
-                                                { l }
+  { l }
 
 var:
 |   p=boption(PROBE) i=ext(IDENT)   { (p, i) }
@@ -157,7 +188,7 @@ node_decl:
 | NODE id=IDENT LPAREN v=vars RPAREN
     RETURNS LPAREN rv=vars RPAREN
     lv=var_decl
-    LET b=nonempty_list(terminated(ext(eqn), SEMICOLON)) TEL
+    b=body
 { { name = id;
     args = v;
     ret = rv;