ltopArg.ml 27.9 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
        
        (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
350 351
  let l = List.filter (fun (cmd,opt,arg) -> cmd<>"" || arg<>"" || opt <> "")
      (to_string args) in
352 353 354 355 356 357 358 359
  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  =
360 361
  let l = List.filter (fun (cmd,opt,arg) -> cmd<>"" || arg<>"" || opt <> "")
      (to_string args) in
362 363 364 365 366 367 368 369 370 371 372 373 374
  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
375 376 377 378 379 380 381 382 383 384

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

385

386 387
let (parse_rp_string : string -> unit) =
  fun str -> 
388 389 390 391 392 393
    (*     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] -> 
394 395 396 397 398 399 400 401
            (* 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 )
402
        | "lutin"::_ ->
403 404 405 406 407
            let rp_args = 
              (match args.seed with
                   None ->  rp_args
                 | Some i -> rp_args@["-seed";string_of_int i])
            in
408
            Lutin(Array.of_list rp_args )
409 410 411 412 413 414 415 416
                
        (*
          for lutin programs we accept:
          "lutin:toto.luc::"
          "lutin:toto.luc:toto:"
          "lutin:toto.luc:-main toto:"
        *)

417
        | "v6"::prog::node::opts -> 
erwan's avatar
erwan committed
418
            let args = ("lv6"::prog::"-node"::node::"--expand-io-type"::opts) in
419
            LustreV6(Array.of_list args)
420 421 422 423 424 425 426 427 428 429 430 431 432 433 434
        | ["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
435 436 437
(*     with *)
(*         e  -> failwith ("error in --reactive-program: " ^ Printexc.to_string e *)
(*                        ) *)
438 439


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

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
459
      | "ocaml" -> Some Ocamlopt
460 461 462 463 464 465 466 467 468 469 470
      | _ -> 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"
471
      | Ocamlopt -> "ocaml"
472

473

474 475 476 477 478 479 480 481 482 483 484 485 486 487
(************************************************************************)

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

488 489
let usage_out = Util.usage_out

490 491
(***********************************************************************)

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

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

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

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

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

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

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

    "--sut-compiler", Arg.String
      (fun s ->
544 545 546 547 548 549 550 551 552
	      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
553
      ),
554
    "<string> (lv4, lv6, scade)\t Compiler used for the sut [works with --old-mode only!].";
555 556 557

    "--oracle-compiler", Arg.String
      (fun s ->
558 559 560 561 562 563
	      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
564
      ),
565
    "<string> (lv4, lv6, or scade)\t Compiler used for the oracle [works with --old-mode only!].";
566

Erwan Jahier's avatar
Erwan Jahier committed
567 568 569 570 571 572 573 574 575 576 577 578 579
    "--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);

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

583 584 585
    "--seed", Arg.Int (fun s -> args.seed <- Some s),
    "<string>\tSet the seed provided to Lutin programs";

586
    "--reset-cov-file", Arg.Unit (fun _ -> args.reset_cov_file <- true),
587
    "";
588 589

    "--stop-on-oracle-error", Arg.Unit (fun _ -> args.stop_on_oracle_error <- true),
590
    "";
591 592

    "--test-length", Arg.Int (fun i -> args.step_nb <- i),
593
    "<int>\tNumber of steps to be done";
594 595 596
    "-l", Arg.Int (fun i -> args.step_nb <- i),
    ("<int>\t\t(currently, " ^ (string_of_int args.step_nb) ^ ").\n");

597 598 599 600
    (*     "--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"); *)
601 602 603 604 605 606 607


    "--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";


608
    "--fair", Arg.Unit (fun _ -> args.compute_volume <- true),
609
    ("\t\tCompute the polyhedra volumes before drawing: ");
610
    "--compute-poly-volume", Arg.Unit (fun _ ->  args.compute_volume <- true), 
611 612 613
    "more fair, but more expensive.\n";

    "--thick-draw", Arg.Int (fun i -> args.draw_nb <- i),
614
    "<int>\tNumber of draw to be done in each formula ";
615 616
    "-td", Arg.Int (fun i -> args.draw_nb <- i),
    ("<int>\t\tat each step (currently, " ^
617
       (string_of_int args.draw_nb) ^ ").\n");
618 619

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

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

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

    "--draw-all-formula", Arg.Unit (fun _ -> args.all_formula <- true),
629
    "\tTries all the formula reachable from the current state." ;
630
    "--draw-all-vertices", Arg.Unit (fun _ -> args.all_vertices <- true),
631
    "\tTries all the polyhedra vertices.\n" ;
632

633 634
    "--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";
635

636 637 638 639
    (* 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"); *)
640 641 642

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

646
    "--overwrite-output", Arg.Unit (fun () -> args.overwrite_output <- true),
647
    ("\tOverwrite \"" ^
648
       args.output ^ "\" if it exists without tring to invent a new name");
649 650
    "-oo", Arg.Unit (fun () -> args.overwrite_output <- true), "\n";

651
    "--batch", Arg.Unit (fun () -> args.go <- true),
652
    "\t\t\tStart the testing process directly, without prompting.";
653
    "--go", Arg.Unit (fun () -> args.go <- true), "\n";
654
    "-go", Arg.Unit (fun () -> args.go <- true), "\n";
655

656 657 658
    (*     "--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"; *)
659

660 661
    "--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";
662 663 664 665 666 667 668 669 670 671

    "--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" ;

672
    "--show-step", Arg.Unit (fun () -> args.show_step <- true),
673
    "\t\tSet on the show step mode.";
674

675
    "--do-not-show-step", Arg.Unit (fun () -> args.show_step <- false),
676
    "\tSet off the show step mode.\n";
677 678

    "--verbose", Arg.Int (fun i -> args.verbose <- i),
679
    "\t\tSet the verbose level.";
680 681
    "-v", Arg.Int( fun i -> args.verbose <- i),"\n";

682
    "--reactive", Arg.Unit (fun () -> args.reactive <- true),
683
    "\t\tSet on the reactive mode.";
684
    "-r", Arg.Unit (fun () -> args.reactive <- true),"\n";
685 686

    "--prompt", Arg.String (fun s -> args.prompt <- Some s),
687
    "\t\tReplace the default prompt.\n";
688 689 690

    "--extra-source-files", Arg.String
      (fun s ->
691 692 693 694
	      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";
695 696 697

    "--extra-libs", Arg.String
      (fun s ->
698 699 700
	      Unix.putenv "EXTRA_LIBS" (String.escaped s);
	      args.extra_libs <- Some s),
    "\t\tSet the EXTRA_LIBS environment variable.\n";
701 702 703

    "--extra-libdirs", Arg.String
      (fun s ->
704 705 706
	      Unix.putenv "EXTRA_LIBDIRS" (String.escaped s);
	      args.extra_libdirs <- Some s),
    "\tSet the EXTRA_LIBDIRS environment variable.\n";
707 708 709

    "--extra-includedirs", Arg.String
      (fun s ->
710 711 712
	      Unix.putenv "EXTRA_INCLUDEDIRS" (String.escaped s);
	      args.extra_includedirs <- Some s),
    "\tSet the EXTRA_INCLUDEDIRS environment variable.\n";
713 714 715

    "--step-mode", Arg.String
      (fun s -> 
716 717 718 719 720 721 722 723 724 725 726 727 728 729
	      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
730
      ),
731
    "\t\tSet the step mode used to perform the step.\n";
732

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

736 737 738 739
    "--luciole", Arg.Unit (fun _ -> args.luciole_mode <- true),
    "\t Call lurette via luciole.";

    "--pre-processor", Arg.String (fun s -> args.pp <- Some s),
740
    "\tPre-processor for Lucky files (e.g., cpp).";
741 742 743 744
    "-pp", Arg.String (fun s -> args.pp <- Some s), "\n";


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

    "--tmp-dir",  Arg.String 
      (fun s -> 
749 750 751
	      args.tmp_dir_provided <- Some s;
	      args.tmp_dir <- s;  
	      Unix.putenv "TMPDIR" s
752
      ),
753
    "\t\tUse that directory to put temporary files.\n";
754 755

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

758
    "--gnuplot", Arg.Unit (fun () -> args.display_gnuplot <- true),
759
    "\t\tCall gnuplot.";
760 761

    "--no-gnuplot", Arg.Unit (fun () -> args.display_gnuplot <- false),
762
    "\tDo not call gnuplot.";
763 764
    "-ngp", Arg.Unit (fun () -> args.display_gnuplot <- false), "\n";

765
    "--sim2chro", Arg.Unit (fun () -> args.display_sim2chro <- true),
766
    "\t\tCall sim2chro.";
767

768
    "--no-sim2chro", Arg.Unit (fun () -> args.display_sim2chro <- false),
769
    "\tDo not call sim2chro.";
770
    "-ns2c", Arg.Unit (fun () -> args.display_sim2chro <- false), "\n";
771

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

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

778

779
    "--ocaml-version", Arg.Unit (fun _ -> (print_string (Sys.ocaml_version^"\n") ; exit 0)),
780
    "\t\tDisplay the version ocaml version lurette was compiled with and exit." ;
781 782

    "--version", Arg.Unit (fun _ -> (print_string (Version.str^"-"^Version.sha) ; exit 0)),
783
    "\t\tDisplay the version and exit." ;
784
    "-version", Arg.Unit (fun _ -> (print_string (Version.str^"-"^Version.sha) ; exit 0)),
785
    "" ;
786
    "-v", Arg.Unit (fun _ -> (print_string (Version.str^"-"^Version.sha) ; exit 0)),
787
    "" ;
788 789


790
    "--help", Arg.Unit (fun _ -> (usage_out speclist usage ; exit 0)),
791
    "\t\tDisplay this list of options." ;
792
    "-help", Arg.Unit (fun _ -> (usage_out speclist usage ; exit 0)),
793
    "";
794
    "-h", Arg.Unit (fun _ -> (usage_out speclist usage ; exit 0)),
795
    ""
796
  ]
797 798 799 800 801 802 803

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

804