lurette 0.78 Thu, 29 Aug 2002 15:19:15 +0200 by jahier

Parent-Version:      0.77
Version-Log:

source/parse_env.ml:
   Fix a bug where empty ctrl expr labels were causing
   a parse error.

source/control.ml,mli:
   Add those files to the project as should have been done for a while...

   Do not handle infinite values for ctrl expr counters anymore as it is
   useless (and not so easy to be handled properly).

Project-Description: Lurette

.lurette.prcs_aux

@@ -3,7 +3,7 @@
 (Created-By-Prcs-Version 1 3 3)
 (source/command_line_ima_exe.mli 1082 1021651153 b/34_command_li 1.3)
 (doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
-(source/env_state.ml 19663 1027092697 51_env_state. 1.24)
+(source/env_state.ml 19662 1030627155 51_env_state. 1.25)
 (source/graph.ml 2563 1027066799 14_graph.ml 1.7)
 (bin/Makefile.ima_exe 2013 1027066799 b/41_Makefile.i 1.3)
 (source/util.ml 14262 1030614411 35_util.ml 1.24)
@@ -29,9 +29,10 @@
 (test/passerelle.ima 972 1027066799 b/17_passerelle 1.7)
 (source/ima_exe.ml 11903 1030614411 b/32_ima_exe.ml 1.16)
 (doc/automata_format 0 1007379917 b/3_automata_f 1.1)
+(source/control.ml 4179 1030627155 c/4_control.ml 1.1)
 (source/eval.ml 7755 1027066799 49_eval.ml 1.13)
 (source/gen_stubs.ml 33359 1030614411 24_generate_l 1.30)
-(source/parse_env.ml 22104 1027066799 41_parse_env. 1.20)
+(source/parse_env.ml 22055 1030627155 41_parse_env. 1.21)
 (doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
 (source/automata.mli 3397 1027349504 b/46_automata.m 1.2)
 (source/sim2chro.ml 2720 1027943375 b/24_sim2chro.m 1.10)
@@ -47,16 +48,16 @@
 (test/usager.ima 493 1027066799 b/14_usager.env 1.8)
 (README 74 1011881677 10_README 1.2)
 (test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
-(OcamlMakefile 25078 1030614411 17_OcamlMakef 1.35)
+(OcamlMakefile 25170 1030627155 17_OcamlMakef 1.36)
 (source/command_line_ima_exe.ml 2792 1021651153 b/33_command_li 1.4)
 (test/ControleurPorte.rif.exp 4756 1028297733 b/29_Controleur 1.8)
 (Makefile.lurette 609 1030614411 b/38_Makefile.l 1.8)
 (source/show_env.ml 3603 1030532285 43_show_env.m 1.12)
 (source/gne.mli 1079 1027066799 b/36_gne.mli 1.2)
 (source/automata.ml 15708 1027349504 b/47_automata.m 1.2)
+(doc/synthese 2556 1007379917 b/2_synthese 1.1)
 (bin/Makefile.lurette_lib 1765 1030525986 c/2_Makefile.l 1.1)
 (bin/Makefile.gen_stubs 472 1030532285 b/42_Makefile.g 1.2)
-(doc/synthese 2556 1007379917 b/2_synthese 1.1)
 (test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
 (source/show_env.mli 1091 1027066799 42_show_env.m 1.7)
 (test/Makefile 104 1030614411 c/0_Makefile 1.3)
@@ -77,3 +78,4 @@
 (source/print.ml 5883 1030532285 47_print.ml 1.18)
 (test/vrai_tram.h 2468 1027066799 b/7_vrai_tram. 1.3)
 (bin/Makefile.show_ima 1039 1027066799 b/40_Makefile.s 1.4)
+(source/control.mli 2978 1030627155 c/3_control.ml 1.1)

OcamlMakefile

@@ -5,7 +5,7 @@
 #                            For updates see:
 #             http://miss.wu-wien.ac.at/~mottl/ocaml_sources
 #
-#        $Id: OcamlMakefile 1.35 Thu, 29 Aug 2002 11:46:51 +0200 jahier $
+#        $Id: OcamlMakefile 1.36 Thu, 29 Aug 2002 15:19:15 +0200 jahier $
 #
 ###########################################################################
 # Set these variables to the names of the sources to be processed and
@@ -509,11 +509,13 @@ vroum:
 	/usr/bin/time -v ./lurette 10000 1 1 tram.env  usager.env  porte.env  \
 	    passerelle.env -seed 1015403953 -ns2c --no-oracle 
 
-giro_make:
-	../../make_lurette  -sut onlyroll
+vroum2:
+	/usr/bin/time -v lurettetop -seed 1015403953 -ns2c -sut ControleurPorte \
+	-l 10000 -tf 1 -td 1 -go tram  usager  porte  passerelle 
 
-giro: giro_make
-	./lurette 10 1 1 giro.ima
+
+giro: 
+	lurettetop -sut onlyroll giro
 
 
 time:

lurette.prj

 ;; -*- Prcs -*-
 (Created-By-Prcs-Version 1 3 3)
 (Project-Description "Lurette")
-(Project-Version lurette 0 77)
-(Parent-Version lurette 0 76)
+(Project-Version lurette 0 78)
+(Parent-Version lurette 0 77)
 (Version-Log "
+source/parse_env.ml:
+   Fix a bug where empty ctrl expr labels were causing
+   a parse error.
 
-source/lurettetop.ml:
-   Building every temporary files in /tmp/lurette2313/.
+source/control.ml,mli:
+   Add those files to the project as should have been done for a while...
+
+   Do not handle infinite values for ctrl expr counters anymore as it is 
+   useless (and not so easy to be handled properly).
 
 ")
 (New-Version-Log "")
-(Checkin-Time "Thu, 29 Aug 2002 11:46:51 +0200")
+(Checkin-Time "Thu, 29 Aug 2002 15:19:15 +0200")
 (Checkin-Login jahier)
 (Populate-Ignore ())
 (Project-Keywords)
@@ -50,7 +56,7 @@ source/lurettetop.ml:
   (source/rnumsolver.ml (lurette/b/27_rnumsolver 1.6 644))
 
   (source/parse_env.mli (lurette/40_parse_env. 1.9 644))
-  (source/parse_env.ml (lurette/41_parse_env. 1.20 644))
+  (source/parse_env.ml (lurette/41_parse_env. 1.21 644))
 
   (source/show_env.mli (lurette/42_show_env.m 1.7 644))
   (source/show_env.ml (lurette/43_show_env.m 1.12 644))
@@ -65,7 +71,7 @@ source/lurettetop.ml:
   (source/eval.ml (lurette/49_eval.ml 1.13 644))
 
   (source/env_state.mli (lurette/50_env_state. 1.21 644))
-  (source/env_state.ml (lurette/51_env_state. 1.24 644))
+  (source/env_state.ml (lurette/51_env_state. 1.25 644))
 
   (source/automata.mli (lurette/b/46_automata.m 1.2 644))
   (source/automata.ml (lurette/b/47_automata.m 1.2 644))
@@ -79,11 +85,14 @@ source/lurettetop.ml:
   (source/lurettetop.ml (lurette/c/1_lurettetop 1.3 644))
   (source/gen_stubs.ml (lurette/24_generate_l 1.30 644))
 
+  (source/control.mli (lurette/c/3_control.ml 1.1 644))
+  (source/control.ml (lurette/c/4_control.ml 1.1 644))
+
 ; little script that sets env vars and starts the lurette build
   (make_lurette (lurette/27_make_luret 1.15 755))
 
 ;; Make files
-  (OcamlMakefile (lurette/17_OcamlMakef 1.35 644))
+  (OcamlMakefile (lurette/17_OcamlMakef 1.36 644))
   (Makefile.lurette (lurette/b/38_Makefile.l 1.8 644))
 
   (bin/Makefile.show_ima (lurette/b/40_Makefile.s 1.4 644))
@@ -134,8 +143,6 @@ source/lurettetop.ml:
 
   (test/Makefile (lurette/c/0_Makefile 1.3 644))
 
-
-
 )
 (Merge-Parents)
 (New-Merge-Parents)

source/control.ml

+(*-----------------------------------------------------------------------
+** Copyright (C) 2002 - Verimag.
+** This file may only be copied under the terms of the GNU Library General
+** Public License 
+**-----------------------------------------------------------------------
+**
+** File: control.ml
+** Author: jahier@imag.fr
+*)
+
+module StringMap = struct
+  include Map.Make(struct type t = string let compare = compare end)
+end
+
+
+(** Contains all the necessary information to say whether a variable
+  is recoverable or not.
+
+  More precisely, if a control variable [v] comes from a draw between
+  2 values [min] and [max], then we store and maintain [min] and
+  [max] (ie, we apply to it the same computation as [v]). A variable
+  is recoverable if other values would have been possible; hence, we
+  have:
+
+    [v] is recoverable <=> [(v=0 and max >= 1) or (v>0 and min <=0)].
+
+  XXX Normal draw.
+*)
+type recovery_info = (int * int) option
+
+let (string_of_recov : recovery_info -> string) =
+  fun r -> 
+    match r with
+	None -> ""
+      | Some(min, max) -> 
+	  (" [" ^ (string_of_int min) ^ ", " ^ (string_of_int max) ^ "]")
+
+(* exported *)
+type state = (int * recovery_info) StringMap.t 
+
+(* exported *)
+let (compose_state : state -> state -> state) =
+  fun st1 st2 ->
+    (StringMap.fold 
+       (fun str v acc -> StringMap.add str v acc)
+       st1 
+       st2)
+
+
+(* fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b *)
+
+let (state_size : state -> int) =
+  fun st -> 
+    StringMap.fold (fun _ _ cpt -> cpt+1) st 0
+
+(* exported *)
+let (print_state : state -> unit) = 
+   fun st -> 
+     let (pp: string -> int * recovery_info -> unit) = 
+       fun id (i, recov) -> 
+	 output_string stderr ("\t" ^ id ^ " = ");
+	 output_string stderr (string_of_int i);
+	 output_string stderr (" (" ^ (string_of_recov recov) ^ ")\n");
+     in
+       output_string stderr ("Control state: \n");
+       StringMap.iter pp st;
+       flush stderr
+
+(* exported *)
+let (new_state : unit -> state) =
+  fun _ -> 
+    StringMap.empty
+
+(* exported *)
+let (set : string  -> int -> state -> state) =
+  fun id i st -> 
+    StringMap.add id (i, None) st
+
+
+(* exported *)
+let (draw_between : string -> int -> int -> state -> state) =
+  fun id min max st -> 
+    let draw = min + (Random.int (max - min + 1)) in
+      StringMap.add id (draw, (Some(min, max))) st
+
+(* exported *)
+let (draw_gauss : string -> float -> float -> state -> state) =
+  fun id m std st -> 
+    let f = Util.gauss_draw m std in
+    let max_recovering = int_of_float (m +. 100. *. std) in
+    let draw = int_of_float (if f -. (ceil f) < 0.5 then f else f +. 1.) in
+      StringMap.add id (draw, None) st
+
+(* exported *)
+let (dec : string -> state -> state) =
+  fun id st -> 
+    assert (StringMap.mem id st);
+    ( match (StringMap.find id st) with
+	  (i, None) -> 
+	    StringMap.add id (i-1, None) st
+	| (i, Some(min, max)) -> 
+	    StringMap.add id (i-1, Some(min-1, max-1)) st
+    )
+
+(* exported *)
+let (return : string -> state -> int) =
+  fun id st -> 
+    fst (StringMap.find id st)
+
+(* exported *)
+let (return_comp : string -> state -> int) =
+  fun id st -> 
+    if (fst (StringMap.find id st)) > 0 then 0 else 1
+
+
+(* exported *)
+let (is_recoverable : string -> state -> bool) =
+  fun id st -> 
+    let (v, r) = StringMap.find id st in
+      match StringMap.find id st with 
+	  (_,None) -> false
+	| (i, Some(min, max)) -> (i<=0 && max >= 1) || (i>0 && min <=0)
+
+
+
+type expr = state -> state
+
+let (compose_expr : expr -> expr -> expr) =
+  fun e1 e2 -> 
+    (fun state -> e2 (e1 state))
+
+
+type test = 
+  | EqExpr of number * number 
+  | GtExpr of number * number 
+  | GeExpr of number * number 
+and number = 
+  | VarExpr of string 
+  | IntExpr of int 
+
+let (ite : test -> expr -> expr -> state -> state) =
+  fun test e1 e2 st -> 
+    let number_to_int st n =
+      match n with 
+	  VarExpr(id) -> return id st
+	| IntExpr(i) -> i
+    in
+    let bool = 
+      match test with
+	  EqExpr(n1, n2) -> ((number_to_int st n1) = (number_to_int st n2))
+	| GtExpr(n1, n2) -> ((number_to_int st n1) > (number_to_int st n2))
+	| GeExpr(n1, n2) -> ((number_to_int st n1) >= (number_to_int st n2))
+    in
+      if bool then (e1 st) else (e2 st)

source/control.mli

+(*-----------------------------------------------------------------------
+** Copyright (C) 2002 - Verimag.
+** This file may only be copied under the terms of the GNU Library General
+** Public License 
+**-----------------------------------------------------------------------
+**
+** File: control.mli
+** Author: jahier@imag.fr
+*)
+
+(** Defines a [state] ADT that is used for control purposes when
+  executing [ima]. In particular, it is used to translate dynamically
+  lengthed loops of Lutin. This ADT basically maps idents ([string]s)
+  to [int]s.
+*)
+
+type state
+
+val new_state : unit -> state
+val print_state : state -> unit
+
+val compose_state : state -> state -> state
+
+val set : string -> int -> state -> state
+(** [set id i st] sets [id] to [i] in [st]. *)
+
+val draw_between : string -> int -> int -> state -> state
+(** [loop_between id min max] sets [id] to a value uniformally drawn
+  between [min] and [max] in [st]. *)
+
+val draw_gauss : string -> float -> float -> state -> state
+(** [loop_gauss id m std st] sets [id] to a vaue drawn according to a
+  normal law of mean [m] and standard deviation [std] in [st]. *)
+
+val dec : string -> state -> state
+(** [dec id st] decrements [id] in [st]. *)
+
+val return : string -> state -> int
+(** [return id st] returns the binding of [id] in [st]. *)
+
+(* val return_comp : string -> state -> int *)
+(** [return id st] returns 1 if [id] is bound to 0 in [st], and
+  returns 1 otherwise. *)
+
+
+val is_recoverable : string -> state -> bool
+(** [is_recoverable v st] iff [v] is recoverable, namely, if <<other
+  values for the variable are possible according to the spec>>.
+
+  For instance, if [v] has been drawn to 5 after a draw between 2 and
+  9, it means that all values from 2 to 9 would have been legal
+  too. Therefore, if: 
+  - a loop is garded by the value of v, 
+  - [v] is bound to 0 at the current step,
+  - no satisfiable formula can drawn in the end branch of the
+    loop,
+
+  then, since [v] could have been drawn to a bigger value (7, 8, or 9), 
+  it means that the body of the loop can be tried some more. 
+  
+  Similarly, if:  
+  - [v] is not bound to 0 at the current step, but at least 2 steps 
+    have performed
+  - the formula in the body of the loop not satisfiable
+
+  then it means that the end branch can be tried.
+
+  In such cases, we say that variable [v] is recoverable.
+
+  XXX Should variable resulting from a normal draw be always
+  recoverable?  Mathematically, certainly, but in practice?
+*)
+
+
+type expr = state -> state
+(** e.g., [loop_between foo 3 10] is a [expr]. 
+  [(return "foo" (loop_between "foo" 3 10)] is a [post_expr]. 
+*)
+
+val compose_expr : expr -> expr -> expr
+
+type test = 
+  | EqExpr of number * number 
+  | GtExpr of number * number 
+  | GeExpr of number * number 
+and number = 
+  | VarExpr of string 
+  | IntExpr of int 
+ 
+
+val ite : test -> expr -> expr -> state -> state 
+(**  [ite test e1 e2 st] evaluates [e1] if [test] is true, [e2] otherwise. *)
+
+val state_size : state -> int

source/env_state.ml

@@ -16,7 +16,7 @@ open Formula
 (****************************************************************************)
 
 
-(* 
+(*
 ** The environment is a list of graphs whose arcs are labelled by weighted 
 ** formula. 
 *)

source/parse_env.ml

@@ -351,10 +351,12 @@ and (parse_list_ctrl_expr : aut_token -> Control.expr) =
 	print_err_msg tok_list "parse_list_ctrl_expr" ;
 	raise e
     in
-      List.fold_left 
-	(fun ce1 ce2 -> (fun st -> ce2 (ce1 st)))
-	(List.hd ce_list) 
-	(List.tl ce_list)
+      if ce_list = [] then (fun x -> x)
+      else
+	List.fold_left 
+	  (fun ce1 ce2 -> (fun st -> ce2 (ce1 st)))
+	  (List.hd ce_list) 
+	  (List.tl ce_list)
 and (parse_ctrl_expr: aut_token -> Control.expr) = 
   fun tok -> 
     let tok_list = Stream.npeek 10 tok in
@@ -363,9 +365,6 @@ and (parse_ctrl_expr: aut_token -> Control.expr) =
 	    [< 'Genlex.Ident "Set" ; 'Genlex.Ident varname ; 'Genlex.Int i 
 	    >] ->
 	      (Control.set varname i)
-	  | [< 'Genlex.Ident "Set_inf" ; 'Genlex.Ident varname 
-	    >] ->
-	      (Control.set_inf varname)
 	  | [< 'Genlex.Ident "Draw_between" ; 'Genlex.Ident varname ;
 	       'Genlex.Int min ; 'Genlex.Int max 
 	    >] ->