Commit b1a40b56 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.40 Fri, 22 Jul 2005 17:06:41 +0200 by jahier

Parent-Version:      1.39
Version-Log:

source/luc_exe.ml
source/command_line_luc_exe.ml
source/command_line_luc_exe.mli
source/lurette.ml
source/command_line.ml
source/command_line.mli
source/lucky.ml
source/rif.ml
source/env_state.mli
source/env_state.ml
source/run_aut.mli
source/run_aut.ml
source/lurettetop.ml
ihm/xlurette/xlurette_glade_main.ml
  Add a reactive mode where the output of the previous cycle is returned
  when the Lucky environment is blocked (because no transition from
  the current node(s) is labelled by a satisfiable constraint.

Remove the dependence on cygwin to run it under windows.

In particular, to be able to do that, I now use socket instead of pipes
in order to communicate between lurettetop and xlurette.

Also, define proper, cp, rm, etc instead of doing them by sys calls.

A lot of changes to make it work with the scade gui

Project-Description: Lurette
parent 3a6425a6
This diff is collapsed.
......@@ -8,22 +8,50 @@
# INCDIRS = $(HOME)/$(HOST_TYPE)/lib
# LIBDIRS = $(HOME)/$(HOST_TYPE)/lib
INCDIRS = $(HOME)/$(HOSTTYPE)/lib $(SCADE_INSTALL_DIR)/lib
LIBDIRS = $(HOME)/$(HOSTTYPE)/lib $(SCADE_INSTALL_DIR)/lib
ifeq ($(HOST_TYPE),cygwin)
EXE :=
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/
EXE := .exe
HOSTTYPE32=win32
OCAMLMAKEFILE = $(HOME)/lurette/OcamlMakefile
else
ifeq ($(HOST_TYPE),sparc-sun)
EXE :=
INCDIRS = $(HOME)/$(HOSTTYPE)/lib $(SCADE_INSTALL_DIR)/lib
LIBDIRS = $(HOME)/$(HOSTTYPE)/lib $(SCADE_INSTALL_DIR)/lib
OCAMLLIB = /usr/local/soft/ocaml/3.08/lib/ocaml
CAML_INSTALL_DIR=/usr/local/soft/ocaml/3.08/
SYNCHRONE_DIR=/usr/local/www/SYNCHRONE
SYNCHRONE_LURETTE_DIR=/usr/local/www/SYNCHRONE/lurette/
EXE := #
HOSTTYPE32=$(HOST_TYPE)
else
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
CAML_INSTALL_DIR=/import/linux/soft/ocaml/3.08.3/
SYNCHRONE_DIR=/usr/local/www/SYNCHRONE
SYNCHRONE_LURETTE_DIR=/usr/local/www/SYNCHRONE/lurette/
EXE := #
HOSTTYPE32=$(HOST_TYPE)
endif
endif
LURETTE_PATH = $(HOME)/lurette
ALL_SOURCES = $(SOURCES) $(SOURCES_OCAML)
OCAMLMAKEFILE = $(HOME)/lurette/OcamlMakefile
ifeq ($(HOST_TYPE),cygwin)
EXE := .exe
else
EXE :=
endif
LURETTE_PATH = $(HOME)/lurette
ALL_SOURCES = $(SOURCES) $(SOURCES_OCAML)
......@@ -5,7 +5,7 @@
# For updates see:
# http://www.oefai.at/~markus/ocaml_sources
#
# $Id: OcamlMakefile 1.52 Mon, 08 Mar 2004 13:46:15 +0100 jahier $
# $Id: OcamlMakefile 1.53 Fri, 22 Jul 2005 17:06:41 +0200 jahier $
#
###########################################################################
......@@ -733,24 +733,24 @@ endif
$(QUIET)pp=`sed -n -e 's/(\*pp \([^*]*\) \*)/\1/p;q' $<`; \
if [ -z "$$pp" ]; then \
echo $(INTF_OCAMLC) -c $(THREAD_FLAG) \
$(OCAMLFLAGS) $(INCFLAGS) $<; \
$(OCAMLFLAGS) $(INCFLAGS) "$<"; \
$(INTF_OCAMLC) -c $(THREAD_FLAG) $(OCAMLFLAGS) \
$(INCFLAGS) $<; \
$(INCFLAGS) "$<"; \
else \
echo $(INTF_OCAMLC) -c -pp \"$$pp\" $(THREAD_FLAG) \
$(OCAMLFLAGS) $(INCFLAGS) $<; \
$(OCAMLFLAGS) $(INCFLAGS) "$<"; \
$(INTF_OCAMLC) -c -pp "$$pp" $(THREAD_FLAG) \
$(OCAMLFLAGS) $(INCFLAGS) $<; \
$(OCAMLFLAGS) $(INCFLAGS) "$<"; \
fi
.ml.cmi .ml.$(EXT_OBJ) .ml.cmx .ml.cmo: $(EXTRADEPS)
$(QUIET)pp=`sed -n -e 's/(\*pp \([^*]*\) \*)/\1/p;q' $<`; \
if [ -z "$$pp" ]; then \
echo $(REAL_OCAMLC) -c $(ALL_OCAMLCFLAGS) $<; \
$(REAL_OCAMLC) -c $(ALL_OCAMLCFLAGS) $<; \
$(REAL_OCAMLC) -c $(ALL_OCAMLCFLAGS) $<; \
else \
echo $(REAL_OCAMLC) -c -pp \"$$pp\" \
$(ALL_OCAMLCFLAGS) $<; \
$(ALL_OCAMLCFLAGS) $<; \
$(REAL_OCAMLC) -c -pp "$$pp" $(ALL_OCAMLCFLAGS) $<; \
fi
......
V1.40
* Add a reactive mode where the output of the previous cycle is returned
when the Lucky environment is blocked (because no transition from
the current node(s) is labelled by a satisfiable constraint.
* First version of the integration in the Scade editor
* Replace the Cudd package by an home made (Pascal Raymond) BDD
package
V1.39
* Fix a bug where the probability of a translation was sligthly wrong
in some circumstances (namely, when a formula happens to be false
because of the numeric part; in such a case, the draw was done again
from the current node instead of doing it from the last choice point).
in some circumstances (namely, when a formula happens to be false
because of the numeric part; in such a case, the draw was done
again from the current node instead of doing it from the last
choice point).
* Add a button in xlurette that generates default environments for the
current SUT.
* Add a button in xlurette to explicitely generate default
environments for the current SUT.
V1.38
* When no environment is provided, also generate a file named
"<node>_env_UD" in addition to the fake env in "<node>_env". That one
is more elaborated and contraints the output variables so that they
move up and down.
* When no environment is provided, also generate a file named
"<node>_env_UD.luc" in addition to the fake environment
"<node>_env.luc". That one is more elaborated and contraints the
output variables so that they move up and down (saw-edge curve).
* Fix a bug due to the fact that not all variable name start with "_"
in the C code generated by scade, as it was assumed (and generally the case).
* Fix a bug due to the fact that not all variable name start with "_"
in the C code generated by scade, as it was assumed (and generally
the case).
* Fix a bug occurring for lucky formula containing more than 1200 monomes
(float overflew when counting the number of solutions).
* Fix a bug occurring for lucky formula containing more than 1200
monomes because float overflew when counting the number of
solutions. The fix consisted in using a float/logarithm-based
encoding, where the mantissa is a float, and where the exponent is
an integer.
V1.37
* The automatically generated oracle in now named "<sut_node>_always_true.lus"
instead of "always_true.lus".
* The automatically generated oracle in now named
"<sut_node>_always_true.lus" instead of just "always_true.lus".
* fix a bug where xlurettte was crashing down when the seed field
* fix a bug where xlurettte was crashing down when the seed field
(spin button) was empty.
* Allow negative values to be set in xlurette as a seed.
......@@ -34,19 +51,21 @@ V1.37
V1.36
* A better error msg is displayed when one try to write something like
"x : int ^ 3 ~default pre x ^ 3", which is currently not supported.
* A better error msg is displayed when one try to write something
like "x : int ^ 3 ~default pre x ^ 3", which is currently not
supported.
* Fix a bug in gen_fake_lucky that was introduced in V1.33
(incorrect environment were generated).
* Fix a bug in gen_fake_lucky that was introduced in V1.33 (incorrect
environments were generated).
V1.35
* The file <node>_io.c generated by sildex is now automatically deleted
(it is included by <node>.c, and causes compile errors even if lurette
does not use its content, which is only meant for the sildex simulator).
* The file <node>_io.c generated by sildex is now automatically
deleted (it is included by <node>.c, and causes compile errors even
if lurette does not use its content, which is only meant for the
sildex simulator).
* Fix a bug in the step by step mode where the graph was not always
* Fix a bug in the step by step mode where the graph was not always
refreshed when the step was not 1.
V1.34
......
*********** BUGS
* ???
1 000 000 000
Fatal error: exception Assert_failure("/home/jahier/lurette/source/solver.ml", 30038, 30050)
* Le remplacement dynamique de .luc est tres surement cassé (les current_nodes
ne sont pas mis a jour) -> le retester
(nb : cette feature n'est pas documenté de toutes facons)
* time lucky -l 100 six_lines.luc
prend 5 secondes pour n=1000 alors que
time lucky -l 10 six_lines.luc
prend 170 secondes pour n=10000
!!!
* Quand Scade utilise des float, comme caml utilise des doubles,
je dois faire un cast. Il me faudrait un moyen de dire au solver
de ne pas générer des flottants trop grands (max float) quand
real est un float. Je ne vois pas bien comment faire, mais bon.
Ou alors, je limite systematiquement à max_c_float...
* NF : Je viens d'avoir une erreur en utilisant un dossier dont le nom
* 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
éviter en mettant entre guillemets chaques arguments. Ca ne vaut
peut être pas le coup de corriger cela (modification du script
appelant gen_stubs_exe, puis de toutes les commande exécutées par
gen_stubs_exe (appels de cp par exemple)). Une petite note dans la
doc peut être suffisante.
»
* XXX attention a l'affichage du .rif quand lus est syntaxiquement faux dans
l'onglet "diagram manager" d'xlurette.
* cygwin : lurettetop ne marche pas sous un shell cygwin parce qu'il ne
trouve pas le Makefile.lurette. lapin compris pourquoi...
*********** Performances
* time lucky -l 100 six_lines.luc
prend 5 secondes pour n=1000 alors que pour n=10000
time lucky -l 10 six_lines.luc
prend 170 secondes !!! (pour faire autant de tirage in fine ...)
Bien sur, il manipule 10000 variables au lieu de 1000, mais tout de même.
*********** A faire
* precision ne devrait pas vouloir dire "nombre de chiffres apres le virgule"
mais "nombre de chiffres significatifs". Ca me permettrait de plus d'implementer
un Polyhedron.rat_of_float qui soit moint délirant, ainsi que de donner
un max_float qui vaudrait max_int sans risque que ca pete.
* Utiliser le mode --log avec xlurette aussi (pas seulement avec scade_gui)
* j'ai retiré les -I et -L dans Makefile.lurette parce que ca provoquait
des erreurs quand les var telles EXTRA_LIB etaient vides. -> il faudrait
que je les rajoute automatiquement au niveau de xlurette ou mieux,
de lurettetop (quand elles n'y sont pas).
* portage windows
- sim2chro
*** noter quelque part les bidouilles que j'ai du faire
pour compiler le bouzin sous win32
- en particulier, j'ai du faire croire a camlidl que je n'etais
pas sous win32 (#undef _WIN32). En effet, camlidl a été compilé
avec ocamc/mingw et l'option --mno-cygwin. En effet, ...
* autoriser plusieurs automates dans le meme fichier
* gen_stubs devrait etre une API, pas un script
* quand on quitte lurette, on perd les .o et les executables, ce qui
est dommage quand les .c générés sont énormes !!!
* il me faudrait un bouton "gen fake env" qui fasse l'appel idoine explicitement
plutot que d'avoir a le faire en donnant un environement vide.
* de plus, quand scade genere de fcext.dc, le fait de creer un repertoire <node>
est un peu penible, parce que le plus pratique devient alors de
changer de repertoire en allant dans celui-ci, puis de relancer lurette ...
* XXX attention a l'affichage du .rif quand lus est syntaxiquement faux dans
l'onglet "diagram manager" d'xlurette.
* Le remplacement dynamique de .luc est tres surement cassé (les current_nodes
ne sont pas mis a jour) -> le retester
(nb : cette feature n'est pas documenté de toutes facons, et plus utilisé)
* Au sujet des l'heuristique nbac -> lucky, il faudrait peut-etre verifier
que tous les points sont ergodiques (recurrents).
* Dans le mem ordre d'idée :
* Dans le meme ordre d'idée :
Cela pourrait etre relativement utile de connaitre les temps de passage
de chaque noeud (temps au sens, chaine de Markov). En faisant abstraction
......@@ -91,15 +135,6 @@ INCONV
* utiliser la meme version de caml pour gcc2 et gcc3 car sinon
on ne peut pas reproduire les tests a partir de la graine !!!
* cygwin
- xlurette
installer lablgtk
http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist
-lucky
//PAVE/jahier/cygwin/lib/libcudd_caml.a(cudd_caml.o)(.text+0x1c0e):cudd_caml.c: undefined reference to `_gc_full_major'
- gen_stubs
File /tmp/lurette1/modele_vehicule.h could not be opened.
- sim2chro
* le nom du repertoire share est particulierement mal choisi...
......@@ -119,10 +154,6 @@ INCONV
* tuer la fenetre de parametres plus proprement.
* rajouter une option --verbose <int> pour avoir plusieurs niveau de verbosité.
Ameliorer aussi les messages correspondant
* Faire une experience ou je n'utilise plus du tout les bdds mais je
passe par une forme normale pour les booleans pour voir
......@@ -131,28 +162,13 @@ donne une repartition 25/75, et depend de l'ordre dans lequel
apparaissent les monomes. Ca fout les boules...
* autoriser plusieurs automates dans le meme fichier
* Finir lucky2lus
* rajouter une option --reactive dans lucky où il rend ses valeurs precedentes
si aucune formule n'est satisfiable (ainsi que --reactive-no-warning)
* plot a besion de gnu-awk ... Je devrais ecrire moi-meme en caml
le programme qui genere le bon format pour gnuplot...
En plus, Pour les gros fichier, ca rame à donf !
* Finir le compilo lutin de Yvan
* Les alias doivent ils etre dans le .rif au meme titre
que les autres variables locales -> ajouter une option !
* Ajouter la possibilité de pouvoir rejouer un séquence et de la continuer
(? redondant avec la graine ?)
* inclure la libc en statique (comme pascal)
ou mettre tous les .so dans un repertoire (comme matlab) ???
......
Cuddaux 0.9:
============
First release.
#=======================================
# Configuration Section
#=======================================
#---------------------------------------
# Directories
#---------------------------------------
SRCDIR = $(shell pwd)
#
#
#
# XXX autoconf
CUDD_INSTALL = $(HOME)/$(HOSTTYPE)
ifndef BIN_INSTALL_DIR
BIN_INSTALL_DIR := $(HOME)/$(HOSTTYPE)/bin
endif
ifndef INC_INSTALL_DIR
INC_INSTALL_DIR := $(HOME)/$(HOSTTYPE)/include
endif
ifndef LIB_INSTALL_DIR
LIB_INSTALL_DIR := $(HOME)/$(HOSTTYPE)/lib
endif
#---------------------------------------
# C part
#---------------------------------------
CC = gcc
ICFLAGS = \
-I$(CUDD_INSTALL)/include \
-Winline -Wimplicit-function-declaration \
-Wall
#
# XCFLAGS should be the same than the one with which CUDD is compiled
#
# i386-linux
# XCFLAGS = -DHAVE_IEEE_754 -DBSD # -mcpu=pentiumpro -malign-double
#XCFLAGS = -mcpu=i386 -DHAVE_IEEE_754 -DBSD
# sparc-sun
# XCFLAGS = -mcpu=ultrasparc -DHAVE_IEEE_754 -DUNIX100
# Windows95/98/NT with Cygwin tools
XCFLAGS = -mcpu=i386 -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
#=======================================
# End of Configuration Section
#=======================================
#---------------------------------------
# Files
#---------------------------------------
CCMODULES = \
cuddauxAddIte cuddauxBridge cuddauxCompose \
cuddauxGenCof cuddauxMisc cuddauxTDGenCof
CCSRC = cuddaux.h cuddauxInt.h $(CCMODULES:%=%.c)
CCLIB_TOINSTALL = libcuddaux.a libcuddaux_debug.a libcuddaux_prof.a
CCINC_TOINSTALL = cuddaux.h
#---------------------------------------
# Rules
#---------------------------------------
# Global rules
all: $(CCLIB_TOINSTALL)
debug: libcuddaux_debug.a
prof: libcuddaux_prof.a
install: all
cp -f $(CCLIB_TOINSTALL) $(LIB_INSTALL_DIR)
cp -f $(CCINC_TOINSTALL) $(INC_INSTALL_DIR)
distclean: mostlyclean
(cd $(LIB_INSTALL_DIR); /bin/rm -f $(CCLIB_TOINSTALL))
(cd $(INC_INSTALL_DIR); /bin/rm -f $(CCINC_TOINSTALL))
mostlyclean:
/bin/rm -f cuddaux.?? cuddaux.??? cuddaux.info
/bin/rm -fr html
clean:
/bin/rm -f *.[ao]
tar: $(CCSRC) Makefile README Changes cuddaux.texi texinfo.tex
(cd ..; tar zcvf $(HOME)/cuddaux.tgz $(^:%=cuddaux/%))
dist: $(CCSRC) Makefile README Changes cuddaux.texi texinfo.tex cuddaux.dvi cuddaux.info html
(cd ..; tar zcvf $(HOME)/cuddaux.tgz $(^:%=cuddaux/%))
# TEX rules
cuddaux.dvi: cuddaux.texi
texi2dvi $<
cuddaux.ps: cuddaux.dvi
dvips -o $@ $<
cuddaux.info: cuddaux.texi
makeinfo --no-split $<
cuddaux.html: cuddaux.texi
texi2html -split=chapter -nosec_nav -subdir=html $<
#--------------------------------------------------------------
# IMPLICIT RULES AND DEPENDENCIES
#--------------------------------------------------------------
.SUFFIXES: .c .h .o .a
#-----------------------------------
# C
#-----------------------------------
libcuddaux.a: $(CCMODULES:%=%.o)
ar rcs libcuddaux.a $^
libcuddaux_debug.a: $(CCMODULES:%=%_debug.o)
ar rcs $@ $^
libcuddaux_prof.a: $(CCMODULES:%=%_prof.o)
ar rcs $@ $^
%.o: %.c cuddaux.h
$(CC) $(CFLAGS) -c -o $@ $<
%_debug.o: %.c cuddaux.h
$(CC) $(CFLAGS_DEBUG) -c -o $@ $<
%_prof.o: %.c cuddaux.h
$(CC) $(CFLAGS_PROF) -c -o $@ $<
* Files
The basic distribution contain the following files:
README
Makefile
Changes
cuddaux.h cuddauxInt.h
cuddauxAddIte.c cuddauxBridge.c cuddauxCompose.c
cuddauxGenCof.c cuddauxMisc.c cuddauxTDGenCof.c
* What's needed :
- An ANSI C compiler (gcc is the only tested compiler)
- GNU make
- The CUDD BDDs library (http://vlsi.colorado.edu/software.html)
* This code provides additional functions to the CUDD library. Many of
them allows to replace 0-1 ADDs by BDDs, some offers equivalent
functions for ADDs than the functions implemented for BDDs, others
offers a different interface, and last new functions are implemented.
* IMPORTANT REMARK: Some functions relies on the distinghuished
"background" ADD node of CUDD. This node can be modified by
Cudd_SetBackground(). However this last function doesn't empty the
cache, which can lead to erroneous results. So be cautious, call
Cudd_SetBackground() before using such functions, or otherwise call
the function Cudd_ReduceHeap(man,CUDD_REORDER_NONE)
to clear the cache.
* To build,
Inspect Makefile and set properly variables.
make all: build the bytecode version of the interface
make install: installs the two versions of the interface
* Documentation:
Available in DVI (cuddaux.dvi), INFO (cuddaux.info), and HTML (html/*)
formats
IMPORTANT REMARK: The C compilation flags (processor, alignement)
should be the same than those with which CUDD is compiled.
/* $Id: cuddaux.h 1.2 Fri, 13 Feb 2004 16:03:37 +0100 jahier $ */
#ifndef __CUDDAUX_H__
#define __CUDDAUX_H__
#include "cudd.h"
struct list_t {
struct list_t* next;
DdNode* node
};
typedef struct list_t list_t;
/* File cuddauxAddIte.c */
/* f is a BDD, g and h are ADDs */
DdNode* Cuddaux_addIte(DdManager* dd, DdNode* f, DdNode* g, DdNode* h);
DdNode* Cuddaux_addBddAnd(DdManager* dd, DdNode* f, DdNode* g);
DdNode* Cuddaux_addIteConstant(DdManager* dd, DdNode* f, DdNode* g, DdNode* h);
DdNode* Cuddaux_addEvalConst(DdManager* dd, DdNode* f, DdNode* g);
/* File cuddauxBridge.c */
/* f is an ADD */
DdNode* Cuddaux_addTransfer(DdManager* ddS, DdManager* ddD, DdNode* f);
/* File cuddauxGenCof.c */
/* f and c are BDDs */
DdNode* Cuddaux_bddRestrict(DdManager * dd, DdNode * f, DdNode * c);
/* f is an ADD, c a BDD */
DdNode* Cuddaux_addRestrict(DdManager * dd, DdNode * f, DdNode * c);
DdNode* Cuddaux_addConstrain(DdManager * dd, DdNode * f, DdNode * c);
/* File cuddauxTDGenCof.c */
/* f and c are BDDs */
DdNode* Cuddaux_bddTDRestrict(DdManager* dd, DdNode* f, DdNode* c);
DdNode* Cuddaux_bddTDConstrain(DdManager* dd, DdNode* f, DdNode* c);
/* f is an ADD, c a BDD */
DdNode* Cuddaux_addTDRestrict(DdManager* dd, DdNode* f, DdNode* c);
DdNode* Cuddaux_addTDConstrain(DdManager* dd, DdNode* f, DdNode* c);
/* inf and sup are BDDs */