lurettetop.ml 26.8 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
(*pp camlp4o *)
(*-----------------------------------------------------------------------
** Copyright (C) 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
**
** File: lurettetop.ml
** Main author: jahier@imag.fr
*)

12

13
14
15
16
17
18
19
20
21
22
(** lurette toplevel loop. *)

let usage = "
usage: lurettetop [<options>] [<env ([x] env)*>]

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

Command line <options> are:
"
23
type draw_mode = Verteces | Edges | Inside
24
25
26
27
28
29
30
31

type flagT = {
  mutable sut : string ;  
  mutable oracle : string option ;
  mutable env : string ;
  mutable step_nb : int;
  mutable formula_nb : int ;
  mutable draw_nb : int ;
32
  mutable draw_mode : draw_mode ;
33
34
35
36
37
  mutable step_by_step : bool ref ;
  mutable display_local_var : bool ref ;
  mutable display_sim2chro : bool ref;
  mutable seed : int option ;
  mutable verbose : bool ref ;
38
  mutable show_step : bool ref ;
39
40
  mutable output : string ;
  mutable make_opt : string ;
41
  mutable prompt : string option ;
42
  mutable go : bool ref ;
43
  mutable restore : string option;
44
(* a flag to know whether lurette_exe needs to be (re-)build *)
45
46
47
48
  mutable to_build : bool ref ;
  mutable prefix : string
  

49
50
51
52
53
54
55
}


let (flag : flagT) = {
  sut = "" ;
  oracle = None ;
  env = "";
56
  make_opt = "nc" ;
57
58
59
  step_nb = 10;
  formula_nb = 1 ;
  draw_nb  = 1 ;
60
  draw_mode = Inside ;
61
  step_by_step = ref false ;
62
  show_step = ref false ;
63
64
65
66
67
  display_local_var = ref true ;
  display_sim2chro = ref true ;
  seed = None ;
  verbose = ref false ;
  output = "lurette.rif" ;
68
  prompt = None ;
69
  go = ref false ;
70
  restore = None ;
71
72
  to_build = ref true;
  prefix = ""
73
74
75
76
}

let rec speclist = 
  [
77
78
79
80
81
82
83
    "--sut", Arg.String 
      (fun s -> 
	 let file = 
	   try Filename.chop_extension s
	   with Invalid_argument _ -> s
	 in 
	   flag.sut <- file), 
84
       "<string>\tFile name of the system under test (without extension).";
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
    "-sut", Arg.String 
      (fun s ->
	 let file = 
	   try Filename.chop_extension s
	   with Invalid_argument _ -> s
	 in 
	   flag.sut <- file), 
      " <string>\n" ;

    "--oracle", Arg.String (fun s -> 
	 let file = 
	   try Filename.chop_extension s
	   with Invalid_argument _ -> s
	 in 
	   flag.oracle <- Some file), 
100
       "<string>\tFile name of the oracle (without extension).";
101
102
103
104
105
106
107
    "-oracle", Arg.String (fun s -> 
	 let file = 
	   try Filename.chop_extension s
	   with Invalid_argument _ -> s
	 in 
	   flag.oracle <- Some file), 
    " <string>\n";
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124

    "--test-length", Arg.Int (fun i -> flag.step_nb <- i),
       "<int>\tNumber of steps to be done";
    "-l", Arg.Int (fun i -> flag.step_nb <- i),  
    ("<int>\t\t(default=" ^ (string_of_int flag.step_nb) ^ ").\n");

    "--thick-form", Arg.Int (fun i -> flag.formula_nb <- i),
       "<int>\tNumber of formula to be drawn at each step";
    "-tf", Arg.Int (fun i -> flag.formula_nb <- i), 
    ("<int>\t\t(default=" ^ (string_of_int flag.formula_nb) ^ ").\n");

    "--thick-draw", Arg.Int (fun i -> flag.draw_nb <- i),
       "<int>\tNumber of draw to be done in each formula ";
    "-td", Arg.Int (fun i -> flag.draw_nb <- i),
    ("<int>\t\tat each step (default=" ^ 
     (string_of_int flag.draw_nb) ^ ").\n");
    
125
    "--draw-inside", Arg.Unit (fun _ -> flag.draw_mode <- Inside),
126
       "\tDraw on the edges of the convex hull of solutions.\n ";
127
128

    "--draw-edges", Arg.Unit (fun _ -> flag.draw_mode <- Edges),
129
       "\t\tDraw on the edges of the convex hull of solutions.\n ";
130

131
    "--draw-verteces", Arg.Unit (fun _ -> flag.draw_mode <- Verteces),
132
       "\tDraw among the verteces of the convex hull of solutions.\n ";
133
134


135
136
137
138
    "--seed", Arg.Int (fun i -> flag.seed <- Some i),
       "<int>\t\tSeed the random engine is init with." ;
    "-seed", Arg.Int (fun i -> flag.seed <- Some i), " <int>\n";

139
(* This option is not meant to be available to end-users...  *)
140
141
    "--make-opt", Arg.String (fun s -> flag.make_opt <- s), 
    ("<string>\tOptions to call make with when building \n" ^ 
142
     "\t\t\tlurette (default=\"" ^ flag.make_opt ^ "\").\n");
143
144
145
146
147
148
149
150
151
152

    "--output", Arg.String (fun s -> flag.output <- s),
    ("<string>\tSet the output file name (default is \"" ^ 
    flag.output ^ "\").");
    "-o", Arg.String (fun s -> flag.output <- s), "<string>\n";

    "--go", Arg.Set flag.go, 
    "\t\t\tStart the testing process directly without prompting.";
    "-go", Arg.Set flag.go, "\n";

153
    "--restore", Arg.String (fun s -> flag.restore <- Some s), 
154
       "<string>\tFile name of the package containing"
155
       ^ "\n\t\t\tthe temporarily files to be restored (cf the pack command).\n";
156

157
158
159
    "--step", Arg.Set flag.step_by_step, "\t\tRun lurette step by step." ;
    "-s", Arg.Set flag.step_by_step, "\n";

160
161
162
    "--show-step", Arg.Set flag.show_step,
       "\t\tSet on the show step mode."; 

163
164
165
    "--do-not-show-step", Arg.Clear flag.show_step,
       "\t\tSet off the show step mode."; 

166
167
168
169
    "--verbose", Arg.Set flag.verbose,
       "\t\tSet on the verbose mode.";
    "-v", Arg.Set flag.verbose,"\n";

170
171
172
    "--prompt", Arg.String (fun s -> flag.prompt <- Some s), 
       "\t\tReplace the default prompt.\n";

173
174
175
    "--prefix", Arg.String (fun s -> flag.prefix <-  s), 
       "\t\tstring to append before the call to lurette (e.g., \"/usr/bin/times \").\n";

176

177
    "--sim2chro", Arg.Set flag.display_sim2chro,
178
       "\t\tCall sim2chro when lurette resumes.\n";
179
180

    "--no-sim2chro", Arg.Clear flag.display_sim2chro,
181
       "\tDo not call sim2chro when lurette resumes.";
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
    "-ns2c", Arg.Clear flag.display_sim2chro, "\n";

    "--local-var", Arg.Set flag.display_local_var,
       "\t\tDisplay environment local variables in sim2chro (default).";

    "--no-local-var", Arg.Clear flag.display_local_var,
       "\tDo not display environment local variables in sim2chro.\n" ;

    "--help", Arg.Unit (fun _ -> (Arg.usage speclist usage ; exit 0)),
       "\t\tDisplay this list of options." ;
    "-help", Arg.Unit (fun _ -> (Arg.usage speclist usage ; exit 0)),
    "";
    "-h", Arg.Unit (fun _ -> (Arg.usage speclist usage ; exit 0)),
    ""
]



200
201
let (build : string -> string -> string -> bool) =
  fun user_dir lurette_tmp_dir lurette_dir ->
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
    let sut = 
      if Filename.is_relative flag.sut 
      then (user_dir ^ flag.sut) 
      else flag.sut 
    in
      if not (Sys.file_exists (sut ^ ".lus"))
      then
	(
	  output_string stdout ("*** File " ^ sut ^ 
				".lus does not exist.\n");
	  flush stdout;
	  false
	)
      else
	(
	  output_string stderr "  building lurette ...\n";
	  flush stderr;
	  if (flag.sut = "" or flag.env = "")
	  then
	    (
	      print_string "*** 
223
224
  Both the sut and the env fields should be filled
  with set_sut and set_env commands respectively.\n ";
225
226
227
228
229
230
231
232
233
234
235
236
237
	      false
	    )
	  else
	    let (oracle, oracle2) =  
	      match flag.oracle 
	      with 
		  None -> "", (lurette_tmp_dir ^ "/always_true") 
		| Some str -> 
		    let str2 = 
		      if Filename.is_relative str then (user_dir ^ str) else str 
		    in
		      (str2, str2)
	    in
238
	    let make_cmd = 
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
	      ("make -I " ^ user_dir ^ " -f " 
	       ^ lurette_dir ^ "/Makefile.lurette " ^ flag.make_opt ^ "> make_lurette.log \n")
	    in
	      if oracle2 <>  (lurette_tmp_dir ^ "/always_true")
		&& not (Sys.file_exists (oracle2 ^ ".lus"))
	      then
		(
		  output_string stdout ("*** File " ^ oracle2 ^ 
					".lus does not exist.\n");
		  flush stdout;
		  false
		)
	      else
		(
		  Unix.putenv "SUT" (sut ^ ".c");
		  Unix.putenv "ORACLE" (oracle2 ^ ".c");
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
		  try 
		    Util.gen_stubs sut oracle ;
		    output_string stderr make_cmd ;
		    flush stderr ;
		    flush stdout;
		    if 
		      ((Sys.command make_cmd) <> 0)
		    then 
		      false
		    else 
		      (
			output_string stderr "   ...make ok.\n";
			true
		      )
		  with Failure e -> 
270
		    (
271
272
273
		      output_string stdout e ;
		      flush stdout ;
		      false
274
275
276
		    )
		)
	)
277
	
278
279
(* run lurette and returns the exit status *)
let (run : string -> int) =
280
  fun lurette_tmp_dir ->
281
282
283
284
285
    let seed_str = 
      match flag.seed with 
	  None -> "" 
	| Some i -> (" -seed " ^ (string_of_int i))
    and verb_str = if !(flag.verbose) then " -v" else ""
286
    and show_step_str = if !(flag.show_step) then " --show-step" else ""
287
288
289
290
291
    and draw_mode_str = 
      match flag.draw_mode with
	  Inside -> " "
	| Edges -> " --draw-edges"
	| Verteces -> " --draw-verteces" 
292
293
294
295
296
297
298
299
300
301
    and orac_str = 
      match flag.oracle with 
	  None -> " --no-oracle" 
	| Some str -> ""
    and outp_str = (" -o " ^ flag.output)
    and step_str = if !(flag.step_by_step) then " -s" else ""
    and sim2_str = if !(flag.display_sim2chro) then " --call-sim2chro" else " -ns2c"
    and dlvr_str = 
      if !(flag.display_local_var) then " --display-local-var " else " -nlv "
    in
302
    let times0 = Unix.times () in
303
    let run                                                                                                                                                                                       _cmd =
304
      (flag.prefix ^ " " ^ lurette_tmp_dir ^ "/lurette " ^ 
305
306
      (string_of_int flag.step_nb) ^ " " ^
      (string_of_int flag.formula_nb) ^ " " ^
307
308
309
      (string_of_int flag.draw_nb) ^ " " ^ 
       draw_mode_str ^ seed_str ^ verb_str ^ show_step_str ^ orac_str ^ 
       outp_str ^ step_str ^ sim2_str ^ dlvr_str ^ flag.env
310
      )
311
    in
312
313
314
    let result =
      output_string stderr (run_cmd ^ "\n");
      flush stderr;
315
      Sys.command run_cmd
316
317
318
319
320
321
322
323
324
325
326
327
    in
      if result = 0 then
	(
	  let times1 = Unix.times () in
	  let times = 
	    times1.Unix.tms_cutime
	    +.times1.Unix.tms_cstime
	    -.times0.Unix.tms_cutime
	    -.times0.Unix.tms_cstime
	  in
	  let times_str = string_of_float times in
	    output_string stdout 
328
	      ("\nThe execution lasted " ^ times_str ^ " second" ^ 
329
330
331
332
333
334
335
336
	       (if times > 1. then "s" else "") ^ ".\n" ^
	       "********************************************************************\n");
	    flush stdout;
	    result
	)
	else
	  result
     
337
338
339
340
341
342
343
344
345
type cmd =
    Sut of string
  | Oracle of string
  | MakeOpt of string
  | Env of string
  | StepNb of int
  | FormulaNb of int
  | DrawNb of int
  | Step of bool
346
  | DisplaySim2chro of bool
347
  | DisplayLocalVar of bool
348
  | StepByStep of bool
349
  | Seed of int
350
  | RandomSeed
351
  | Verbose of bool
352
  | ShowStep of bool
353
  | Output of string
354
  | CallSim2chro
355
356
357
  | Build
  | Clean
  | Run
358
359
360
  | DrawInside
  | DrawEdges
  | DrawVerteces
361
362
363
  | Quit
  | Help
  | Man
364
  | Prompt of string
365
  | Prefix of string
366
  | Pack of string
367
  | Show
368
369
370
371
372
373
374
  | HelpSimple
  | Error of string

let lexer = Genlex.make_lexer []

type tok = Genlex.token Stream.t

375
376
377
378
379
380
381
382
383
384
385
386
387

let (remove_extension : string -> string) =
  fun str -> 
    let file_ext = Filename.basename str
    and dir  = Filename.dirname str in
    let file = try Filename.chop_extension file_ext with _ -> file_ext in
      (Filename.concat dir file)

let _ = assert ((remove_extension "../toto/tutu.lus") = "../toto/tutu")
let _ = assert ((remove_extension "/home/toto/tutu.lus") = "/home/toto/tutu")
let _ = assert ((remove_extension "home/toto/tutu.lus") = "home/toto/tutu")
let _ = assert ((remove_extension "home/toto/tutu") = "home/toto/tutu")

388
389
390
391
392
let rec 
  (read_cmd : tok -> cmd) =
  fun tok -> 
    match tok with parser
      | [< 'Genlex.Ident "run" >] -> Run
393
      | [< 'Genlex.Ident "r" >] -> Run
394
      | [< 'Genlex.Ident "b" >] -> Build
395
      | [< 'Genlex.Ident "build" >] -> Build
396
397
398
399
400
401
402
403
404
      | [< 'Genlex.Ident "set_draw_mode" ;'Genlex.Ident id >] -> 
	  (
	    match id with 
		"inside" -> DrawInside
	      | "edges"  -> DrawEdges
	      | "verteces" -> DrawVerteces
	      | _ -> Error ("Unknown draw mode (" ^ id ^ ")\n")
	  )
      | [< 'Genlex.Ident "show" >] -> Show
405
      | [< 'Genlex.Ident "clean" >] -> Clean
406
      | [< 'Genlex.Ident "set_prompt"; 'Genlex.String str >] -> Prompt(str)
407
      | [< 'Genlex.Ident "set_prefix"; 'Genlex.String str >] -> Prefix(str)
408
409
      | [< 'Genlex.Ident "set_env" ; 'Genlex.String str >] -> Env(str)
(*       | [< 'Genlex.Ident "set_env" ; str = parse_env >] -> Env(str) *)
410
411
      | [< 'Genlex.Ident "set_sut" ; str = parse_file_name >] -> Sut(str)
      | [< 'Genlex.Ident "set_oracle" ; str = parse_file_name >] -> Oracle(str)
412
413
414
415
416
      | [< 'Genlex.Ident "set_make_opt" ; 'Genlex.Ident str >] -> MakeOpt(str)
      | [< 'Genlex.Ident "set_test_length" ; 'Genlex.Int i >] -> StepNb(i)
      | [< 'Genlex.Ident "set_formula_nb" ; 'Genlex.Int i >] -> FormulaNb(i)
      | [< 'Genlex.Ident "set_draw_nb" ; 'Genlex.Int i >] -> DrawNb(i)
      | [< 'Genlex.Ident "set_seed" ; 'Genlex.Int i >] -> Seed(i)
417
      | [< 'Genlex.Ident "set_seed_randomly" >] -> RandomSeed
418

419
420
421
422
423
      | [< 'Genlex.Ident "set_step_by_step" ; 'Genlex.Ident str >] -> 
	  if List.mem str ["t";"true"] 
	  then StepByStep(true)
	  else StepByStep(false)

424
425
426
427
      | [< 'Genlex.Ident "set_display_sim2chro" ; 'Genlex.Ident str >] -> 
	  if List.mem str ["t";"true"] 
	  then DisplaySim2chro(true)
	  else DisplaySim2chro(false)
428
429
430
431
432
433
434
435
436
437
      | [< 'Genlex.Ident "set_display_local_var" ; 'Genlex.Ident str >] -> 
	  if List.mem str ["t";"true"] 
	  then DisplayLocalVar(true)
	  else DisplayLocalVar(false)

      | [< 'Genlex.Ident "set_verbose" ; 'Genlex.Ident str >] -> 
	  if List.mem str ["t";"true"] 
	  then Verbose(true)
	  else Verbose(false)

438
439
440
441
442
      | [< 'Genlex.Ident "set_show_step" ; 'Genlex.Ident str >] -> 
	  if List.mem str ["t";"true"] 
	  then ShowStep(true)
	  else ShowStep(false)

443
      | [< 'Genlex.Ident "set_output" ; str = parse_file_name>] -> Output(str ^ ".rif")
444
      | [< 'Genlex.Ident "sim2chro" >] -> CallSim2chro
445
446
447
448
449
450
451
452

      | [< 'Genlex.Ident "quit"  >] -> Quit
      | [< 'Genlex.Ident "q"  >] -> Quit
      | [< 'Genlex.Ident "bye"  >] -> Quit
      | [< 'Genlex.Ident "exit"  >] -> Quit

      | [< 'Genlex.Ident "man"  >] -> Man

453
454
      | [< 'Genlex.Ident "pack"  ; 'Genlex.Ident file >] -> Pack(file)

455
456
457
458
459
460
      | [< 'Genlex.Ident "help"  >] -> Help
      | [< 'Genlex.Ident "h"  >] -> Help
      | [< 'Genlex.Ident "?"  >] -> Help
      | [< 'Genlex.Ident _ >]  -> Error "Unknown command.\n"
      | [<   >] -> HelpSimple

461
462
463
464
465
and  
  (parse_file_name : tok -> string) = 
  fun tok -> 
    try
      match tok with parser 
466
467
	| [<  'Genlex.String str >] -> 
	    if str = "" then "" else remove_extension str 
468
	| [<  'Genlex.Ident id  >] -> id
469
	| [<  >]  ->  "" 
470
471
      with _ -> 
	print_string 
472
473
474
	   "*** parse error: cannot parse that file name.\n";
	flush stdout;
	""
475
and  
476
  (parse_env : tok -> string) = 
477
478
  fun tok -> 
    try
479
480
481
482
      (
	match tok with parser 
	  | [<  'Genlex.Ident "x" ; tail = parse_env >] -> (" x " ^ tail)
	  | [<  'Genlex.String str ; tail = parse_env >] -> 
483
484
	      ((remove_extension str) ^ ".luc " ^ tail) 
	  | [<  'Genlex.Ident id  ; tail = parse_env >] -> (id ^ ".luc " ^ tail)
485
486
487
488
489
490
491
492
493
494
	  | [< _ >]  ->  "" 
      )
    with e -> 
      print_string (Printexc.to_string e);
      print_string 
         "*** Error when parsing the environment field.\n";
      flush stdout;
      ""
	
	
495

496
let cmd_usage = "  Type h for help, or man for a small user manual.
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
"

let man = "
Once lurettetop has been run, a prompt is printed waiting for 
user queries. One first need at least to set the sut (system 
under test) and the environement fields like that:

    [your shell prompt] lurettetop  
    <lurette> set_sut my_program_to_test
    <lurette> set_oracle my_oracle
    <lurette> set_env my_env_file1 my_env_file2 x my_env_file3

And then the testing process can start:

    <lurette> run
       ... [test, test, test, ...]
   
Equivalently, you can directly set values at the command line:

    [your shell prompt] lurettetop --sut my_program_to_test  \\
                          --oracle my_oracle \\
                          my_env_file1 my_env_file2 x my_env_file3
    <lurette> run
       ... [test, test, test, ...]
"

	
let (display_cmd : unit -> unit) = 
  fun _ -> 
    let msg =  "The commands are: 

528
run, r
529
     to start the testing process. Note that the sut and the environment
530
531
     fields (described below) should be set.

532
quit q, bye  
533
534
535
536
537
538
539
540
541
542
543
544
     to quit the lurette top level


help, h, ?
     display this list of commands

man
     display a small user manual

clean
     run a make clean (you can try it if <<run>> failed)

545
546
547
548
549
pack <file_name>
     package up in <file_name>.tgz files created in a temporary 
     directory. This file can then be given in argument of the 
     <<--restore>> option of lurettetop so that they are not 
     computed again.
550
551
552
553

show
    show of post-script version of the current environment

554

555
set_env  \"<env ([x] env)*>\"  (env=<file name>)                   
556
     to set the environment field (.luc files). Automata of
557
558
559
560
561
562
563
     environments separated by \"x\" are multiplied.
     The current value of this field is "
	       ^ 
	       (if flag.env = "" 
		then "UNSET!" 
		else ("\"" ^ flag.env ^ "\" ")) ^ "

564
set_sut  <file name>            
565
566
567
     to set the sut field. Its current value is " ^ 
	       (if flag.sut = "" 
		then "UNSET!" 
568
		else("\"" ^ flag.sut ^ "\"")) ^ "
569

570
set_oracle  <file name>      
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
     to set the oracle field. Its current value is " ^ 
	       (match flag.oracle with
		    None ->  "unset" 
		  | Some str -> ("\"" ^ str ^ "\"")) ^ "
    
set_test_length  <integer>
     to set the test length. Its current value is \"" ^ 
	       (string_of_int flag.step_nb) ^ "\"

set_formula_nb  <integer>                      
     to set the number of formula to be drawn at each step. Its current 
     value is \"" 
	       ^ (string_of_int flag.formula_nb) ^ "\"

set_draw_nb  <integer>
     to set the number of draw to be done in each formula at each step
     Its current value is \"" ^ (string_of_int flag.draw_nb) ^ "\"

589
590
591
592
593
594
595
596
597
598
599
set_draw_mode <draw_mode>
    set the draw mode, which can be either be inside, edges, or verteces.
    - inside : draw inside the convex hull of solutions.
    - edges : draw on the edges of the convex hull of solutions.
    - verteces : draw among the verteces of the convex hull of solutions.
    Its current mode is \"" ^ (match flag.draw_mode with
			    	 Inside -> "inside"
			       | Edges -> "edges"
			       | Verteces -> "verteces" 
			    ) ^ "\".

600
601
602
603
604
set_seed  <integer>
     to set the seed the random engine is initialised with.
     Its current value is " ^ (match flag.seed with
			       None ->  "chose randomly" 
			     | Some i -> ("\"" ^ (string_of_int i) ^ "\""))  ^ "
605
606
607

set_seed_randomly
     to the system set a seed randomly.
608
609
610
611
612
613
614
615
616
  
set_step_by_step  <boolean>
     to set a flag saying whether or not the test should proceed step
     by step. Its current value is " ^ (if !(flag.step_by_step) 
			   then "\"true\""
			   else "\"false\"") ^ "

set_display_sim2chro  <boolean>
     to set a flag saying whether or not sim2chro is called when 
617
       lurette resumes. Its current value is " 
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
	       ^ (if !(flag.display_sim2chro)
			   then "\"true\""
			   else "\"false\"") ^ "

set_display_local_var  <boolean>
     to set a flag saying whether or not the local var be displayed in  
     sim2cro. Its current value is " ^ (if !(flag.display_local_var) 
			   then "\"true\""
			   else "\"false\"") ^ "

set_verbose  <boolean>
     to set on and off a verbose mode. Its current value is " 
	       ^ (if !(flag.verbose) 
			   then "\"true\""
			   else "\"false\"") ^ "

634
635
636
637
638
639
640
641
642
643
644
set_show_step  <boolean>
     to set on and off a show step mode. Its current value is " 
	       ^ (if !(flag.show_step) 
			   then "\"true\""
			   else "\"false\"") ^ "

set_prefix  \"<string>\"
     to set the string that is appended before the call to lurette.
     This useful, e.g., for timings.
     Its current value is \"" ^ flag.prefix ^ "\"

645
set_make_opt  <string>
646
     to set the options to give to make for building lurette
647
648
649
650
651
652
     Its current value is \"" ^ flag.make_opt ^ "\"

set_output  <string>
     to set the name of the file the (rif) output of the test is
     put into. Its current value is \"" ^ flag.output ^ "\"

653
654
655
sim2chro
    call sim2chro

656
657
658
659
660
"
    in
      print_string msg
    

661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
let (read_commands : string -> string -> string -> (unit -> string) -> bool) =
  fun user_dir lurette_tmp_dir lurette_dir readline -> 
    try 
      ( match (read_cmd (lexer (Stream.of_string (readline ())))) with
	    Sut(str) -> 
	      flag.sut <- str ; flag.to_build := true; true
	  | Oracle(str) ->
	      if str = "" then
		( flag.oracle <- None ; flag.to_build := true; true)
	      else 
		( flag.oracle <- Some str ; flag.to_build := true; true)
	  | MakeOpt(str) -> 
	      flag.make_opt <- str; true
	  | Env(llist) -> 
	      flag.env <- llist; true
	  | StepNb(i) -> 
	      flag.step_nb <- i; true
	  | FormulaNb(i) -> 
	      flag.formula_nb <- i; true
	  | DrawNb(i) -> 
	      flag.draw_nb <- i; true
	  | Step(b) -> 
	      flag.step_by_step := b; true
	  | DisplaySim2chro(b) -> 
	      flag.display_sim2chro := b; true
	  | DisplayLocalVar(b) -> 
	      flag.display_local_var := b; true
	  | StepByStep(b) -> 
	      flag.step_by_step := b; true
	  | Seed(i) -> 
	      flag.seed <- Some i; true
	  | RandomSeed -> 
	      flag.seed <- None; true
	  | Verbose(b) -> 
	      flag.verbose := b; true
	  | ShowStep(b) -> 
	      flag.show_step := b; true
	  | Prompt(p) -> 
	      flag.prompt <- Some p; true
	  | Prefix(p) -> 
	      flag.prefix <-  p; true
	  | DrawInside -> 
	      flag.draw_mode <- Inside; true
	  | DrawEdges -> 
	      flag.draw_mode <- Edges; true
	  | DrawVerteces -> 
	      flag.draw_mode <- Verteces; true
	  | Output(str) -> 
	      flag.output <- str; true
	  | Clean -> 
	      let rm_cmd = ("rm -f " ^ lurette_tmp_dir ^ "/*") in 
	      let _ = Sys.command rm_cmd in
		print_string (rm_cmd ^ "\n");
		flag.to_build := true; 
		true
	  | Build -> 
	      let build_ok = build user_dir lurette_tmp_dir lurette_dir in
		if 
		  not build_ok 
		then 
		  print_string "\n*** Cannot build lurette, sorry.\n"
		else
		  flag.to_build := false; 
		flush stdout;
		true
	  | Run -> 
	      if (not !(flag.to_build) or (build user_dir lurette_tmp_dir lurette_dir))
	      then 
		(
		  flag.to_build := false;
		  Unix.chdir user_dir;
		  let result = run lurette_tmp_dir in
		    if 
		      result <> 0  
		    then 
		      output_string stdout "\n*** Can not run lurette, sorry.\n"

		    else 
		      (output_string stderr "   ... lurette ok.\n"; flush stderr)
		)
	      else 
		print_string "\n*** Cannot build lurette, sorry.\n";
	      flush stdout;
	      Unix.chdir lurette_tmp_dir;
	      true
		
	  | Show ->
	      Unix.chdir user_dir;
	      Util.show_luc flag.env;
	      Unix.chdir lurette_tmp_dir;
	      true
	  | CallSim2chro ->
	      Util.sim2chro (Filename.concat user_dir flag.output);
	      true
	  | Quit -> false
	  | HelpSimple -> print_string cmd_usage; true
	  | Help -> display_cmd (); true
	  | Man -> print_string man ; true
	  | Pack(file) ->
	      let 
		cmd = ("mv " ^ lurette_tmp_dir ^ " /tmp/" ^ file ^  
		       "; cd " ^ user_dir ^ "; tar cvfz " ^ 
		       file ^ ".tgz /tmp/" ^ file ^ 
		       " > tar.log; mv /tmp/" ^ 
		       file ^ " " ^ lurette_tmp_dir ^ " >> tar.log " ) 
			
	      in
	      let tar_res = 
		output_string stderr (cmd ^ "\n") ; 
		flush stderr;
		Sys.command cmd 
	      in	 
		if tar_res <> 0 
		then 
		  (
		    print_string ("*** <<" ^ cmd ^ 
				  ">> failed. Is gnu-tar in your path ?\n");
		    flush stdout;
		    true
		  )
		else
		  true
	  | Error(errmsg) -> 
	      print_string errmsg; 
	      print_string cmd_usage;
	      true
      )
    with 
	End_of_file -> raise End_of_file
      | e -> 
	  print_string ("Bad command\n " ^ (Printexc.to_string e) ^ "\n") ; 
	  print_string cmd_usage ;
	  true
    



798
799
800
801
802
803
804
805
806
let rec (main_loop : string -> string -> string -> int -> unit) =
  fun user_dir lurette_tmp_dir lurette_dir cpt ->
    let _ = 
      print_string 
	(
	  match flag.prompt with 
	      None -> "<lurette " ^ (string_of_int cpt) ^ "> "
	    | Some prompt -> prompt
	) ; 
807
      flush stdout
808
    in
809
    let continue = read_commands user_dir lurette_tmp_dir lurette_dir (read_line) in
810
      if continue 
811
      then main_loop user_dir lurette_tmp_dir lurette_dir (cpt+1)
812
      else print_string "bye!\n"
813
814


815
816


817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
let (get_fresh_dir : unit -> string) = 
  fun _ ->  
    let rec get_fresh_dir_rec n = 
      let dir = "/tmp/lurette" ^ (string_of_int n) in 
	if 
	  not (Sys.file_exists dir) 
	then 
	  (  
	    Unix.mkdir dir 0o755;
	    dir 
	  )
	else 
	  get_fresh_dir_rec (n+1) 
    in 
      get_fresh_dir_rec 1 
832
833

   
834
835
836
837
838
839
840
841
842
843
844
845
let (rm_dir : string -> unit) =
  fun dir -> 
    (* XXX probably not very portable ...*)
    let cmd = ("rm -rf " ^ dir) in
      print_string cmd;
      print_string "\n";
      flush stdout;
      if Sys.command cmd <> 0 
      then print_string ("Can not remove" ^ dir ^ "\n")



846
let _ =
847
848
849
850
851
852
  let user_dir = (Unix.getcwd ()) ^ "/"  in 
  let lurette_dir = 
    try Sys.getenv "LURETTE_PATH"
    with _ -> 
      print_string "Environment var LURETTE_PATH is unset.\n";
      exit 2
853
  in 
854
  let tmp_dir = get_fresh_dir () in
855
856
  let lurette_tmp_dir = 
    match flag.restore with
857
	None -> tmp_dir
858
859
      | Some file ->
	  (* XXX autoconf: gnu tar ougth to be installed ! *)
860
861
	  let cmd = ("tar xvfz " ^ user_dir ^ file ^ " --directory " ^ tmp_dir) in 
	  let tar_res = 
862
863
	    output_string stderr (cmd ^ "\n"); 
	    flush stderr;
864
865
866
867
868
869
870
871
872
873
874
875
	    Sys.command cmd 
	  in
	    if tar_res <> 0 
	    then 
	      (
		print_string ("*** <<" ^ cmd ^ 
			      ">> failed. Is gnu-tar in your path?\n");
		flush stdout;
		exit 2
	      )
	    else
	      (tmp_dir ^ "/tmp/" ^ (remove_extension file))
876
  in
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899

    
  let lurette_rc = (user_dir ^ ".lurette_rc") in
  let _ = 
    (* read command in the .lurette_rc file *)
    ( 
      if Sys.file_exists lurette_rc then
	let ic = (open_in lurette_rc) in
	  try
	    while true do
	      let _ = 
		read_commands user_dir lurette_tmp_dir lurette_dir 
		  (fun _ -> (input_line ic))
	      in
		()
	   done 
	  with End_of_file -> 
	    close_in ic 
    );
    
    
    (* read the lurettetop command line options (that will override the 
       .lurette.=_rc ones) *)
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
    let env_saved = flag.env in
      flag.env <- "";
	
      ( try
	  Arg.parse speclist 
	      (fun s -> 
		 if s = "x" 
		 then flag.env <- (flag.env ^ " x ")
		 else flag.env <-
		   let env = 
		     try Filename.chop_extension s
		     with Invalid_argument _ -> s
		   in 
		     if Filename.is_implicit env
		     then (flag.env ^ user_dir ^ env ^ ".luc ")
		     else (flag.env ^ env ^ ".luc ")
	      ) 
	      usage
	with 
	    Failure(e) ->
	      print_string e;
	      flush stdout ;
	      flush stderr ;
	      exit 2
	  | _ ->
	      exit 2
      );
      if (flag.env = "") then flag.env <- env_saved;
	    
929
  in
930
931
932
  let _ = Sys.command ("cp " ^ lurette_dir ^ "/source/lurette.ml " ^ lurette_tmp_dir ^
		       " ; cp " ^ lurette_dir ^ "/source/lurette.mli " ^ lurette_tmp_dir)
  in
933
934
935
936
937
938
939
940
941
942
    Unix.chdir lurette_tmp_dir;
    if 
      !(flag.go)
    then 
      (
	if 
	  build user_dir lurette_tmp_dir lurette_dir
	then
	  (
	    Unix.chdir user_dir;
943
944
945
946
947
948
949
950
	    if 
	      (run lurette_tmp_dir) <> 0
	    then 
	      (
		print_string "Can not create dir in /tmp/\n";
		exit 1
	      );
	    rm_dir lurette_tmp_dir;
951
952
953
	  )
	else  
	  (
954
	    print_string "Can not build lurette, sorry\n";
955
956
957
958
959
960
961
	    rm_dir lurette_tmp_dir;
	    exit 1
	  )
      )
    else 
      (* flag.go *)
      (
962
	main_loop user_dir lurette_tmp_dir lurette_dir 1;
963
964
965
	Unix.chdir user_dir;
	rm_dir lurette_tmp_dir
      )
966
967
968
969