Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_extract.ml @ 8c934ccd

History | View | Annotate | Download (22.1 KB)

1
open Lustre_types
2
open Utils
3
open Seal_utils			
4
open Zustre_data (* Access to Z3 context *)
5
   
6

    
7
(* Switched system extraction *)
8
type element = IsInit | Expr of expr
9
type guard = (element * bool) list
10
type guarded_expr = guard * element
11
type mdef_t = guarded_expr list
12

    
13
let pp_elem fmt e =
14
  match e with
15
  | IsInit -> Format.fprintf fmt "init"
16
  | Expr e -> Printers.pp_expr fmt e
17

    
18
let pp_guard_expr fmt (gl,e) =
19
  Format.fprintf fmt "%a -> %a"
20
    (fprintf_list ~sep:"; "
21
       (fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) gl
22
    pp_elem e
23

    
24
let pp_mdefs fmt gel = fprintf_list ~sep:"@ " pp_guard_expr fmt gel
25

    
26
  
27
let add_init defs vid =
28
  Hashtbl.add defs vid [[], IsInit]
29

    
30
let deelem e =  match e with
31
    Expr e -> e
32
  | IsInit -> assert false (* Wasn't expecting isinit here: we are building values! *)
33

    
34
let is_eq_elem elem elem' =
35
  match elem, elem' with
36
  | IsInit, IsInit -> true
37
  | Expr e, Expr e' ->
38
     Corelang.is_eq_expr e e'
39
  | _ -> false
40

    
41
let select_elem elem (gelem, _) =
42
  is_eq_elem elem gelem
43

    
44

    
45
(**************************************************************)
46
(* Convert from Lustre expressions to Z3 expressions and back *)
47
(* All (free) variables have to be declared in the Z3 context *)
48
(**************************************************************)
49

    
50
let is_init_name = "__is_init"
51

    
52
let const_defs = Hashtbl.create 13
53
let is_const id = Hashtbl.mem const_defs id
54
let get_const id = Hashtbl.find const_defs id
55
                 
56
(* expressions are only basic constructs here, no more ite, tuples,
57
   arrows, fby, ... *)
58
let expr_to_z3_expr, zexpr_to_expr =
59
  (* List to store converted expression. Some expressions seem to
60
     produce segfaults in z3. Storing the processed ones may solved
61
     the issue. Using list instead of hash to ease the comparison of
62
     expressions. *)
63
  let hash = ref [] in
64
  let comp_expr e (e', _) = Corelang.is_eq_expr e e' in
65
  let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in
66
  let mem_expr e = List.exists (comp_expr e) !hash in
67
  let mem_zexpr ze = List.exists (comp_zexpr ze) !hash in
68
  let get_zexpr e =
69
    let (_, ze) = List.find (comp_expr e) !hash in
70
    ze
71
  in
72
  let get_expr ze =
73
    let (e, _) = List.find (comp_zexpr ze) !hash in
74
    e
75
  in
76
  let add_expr e ze = hash := (e, ze)::!hash in
77
  let rec e2ze e =
78
    if mem_expr e then (
79
      get_zexpr e
80
    )
81
    else (
82
      let res =
83
        match e.expr_desc with
84
        | Expr_const c ->
85
           let z3e = Zustre_common.horn_const_to_expr c in
86
           add_expr e z3e;
87
           z3e
88
        | Expr_ident id -> (
89
          if is_const id then (
90
            let c = get_const id in
91
            let z3e = Zustre_common.horn_const_to_expr c in
92
            add_expr e z3e;
93
            z3e
94
        )
95
        else (
96
          let fdecl_id = Zustre_common.get_fdecl id in
97
          let z3e = Z3.Expr.mk_const_f !ctx fdecl_id in
98
          add_expr e z3e;
99
          z3e
100
          )
101
        )
102
      | Expr_appl (id,args, None) (* no reset *) ->
103
         let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in
104
         add_expr e z3e;
105
         z3e
106
         
107
      | _ -> assert false
108
      in
109
      res
110
    )
111
  in
112
  let rec ze2e ze =
113
    let ze_name ze =
114
      let fd = Z3.Expr.get_func_decl ze in
115
      Z3.Symbol.to_string (Z3.FuncDecl.get_name fd)
116
    in
117
    if mem_zexpr ze then
118
      None, Some (get_expr ze)
119
    else
120
      let open Corelang in
121
      let fd = Z3.Expr.get_func_decl ze in
122
      let zel = Z3.Expr.get_args ze in
123
      match Z3.Symbol.to_string (Z3.FuncDecl.get_name fd), zel with
124
      (*      | var, [] -> (* should be in env *) get_e *)
125

    
126
      (* Extracting IsInit status *)
127
      | "not", [ze] when ze_name ze = is_init_name ->
128
         Some false, None
129
      | name, [] when name = is_init_name -> Some true, None
130
      (* Other constructs are converted to a lustre expression *)
131
      | op, _ -> (
132
        
133
        
134
        if Z3.Expr.is_numeral ze then
135
          let e =
136
            if Z3.Arithmetic.is_real ze then
137
              let num =  Num.num_of_ratio (Z3.Arithmetic.Real.get_ratio ze) in
138
              let s = Z3.Arithmetic.Real.numeral_to_string ze in
139
              mkexpr
140
                Location.dummy_loc
141
                (Expr_const
142
                   (Const_real
143
                      (num, 0, s)))
144
            else if Z3.Arithmetic.is_int ze then
145
              mkexpr
146
                Location.dummy_loc
147
                (Expr_const
148
                   (Const_int
149
                      (Big_int.int_of_big_int (Z3.Arithmetic.Integer.get_big_int ze))))
150
            else if Z3.Expr.is_const ze then
151
              match Z3.Expr.to_string ze with
152
              | "true" -> mkexpr Location.dummy_loc
153
                            (Expr_const (Const_tag (tag_true)))
154
              | "false" ->
155
                 mkexpr Location.dummy_loc
156
                   (Expr_const (Const_tag (tag_false)))
157
              | _ -> assert false
158
            else
159
              (
160
                Format.eprintf "Const err: %s %b@." (Z3.Expr.to_string ze) (Z3.Expr.is_const ze);
161
                assert false (* a numeral but no int nor real *)
162
              )
163
          in
164
          None, Some e
165
        else
166
          match op with
167
          | "not" | "=" | "-" | "*" | "/"
168
            | ">=" | "<=" | ">" | "<" 
169
            ->
170
             let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
171
             None, Some (mkpredef_call Location.dummy_loc op args)
172
          | "+" -> ( (* Special treatment of + for 2+ args *)
173
            let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
174
            let e = match args with
175
                [] -> assert false
176
              | [hd] -> hd
177
              | e1::e2::tl ->
178
                 let first_binary_and = mkpredef_call Location.dummy_loc op [e1;e2] in
179
                 if tl = [] then first_binary_and else
180
                   List.fold_left (fun e e_new ->
181
                       mkpredef_call Location.dummy_loc op [e;e_new]
182
                     ) first_binary_and tl
183
                 
184
            in
185
            None, Some e 
186
          )
187
          | "and" -> (
188
            (* Special case since it can contain is_init pred *)
189
            let args = List.map (fun ze -> ze2e ze) zel in
190
            match args with
191
            | [] -> assert false
192
            | [hd] -> hd
193
            | hd::tl ->
194
               List.fold_left
195
                 (fun (is_init_opt1, expr_opt1) (is_init_opt2, expr_opt2) ->
196
                   (match is_init_opt1, is_init_opt2 with
197
                      None, x | x, None -> x
198
                      | Some _, Some _ -> assert false),
199
                   (match expr_opt1, expr_opt2 with
200
                    | None, x | x, None -> x
201
                    | Some e1, Some e2 ->
202
                       Some (mkpredef_call Location.dummy_loc "&&" [e1; e2])
203
                 ))
204
                 hd tl 
205
          )
206
                   
207
          | op -> 
208
             let args = List.map (fun ze ->  (snd (ze2e ze))) zel in
209
             Format.eprintf "deal with op %s (%i). Expr is %s@."  op (List.length args) (Z3.Expr.to_string ze); assert false
210
      )
211
  in
212
  (fun e -> e2ze e), (fun ze -> ze2e ze)
213

    
214
let is_init_z3e = Z3.Expr.mk_const_s !ctx is_init_name  Zustre_common.bool_sort 
215
let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e 
216

    
217
(*****************************************************************)
218
(* Checking sat(isfiability) of an expression and simplifying it *)
219
(* All (free) variables have to be declared in the Z3 context    *)
220
(*****************************************************************)
221
               
222
let check_sat, clean_guard = 
223
  (
224
    fun l ->
225
    let solver = Z3.Solver.mk_simple_solver !ctx in
226
    try (
227
    let zl =
228
      List.map (fun (e, posneg) ->
229
          let ze =
230
            match e with
231
            | IsInit -> is_init_z3e
232
            | Expr e -> expr_to_z3_expr e 
233
          in
234
          if posneg then
235
            ze
236
          else
237
            neg_ze ze
238
        ) l
239
    in
240
    let status_res = Z3.Solver.check solver zl in
241
    let sat = match status_res with
242
      | Z3.Solver.UNSATISFIABLE -> false
243
      | _ -> true in
244
    sat, if not sat then [] else l
245
    )
246
    with Zustre_common.UnknownFunction(id, msg) -> (
247
      report ~level:1 msg;
248
      true, l (* keeping everything. *)
249
    )
250
      
251
  
252
  ),
253
  ( fun l ->
254
    try (
255
        let solver = Z3.Solver.mk_simple_solver !ctx in
256
     let zl =
257
    List.map (fun (e, posneg) ->
258
        let ze = expr_to_z3_expr e 
259
        in
260
        if posneg then
261
          ze
262
        else
263
          neg_ze ze
264
      ) l
265
     in
266
     let goal = Z3.Goal.mk_goal !ctx false false false in
267
     let status_res = Z3.Solver.check solver zl in
268
     Z3.Goal.add goal zl;
269
    let goal' = Z3.Goal.simplify goal None in
270
    
271
    Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@."
272
      (Z3.Goal.to_string goal)
273
      (Z3.Goal.to_string goal')
274
      (Z3.Solver.string_of_status status_res)
275
    ;
276
    let ze = Z3.Goal.as_expr goal' in
277
    Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze);
278
   (* let l =
279
      match zexpr_to_expr ze with
280
      | None, None -> []
281
      | None, Some e -> [e, true]
282
      | _ -> assert false
283
    (*      | Some init, None -> [IsInit, init]
284
      | Some init, Some e -> [IsInit, init; Expr e, true]
285
     *)  in
286
     *)
287
    l
288
    )
289
      with Zustre_common.UnknownFunction(id, msg) -> (
290
      report ~level:1 msg;
291
      l (* keeping everything. *)
292
    )
293
  )
294

    
295

    
296
(**************************************************************)
297

    
298
  
299
let clean_sys sys =
300
  List.fold_left (fun accu (guards, updates) ->
301
      let guards' = clean_guard guards in
302
      let sat, _ =  check_sat (List.map (fun (g, pn) -> Expr g, pn) guards') in
303
      (*Format.eprintf "Guard: %a@.Guard cleaned: %a@.Sat? %b@."
304
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards
305
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards'
306
        sat
307

    
308
      ;*)
309
        if sat then
310
        (guards', updates)::accu
311
      else
312
        accu
313
    )
314
    [] sys
315
  
316
let combine_guards ?(fresh=None) gl1 gl2 =
317
  (* Filtering out trivial cases. More semantics ones would have to be
318
     addressed later *)
319
  let check (gexpr, posneg) l =
320
    (* Check if gepxr is part of l *)
321
    let sel_fun = select_elem gexpr in
322
    if List.exists sel_fun l then
323
      (* Checking the guard value posneg *)
324
      let _, status = List.find sel_fun l in
325
      status=posneg, l
326
    else
327
      (* Valid: no overlap *)
328
      (* Individual checkat *)
329
      let ok, e = check_sat [gexpr, posneg] in
330
      if ok then
331
        let l = e@l in
332
        let ok, l = check_sat l in
333
        ok, l 
334
      else
335
        true, l
336
  in
337
  let ok, gl =
338
    List.fold_left (
339
        fun (ok, l) g ->
340
        (* Bypass for negative output *)
341
        if not ok then false, []
342
        else
343
          check g l 
344
      ) (true, gl2) gl1
345
  in
346
  if ok then
347
    match fresh with
348
      None -> true, gl
349
    | Some fresh_g -> (
350
    (* Checking the fresh element *)
351
      check fresh_g gl
352
    )
353
  else
354
    ok, []
355

    
356
(* Encode "If gel1=posneg then gel2":
357
   - Compute the combination of guarded exprs in gel1 and gel2:
358
     - Each guarded_expr in gel1 is transformed as a guard: the
359
       expression is associated to posneg.
360
     - Existing guards in gel2 are concatenated to that list of guards
361
     - We keep expr in the ge of gel2 as the legitimate expression 
362
 *)
363
let concatenate_ge gel1 posneg gel2 =
364
  List.fold_left (
365
      fun accu (g2,e2) ->
366
      List.fold_left (
367
          fun accu (g1,e1) ->
368
          let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in
369
          if ok then
370
            (gl, e2)::accu
371
          else
372
            accu
373
        ) accu gel1
374
    ) [] gel2
375

    
376
let rec rewrite defs expr : guarded_expr list =
377
  let rewrite = rewrite defs in
378
  match expr.expr_desc with
379
  | Expr_appl (id, args, None) ->
380
     let args = rewrite args in
381
     List.map (fun (guards, e) ->
382
           guards,
383
           Expr {expr with expr_desc = Expr_appl(id, deelem e, None)}
384
       ) args 
385
  | Expr_const _  -> [[], Expr expr]
386
  | Expr_ident id ->
387
     if Hashtbl.mem defs id then
388
       Hashtbl.find defs id
389
     else
390
       (* id should be an input *)
391
       [[], Expr expr]
392
  | Expr_ite (g, e1, e2) ->
393
     let g = rewrite g and
394
         e1 = rewrite e1 and
395
         e2 = rewrite e2 in
396
     (concatenate_ge g true e1)@
397
       (concatenate_ge g false e2)
398
  | Expr_merge (g, branches) ->
399
     assert false (* TODO: deal with merges *)
400
    
401
  | Expr_when (e, _, _) -> rewrite e
402
  | Expr_arrow _ -> [[], IsInit] (* At this point the only arrow should be true -> false *)
403
  | Expr_tuple el ->
404
     (* Each expr is associated to its flatten guarded expr list *)
405
     let gell = List.map rewrite el in
406
     (* Computing all combinations: we obtain a list of guarded tuple *)
407
     let rec aux gell : (guard * expr list) list =
408
       match gell with
409
       | [] -> assert false (* Not happening *)
410
       | [gel] -> List.map (fun (g,e) -> g, [deelem e]) gel
411
       | gel::getl ->
412
          let getl = aux getl in
413
          List.fold_left (
414
              fun accu (g,e) ->
415
              List.fold_left (
416
                    fun accu (gl, minituple) ->
417
                    let is_compat, guard_comb = combine_guards g gl in
418
                    if is_compat then
419
                      let new_gt : guard * expr list = (guard_comb, (deelem e)::minituple) in
420
                      new_gt::accu
421
                    else
422
                      accu
423
                  
424
                  ) accu getl
425
            ) [] gel
426
     in
427
     let gtuples = aux gell in
428
     (* Rebuilding the valid type: guarded expr list (with tuple exprs) *)
429
     List.map (fun (g,tuple) -> g, Expr {expr with expr_desc = Expr_tuple tuple}) gtuples
430
  | Expr_fby _
431
    | Expr_appl _
432
                (* Should be removed by mormalization and inlining *)
433
    -> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false
434
  | Expr_array _ | Expr_access _ | Expr_power _
435
                                              (* Arrays not handled here yet *)
436
    -> assert false
437
  | Expr_pre _ -> (* Not rewriting mem assign *)
438
     assert false
439
and add_def defs vid expr =
440
  Hashtbl.add defs vid (rewrite defs expr)
441

    
442
(* Takes a list of guarded exprs (ge) and a guard
443
returns the same list of ge splited into the ones where the guard is true and the ones where it is false. In both lists the associated ge do not mention that guard anymore.
444

    
445
When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *)
446
let split_mdefs elem (mdefs: guarded_expr list) =
447
  List.fold_left (
448
      fun (selected, left_out)
449
          ((guards, expr) as ge) ->
450
      (* select the element of guards that match the argument elem *)
451
      let sel, others_guards = List.partition (select_elem elem) guards in
452
      match sel with
453
      (* we extract the element from the list and add it to the
454
         appropriate list *)
455
      | [_, sel_status] ->
456
         if sel_status then
457
           (others_guards,expr)::selected, left_out
458
         else selected, (others_guards,expr)::left_out
459
      | [] -> (* no such guard exists, we have to duplicate the
460
              guard_expr in both lists *)
461
         ge::selected, ge::left_out
462
      | _ -> (
463
        Format.eprintf "@.Spliting list on elem %a.@.List:%a@."
464
          pp_elem elem
465
          pp_mdefs mdefs;
466
        assert false (* more then one element selected. Should
467
                          not happen , or trival dead code like if
468
                              x then if not x then dead code *)
469
      )
470
    ) ([],[]) mdefs
471
    
472
let split_mem_defs
473
      (elem: element)
474
      (mem_defs: (ident * guarded_expr list) list)
475
      :
476
      ((ident * mdef_t) list) * ((ident * mdef_t) list)
477
  
478
  =
479
  List.fold_right (fun (m,mdefs)
480
                       (accu_pos, accu_neg) ->
481
      let pos, neg =
482
        split_mdefs elem mdefs 
483
      in
484
      (m, pos)::accu_pos,
485
      (m, neg)::accu_neg
486
    ) mem_defs ([],[])
487

    
488

    
489
(* Split a list of mem_defs into init and step lists of guarded
490
   expressions per memory. *)
491
let split_init mem_defs =
492
  split_mem_defs IsInit mem_defs 
493

    
494
let pick_guard mem_defs : expr option =
495
  let gel = List.flatten (List.map snd mem_defs) in
496
  let gl = List.flatten (List.map fst gel) in
497
  let all_guards =
498
    List.map (
499
        (* selecting guards and getting rid of boolean *)
500
        fun (e,b) ->
501
        match e with
502
        | Expr e -> e
503
        | _ -> assert false
504
      (* should have been filtered out
505
                                      yet *)
506
      ) gl
507
  in
508
  (* TODO , one could sort by occurence and provided the most common
509
     one *)
510
  try
511
  Some (List.hd all_guards)  
512
  with _ -> None
513
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions)
514
*)
515
let rec build_switch_sys
516
          (mem_defs : (Utils.ident * guarded_expr list) list )
517
          prefix
518
        :
519
          ((expr * bool) list * (ident * expr) list ) list =
520
  (* if all mem_defs have empty guards, we are done, return prefix,
521
     mem_defs expr.
522

    
523
     otherwise pick a guard in one of the mem, eg (g, b) then for each
524
     other mem, one need to select the same guard g with the same status b, *)
525
  if List.for_all (fun (m,mdefs) ->
526
         (* All defs are unguarded *)
527
         match mdefs with
528
         | [[], _] -> true
529
         | _ -> false
530
       ) mem_defs
531
  then
532
    [prefix ,
533
     List.map (fun (m,gel) ->
534
         match gel with
535
         | [_,e] ->
536
            let e =
537
              match e with
538
              | Expr e -> e
539
              | _ -> assert false (* No IsInit expression *)
540
            in
541
            m,e
542
         | _ -> assert false
543
       ) mem_defs]
544
  else
545
    (* Picking a guard *)
546
    let elem_opt : expr option = pick_guard mem_defs in
547
    match elem_opt with
548
      None -> []
549
    | Some elem -> (
550
      let pos, neg =
551
        split_mem_defs
552
          (Expr elem)
553
          mem_defs
554
      in
555
      (* Special cases to avoid useless computations: true, false conditions *)
556
      match elem.expr_desc with
557
      | Expr_ident "true"  ->   build_switch_sys pos prefix
558
      | Expr_const (Const_tag tag) when tag = Corelang.tag_true
559
        ->   build_switch_sys pos prefix
560
      | Expr_ident "false" ->   build_switch_sys neg prefix
561
      | Expr_const (Const_tag tag) when tag = Corelang.tag_false 
562
        ->   build_switch_sys neg prefix
563
      | _ -> (* Regular case *)
564
         (* let _ = (
565
          *     Format.eprintf "Expr is %a@." Printers.pp_expr elem;
566
          *     match elem.expr_desc with
567
          *     | Expr_const _ -> Format.eprintf "a const@."
568
          *                     
569
          *     | Expr_ident _ -> Format.eprintf "an ident@."
570
          *     | _ -> Format.eprintf "something else@."
571
          *   )
572
          * in *)
573
         (build_switch_sys pos ((elem, true)::prefix))
574
         @
575
           (build_switch_sys neg ((elem, false)::prefix))
576
    )
577

    
578

    
579
      
580
(* Take a normalized node and extract a list of switches: (cond,
581
   update) meaning "if cond then update" where update shall define all
582
   node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *)
583
let node_as_switched_sys consts (mems:var_decl list) nd =
584
  (* rescheduling node: has been scheduled already, no need to protect
585
     the call to schedule_node *)
586
  let nd_report = Scheduling.schedule_node nd in
587
  let schedule = nd_report.Scheduling_type.schedule in
588
  let eqs, auts = Corelang.get_node_eqs nd in
589
  assert (auts = []); (* Automata should be expanded by now *)
590
  let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in
591
  let defs : (ident,  guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
592
  let add_def = add_def defs in
593

    
594
  let vars = Corelang.get_node_vars nd in
595
  (* Registering all locals variables as Z3 predicates. Will be use to
596
     simplify the expansion *) 
597
  let _ =
598
    List.iter (fun v ->
599
        let fdecl = Z3.FuncDecl.mk_func_decl_s
600
                      !ctx
601
                      v.var_id
602
                      []
603
                      (Zustre_common.type_to_sort v.var_type)
604
        in
605
        ignore (Zustre_common.register_fdecl v.var_id fdecl)
606
      ) vars
607
  in
608
  let _ =
609
    List.iter (fun c -> Hashtbl.add const_defs c.const_id c.const_value) consts
610
  in
611
  
612
  (* Registering node equations: identifying mem definitions and
613
     storing others in the "defs" hashtbl. *)
614
  let mem_defs =
615
    List.fold_left (fun accu eq ->
616
        match eq.eq_lhs with
617
        | [vid] ->
618
           (* Only focus on non memory definitions *)
619
           if not (List.exists (fun v -> v.var_id = vid) mems) then (
620
             report ~level:3 (fun fmt ->
621
                 Format.fprintf fmt "Registering variable %s@." vid);
622
             add_def vid eq.eq_rhs;
623
             accu
624
           )
625
           else
626
             (
627
               match eq.eq_rhs.expr_desc with
628
               | Expr_pre def_m ->
629
                  report ~level:3 (fun fmt ->
630
                      Format.fprintf fmt "Preparing mem %s@." vid);
631
                  (vid, rewrite defs def_m)::accu
632
               | _ -> assert false
633
             )
634
        | _ -> assert false (* should have been removed by normalization *)
635
      ) [] sorted_eqs
636
  in
637

    
638
  
639
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@.");
640
  (* Printing memories definitions *)
641
  report ~level:3
642
    (fun fmt ->
643
      Format.fprintf fmt
644
        "@[<v 0>%a@]@ "
645
        (Utils.fprintf_list ~sep:"@ "
646
           (fun fmt (m,mdefs) ->
647
             Format.fprintf fmt
648
               "%s -> [@[<v 0>%a@] ]@ "
649
               m
650
               (Utils.fprintf_list ~sep:"@ "
651
                  pp_guard_expr) mdefs
652
        ))
653
        mem_defs);
654
  
655
  let init_defs, update_defs =
656
    split_init mem_defs 
657
  in
658
  report ~level:3
659
    (fun fmt ->
660
      Format.fprintf fmt
661
        "@[<v 0>Init:@ %a@ Step@ %a@]@ "
662
        (Utils.fprintf_list ~sep:"@ "
663
           (fun fmt (m,mdefs) ->
664
             Format.fprintf fmt
665
               "%s -> @[<v 0>[%a@] ]@ "
666
               m
667
               (Utils.fprintf_list ~sep:"@ "
668
                  pp_guard_expr) mdefs
669
        ))
670
        init_defs
671
        (Utils.fprintf_list ~sep:"@ "
672
           (fun fmt (m,mdefs) ->
673
             Format.fprintf fmt
674
               "%s -> @[<v 0>[%a@] ]@ "
675
               m
676
               (Utils.fprintf_list ~sep:"@ "
677
                  pp_guard_expr) mdefs
678
        ))
679
        update_defs);
680

    
681
  let sw_init= 
682
    build_switch_sys init_defs []
683
  in
684
  let sw_sys =
685
    build_switch_sys update_defs []
686
  in
687
  clean_sys sw_init, clean_sys sw_sys