- some steps towards integration of automata

src/automata.ml

@@ -9,6 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
+open Utils
 open LustreSpec
 open Corelang
 
@@ -18,18 +19,20 @@ let mkbool loc b =
 let mkident loc id =
  mkexpr loc (Expr_ident id)
 
-let init (loc, restart, st) =
+let init loc restart st =
  mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st])
 
-let add_branch expr (loc, restart, st) cont =
- mkexpr loc (Expr_ite (expr, init (loc, restart, st), cont))
+let add_branch (loc, expr, restart, st) cont =
+ mkexpr loc (Expr_ite (expr, init loc restart st, cont))
 
-let mkhandler loc st unless until locals eqs =
+let mkhandler loc st unless until locals (eqs, asserts, annots) =
  {hand_state = st;
   hand_unless = unless;
   hand_until = until;
   hand_locals = locals;
   hand_eqs = eqs;
+  hand_asserts = asserts;
+  hand_annots = annots;
   hand_loc = loc}
 
 let mkautomata loc id handlers =
@@ -37,16 +40,43 @@ let mkautomata loc id handlers =
    aut_handlers = handlers;
    aut_loc = loc}
 
+let node_of_handler loc id inputs outputs handler =
+ Node {
+   node_id = id;
+   node_type = Types.new_var ();
+   node_clock = Clocks.new_var true;
+   node_inputs = inputs;
+   node_outputs = outputs;
+   node_locals = handler.hand_locals;
+   node_gencalls = [];
+   node_checks = [];
+   node_asserts = handler.hand_asserts; 
+   node_eqs = handler.hand_eqs;
+   node_dec_stateless = false;
+   node_stateless = None;
+   node_spec = None;
+   node_annot = handler.hand_annots
+ }
+
+let handler_read handler =
+ List.fold_left (fun read eq -> get_expr_vars read eq.eq_rhs) ISet.empty handler.hand_eqs
+
+let handler_write handler =
+ List.fold_left (fun write eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs) ISet.empty handler.hand_eqs
+
+let expr_of_exit_conditions loc st conds =
+ List.fold_right add_branch conds (init loc false st)
+
 let pp_restart fmt restart =
   Format.fprintf fmt "%s" (if restart then "restart" else "resume")
 
-let pp_unless fmt (expr, restart, st) =
+let pp_unless fmt (_, expr, restart, st) =
   Format.fprintf fmt "unless %a %a %s"
     Printers.pp_expr expr
     pp_restart restart
     st
 
-let pp_until fmt (expr, restart, st) =
+let pp_until fmt (_, expr, restart, st) =
   Format.fprintf fmt "until %a %a %s"
     Printers.pp_expr expr
     pp_restart restart

src/causality.ml

@@ -532,7 +532,7 @@ let merge_with g1 g2 =
   end
 
 let add_external_dependency outputs mems g =
-  let caller ="!_world" in
+  let caller ="!!_world" in
   begin
     IdentDepGraph.add_vertex g caller;
     ISet.iter (fun o -> IdentDepGraph.add_edge g caller o) outputs;

src/corelang.ml

@@ -891,6 +891,25 @@ and get_eq_calls nodes eq =
 and get_node_calls nodes node =
   List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty node.node_eqs
 
+let rec get_expr_vars vars e =
+  get_expr_desc_vars vars e.expr_desc
+and get_expr_desc_vars vars expr_desc =
+  match expr_desc with
+  | Expr_const _ -> vars
+  | Expr_ident x -> Utils.ISet.add x vars
+  | Expr_tuple el
+  | Expr_array el -> List.fold_left get_expr_vars vars el
+  | Expr_pre e1 -> get_expr_vars vars e1
+  | Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1 
+  | Expr_access (e1, d) 
+  | Expr_power (e1, d)   -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d]
+  | Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e]
+  | Expr_arrow (e1, e2) 
+  | Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2]
+  | Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl
+  | Expr_appl (_, arg, None)   -> get_expr_vars vars arg
+  | Expr_appl (_, arg, Some (r,_)) -> get_expr_vars (Utils.ISet.add r vars) arg
+
 
 let rec expr_has_arrows e =
   expr_desc_has_arrows e.expr_desc

src/corelang.mli

@@ -108,6 +108,7 @@ val get_typedefs: program -> top_decl list
 val get_dependencies : program -> top_decl list
 (* val prog_unfold_consts: program -> program *)
 
+val get_expr_vars: Utils.ISet.t -> expr -> Utils.ISet.t
 val expr_replace_var: (ident -> ident) -> expr -> expr
 val eq_replace_rhs_var: (ident -> bool) -> (ident -> ident) -> eq -> eq
 

src/lustreSpec.ml

@@ -144,10 +144,12 @@ type automata_desc =
 
 and handler_desc =
   {hand_state: ident;
-   hand_unless: (expr * bool * ident) list;
-   hand_until: (expr * bool * ident) list;
+   hand_unless: (Location.t * expr * bool * ident) list;
+   hand_until: (Location.t * expr * bool * ident) list;
    hand_locals: var_decl list;
    hand_eqs: eq list;
+   hand_asserts: assert_t list;
+   hand_annots: expr_annot list;
    hand_loc: Location.t}
 
 type statement =

src/parser_lustre.mly

@@ -259,30 +259,30 @@ eq_list:
 | automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
 
 automaton:
- AUTOMATON type_ident handler_list { failwith "not implemented" }
+ AUTOMATON type_ident handler_list { (Automata.mkautomata (get_loc ()) $2 $3); failwith "not implemented" }
 
 handler_list:
      { [] }
 | handler handler_list { $1::$2 }
 
 handler:
- STATE UIDENT ARROW unless_list locals LET eq_list TEL until_list { () }
+ STATE UIDENT ARROW unless_list locals LET eq_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }
 
 unless_list:
-    { Automata.init }
-| unless unless_list { let (expr1, case1) = $1 in (fun case -> Automata.add_branch expr1 case1 ($2 case)) }
+    { [] }
+| unless unless_list { $1::$2 }
 
 until_list:
-    { Automata.init }
-| until until_list { let (expr1, case1) = $1 in (fun case -> Automata.add_branch expr1 case1 ($2 case)) }
+    { [] }
+| until until_list { $1::$2 }
 
 unless:
-  UNLESS expr RESTART UIDENT { ($2, (get_loc (), true, $4))  }
-| UNLESS expr RESUME UIDENT  { ($2, (get_loc (), false, $4)) }
+  UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
+| UNLESS expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
 
 until:
-  UNTIL expr RESTART UIDENT { ($2, (get_loc (), true, $4))  }
-| UNTIL expr RESUME UIDENT  { ($2, (get_loc (), false, $4)) }
+  UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
+| UNTIL expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
 
 assert_:
 | ASSERT expr SCOL {mkassert ($2)}