ima_exe.ml 7.57 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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
  user_seed = 0 ;
  boot = false
}


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

let lexer = Genlex.make_lexer ["t"; "f"; "#"]

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

let (get_inputs : vnt list -> rif_stream -> env_in) =
  fun vntl stream -> 
    (** The first token ougth to be a valid token (namely, rif pragmas have
      been filtered out). *)
  
    let tbl = Hashtbl.create (List.length vntl) in
    let _ = 
      List.iter
	(fun  vnt ->  
	   let new_stream =
	     match Stream.peek stream with
		 Some(_) -> stream
	       | None -> 
		   let line = read_line () in
		     lexer(Stream.of_string line) 
	   in
	   let (vn, vt) = vnt in
	     match (vnt, (Stream.next new_stream)) with
55
56
57
58
		 ((vn, BoolT), Genlex.Kwd "t") -> Hashtbl.add tbl vn (B(true))
	       | ((vn, BoolT), Genlex.Kwd "f") -> Hashtbl.add tbl vn (B(false))
	       | ((vn, BoolT), Genlex.Int 0)   -> Hashtbl.add tbl vn (B(false))
	       | ((vn, BoolT), Genlex.Int 1)   -> Hashtbl.add tbl vn (B(true))
59
		   
60
61
	       | ((vn, IntT(_,_)), Genlex.Int i) -> Hashtbl.add tbl vn (N(I(i)))
	       | ((vn, FloatT(_,_)), Genlex.Float f) -> Hashtbl.add tbl vn (N(F(f)))
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

	       | _ -> failwith ("*** Bad input. A " ^ (var_type_to_string2 vt) ^ 
				" was expected for variable " ^ vn ^ ".\n")
	)
	vntl
    in
      tbl
    
let rec (read_rif_input : vnt list -> env_in) =
  fun vntl -> 
    (** Reads the environment inputs on stdin. It should respect the rif format. *)
    let line = read_line () in
    let stream = lexer(Stream.of_string line) in
    let tok_list = Stream.npeek 2 stream in
      match tok_list with
	  [Genlex.Kwd "#"; Genlex.Ident "outs"] ->
	    Stream.junk stream ; 
	    Stream.junk stream ; 
	    get_inputs vntl stream 
	| [Genlex.Kwd "#"; _] -> 
	    (* Ignore everything after a "#"... if it is not followed by "outs". *)
	    read_rif_input vntl
	| _ -> get_inputs vntl stream 


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
90
      List.iter (print_var_value stdout) ae_l
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


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

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) 
      then print_string usage 
      else
	main2 ()
    with 
	Failure(errmsg) -> print_string errmsg
      | 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
117
118
119
	      ShowAut -> options.show_automata <- true ; (n+1)
	    | NoShowAut -> options.show_automata <- false ; (n+1)
	    | Boot -> options.boot <- true ; (n+1)
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
152
153
154
155
156
157
158
159
160
161
162
	    | 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
163
    let () = Env_state.read_env_state env_llist in
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
     
    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
    let local_var_name_and_type_list = 
      Util.sort_list_string_pair local_var_name_and_type_list_unsorted 
    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 ;      


187
188
189
190
191
      if options.show_automata then (
	Show_env.generate_env_graph [[]] ("automata" ^ (string_of_int (Hashtbl.hash Sys.argv))) ;  
	Util.gv ("automata" ^ (string_of_int (Hashtbl.hash Sys.argv)) ^ ".ps")
      ) ;

192
      Env_state.set_output_var_names (Env_state.out_env_unsorted ()) ;
193
194
195


      (* Initializing the solution number table *)
196
197
198
199
      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);
200
201
202
203
204
205
206
207
208
209
210
211

      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
212
213
214
215
	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)
216
217
	    | _ -> assert false
	in
218
	  Env.env_step nll call out loc ;
219
	  Env.update_pre (Env_state.input ()) (Env_state.output ()) (Env_state.local ()) ;
220
221
222
223
224
225
226
227
228
229
	  write_rif_output (Env_state.out_env_unsorted ()) out ;
      else ();  

      main_loop 1 ;
      flush stdout

and
  main_loop t = 

  let _ = print_string ("\n# step " ^ (string_of_int t) ^ ":\n"); flush stdout in
230
  let previous_nodes = (Env_state.current_nodes ()) in
231
232

  let input = read_rif_input (Env_state.in_env_unsorted ()) in
233
  let nll_call_out_loc_list = Env.env_try 1 1 input in
234

235
236
237
  let (nll, call, out, loc) = 
    match nll_call_out_loc_list with
	[(nll, call, out, loc)] -> (nll, call, out, loc)
238
239
240
      | _ -> assert false
  in

241
242
243
244
245
246
    if options.show_automata then (
      Show_env.generate_env_graph 
          [[]] ("automata" ^ (string_of_int (Hashtbl.hash Sys.argv)))
    );
    
    Env.env_step nll call out loc ;
247
    Env.update_pre (Env_state.input ()) (Env_state.output ()) (Env_state.local ()) ;
248
    
249
250
251
252
    (* Inputs and pre vars may change at ech new step, therefore we need to clear
       that table. *)
    Env_state.clear_bdd () ;

253
254
255
256
257
258
259
260
261
    write_rif_output (Env_state.out_env_unsorted ()) out ;
    main_loop (t+1) 
;;
      


main ();;