Commit 04e06981 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.42 Fri, 20 Jan 2006 15:06:27 +0100 by jahier

Parent-Version:      1.41
Version-Log:

source/luc_exe.ml
source/command_line_luc_exe.ml
source/lurette.ml
source/graph.ml
source/lucky.mli
source/lucky.ml
source/util.ml
source/formula_to_bdd.ml
source/formula_to_bdd.mli
source/fair_bddd.ml
source/fair_bddd.mli
source/bddd.ml
source/bddd.mli
source/solver.mli
source/solver.ml
source/polyhedron.ml
source/polyhedron.mli
source/store.mli
source/store.ml
source/parse_luc.mli
source/parse_luc.ml
source/show_env.ml
source/env_state.mli
source/env_state.ml
source/run_aut.mli
source/run_aut.ml
source/lurettetop.ml
source/draw.mli
source/draw.ml
source/gen_stubs.ml
source/parse_c_scade.ml
source/ne.ml
source/prevar.ml
source/prevar.mli
source/show_luc.ml
utils/lucky.el
install/configure.in
Makefile.common.source
install/Makefile.lurette.in
user-rules
source/Makefile.lurettetop
source/Makefile.gen_fake_lutin
source/Makefile.show_luc
source/Makefile.lucky
source/Makefile.gen_stubs
source/Makefile.lurette_lib
source/Makefile
RUN_ME
TODO
test/time-joly.exp
test/time-joly.res
test/time-ecrins.exp
ihm/xlurette/xlurette_glade_main.ml
ihm/xlurette/xlurette_glade_interface.ml
ihm/xlurette/makefile
polka/caml/Makefile
polka/Makefile.config
source/Makefile.gen_fake_lucky
install/xlurette_sh.in
install/xlurette.sh.in
install/xlurette.bat.in
install/set_env_var.in
install/lurettetop_sh.in
install/lurettetop.sh.in
install/lurettetop.bat.in
install/gen_stubs.sh.in
source/poly_draw.ml
source/poly_draw.mli
source/lustreExp.ml
source/lustreExp.mli
source/exp.ml
source/var.ml
source/type.mli
examples/xlurette/fault-tolerant-heater/degradable-sensors.luc
examples/xlurette/fault-tolerant-heater/heater_control_env.luc
examples/xlurette/fault-tolerant-heater/sensors.luc
source/parser.mly
doc/lurette-man/lurette-man.tex
source/parse_sildex.ml
test/time-asti.exp
RELEASE-NOTES
FAQ
source/gnuplot-socket.ml
source/luc4ocaml.ml
source/luc4ocaml.mli
source/Makefile.gnuplot-rif
source/gnuplot-rif.ml
source/luckyDraw.mli
source/luckyDraw.ml
source/luc4ocaml_nolbl.mli
source/luc4ocaml_nolbl.ml
source/lucky2lus.ml
source/Makefile.luc4ocaml
source/Makefile.lurette_ocaml_lib
source/Makefile.lurette_debug
source/Makefile.luckyDraw
source/Makefile.lucky2lus
xlurette/Scade/GenMake_l4sim.tcl
examples/lucky/external_code/call_external_c_code.luc
examples/lucky/external_code/Makefile
VERSION
install/configure
install/set_env_var.bat.in

Quite a lot of changes this time... far too much...

Fix a at least 5 bugs, and re-organize directories, in particular
the test dir. too much to say...

 * pre pre x was always equal to pre x (bugs introduced in 1.39 or something
I think...).
 * ...

One big improvment is that I have completely changed the way runtime automaton
are handled, using continuations instead of maitaining an explicit
data-structure.
This let me reduce the run_aut module by 75 percent, resulting in much clearer
code, and less buggy, and more efficient. ouaw!

thanks to that, I support DAG now (was rejected before).

The executable that do not need env var are no more called via a script that
call set_env_var, so that they are fully stand-alone: show_luc, lucky,
gen_fake_lucky. This is why util was splitted (util+util2)

source/var.ml
source/lucaml.ml  -> luc4ocaml.ml
source/lucaml.mli -> luc4ocaml.mli

source/run_aut.ml:
   Fix a bug during the backtraking in the dynamic tree.

source/env_state.ml

source/formula_to_bdd.ml
   sort the list of free index, because the first order of variable is
generally
   better.

source/bddd.ml
source/bddd.mli
source/solver.mli
source/solver.ml
source/polyhedron.ml
source/polyhedron.mli
source/store.mli
   Add the verbosity level in a few functions.

source/store.ml
   FIX A BUG in the bdd traversal. Some branches were never visited because
   I was raising a No_numeric_solution exception instead od returning an empty
   store when adding a constraint... This embarassing bug is there from the
   begining... Ouille!

   Also, when a valid integer cannot be found, return a wrong one, which is a
   bug really. But is it better than the current state were raising the no_num
   expt would cut some branches in the bdd. I will fix that problem later.

source/parse_luc.ml
source/lustreExp.ml
source/lustreExp.mli
   The list of pre vars was computed with a ref, which is bad. Moreover,
   the same pre var was created with different indexes, which did not lead
   to incorrect behavior, but still...

source/exp.ml
test/bj.luc
examples/lucky/external_code/call_external_c_code.luc
examples/lucky/external_code/Makefile

Project-Description: Lurette
parent 98380cec
This diff is collapsed.
The Lurette FAQ
* I have an error message that looks like:
* Using LuckyDraw or luc4ocaml, I hace errors such as :
<<luckyDraw.cmx is not a compilation unit description.>>
Certainly you are using a version of ocaml that does not match
the version of the lib it has been compiled with.
* Using lurette, I have an error message that looks like:
"
/tmp/lurette1/lurette__sut.c line 5: parse error before Ctx
...
......@@ -13,7 +20,7 @@ node named "foo". Make sure that you do not have any "foo.c" or
in your current directory. It might confuse Lurette.
* I have an error message that looks like:
* Using lurette, I have an error message that looks like:
"
Undefined first referenced
symbol in file
......
#!/bin/sh
#
# This script creates in lurette-V2-*/$(arch)/bin/ sh scripts
# that sets enviroment variables necessary to the binaries
# in lurette-V2-*/$(arch)/bin to run correctly.
#
# For example, it creates the sh script xlurette that sets
# the rigth env vars and then launches xlurette_exe.
#
# The list of all scripts that are generated that way is
# provided in the README file.
#
CURRENT_DIR=`pwd`
cd share
rm -f config.cache
./configure --prefix $CURRENT_DIR
......@@ -4,21 +4,26 @@
#
# Where to find libs
# INCDIRS = $(HOME)/$(HOST_TYPE)/lib
# LIBDIRS = $(HOME)/$(HOST_TYPE)/lib
ifeq ($(HOST_TYPE),cygwin)
OCAMLLIB = "c:\TEMP\ocaml\lib"
INCDIRS = u:\\cygwin\\lib c:\\TEMP\\ocaml\\lib
LIBDIRS = u:\\cygwin\\lib c:\\TEMP\\ocaml\\lib c:\\cygwin\\lib\\mingw
CAML_INSTALL_DIR=/cygdrive/c/TEMP/ocaml
SYNCHRONE_DIR=//ARPONT/www-verimag/SYNCHRONE
SYNCHRONE_LURETTE_DIR=//ARPONT/www-verimag/SYNCHRONE/lurette/
ifeq ($(HOST_TYPE),win32)
OCAML_LIB="c:\TEMP\ocaml\lib"
OCAMLOPT = /cygdrive/c/TEMP/ocaml/bin/ocamlopt
OCAMLC = /cygdrive/c/TEMP/ocaml/bin/ocamlc
OCAML = /cygdrive/c/TEMP/ocaml/bin/ocaml
CPP_COMPILER=g++ -mno-cygwin
CPP_LINKER=g++ -mno-cygwin
CC=gcc -mno-cygwin -Wall -g -DWIN32 -I "c:\TEMP\ocaml\lib"
OCAMLLIB = "c:\TEMP\ocaml\lib"
INCDIRS = u:\\cygwin\\lib c:\\TEMP\\ocaml\\lib
LIBDIRS = u:\\cygwin\\lib c:\\TEMP\\ocaml\\lib
CAML_INSTALL_DIR=/cygdrive/c/TEMP/ocaml
SYNCHRONE_DIR=//ARPONT/www-verimag/SYNCHRONE
SYNCHRONE_LURETTE_DIR=//ARPONT/www-verimag/SYNCHRONE/lurette/
EXE := .exe
HOSTTYPE32=win32
DWIN32 = -DWIN32
DWIN32 = -DWIN32 -mno-cygwin -I "c:\TEMP\ocaml\lib" -L "c:\TEMP\ocaml\lib"
else
ifeq ($(HOST_TYPE),sparc-sun)
EXE :=
......@@ -33,12 +38,14 @@ ifeq ($(HOST_TYPE),sparc-sun)
HOSTTYPE32=$(HOST_TYPE)
DWIN32 =
else
# LINUX quoi ...
EXE :=
INCDIRS = $(HOME)/$(HOSTTYPE)/lib $(SCADE_INSTALL_DIR)/lib
LIBDIRS = $(HOME)/$(HOSTTYPE)/lib $(SCADE_INSTALL_DIR)/lib
OCAMLLIB = /usr/local/soft/ocaml/3.08.3/lib/ocaml
# XXX si je met des choses la, elles se retrouvent dans les .cmxa gnrs, ce qui n'est pas de bonne augure...
INCDIRS = $(HOME)/$(HOSTTYPE)/lib
LIBDIRS = $(HOME)/$(HOSTTYPE)/lib
OCAMLLIB = /usr/local/soft/ocaml/3.09.0/lib/ocaml
CAML_INSTALL_DIR=/import/linux/soft/ocaml/3.08.3/
CAML_INSTALL_DIR=/import/linux/soft/ocaml/3.09.0/
SYNCHRONE_DIR=/usr/local/www/SYNCHRONE
SYNCHRONE_LURETTE_DIR=/usr/local/www/SYNCHRONE/lurette/
EXE := #
......@@ -49,10 +56,7 @@ endif
OCAMLMAKEFILE = $(HOME)/lurette/OcamlMakefile
LURETTE_PATH = $(HOME)/lurette
OCAMLMAKEFILE = $(HOME)/lurette/OcamlMakefile
LURETTE_PATH = $(HOME)/lurette
ALL_SOURCES = $(SOURCES) $(SOURCES_OCAML)
luc4ocaml is an ocaml library that makes it possible to call Lucky
programs from Ocaml.
*************************************************************************
* INSTALLATION
Just copy the files of the ./lib directory wherever it is convenient for you.
For example, in the
`ocamlc -where`/lucky
directory (that you have to create before)
*************************************************************************
* DOCUMENTATION
The Ocamldoc documentation of that API is in
doc/html/
Confere also the following directories to find examples:
examples/ocaml
examples/rml
examples/lucky
*************************************************************************
* Building files
Thoses example directories contain Makefile that illustrate how programs
should be compiled. Basically one needs to:
(1) import the following ocaml librairies(*):
unix.cmxa str.cmxa bdd.cmxa polka.cmxa luc4ocaml.cmxa
to be used it with ocamlopt, and:
luc4ocaml.cma
to be used it with ocamlc.
(2) tell the ocaml compiler where to find those libs, e.g.,
ocamlc -I +lucky
if you have installed your lucky lib in the `ocamlc -where`/lucky directory.
(*) is someone knows how to group several cmxa into a single file, please
mail me (jahier@imag.fr). nb: for .cma/ocamlc, it works fine.
The necessary libraries are in "lib"
Luckydraw is an ocaml library that makes the Lucky solver and drawer
available from OCaml programs.
*************************************************************************
* INSTALLATION
Just copy the files of the ./lib directory wherever it is convenient for you.
For example, in the
`ocamlc -where`/lucky
directory (that you have to create before)
*************************************************************************
* DOCUMENTATION
The Ocamldoc documentation of that API is in
doc/html/
Confere also the following directories to find examples:
examples/ocaml
examples/c
*************************************************************************
* Building files
Thoses example directories contain Makefile that illustrate how programs
should be compiled. Basically one needs to:
(1) import the following ocaml librairies(*):
unix.cmxa str.cmxa bdd.cmxa polka.cmxa luc4ocaml.cmxa
to be used it with ocamlopt, and:
luc4ocaml.cma
to be used it with ocamlc.
(2) tell the ocaml compiler where to find those libs, e.g.,
ocamlc -I +lucky
if you have installed your lucky lib in the `ocamlc -where`/lucky directory.
(*) is someone knows how to group several cmxa into a single file, please
mail me (jahier@imag.fr). nb: for .cma/ocamlc, it works fine.
The Lurette V2 package
* What is needed
- gcc
- gnu gcc
- gmp (Gnu multiple precision lib)
and optionnally
- gnuplot V3.8i or higher
- dot (graphviz)
to be able to visualize automata.
* Installation rules
......@@ -27,9 +29,6 @@ env vars and then launches xlurette_exe.
-o-
* List of provided tools
......@@ -56,12 +55,6 @@ lurettetop:
xlurette. You can type "help" at the prompt to see the list of
commands.
lutin:
lutin is an high level language/compiler for specifying
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.
lucky:
A lucky (.luc) files interpreter. ".luc" file is the abstract
machine format the Lutin compiler produces. Being able to
......@@ -73,8 +66,7 @@ There are also tools which are used by the ones above that one might
want to use.
gen_fake_lucky:
gen_fake_lutin:
generates a fake lucky/lutin file (from C files generated by the
generates a fake lucky 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.
......@@ -89,10 +81,8 @@ sim2chro:
A timing diagram visualiser (.rif files) by Yann Rémond.
gnuplot-rif:
An sh-script that uses gnuplot to visualise timing diagrams (.rif
files). Requires plot (by M. Sternberg) that is provided into
this package. nb : plot requires gawk (gnu awk) that is not
provided.
A program that uses gnuplot to visualise timing diagrams (.rif
files).
Also confere the tool section at the url
......@@ -104,7 +94,7 @@ http://www-verimag.imag.fr/~synchron/
* AUTHORS
Erwan Jahier Pascal Raymond Yvan Roux Nicolas Halbwachs
Erwan Jahier and Pascal Raymond
-o-
......@@ -115,10 +105,8 @@ http://www-verimag.imag.fr/~synchron/
of them:
o ocaml, camlidl by the ocaml INRIA team
o Cudd, a BDD library by Fabio Somenzi
o polka, cuddaux and mlcuddidl by Bertrand Jeannet
o polka, by Bertrand Jeannet
o sim2chro, by Yann Rémond
o plot, by Michael Sternberg (requires gnu-awk)
o Ocamlmakefile by Markus Mottl
o autoconf, make, emacs, latex, gtk, gnuplot...
o emacs, autoconf, make, latex, gtk, gnuplot...
V1.42
* Fix a couple of Bugs (one in the automata product, one in the bdd traversal)
* Clean-up the distribution, split it up into several packages, etc.
V1.41
* Add External function call from Lucky.
......@@ -21,6 +27,8 @@ V1.40
transition from the current node(s) is labelled by a satisfiable
constraint.
* -verbose now takes an integer (verbosity level)
* First version of the integration in the Scade editor
* Replace the Cudd package by an home made (Pascal Raymond) BDD
......
#!/bin/sh
#
# shell script to execute to install Lurette
# qu <msg> <variable>
qu () {
eval answer=\$$2
accept=
while test -z "$accept"; do
echo
echo "$1"
echo -n "I will use \"$answer\", "
echo -n "hit return to accept, or enter new value: "
read new
if test -z "$new"; then
accept=y
else
answer=$new
fi
done
eval $2=\"$answer\"
}
echo "Lurette installation procedure"
INSTALL_DIR=$PWD
qu "Where do you want to install files (absolute path)?" INSTALL_DIR
echo "
Binaries will be installed in $INSTALL_DIR/bin/ and libraries in
$INSTALL_DIR/lib/. Those directories will be created if necessary.
"
GO=yes
qu "Do you want to proceed the installation (yes/no)?" GO
if test $GO = yes; then
cd install
rm -f config.cache
echo "./configure --prefix $INSTALL_DIR"
./configure --prefix $INSTALL_DIR
else
echo "quitting Lurette installation procedure..."
fi
*********** BUGS
* ???
1 000 000 000
Fatal error: exception Assert_failure("/home/jahier/lurette/source/solver.ml", 30038, 30050)
......@@ -12,7 +14,7 @@ de ne pas g
real est un float. Je ne vois pas bien comment faire, mais bon.
Ou alors, je limite systematiquement à max_c_float...
* Les noms de repertoires avec des espaces foutent la merde .
* Les noms de repertoires avec des espaces foutent la merde.
«
NF : Je viens d'avoir une erreur en utilisant un dossier dont le nom
contient un espace (erreur de gen_stubs). Ceci doit pouvoir être
......@@ -45,8 +47,26 @@ Bien sur, il manipule 10000 variables au lieu de 1000, mais tout de m
*********** A faire
* pour les declarations de fonctions externes, il faudrait plutot utiliser
t1 * t2 -> t3 plitot que t1 -> t2 -> t3, comme le dis la doc d'ailleurs...
* Luc4ocaml : rajouter un get_vertices
* verifier que les ~init secomportent correctement en cas de produit d'automate
* les env_state.d.memory devraient etre des Value.t VarMap.t plutot
que des Var.subst list !!
* Faudrait voir a essayer re reordonner les variables des bdds de temps
à autre (?)
* fonctions externes :
- Faire un tri topologique pour accepter les programmes
du style 'x=f(y) and y=g(z)'
- Rajouter une option --side-effet pour les fonctions qui en font
- Faire en sorte que les fonctions a effets de bords soient appelées
aussi souvent qu'elles apparaissent dans le code
* Ajouter une option -int32 qui utilise des Int32 pour éviter des soucis
avec des entiers trop grands.
......@@ -136,14 +156,6 @@ INCONV
(1) ca oblige les gens à avoir un compilo caml chez eux...
* Hashtbl.length existe dans la 3.08 !!
* utiliser la meme version de caml pour gcc2 et gcc3 car sinon
on ne peut pas reproduire les tests a partir de la graine !!!
* le nom du repertoire share est particulierement mal choisi...
* mettre les .pl* dans le repertoire temporaire.
> * différents fichiers temporaires sont générés dans le répertoire
......@@ -208,10 +220,6 @@ Mais ca complique. On verra apres.
-> appeler du caml ? du C ?
* reporter le contenu de la nouvelle section de d1.1-v2 dans les entetes de modules
* il faudrait au moins pouvoir avoir des pre sur des var de types structurés
* En fait, il faudrait ecrire les regles de typage des expressions
......@@ -228,11 +236,6 @@ Mais ca complique. On verra apres.
pour les contraintes de dimension > 1 (cf code commenté dans store.ml)
* giro :
-> Il faudrait rajouter la possibilité de faire, par ex, des
tirages selon une loi normale pour les variables a générer.
-> En faire un envt plus realiste
* autoconf :
-> tester si gtk est la
......
VERSION_DATE=22-07-05
VERSION=V2-1.40
VERSION_DATE=20-01-06
VERSION=1.41
export VERSION
export VERSION_DATE
inputs {
Heat_on : bool;
}
outputs {
U:real ~min 1.0 ~max 60.0
}
locals {
downI : int ~alias (-100);
upI : int ~alias 100;
Dudt : float ~min -100.0 ~max 100.0
}
nodes { 0 : stable; 1 : stable
}
start_node { 0 }
</