Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / automata.ml @ 2822cf55

History | View | Annotate | Download (3.72 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
let mkbool loc b =
17
 mkexpr loc (Expr_const (const_of_bool b))
18

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

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

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

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

    
38
let mkautomata loc id handlers =
39
  {aut_id = id;
40
   aut_handlers = handlers;
41
   aut_loc = loc}
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

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

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

    
79
let pp_until fmt (_, expr, restart, st) =
80
  Format.fprintf fmt "until %a %a %s"
81
    Printers.pp_expr expr
82
    pp_restart restart
83
    st
84

    
85
let pp_handler fmt handler =
86
  Format.fprintf fmt "state %s -> %a %a let %a tel %a"
87
    handler.hand_state
88
    (Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
89
    (fun fmt locals ->
90
      match locals with [] -> () | _ ->
91
	Format.fprintf fmt "@[<v 4>var %a@]@ " 
92
	  (Utils.fprintf_list ~sep:"@ " 
93
	     (fun fmt v -> Format.fprintf fmt "%a;" Printers.pp_node_var v))
94
	  locals)
95
    handler.hand_locals
96
    Printers.pp_node_eqs handler.hand_eqs
97
    (Utils.fprintf_list ~sep:"@ " pp_until) handler.hand_until
98

    
99
let pp_automata fmt aut =
100
  Format.fprintf fmt "automaton %s %a"
101
    aut.aut_id
102
    (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers
103

    
104
(*
105
let rec extract_node expr top_decls =
106
  match expr.expr_desc with
107
  | Expr_const _
108
  | Expr_ident _
109
  | Expr_tuple _
110
  | Expr_ite   of expr * expr * expr
111
  | Expr_arrow of expr * expr
112
  | Expr_fby of expr * expr
113
  | Expr_array of expr list
114
  | Expr_access of expr * Dimension.dim_expr
115
  | Expr_power of expr * Dimension.dim_expr
116
  | Expr_pre of expr
117
  | Expr_when of expr * ident * label
118
  | Expr_merge of ident * (label * expr) list
119
  | Expr_appl
120
*)
121

    
122
(* Local Variables: *)
123
(* compile-command:"make -C .." *)
124
(* End: *)