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/

lutExe.ml 92.8 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
(* 

A) Tout ce qu'il faut pour intégrer facilement Lutin à Lurette
--------------------------------------------------------------

- création/initialisation à partir d'un Expand.t
  (ou directement d'un fichier Lutin)
  résultat : le control_state initial

- (1) génération de contraintes satisfiables, avec :
    une valeur des ins * une valeur des pres * un control state
    -> un comportement REALISABLE (goto, vanish, raise programmé)
       + une fonction pour obtenir d'autres comportements satisfiables alternatifs 
         (test épais du contrôle)
    -> plus/pas de comportements

N.B. c'est un peu une liste "lazzy" des comportements possibles

- (2) pour les comportements REALISABLES de type "Goto",
  (i.e. un couple contrainte réalisable * control_state suivant) :
  génération d'une (liste) de solutions concrètes :
  (valeur des sorties, valeur des locales)
N.B. pourrait être lazzy ? ce qui n'est pas le cas pour lucky, où
on demande explicitement "n" solutions.

- pour rappeler (1), un utilitaire qui "merge" (en élagant) :
  valeur des ins * valeur des outs * valeur des locales
  -> valeur des pres 

B) Pour faire un Lutin "réactif" simple
---------------------------------------

C'est juste une version simplifiée où on fournit juste
un step qui fait une réaction complète :
valeur des ins * prg -> valeur des outs * prg suivant

N.B. dans un premier temps, c'est un step simple qu'on
  utilisera pour les appels interne "exist outs = node(ins)",
  On verra plus tard pour la version Lurette récursive !

*)

43
open LutErrors;;
44
45
46
47
48
49
open Printf;;
open CoIdent ;;
open CoAlgExp ;;
open CoTraceExp ;;

let dbg = Verbose.get_flag "LutExe"
50
let dbgrun = Verbose.get_flag "Run"
51

52

53
54
55
56
57
58
59
(* store = current (given) values + past values *)
type store = { curs: Var.env; pres: Var.env }


(* "lucky" out list + loc list  *)
type support = Exp.var list * Exp.var list

60
(** type t holds several global useful info *)
61
type t = {
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
  arg_opt: MainArg.t;
  expanded_code: Expand.t;
  (* translation CoIdent -> Exp.var is done once *)
  in_vars: Exp.var list;
  out_vars: Exp.var list;
  loc_vars: Exp.var list;
  (* (partial) initial values of global vars (ins/outs *)
  init_pres: Value.OfIdent.t;

  id2var_tab: (string, Exp.var) Hashtbl.t;

  (* REQUIRED BY SolveR.solve_formula *)
  (* list of names for outputs ... *)
  out_var_names: string list;
  (* ... formula (and) for bool vars ... *)
  bool_vars_to_gen: Exp.formula;
  (* ... and var list for nums ! *)
  num_vars_to_gen: Exp.var list;
80
81
}

82
83
84
85
let in_var_list it = it.in_vars
let out_var_list it = it.out_vars
let loc_var_list it = it.loc_vars

86
87


88
89
90
91
92
93
94
95
96
97
98
99
(* TRANSLATION Lutin -> Lucky

	N.B. necessary to use the Lucky formula solver

   How it works:
	Glue provides a generic lutin exp to lucky exp
	(i.e. CoAlgExp.t to Exp.t) parameterized by:
	- a bool specifying if partial eval must be done
	  (i.e. constant propagation)
	- an "ident" solver, wich translate ident into Exp.t
	  (maybe mutually recursive with lucky_exp_of !)
 
100
101
*)

102
103
104
105
106
let (to_event_var:'a Var.t -> Event.var) = 
  fun v -> 
    Var.name v, Type.to_data_t (Var.typ v) 


107
108
109
110
111
112
113
(**
	Basic unalias id2exp to use with Glue.lucky_exp_of
	- Requires a LutExe.t structure
	- aliases are unaliased
	- support vars are kept as it 

=> No longer used ? 
114
*)
115
let rec unalias (it:t) (eval:bool) (idref:CoAlgExp.node) = (
116
117
118
	match idref with
	| CoAlgExp.AE_alias id -> (
		let xenv = it.expanded_code in
119
		(* let nme = CoIdent.to_string id in *)
120
		let e = (Util.hfind (Expand.alias_tab xenv) id).Expand.ai_def_exp in
121
		Glue.lucky_exp_of eval (unalias it) e
122
123
	)
	| CoAlgExp.AE_support id -> (
124
		Glue.lucky_exp_var_ref (id2var it id)
125
126
127
128
	)
	| CoAlgExp.AE_pre id -> assert false
	| _ -> assert false
) 
129
130
131
132
133
134
135
136
(**
	Static unalias id2exp to use with Glue.lucky_exp_of
	- Requires just a source program Expant.t
	- aliases are unaliased
	- support vars not supported (error)

=> mainly used for evaluating compile-time constants
	(init, range of in/out) 
137
138
139
140
141
*)
and static_unalias (xenv:Expand.t) (eval:bool) (idref:CoAlgExp.node) = (
	match idref with
	| CoAlgExp.AE_alias id -> (
		(* let nme = CoIdent.to_string id in *)
142
		let e = (Util.hfind (Expand.alias_tab xenv) id).Expand.ai_def_exp in
143
144
		Glue.lucky_exp_of eval (static_unalias xenv) e
	)
145
146
147
148
149
	| CoAlgExp.AE_support id -> (
		raise (
		Internal_error ("LutExe.static_unalias",
			"unexpected support variable("^(CoIdent.to_string id)^")"
	)))
150
151
152
	| CoAlgExp.AE_pre id -> assert false
	| _ -> assert false
)
153
154
155
156
157
(**
	Create a Var.t and store it in table
=> this table is supposed to become the id2var_tab
	of a LutExe.t
*)
158
159
160
161
162
and new_id2var
	(tab: (string, Exp.var) Hashtbl.t)
	(xenv: Expand.t)
	(id:CoIdent.t) =
(
163
	let info = Util.hfind (Expand.support_tab xenv) id in
164
165
166
167
	let var = Glue.lucky_var_of (static_unalias xenv) info in
	Hashtbl.add tab id var;
	var
)
168
169
170
(**
	Retrieve a Var.t ina LutExe.t
*)
171
and id2var (it:t) (id:CoIdent.t) = (
172
	(* let info = Util.hfind (Expand.support_tab xenv) id in *)
173
	(* Glue.lucky_var_of unalias info *)
174
	Util.hfind it.id2var_tab id
175
)
176

177

178
(**
179
180
181
182
	Builds a LutExe.t structure
	from a Expand.t structure
	(i.e. a pre-compiled Lutin program)
*)
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
let of_expanded_code (opt:MainArg.t) (exped: Expand.t) = (
  (** computes and stores info for the execution *)
  let id2var_tab = Hashtbl.create 10 in
	 (* lucky-like vars are created once for all *)
  let ivs = List.map (new_id2var id2var_tab exped)
	 (Expand.input_list exped) in
  let ovs = List.map (new_id2var id2var_tab exped)
	 (Expand.output_list exped) in
  let ovns = List.map (Var.name) ovs in
  let lvs = List.map (new_id2var id2var_tab exped)
	 (Expand.local_out_list exped) in
	 (* all uncontrolables ... *)
  let uvs = ovs @ lvs in
  let isbool v = ((Var.typ v) = Type.BoolT) in
  let isnum v = (match (Var.typ v) with Type.IntT | Type.FloatT -> true | _ -> false) in
  let bvs = List.filter isbool uvs in 
  let nvs = List.filter isnum uvs in 
  let bvf = match bvs with
	 | [] -> Exp.True
	 | h::t -> List.fold_left (fun acc v -> (Exp.And(Exp.Bvar(v), acc))) (Exp.Bvar h) t
  in
	 (* init pres *)
  let addpre acc x = (
	 match Var.init x with
207
208
		| None -> acc
		| Some e -> (
209
210
211
212
213
214
215
216
			 let v = Exp.to_value e in
			   Value.OfIdent.add acc (Var.name x, v)
		  )
  ) in
  let ip = List.fold_left addpre (Value.OfIdent.empty) ivs in
  let ip = List.fold_left addpre ip ovs in
	 {
      arg_opt = opt;
217
218
219
220
221
222
223
224
225
		expanded_code = exped;
		out_vars = ovs;
		in_vars = ivs;
		loc_vars = lvs;
		id2var_tab = id2var_tab;
		init_pres = ip;
		out_var_names = ovns;
		bool_vars_to_gen = bvf;
		num_vars_to_gen = nvs;
226
	 }
227
228
)

229
(**
230
231
	Builds a LutExe.t structure
	from a lutin file + a main node
232
233
234
235

	N.B. some fields are redundant, they are stored
	to ease te connection with the lucky solver.
*)
236
let make opt infile mnode = (
237
  (** open the file, compile and expand the main node ... *)
238
    let libs = MainArg.libs opt in 
239
240
241
    let mainprg = 
      assert (infile <> []); 
      Parsers.reinit_parser ();
242
      Parsers.read_lut infile
243
    in
244
245
    Verbose.put ~flag:dbg "LutExe.make: Parsers.read_lut infile [%s] OK\n"
                (String.concat ";" infile);
246
    let tlenv = CheckType.check_pack libs mainprg in
247
    Verbose.put ~flag:dbg "LutExe.make: CheckType.check_pack OK\n";
248

249
250
251
252
253
254
255
256
    let _ = !Solver.clear_snt (); !Solver.init_snt () in
    let mnode = if mnode <> "" then mnode else (
      let all_nodes = Hashtbl.fold
        (fun n _ acc -> n::acc)
        mainprg.Syntaxe.pck_nodetab
        []
      in
        (* It is not necessary to build to complete list to take the first
257
           one, but I'm sure that list will be useful in the future... R1.*)
258
259
      let mnode = if all_nodes = [] then
        (* shouldn't that be checked before? *)
260
        raise (LutErrors.Global_error ("Lutin files '"^(String.concat "," infile)^ 
261
262
263
264
265
266
267
                                      "' contains no node"))
      else List.hd all_nodes 
      in
        Verbose.put ~level:1 "# No node is specified: will use %s \n" mnode;
        mnode
    ) in
    let exped = Expand.make tlenv mainprg mnode in
268
269
    Verbose.put ~flag:dbg "LutExe.make: Expand.make %s OK\n" mnode;
    (* actual result .... *)
270
271
(*     Verbose.put ~flag:dbg "Event.set_seed %i\n"(MainArg.seed opt); *)
(*     Event.set_seed (MainArg.seed opt); (* transmit the seed to the event handler *)  *)
272
273
274
275
    if MainArg.run opt then 
		of_expanded_code opt exped
    else
      exit 0
276
  
277
278
)

279
(** Execution *)
280

281
(** control state = Lutin trace exp *)
282
283
284
(* type control_state =  (t * CoTraceExp.t) *)
type control_state =  CoTraceExp.t

285
let string_of_control_state t =  CoTraceExp.dumps t
286

287
(** initial control state *)
288
289
290
291
292
293
294
295
let get_init_state it = (
   (* ident de la trace principale *)
	let xenv = it.expanded_code in
   let init_id = Expand.main_trace xenv in
   let init_info = Expand.get_trace_info xenv init_id in
   init_info.Expand.ti_def_exp
)

296
(** initial pre values *)
297
298
let get_init_pres it = it.init_pres

299
300


301
302
303
304
305
306
307
308
(** A "guard" is a SATISFIABLE constraint used in a goto *)
(* => for the time being, a lucky bool exp (Exp.formula) 
TODO: 
	=> hold a normalized version (BDD) ?
	=> or even a solution ?
	=> hold the support of the constraint ?
	   (for the time being, all local vars are generated,
		even out of their scope)
309
310
*)

311
312
313
314
(** keep the solution(s) *) 
type solutions = (Var.env_out * Var.env_loc) list
type guard = {
	g_form : Exp.formula;
315
	mutable g_sol : solutions option;
316
   mutable g_bdd : Bdd.t option;
317
   g_src : CoIdent.src_stack list
318
}
319
320
321

let rm_ctrl_nt = Str.global_replace (Str.regexp "[\n\t]") " " 

322
323
let (guard_to_string : guard -> string) =
 fun g -> 
324
   rm_ctrl_nt(Exp.formula_to_string g.g_form)
325

326
let empty_guard = {g_form = Exp.True; g_sol = None; g_bdd=None; g_src=[] }
327

Pascal Raymond's avatar
Pascal Raymond committed
328
let ws = Str.regexp "[ \t\n]+"
329
let string_of_guard g = (
Pascal Raymond's avatar
Pascal Raymond committed
330
331
332
	let s = Exp.formula_to_string g.g_form in
	let sl = Str.split ws s in
	String.concat " " sl
333
334
)

335
336
(**
	Full eval id2exp for Glue.lucky_exp_of
337
	- unaliasing
338
	- replace uncontrolable by their values
339
	- partial eval (always)
340
341
=> requires a LutExe.t for unaliasing and a data context
	(uncontrol. values)
342
343
*)

344
345
let rec contextual_id2exp (it:t) data (eval:bool) (idref:CoAlgExp.node) = (
	let unalias s =
346
		(Util.hfind (Expand.alias_tab it.expanded_code) s).Expand.ai_def_exp
347
	in
348
349
350
	match idref with
	| CoAlgExp.AE_alias id -> (
		let e' = unalias id in
351
		contextual_lutexp2exp it data e'
352
353
354
355
356
357
358
	)
	| CoAlgExp.AE_support id -> (
		(* does the value exist in data.curs ? *)
		let res = try (
           let v = Value.OfIdent.get data.curs id in
			Glue.lucky_exp_of_value v
		) with Not_found -> (
359
			Glue.lucky_exp_var_ref (id2var it id)
360
361
362
363
364
365
366
367
368
		) in res
	)
	| CoAlgExp.AE_pre id -> (
		(* the value MUST be data.pres *)
		try (
			let v = Value.OfIdent.get data.pres id in
			Glue.lucky_exp_of_value v
		) with Not_found -> raise (
			Internal_error ("LutExe.contextual_id2exp",
369
370
				"can't find the value of pre("^(CoIdent.to_string id)^
              ") in the current context"
371
372
373
374
375
376
			)
		)
	
	)
	| _ -> assert false
) and
377
contextual_lutexp2exp (it:t) data e = (
378
	(* PARTIAL EVAL *)
379
	Glue.lucky_exp_of true (contextual_id2exp it data) e
380
381
)

382
(** exceptions and type *)
383
384
exception Deadlock of int (* Attach the event nb to ease debugging when this exc 
                             is raised at top-level *)
385

386
387
388
389
390
391
392
393
394
395
396
397
exception Stop
exception Exception of string
type internal_state = control_state * Var.env

let get_init_internal_state (it:t) = (get_init_state it, get_init_pres it)


let make_pre : t -> Var.env_in -> Var.env_out -> Var.env_loc -> Var.env =
fun            it   ins           outs           locs        -> (
	(* for the time being we keep all variables, even if they are not used in a pre ... *)
	Value.OfIdent.union ins (Value.OfIdent.union outs locs)
)
398

399
400
401
402
403
404
(** Interface with the solver
=> the lucky solver was designed to do more than we need here !
*)

(* reuse Solver.solve_formula, returns solutions *)
let find_some_sols 
405
406
407
408
409
410
	 (it:t)
	 (tfdn: Thickness.formula_draw_nb)
	 (tn: Thickness.numeric)
	 (g : guard)
    = match g.g_sol with
      | Some s -> s
Erwan Jahier's avatar
Erwan Jahier committed
411
      | None ->
412
        let zesol,bdd = (
413
414
	       let solver_vl = ref 0 in
	       Verbose.exe ~flag:dbg (fun _ -> solver_vl := 3);
415
	       let is_bool_sat,bdd = Solver.is_satisfiable_bdd
416
417
418
419
420
421
422
423
424
		      Value.OfIdent.empty      (* input: Var.env_in *)
		      Value.OfIdent.empty      (* memory: Var.env *)
              (* 		!solver_vl  *)
            (Verbose.level())
		      "LutExe.is_bool_sat"     (* ctx_msg: string *)
		      g.g_form
		      "LutExe.is_bool_sat"     (* msg: string (?) *)
	       in
	       if not is_bool_sat then (
425
		      [],bdd
426
427
428
429
430
	       ) else (
		      let sols = Solver.solve_formula
			     Value.OfIdent.empty      (* input: Var.env_in *)
			     Value.OfIdent.empty      (* memory: Var.env *)
                (* 			!solver_vl                (* vl: int *) *)
431
              (Verbose.level())
432
433
434
435
436
437
438
439
			     "LutExe.solve_guard"     (* msg: string *)
			     [it.out_var_names]       (* output_var_names: Var.name list list *)
      	     tfdn                     (* p: Thickness.formula_draw_nb *)
			     tn                       (* num_thickness Thickness.numeric *)
			     it.bool_vars_to_gen      (* bool_vars_to_gen_f: formula *)
			     it.num_vars_to_gen       (* num_vars_to_gen: var list *)
			     g.g_form                 (* f: formula *)
		      in 
440
            sols,bdd
441
	       )
442
443
        ) in (
          g.g_sol <- Some zesol;
444
          g.g_bdd <- Some bdd;
445
446
          zesol
        )
447

448

449
450
451
452
453
454
455
456
457
458
let find_one_sol it g =
  let thick =  match MainArg.step_mode it.arg_opt with
    | Lucky.StepInside -> (1,0,Thickness.AtMost 0)
    | Lucky.StepEdges ->  (0,1,Thickness.AtMost 0)
    | Lucky.StepVertices ->  (0,0,Thickness.AtMost 1)
  in
    match find_some_sols it 1 thick g with
	   | s::_ -> s
	   | [] -> raise Not_found
          
459
460

(* check_sat *)
461
let check_satisfiablity (it:t) (g: guard) = (
462
	try (
463
464
465
466
467
468
		Verbose.exe ~flag:dbg
        (fun () -> 
           Printf.printf
			    "--check satisfiablility of \"%s\"\n"
		       (* (Exp.formula_to_string g.g_form); *)
		       (string_of_guard g));
469
470
	  let _ = find_one_sol it g in
		 true
471
472
473
	) with Not_found -> false
)

Erwan Jahier's avatar
Erwan Jahier committed
474
475
476
477
478
479
480
481
482
483
484
485
let min_max_src (bl1,el1,bc1,ec1,bchar1,echar1) (bl2,el2,bc2,ec2,bchar2,echar2) =
  let bl,bc =
    if bl1 < bl2 then bl1,bc1 else if
       bl1 > bl2 then bl2,bc2 else bl1, min bc1 bc2
  in
  let el,ec =
    if el1 > el2 then el1,ec1 else if
       el1 < el2 then el2,ec2 else el1, max ec1 ec2
  in
  (bl,el,bc,ec, min bchar1 bchar2, max echar1 echar2) 
  
  
486
(* Returns the begin/end line/char of a val_exp *)
Erwan Jahier's avatar
Erwan Jahier committed
487
488
489
490
491
492
493
494
495
496
497
498
499
  let (cstr_src_info_of_val_exp : Syntaxe.val_exp -> int * int * int * int * int * int) =
    fun e -> 
      let rec aux (bl,el,bc,ec,bchar,echar) e =
        let acc =
          min_max_src (bl,el,bc,ec,bchar,echar)
            (e.Lexeme.src.Lexeme.line,
             e.Lexeme.src.Lexeme.line,
             e.Lexeme.src.Lexeme.cstart,
             e.Lexeme.src.Lexeme.cend,
             e.Lexeme.src.Lexeme.chstart,
             e.Lexeme.src.Lexeme.chend
            )
        in
500
        match e.Lexeme.it with
Erwan Jahier's avatar
Erwan Jahier committed
501
502
503
504
505
506
507
508
509
510
511
512
513
        | Syntaxe.PRE_n id -> min_max_src acc
          (id.Lexeme.src.Lexeme.line,
           id.Lexeme.src.Lexeme.line,
           id.Lexeme.src.Lexeme.cstart,
           id.Lexeme.src.Lexeme.cend,
           id.Lexeme.src.Lexeme.chstart,
           id.Lexeme.src.Lexeme.chend)
        | Syntaxe.CALL_n (_,vel) -> List.fold_left aux acc vel
        | Syntaxe.ERUN_n(_, ve1, ve2) -> aux (aux acc ve1) ve2
        | Syntaxe.RUN_n (_, ve1, _) ->  aux acc ve1
        | Syntaxe.ASSERT_n (_, ve1, _) ->  aux acc ve1
        | _ -> acc
      in
514
      aux (e.Lexeme.src.Lexeme.line, e.Lexeme.src.Lexeme.line, 
Erwan Jahier's avatar
Erwan Jahier committed
515
           e.Lexeme.src.Lexeme.cstart, e.Lexeme.src.Lexeme.cend, 
516
517
           e.Lexeme.src.Lexeme.chstart, e.Lexeme.src.Lexeme.chend) e
      
518
exception No_src_info
519

520
let rec (to_src_info:  CoIdent.src_stack -> Event.src_info_atom) =
521
  fun l ->
522
    match l with
523
      | [] -> raise No_src_info
524
      | (lxm, _,None)::tl ->
525
526
527
        {
          Event.file = lxm.Lexeme.file;
          Event.line = lxm.Lexeme.line, lxm.Lexeme.line;
Erwan Jahier's avatar
Erwan Jahier committed
528
          Event.char = lxm.Lexeme.cstart, lxm.Lexeme.cend;
529
          Event.stack = if tl=[] then None else Some (to_src_info tl);
530
          Event.str = lxm.Lexeme.str;
531
        }
532
      | (lxm,_,Some ve)::tl -> 
Erwan Jahier's avatar
Erwan Jahier committed
533
        let line_b, line_e, col_b, col_e, char_b, char_e = cstr_src_info_of_val_exp ve in
534
        let file = lxm.Lexeme.file in
535
        let filecontent = Mypervasives.readfile file in
536
537
538
        {
          Event.str =
            (try String.sub filecontent char_b (char_e - char_b + 1)
Erwan Jahier's avatar
Erwan Jahier committed
539
540
             with _ ->
             try String.sub filecontent char_b (String.length filecontent - char_b)
541
542
543
544
             with _ ->
               Printf.sprintf "%s: fail to get chars %i-%i" file char_b char_e);
          Event.file = file;
          Event.line = line_b, line_e;
Erwan Jahier's avatar
Erwan Jahier committed
545
          Event.char = col_b, col_e;
546
547
          Event.stack = if tl=[] then None else Some (to_src_info tl);
        }
548
549


550
let add_to_guard_nc it data (e:CoAlgExp.t) (acc:guard) (si:CoTraceExp.src_info) =
551
552
553
554
555
(* translate e into an Exp.t using lucky_exp_of with an id2exp:
	- that performs unalias
	- that replace input/pre values
*)
	(* necessarily a formula (bool exp), if we rely on type checking ! *)
556
	(* let xenv = it.expanded_code in *)
557
558
559
560
561
562
563
564
565
566
567
568
  let le = contextual_lutexp2exp it data e in
  let f = match le with
	 | Exp.Formu f -> f
	 | _ -> assert false
  in
  let nf = match acc.g_form with
	 | Exp.True -> f
	 | x -> Exp.And (f, x)
  in
    {
	   g_form = nf;
	   g_sol = None;
569
	   g_bdd = None;
570
571
572
      g_src = if snd si = [] then acc.g_src else (snd si)::acc.g_src
	 } 

573
574
exception LocalDeadlock 

575
576
577
(** Add a new constraint to an existing guard *)
let add_to_guard it data (e:CoAlgExp.t) (acc:guard) (si:CoTraceExp.src_info) = (
   let res = add_to_guard_nc it data e acc si in
578
	 if (check_satisfiablity it res) then res
579
	 else raise LocalDeadlock
580
581
)

582
(** Tries to compute a value in a context *)
583
exception Not_a_constant of string 
584
585
let compute_exp (it:t) data e = (
	let le = contextual_lutexp2exp it data e in
586
	try Exp.to_value le
587
	with _ -> raise (Not_a_constant (Exp.to_string le)) 
588
)
589
590
591
592
593
(* same but accept non existing *)
let try_compute_exp (it:t) data e = (
	let le = contextual_lutexp2exp it data e in
	Exp.to_value le
)
594
595
596
(** i.e. but must be int *)
let compute_int (it:t) data e = (
	match (compute_exp it data e) with
597
	| Value.N ( Value.I i) -> Util.int_of_num i
598
599
	| _ -> assert false
)
600

601
(** A behavior (step) of a program *)
602
603
604
605
606
607
type behavior =
| Goto of guard * control_state 
| Raise of string
| Vanish

let string_of_behavior = function
608
609
| Goto (g,c) -> 
   Printf.sprintf "Goto (%s, %s)" (string_of_guard g) (string_of_control_state c)
610
611
612
613
| Vanish -> "Vanish"
| Raise x -> Printf.sprintf "Raise %s" x

type behavior_gen =
614
|  NoMoreBehavior of int
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
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
|  SomeBehavior of behavior * (unit -> behavior_gen)


(*****************************************************************************
genpath est la fonction récursive avec continuation :

- un env pour résoudre les alias
- une valeur des data (courants et pres)
- un accumulateur de contrainte (?)
- une continuation
Retourne :
1 behavior + 1 behavior gen


La fonction récursive:
- réalise un parcours "lazzy" de l'arbre de priorité des comportements
- un point dans ce parcours est parfaitement déterminé par :
  * un point de contrôle (statement lutin : CoTraceExp.t)
  * les attributs qui résume le chemin ayant conduit à ce point de contrôle :
    - la valeur des non-contôlables (ins + pres)
	 - l'ensemble des non-contrôlable à traiter
      n.b. ces 2 infos sont dynamiques à cause des scopes de vars. locales,
    - un accumulateur de contraintes, qui permet d'OPTIMISER
	   le parcours (assert, et para) mais N'EST PAS STRICTEMENT
      nécéssaire  
    - la continuation qui dit comment traiter les feuilles
- un point peut s'avérer être un cul de sac, auquel cas il faut
  faut explorer une autre branche. C'est pourquoi la fonction
  récursive prend en argument UNE LISTE de points d'exploration :
  * initialement, il n'y a qu'un point (le top level)
  * au cours de la descente, des points "alternatifs" sont insérés
   (opérateur priorité)
  * en cas de deadlock, on passe au point suivant dans la
    liste de priorité, s'il n'y en a pas, on a un deadlock général

N.B. Pour l'instant, ON SE CONCENTRE SUR LA SEMANTIQUE
DETERMINSITE : i.e. on génère exactement UN comportement :

- les choix INDETERMINISTES (probabilistes) sont transformés
  en choix DETERMINSTES (prioritaires)
- les autres possibilités ne sont pas considérées (pour l'instant)
  donc l'interface "facon lurette" pour faire du test épais dans
  le contrôle est pour l'instant purement "cosmétique"

Traitement des supports locaux:

L'idéal serait de gérer finement les variables locales et leurs pre's
au niveau des scopes (exists), typiquement :
- exist porte la liste des vars + leurs valeurs pres:
  * initialement, les pres sont optionnels (programmés)
  * puis après, ils découlent de la réaction précédente.
Le problème est que la valeur des pres n'est pas connue
au moment puisque la résolution des contraintes est reportée
au top-level, il faudrait donc quand on traite un exist :
  - propager les valeurs des pres,
  - évaluer avec une continuation qui répercute un exists avec
    pres INCONNUS
  - une fois la réaction top-level effectuée, répercuter les 
    valeurs tirées sur les exists "pendants"
=> c'est un peu lourd, on fait à l'ancienne en se basant 
sur l'hypothèse (la propriété !) d'unicité des noms des
variables locales :
  - toutes les variables locales sont considérées "vivantes",
    même en dehors de leur scope. Ca ne pose pas de problème
    puisque qu'on sait par analyse statique (binding) qu'elle
    ne seront jamais utilsée en dehors de leur scope.
  - en conséquence, le scope n'est utilisé QUE pour la
    réinitialisation des pres (après on l'oublie)
  - les pres sont recherchés dans le paquet global
  - une conséquence est que TOUTES les locales sont générées
    et stockées, même quand elles ne servent pas ...

********************************************************************************)

(* A continuation "explore" a leaf
   according to the calling context,
   returns a behavior or raise Deadlock
Pascal Raymond's avatar
Pascal Raymond committed
692
693
694

Debug: a continuation holds a mnemo to help debug

695
*)
Pascal Raymond's avatar
Pascal Raymond committed
696
type cont_mnemo =
697
698
699
700
701
702
703
  | Cnoeps
  | Cfby of control_state
  | Ctry of control_state option 
  | Cpara_head of control_state
  | Cpara_tail of guard * control_state
  | Ccatch of string * control_state option
  | Crun of string
Pascal Raymond's avatar
Pascal Raymond committed
704
705

let string_of_cont_mnemo = function
706
707
708
709
710
711
712
  | Cnoeps  -> "/e" 
  | Cfby cs -> Printf.sprintf ".%s" (string_of_control_state cs)
  | Ctry None -> Printf.sprintf "?"
  | Ctry (Some cs) -> Printf.sprintf "?/%s" (string_of_control_state cs)
  | Ccatch (x, None) -> Printf.sprintf "?%s" x
  | Ccatch (x, Some cs) -> Printf.sprintf "?%s/%s" x (string_of_control_state cs)
  | Cpara_head cs -> Printf.sprintf "&(%s)" (string_of_control_state cs)
713
714
  | Cpara_tail (g, cs) -> 
     Printf.sprintf "&&(%s, %s)" (string_of_guard g) (string_of_control_state cs)
715
  | Crun (s) -> Printf.sprintf "!%s" s
Pascal Raymond's avatar
Pascal Raymond committed
716

717

718
719
720
type e = Event.t
type ctx = Event.t

Pascal Raymond's avatar
Pascal Raymond committed
721
722
723
724
type continuation = {
	doit: behavior -> behavior;
	dbg: cont_mnemo list
}
725
type continuation_ldbg = {
726
727
  doit_ldbg:ctx -> behavior -> (ctx -> behavior -> e)
  ->  (ctx -> e) -> (ctx -> string -> e) -> e;
728
 	dbg_ldbg: cont_mnemo list
729
}
Pascal Raymond's avatar
Pascal Raymond committed
730

731
732
733
734
735
736
let (mk_cont : (behavior -> behavior) -> cont_mnemo -> continuation -> continuation) = 
  fun f d cin -> {
    doit = f;
    dbg = d::(cin.dbg);
  }

737
738
739
let (mk_cont_ldbg : ctx ->  
     (ctx -> behavior -> (ctx -> behavior -> e) -> 
      (ctx -> e) -> (ctx -> string -> e) -> e) -> 
740
     cont_mnemo -> continuation_ldbg ->  
741
     (ctx -> continuation_ldbg -> e) -> e) =
742
743
  fun ctx f d cin cont -> 
    cont ctx {           
744
745
746
747
	   doit_ldbg = f;
	   dbg_ldbg = d::(cin.dbg_ldbg);
    }

748
749
750
751
752
753
754
755
(* a "virtual" branch in the exploration priority tree *)
type branch = {
	br_ctrl: CoTraceExp.t;
	br_data: store;	
	br_supp: support;
	br_acc: guard;
	br_cont: continuation;
}
756
757
758
759
760
761
762
type branch_ldbg = {
	br_ctrl_ldbg: CoTraceExp.t;
	br_data_ldbg: store;	
	br_supp_ldbg: support;
	br_acc_ldbg: guard;
	br_cont_ldbg: continuation_ldbg;
}
763

Pascal Raymond's avatar
Pascal Raymond committed
764
765
766
767
768
let string_of_branch b = (
	"  control: "^(string_of_control_state b.br_ctrl)^"\n"^
	"  data.ins: "^(Value.OfIdent.to_short_string b.br_data.curs)^"\n"^
	"  data.pres: "^(Value.OfIdent.to_short_string b.br_data.pres)
)
769
770
771
772
773
let string_of_branch_ldbg b = (
	"  control: "^(string_of_control_state b.br_ctrl_ldbg)^"\n"^
	"  data.ins: "^(Value.OfIdent.to_short_string b.br_data_ldbg.curs)^"\n"^
	"  data.pres: "^(Value.OfIdent.to_short_string b.br_data_ldbg.pres)
)
Pascal Raymond's avatar
Pascal Raymond committed
774

775

776
777
778
779
780
781
782
(* misc. utils *)
let put_in_seq te1 te2 = (
   if(te1 = TE_eps) then te2
   else if(te2 = TE_eps) then te1
   else (TE_fby (te1,te2))
)
let put_in_para te1 te2 = (
783
  match (te1,te2) with
784
785
786
787
788
789
   | (TE_eps, x) -> x
   | (x, TE_eps) -> x
   | (x, TE_para yl) -> TE_para (x::yl)
   | (x,y) -> TE_para [x; y]
)

790
let (event_incr : ctx -> MainArg.t -> ctx) =
791
792
793
794
  fun ctx opt -> 
  MainArg.event_incr opt;
  Event.incr_event_nb ctx

795
let rec genpath 
Erwan Jahier's avatar
Erwan Jahier committed
796
797
798
799
800
801
          (it : t)
	       (data : store)  (* data env = inputs + pres *)
          (x : CoTraceExp.t)     (* control = lutin trace *)
  = (
  (*-------------------------------------------*)
  (* Correspondance id de trace -> trace exp
802
         N.B. on traque les récursions ?  *)
Erwan Jahier's avatar
Erwan Jahier committed
803
  (*-------------------------------------------*)
804
805
806
807
808
  let xenv = it.expanded_code in
  let id2trace s =
    (Util.hfind (Expand.trace_tab xenv) s).Expand.ti_def_exp
  in
  
Erwan Jahier's avatar
Erwan Jahier committed
809
810
811
  (*-------------------------------------------*
	* Fonction récursive :
   * --------------------------------------------*)
812
813
814
815
816
  let rec rec_genpath br = (
	 let data = br.br_data in
	 let x = br.br_ctrl in
	 let acc = br.br_acc in
	 let cont = br.br_cont in
817
	 Verbose.exe
818
      ~level:3 ~flag:dbg
819
820
821
822
823
824
825
826
      (fun _ -> 
		 Printf.fprintf stderr "++REC_GENTRANS:\n" ;
		 Printf.fprintf stderr "|> CTRL: %s\n" (string_of_control_state br.br_ctrl);	
		 Printf.fprintf stderr "   CONT:\n";
		 List.iter (fun c -> Printf.fprintf 
                             stderr "    %s;\n" (string_of_cont_mnemo c)) br.br_cont.dbg;
		 Printf.fprintf stderr "--------\n";
		);
827
    match br.br_ctrl with
828

Erwan Jahier's avatar
Erwan Jahier committed
829
830
831
832
833
834
835
836
	 (** Aliased trace *)
    | TE_ref s -> (rec_genpath ({br with br_ctrl = id2trace s}))

	 (** Leaves: apply cont *)
    | TE_raise s -> cont.doit (Raise s)
    | TE_eps -> cont.doit Vanish
	 (** No eps: forbids e to vanish (but not to raise !) *)
	 | TE_noeps e -> (
837
838
839
840
841
842
843
844
845
846
847
848
		let noeps_cont = 
        mk_cont (fun a ->
				     Verbose.exe ~flag:dbg 
                             (fun () -> 
                              Printf.printf
                                "-- noeps_cont (%s)\n   in context %s\n"
					                 (string_of_behavior a) (string_of_control_state x));
				     match a with
				     | Vanish -> raise (Deadlock (MainArg.get_event_nb it.arg_opt))
				     | z -> cont.doit z
			       ) (Cnoeps) cont 
      in
Erwan Jahier's avatar
Erwan Jahier committed
849
850
851
852
		rec_genpath ({br with br_ctrl=e; br_cont=noeps_cont})
	 )
    (** Constraint: ~same but solve the conjunction first *)
    | TE_constraint (ae,si) -> (
853
854
      try 
        MainArg.event_incr it.arg_opt; (* try *)
855
		  let new_acc = add_to_guard it data ae acc si in
856
857
858
859
        MainArg.event_incr it.arg_opt; (* sat ou usat*)
		  cont.doit (Goto (new_acc, TE_eps))
      with LocalDeadlock ->
        raise (Deadlock (MainArg.get_event_nb it.arg_opt))
Erwan Jahier's avatar
Erwan Jahier committed
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
	 (* n.b. raise Deadlock if impossible *)
    )
    (** Sequence *)
    | TE_fby (te1, te2) -> (
		let fby_cont = mk_cont (fun a ->
			                     Verbose.exe ~flag:dbg 
                                          (fun () -> 
                                           Printf.printf
                                             "-- fby_cont (%s)\n  in context %s\n"
					                              (string_of_behavior a) 
                                             (string_of_control_state x));
			                     match a with
				                  | Goto (cl,n) -> cont.doit (Goto (cl, put_in_seq n te2))
				                  | Vanish -> rec_genpath ({br with br_ctrl=te2 })
				                  | Raise _ -> cont.doit a
		                       ) (Cfby te2) cont in
      rec_genpath ({br with br_ctrl=te1; br_cont=fby_cont})
    )

879
880
    | TE_prio [] -> raise (Deadlock (MainArg.get_event_nb it.arg_opt))
	 | TE_prio (te::tel) -> (
881
882
883
884
885
886
887
    (** Priority: Deadlock is catched HERE *)
		try (rec_genpath ({br with br_ctrl=te})) with 
      | Deadlock _ -> (
        MainArg.event_incr it.arg_opt; (* try *) 
        MainArg.event_incr it.arg_opt; (* sat ou usat *)
		  rec_genpath ({br with br_ctrl=(TE_prio tel)})
		)
Erwan Jahier's avatar
Erwan Jahier committed
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
    )

	 (** Try similar to a recurse priority *)
    | TE_try (e,eco) -> (
		let try_cont = mk_cont (fun a ->
			                     Verbose.exe ~flag:dbg 
                                          (fun () -> 
                                           Printf.printf 
                                             "-- try_cont (%s)\n  in context %s\n"
					                              (string_of_behavior a) 
                                             (string_of_control_state x));
			                     match a with
				                  | Goto (cl,n) -> cont.doit (Goto (cl, TE_try (n,eco)))
				                  | _ -> cont.doit a 
		                       ) (Ctry eco) cont in
903
904
905
		try rec_genpath ({br with br_ctrl=e; br_cont=try_cont})
      with 
      | Deadlock _ -> (
906
907
908
909
910
911
			 let ec = match eco with
				| Some e' -> e'
				| None -> TE_eps
			 in
			 rec_genpath ({br with br_ctrl=ec})
		  )
Erwan Jahier's avatar
Erwan Jahier committed
912
913
914
915
916
917
	 )
    (** INFINITE WEAK LOOP *)
	 (* must behaves exactly as: (te\eps fby loop te) |> eps *)
    | TE_loop te -> (
		let e' =
		  TE_prio [
918
				put_in_seq (TE_noeps te) (TE_loop te)
Erwan Jahier's avatar
Erwan Jahier committed
919
			 ;
920
921
				TE_eps
			 ]
Erwan Jahier's avatar
Erwan Jahier committed
922
923
924
925
926
927
928
929
930
931
932
933
		in
		rec_genpath ({br with br_ctrl=e'})
	 )
    (** INFINITE STRONG LOOP *)
	 (* must behaves exactly as: (te\eps fby omega te) *)
    | TE_omega te -> (
		let e' = put_in_seq (TE_noeps te) (TE_omega te)
		in
		rec_genpath ({br with br_ctrl=e'})
	 )
	 (** ASSERT *) 
	 (* default assert is WEAK for backward compatibility
934
935
			      must behave EXACTLY as 
				   trap STOP in (te fby raise STOP) &> omega a
Erwan Jahier's avatar
Erwan Jahier committed
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
	  *)
    | TE_assert (a, te, si) -> (
		let stopid = CoIdent.get_fresh (Expand.ident_space xenv) "Stop_loop" in
		let e' = TE_catch (
			          stopid,
			          put_in_para
				         (put_in_seq te (TE_raise stopid))
				         (TE_omega (TE_constraint (a,si)))
				       ,
			            None
		           ) in
		rec_genpath ({br with br_ctrl=e'})
	 )
	 (** STRONG ASSERT *) 
	 (* must behave EXACTLY as
951
				   trap STOP in omega a &> (te fby raise STOP)
Erwan Jahier's avatar
Erwan Jahier committed
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
	  *)
    | TE_strong_assert (a, te, si) -> (
		let stopid = CoIdent.get_fresh (Expand.ident_space xenv) "Stop_loop" in
		let e' = TE_catch (
			          stopid,
			          put_in_para
				         (TE_omega (TE_constraint (a,si)))
				         (put_in_seq te (TE_raise stopid))
				       ,
			            None
		           ) in
		rec_genpath ({br with br_ctrl=e'})
	 )
    (** Exist: problem modifies the data and support, and the cont *)
    | TE_exist (ectx, te) -> (
		let addp inpres (id, eo) = ( 
		  match eo with
		  | None -> inpres
		  | Some e -> (
			 (* first translate to lucky ... *)
			 let v = try compute_exp it data e
973
974
975
976
					   with Not_a_constant msg ->
                    raise (Internal_error ("LutExe.add_pres",
                                           ("initial value of \""^id^"\" ("^msg^
                                              ")must be a uncontrolable expression")))
Erwan Jahier's avatar
Erwan Jahier committed
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
			 in Value.OfIdent.add inpres (id, v)
		  )
		) in
		let new_pres = List.fold_left addp data.pres ectx in
		let new_data = {data with pres=new_pres} in
      rec_genpath ({br with br_ctrl=te; br_data = new_data })
    )
    (** Parallel: at least one ? *)
    | TE_para ([]) -> assert false
    | TE_para ([e]) -> rec_genpath ({br with br_ctrl = e })
    | TE_para (e::el) -> (
		(* continuation for the head statement *)
		let para_head_cont = 
        mk_cont
          ( fun a ->
				Verbose.exe ~flag:dbg
                        (fun () -> 
                         Printf.printf  "-- para_head_cont (%s)\n   in context %s\n"
995
996
					                         (string_of_behavior a) 
                                        (string_of_control_state x));
Erwan Jahier's avatar
Erwan Jahier committed
997
998
999
1000
1001
1002
				match a with
        		(* 1st raises s: whole raises s *)
				| Raise s -> ( cont.doit (Raise s) )
        		(* 1st vanishes: others continue *)
				| Vanish -> (
				  rec_genpath ({br with br_ctrl = TE_para(el)})
1003
				)
Erwan Jahier's avatar
Erwan Jahier committed
1004
1005
1006
1007
1008
1009
1010
1011
1012
				(* 1st do a trans ... *)
				| Goto (cl,n) -> (
				  let para_tail_cont = 
                mk_cont
                  (fun a ->
						 match a with
						 (* others vanish, 1st continue *)
						 | Vanish -> ( cont.doit (Goto (cl,n)) )
						 (* others raise -> forbidden *)
1013
						 | Raise s -> (raise  (Deadlock (MainArg.get_event_nb it.arg_opt)) )
Erwan Jahier's avatar
Erwan Jahier committed
1014
1015
1016
1017
						 | Goto (tcl, tn) -> (
							(* N.B. cl IS ALREADY accumulated in tcl *)
							cont.doit (Goto (tcl, put_in_para n tn))
						 )
1018
					   ) (Cpara_tail (cl, n)) cont in 
1019
              	 (* N.B. cl CONTAINS incoming acc, thus it becomes the whole rec_acc *)
1020
1021
1022
1023
1024
1025
					 let tail_acc = cl in
                (*** BIG BUG: the other_brs IS NOT THE RIGHT ONE ->
                     SHOULD BE THE ONE REACHED WHEN THE Goto (cl,n) WAS GENERATED !!!
                 ***)
           		 rec_genpath ({br with br_ctrl= TE_para(el); br_acc=tail_acc;
                                      br_cont=para_tail_cont})
Erwan Jahier's avatar
Erwan Jahier committed
1026
1027
1028
1029
				)
			 ) (Cpara_head (TE_para el)) cont in
      rec_genpath ({br with br_ctrl=e; br_cont=para_head_cont})
    )
1030
1031


Erwan Jahier's avatar
Erwan Jahier committed
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
	 (** Catch *)
    | TE_catch (i,e,eco) -> (
		let catch_cont = 
        mk_cont
          (fun a ->
			  Verbose.exe ~flag:dbg 
                       (fun () -> 
                        Printf.printf
                          "-- catch_cont (%s)\n   in context %s\n"
					           (string_of_behavior a) (string_of_control_state x));
			  match a with
			  | Goto (cl,n) -> cont.doit (Goto (cl, TE_catch(i, n, eco)))
			  | Raise x -> (
           	 if ( x == i) then (
              	match eco with
              	| None -> cont.doit Vanish
              	| Some ec -> (
                 rec_genpath ({br with br_ctrl=ec })
              	)
           	 ) else cont.doit (Raise x)
			  )
			  | _ -> cont.doit a
          ) (Ccatch (i,eco)) cont in
      rec_genpath ({br with br_ctrl=e ; br_cont=catch_cont})
    )
	 (** Probabilistic choice 
1058
1059
			       we use an internal structure for storing
			       choices where weights are already evaluated
Erwan Jahier's avatar
Erwan Jahier committed
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
	  *)
    | TE_choice wtel -> (
		let weval (s,l) (te, weo) = (
		  let w = match weo with
			 | None -> 1
			 | Some we -> compute_int it data we
		  in
		  if (w <= 0) then
			 (* HERE: warns if strictly negative ? *)
			 (s,l)
		  else (
			 (s+w, (w,te)::l)
		  )
		) in
		let (sum, cel) = List.fold_left weval (0, []) wtel in
1075
1076
1077
1078
1079
1080
1081
      try 
		  let e' = match cel with
		    | [] -> raise (LocalDeadlock)
		    | [(_,e)] -> e
		    | _ -> TE_dyn_choice (sum, cel)
		  in rec_genpath ({br with br_ctrl=e'}) 
      with LocalDeadlock -> raise (Deadlock (MainArg.get_event_nb it.arg_opt))
Erwan Jahier's avatar
Erwan Jahier committed
1082
1083
	 )
	 (* ad hoc node for dynamic simulation: 
1084
1085
1086
1087
1088
			      weights are evaluated (int), guaranted to be > 0,
			      and whose sum is given.
			      Optimize the selection of a head.
			      N.B. the order of the remaining choices is flip-floped
			      as each call (optimization of the "fold").
Erwan Jahier's avatar
Erwan Jahier committed
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
	  *)
    | TE_dyn_choice (sum, cel) -> (
		let rec select_first sum acc cel= (
		  match cel with
		  | [] -> assert false
		  | [(wc, e)] -> assert (sum = wc); (wc,e)::acc
		  | (wc,e)::cel' -> (
          assert (sum > 0);
			 if (Random.int sum < wc) then
				(wc, e)::(acc @ cel')
			 else select_first (sum - wc) ((wc,e)::acc) cel'
		  )
		) in
		let e' = match (select_first sum [] cel) with
		  | [] -> assert false
		  | [(_,e)] -> e
		  | (wc,e)::cel' ->
			  TE_prio [ e; TE_dyn_choice (sum - wc, cel') ]
		in rec_genpath ({br with br_ctrl=e'}) 
	 )
    (** Probabilistic loops
1110
1111
1112
			       just like for choice, we use an ad hoc internal structure
			       holding the dynamic informations
			       (loop counter, goon/stop weight functions) 
Erwan Jahier's avatar
Erwan Jahier committed
1113
1114
1115
	  *)
	 | TE_dyn_loop (getweights, cpt, te) -> (
		(* equivalent to:
1116
1117
				       |goon(cpt): (te \ eps) . dyn_loop(cpt+1, goon, stop, te)
				       |stop(cpt): eps
Erwan Jahier's avatar
Erwan Jahier committed
1118
1119
		 *)
		let (gw, sw) = getweights cpt in
1120
      try
Erwan Jahier's avatar
Erwan Jahier committed
1121
		let e' = ( match (gw, sw) with 
1122
				     | (0,0) -> raise (LocalDeadlock)
Erwan Jahier's avatar
Erwan Jahier committed
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
				     | (0,_) -> TE_eps
				     | (_,_) -> (
					    let goon_branch = put_in_seq
						                     (TE_noeps te)
						                     (TE_dyn_loop (getweights, cpt+1, te))
					    in
					    match sw with
					    | 0 -> goon_branch
					    | _ -> TE_dyn_choice (gw + sw, [ (gw, goon_branch) ; (sw, TE_eps) ])
				     )
			      ) in
		rec_genpath ({br with br_ctrl=e'}) 
1135
      with LocalDeadlock -> raise (Deadlock (MainArg.get_event_nb it.arg_opt))
Erwan Jahier's avatar
Erwan Jahier committed
1136
1137
	 )
	 (** N.B. the "cpt" here is a unique identifier used for compilation
1138
			       -> not relevant for dynamic simulation
Erwan Jahier's avatar
Erwan Jahier committed
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
	  *)
    | TE_loopi (_,min,max,te,si) -> (
		(* eval min and max ONCE here *)
		let imin = compute_int it data min in 
		let imax = compute_int it data max in 
		if ((imin >= 0) && (imin <= imax)) then (
		  (* HERE *)
		  let e' = TE_dyn_loop (LoopWeights.interval imin imax, 0, te) in
		  rec_genpath ({br with br_ctrl=e'})
		) else (
		  (* HERE: need to have a real notion of run-time error with source ref *)
		  let msg = Printf.sprintf
					     "Run-time error: bad step interval in loop (%d, %d)" imin imax
		  in
		  raise (Global_error msg) 
1154
		)
Erwan Jahier's avatar
Erwan Jahier committed
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
	 )
    | TE_loopa (_,av,ecopt,te,si) -> (
		(* eval min and max ONCE here *)
		let iav = compute_int it data av in 
		let iec = match ecopt with
		  | None -> 1+ ((10 * iav) / 100)
		  | Some x -> compute_int it data x
		in
		if ((iec > 0) && (iav > iec) && (iec <= ((20 * iav) /100))) then (
		  (* HERE *)
		  let e' = TE_dyn_loop (LoopWeights.average iav iec, 0, te) in
		  rec_genpath ({br with br_ctrl=e'})
		) else (
		  (* HERE: need to have a real notion of run-time error with source ref *)
		  let msg = Printf.sprintf
					     "Run-time error: bad step average in loop (%d, %d)" iav iec
1171
		  in
Erwan Jahier's avatar
Erwan Jahier committed
1172
		  raise (Global_error msg) 
1173
		)
Erwan Jahier's avatar
Erwan Jahier committed
1174
1175
	 )
	 (* Run initial:
1176
1177
1178
1179
1180
1181
			      - rid is the name of the instance, the expanded code is available
			      through "it.expanded_code.runtab"
			      - vars is the list of vars computed by the run (LocalIns) 
			      - args is the list of input args (uncontrolable expressions)
			      - e is the trace to execute in the new scope
		         => creates a LutExe.t in its initial state and calls TE_dyn_erun
Erwan Jahier's avatar
Erwan Jahier committed
1182
1183
1184
1185
1186
1187
1188
1189
1190
	  *)
	 | TE_erun (rid, vars, args, e) -> (
		(* evaluate init vals in vars cf. TE_exist *)
		let addp inpres (id, eo) = ( 
		  match eo with
		  | None -> inpres
		  | Some e -> (
			 (* first translate to lucky ... *)
			 let v = try compute_exp it data e
1191
1192
1193
1194
				with Not_a_constant msg ->
              raise (Internal_error ("LutExe.add_pres",
                                     ("initial value of \""^id^"\" ("^msg^
                                         ") must be a uncontrolable expression")))
Erwan Jahier's avatar
Erwan Jahier committed
1195
1196
			 in Value.OfIdent.add inpres (id, v)
		  )
1197
1198
		) 
      in
Erwan Jahier's avatar
Erwan Jahier committed
1199
1200
		let new_pres = List.fold_left addp data.pres vars in
		let new_data = {data with pres=new_pres} in
1201
1202


Erwan Jahier's avatar
Erwan Jahier committed
1203
1204
		(* get the corresponding expanded code *)
		let (zecode : Expand.t) = Expand.get_run_expanded_code it.expanded_code rid in
1205

Erwan Jahier's avatar
Erwan Jahier committed
1206
1207
1208
		(* build a slave LutExe *)
		let zeexe = of_expanded_code it.arg_opt zecode in
		let inits = get_init_internal_state zeexe in
1209

Erwan Jahier's avatar
Erwan Jahier committed
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
		(* builds the corresponding abstract reactive prg *)
		let zereact = Reactive.DoStep (to_reactive_prg zeexe inits) in 
		let outids = List.map (fun (id,_) -> id) vars in
		(* build the initial TE_dyn_erun *)
		let e' = TE_dyn_erun (rid, zereact, outids, args, e) in
		rec_genpath ({br with br_ctrl=e'; br_data = new_data})
	 )
	 | TE_dyn_erun_ldbg (rid, react, vars, args, e) -> assert false
	 | TE_dyn_erun (rid, react, vars, args, e) -> (
		(* Evaluates args in context *)
		let eval_arg x = compute_exp it data x in 
		let ins = List.map eval_arg args in 
		(* call the reactive prog *)
		try (
		  let (outs, react') = Reactive.step react ins in
		  (* stores the values in the LocalIns vars *) 
		  Verbose.exe ~flag:dbgrun
                    (fun () -> 
                     Printf.printf
					        "-- run of %s(%s) gives (%s):=(%s)\n   "
					        rid
					        (Value.list_to_string ins ",")
					        (CoIdent.list_to_string vars ",")
					        (Value.list_to_string outs ","));

		  (* let ivars = List.map (id2var it) vars in *)
		  let new_ins = Value.OfIdent.add_list2 data.curs vars outs in 
		  let new_data = {data with curs=new_ins} in
		  (* new cont *)
		  let run_cont = 
          mk_cont
            (fun a ->
1242
1243
1244
1245
1246