Commit 124c55f1 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.135 Tue, 06 May 2003 15:51:08 +0200 by jahier

Parent-Version:      0.134
Version-Log:

Implement a check_assertion rule that checks every programs assertions.

source/*.ml:
   Consistently display the help msg on stderr if something bad happened,
   and on stdout if --help is provided at the command line.

source/lurette.ml:
source/sim2chro.ml:
   Fix a bug (found by Nicolas Dervaux) where the sut output var were
   not in the same order than in their declaration.

   Also, interchange input by output in the produced rif file, since
   it is more sensible this way from the tester point of view.

Project-Description: Lurette
parent 4bc90dac
This diff is collapsed.
The LURETTE V2 package
The LURETTE V2 package
* WHAT IS IT?
The lurette V2 package is a set of tools that let one test and
simulate reactive programs (e.g., written in lustre). Its heart is
made of an engine that draws (boolean, integers and real) values
according to a non-deterministic specification written in the lutin
The lurette V2 package is a set of tools that let one test and
simulate reactive programs (e.g., written in lustre). Its heart is
made of an engine that draws (boolean, integers and real) values
according to a non-deterministic specification written in the lutin
language.
The provided tools are:
xlurette:
xlurette is a GUI build on top of lurettetop (see above).
It is probably your best entry point if you want to
(automatically) test your lustre programs.
Cf doc/lurette-tut.ps and/or check the tooltip displayed
when mouse pointing at the different buttons of the GUI.
xlurette:
xlurette is a GUI build on top of lurettetop (see above). It is
probably your best entry point if you want to test your lustre
programs.
Cf doc/lurette-tut.ps and/or check the tool-tip displayed when
mouse pointing at the different buttons of the GUI.
lurettetop:
lurettetop is a top level loop that let one test
reactive programs written in lustre. It is basically the non
graphical version of xlurette.
You can type "help" at the prompt for more information.
lurettetop is a top level loop that let one test reactive
programs written in lustre. It is basically the non graphical
version of xlurette. You can type "help" at the prompt to see
the list of commands.
lutin:
lutin is an high level language for specifying non
deterministic systems. As far as lurette is concerned,
lutin can be used to simulate the System Under Test
environnement.
lutin:
lutin is an high level language/compiler for specifying non
deterministic systems. As far as lurette is concerned, lutin can
be used to simulate the System Under Test (SUT) environment.
More information is available in the doc/lutin.pdf file.
There are also tools which are used by the ones above that one might
want to use.
gen_fake_lutin:
generates a fake lutin file (from C files generated by the
lustre compiler). It is automatically called from xlurette,
whenever you try to test a program without providing any
environment for it; hence you should not need to use
it directly.
generates a fake lutin file (from C files generated by the
lustre compiler). It is automatically called from xlurette,
whenever you try to test a program without providing an
environment for it; hence you should not need to use it directly.
show_luc:
This program lets you vizualise lucky (.luc) files offline.
It is also called automatically from xlurette and lurettetop.
This program lets you vizualise lucky (.luc) files off-line. It
is also called automatically from xlurette and lurettetop.
lucky:
A lucky (.luc) files interpreter. ".luc" file is the abstract
machine format the lutin compiler produces.
Being able to simulate/executes lutin programs outside xlurette
can sometimes be convenient.
lucky:
A lucky (.luc) files interpreter. ".luc" file is the abstract
machine format the lutin compiler produces. Being able to
simulate/executes lutin programs outside xlurette can sometimes
be convenient.
Also cf the tool section at the url http://www-verimag.imag.fr/~synchron/
Also confere the tool section at the url http://www-verimag.imag.fr/~synchron/
-o-
-o-
* INSTALLATION
......@@ -63,7 +66,7 @@ Also cf the tool section at the url http://www-verimag.imag.fr/~synchron/
$ cd lurette-XXX
$ ./INSTALL
-o-
-o-
* Authors
......
......@@ -5,20 +5,20 @@
*********** A faire maintenant
* attention, xlurette suppose que j'ai du lustre (appel de lusinfo),
alors que j'avais dit que ca aurait pu etre du c ...
* lurettetop :utilise Filename.temp_file pour creer un repertoire temporaire
pour lurette.
* xlurette: si le nom du repertoire est le meme que le repertoire courant, je pourrais l'omettre ...
* Utiliser l'ordre des parametres plutot que leur noms
Quoique, quand on fait le produit de plusieurs automates,
ca n'est guere pratique...
--> 2 options : --var-order (default), --var-name
* rajouter une option qui dit si les formules doivent etre tronquees
dans show_luc
* Mettre a jour le parseur wrt les modifs que j'ai faite a la syntax
(noeuds transiants/stationnaires + formula = ...)
* rajouter une commande plot qui fasse appel a gnuplot plut qu'a sim2chro.
* Repasser a une notation infixée pour le format lucky. Ne pas faire
la verif de type en meme temps que le parsing ->
......@@ -46,6 +46,12 @@ la verif de type en meme temps que le parsing ->
* remplacer l'epaisseur de formules par un taux de couverture
* rajouter une option qui dit si les formules doivent etre tronquees
dans show_luc
* Mettre a jour le parseur wrt les modifs que j'ai faite a la syntax
(noeuds transiants/stationnaires + formula = ...)
......
......@@ -39,9 +39,17 @@ ICFLAGS = \
#
# XCFLAGS should be the same than the one with which CUDD is compiled
#
XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
# i386-linux
# XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
# sparc-sun
# XCFLAGS = -mcpu=ultrasparc -DHAVE_IEEE_754 -DUNIX100
# Windows95/98/NT with Cygwin tools
XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DHAVE_GETRLIMIT=0 -DRLIMIT_DATA_DEFAULT=67108864
CFLAGS = $(ICFLAGS) $(XCFLAGS) -O3 -DNDEBUG
CFLAGS_DEBUG = $(ICFLAGS) $(XCFLAGS) -O1 -g -UNDEBUG
CFLAGS_PROF = $(ICFLAGS) $(XCFLAGS) -O3 -DNDEBUG -g -pg
......
-include $(LURETTE_PATH)/Makefile.common
-include $(LURETTE_PATH)/Makefile.common.source
ifndef BIN_INSTALL_DIR
BIN_INSTALL_DIR := ../../$(HOSTTYPE)/bin
BIN_INSTALL_DIR := ../../$(HOST_TYPE)/bin
endif
THREAD=
# THREAD=-thread threads.cma
xlurette: dummy
mlglade xlurette.glade
mv xlurette_glade_interface.ml xlurette_glade_interface.ml0
cat xlurette_glade_interface.ml0 \
| sed -e 's/\"pixmaps\//((Unix.getenv \"LURETTE_PATH\") \^ \"\/share\/pixmaps\/\" \^ \"/' \
| sed -e 's/.xpm\"/.xpm\")/' \
> xlurette_glade_interface.ml
ocamlc -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlc -c -i -I +lablgtk -labels -c xlurette_glade_callbacks.ml
ocamlc -c -pp "camlp4o" -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
......@@ -21,22 +28,37 @@ xlurette: dummy
opt: dummy
mlglade xlurette.glade
ocamlopt -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlopt -c -I +lablgtk -labels -c xlurette_glade_callbacks.ml
ocamlopt -c -pp "camlp4o" -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
ocamlopt -I +lablgtk -I +str -labels -o xlurette unix.cmxa lablgtk.cmxa gtkInit.cmx \
mv xlurette_glade_interface.ml xlurette_glade_interface.ml0
cat xlurette_glade_interface.ml0 \
| sed -e 's/\"pixmaps\//((Unix.getenv \"LURETTE_PATH\") \^ \"\/share\/pixmaps\/\" \^ \"/' \
| sed -e 's/.xpm\"/.xpm\")/' \
> xlurette_glade_interface.ml
ocamlopt.opt -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlopt.opt -c -I +lablgtk -labels -c xlurette_glade_callbacks.ml
ocamlopt.opt -c -pp "camlp4o" -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
ocamlopt.opt -I +lablgtk -I +str -labels -o xlurette unix.cmxa lablgtk.cmxa gtkInit.cmx \
xlurette_glade_callbacks.cmx xlurette_glade_interface.cmx xlurette_glade_main.cmx
opt_opt: dummy
mlglade xlurette.glade
mv xlurette_glade_interface.ml xlurette_glade_interface.ml0
cat xlurette_glade_interface.ml0 \
| sed -e 's/\"pixmaps\//((Unix.getenv \"LURETTE_PATH\") \^ \"\/share\/pixmaps\/\" \^ \"/' \
| sed -e 's/.xpm\"/.xpm\")/' \
> xlurette_glade_interface.ml
ocamlopt.opt -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlopt.opt -c -I +lablgtk -labels -c xlurette_glade_callbacks.ml
ocamlopt.opt -pp "camlp4o" -c -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
ocamlopt.opt -linkall -I +lablgtk -I +str -labels -o xlurette str.cmxa unix.cmxa lablgtk.cmxa gtkInit.cmx \
ocamlopt.opt -I +lablgtk -I +str -labels -o xlurette unix.cmxa lablgtk.cmxa gtkInit.cmx \
xlurette_glade_callbacks.cmx xlurette_glade_interface.cmx xlurette_glade_main.cmx
# ocamlopt.opt -cclib /usr/openwin/lib/libXext.a -cclib /usr/openwin/lib/libX11.a -cclib /usr/local/lib/libglib.a -cclib /usr/local/lib/libgdk.a -cclib /usr/local/lib/libgtk.a -cclib /usr/local/lib/libgmodule.a -cclib -L/usr/openwin/lib -I /home/jahier/sparc-sun/lib -I +lablgtk -I +str -labels -o xlurette str.cmxa unix.cmxa lablgtk.cmxa gtkInit.cmx xlurette_glade_callbacks.cmx xlurette_glade_interface.cmx xlurette_glade_main.cmx -cclib -v
install: xlurette
install: opt
cp xlurette $(BIN_INSTALL_DIR)
......
......@@ -77,14 +77,14 @@
<widget>
<class>GtkButton</class>
<name>show_env_button</name>
<tooltip>Show the automata corresponding to the current environment</tooltip>
<tooltip>Show the automata view of the SUT environment</tooltip>
<can_focus>True</can_focus>
<signal>
<name>clicked</name>
<handler>show_env_button_clicked</handler>
<last_modification_time>Thu, 12 Sep 2002 08:23:10 GMT</last_modification_time>
</signal>
<label>Show Environment</label>
<label>Sut Environment</label>
<relief>GTK_RELIEF_NORMAL</relief>
<child>
<left_attach>0</left_attach>
......@@ -438,6 +438,7 @@
<widget>
<class>GtkCombo</class>
<name>sut_name</name>
<can_focus>True</can_focus>
<value_in_list>False</value_in_list>
<ok_if_empty>True</ok_if_empty>
<case_sensitive>False</case_sensitive>
......@@ -449,7 +450,7 @@
<class>GtkEntry</class>
<child_name>GtkCombo:entry</child_name>
<name>sut_name_entry</name>
<tooltip>Name of the program under test</tooltip>
<tooltip>Name of the file containing the System Under Test (SUT)</tooltip>
<can_focus>True</can_focus>
<signal>
<name>changed</name>
......@@ -467,6 +468,7 @@
<widget>
<class>GtkCombo</class>
<name>sut_node</name>
<can_focus>True</can_focus>
<value_in_list>False</value_in_list>
<ok_if_empty>True</ok_if_empty>
<case_sensitive>False</case_sensitive>
......@@ -483,7 +485,7 @@
<class>GtkEntry</class>
<child_name>GtkCombo:entry</child_name>
<name>sut_node_entry</name>
<tooltip>Sut node name</tooltip>
<tooltip>SUT node name</tooltip>
<can_focus>True</can_focus>
<signal>
<name>changed</name>
......@@ -521,6 +523,7 @@
<widget>
<class>GtkCombo</class>
<name>oracle_name</name>
<can_focus>True</can_focus>
<value_in_list>False</value_in_list>
<ok_if_empty>True</ok_if_empty>
<case_sensitive>False</case_sensitive>
......@@ -554,6 +557,7 @@
<widget>
<class>GtkCombo</class>
<name>oracle_node</name>
<can_focus>True</can_focus>
<value_in_list>False</value_in_list>
<ok_if_empty>True</ok_if_empty>
<case_sensitive>False</case_sensitive>
......@@ -583,6 +587,7 @@
<widget>
<class>GtkCombo</class>
<name>env_name</name>
<can_focus>True</can_focus>
<value_in_list>False</value_in_list>
<ok_if_empty>True</ok_if_empty>
<case_sensitive>False</case_sensitive>
......@@ -608,7 +613,7 @@
<class>GtkEntry</class>
<child_name>GtkCombo:entry</child_name>
<name>env_name_entry</name>
<tooltip>Environment file name</tooltip>
<tooltip>Environment file name: its input (resp output) variable types and names should match exactly the SUT output variables (resp input). Note that if no environment is provided, a fake one will generated; this file can serve as a basis to write more sensible environment for the current SUT.</tooltip>
<can_focus>True</can_focus>
<editable>True</editable>
<text_visible>True</text_visible>
......@@ -755,7 +760,7 @@
<handler>quit</handler>
<last_modification_time>Thu, 19 Sep 2002 08:53:53 GMT</last_modification_time>
</signal>
<label> </label>
<label> </label>
<icon>close.xpm</icon>
</widget>
</widget>
......@@ -921,7 +926,7 @@
<widget>
<class>GtkLabel</class>
<name>rif_file_label</name>
<label>Output file</label>
<label>Base output file name </label>
<justify>GTK_JUSTIFY_LEFT</justify>
<wrap>False</wrap>
<xalign>0.5</xalign>
......@@ -1012,8 +1017,8 @@
<widget>
<class>GtkEntry</class>
<name>rif_file</name>
<tooltip>Name of file the test results is put in</tooltip>
<name>rif_file_basename</name>
<tooltip>Begin of the (.rif) file name used to save the test data. If empty, the default value is made of the name of the sut, the name of its environment, and the test length</tooltip>
<can_focus>True</can_focus>
<editable>True</editable>
<text_visible>True</text_visible>
......
This diff is collapsed.
......@@ -36,6 +36,44 @@ type tok = Genlex.token Stream.t
let ok_str = " OK!
"
(**************************************************************************)
let (give_fresh_file_name : string -> string -> string) =
fun prefix suffix ->
let rec (give_fresh_file_name_aux : int -> string) =
fun i ->
let file = (prefix ^ (string_of_int i) ^ suffix) in
if
not (Sys.file_exists file)
then
file
else
give_fresh_file_name_aux (i+1)
in
give_fresh_file_name_aux 1
let rif_file = ref ""
let get_rif_file _ = !rif_file
let (update_rif_file_name : string -> string -> string -> string -> unit) =
fun rif_base_name0 str1 str2 str3 ->
(*
invent a fresh file name, using the provided in rif_base_name0 if not
empty, the 3 other strings otherwise
*)
let rif_base_name =
if
rif_base_name0 <> ""
then
rif_base_name0
else
(* We invent a name if no one is provided *)
(str1 ^ "-" ^ str2 ^ "-" ^ str3 ^ "-")
in
rif_file := (give_fresh_file_name rif_base_name ".rif")
(**************************************************************************)
......@@ -88,20 +126,6 @@ let (gen_stubs : string -> string -> unit) =
flush stderr
)
(**************************************************************************)
let (give_fresh_file_name : string -> string -> string) =
fun prefix suffix ->
let rec (give_fresh_file_name_aux : int -> string) =
fun i ->
let file = (prefix ^ (string_of_int i) ^ suffix) in
if
not (Sys.file_exists file)
then
file
else
give_fresh_file_name_aux (i+1)
in
give_fresh_file_name_aux 1
(**************************************************************************)
......@@ -123,7 +147,11 @@ let rec (readfile_line : in_channel -> string list -> string list) =
let (lusinfo : string -> string list) =
fun file ->
let file_info = file ^ ".nodes_info" in
let cmd = ("lusinfo " ^ file ^ " nodes > " ^ file_info) in
let file_lus =
try ((Filename.chop_extension file) ^ ".lus")
with Invalid_argument _ -> (file ^ ".lus")
in
let cmd = ("lusinfo " ^ file_lus ^ " nodes > " ^ file_info) in
let _ =
if Sys.file_exists file_info then Sys.remove file_info;
if
......@@ -393,23 +421,12 @@ class customized_callbacks = object(self)
(* end *)
(* ) *)
(* in *)
print_string "\ncoucou \n";
flush stdout
method display_rif_file_clicked () =
let cmd_display =
("set_output " ^ self#top_xlurette#rif_file#text ^ "\n" ^
"sim2chro\n") in
output_string oc cmd_display ;
if debug then output_string stderr cmd_display;
flush oc;
flush stderr
output_string oc "\nDelete file \n";
flush oc
method call_sim2chro_clicked () =
let cmd_display =
("set_output " ^ self#top_xlurette#rif_file#text ^ "\n" ^
"sim2chro\n") in
("set_output " ^ (get_rif_file ()) ^ "\n" ^ "sim2chro\n") in
output_string oc cmd_display ;
if debug then output_string stderr cmd_display;
......@@ -439,8 +456,10 @@ class customized_callbacks = object(self)
let draw_nb = self#top_xlurette#draw_nb#text in
let cmd_draw_nb = ("set_draw_nb " ^ draw_nb ^ "\n") in
let rif_file = self#top_xlurette#rif_file#text in
let cmd_rif_file = ("set_output " ^ rif_file ^ "\n") in
let rif_file = (get_rif_file ()) in
let cmd_rif_file =
if rif_file = "" then "" else ("set_output " ^ rif_file ^ "\n")
in
let cmd_step =
if self#top_xlurette#radiobutton_step_yes#active
......@@ -565,9 +584,9 @@ class customized_callbacks = object(self)
)
method read_rif_files () =
let rif_files = (List.rev (get_files_list_filtered "*.rif" [])) in
(* let rif_files = (List.rev (get_files_list_filtered "*.rif" [])) in *)
(* if rif_files <> [] then *)
(* self#top_xlurette#list_rif_files#clear_items 0 100; *)
(* self#top_xlurette#list_rif_files#clear_items 0 100; *)
(* ( *)
(* let _ = *)
(* List.fold_left *)
......@@ -580,7 +599,7 @@ class customized_callbacks = object(self)
(* rif_files *)
(* in *)
()
(* self#top_xlurette#env_name#entry#set_text env *)
(* self#top_xlurette#env_name#entry#set_text env *)
(* ) *)
......@@ -610,8 +629,14 @@ class customized_callbacks = object(self)
self#read_env_files ();
self#top_xlurette#env_name#entry#set_text (node ^ "_env.lut")
);
self#top_xlurette#rif_file#set_text (give_fresh_file_name "lurette" ".rif");
);
update_rif_file_name
self#top_xlurette#rif_file_basename#text
(remove_extension self#top_xlurette#sut_name#entry#text)
(remove_extension self#top_xlurette#env_name#entry#text)
self#top_xlurette#test_length#text ;
let all_cmds = (self#get_all_cmds ()) ^ "run\n" in
if self#top_xlurette#radiobutton_step_yes#active
......@@ -687,10 +712,10 @@ class customized_callbacks = object(self)
method set_draw_nb i =
self#top_xlurette#draw_nb#set_text (string_of_int i)
method get_rif_file () =
self#top_xlurette#rif_file#text
method set_rif_file str =
self#top_xlurette#rif_file#set_text str
method get_rif_file_basename () =
self#top_xlurette#rif_file_basename#text
method set_rif_file_basename str =
self#top_xlurette#rif_file_basename#set_text str
method get_restore () =
self#top_xlurette#saved_session_file#text
......@@ -883,10 +908,10 @@ let rec speclist callbacks =
"--output", Arg.String (fun s -> callbacks#set_rif_file s),
"--output", Arg.String (fun s -> callbacks#set_rif_file_basename s),
("<string>\tSet the output file name (default is \"" ^
(callbacks#get_rif_file ()) ^ "\").");
"-o", Arg.String (fun s -> callbacks#set_rif_file s), "<string>\n";
(callbacks#get_rif_file_basename ()) ^ "\").");
"-o", Arg.String (fun s -> callbacks#set_rif_file_basename s), "<string>\n";
"--restore", Arg.String (fun s -> callbacks#set_restore s; restore := true),
......@@ -909,29 +934,16 @@ let rec speclist callbacks =
let main () =
let _ =
let _ =
(* Check that LURETTE_PATH env var is set. *)
try
Sys.getenv "LURETTE_PATH"
with Not_found ->
(
print_string "*** Can not run xlurette, sorry. \n***";
print_string "You need to set the LURETTE_PATH env variable properly.\n";
flush stdout;
exit 2;
)
in
(* To turn around a bug in mlglade which searches the pixmaps dir
in the current dir instead of the xlurette one... *)
Sys.remove "pixmaps";
try
(* XXX Won't work under window$ !!! *)
Unix.symlink
(Filename.concat (Unix.getenv "LURETTE_PATH") "ihm/xlurette/pixmaps")
"pixmaps";
with _ ->
print_string "*** Can not create a file in the current directory.\n";
flush stdout
(* Check that LURETTE_PATH env var is set. *)
try
Sys.getenv "LURETTE_PATH"
with Not_found ->
(
print_string "*** Can not run xlurette, sorry. \n***";
print_string "You need to set the LURETTE_PATH env variable properly.\n";
flush stdout;
exit 2;
)
in
let callbacks = new customized_callbacks in
let xlurette = new Xlurette_glade_interface.top_xlurette callbacks in
......@@ -1021,6 +1033,7 @@ let main () =
if (callbacks#get_env () = "") then callbacks#set_env env_saved;
xlurette#xlurette#show() ;
xlurette#xlurette#connect#destroy ~callback: quit;
let _ = Timeout.add ~ms:100 ~callback:callbacks#read_pipe in
......
digraph G {
size="7.5,10" ;
rankdir = TB ;
}
digraph G {
size="7.5,10" ;
rankdir = LR ;
}
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 134)
(Parent-Version lurette 0 133)
(Project-Version lurette 0 135)
(Parent-Version lurette 0 134)
(Version-Log "
Various changes related to the packaging of lurette.
Implement a check_assertion rule that checks every programs assertions.
source/*.ml:
Consistently display the help msg on stderr if something bad happened,
and on stdout if --help is provided at the command line.
source/lurette.ml:
source/sim2chro.ml:
Fix a bug (found by Nicolas Dervaux) where the sut output var were
not in the same order than in their declaration.
Also, interchange input by output in the produced rif file, since
it is more sensible this way from the tester point of view.
")
(New-Version-Log ""
)
(Checkin-Time "Tue, 22 Apr 2003 17:18:57 +0200")
(Checkin-Time "Tue, 06 May 2003 15:51:08 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -22,14 +34,14 @@ Various changes related to the packaging of lurette.
;; Sources files for luc_exe
(source/luc_exe.mli (lurette/b/31_ima_exe.ml 1.2 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.30 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.31 644))
(source/command_line_luc_exe.ml (lurette/b/33_command_li 1.14 644))
(source/command_line_luc_exe.mli (lurette/b/34_command_li 1.10 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.13 644))
(source/lurette.ml (lurette/12_lurette.ml 1.67 644))
(source/lurette.ml (lurette/12_lurette.ml 1.68 644))
(source/command_line.ml (lurette/b/20_command_li 1.13 644))
(source/command_line.mli (lurette/b/21_command_li 1.11 644))
......@@ -76,14 +88,14 @@ Various changes related to the packaging of lurette.
(source/automata.mli (lurette/b/46_automata.m 1.3 644))
(source/automata.ml (lurette/b/47_automata.m 1.7 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.6 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.15 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.7 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.16 644))
(source/gne.mli (lurette/b/36_gne.mli 1.5 644))
(source/gne.ml (lurette/b/37_gne.ml 1.5 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.31 644))