ima_exe.ml 9.63 KB
Newer Older
1
2
3
4
5
6
7
(*-----------------------------------------------------------------------
 ** Copyright (C) 2001, 2002 - Verimag.
 ** This file may only be copied under the terms of the GNU Library General
 ** Public License 
 **-----------------------------------------------------------------------
 **
 ** File: ima_exe.ml
8
 ** Author: jahier@imag.fr
9
10
11
12
13
14
15
16
17
18
19
20
21
22
 *)

(*------------------------------------------------------------------------*)

open Util
open Formula
open Env_state
open List
open Command_line_ima_exe

(*------------------------------------------------------------------------*)


let (options:Command_line_ima_exe.optionsT) = {
23
  show_automata = false ;
24
25
26
27
28
29
30
31
  user_seed = 0 ;
  boot = false
}


(*------------------------------------------------------------------------*)
(* RIF parsing *)

32
let lexer = Genlex.make_lexer ["#"; "#@"; "@#"]
33
34
35
36

type rif_token = Genlex.token 
type rif_stream = Genlex.token Stream.t

37
38
39
40
41
let rif_pragmas = ["inputs"]

(* Which pragmas should be defined ? *)
(* let rif_pragmas = ["outs";"outputs";"program";"inputs";"step";"reset"] *)

42
43
let rec (read_rif_input : vnt list -> env_in) =
  fun vntl -> 
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
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
142
143
144
145
146
147
148
149
150
151
    (** Reads the environment input values on stdin. It should
      follow the rif format. *)
    let tbl = Hashtbl.create (List.length vntl) in
      if vntl = []
      then tbl
      else 
	let line = read_line () in
	let stream = lexer(Stream.of_string line) in
	  parse_rif_stream vntl stream tbl
	    
and (parse_rif_stream : vnt list -> rif_stream -> env_in -> env_in) =
  fun vntl stream tbl -> 
    if vntl = []
    then tbl
    else 
      let tok_list = Stream.npeek 2 stream in
	match tok_list with 
	  | [Genlex.Kwd "#"; Genlex.Ident id] ->
	      if List.mem id rif_pragmas
	      then 
		(
		  Stream.junk stream ;
		  Stream.junk stream ; 
		  parse_rif_stream vntl stream tbl
		)
	      else
		(* We skip everything that occurs after a [#] not followed by a
		   member of [rif_pragmas], until the next eol. *)
		(
		  Stream.junk stream ; 
		  parse_rif_stream vntl (lexer (Stream.of_string (read_line ()))) tbl
		)

	  | (Genlex.Kwd "#")::_ 
	      (* Ditto *)
	    ->
	      Stream.junk stream ; 
	      parse_rif_stream vntl (lexer (Stream.of_string (read_line ()))) tbl
		
	  | (Genlex.Kwd "#@")::_ ->
	      (* Beginning of multi-line comment. Note that here,
		 unlike the rif format, we ignore multi line pragmas;
		 namely, we handle them as a lusti-line comment. *)
	      (
		Stream.junk stream ;
		ignore_toks_until_end_of_pragmas vntl stream tbl
	      ) 

	  | (Genlex.Float f)::_ ->
	      (
		Stream.junk stream ;
		Hashtbl.add tbl (fst (hd vntl)) (N(F(f))) ;
		parse_rif_stream (tl vntl) stream tbl
	      )

	  | (Genlex.Int i)::_ ->
	      (
		Stream.junk stream ;
		if ((var_type_to_string (snd (hd vntl))) = "bool")
		then 
		  if i = 0 
		  then Hashtbl.add tbl (fst (hd vntl)) (B(false))
		  else Hashtbl.add tbl (fst (hd vntl)) (B(true))
		else Hashtbl.add tbl (fst (hd vntl)) (N(I(i))) ;
		parse_rif_stream (tl vntl) stream tbl
	      )
	      
	  | (Genlex.Ident b)::_ ->
	      (
		Stream.junk stream ;
		if mem b ["f"; "F";"false"]
		then Hashtbl.add tbl (fst (hd vntl)) (B(false))
		else if  mem b ["t"; "T";"true"]
		    then Hashtbl.add tbl (fst (hd vntl)) (B(true))
		else 
		  failwith ("### parse error. " ^ b ^ " is unknown \n") ;
		
		parse_rif_stream (tl vntl) stream tbl
	      )
	      
	  | [] -> 
	      (* Eol is is reached; proceed with the next one *)
	      parse_rif_stream vntl (lexer (Stream.of_string (read_line ()))) tbl

	  | _ -> failwith ("### parse error.\n")
	      
and (ignore_toks_until_end_of_pragmas : vnt list -> rif_stream -> env_in 
       -> env_in) =
  fun vntl stream tbl -> 
    (* ignore all tokens until "@#" is reached *)
    let tok_opt = Stream.peek stream in
      match tok_opt  with
	| Some(Genlex.Kwd "@#") ->
	    (
	      Stream.junk stream ;
	      parse_rif_stream vntl stream tbl
	    )
	| Some(_) ->
	    (
	      Stream.junk stream ;
	      ignore_toks_until_end_of_pragmas vntl stream tbl 
	    )
	| None -> 
	    (* Eol is is reached; proceed with the next one *)
	    ignore_toks_until_end_of_pragmas vntl 
	    (lexer (Stream.of_string (read_line ()))) tbl
	    
    
152
153
154
155

let (write_rif_output : vnt list -> env_out -> unit) =
  fun vntl output -> 
    let ae_l = List.map (fun (vn, _) -> List.assoc vn output) vntl in
156
      List.iter (print_var_value stdout) ae_l
157
158
159
160
161
162
163
164
165
166
167
168


(*------------------------------------------------------------------------*)

let arg_nb = (Array.length Sys.argv) 

external random_seed: unit -> int = "sys_random_seed";;

let rec (main : unit -> 'a) =
  fun _ ->
    try
      if (arg_nb < 2) 
169
      then output_string stderr usage 
170
171
172
      else
	main2 ()
    with 
173
	Failure(errmsg) -> output_string stderr errmsg
174
175
176
177
178
179
180
181
182
      | e -> raise e	

and 
  (get_ima_exe_options: int -> int) =
  fun n -> 
    try 
      begin
	let opt = List.assoc Sys.argv.(n) Command_line_ima_exe.string_to_option in
	  match opt with
183
184
185
	      ShowAut -> options.show_automata <- true ; (n+1)
	    | NoShowAut -> options.show_automata <- false ; (n+1)
	    | Boot -> options.boot <- true ; (n+1)
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
	    | Seed ->
		let str = (Sys.argv.(n+1)) in
		  options.user_seed <- cmd_line_string_to_int str 
		    ("*** Error when calling ima_exe: an " ^
		     "integer is expected after the " ^
		     "option --with-seed\n") ;
		  n+2
      end
    with Not_found -> n
and
  (get_env_from_args: int -> string list list -> string list list) =
  fun n file_ll -> 
    (** Returns the environment file names given at top-level into a
      list of list.  E.g., if the call [ima_exe env1 x env2 x env3
      env4] is done, then [get_env_from_args 10 []] (where 10 is the
      arg nb) returns [[["env1"; "env2"; "env3"]; ["env4"]]].

      Also set the command line options if any.  *)
    if (n = arg_nb) then file_ll
    else
      let m = get_ima_exe_options n in
	(* m > n iff Sys.argv.(n) is an option *)
	if 
	  (m > n) 
	then 
	  get_env_from_args m file_ll
	else
	  let arg = Sys.argv.(m) in
	    if 
	      (arg = "x") 
	    then
	      match file_ll with
		  sl::sll -> 
		    let env = Sys.argv.(n+1) in
                      get_env_from_args (n+2) ((env::sl)::sll)
		| []  -> assert false
	    else 
	      get_env_from_args (n+1) ([arg]::file_ll)
and
  (main2 : unit -> 'a) =
  fun _ -> 
    (* Initialisation of `Env_state.env_state' *)
    let env_llist = (get_env_from_args 1 []) in
229
    let () = Env_state.read_env_state env_llist in
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
     
    let local_var_name_and_type_list_unsorted0 = Env_state.loc_env_unsorted () in
    let local_var_name_and_type_list_unsorted = 
      List.map (fun (vn, vt) -> (vn, (var_type_to_string vt)))
	local_var_name_and_type_list_unsorted0
    in
      
    (* Initialisation of the random engine *)
    let seed = 
      if (options.user_seed = 0)
      then (random_seed ())
      else  options.user_seed
    in
      Random.init seed ;
      print_string "#The random engine was initialized with the seed ";
      print_int seed;
      print_string "\n ";
      flush stdout ;      


250
      if options.show_automata then (
251
252
253
	Show_env.generate_env_graph (flatten (Env_state.current_nodes ())) [] 
		("automata" ^ (string_of_int (Hashtbl.hash Sys.argv))) 
		(Env_state.graph ()) ;
254
255
256
	Util.gv ("automata" ^ (string_of_int (Hashtbl.hash Sys.argv)) ^ ".ps")
      ) ;

257
      Env_state.set_output_var_names (Env_state.out_env_unsorted ()) ;
258
259
260


      (* Initializing the solution number table *)
261
262
263
264
      Env_state.set_sol_number 
	(Bdd.dtrue (Env_state.bdd_manager ())) (Util.one_sol, Util.zero_sol);
      Env_state.set_sol_number 
	(Bdd.dfalse (Env_state.bdd_manager ())) (Util.zero_sol, Util.one_sol);
265
266
267
268
269
270
271
272
273
274
275
276

      print_string "#inputs ";
      List.iter 
	(fun (vn,vt) -> 
	   print_string (vn ^ ":" ^ (var_type_to_string2 vt) ^ " ")
	) 
	(Env_state.out_env_unsorted ());
      print_string "\n";
      flush stdout;

      if options.boot 
      then
277
278
279
280
	let nll_call_out_loc_list = Env.env_try 1 1 (Hashtbl.create 0) in
	let (nll, call, out, loc) = 
	  match nll_call_out_loc_list with
	      [(nll, call, out, loc)] -> (nll, call, out, loc)
281
282
	    | _ -> assert false
	in
283
	  Env.env_step nll call out loc ;
284
	  Env.update_pre (Env_state.input ()) (Env_state.output ()) (Env_state.local ()) ;
285
286
287
288
289
290
291
292
293
	  write_rif_output (Env_state.out_env_unsorted ()) out ;
      else ();  

      main_loop 1 ;
      flush stdout

and
  main_loop t = 

294
  let previous_nodes = (Env_state.current_nodes ()) in
295
296
  let nl = List.flatten previous_nodes in
  let _ = 
297
298
299
300
301
302
303
304

(* xxx --verbose !!! *)
(*     List.iter  *)
(*       (fun n -> output_string stderr ((string_of_int n) ^ " "))  *)
(*       nl; *)
(*     flush stderr; *)
(* xxx *)

305
306
307
308
309
310
311
    print_string ("\n# step " ^ (string_of_int t) ^ " (") ;
    if (List.length nl)  > 1
    then 
      (
	print_string "current nodes are ";
	List.iter 
	  (fun n -> print_string ((string_of_int n) ^ " ")) 
312
	  nl
313
314
315
316
317
318
319
320
321
322
      )
    else 
      (
	print_string "current node is ";
	print_string (string_of_int (List.hd nl))
      );
 
    print_string ("):\n") ;
    flush stdout 
  in
323
  let input = read_rif_input (Env_state.in_env_unsorted ()) in
324
  let nll_call_out_loc_list = Env.env_try 1 1 input in
325

326
327
328
  let (nll, call, out, loc) = 
    match nll_call_out_loc_list with
	[(nll, call, out, loc)] -> (nll, call, out, loc)
329
330
      | _ -> assert false
  in
331
332
    
    Env.env_step nll call out loc ;
333
    Env.update_pre (Env_state.input ()) (Env_state.output ()) (Env_state.local ()) ;
334
    
335
336
337
338
    (* Inputs and pre vars may change at ech new step, therefore we need to clear
       that table. *)
    Env_state.clear_bdd () ;

339
    write_rif_output (Env_state.out_env_unsorted ()) out ;
340
341
342
343
344
    if options.show_automata then (
      Show_env.generate_env_graph (flatten (Env_state.current_nodes ()))
          [] ("automata" ^ (string_of_int (Hashtbl.hash Sys.argv))) 
	  (Env_state.graph ())
    );
345
346
347
348
349
350
351
352
    main_loop (t+1) 
;;
      


main ();;