ltopArg.ml 27.8 KB
Newer Older
1
2

let usage = "
3
usage: lurettetop [<options>]
4
5
6
7

lurettetop is a top level loop that let one use lurette.
Type help and/or man at the prompt for more info.

8
launch 'lurettetop --help' to see the available options.
9
10
"

11
12
let rp_help =" 
  To specify a reactive program to be used in the test session, one should
13
  use a string with the following format: \"machine_kind:language:file:node\" 
14
      where:
15
     - machine_kind can be : 'sut', 'oracle', or 'env'
16
17
18
19
20
21
22
     - language can be : 
        + 'v4'     to use the Lustre V4 programs
        + 'v6'     to use the Lustre V6 programs
        + 'lutin'  to use the Lutin programs
        + 'ocaml'  to use the Ocaml programs [ocaml]
        + 'ec'     to use the ec programs
        + 'ec_exe' to use a standalone executable obtained from an .ec file [ex_exe] 
23
24
25
     - file should be an existing file (compatible with the ''compiler'' field)
     - node should be a node of file (if meaningful) or empty

26
27
28
29
30
  [ocaml] In the 'ocaml' mode, the file can be an f.ml file, or a f.cmxs file.
  If an ml file is provided, lurettetop try to generate a cmxs file from it.
  If your caml program depends on library, or on other files, please generate
  the f.cmxs file by yourself (cf the ocaml documentation).

31
  [ec_exe] In the 'ec_exe' mode, lurette suppose that 'file.ec' has been compiled
32
33
34
35
36
  into an executable that is named 'file' (for instance, via ec2c -loop). 
  That executable must read/write its I/O using the RIF convention.
  The rationale for that mode is to be able to deal with Lustre programs that
  use C code. The 'file.ec' is just used to retrieve the I/O var names 
  and types actually.
37
38
39
40
41
42

  An alternative format is the following: \"machine_kind:socket:sock_addr:port\" where
     - machine_kind is as above
     - sock_addr is a valid internet adress
     - port is a free port on sock_addr

43
  The lurettetop process play the role of the client ; exchanges on the socket
44
45
  should respect the RIF (Reactive Input Format).

46
  Hence, to sum-up, we currently support:
47
48
49

  \"<sut|env|oracle>:lutin:prog:node\"        For lutin programs
  \"<sut|env|oracle>:v6:prog:node\"           For lustre V6 programs
50
  \"<sut|env|oracle>:v4:prog:node\"           For lustre V4 programs
51
  \"<sut|env|oracle>:ec:prog:\"               For lustre expanded code programs
52
  \"<sut|env|oracle>:ec_exe:prog:\"           For lustre expanded code programs that have been compiled
53
  \"<sut|env|oracle>:socket:addr:port\"       For reactive programs that read/write on a socket
54
  \"<sut|env|oracle>:socket_init:addr:port\"  Ditto + read I/O init values before the first step
55
56
57

    Examples: 
     \"sut:v6:controler.lus:main\"
58
     \"env:lutin:train.lut:tgv\" 
59
     \"oracle:socket:127.0.0.0:2042\" 
60
61
62
63
64
65
66
67
68
69
70
 
   If one needs to pass other options, one just need to add it 
   at the end of the rp, separating options by ':'. 
   
   For instance, if the train.lut requires an extern dynamic library
   libm.so, one would need to pass the option \"-L libm.so\" to the 
   Lutin interpreter. In order to do the same from lurettetop, 
   one would write:
    
      \"env:lutin:train:tgv:-L:libm.so\" 
"
71
72

(* compiler used to compiler sut and oracles *)
73
(* XXX obselete soon! *)
74
type compiler = VerimagV4 | VerimagV6 | Scade | ScadeGUI | Sildex | Stdin | Ocamlopt
75
76

type step_mode = | Inside | Edges | Vertices
77
78
79
80
let step_mode_to_string = function
  | Inside -> "--step-inside"
  | Edges -> "--step-edges"
  | Vertices -> "--step-vertices"
81
82
83

type verbose_level = int

84
85
86
87
88
type program_kind = SUT | Env | Oracle | PK_error of string


type reactive_program =
  | LustreV4 of string * string 
89
  | LustreV6 of string array
90
  | LustreEc of string
91
  | LustreEcExe of string
92
  | Lutin of string array
93
  | Socket of string * int
94
  | SocketInit of string * int
95
  | Ocaml of string 
96
97
98
99
100

let program_kind_of_string = function
  | "sut" -> SUT
  | "oracle" -> Oracle
  | "env" -> Env
101
  | s -> PK_error("*** Error: Unsupported kind of reactive program: \""^s ^"\"")
102
103
104
105
106
107
108
109
110

let program_kind_to_string = function
  | SUT -> "sut"
  | Oracle ->  "oracle"
  | Env -> "env"
  | PK_error msg -> "Error:" ^ msg

let reactive_program_to_string = function
  | LustreV4(f,node) -> "v4:"^f^":"^node
111
  | LustreV6(args) -> "v6:"^(String.concat ":" (Array.to_list args))
112
  | LustreEc(f) -> "ec:"^f^":"
113
  | LustreEcExe(f) -> "ec_exe:"^f^":"
114
  | Lutin(args)  -> "lutin:"^(String.concat ":" (Array.to_list args))
115
  | Socket(addr,port) -> "socket:"^addr^":"^(string_of_int port)
116
  | SocketInit(addr,port) -> "socket_init:"^addr^":"^(string_of_int port)
117
  | Ocaml(str) -> "ocaml:" ^ str
118
type t = {
119
120
121
122
123
124

  mutable suts : reactive_program list ;
  mutable envs : reactive_program list ;
  mutable oracles : reactive_program list ;


125
(* Obselete !!!! *)
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
  mutable sut_cmd : string ;
  mutable oracle_cmd : string ;
  mutable sut : string ;
  mutable sut_node : string ;
  mutable oracle : string option ;
  mutable oracle_node : string ;
  mutable env : string;
  mutable env_node : string ;
  mutable sut_compiler : compiler ;
  mutable oracle_compiler : compiler ;

  mutable step_nb : int;
  mutable draw_nb : int ;

  mutable draw_inside : int ;
  mutable draw_edges : int ;
  mutable draw_vertices : int ;
  mutable all_formula : bool ;
  mutable all_vertices : bool ;

  mutable step_mode : step_mode;
  mutable luciole_mode : bool;
148
  mutable delay_env_outputs : bool;
149

150
151
152
  mutable step_by_step : int option ; 
  mutable display_local_var : bool ;
  mutable display_sim2chro : bool;
153
  mutable display_gnuplot : bool;
154
155
156
  mutable seed : int option ;
  mutable precision : int ;
  mutable verbose : verbose_level ;
157
158
  mutable reactive : bool ;
  mutable show_step : bool ;
159
  mutable output : string ;
160
161
  mutable overwrite_output : bool;

162
163
164
165
166
167
  mutable make_opt : string ;
  mutable prompt : string option ;
  mutable extra_cfiles : string option ;
  mutable extra_libs : string option ;
  mutable extra_libdirs : string option ;
  mutable extra_includedirs : string option ;
168
  mutable go : bool ;
169
170
171
172
  mutable restore : string option;
(* this is a flag to know whether lurette needs to be (re-)build *)
  mutable prefix : string ;
  mutable sut_dir : string ;
173
  mutable compute_volume : bool;
174
175
176
177
178
  mutable pp : string option;
  mutable tmp_dir : string;
  mutable tmp_dir_provided : string option;
  mutable c_generator : string;

179
  mutable direct_mode : bool;
180
181
182
183
184
185
  mutable root_node : string; (* different from the sut_node sensible only for the scade gui *)
  mutable log : bool;
  mutable scade_gui : bool;
  mutable socket_inet_addr : string option; (* if None, we use stdin/stdout *)
  mutable socket_port : int option;
  mutable socket_err_port : int option;
186
  mutable debug_ltop : bool;
187
  mutable ldbg : bool;
188
189
190
191
192
  
  mutable cov_file : string;
  mutable reset_cov_file : bool;
  mutable stop_on_oracle_error : bool;

193
194
195
196
197
198
199
200
201
202
(* 
   I am using references for that in order to be able to replace them
   by sockets if necessary (i.e., once the sockets are connected) *)
  mutable icr : Pervasives.in_channel;
  mutable ocr : Pervasives.out_channel;
  mutable ecr : Pervasives.out_channel;
}


let (args : t) = {
203
204
205
206
  suts = [];
  oracles= [];
  envs = [];

207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
  oracle_cmd = "" ;
  sut_cmd = "" ;
  sut = "" ;  
  sut_node = "" ;
  oracle = None ;
  oracle_node = "" ;
  env = "";
  env_node = "";
  sut_compiler = VerimagV6;
  oracle_compiler = VerimagV6;
  make_opt = "nc" ;
  step_nb = 10;
  draw_nb  = 1 ;
  draw_inside = 0 ;
  draw_edges = 0 ;
  draw_vertices = 0 ;
  all_formula = false ;
  all_vertices = false ;
  step_mode = Inside ;
  luciole_mode = false;
227
  delay_env_outputs = false;
228
229
  step_by_step = None ;
  show_step = false ;
230
  display_local_var = false ;
231
  display_sim2chro = true ;
232
  display_gnuplot = true ;
233
234
235
  seed = None ;
  precision = 2;
  verbose = 0 ;
236
  reactive = false ;
237
  output = "lurette.rif" ;
238
  overwrite_output = false;
239
240
241
242
243
  prompt = None ;
  extra_cfiles = None ;
  extra_libs = None ;
  extra_libdirs = None ;
  extra_includedirs = None ;
244
  go = false ;
245
246
247
  restore = None ;
  prefix = "";
  sut_dir = ".";
248
  compute_volume = false;
249
250
251
252
253
  pp = None;
  tmp_dir = ".";
  tmp_dir_provided = None;
  c_generator = "";

254
  direct_mode = true;
255

256
257
258
259
260
261
  root_node = "";
  log = false;
  scade_gui = false;
  socket_inet_addr = None;
  socket_port = None;
  socket_err_port = None;
262
  debug_ltop = false;
263
  ldbg = false;
264

265
266
267
268
  cov_file = "lurette.cov";
  reset_cov_file = false;
  stop_on_oracle_error = false;
 
269
270
271
272
273
  ocr =  stdout;
  icr =  stdin;
  ecr =  stderr;
}

274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
(* exported 
   usefull to generete batch file and .lurette_rc files
*)
let (to_string : t -> (string * string * string) list) = 
  fun args -> 
    let rp_to_string rp kind = (" \"" ^kind^":" ^ (reactive_program_to_string rp) ^ "\"") in
    let soi = string_of_int in
    let bool_opt b x1 x2 = if b then (x1,x2,"") else "","","" in
    let quote str = "\"" ^ str ^"\"" in
      (List.map (fun rp -> "add_rp", "-rp", rp_to_string rp "sut") args.suts) @
      (List.map (fun rp -> "add_rp", "-rp", rp_to_string rp "env") args.envs) @
      (List.map (fun rp -> "add_rp", "-rp", rp_to_string rp "oracle") args.oracles) @
      [
        "stl ", "--test-length", soi args.step_nb;
        
        "set_draw_nb",           "--thick-draw", soi args.draw_nb;
        "set_draw_inside",       "--draw-inside", soi args.draw_inside;
        "set_draw_edges",        "--draw-edges", soi args.draw_edges;
        "set_draw_vertices",     "--draw-vertices", soi args.draw_vertices;

        bool_opt args.direct_mode  "set_direct_mode"  "--direct";
295
        bool_opt (not args.direct_mode)  "set_old_mode"  "--old-mode";
296
297
298
299
        bool_opt args.all_formula  "set_draw_all_formula"  "--draw-all-formula";
        bool_opt args.all_vertices "set_draw_all_vertices" "--draw-all-vertices";

        bool_opt args.display_local_var "set_display_local_var true" "--local-var";
300
301
        bool_opt (not args.display_sim2chro) "set_display_sim2chro" "--no-sim2chro";
        bool_opt (not args.display_gnuplot) "set_display_gnuplot" "--no-gnuplot";
302
303
304
305

        bool_opt args.log "log" "--log";
        bool_opt args.compute_volume "set_fair_mode" "--compute-poly-volume";

306
307
        bool_opt args.stop_on_oracle_error "stop_on_oracle_error true" "--stop-on-oracle-error";        
        bool_opt args.debug_ltop  "set_dbg_on"  "--dbg";
308
309
        bool_opt args.ldbg  "set_ldbg_on"  "--ldbg";

310

311
312
313
        "set_verbose", "--verbose", soi args.verbose ;
        "set_precision", "--precision" , soi args.precision;
        "set_rif", "--output", args.output;
314
        bool_opt args.overwrite_output "set_overwrite_output" "--overwrite-output" ;
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
        
        (match args.step_by_step with
           | None -> "set_step_by_step_off", "", ""
           | Some i -> "set_step_by_step", "--step", soi i);

        (match args.seed with
           | None -> "set_seed_randomly", "", ""
           | Some i -> "set_seed", "-seed", soi i);
        (match args.extra_cfiles with
           | None -> "","",""
           | Some str -> "set_extra_cfiles", "--extra-source-files", quote str) ;
        (match args.extra_libs with
           | None -> "","",""
           | Some str -> "set_extra_libs", "--extra-libs", quote str) ;
        (match args.extra_libdirs with
           | None -> "","",""
           | Some str -> "set_extra_libdirs", "--extra-libdirs", quote str) ;

        (match args.extra_includedirs with
           | None -> "","",""
           | Some str -> "set_extra_includedirs", "--extra-includirs", quote str) ;


        "set_cov_file", "--cov-file ", quote args.cov_file;

        (match args.step_mode with
             Inside  -> "set_step_mode", "--step-mode", "inside"
           | Edges  -> "set_step_mode", "--step-mode", "edges"
           | Vertices -> "set_step_mode", "--step-mode", "vertices"
        )

      ]

let gen_lurette_rc () =
  let oc = open_out ".lurette_rc" in
  let l = List.filter (fun (cmd,opt,arg) -> cmd<>"" || arg<>"" || opt <> "") (to_string args) in
  let l = List.map (fun (cmd, _, arg) -> cmd ^ " " ^ arg ^ "\n") l in
    List.iter (output_string oc) l;
    flush oc;
    output_string args.ecr ("'.lurette_rc' has been updated.\n");
    flush args.ecr;
    close_out oc

let gen_lurettetop_call args  =
  let l = List.filter (fun (cmd,opt,arg) -> cmd<>"" || arg<>"" || opt <> "") (to_string args) in
  let l = List.map (fun (_, opt, arg) -> opt ^ " " ^ arg ^ " ") l in
    String.concat "" l

let gen_batch file =
  let file = if file = "" then "lurette.batch" else file in
  let oc = open_out (Filename.concat args.sut_dir file) in
  let str = gen_lurettetop_call args in
    output_string oc "lurettetop -go ";
    output_string oc str;
    flush oc;
    output_string args.ecr ("The batch file " ^ file ^ " has been created.\n");
    flush args.ecr;
    close_out oc
373
374
375
376
377
378
379
380
381
382

let string_to_step_mode = function
  | "inside" -> Inside
  | "edges" -> Edges
  | "vertices" -> Vertices
  | _ ->
      output_string args.ocr "\n Warning: bad step mode. ";
      flush args.ocr;
      Inside

383

384
385
let (parse_rp_string : string -> unit) =
  fun str -> 
386
387
388
389
390
391
    (*     try *)
    let l = (Str.split (Str.regexp ":") str) in
    let rp_args = List.tl l in
    let rp = 
      match rp_args with
        | ["lutin";prog; node] -> 
392
393
394
395
396
397
398
399
            (* for backward compatibility, i add the 'main' in necessary... *)
            let rp_args = ("lutin"::prog::"-main"::node::[]) in
            let rp_args = 
              (match args.seed with
                   None ->  rp_args
                 | Some i -> rp_args@["-seed";string_of_int i])
            in
                Lutin(Array.of_list rp_args )
400
        | "lutin"::_ ->
401
402
403
404
405
406
            let rp_args = 
              (match args.seed with
                   None ->  rp_args
                 | Some i -> rp_args@["-seed";string_of_int i])
            in
                Lutin(Array.of_list rp_args )
407
408
409
410
411
412
413
414
                
        (*
          for lutin programs we accept:
          "lutin:toto.luc::"
          "lutin:toto.luc:toto:"
          "lutin:toto.luc:-main toto:"
        *)

415
        | "v6"::prog::node::opts -> 
erwan's avatar
erwan committed
416
            let args = ("lv6"::prog::"-node"::node::"--expand-io-type"::opts) in
417
            LustreV6(Array.of_list args)
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
        | ["ec_exe"; prog] -> LustreEcExe(prog)
        | ["ec"; prog] -> LustreEc(prog)
        | ["ec"; prog; _] -> LustreEc(prog)
        | ["v4"; prog; node] -> LustreV4(prog, node)
        | ["ocaml"; cmxs] -> Ocaml(cmxs)
        | ["socket"; addr; port] -> Socket(addr, int_of_string port)
        | ["socket_init"; addr; port] -> SocketInit(addr, int_of_string port)
        | _ -> failwith ("*** Error: Unsupported kind of reactive program: \""
                         ^ str ^ "\"\n" ^ rp_help)
    in
      match program_kind_of_string (List.hd l) with
        | SUT -> if not (List.mem rp args.suts) then args.suts <- rp::args.suts
        | Env -> if not (List.mem rp args.envs) then args.envs <- rp::args.envs
        | Oracle -> if not (List.mem rp args.oracles) then args.oracles <- rp::args.oracles
        | PK_error msg -> failwith msg
433
434
435
(*     with *)
(*         e  -> failwith ("error in --reactive-program: " ^ Printexc.to_string e *)
(*                        ) *)
436
437


438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456

let (string_to_compiler:string -> compiler option) =
  fun s ->
    match s with
      | "verimag" -> Some VerimagV4
      | "Verimag" -> Some VerimagV4
      | "lv4" -> Some VerimagV4
      | "v4" -> Some VerimagV4
      | "lv6" -> Some VerimagV6
      | "v6" -> Some VerimagV6
      | "scade-gui" -> Some ScadeGUI
      | "scade_gui" -> Some ScadeGUI
      | "scade" ->   Some Scade
      | "Scade" ->   Some Scade
      | "sildex" ->   Some Sildex
      | "Sildex" ->   Some Sildex
      | "stdin/stdout" -> Some Stdin
      | "stdin" -> Some Stdin
      | "Stdin" -> Some Stdin
457
      | "ocaml" -> Some Ocamlopt
458
459
460
461
462
463
464
465
466
467
468
      | _ -> None

let (compiler_to_string : compiler -> string) =
  fun c ->
    match c with
      | VerimagV4 -> "lv4"
      | VerimagV6 -> "lv6"
      | Scade -> "scade"
      | ScadeGUI -> "scade-gui"
      | Sildex -> "sildex"
      | Stdin -> "stdin"
469
      | Ocamlopt -> "ocaml"
470

471

472
473
474
475
476
477
478
479
480
481
482
483
484
485
(************************************************************************)

let (get_full_path: string -> string -> string) =
  fun dir str ->
    (* str is supposed to be a blank separated list of files. If those files
       have no path, explicitely append it the one of the user directory. *)
    let l0 = Util2.string_to_string_list str in
    let l1 =
      List.map
	(fun s -> if  (Filename.is_relative s) then (Filename.concat dir s) else s)
	l0
    in
      List.fold_left (fun acc s -> acc ^ s ^ " ") "" l1

486
487
let usage_out = Util.usage_out

488
489
(***********************************************************************)

Erwan Jahier's avatar
Erwan Jahier committed
490
491
let old_speclist = [
   "--sut", Arg.String
492
      (fun file -> args.sut <- file),
493
    "<string>\tFile name of the system under test [works with --old-mode only!].";
494
495
    "-sut", Arg.String
      (fun file -> args.sut <-  file),
496
    " <string>\n" ;
497
498
499

    "--sut-cmd", Arg.String
      (fun cmd -> args.sut_cmd <- cmd),
500
    "<string>\tCommand that launches the system under test [works with --old-mode only!].";
501
502
    "-sut-cmd", Arg.String
      (fun cmd -> args.sut_cmd <- cmd),
503
    " <string>\n" ;
504
505
506

    "--oracle-cmd", Arg.String
      (fun cmd -> args.oracle_cmd <- cmd),
507
    "<string>\tCommand that launches the oracle [works with --old-mode only!].";
508
509
    "-oracle-cmd", Arg.String
      (fun cmd -> args.oracle_cmd <- cmd),
510
    " <string>\n" ;
511
512
513

    "--main-sut-node", Arg.String
      (fun s -> args.sut_node <- s),
514
    "<string>\tMain node name of the system under test [works with --old-mode only!].";
515
516
    "-msn", Arg.String
      (fun s -> args.sut_node <- s),
517
    " <string>\n" ;
518
519
520

    "--main-env-node", Arg.String
      (fun s -> args.env_node <- s),
521
    "<string>\tMain node name of the environment (meaningful for lutin only) [works with --old-mode only!].";
522
523
    "-men", Arg.String
      (fun s -> args.env_node <- s),
524
    " <string>\n" ;
525
526

    "--oracle", Arg.String (fun file -> args.oracle <- 
527
528
			                     Some (file)),
    "<string>\tFile name of the oracle [works with --old-mode only!].";
529
    "-oracle", Arg.String (fun file -> args.oracle <- 
530
			                    Some (file)),
531
532
533
534
    " <string>\n";

    "--main-oracle-node", Arg.String
      (fun s -> args.oracle_node <- s),
535
    "<string>\tMain node name of the oracle [works with --old-mode only!].";
536
537
    "-man", Arg.String
      (fun s -> args.oracle_node <- s),
538
    " <string>\n" ;
539
540
541

    "--sut-compiler", Arg.String
      (fun s ->
542
543
544
545
546
547
548
549
550
	      match (string_to_compiler s) with
	          Some ScadeGUI -> 
	            args.sut_compiler <- ScadeGUI;
	            args.scade_gui <- true
	        | Some comp -> args.sut_compiler <- comp
	        | None ->
	            output_string args.ocr (s ^ " is not a supported compiler.\n");
	            flush args.ocr;
	            exit 2
551
      ),
552
    "<string> (lv4, lv6, scade)\t Compiler used for the sut [works with --old-mode only!].";
553
554
555

    "--oracle-compiler", Arg.String
      (fun s ->
556
557
558
559
560
561
	      match (string_to_compiler s) with
	          Some comp -> args.oracle_compiler <- comp
	        | None ->
	            output_string args.ocr (s ^ " is not a supported compiler.\n");
	            flush args.ocr;
	            exit 2
562
      ),
563
    "<string> (lv4, lv6, or scade)\t Compiler used for the oracle [works with --old-mode only!].";
564

Erwan Jahier's avatar
Erwan Jahier committed
565
566
567
568
569
570
571
572
573
574
575
576
577
    "--direct", Arg.Unit (fun () -> args.direct_mode <- true),
    "\tSet the direct mode.\n" ;
    "--old-mode", Arg.Unit (fun () -> args.direct_mode <- false),
    "\tUnset the direct mode.\n" 
]

let rec speclist =
  [
    "--reactive-program", Arg.String (fun str -> parse_rp_string str),
    "<string>.";    
    "-rp", Arg.String (fun str -> parse_rp_string str),
    ("<string> " ^ rp_help);

578
579
580
581
    "--cov-file", Arg.String (fun s -> args.cov_file <- s),
    "<string>\tfile name coverage info will be put into";

    "--reset-cov-file", Arg.Unit (fun _ -> args.reset_cov_file <- true),
582
    "";
583
584

    "--stop-on-oracle-error", Arg.Unit (fun _ -> args.stop_on_oracle_error <- true),
585
    "";
586
587

    "--test-length", Arg.Int (fun i -> args.step_nb <- i),
588
    "<int>\tNumber of steps to be done";
589
590
591
    "-l", Arg.Int (fun i -> args.step_nb <- i),
    ("<int>\t\t(currently, " ^ (string_of_int args.step_nb) ^ ").\n");

592
593
594
595
    (*     "--thick-form", Arg.Int (fun i -> args.formula_nb <- i), *)
    (*        "<int>\tNumber of formula to be drawn at each step"; *)
    (*     "-tf", Arg.Int (fun i -> args.formula_nb <- i),  *)
    (*     ("<int>\t\t(currently, " ^ (string_of_int args.formula_nb) ^ ").\n"); *)
596
597
598
599
600
601
602


    "--precision", Arg.Int (fun i -> args.precision <- i),
    "<int>\tnumber of digit after the dot used for floating points.\n" ;
    "-p", Arg.Int (fun i -> args.precision <- i), " <int>\n";


603
    "--fair", Arg.Unit (fun _ -> args.compute_volume <- true),
604
    ("\t\tCompute the polyhedra volumes before drawing: ");
605
    "--compute-poly-volume", Arg.Unit (fun _ ->  args.compute_volume <- true), 
606
607
608
    "more fair, but more expensive.\n";

    "--thick-draw", Arg.Int (fun i -> args.draw_nb <- i),
609
    "<int>\tNumber of draw to be done in each formula ";
610
611
    "-td", Arg.Int (fun i -> args.draw_nb <- i),
    ("<int>\t\tat each step (currently, " ^
612
       (string_of_int args.draw_nb) ^ ").\n");
613
614

    "--draw-inside", Arg.Int (fun i -> args.draw_inside <- i),
615
    "<int>\tDraw on the edges of the convex hull of solutions.";
616
617

    "--draw-edges", Arg.Int (fun i -> args.draw_edges <- i),
618
    "<int>\tDraw on the edges of the convex hull of solutions.";
619
620

    "--draw-vertices", Arg.Int (fun i -> args.draw_vertices <- i),
621
    "<int>\tDraw among the vertices of the convex hull of solutions.\n ";
622
623

    "--draw-all-formula", Arg.Unit (fun _ -> args.all_formula <- true),
624
    "\tTries all the formula reachable from the current state." ;
625
    "--draw-all-vertices", Arg.Unit (fun _ -> args.all_vertices <- true),
626
    "\tTries all the polyhedra vertices.\n" ;
627

628
629
    "--dbg", Arg.Unit (fun () -> args.debug_ltop <- true), " debug mode (to debug lurettetop)\n";
    "-ldbg", Arg.Unit (fun () -> args.ldbg <- true), " use the lurette debugger \n";
630

631
632
633
634
    (* This option is not meant to be available to end-users...  *)
    (*     "--make-opt", Arg.String (fun s -> args.make_opt <- s),  *)
    (*     ("<string>\tOptions to call make with when building \n" ^  *)
    (*      "\t\t\tlurette (currently, \"" ^ args.make_opt ^ "\").\n"); *)
635
636
637

    "--output", Arg.String (fun s -> args.output <- s),
    ("<string>\tSet the output file name (currently,  \"" ^
638
       args.output ^ "\").");
639
640
    "-o", Arg.String (fun s -> args.output <- s), "<string>\n";

641
    "--overwrite-output", Arg.Unit (fun () -> args.overwrite_output <- true),
642
    ("\tOverwrite \"" ^
643
       args.output ^ "\" if it exists without tring to invent a new name");
644
645
    "-oo", Arg.Unit (fun () -> args.overwrite_output <- true), "\n";

646
    "--batch", Arg.Unit (fun () -> args.go <- true),
647
    "\t\t\tStart the testing process directly, without prompting.";
648
    "--go", Arg.Unit (fun () -> args.go <- true), "\n";
649
    "-go", Arg.Unit (fun () -> args.go <- true), "\n";
650

651
652
653
    (*     "--restore", Arg.String (fun s -> args.restore <- Some s), *)
    (*        "<string>\tFile name of the package containing" *)
    (*        ^ "\n\t\t\tthe temporarily files to be restored (cf the pack command).\n"; *)
654

655
656
    "--step", Arg.Int (fun i -> args.step_by_step <- Some i), "\t\tRun lurette step by step." ;
    "-s", Arg.Int (fun i -> args.step_by_step <- Some i), "\n";
657
658
659
660
661
662
663
664
665
666

    "--socket-inet-addr", Arg.String (fun i -> args.socket_inet_addr <- Some i),
    "\t\tSet the socket address.\n" ;

    "--socket-io-port", Arg.Int (fun i -> args.socket_port <- Some i),
    "\t\tSet the socket io port.\n" ;

    "--socket-err-port", Arg.Int (fun i -> args.socket_err_port <- Some i),
    "\t\tSet the socket error port.\n" ;

667
    "--show-step", Arg.Unit (fun () -> args.show_step <- true),
668
    "\t\tSet on the show step mode.";
669

670
    "--do-not-show-step", Arg.Unit (fun () -> args.show_step <- false),
671
    "\tSet off the show step mode.\n";
672
673

    "--verbose", Arg.Int (fun i -> args.verbose <- i),
674
    "\t\tSet the verbose level.";
675
676
    "-v", Arg.Int( fun i -> args.verbose <- i),"\n";

677
    "--reactive", Arg.Unit (fun () -> args.reactive <- true),
678
    "\t\tSet on the reactive mode.";
679
    "-r", Arg.Unit (fun () -> args.reactive <- true),"\n";
680
681

    "--prompt", Arg.String (fun s -> args.prompt <- Some s),
682
    "\t\tReplace the default prompt.\n";
683
684
685

    "--extra-source-files", Arg.String
      (fun s ->
686
687
688
689
	      Unix.putenv "EXTRA_SOURCE_FILES" (String.escaped (get_full_path (Sys.getcwd ()) s));
	      args.extra_cfiles <- Some (get_full_path (Sys.getcwd ()) s)),
	 
    "\t\tSet the EXTRA_SOURCE_FILES environment variable.\n";
690
691
692

    "--extra-libs", Arg.String
      (fun s ->
693
694
695
	      Unix.putenv "EXTRA_LIBS" (String.escaped s);
	      args.extra_libs <- Some s),
    "\t\tSet the EXTRA_LIBS environment variable.\n";
696
697
698

    "--extra-libdirs", Arg.String
      (fun s ->
699
700
701
	      Unix.putenv "EXTRA_LIBDIRS" (String.escaped s);
	      args.extra_libdirs <- Some s),
    "\tSet the EXTRA_LIBDIRS environment variable.\n";
702
703
704

    "--extra-includedirs", Arg.String
      (fun s ->
705
706
707
	      Unix.putenv "EXTRA_INCLUDEDIRS" (String.escaped s);
	      args.extra_includedirs <- Some s),
    "\tSet the EXTRA_INCLUDEDIRS environment variable.\n";
708
709
710

    "--step-mode", Arg.String
      (fun s -> 
711
712
713
714
715
716
717
718
719
720
721
722
723
724
	      let m = 
	        match s with
	          | "Inside" -> Inside
	          | "inside" -> Inside
	          | "Edges" -> Edges
	          | "edges" -> Edges
	          | "Vertices" -> Vertices
	          | "vertices" -> Vertices
	          | _ -> 
		           output_string args.ocr (s ^ " is not a valid step mode.\n");
		           flush args.ocr;
		           exit 2
	      in
	        args.step_mode <- m
725
      ),
726
    "\t\tSet the step mode used to perform the step.\n";
727

728
729
730
    "--delay-env-outputs", Arg.Unit (fun _ -> args.delay_env_outputs <- true),
    "\t Delay the outputs of the environements before transmitting them to the oracles.";

731
732
733
734
    "--luciole", Arg.Unit (fun _ -> args.luciole_mode <- true),
    "\t Call lurette via luciole.";

    "--pre-processor", Arg.String (fun s -> args.pp <- Some s),
735
    "\tPre-processor for Lucky files (e.g., cpp).";
736
737
738
739
    "-pp", Arg.String (fun s -> args.pp <- Some s), "\n";


    "--prefix", Arg.String (fun s -> args.prefix <-  s),
740
    "\t\tA string to append before the call to lurette (e.g., \"/usr/bin/times \").\n";
741
742
743

    "--tmp-dir",  Arg.String 
      (fun s -> 
744
745
746
	      args.tmp_dir_provided <- Some s;
	      args.tmp_dir <- s;  
	      Unix.putenv "TMPDIR" s
747
      ),
748
    "\t\tUse that directory to put temporary files.\n";
749
750

    "--log",  Arg.Unit (fun _ -> args.log <- true),
751
    "\t\tRedirect stdout to a log file (lurette_stdout.log)\n";
752

753
    "--gnuplot", Arg.Unit (fun () -> args.display_gnuplot <- true),
754
    "\t\tCall gnuplot.";
755
756

    "--no-gnuplot", Arg.Unit (fun () -> args.display_gnuplot <- false),
757
    "\tDo not call gnuplot.";
758
759
    "-ngp", Arg.Unit (fun () -> args.display_gnuplot <- false), "\n";

760
    "--sim2chro", Arg.Unit (fun () -> args.display_sim2chro <- true),
761
    "\t\tCall sim2chro.";
762

763
    "--no-sim2chro", Arg.Unit (fun () -> args.display_sim2chro <- false),
764
    "\tDo not call sim2chro.";
765
    "-ns2c", Arg.Unit (fun () -> args.display_sim2chro <- false), "\n";
766

767
    "--local-var", Arg.Unit (fun () -> args.display_local_var <- true),
768
    "\t\tDisplay environment local variables in sim2chro (on).";
769

770
    "--no-local-var", Arg.Unit (fun () -> args.display_local_var <- false),
771
    "\tDo not display environment local variables in sim2chro.\n" ;
772

773

774
    "--ocaml-version", Arg.Unit (fun _ -> (print_string (Sys.ocaml_version^"\n") ; exit 0)),
775
    "\t\tDisplay the version ocaml version lurette was compiled with and exit." ;
776
777

    "--version", Arg.Unit (fun _ -> (print_string (Version.str^"-"^Version.sha) ; exit 0)),
778
    "\t\tDisplay the version and exit." ;
779
    "-version", Arg.Unit (fun _ -> (print_string (Version.str^"-"^Version.sha) ; exit 0)),
780
    "" ;
781
    "-v", Arg.Unit (fun _ -> (print_string (Version.str^"-"^Version.sha) ; exit 0)),
782
    "" ;
783
784


785
    "--help", Arg.Unit (fun _ -> (usage_out speclist usage ; exit 0)),
786
    "\t\tDisplay this list of options." ;
787
    "-help", Arg.Unit (fun _ -> (usage_out speclist usage ; exit 0)),
788
    "";
789
    "-h", Arg.Unit (fun _ -> (usage_out speclist usage ; exit 0)),
790
    ""
791
  ]
792
793
794
795
796
797
798

let (explicit_the_file : string -> string) =
  fun s -> 
    if Filename.is_implicit s
    then (Filename.concat args.sut_dir s)
    else s

799