Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / automata.ml @ 3b2bd83d

History | View | Annotate | Download (14.5 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
open Utils
13
open LustreSpec
14
open Corelang
15

    
16

    
17
type aut_state =
18
    {
19
      incoming_r' : var_decl;
20
      incoming_s' : var_decl;
21
      incoming_r : var_decl;
22
      incoming_s : var_decl;
23
      actual_r : var_decl;
24
      actual_s : var_decl
25
    }
26

    
27
let as_clock var_decl =
28
  let tydec = var_decl.var_dec_type in
29
  { var_decl with var_dec_type = { ty_dec_desc = Tydec_clock tydec.ty_dec_desc; ty_dec_loc = tydec.ty_dec_loc } }
30

    
31
let mkbool loc b =
32
 mkexpr loc (Expr_const (const_of_bool b))
33

    
34
let mkident loc id =
35
 mkexpr loc (Expr_ident id)
36

    
37
let mkconst loc id =
38
 mkexpr loc (Expr_const (Const_tag id))
39

    
40
let mkfby loc e1 e2 =
41
 mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2)))
42

    
43
let mkpair loc e1 e2 =
44
 mkexpr loc (Expr_tuple [e1; e2])
45

    
46
let mkidentpair loc restart state =
47
 mkexpr loc (Expr_tuple [mkident loc restart; mkident loc state])
48

    
49
let add_branch (loc, expr, restart, st) cont =
50
 mkexpr loc (Expr_ite (expr, mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st]), cont))
51

    
52
let mkhandler loc st unless until locals (stmts, asserts, annots) =
53
 {hand_state = st;
54
  hand_unless = unless;
55
  hand_until = until;
56
  hand_locals = locals;
57
  hand_stmts = stmts;
58
  hand_asserts = asserts;
59
  hand_annots = annots;
60
  hand_loc = loc}
61

    
62
let mkautomata loc id handlers =
63
  {aut_id = id;
64
   aut_handlers = handlers;
65
   aut_loc = loc}
66

    
67
let expr_of_exit loc restart state conds tag =
68
  mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag))
69

    
70
let rec unless_read reads handler =
71
  let res =
72
  List.fold_left (fun read (_, c, _, _) -> get_expr_vars read c) reads handler.hand_unless
73
  in
74
(
75
(*
76
Format.eprintf "unless_reads %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements reads);
77
Format.eprintf "unless_reads' %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res);
78
*)
79
res
80
)
81

    
82
let rec until_read reads handler =
83
  List.fold_left (fun read (_, c, _, _) -> get_expr_vars read c) reads handler.hand_until
84

    
85
let rec handler_read reads handler =
86
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
87
  let allvars =
88
    List.fold_left (fun read stmt ->
89
      match stmt with
90
      | Eq eq -> get_expr_vars read eq.eq_rhs
91
      | Aut aut -> automata_read read aut) reads handler.hand_stmts
92
  in let res = ISet.diff allvars locals
93
     in
94
(
95
(*
96
Format.eprintf "handler_allvars %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements allvars);
97
Format.eprintf "handler_read %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res);
98
*)
99
res
100
)
101

    
102
and automata_read reads aut =
103
  List.fold_left (fun read handler -> until_read (handler_read (unless_read read handler) handler) handler) reads aut.aut_handlers
104

    
105
let rec handler_write writes handler =
106
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
107
  let allvars =
108
    List.fold_left (fun write stmt ->
109
      match stmt with
110
      | Eq eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs
111
      | Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts
112
  in ISet.diff allvars locals
113

    
114
let node_vars_of_idents node iset =
115
  List.fold_right (fun v res -> if ISet.mem v.var_id iset then v :: res else res) (get_node_vars node) []
116

    
117
let mkautomata_state used typedef loc id =
118
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = loc } in
119
  let tydec_state id = { ty_dec_desc = Tydec_const id; ty_dec_loc = loc } in
120
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = loc } in
121
  let incoming_r' = mk_new_name used (id ^ "__next_restart_in") in
122
  let incoming_s' = mk_new_name used (id ^ "__next_state_in") in
123
  let incoming_r = mk_new_name used (id ^ "__restart_in") in
124
  let incoming_s = mk_new_name used (id ^ "__state_in") in
125
  let actual_r = mk_new_name used (id ^ "__restart_act") in
126
  let actual_s = mk_new_name used (id ^ "__state_act") in
127
  {
128
    incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false, None);
129
    incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false, None);
130
    incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false, None);
131
    incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false, None);
132
    actual_r = mkvar_decl loc (actual_r  , tydec_bool, ckdec_any, false, None);
133
    actual_s = mkvar_decl loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false, None)
134
  }
135

    
136
let vars_of_aut_state aut_state =
137
  [aut_state.incoming_r'; aut_state.incoming_r; aut_state.actual_r; aut_state.incoming_s'; as_clock aut_state.incoming_s; as_clock aut_state.actual_s]
138

    
139
let node_of_unless nused used node aut_id aut_state handler =
140
(*Format.eprintf "node_of_unless %s@." node.node_id;*)
141
  let inputs = unless_read ISet.empty handler in
142
  let var_inputs = aut_state.incoming_r (*:: aut_state.incoming_s*) :: (node_vars_of_idents node inputs) in
143
  let var_outputs = aut_state.actual_r :: aut_state.actual_s :: [] in
144
  let init_expr = mkpair handler.hand_loc (mkident handler.hand_loc aut_state.incoming_r.var_id) (mkconst handler.hand_loc handler.hand_state) in
145
(*  let init_expr = mkidentpair handler.hand_loc aut_state.incoming_r.var_id aut_state.incoming_s.var_id in *)
146
  let expr_outputs = List.fold_right add_branch handler.hand_unless init_expr in
147
  let eq_outputs = Eq (mkeq handler.hand_loc ([aut_state.actual_r.var_id; aut_state.actual_s.var_id], expr_outputs)) in
148
  let node_id = mk_new_name nused (Format.sprintf "%s__%s_unless" aut_id handler.hand_state) in
149
  let args = List.map (fun v -> mkexpr handler.hand_loc (Expr_when (mkident handler.hand_loc v.var_id, aut_state.incoming_s.var_id, handler.hand_state))) var_inputs in
150
  let reset = Some (mkident handler.hand_loc aut_state.incoming_r.var_id) in
151
  {
152
    node_id = node_id;
153
    node_type = Types.new_var ();
154
    node_clock = Clocks.new_var true;
155
    node_inputs = List.map copy_var_decl var_inputs;
156
    node_outputs = List.map copy_var_decl var_outputs;
157
    node_locals = [];
158
    node_gencalls = [];
159
    node_checks = [];
160
    node_asserts = []; 
161
    node_stmts = [ eq_outputs ];
162
    node_dec_stateless = false;
163
    node_stateless = None;
164
    node_spec = None;
165
    node_annot = []
166
  },
167
  mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset))
168

    
169

    
170
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name)
171

    
172
let rec rename_stmts_outputs frename stmts =
173
  match stmts with
174
  | []           -> []
175
  | (Eq eq) :: q   -> let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in
176
		      eq' :: rename_stmts_outputs frename q
177
  | (Aut aut) :: q -> let handlers' = List.map (fun h -> { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts}) aut.aut_handlers in
178
                      let aut' = Aut { aut with aut_handlers = handlers' } in
179
		      aut' :: rename_stmts_outputs frename q
180

    
181
let mk_frename used outputs =
182
  let table = ISet.fold (fun name table -> IMap.add name (rename_output used name) table) outputs IMap.empty in
183
  (fun name -> try IMap.find name table with Not_found -> name)
184

    
185
let node_of_assign_until nused used node aut_id aut_state handler =
186
(*Format.eprintf "node_of_assign_until %s@." node.node_id;*)
187
  let writes = handler_write ISet.empty handler in
188
  let inputs = ISet.diff (handler_read (until_read ISet.empty handler) handler) writes in
189
  let frename = mk_frename used writes in
190
  let var_inputs = aut_state.actual_r (*:: aut_state.actual_s*) :: node_vars_of_idents node inputs in
191
  let new_var_locals = node_vars_of_idents node writes in
192
  let var_outputs = List.sort IdentModule.compare (node_vars_of_idents node writes) in
193
  let new_var_outputs = List.map (fun vdecl -> { vdecl with var_id = frename vdecl.var_id }) var_outputs in
194
  let new_output_eqs = List.map2 (fun o o' -> Eq (mkeq handler.hand_loc ([o'.var_id], mkident handler.hand_loc o.var_id))) var_outputs new_var_outputs in
195
  let init_until = mkpair handler.hand_loc (mkconst handler.hand_loc tag_false) (mkconst handler.hand_loc handler.hand_state) in
196
  let until_expr = List.fold_right add_branch handler.hand_until init_until in
197
  let until_eq = Eq (mkeq handler.hand_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], until_expr)) in
198
  let node_id = mk_new_name nused (Format.sprintf "%s__%s_handler_until" aut_id handler.hand_state) in
199
  let args = List.map (fun v -> mkexpr handler.hand_loc (Expr_when (mkident handler.hand_loc v.var_id, aut_state.actual_s.var_id, handler.hand_state))) var_inputs in
200
  let reset = Some (mkident handler.hand_loc aut_state.actual_r.var_id) in
201
  List.fold_left (fun res v -> ISet.add v.var_id res) ISet.empty var_outputs,
202
  {
203
    node_id = node_id;
204
    node_type = Types.new_var ();
205
    node_clock = Clocks.new_var true;
206
    node_inputs = List.map copy_var_decl var_inputs;
207
    node_outputs = List.map copy_var_decl (aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
208
    node_locals = List.map copy_var_decl (new_var_locals @ handler.hand_locals);
209
    node_gencalls = [];
210
    node_checks = [];
211
    node_asserts = handler.hand_asserts; 
212
    node_stmts = until_eq :: new_output_eqs @ handler.hand_stmts;
213
    node_dec_stateless = false;
214
    node_stateless = None;
215
    node_spec = None;
216
    node_annot = handler.hand_annots
217
  },
218
  mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset))
219

    
220
let typedef_of_automata aut =
221
  let tname = Format.sprintf "%s__type" aut.aut_id in
222
  { tydef_id = tname;
223
    tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers)
224
  }
225

    
226
let expand_automata nused used owner typedef node aut =
227
  let initial = (List.hd aut.aut_handlers).hand_state in
228
  let aut_state = mkautomata_state used typedef aut.aut_loc aut.aut_id in
229
  let unodes = List.map (fun h -> node_of_unless nused used node aut.aut_id aut_state h) aut.aut_handlers in
230
  let aunodes = List.map (fun h -> node_of_assign_until nused used node aut.aut_id aut_state h) aut.aut_handlers in
231
  let all_outputs = List.fold_left (fun all (outputs, _, _) -> ISet.union outputs all) ISet.empty aunodes in
232
  let unless_handlers = List.map2 (fun h (n, c) -> (h.hand_state, c)) aut.aut_handlers unodes in
233
  let unless_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.incoming_s.var_id, unless_handlers)) in
234
  let unless_eq = mkeq aut.aut_loc ([aut_state.actual_r.var_id; aut_state.actual_s.var_id], unless_expr) in
235
  let assign_until_handlers = List.map2 (fun h (_, n, c) -> (h.hand_state, c)) aut.aut_handlers aunodes in
236
  let assign_until_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.actual_s.var_id, assign_until_handlers)) in
237
  let assign_until_vars = [aut_state.incoming_r'.var_id; aut_state.incoming_s'.var_id] @ (ISet.elements all_outputs) in
238
  let assign_until_eq = mkeq aut.aut_loc (assign_until_vars, assign_until_expr) in
239
  let fby_incoming_expr = mkfby aut.aut_loc (mkpair aut.aut_loc (mkconst aut.aut_loc tag_false) (mkconst aut.aut_loc initial)) (mkidentpair aut.aut_loc aut_state.incoming_r'.var_id aut_state.incoming_s'.var_id) in
240
  let incoming_eq = mkeq aut.aut_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], fby_incoming_expr) in
241
  let locals' = vars_of_aut_state aut_state in
242
  let eqs' = [Eq unless_eq; Eq assign_until_eq; Eq incoming_eq] in
243
  (  List.map2 (fun h (n, _) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers unodes
244
   @ List.map2 (fun h (_, n, _) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers aunodes,
245
  locals',
246
  eqs')
247

    
248
let expand_node_stmt nused used owner node (top_types, top_nodes, locals, eqs) stmt =
249
  match stmt with
250
  | Eq eq -> (top_types, top_nodes, locals, (Eq eq)::eqs)
251
  | Aut aut ->
252
    let typedef = typedef_of_automata aut in
253
    let used' name = used name || List.exists (fun v -> v.var_id = name) locals in
254
    let nused' name =
255
      nused name ||
256
      List.exists (fun t -> match t.top_decl_desc with
257
      | ImportedNode nd -> nd.nodei_id = name | Node nd -> nd.node_id = name
258
      | _ -> false) top_nodes in
259
    let (top_decls', locals', eqs') = expand_automata nused' used' owner typedef node aut in
260
    let top_typedef = mktop_decl aut.aut_loc owner false (TypeDef typedef) in
261
    (top_typedef :: top_types, top_decls'@top_nodes, locals'@locals, eqs'@eqs)
262

    
263
let expand_node_stmts nused used loc owner node =
264
  let (top_types', top_nodes', locals', eqs') =
265
    List.fold_left (expand_node_stmt nused used owner node) ([], [], [], []) node.node_stmts in
266
  let node' = 
267
    { node with node_locals = locals'@node.node_locals; node_stmts = eqs' } in
268
  let top_node = mktop_decl loc owner false (Node node') in
269
  top_types', top_node, top_nodes'
270

    
271
let rec expand_decls_rec nused top_decls =
272
  match top_decls with
273
  | [] -> []
274
  | top_decl::q ->
275
    match top_decl.top_decl_desc with
276
    | Node nd ->
277
      let used name =
278
	   List.exists (fun v -> v.var_id = name) nd.node_inputs
279
	|| List.exists (fun v -> v.var_id = name) nd.node_outputs
280
	|| List.exists (fun v -> v.var_id = name) nd.node_locals in
281
      let (top_types', top_decl', top_nodes') = expand_node_stmts nused used top_decl.top_decl_loc top_decl.top_decl_owner nd in
282
      top_types' @ (top_decl' :: expand_decls_rec nused (top_nodes'@q))
283
    | _       -> top_decl :: expand_decls_rec nused q
284

    
285
let expand_decls top_decls =
286
  let top_names = List.fold_left (fun names t -> match t.top_decl_desc with
287
    | Node nd         -> ISet.add nd.node_id names
288
    | ImportedNode nd -> ISet.add nd.nodei_id names
289
    | _               -> names) ISet.empty top_decls in
290
  let nused name = ISet.mem name top_names in
291
  expand_decls_rec nused top_decls
292

    
293
(* Local Variables: *)
294
(* compile-command:"make -C .." *)
295
(* End: *)
296