Project

General

Profile

Revision 29ced7be

View differences:

src/automata.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12
open Utils
12 13
open LustreSpec
13 14
open Corelang
14 15

  
......
18 19
let mkident loc id =
19 20
 mkexpr loc (Expr_ident id)
20 21

  
21
let init (loc, restart, st) =
22
let init loc restart st =
22 23
 mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st])
23 24

  
24
let add_branch expr (loc, restart, st) cont =
25
 mkexpr loc (Expr_ite (expr, init (loc, restart, st), cont))
25
let add_branch (loc, expr, restart, st) cont =
26
 mkexpr loc (Expr_ite (expr, init loc restart st, cont))
26 27

  
27
let mkhandler loc st unless until locals eqs =
28
let mkhandler loc st unless until locals (eqs, asserts, annots) =
28 29
 {hand_state = st;
29 30
  hand_unless = unless;
30 31
  hand_until = until;
31 32
  hand_locals = locals;
32 33
  hand_eqs = eqs;
34
  hand_asserts = asserts;
35
  hand_annots = annots;
33 36
  hand_loc = loc}
34 37

  
35 38
let mkautomata loc id handlers =
......
37 40
   aut_handlers = handlers;
38 41
   aut_loc = loc}
39 42

  
43
let node_of_handler loc id inputs outputs handler =
44
 Node {
45
   node_id = id;
46
   node_type = Types.new_var ();
47
   node_clock = Clocks.new_var true;
48
   node_inputs = inputs;
49
   node_outputs = outputs;
50
   node_locals = handler.hand_locals;
51
   node_gencalls = [];
52
   node_checks = [];
53
   node_asserts = handler.hand_asserts; 
54
   node_eqs = handler.hand_eqs;
55
   node_dec_stateless = false;
56
   node_stateless = None;
57
   node_spec = None;
58
   node_annot = handler.hand_annots
59
 }
60

  
61
let handler_read handler =
62
 List.fold_left (fun read eq -> get_expr_vars read eq.eq_rhs) ISet.empty handler.hand_eqs
63

  
64
let handler_write handler =
65
 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
66

  
67
let expr_of_exit_conditions loc st conds =
68
 List.fold_right add_branch conds (init loc false st)
69

  
40 70
let pp_restart fmt restart =
41 71
  Format.fprintf fmt "%s" (if restart then "restart" else "resume")
42 72

  
43
let pp_unless fmt (expr, restart, st) =
73
let pp_unless fmt (_, expr, restart, st) =
44 74
  Format.fprintf fmt "unless %a %a %s"
45 75
    Printers.pp_expr expr
46 76
    pp_restart restart
47 77
    st
48 78

  
49
let pp_until fmt (expr, restart, st) =
79
let pp_until fmt (_, expr, restart, st) =
50 80
  Format.fprintf fmt "until %a %a %s"
51 81
    Printers.pp_expr expr
52 82
    pp_restart restart
src/causality.ml
532 532
  end
533 533

  
534 534
let add_external_dependency outputs mems g =
535
  let caller ="!_world" in
535
  let caller ="!!_world" in
536 536
  begin
537 537
    IdentDepGraph.add_vertex g caller;
538 538
    ISet.iter (fun o -> IdentDepGraph.add_edge g caller o) outputs;
src/corelang.ml
891 891
and get_node_calls nodes node =
892 892
  List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty node.node_eqs
893 893

  
894
let rec get_expr_vars vars e =
895
  get_expr_desc_vars vars e.expr_desc
896
and get_expr_desc_vars vars expr_desc =
897
  match expr_desc with
898
  | Expr_const _ -> vars
899
  | Expr_ident x -> Utils.ISet.add x vars
900
  | Expr_tuple el
901
  | Expr_array el -> List.fold_left get_expr_vars vars el
902
  | Expr_pre e1 -> get_expr_vars vars e1
903
  | Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1 
904
  | Expr_access (e1, d) 
905
  | Expr_power (e1, d)   -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d]
906
  | Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e]
907
  | Expr_arrow (e1, e2) 
908
  | Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2]
909
  | Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl
910
  | Expr_appl (_, arg, None)   -> get_expr_vars vars arg
911
  | Expr_appl (_, arg, Some (r,_)) -> get_expr_vars (Utils.ISet.add r vars) arg
912

  
894 913

  
895 914
let rec expr_has_arrows e =
896 915
  expr_desc_has_arrows e.expr_desc
src/corelang.mli
108 108
val get_dependencies : program -> top_decl list
109 109
(* val prog_unfold_consts: program -> program *)
110 110

  
111
val get_expr_vars: Utils.ISet.t -> expr -> Utils.ISet.t
111 112
val expr_replace_var: (ident -> ident) -> expr -> expr
112 113
val eq_replace_rhs_var: (ident -> bool) -> (ident -> ident) -> eq -> eq
113 114

  
src/lustreSpec.ml
144 144

  
145 145
and handler_desc =
146 146
  {hand_state: ident;
147
   hand_unless: (expr * bool * ident) list;
148
   hand_until: (expr * bool * ident) list;
147
   hand_unless: (Location.t * expr * bool * ident) list;
148
   hand_until: (Location.t * expr * bool * ident) list;
149 149
   hand_locals: var_decl list;
150 150
   hand_eqs: eq list;
151
   hand_asserts: assert_t list;
152
   hand_annots: expr_annot list;
151 153
   hand_loc: Location.t}
152 154

  
153 155
type statement =
src/parser_lustre.mly
259 259
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
260 260

  
261 261
automaton:
262
 AUTOMATON type_ident handler_list { failwith "not implemented" }
262
 AUTOMATON type_ident handler_list { (Automata.mkautomata (get_loc ()) $2 $3); failwith "not implemented" }
263 263

  
264 264
handler_list:
265 265
     { [] }
266 266
| handler handler_list { $1::$2 }
267 267

  
268 268
handler:
269
 STATE UIDENT ARROW unless_list locals LET eq_list TEL until_list { () }
269
 STATE UIDENT ARROW unless_list locals LET eq_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }
270 270

  
271 271
unless_list:
272
    { Automata.init }
273
| unless unless_list { let (expr1, case1) = $1 in (fun case -> Automata.add_branch expr1 case1 ($2 case)) }
272
    { [] }
273
| unless unless_list { $1::$2 }
274 274

  
275 275
until_list:
276
    { Automata.init }
277
| until until_list { let (expr1, case1) = $1 in (fun case -> Automata.add_branch expr1 case1 ($2 case)) }
276
    { [] }
277
| until until_list { $1::$2 }
278 278

  
279 279
unless:
280
  UNLESS expr RESTART UIDENT { ($2, (get_loc (), true, $4))  }
281
| UNLESS expr RESUME UIDENT  { ($2, (get_loc (), false, $4)) }
280
  UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
281
| UNLESS expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
282 282

  
283 283
until:
284
  UNTIL expr RESTART UIDENT { ($2, (get_loc (), true, $4))  }
285
| UNTIL expr RESUME UIDENT  { ($2, (get_loc (), false, $4)) }
284
  UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
285
| UNTIL expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
286 286

  
287 287
assert_:
288 288
| ASSERT expr SCOL {mkassert ($2)}

Also available in: Unified diff