Commit 4bc90dac authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.134 Tue, 22 Apr 2003 17:18:57 +0200 by jahier

Parent-Version:      0.133
Version-Log:

Various changes related to the packaging of lurette.

Project-Description: Lurette
parent dbc00f74
This diff is collapsed.
#
# Makefile to build, lurette, lucky, and co, plus cuddaux and mlcuddidl.
#
# In order to use and install it, you need somehow in your paths:
#
# (1) The ocaml compiler (version 3.02 or higher):
# http://caml.inria.fr/
#
# (2) The stub code generator CamlIDL (version 1.04):
# http://caml.inria.fr/camlidl/
#
# (3) The BDD library CUDD (version 2.3.1)
# http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html
#
# You also need cuddaux aux and mlcuddidl by Bertrand Jeannet, but since it
# GNU-software, and to make the installation process smother, I have chosen
# to include them in this package.
#
#########################################################################
# Where to install bins, libs, and include files
BIN_INSTALL_DIR = $(LURETTE_PATH)/$(HOST_TYPE)/bin
LIB_INSTALL_DIR = $(LURETTE_PATH)/$(HOST_TYPE)/lib
INC_INSTALL_DIR = $(LURETTE_PATH)/$(HOST_TYPE)/include
INCDIRS = $(LURETTE_PATH)/$(HOST_TYPE)/lib /home/jahier/lib
LIBDIRS = $(LURETTE_PATH)/$(HOST_TYPE)/lib /home/jahier/lib
# OCAML tools
OCAMLC = ocamlc.opt
OCAMLOPT = ocamlopt.opt
OCAMLDEP = ocamldep
OCAMLLIB = /home/jahier/lib/ocaml
OCAMLBEST = opt
OCAMLVERSION = 3.06
CAMLIDL = camlidl
all: Cuddaux Mlcuddidl Lucky-and-co Xlurette
Lucky-and-co:
cd source; make install
Cuddaux:
cd cuddaux ; make install
Mlcuddidl:
cd mlcuddidl ; make install
Xlurette:
cd ihm/xlurette ; make install
-include ../.$(HOSTTYPE)/Makefile.common
-include ../user-rules
......@@ -5,10 +5,9 @@
# Where to find libs
INCDIRS = /home/jahier/$(HOSTTYPE)/lib
LIBDIRS = /home/jahier/$(HOSTTYPE)/lib
INCDIRS = /home/jahier/$(HOST_TYPE)/lib
LIBDIRS = /home/jahier/$(HOST_TYPE)/lib
HOST_TYPE=i386-linux
OCAMLMAKEFILE = /home/jahier/lurette/OcamlMakefile
LURETTE_PATH = /home/jahier/lurette
......
The LUCKY package
The LURETTE V2 package
* WHAT IS IT?
The lucky package is a set of tools that let one test and simulate
reactive programs (e.g., written in lustre). The heart of it made of
an engine that draws (boolean, integers and real) values according to
a non-deterministic specification.
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:
......@@ -16,64 +17,59 @@ 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.
lurettetop:
lurettetop is a top level loop that let one test
reactive programs written in lustre.
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 can be useful either if xlurette is broken
or if (like me) your are not a GUI-clickodrom fan.
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.
More information is available in the doc/lutin.pdf file.
lucky:
Previous tools use a descrition a the environement
contained in a .luc files.
show_luc:
This program lets you vizualise .luc files offline.
-o-
* WHAT IS NEEDED?
For lurettetop and xlurette, you need:
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.
(a) An ocaml compiler (version 3.06):
http://caml.inria.fr/
show_luc:
This program lets you vizualise lucky (.luc) files offline.
It is also called automatically from xlurette and lurettetop.
(b) The CamlIDL stub code generator (version 1.04):
http://caml.inria.fr/camlidl/
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.
For show_luc (and hence for the other tools since the can use show_luc),
you need:
(a) gv (for post-script viewing)
(b) dot (for graph drawing)
Also cf the tool section at the url http://www-verimag.imag.fr/~synchron/
-o-
* BINARY VERSION INSTALLATION
Here is what you need to do to install and use those tools.
$ tar xvfz lurette-XXX.tgz
* INSTALLATION
$ tar xvfz luretteV2-XXX.tgz
$ cd lurette-XXX
$ ./INSTALL
$ source lucky_init.sh
# or "source lucky_init.csh" if you are using csh
# also, you may wish to put that statement in your .bashrc ot something
$ make install
# if you wish to install tools anywhere else than lurette-XXX/os_type/{bin,lib}
-o-
* Authors
Erwan Jahier
Pascal Raymond
Yvan Roux
......
......@@ -5,7 +5,6 @@
*********** A faire maintenant
* Utiliser l'ordre des parametres plutot que leur noms
Quoique, quand on fait le produit de plusieurs automates,
ca n'est guere pratique...
......@@ -75,9 +74,6 @@ la verif de type en meme temps que le parsing ->
-> #test_failure
* Finir le fichier README. Faire un fichier INSTALL.
* utiliser Unix.create_process plutot que Sys.command partout !!
......
......@@ -15,15 +15,15 @@ SRCDIR = $(shell pwd)
CUDD_INSTALL = /home/jahier/$(HOSTTYPE)
ifndef BIN_INSTALL_DIR
BIN_INSTALL_DIR := ~/$(HOSTTYPE)/bin
BIN_INSTALL_DIR := /home/jahier/$(HOSTTYPE)/bin
endif
ifndef INC_INSTALL_DIR
INC_INSTALL_DIR := ~/$(HOSTTYPE)/include
INC_INSTALL_DIR := /home/jahier/$(HOSTTYPE)/include
endif
ifndef LIB_INSTALL_DIR
LIB_INSTALL_DIR := ~/$(HOSTTYPE)/lib
LIB_INSTALL_DIR := /home/jahier/$(HOSTTYPE)/lib
endif
......
......@@ -19,7 +19,7 @@ xlurette: dummy
-I +lablgtk -I +str -o xlurette str.cma unix.cma lablgtk.cma gtkInit.cmo \
xlurette_glade_callbacks.cmo xlurette_glade_interface.cmo xlurette_glade_main.cmo
xlurette.opt: 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
......@@ -27,7 +27,7 @@ xlurette.opt: dummy
ocamlopt -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
xlurette.opt_opt: dummy
opt_opt: dummy
mlglade xlurette.glade
ocamlopt.opt -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlopt.opt -c -I +lablgtk -labels -c xlurette_glade_callbacks.ml
......
......@@ -84,7 +84,7 @@
<handler>show_env_button_clicked</handler>
<last_modification_time>Thu, 12 Sep 2002 08:23:10 GMT</last_modification_time>
</signal>
<label>Environment</label>
<label>Show Environment</label>
<relief>GTK_RELIEF_NORMAL</relief>
<child>
<left_attach>0</left_attach>
......@@ -466,7 +466,7 @@
<widget>
<class>GtkCombo</class>
<name>combo2</name>
<name>sut_node</name>
<value_in_list>False</value_in_list>
<ok_if_empty>True</ok_if_empty>
<case_sensitive>False</case_sensitive>
......@@ -482,9 +482,14 @@
<widget>
<class>GtkEntry</class>
<child_name>GtkCombo:entry</child_name>
<name>sut_node</name>
<name>sut_node_entry</name>
<tooltip>Sut node name</tooltip>
<can_focus>True</can_focus>
<signal>
<name>changed</name>
<handler>on_sut_node_changed</handler>
<last_modification_time>Fri, 18 Apr 2003 12:07:57 GMT</last_modification_time>
</signal>
<editable>True</editable>
<text_visible>True</text_visible>
<text_max_length>0</text_max_length>
......@@ -564,7 +569,7 @@
<widget>
<class>GtkEntry</class>
<child_name>GtkCombo:entry</child_name>
<name>combo-entry3</name>
<name>oracle_node_entry</name>
<tooltip>Oracle node name</tooltip>
<can_focus>True</can_focus>
<editable>True</editable>
......@@ -750,7 +755,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>
......
......@@ -306,7 +306,7 @@ let _ = tooltips#set_tip ~text:"Name of the program under test" sut_name#coerce
let _ = sut_name_entry#set_editable true in
let _ = sut_name_entry#set_visibility true in
let _ = sut_name_entry#set_max_length 0 in
let combo2 = GEdit.combo
let sut_node = GEdit.combo
~packing:(hbox13#pack ~padding:0
~fill:true
~expand:true
......@@ -317,13 +317,13 @@ let combo2 = GEdit.combo
~use_arrows:`DEFAULT
()
in
let sut_node = combo2#entry
let sut_node_entry = sut_node#entry
in
let _ = GtkBase.Widget.set_can_focus combo2#as_widget true in
let _ = tooltips#set_tip ~text:"Sut node name" combo2#coerce in
let _ = sut_node#set_editable true in
let _ = sut_node#set_visibility true in
let _ = sut_node#set_max_length 0 in
let _ = GtkBase.Widget.set_can_focus sut_node#as_widget true in
let _ = tooltips#set_tip ~text:"Sut node name" sut_node#coerce in
let _ = sut_node_entry#set_editable true in
let _ = sut_node_entry#set_visibility true in
let _ = sut_node_entry#set_max_length 0 in
let hbox14 = GPack.hbox
~spacing:0
~homogeneous:false
......@@ -368,13 +368,13 @@ let oracle_node = GEdit.combo
~use_arrows:`DEFAULT
()
in
let combo_entry3 = oracle_node#entry
let oracle_node_entry = oracle_node#entry
in
let _ = GtkBase.Widget.set_can_focus oracle_node#as_widget true in
let _ = tooltips#set_tip ~text:"Oracle node name" oracle_node#coerce in
let _ = combo_entry3#set_editable true in
let _ = combo_entry3#set_visibility true in
let _ = combo_entry3#set_max_length 0 in
let _ = oracle_node_entry#set_editable true in
let _ = oracle_node_entry#set_visibility true in
let _ = oracle_node_entry#set_max_length 0 in
let env_name = GEdit.combo
~packing:(table2#attach ~left:1
~top:1
......@@ -462,7 +462,7 @@ let button20 = toolbar4#insert_button
in
let _ = tooltips#set_tip ~text:"Stop the current run" button20#coerce in
let button36 = toolbar4#insert_button
~text: " "
~text: " "
~icon:(GMisc.pixmap (GDraw.pixmap_from_xpm ~file:"pixmaps/close.xpm" ()) ())#coerce
()
in
......@@ -1208,6 +1208,19 @@ let delete_rif_button = toolbar8#insert_button
()
in
let _ = tooltips#set_tip ~text:"Delete selected file" delete_rif_button#coerce in
let label27 = GMisc.label
~text: "This page does not work yet, sorry"
~packing:(vbox15#pack ~padding:0
~fill:false
~expand:true
)
~xalign:0.5
~yalign:0.5
~xpad:0
~ypad:0
~line_wrap:false
()
in
let time_diagrams_label = GMisc.label
~text: "Timing diagrams"
~xalign:0.5
......@@ -1241,6 +1254,8 @@ let _ = button17#connect#clicked
~callback:callbacks#run_lurette in
let _ = oracle_name_entry#connect#changed
~callback:callbacks#on_oracle_name_changed in
let _ = sut_node_entry#connect#changed
~callback:callbacks#on_sut_node_changed in
let _ = sut_name_entry#connect#changed
~callback:callbacks#on_sut_name_changed in
let _ = button33#connect#clicked
......@@ -1281,13 +1296,13 @@ method hbox13 = hbox13
method eventbox1 = eventbox1
method sut_name = sut_name
method sut_name_entry = sut_name
method combo2 = combo2
method sut_node = combo2
method sut_node = sut_node
method sut_node_entry = sut_node
method hbox14 = hbox14
method oracle_name = oracle_name
method oracle_name_entry = oracle_name
method oracle_node = oracle_node
method combo_entry3 = oracle_node
method oracle_node_entry = oracle_node
method env_name = env_name
method env_name_entry = env_name
method scrolledwindow2 = scrolledwindow2
......@@ -1358,6 +1373,7 @@ method vbox15 = vbox15
method toolbar8 = toolbar8
method sim2chro = sim2chro
method delete_rif_button = delete_rif_button
method label27 = label27
method time_diagrams_label = time_diagrams_label
initializer callbacks#set_xlurette self;
notebook1#prepend_page
......
......@@ -40,6 +40,7 @@ let ok_str = " OK!
(**************************************************************************)
let pre_sut_node = ref ""
let (remove_extension : string -> string) =
fun str ->
......@@ -485,8 +486,8 @@ class customized_callbacks = object(self)
then "set_show_step true \n"
else "set_show_step false \n"
in
cmd_oracle ^ cmd_test_length ^ cmd_formula_nb ^ cmd_draw_nb
^ cmd_rif_file ^ cmd_env ^ cmd_sut ^ cmd_step ^ cmd_seed
cmd_test_length ^ cmd_formula_nb ^ cmd_draw_nb
^ cmd_rif_file ^ cmd_sut ^ cmd_env ^ cmd_oracle ^ cmd_step ^ cmd_seed
^ cmd_draw_mode ^ cmd_call_sim2chro ^ cmd_display_local
^ cmd_verbose ^ cmd_show_step
......@@ -494,21 +495,55 @@ class customized_callbacks = object(self)
method on_sut_name_changed () =
let sut = self#top_xlurette#sut_name#entry#text in
if
sut <> ""
sut = ""
then
(
let nodes = (lusinfo self#top_xlurette#sut_name#entry#text) in
if nodes <> [] then self#top_xlurette#sut_node#set_popdown_strings nodes
self#top_xlurette#sut_node#entry#set_text "";
self#top_xlurette#env_name_entry#entry#set_text ""
)
else
self#top_xlurette#sut_node#entry#set_text ""
(
let nodes = (lusinfo self#top_xlurette#sut_name#entry#text) in
if
(* this test is to avoid spurious strings to be written *)
nodes <> []
then
(
self#top_xlurette#sut_node#set_popdown_strings nodes;
let sut_node = self#top_xlurette#sut_node#entry#text in
if
sut_node <> !pre_sut_node
then
(
self#top_xlurette#env_name_entry#entry#set_text "";
pre_sut_node := sut_node
)
)
)
method on_sut_node_changed () =
let sut_node = self#top_xlurette#sut_node_entry#entry#text in
if
sut_node <> !pre_sut_node
then
(
self#top_xlurette#env_name_entry#entry#set_text "" ;
self#top_xlurette#oracle_name_entry#entry#set_text "" ;
self#top_xlurette#oracle_node_entry#entry#set_text "" ;
pre_sut_node := sut_node
)
method read_lustre_files () =
let files = (get_files_list_filtered "*.lus" [""]) in
let sut = self#top_xlurette#sut_name#entry#text
and oracle = self#top_xlurette#oracle_name#entry#text
and sut_node = self#top_xlurette#sut_node#entry#text
and oracle_node = self#top_xlurette#oracle_node#entry#text
and sut_node = self#top_xlurette#sut_node_entry#entry#text
and oracle_node = self#top_xlurette#oracle_node_entry#entry#text
in
if files <> [] then
(
......@@ -516,8 +551,8 @@ class customized_callbacks = object(self)
self#top_xlurette#oracle_name#set_popdown_strings files ;
self#top_xlurette#sut_name#entry#set_text sut;
self#top_xlurette#oracle_name#entry#set_text oracle;
self#top_xlurette#sut_node#entry#set_text sut_node;
self#top_xlurette#oracle_node#entry#set_text oracle_node
self#top_xlurette#sut_node_entry#entry#set_text sut_node;
self#top_xlurette#oracle_node_entry#entry#set_text oracle_node
)
method read_env_files () =
......@@ -555,25 +590,26 @@ class customized_callbacks = object(self)
let nodes = (lusinfo oracle) in
if nodes <> [] then self#top_xlurette#oracle_node#set_popdown_strings nodes;
else
self#top_xlurette#oracle_node#entry#set_text ""
self#top_xlurette#oracle_node_entry#entry#set_text ""
method run_lurette () =
if
self#top_xlurette#env_name#entry#text = ""
self#top_xlurette#env_name#entry#text = ""
then
(* Generate an environment for the current sut *)
(
let sut = self#top_xlurette#sut_name#entry#text in
let node = self#top_xlurette#sut_node#entry#text in
let sut = self#top_xlurette#sut_name_entry#entry#text in
let node = self#top_xlurette#sut_node_entry#entry#text in
self#put "Since no environment is provided, I generate a fake one named\n";
self#put (node ^ "_env.lut, that you can edit and modify.\n\n");
gen_stubs sut node ;
gen_fake_lutin (node ^ ".h") ;
self#top_xlurette#env_name#entry#set_text (node ^ "_env.lut");
(* Fill the combo boxes again, since more files may have been created *)
self#read_lustre_files ();
self#read_env_files ()
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");
......@@ -606,9 +642,9 @@ class customized_callbacks = object(self)
method get_env () =
self#top_xlurette#env_name#entry#text
self#top_xlurette#env_name_entry#entry#text
method set_env str =
self#top_xlurette#env_name#entry#set_text str
self#top_xlurette#env_name_entry#entry#set_text str
method get_sut () =
self#top_xlurette#sut_name#entry#text
......@@ -616,7 +652,7 @@ class customized_callbacks = object(self)
self#top_xlurette#sut_name#entry#set_text str
method get_sut_node () =
self#top_xlurette#sut_node#entry#text
self#top_xlurette#sut_node_entry#entry#text
method set_sut_node str =
self#top_xlurette#sut_node#entry#set_text str
......@@ -722,7 +758,8 @@ class customized_callbacks = object(self)
| [< 'Genlex.Ident "set_env" ; 'Genlex.String str >] ->
self#set_env str
| [< 'Genlex.Ident "set_sut" ; str = parse_file_name ; node = parse_node>] ->
| [< 'Genlex.Ident "set_sut" ; str = parse_file_name ; node = parse_node >] ->
pre_sut_node := node;
self#set_sut str;
self#set_sut_node node
......@@ -884,18 +921,17 @@ let main () =
exit 2;
)
in
if not (Sys.file_exists "pixmaps")
(* To turn around a bug in mlglade which searches the pixmaps dir
in the current dir instead of the xlurette one... *)
then
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
(* 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
in
let callbacks = new customized_callbacks in
let xlurette = new Xlurette_glade_interface.top_xlurette callbacks in
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 133)
(Parent-Version lurette 0 132)
(Project-Version lurette 0 134)
(Parent-Version lurette 0 133)
(Version-Log "
source/gen_stubs.ml:
source/ocaml2C.idl:
use double instead of floats at the C level.
Various changes related to the packaging of lurette.
")
(New-Version-Log ""
)
(Checkin-Time "Thu, 17 Apr 2003 13:22:44 +0200")
(Checkin-Time "Tue, 22 Apr 2003 17:18:57 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -30,7 +29,7 @@ source/ocaml2C.idl:
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.13 644))
(source/lurette.ml (lurette/12_lurette.ml 1.66 644))
(source/lurette.ml (lurette/12_lurette.ml 1.67 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))
......@@ -42,7 +41,7 @@ source/ocaml2C.idl:
(source/env.mli (lurette/15_env.mli 1.17 644))
(source/env.ml (lurette/16_env.ml 1.30 644))
(source/util.ml (lurette/35_util.ml 1.44 644))
(source/util.ml (lurette/35_util.ml 1.45 644))
(source/solver.mli (lurette/38_solver.mli 1.14 644))
(source/solver.ml (lurette/39_solver.ml 1.47 644))
......@@ -57,7 +56,7 @@ source/ocaml2C.idl:
(source/pnumsolver.mli (lurette/d/24_pnumsolver 1.2 644))
(source/parse_env.mli (lurette/40_parse_env. 1.14 644))
(source/parse_env.ml (lurette/41_parse_env. 1.42 644))
(source/parse_env.ml (lurette/41_parse_env. 1.43 644))
(source/show_env.mli (lurette/42_show_env.m 1.8 644))
(source/show_env.ml (lurette/43_show_env.m 1.16 644))
......@@ -83,7 +82,7 @@ source/ocaml2C.idl:
(source/gne.mli (lurette/b/36_gne.mli 1.5 644))
(source/gne.ml (lurette/b/37_gne.ml 1.5 644))