Project

General

Profile

« Previous | Next » 

Revision 1eda3e78

Added by Xavier Thirioux almost 8 years ago

- work in progress for automata...

View differences:

src/automata.ml
13 13 
open LustreSpec
14 14 
open Corelang
15 15 

  		




  16
  
  
    
let pp_restart fmt restart =


  		




  17
  
  
    
  Format.fprintf fmt "%s" (if restart then "restart" else "resume")


  		




  18
  
  
    

  		




  19
  
  
    
let pp_unless fmt (_, expr, restart, st) =


  		




  20
  
  
    
  Format.fprintf fmt "unless %a %a %s"


  		




  21
  
  
    
    Printers.pp_expr expr


  		




  22
  
  
    
    pp_restart restart


  		




  23
  
  
    
    st


  		




  24
  
  
    

  		




  25
  
  
    
let pp_until fmt (_, expr, restart, st) =


  		




  26
  
  
    
  Format.fprintf fmt "until %a %a %s"


  		




  27
  
  
    
    Printers.pp_expr expr


  		




  28
  
  
    
    pp_restart restart


  		




  29
  
  
    
    st


  		




  30
  
  
    

  		




  31
  
  
    
let pp_handler fmt handler =


  		




  32
  
  
    
  Format.fprintf fmt "state %s -> %a %a let %a tel %a"


  		




  33
  
  
    
    handler.hand_state


  		




  34
  
  
    
    (Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless


  		




  35
  
  
    
    (fun fmt locals ->


  		




  36
  
  
    
      match locals with [] -> () | _ ->


  		




  37
  
  
    
	Format.fprintf fmt "@[<v 4>var %a@]@ " 


  		




  38
  
  
    
	  (Utils.fprintf_list ~sep:"@ " 


  		




  39
  
  
    
	     (fun fmt v -> Format.fprintf fmt "%a;" Printers.pp_node_var v))


  		




  40
  
  
    
	  locals)


  		




  41
  
  
    
    handler.hand_locals


  		




  42
  
  
    
    Printers.pp_node_eqs handler.hand_eqs


  		




  43
  
  
    
    (Utils.fprintf_list ~sep:"@ " pp_until) handler.hand_until


  		




  44
  
  
    

  		




  45
  
  
    
let pp_automata fmt aut =


  		




  46
  
  
    
  Format.fprintf fmt "automaton %s %a"


  		




  47
  
  
    
    aut.aut_id


  		




  48
  
  
    
    (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers


  		




  49
  
  
    

  		




  50
  16
  
    
let mkbool loc b =


  		




  51
  17
  
    
 mkexpr loc (Expr_const (const_of_bool b))


  		




  52
  18
  
    

  		




  ......




  62
  28
  
    
let add_branch (loc, expr, restart, st) cont =


  		




  63
  29
  
    
 mkexpr loc (Expr_ite (expr, mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st]), cont))


  		




  64
  30
  
    

  		




  65
  
  
    
let mkhandler loc st unless until locals (eqs, asserts, annots) =


  		




  
  31
  
    
let mkhandler loc st unless until locals (stmts, asserts, annots) =


  		




  66
  32
  
    
 {hand_state = st;


  		




  67
  33
  
    
  hand_unless = unless;


  		




  68
  34
  
    
  hand_until = until;


  		




  69
  35
  
    
  hand_locals = locals;


  		




  70
  
  
    
  hand_eqs = eqs;


  		




  
  36
  
    
  hand_stmts = stmts;


  		




  71
  37
  
    
  hand_asserts = asserts;


  		




  72
  38
  
    
  hand_annots = annots;


  		




  73
  39
  
    
  hand_loc = loc}


  		




  ......




  77
  43
  
    
   aut_handlers = handlers;


  		




  78
  44
  
    
   aut_loc = loc}


  		




  79
  45
  
    

  		




  80
  
  
    
let handler_read handler =


  		




  81
  
  
    
 List.fold_left (fun read eq -> get_expr_vars read eq.eq_rhs) ISet.empty handler.hand_eqs


  		




  82
  
  
    

  		




  83
  
  
    
let handler_write handler =


  		




  84
  
  
    
 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


  		




  
  46
  
    
let rec handler_read reads handler =


  		




  
  47
  
    
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in


  		




  
  48
  
    
  let allvars =


  		




  
  49
  
    
    List.fold_left (fun read stmt ->


  		




  
  50
  
    
      match stmt with


  		




  
  51
  
    
      | Eq eq -> get_expr_vars read eq.eq_rhs


  		




  
  52
  
    
      | Aut aut -> List.fold_left handler_read read aut.aut_handlers ) reads handler.hand_stmts


  		




  
  53
  
    
  in ISet.diff allvars locals


  		




  
  54
  
    

  		




  
  55
  
    
let rec handler_write writes handler =


  		




  
  56
  
    
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in


  		




  
  57
  
    
  let allvars =


  		




  
  58
  
    
    List.fold_left (fun write stmt ->


  		




  
  59
  
    
      match stmt with


  		




  
  60
  
    
      | Eq eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs


  		




  
  61
  
    
      | Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts


  		




  
  62
  
    
  in ISet.diff allvars locals


  		




  85
  63
  
    

  		




  86
  64
  
    
let node_of_handler node aut_id handler =


  		




  87
  
  
    
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in 


  		




  88
  
  
    
  let inputs = handler_read handler in


  		




  89
  
  
    
  let outputs = handler_write handler in


  		




  
  65
  
    
  let inputs = handler_read ISet.empty handler in


  		




  
  66
  
    
  let outputs = handler_write ISet.empty handler in


  		




  90
  67
  
    
  {


  		




  91
  68
  
    
    node_id = Format.sprintf "%s_%s_handler" aut_id handler.hand_state;


  		




  92
  69
  
    
    node_type = Types.new_var ();


  		




  93
  70
  
    
    node_clock = Clocks.new_var true;


  		




  94
  
  
    
    node_inputs = List.map (fun v -> get_node_var v node) (ISet.elements (ISet.diff inputs locals));


  		




  95
  
  
    
    node_outputs = List.map (fun v -> get_node_var v node) (ISet.elements (ISet.diff outputs locals));


  		




  
  71
  
    
    node_inputs = List.map (fun v -> get_node_var v node) (ISet.elements inputs);


  		




  
  72
  
    
    node_outputs = List.map (fun v -> get_node_var v node) (ISet.elements outputs);


  		




  96
  73
  
    
    node_locals = handler.hand_locals;


  		




  97
  74
  
    
    node_gencalls = [];


  		




  98
  75
  
    
    node_checks = [];


  		




  99
  76
  
    
    node_asserts = handler.hand_asserts; 


  		




  100
  
  
    
    node_eqs = handler.hand_eqs;


  		




  
  77
  
    
    node_stmts = handler.hand_stmts;


  		




  101
  78
  
    
    node_dec_stateless = false;


  		




  102
  79
  
    
    node_stateless = None;


  		




  103
  80
  
    
    node_spec = None;


  		




  ......




  111
  88
  
    
  let arg = mkexpr loc (Expr_tuple (List.map (fun v -> mkident loc v.var_id) node.node_inputs)) in


  		




  112
  89
  
    
  mkexpr loc (Expr_when (mkexpr loc (Expr_appl (node.node_id, arg, Some (restart, tag_true))), state, tag))


  		




  113
  90
  
    

  		




  114
  
  
    
let assign_aut_handlers loc node actual_r actual_s hnodes =


  		




  
  91
  
    
let assign_aut_handlers loc actual_r actual_s hnodes =


  		




  115
  92
  
    
  let outputs = (snd (List.hd hnodes)).node_outputs in


  		




  116
  93
  
    
  let assign_handlers = List.map (fun (hs, n) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in


  		




  117
  94
  
    
  let assign_expr = mkexpr loc (Expr_merge (actual_s, assign_handlers)) in


  		




  ......




  123
  100
  
    
  { tydef_id = tname;


  		




  124
  101
  
    
    tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers)


  		




  125
  102
  
    
  }


  		




  
  103
  
    
(*


  		




  
  104
  
    
let expand_automata_stmt (top_decls, locals, eqs) stmt =


  		




  
  105
  
    
  match stmt with


  		




  
  106
  
    
  | Eq eq -> (top_decls, locals, eq::eqs)


  		




  
  107
  
    
  | Aut aut ->


  		




  
  108
  
    

  		




  126
  109
  
    

  		




  127
  110
  
    
let expand_automata top_node aut =


  		




  128
  111
  
    
  let node = node_of_top top_node in


  		




  ......




  141
  124
  
    
  let fby_until_expr = mkfby aut.aut_loc (init aut.aut_loc tag_false initial) until_expr in


  		




  142
  125
  
    
  let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in


  		




  143
  126
  
    
  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler node aut.aut_id h)) aut.aut_handlers in


  		




  144
  
  
    
  let assign_eq = assign_aut_handlers aut.aut_loc node actual_r actual_s hnodes in


  		




  
  127
  
    
  let assign_eq = assign_aut_handlers aut.aut_loc actual_r actual_s hnodes in


  		




  145
  128
  
    
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in


  		




  146
  129
  
    
  let tydec_const id = { ty_dec_desc = Tydec_const id; ty_dec_loc = aut.aut_loc } in


  		




  147
  130
  
    
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in


  		




  ......




  149
  132
  
    
                 mkvar_decl aut.aut_loc (actual_r  , tydec_bool, ckdec_any, false);


  		




  150
  133
  
    
                 mkvar_decl aut.aut_loc (incoming_s, tydec_const typedef.tydef_id, ckdec_any, false);


  		




  151
  134
  
    
                 mkvar_decl aut.aut_loc (actual_s  , tydec_const typedef.tydef_id, ckdec_any, false)] in


  		




  152
  
  
    
  let eqs' = [unless_eq; assign_eq; until_eq] in


  		




  153
  
  
    
  let node' = { node with node_locals = locals'@node.node_locals; node_eqs = eqs'@node.node_eqs } in


  		




  
  135
  
    
  let eqs' = [Eq unless_eq; Eq assign_eq; Eq until_eq] in


  		




  
  136
  
    
  let node' = { node with node_locals = locals'@node.node_locals; node_stmts = eqs'@node.node_stmts } in


  		




  154
  137
  
    
  (mktop_decl aut.aut_loc owner false (TypeDef typedef)) ::


  		




  155
  138
  
    
  { top_node with top_decl_desc = Node node' } ::


  		




  156
  139
  
    
  (List.map2 (fun h (hs, n) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes)


  		




  157
  
  
    

  		




  158
  
  
    
let node_extract_automata top_decl =


  		




  
  140
  
    
*)


  		




  
  141
  
    
let rec node_extract_automata top_decl =


  		




  159
  142
  
    
  match top_decl.top_decl_desc with


  		




  160
  
  
    
  | Node nd -> [top_decl]


  		




  
  143
  
    
  | Node nd -> []


  		




  161
  144
  
    
  | _ -> [top_decl]


  		




  162
  145
  
    
(*


  		




  163
  146
  
    
let extract_automata top_decls =


  		












Also available in:  Unified diff