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

command_line.ml 4.84 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
**
** File: command_line.ml
** Main author: jahier@imag.fr
*)


type optionsT = {
  mutable step_by_step : bool ;
  mutable display_local_var : bool ;
  mutable display_sim2chro : bool ;
16
(*   mutable cudd_heap_init : int ; *)
17
  mutable user_seed : int ;
18
  mutable verbose : bool ;
19
  mutable show_step : bool ;
20
  mutable help : bool ;
21
  mutable output : string ;
22
  mutable oracle : bool
23
24
25
}

type cmd_line_optionT = 
26
    Step | NoStep | Help
27
28
  | DisplayLocalVar | NoDisplayLocalVar 
  | Sim2chro | NoSim2chro 
29
  | Inside | Edges 
30
(*   | CuddHeapInit  *)
31
  | Seed | Precision | NoOracle | Verbose | ShowStep | Output
32
33
34

(* Names of the command line options to override the defaults. *)
let (string_to_option: (string * cmd_line_optionT) list) = [
35
36
37
38
39
40
41
42

  ("--help", Help);
  ("-h", Help);

  ("--verbose", Verbose);
  ("-v", Verbose);

  ("--no-oracle", NoOracle);
43

44
45
46
  ("--output", Output);
  ("-o", Output);

47
48
49
50
  ("--no-step", NoStep);
  ("--step", Step);
  ("-s", Step);

51
52
53
  ("--show-step", ShowStep);
  ("-ss", ShowStep);

54
55
56
  ("--with-seed", Seed);
  ("-seed", Seed);

57
58
  ("--precision", Precision);

59
60
61
  ("--call-sim2chro", Sim2chro);
  ("--do-not-call-sim2chro", NoSim2chro);
  ("-ns2c", NoSim2chro);
62

63
64
65
66
  ("--display-local-var", DisplayLocalVar);
  ("--do-not-display-local-var", NoDisplayLocalVar);
  ("-nlv", NoDisplayLocalVar);

67
  ("--draw-inside", Inside);
68
69
  ("--draw-edges", Edges);

70
(*   ("--init-cudd-heap", CuddHeapInit) *)
71
72
73
74
75
76
77
]

let (option_to_usage: cmd_line_optionT -> string) =
  fun opt -> 
    match opt with
	Step -> "Run lurette step by step.\n"
      | NoStep ->  "Do not run lurette step by step (Default).\n"
78
      | Output ->  "Output file name (the default file name is \"lurette.rif\").\n"
79
80
81
82
      | DisplayLocalVar -> "Display environment local variables in sim2chro (Default).\n"
      | NoDisplayLocalVar ->  "Do not display environment local variables in sim2chro.\n"
      | Sim2chro -> "Call sim2chro when lurette resumes (Default).\n"
      | NoSim2chro ->  "Do not call sim2chro when lurette resumes.\n"
83
(*       | CuddHeapInit -> "Set a magic number (related to the gc) that is used by mldd \n\t\t\tfor initializing Dd (Default is 20).\n" *)
84
      | Seed ->  "Set the value of the seed the random engine is initialized with (0 lets the system draw a seed).\n"
85
      | Precision ->  "Set the precision used for numerical values (number of digits).\n"
86
      | NoOracle -> "Do not run the oracle.\n "
87
      | Inside -> "Draw inside the convex hull of solutions.\n "
88
      | Edges -> "Draw inside the convex hull of solutions, but a little bit more at edges and vertices.\n "
89
      | Verbose -> "Set on a wordier mode.\n"
90
      | ShowStep -> "Set on a mode where the step number is printed on the standard output.\n"
91
      | Help -> "Print this message.\n"
92

93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
let (group_common_options: (string * cmd_line_optionT) list -> 
       (string * cmd_line_optionT) list) =
  fun list -> 
    List.fold_left
      (fun acc (str, opt) -> 
         match acc with
             (str2, opt2)::tail -> 
	       if 
		 (opt = opt2)
	       then
		 (((str2  ^ "\n\t\t" ^ str), opt)::tail)
	       else
		 ((str, opt)::(str2, opt2)::tail)
	   | [] -> [(str, opt)]
      )
      []
      list
let usage_options = 
  List.fold_left 
    (fun acc (str, opt) -> acc ^ "\n\t\t" ^ str ^ "\n\t\t\t" ^ (option_to_usage opt))
    ""
    (List.rev (group_common_options string_to_option))

let usage = 
  ("\n\nusage: ./lurette length n p [options]* <file>.env ([x] <file>.env)* \n" ^
   "   where: \n\t o `length' is the number of steps that will be run " ^

   "\n\t o `n' is the number of formula that are drawn at each step" ^

   "\n\t o `p' is the number of solutions that are drawn in each formula" ^
   "\n\t   (resulting in a test ``thickness'' of n*p) " ^

   "\n\t o `<file>.env' contains an environment automata. Environments " ^
   "\n\t   separated by `x' will executed as if their automata where " ^
   "\n\t   multiplied (necessary if they have common output variables).\n " ^

   "\n\t o `options' is a list of options. The available options are: " ^ 
   usage_options ^ "\n\n" ^

   "Example:    ./lurette 1000 3 4 env1.env x env2.env x env3.env env4\n\t" ^
   "will run during 1000 steps; at each step, it will draw 3 formula in the \n\t" ^
   "automata, and it will draw 4 times in each formula (leading to a thickness of 12). \n\t" ^
   "The environment `env1', `env2', and `env3' will be run as a product,  \n\t" ^
   "and `env4' in parallel.\n\n ")


let cmd_line_string_to_int str errmsg =
  try 
    (int_of_string str) 
142
  with Failure ("int_of_string")
143
144
145
146
147
148
149
      -> 
	print_string usage ;
	print_string errmsg ;
	flush stdout ;
	failwith "\n *** Error when calling lurette.\n"