Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

runDirect.ml 22.1 KB
Newer Older
1
2
3
4

open LutExe
open LtopArg

5
type vars = (string * Data.t) list
6
7


8
(* returns a \ b *)
9
10
let list_minus a b =  List.filter (fun v -> not (List.mem v b)) a

11
(* returns a U b *)
12
13
let list_union a b =
  List.fold_left (fun acc x -> if (List.mem x acc) then acc else x::acc) a b
14

15
16
17
18
19
(* I defined mine because i need to know the seed that has been drawn by self_init. *)
let random_seed () =
  let () = Random.self_init () in
    Random.int 10000000

20
21
(* to be able to dump cov info if the exec is stopped by a ctrl-c. *)
let cov_ref = ref None
22
23
24
let gnuplot_pid_ref = ref None
let gnuplot_oc = ref None

25
(* Returns luciole io if necessary *)
26
27
let (check_compat : vars -> vars -> vars -> vars -> vars -> vars -> 
                    int * (vars * vars) option) =
28
29
30
31
32
33
  fun env_in env_out sut_in sut_out oracle_in oracle_out -> 
    (* cf lurette.set_luciole_mode_if_necessary to add a call to luciole *)
    
    let missing_sut_in = list_minus sut_in env_out
    and missing_env_in = list_minus env_in sut_out
    and missing_oracle_in = list_minus oracle_in (sut_out @env_out)  in
34
35
    let luciole_out = list_union missing_sut_in missing_env_in in 
    let luciole_in = list_minus (env_out@sut_out) luciole_out in 
36
      (*     let luciole_in = [] in  *)
37
      
38
39
40
    let vars_to_string vars = 
      String.concat "," (List.map (fun (n,t) -> n^":"^(Data.type_to_string t)) vars) 
    in
41
42
      if missing_sut_in <> [] then (
        let missing_str = vars_to_string missing_sut_in in
43
44
45
          Printf.printf "Some variables are missing in input of the SUT: %s\n" missing_str
      ) ;
      if missing_env_in <> [] then (
46
        let missing_str = vars_to_string missing_env_in in
47
48
49
          Printf.printf "Some variables are missing in input of lutin: %s\n" missing_str
      );
      if luciole_out <> [] then (
50
51
        Printf.printf "try with luciole!\n";
        0, Some(luciole_in,luciole_out)
52
53
54
      ) 
      else if missing_oracle_in <> [] then (
        let missing_str = vars_to_string missing_oracle_in in
55
56
          Printf.printf "Some variables are missing in input of the oracle: %s\n"
                        missing_str;
57
          2,None
58
59
      ) 
      else (
60
        if List.mem ("Step") (fst(List.split luciole_in)) then (
61
62
          Printf.printf
            "*** You cannot use the name 'Step' for a variable with lurette, sorry.\n";
63
64
65
66
67
          flush stdout;
          2,None
        ) else (
          Printf.eprintf "RP Variables are compatible.\n";
          flush stderr;
68
          0, if args.luciole_mode then Some(luciole_in, ["Step",Data.Bool]) else None
69
        )
70
71
      )

72
73
type ctx = Event.t
type e = Event.t
erwan's avatar
erwan committed
74

75
76
77
let rec (list_split: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i* 'j) list -> 
         'a list * 'b list * 'c list * 'd list * 'e list * 'f list
         * 'g list * 'h list * 'i list* 'j list) = 
erwan's avatar
erwan committed
78
  function
79
80
81
82
    | [] -> ([], [], [], [], [], [], [], [], [], [])
    | (x,y,z,t,u,v,w,a,b,c)::l ->
      let (rx, ry, rz, rt, ru, rv, rw, ra, rb, rc) = list_split l in
      (x::rx, y::ry, z::rz, t::rt, u::ru, v::rv, w::rw, a::ra, b::rb, c::rc)
erwan's avatar
erwan committed
83

84
open RdbgPlugin
85
let (make_rp_list : reactive_program list -> 
erwan's avatar
erwan committed
86
      vars list * vars list * (unit -> unit) list * (string -> unit) list * 
87
      (int -> unit) list * (int -> unit) list *
88
        (Data.subst list -> Data.subst list) list * 
89
        (Data.subst list -> ctx -> (Data.subst list -> ctx -> Event.t) ->
90
         Event.t) list * Data.subst list list * Data.subst list list) =
91
  fun rpl -> 
92
    let add_init init (a,b,c,d,e) = (a,b,c,d,e,init,init) in
93
    let aux rp = 
94
      let plugin =
95
        match rp with
96
(*           | LustreV6(prog,node) -> add_init [] (LustreRun.make_v6 prog node) *)
erwan's avatar
erwan committed
97
          | LustreV6(args) -> Lv6Run.make args
98
99
100
101
          | LustreV4(prog,node) -> LustreRun.make_v4 prog node
          | LustreEc(prog)      -> LustreRun.make_ec prog
          | LustreEcExe(prog)   -> LustreRun.make_ec_exe prog
          | Socket(addr, port)  -> LustreRun.make_socket addr port
102
          | SocketInit(addr, port) -> LustreRun.make_socket_init addr port 
103
          | Ocaml(cmxs) -> OcamlRun.make_ocaml cmxs
104
105
          | Lutin(args) -> LutinRun.make args
      in
106
107
108
109
      let ins, outs, reset, kill, save_state, restore_state, step, step_dbg,
          initin, initout =
        plugin.inputs,plugin.outputs,plugin.reset,plugin.kill,plugin.save_state,
        plugin.restore_state,plugin.step,plugin.step_dbg,
110
        plugin.init_inputs,plugin.init_outputs
111
112
113
      in
      let step = if args.debug_ltop then 
        let (string_of_subst : Data.subst -> string) =
114
          fun (str, v) -> str ^ "<-" ^ (Data.val_to_string Util.my_string_of_float v)
115
116
        in
        let sl2str sl = String.concat "," (List.map string_of_subst sl) in
117
118
119
120
121
122
          (fun sli  -> 
             let slo = step sli in
               Printf.eprintf "[%s] step(%s) = (%s) \n" 
                 (reactive_program_to_string rp) (sl2str sli) (sl2str slo);
               flush stderr;
               slo)
123
      else
124
125
        step 
      in
126
127
      ins, outs, reset, kill, save_state, restore_state, step, step_dbg,
      initin, initout     
128
    in
129
      list_split (List.map aux rpl)
130
    
131
132
133
134
135
136
137
138

type cov_opt = 
    NO (* NoOracle *) 
  | OO (* OracleOnly *) 
  | OC of Coverage.t
exception OracleError of string
exception SutStop of cov_opt

139
140
(* Transform a map on a function list into CPS *)
let (step_dbg_sl : 
141
142
  (Data.subst list -> ctx -> 
   (Data.subst list -> ctx -> Event.t) -> Event.t) list -> 
143
144
145
146
147
148
149
150
151
152
153
154
      's list -> 'ctx  -> ('s list -> 'e) -> 'e) = 
  fun step_dbg_sl_l sl ctx cont -> 
    (* ouch! Celle-la est chevelue...  
       La difficulté, c'est de passer un 'List.map step' en CPS.
       Suis-je aller au plus simple ? En tout cas j'ai réussit :)
    *)
    let rec (iter_step  : 
               ('s list -> 'ctx  -> ('s list -> 'ctx  -> 'e) -> 'e) list -> 
              's list list -> 's list -> 'e) = 
      fun stepl res_stepl sl ->
        match stepl with
          | [] -> cont (List.flatten (res_stepl))
155
156
          | step::stepl ->
             step sl ctx (fun res_sl ctx -> iter_step stepl (res_sl::res_stepl) sl)
157
158
159
160
161
    in
      iter_step step_dbg_sl_l [] sl 



162
let (start : unit -> Event.t) =
163
164
  fun () ->
    (* Get sut info (var names, step func, etc.) *)
165
    let _ = if args.debug_ltop then LustreRun.debug := args.debug_ltop in
166
167
168
    let sut_in_l, sut_out_l, sut_reset_l,sut_kill_l, sut_ss_l,
        sut_rs_l, sut_step_sl_l, sut_step_dbg_sl_l, 
        sut_init_in_l, sut_init_out_l = make_rp_list args.suts 
169
    in
erwan's avatar
erwan committed
170
    let sut_reset () = List.iter (fun f-> f ()) sut_reset_l in
171
172
    let sut_save_state i = List.iter (fun f-> f i) sut_ss_l in
    let sut_restore_state i = List.iter (fun f-> f i) sut_rs_l in
173
174
175
    let sut_kill msg = List.iter (fun f -> f msg) sut_kill_l in
    let sut_init_in = List.flatten sut_init_in_l in
    let sut_init_out = List.flatten sut_init_out_l in
176
177

    (* Get oracle info (var names, step func, etc.)*)
178
179
    let oracle_in_l, oracle_out_l, oracle_reset_l, oracle_kill_l, oracle_ss_l,
        oracle_rs_l, oracle_step_sl_l, 
180
        oracle_step_dbg_sl_l, _, _ =
181
      make_rp_list args.oracles
182
    in
183
    let oracle_kill msg = List.iter (fun f -> f msg) oracle_kill_l in
erwan's avatar
erwan committed
184
    let oracle_reset () = List.iter (fun f-> f ()) oracle_reset_l in
185
186
    let oracle_save_state i = List.iter (fun f-> f i) oracle_ss_l in
    let oracle_restore_state i = List.iter (fun f-> f i) oracle_rs_l in
erwan's avatar
erwan committed
187

188
    (* Get env info (var names, step func, etc.)*)
189
190
    let env_in_l, env_out_l, env_reset_l,env_kill_l, env_save_state_l,
        env_restore_state_l, env_step_sl_l, env_step_dbg_sl_l, 
191
      env_init_in_l, env_init_out_l = make_rp_list args.envs 
192
    in
erwan's avatar
erwan committed
193
    let env_reset () = List.iter (fun f-> f ()) env_reset_l in
194
    let env_kill msg = List.iter (fun f -> f msg) env_kill_l in
195
196
    let _env_init_in = Util.rm_dup (List.flatten env_init_in_l) in
    let _env_init_out = Util.rm_dup (List.flatten env_init_out_l) in
197
198
    let env_save_state i = List.iter (fun f-> f i) sut_ss_l in
    let env_restore_state i = List.iter (fun f-> f i) sut_rs_l in
erwan's avatar
erwan committed
199
200
201
202
203
    let reset () =
      if args.verbose > 0 then (
        Printf.eprintf "rdbgRun.start: resetting all RPs\n"; flush stderr);
      sut_reset (); env_reset (); oracle_reset ()
    in
204
205
206
207
208
209
    let save_state i =
      sut_save_state i; env_save_state i; oracle_save_state i
    in
    let restore_state i =
      sut_restore_state i; env_restore_state i; oracle_restore_state i
    in
210

211
    let vars_to_string l = 
212
213
214
      String.concat "\n" (List.map (fun (vn,vt) -> 
        let vt = Data.type_to_string vt in
        Printf.sprintf "\t%s:%s" vn vt) l)
215
    in
216
217
218
219
220
221
    let flat_sut_in  = Util.rm_dup (List.flatten sut_in_l)
    and flat_sut_out = Util.rm_dup (List.flatten sut_out_l)
    and flat_env_in  = Util.rm_dup (List.flatten env_in_l)
    and flat_env_out = Util.rm_dup (List.flatten env_out_l)
    and flat_oracle_in  = Util.rm_dup (List.flatten  oracle_in_l)
    and flat_oracle_out = Util.rm_dup (List.flatten  oracle_out_l)
222
    in
223
    let _ = if args.verbose > 0 then
224
225
226
227
228
        let sut_input_str = vars_to_string flat_sut_in in
        let sut_output_str = vars_to_string flat_sut_out in
        let env_input_str = vars_to_string  flat_env_in in
        let env_output_str = vars_to_string flat_env_out in
        let oracle_input_str = vars_to_string flat_oracle_in in
229
        let oracle_output_str_l = List.map vars_to_string oracle_out_l in
230
        Printf.printf "sut input : \n%s\n"  sut_input_str;
231
        Printf.printf "sut output : \n%s\n" sut_output_str;
232
233
        Printf.printf "env input : \n%s\n"  env_input_str;
        Printf.printf "env output : \n%s\n"  env_output_str;
234
        Printf.printf "oracle(s) input : \n%s\n"  oracle_input_str;
235
236
        List.iter (fun str -> Printf.printf "oracle output : \n%s\n" str) 
                  oracle_output_str_l;
237
        flush stdout
238
    in
239
    (* Check var names and types compat. *)
240
    let res_compat, luciole_io_opt = 
241
242
      check_compat flat_env_in flat_env_out flat_sut_in flat_sut_out 
                   flat_oracle_in flat_oracle_out 
243
244
245
246
247
    in
    let (luciole_kill, luciole_step), luciole_outputs_vars =
      match luciole_io_opt with
        | None -> ((fun _ -> ()),(fun _ -> [])),[]
        | Some (luciole_in, luciole_out) -> 
248
249
          (LustreRun.make_luciole "./lurette_luciole.dro" luciole_in luciole_out), 
          luciole_out
250
    in
251
252
    let seed =
      match args.seed with
253
254
255
        | None -> random_seed ()
        | Some seed -> seed
    in
256
257
    let cov_init = (* XXX faut-il renommer les sorties de l'oracle ou raler en 
                     cas de clash ? *)
258
259
      if List.flatten oracle_out_l = [] then NO else 
        let oracle_out = List.flatten (List.map List.tl oracle_out_l) in
260
        if List.length oracle_out < 1 then OO else 
261
          let is_bool (_,t) = (t = Data.Bool) in
262
263
264
          let names = List.filter is_bool oracle_out in
          let names = fst (List.split names) in
          OC (Coverage.init names args.cov_file args.reset_cov_file)
265
266
    in
    let oc = open_out args.output in
267
268
269
    let sim2chro_oc = 
      if args.display_sim2chro then Util2.sim2chro_dyn () else open_out "/dev/null" 
    in
270
271
    let filter vals vars = 
      List.map (fun (n,t) -> n, 
272
273
274
275
276
277
        try List.assoc n vals
        with Not_found -> 
          let vars_str = String.concat ", " (List.map (fun (n,_) -> n) vals) in
          let msg = Printf.sprintf "Don't find %s in %s\n" n vars_str in
          failwith msg
      ) vars 
278
    in
279
280
281
282

    let rec check_oracles oracle_in_vals i oracle_out_l oracle_out_vals_l cov =
      let check_one_oracle = function 
        | [] -> assert false
283
        | (_, Data.B true)::tail -> tail
284
          
285
        | (_, Data.B false)::tail ->
286
287
288
289
290
          let msg = 
            match cov with 
                OC cov -> Coverage.dump_oracle_io oracle_in_vals tail cov 
              | _ -> ""
          in
291
292
293
          let msg = 
            Printf.sprintf "\n*** The oracle returned false at step %i\n%s" i msg 
          in
294
295
296
          print_string msg;
          flush stdout;
          if args.stop_on_oracle_error then raise (OracleError msg) else tail
297
298

        | (vn, vv)::_  -> 
299
          let vv = Data.val_to_string_type vv in
300
301
302
          let msg = Printf.sprintf 
            "The oracle first output should be a bool; but %s has type %s" vn vv in
          failwith msg
303
      in
304
305
306
307
308
309
310
311
312
313
314
315
      match cov with 
          NO -> NO
        | OO -> ignore (List.map check_one_oracle oracle_out_vals_l); OO
        | OC cov -> 
          let ll = List.map check_one_oracle oracle_out_vals_l in
          let cov =
            List.fold_left
              (fun cov other_oracle_out_vals ->
                Coverage.update_cov other_oracle_out_vals cov) cov ll
          in
          cov_ref := Some cov;
          OC cov
316
    in
317
318
319
320
321
    let update_cov cov = 
      match cov with 
        | NO -> ()
        | OO -> ()
        | OC cov -> 
322
323
324
          let str =
            String.concat ", " (List.map reactive_program_to_string args.oracles) 
          in
325
          Coverage.dump str args.output cov
326
    in
327
    (* The main loop *)
328
329
330
331
332
333
334
335
336
    let killem_all cov = 
      env_kill "quit\n";
      sut_kill "quit\n";
      luciole_kill "quit\n";
      oracle_kill "quit\n";
      close_out oc;
      close_out sim2chro_oc;
      update_cov cov;
    in
337
    let rec loop cov env_in_vals pre_env_out_vals ctx i () =
338
339
      if i > args.step_nb then (killem_all cov; raise (Event.End 0) ) 
      else
340
341
        let luciole_outs = luciole_step (env_in_vals@pre_env_out_vals) in
        let env_in_vals =  List.rev_append luciole_outs env_in_vals in
342
343
344
345
346
347
348
349
        if args.ldbg then (* XXX l'idéal serait de faire ce test à
                             l'exterieur de la boucle en passant la
                             fonction qui va bien selon le
                             mode. Apres tout, c'est l'un des
                             avantages du CPS... *)
          let edata = env_in_vals@pre_env_out_vals in
          let ctx = 
            { ctx with 
350
351
352
353
              Event.step = i;
              Event.name = "ltop";
              Event.depth = 1;
              Event.data = edata;
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
            }
          in
          let cont = loop2 cov env_in_vals pre_env_out_vals ctx i luciole_outs in
          step_dbg_sl env_step_dbg_sl_l env_in_vals ctx cont
        else
          let env_step_sl sl = List.flatten (List.map (fun f -> f sl) env_step_sl_l) in
          let env_out_vals = env_step_sl env_in_vals in
          loop2 cov env_in_vals pre_env_out_vals ctx i luciole_outs env_out_vals
    (*
      {
      step = i;
      data = [];
      next = (fun () -> loop2 cov env_in_vals pre_env_out_vals i luciole_outs env_out_vals);
      terminate = (fun () -> killem_all cov)
      }
    *)          
370
    and
371
        loop2 cov env_in_vals pre_env_out_vals ctx i luciole_outs env_out_vals =
372
373
374
375
      let env_out_vals = 
        try List.map (fun (v,vt) -> v,List.assoc v env_out_vals) flat_env_out 
        with Not_found -> env_out_vals
      in
376
      let env_out_vals = luciole_outs @ env_out_vals in
377
      let sut_in_vals = filter env_out_vals flat_sut_in in        
378
379
380
      if args.ldbg then       
        let edata = sut_in_vals@ env_out_vals in
        let ctx = { ctx with 
381
382
383
384
          Event.step = i;
          Event.name = "ltop";
          Event.depth = 1;
          Event.data = edata;
385
386
        } 
        in
387
388
389
        let cont = 
          loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i luciole_outs
        in
390
391
392
393
        step_dbg_sl sut_step_dbg_sl_l sut_in_vals ctx cont
      else
        let sut_step_sl sl = List.flatten (List.map (fun f -> f sl) sut_step_sl_l) in
        let sut_out_vals = sut_step_sl sut_in_vals in
394
395
396
397
        loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i
              luciole_outs sut_out_vals
    and loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i 
              luciole_outs sut_out_vals =
398
399
400
      let sut_out_vals = 
        try List.map (fun (v,vt) -> v,List.assoc v sut_out_vals) flat_sut_out 
        with Not_found -> sut_out_vals
401
402
403
404
405
406
407
408
409
      in
      let oracle_in_vals = 
        if args.delay_env_outputs 
        then List.rev_append pre_env_out_vals sut_out_vals 
        else List.rev_append     env_out_vals sut_out_vals 
      in
      let oracle_in_vals = List.rev_append luciole_outs oracle_in_vals in
      let oracle_in_vals = filter oracle_in_vals flat_oracle_in in
      let oracle_out_vals_l = List.map (fun f -> f oracle_in_vals) oracle_step_sl_l in
410
411
412
413
414
415
416
417
418
419

      (*       let oracle_out_vals = List.flatten oracle_out_vals_l in *)
      let oracle_out_vals_l = 
        try List.map2 
              (fun oracle_out oracle_out_vals -> 
                List.map (fun (v,vt) -> v,List.assoc v oracle_out_vals) oracle_out
              ) 
              oracle_out_l
              oracle_out_vals_l
        with Not_found -> oracle_out_vals_l
420
      in
421
      let print_val (vn,vv) = Data.val_to_string Util.my_string_of_float vv in
422
      Printf.fprintf oc "#step %d\n" i;
423

424
425
      if args.delay_env_outputs then (
        output_string oc (String.concat " " (List.map print_val (pre_env_out_vals)));
426
427
        output_string 
          sim2chro_oc (String.concat " " (List.map print_val (pre_env_out_vals)));
428
429
430
431
432
433
434
435
      )
      else (
        output_string oc (String.concat " " (List.map print_val env_out_vals));
        output_string sim2chro_oc (String.concat " " (List.map print_val env_out_vals));
      );
      output_string oc (if env_out_vals <> [] then " #outs " else "#outs ");
      output_string oc (String.concat " " (List.map print_val sut_out_vals));
      output_string oc "\n";
436
437
438
439
440
      List.iter (fun l -> 
        output_string oc "#oracle_outs ";
        output_string oc (String.concat " " (List.map print_val l));
        output_string oc "\n";
      ) oracle_out_vals_l;
441
      flush oc;
442

443
444
445
446
447
      output_string sim2chro_oc "#outs ";
      output_string sim2chro_oc (String.concat " " (List.map print_val sut_out_vals));
      output_string sim2chro_oc "\n";
      flush sim2chro_oc;
      
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
      if not args.go && args.display_gnuplot then (
        if  i = 0 then (
          let oc, pid = 
            GnuplotRif.terminal := GnuplotRif.Wxt;
            GnuplotRif.verbose := args.verbose>1;
            GnuplotRif.dynamic := true;
            GnuplotRif.rif_file := args.output;
            GnuplotRif.f ()
          in
          gnuplot_pid_ref := Some pid;
          gnuplot_oc := Some oc
        ) 
        else 
          (match !gnuplot_oc with
            | None -> ()
            | Some oc -> output_string oc "replot\n"; flush oc)
      );
465
      if args.ldbg then (
466
        let edata = sut_out_vals@env_out_vals@(List.flatten oracle_out_vals_l) in
467
468
469
470
471
472
473
474
475
476
        let term () = 
          (match !gnuplot_pid_ref with
            | None -> ()
            | Some pid ->
              print_string "Killing gnuplot...\n"; flush stdout;
              Unix.kill pid Sys.sigkill;
              gnuplot_oc := None;
              gnuplot_pid_ref := None); 
          killem_all cov
        in
477
        let enb = ctx.Event.nb in
478
        let ctx = { ctx with 
479
480
481
482
483
484
          Event.nb = ctx.Event.nb+1;
          Event.step = i;
          Event.name = "ltop";
          Event.depth = 1;
          Event.data = edata;
          Event.terminate = term;
485
486
        } 
        in
487
        { ctx with 
488
          Event.nb = enb;
489
490
491
492
          Event.step = i;
          Event.kind = Event.Ltop;
          Event.depth = 1;
          Event.data = edata;
493
494
495
496
          Event.name = "rdbg";
          Event.lang = "";
          Event.inputs=[];
          Event.outputs=[];
497
          Event.locals = [];
498
          Event.sinfo=None;
499
500
501
502
503
          Event.next = 
            (fun () ->
              loop (check_oracles oracle_in_vals i oracle_out_l oracle_out_vals_l cov) 
                sut_out_vals env_out_vals ctx (i+1) () 
            );
erwan's avatar
erwan committed
504
505
          Event.terminate = term;
          Event.reset = ctx.Event.reset
506
507
508
509
510
        }
      )
      else
        loop (check_oracles oracle_in_vals i oracle_out_l oracle_out_vals_l cov) 
          sut_out_vals env_out_vals ctx (i+1) () 
511
    in
512

513
    let loc = None in
514
    let _ = 
515
516
      if args.compute_volume then Solver.set_fair_mode () 
      else Solver.set_efficient_mode ();
517
518
519
      !Solver.init_snt ();
      Random.init seed;

520
521
      Rif.write oc ("# This is lurette Version " ^ Version.str ^
                      " (\"" ^Version.sha^"\")\n");
522
523
      Rif.write oc ("#seed "^(string_of_int seed)^"\n");

524
      RifIO.write_interface oc 
525
        (luciole_outputs_vars@flat_env_out) flat_sut_out loc (Some oracle_out_l);
526
      Rif.flush oc;
527

528
      RifIO.write_interface sim2chro_oc 
529
        (luciole_outputs_vars@flat_env_out) flat_sut_out loc (Some oracle_out_l);
530
      Rif.flush sim2chro_oc;
531
532
    in
    let ctx =
533
      {
534
535
536
537
538
539
        Event.nb = 1;
        Event.step = 1;
        Event.name = "ltop";
        Event.depth = 1;
        Event.inputs = [];
        Event.outputs = [];
540
        Event.locals = [];
541
542
        Event.data = [];
        Event.terminate = (fun () -> killem_all cov_init);
erwan's avatar
erwan committed
543
        Event.reset = (fun () -> reset ());
544
545
        Event.save_state =  (fun i -> save_state i);
        Event.restore_state = (fun i -> restore_state i);
546
547
548
549
        Event.lang = "";
        Event.next = (fun () -> assert false);
        Event.kind = Event.Ltop;
        Event.sinfo = None;
550
551
      }
    in
552
    let (first_event : Event.t) =
553
554
555
      let res = 
        try 
          if res_compat = 0 then
556
            loop cov_init sut_init_out sut_init_in ctx 0 ()
557
558
559
560
          else 
            raise(Event.End res_compat) 
        with 
          | SutStop cov -> 
561
562
            print_string "The SUT stopped\n";
            flush stdout;
563
564
            update_cov cov;
            raise(Event.End 1)
565
566

          | OracleError str -> 
567
568
569
            print_string str;
            flush stdout;
            raise(Event.End 2)
570
571

          | Failure str -> 
572
            print_string ("Failure occured in lurette: "^str);
573
            flush stdout;
574
            raise(Event.End 2) 
575
          | Event.End i -> raise(Event.End (10*i))
576
          | e -> 
577
578
579
            print_string (Printexc.to_string e);
            flush stdout;
            raise(Event.End 2)
580
      in
581
      res
582
    in
583
    first_event
584

585
586
(* exported *)
let (clean_terminate : unit -> unit) =
587
588
  fun () -> 
    let str = String.concat ", " (List.map reactive_program_to_string args.oracles) in
589
590
591
592
593
594
595
596
597
598
599
600
    (match !cov_ref with 
      | None -> ()
      | Some cov -> Coverage.dump str args.output cov);
    (match !gnuplot_pid_ref with
      | None -> ()
      | Some pid ->
        print_string "Killing gnuplot...\n"; 
        flush stdout;
        Unix.kill pid Sys.sigkill;
        gnuplot_pid_ref := None
    )

601