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/

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

11
open List
12
13
14
15
16
17
18
19
20
21
22
23
24
open Graph
open Formula
open Wtree

(****************************************************************************)


(* 
** The environment is a list of graphs whose arcs are labelled by weighted 
** formula. 
*)

type env_stateT = {
25
26
27
28
  var_names: (string, (vnt list * vnt list * vnt list)) Hashtbl.t;
  (** Var names and types ([vnt]) of input, output, and local vars, 
    given module by module. *)

29
  mutable pre_var_names: var_name list;
30
31
  (** internal names of pre variables. *)

32
  mutable output_var_names: vnt list;
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
  (** Output var names and types. *)

  node_to_file_name: (int, string) Hashtbl.t;
  (** Associates each node in the environment automata with its 
    origin file name (i.e., the [.env] file it comes from).

    We need that information to be able to retrieve the list of
    variables that ougth to be generated from a list of nodes (the
    current nodes in the (virtual) automata product). Indeed, some
    variables that should be drawn do no necessarily appear in
    formula; and once the whole bdd has been traversed for the draw,
    we need to be able to know what variables are still to be drawn.
  *)

  atomic_formula_to_index: ((atomic_formula, int) Hashtbl.t); 
  (** This indexing of (output and local) variable names is used
    for constructing bdds in the boolean solver (for which variables
    are [int], not [string]s).  *)
  index_to_atomic_formula: ((int, atomic_formula) Hashtbl.t); 
  (** Ditto in the other way. *)
53
  mutable index_cpt: int;
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
  (** Counter used to create the index above. *)

  bdd_manager: Manager.t;
  (** bdd engine internal state. *)

  bdd_tbl_global: (formula, Bdd.t) Hashtbl.t;
  bdd_tbl: (formula, Bdd.t) Hashtbl.t;
  (** Transforming a formula into a bdd is expensive, therefore we
    store the result of this transformation in a table. Only formula
    does not depend on pre nor input vars are stored in
    [bdd_tbl_global]. The other ones are stored in the table
    [bdd_tbl], which is cleared at each new step. *)

  snt: (Bdd.t, Util.sol_nb * Util.sol_nb) Hashtbl.t;
  (** Associates to a bdd the (absolute) number of solutions
    contained in its lhs (then) and rhs (else) branches. Note that
    adding those two numbers only give a number of solution that is
    relative to which bdd points to it. *)
  
  mutable current_nodes : node list list;
  (** List of the automata current nodes (there are as many nodes as 
    there are environment run in parallel). *)
  
  mutable graph : (node, arc_info) Graph.t ;
  (** The automata is stored in a Graph.t *)
  
  mutable wtree_table : Wtree.wtree_table ;
  (** Mapping from nodes to [wtree] (see the doc of the [Wtree] module). *)

83
  mutable pre: subst list;
84
85
86
87
88
89
90
  (** Stores the values of pre variables. *)
  mutable input : env_in ;  
  (** Ditto for input vars. *)
  mutable output: env_out ; 
  (** Ditto for output vars. *)
  mutable local : env_loc   
  (** Ditto for local vars. *)
91
92
}

93

94
let (env_state:env_stateT) = {
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
  var_names               = Hashtbl.create 0;
  pre_var_names           = [];
  output_var_names        = [];
  node_to_file_name       = Hashtbl.create 0 ;
  bdd_manager             = Manager.make 10 10 0 0 0;
  graph                   = Graph.create () ;
  wtree_table             = Hashtbl.create 0 ;

(** The following values (possibly) change at each step *)
  pre                     = [];
  input                   = Hashtbl.create 0;
  output                  = [];
  local                   = [];
  current_nodes           = [];
  snt                     = Hashtbl.create 3; 
  bdd_tbl                 = Hashtbl.create 0;
  bdd_tbl_global          = Hashtbl.create 0;
  atomic_formula_to_index = Hashtbl.create 0;
  index_to_atomic_formula = Hashtbl.create 0;
  index_cpt               = 0 
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
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
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
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297

(****************************************************************************)
let (var_names: string -> vnt list * vnt list * vnt list) = 
  fun file ->
    Hashtbl.find env_state.var_names file

let (set_var_names : string -> vnt list * vnt list * vnt list -> unit) =
  fun file vntl -> 
    Hashtbl.replace env_state.var_names file vntl


let (in_env_unsorted : unit -> vnt list) =
  fun _ -> 
    let vnt_list =
      Hashtbl.fold 
	(fun _ (x,_,_) acc -> Util.merge x acc) 
	env_state.var_names
	[] 
    in
      vnt_list
	
let (out_env_unsorted : unit -> vnt list) =
  fun _ -> 
    let vnt_list =
      Hashtbl.fold 
	(fun _ (_,x,_) acc -> Util.merge x acc) 
	env_state.var_names
	[]  
    in
      vnt_list
	
let (loc_env_unsorted : unit -> vnt list) =
  fun _ -> 
    let vnt_list =
      Hashtbl.fold 
	(fun _ (_,_,x) acc -> Util.merge x acc) 
	env_state.var_names
	[]  
    in
      vnt_list


(****************************************************************************)
let (pre_var_names: unit -> var_name list) = 
  fun _ -> 
    env_state.pre_var_names
let (set_pre_var_names: var_name list -> unit) = 
  fun vnl -> 
    env_state.pre_var_names <- vnl

(****************************************************************************)
let (output_var_names: unit -> vnt list) = 
  fun _ -> 
    env_state.output_var_names
let (set_output_var_names: vnt list -> unit) = 
  fun vntl -> 
    env_state.output_var_names <- vntl


(****************************************************************************)
let (file_name: Formula.node -> string) = 
  fun node -> 
    Hashtbl.find env_state.node_to_file_name node 
    
let (set_file_name: Formula.node -> string -> unit) = 
  fun node file -> 
    Hashtbl.replace env_state.node_to_file_name node file 
      
(****************************************************************************)
let (bdd_manager : unit -> Manager.t) =  
  fun _ -> 
    env_state.bdd_manager 



(****************************************************************************)
(****************************************************************************)
(** The following values change at each step *)

(****************************************************************************)
let (graph : unit -> (node, arc_info) Graph.t) = 
  fun _  -> 
    env_state.graph
let (set_graph : (node, arc_info) Graph.t -> unit) =
  fun g -> 
    env_state.graph <- g

(****************************************************************************)
let (wtree_table : unit -> Wtree.wtree_table)  = 
  fun _  -> 
    env_state.wtree_table
let (set_wtree_table : Wtree.wtree_table -> unit) =
  fun wtt -> 
    env_state.wtree_table <- wtt

(****************************************************************************)
let (pre: unit ->  subst list) =
  fun _  -> 
    env_state.pre
let (set_pre: subst list -> unit) =
  fun sl -> 
    env_state.pre <- sl

let (input : unit -> env_in)  = 
  fun _  -> 
    env_state.input
let (set_input: env_in -> unit) =
  fun input -> 
    env_state.input <- input

let (output: unit -> env_out) = 
  fun _  -> 
    env_state.output
let (set_output: env_out -> unit) =
  fun output -> 
    env_state.output <- output

let (local : unit -> env_loc) = 
  fun _  -> 
    env_state.local
let (set_local: env_loc -> unit) =
  fun local -> 
    env_state.local <- local

(****************************************************************************)
let (current_nodes : unit -> node list list) = 
  fun _ -> 
    env_state.current_nodes
let (set_current_nodes: node list list -> unit) =
  fun nll -> 
    env_state.current_nodes <- nll

(****************************************************************************)
let (sol_number : Bdd.t -> Util.sol_nb * Util.sol_nb) =
  fun bdd -> 
    Hashtbl.find env_state.snt bdd

let (set_sol_number : Bdd.t -> Util.sol_nb * Util.sol_nb -> unit) =
  fun bdd sol_nb -> 
      Hashtbl.replace env_state.snt bdd sol_nb

let (clear_sol_numbers: unit -> unit) =
  fun _ -> 
    Hashtbl.clear env_state.snt

let (sol_number_exists : Bdd.t -> bool) =
  fun bdd -> 
      Hashtbl.mem env_state.snt bdd


(****************************************************************************)
let (bdd : formula -> Bdd.t) =
  fun f -> 
    Hashtbl.find env_state.bdd_tbl f

let (set_bdd : formula -> Bdd.t -> unit) =
  fun f bdd -> 
    Hashtbl.replace env_state.bdd_tbl f bdd

let (clear_bdd: unit -> unit) =
  fun _ -> 
    Hashtbl.clear env_state.bdd_tbl


let (bdd_global : formula -> Bdd.t) =
  fun f -> 
    Hashtbl.find env_state.bdd_tbl_global f

let (set_bdd_global : formula -> Bdd.t -> unit) =
  fun f bdd -> 
    Hashtbl.replace env_state.bdd_tbl_global f bdd


(****************************************************************************)
let (index_cpt: unit -> int) = 
  fun _  -> 
    env_state.index_cpt
let (set_index_cpt: int -> unit) = 
  fun i -> 
    env_state.index_cpt <- i

298
299
300
301
let (atomic_formula_to_index : atomic_formula -> int) =
  fun f ->  
    try Hashtbl.find env_state.atomic_formula_to_index f
    with Not_found -> 
302
      set_index_cpt (env_state.index_cpt + 1);
303
304
305
306
307
308
309
      Hashtbl.add env_state.atomic_formula_to_index f env_state.index_cpt;
      Hashtbl.add env_state.index_to_atomic_formula env_state.index_cpt f;
      env_state.index_cpt

let (index_to_atomic_formula : int -> atomic_formula) =
  fun i ->  
    Hashtbl.find env_state.index_to_atomic_formula i
310

311
312
313
314
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
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410


(****************************************************************************)
(****************************************************************************)
 

let rec (add_missing_pre: string list -> string list) =
  (* Even if the automata contains "_pre3toto", we need to store
     "_pre2toto", and "_pre1toto". Thefore we add them here to the
     list of pre vars declared in the automata thanks to this
     function. *)
  fun vnl -> 
    List.fold_left (add_missing_pre_acc) [] vnl
and
  (add_missing_pre_acc: string list -> string -> string list) =
  fun acc pren_vn -> 
    let (n, vn) = Util.split_pre_var_string pren_vn in
    let rec (build_list_pre : string list -> int -> string -> string list) =
      fun acc i str ->
	let prei_str = ("_pre" ^ (string_of_int i) ^ str) in
	  if i = 1 
	  then prei_str::acc
	  else build_list_pre (prei_str::acc) (i-1) str
    in
      Util.merge (build_list_pre [] n vn) acc

let _ = assert ( (add_missing_pre ["_pre3toto"; "_pre2titi"; "_pre2toto"]) 
  =  ["_pre2titi"; "_pre1titi"; "_pre3toto"; "_pre2toto"; "_pre1toto"] )


(** Returns the initial node of the automata defined in
  [file]. Also updates the various fields of [env_state] with the
  content of [file].  *)
let (read_env_state_one_file : string -> node) =
  fun file -> 
    let 
      (* Parses the content of [file]. *)
      Parse_env.Automata(init_node, list_in, list_out, list_loc, 
			 list_pre, list_arcs) = 
      try 
	Parse_env.parse_automata(
	  Parse_env.lexer(Stream.of_channel (open_in file)))
      with e  -> 
	print_string ("*** Error while parsing the environment file " ^ file ^ "\n");
	flush stdout; 
	raise e
    in
    let (list_pre_vn0, _) = List.split list_pre in 
    let list_pre_vn = add_missing_pre list_pre_vn0 in
      
    (* Sets the [graph] field of [env_state]. *)
    let node_nb = (List.length (Graph.get_all_nodes (graph ()))) in
    let (add_arc: Parse_env.read_arc -> unit) =
      fun arc ->
	match arc with
	    Parse_env.Arc(node_from, arc_info, node_to) -> 
	      (add_trans
		 (-)
		 (graph ())
		 (node_from+node_nb) 
		 arc_info 
		 (node_to+node_nb));
    in
      List.iter (add_arc) list_arcs ;

      (* Checks that there is no hole in the node numbers (which
	 would mean that the node number is not equal to the biggest node) *)
      let new_node_nb = (List.length (get_all_nodes (graph ()))) in
	if (for_all 
	      (fun arc -> 
		 match arc with 
		     Parse_env.Arc(node_from, arc_info, node_to) -> 
		       ( node_from >= new_node_nb ) || (node_to >= new_node_nb) 
	      )
	      list_arcs) 
	then failwith "*** Bad env format. Node numbers should be contiguous.\n";
	
	(* Sets the [node_to_file_name] field of [env_state]. *)
	List.iter
	  (fun node -> set_file_name (node+node_nb) file) 
	  (Graph.get_all_nodes (graph ()));

	(* Sets the [var_names] and [pre_var_names] fields of [env_state]. *)
	set_var_names file (list_in, list_out, list_loc) ;

	List.iter 
	  (fun vn -> set_pre_var_names (vn::(pre_var_names ())))
	  list_pre_vn;

	(init_node + node_nb)
      


(* Exported *)
let  (read_env_state : string list list -> unit) =
  fun files_ll -> 
    (** Calls [read_env_state_one_file] on a list of list of files. *)
    let nodes = map (map (read_env_state_one_file)) files_ll in
      set_current_nodes nodes ;
      set_wtree_table (Wtree.build_wtree_table (graph ()))