Commit b3d4d2c7 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.20 Fri, 13 Feb 2004 16:03:37 +0100 by jahier

Parent-Version:      1.19
Version-Log:

source/store.ml:
   Fix a bug found by Bertrand where it was necessary to
   apply substitutions each time a constraint is added
   Maybe it is sometimes overkill, but it is safe,
   and performance does not seem to suffer that much.

source/parse_luc.ml:
   Do not open the .luc file twice, and keep the whole file
   in a string to call the lustre expression parser.
   This was an attempt to make the debbuger work again
   with big .luc file, but it fails... The Stream lib really
   seems to suck AFA ocamldebug is concerned.

   Also shout when a wrong flag is used.

source/lurette.ml:
   when an assertion is violated, put the corresponding vector
   in the .rif file.

Project-Description: Lurette
parent caa32faa
This diff is collapsed.
......@@ -8,9 +8,9 @@
# INCDIRS = $(HOME)/$(HOST_TYPE)/lib
# LIBDIRS = $(HOME)/$(HOST_TYPE)/lib
INCDIRS = $(HOME)/$(HOST_TYPE)/lib $(SCADE_INSTALL_DIR)/lib
INCDIRS = $(HOME)/$(HOSTTYPE)/lib $(SCADE_INSTALL_DIR)/lib
LIBDIRS = $(HOME)/$(HOST_TYPE)/lib $(SCADE_INSTALL_DIR)/lib
LIBDIRS = $(HOME)/$(HOSTTYPE)/lib $(SCADE_INSTALL_DIR)/lib
OCAMLMAKEFILE = $(HOME)/lurette/OcamlMakefile
......
......@@ -71,10 +71,10 @@ Also confere the tool section at the url http://www-verimag.imag.fr/~synchron/
* Authors
Erwan Jahier
Pascal Raymond
Yvan Roux
Nicolas Halbwachs
Erwan Jahier
Pascal Raymond
Yvan Roux
Nicolas Halbwachs
-o-
......@@ -85,7 +85,9 @@ Nicolas Halbwachs
and maintenance of them:
o ocaml, camlidl by the ocaml INRIA team
o Ocamlmakefile
o Cudd, a BDD library by the University of Colorado
o polka, cuddaux and mlcuddidl by B. Jeannet, IRISA
o sim2chro by Y. Rémond - Vérimag
o autoconf, make, emacs, latex, dot, gtk, ...
o sim2chro by Y. Rémond - Verimag
o autoconf, make, emacs, latex, dot, gtk, gnuplot, plot...
****** A faire vite *******
* inclure la libc en statique
* Portage pour TNI
? Les alias doivent ils etre dans le .rif ??
* Rajouter un mot clef final_nodes { node list } dans lucky
qui verifie si le noeud courant est dans la liste quand lucky se bloque
et qui ral le cas écheant.
* Rajouter la fonction abs
* Rajouter le step mode dans lurettetop et xlurette
ie, il faut rajouter dans lurette une option --step-inside --step-edges
--step-vertices (et renommer --draw-inside par --try-inside ??)
* mettre les .rif etc dans un repertoire
+ Rajouter dans lurettetop les options qui permette d'acceder au step mode
(ie, le mode du tirage pour faire un step)
*********** BUGS
* le parseur est trop lent sur les exemples generes par nbac
pbs de maj des nouveuax fichiers dans xlurette
* les .saod, quand ils sont modifiés, ne sont pas recompilé.
* Quand j'essayz un prog scade sous linux, le msg d'erreur
est pas tiptop
* quand une formule s'avere fausse du point de vue des variables
numeriques, il ne faut pas repartir du haut du graphe, mais backtraker
......@@ -29,136 +24,66 @@ par les poids sont un peu contre-intuitives.
En plus, en backtraquant ainsi, je n'ai plus de problemes de dag2three !
et je ne suis plus obligé de ...
* en mode fair, certaines requetes aboutissent a qque chose de vraiment
pas satisfaisant : pleins de polyhedres intermediaires inutiles
sont calcules, selon l'ordre dans lequel arrivent les contraintes...
* Le remplacement dynamique de .luc est tres surement cassé (les current_nodes
* Le remplacement dynamique de .luc est tres surement cassé (les current_nodes
ne sont pas mis a jour) -> le retester
****** Documentation
* Rajouter dans lurettetop les options qui permette d'acceder au step mode
(ie, le mode du tirage pour faire un step)
* il faut rajouter dans lurette une option --step-inside --step-edges
--step-vertices (et renommer --draw-inside par --try-inside ??)
* le retour au source lutin est sans doute cassé (à voir quand le nouveau compilo
lutin sera la)
* Rajouter un mode ecexe dans lurette
* documenter les options ~default, ~alias, etc.
* Decrire l'heuristique utilisée pour choisir le vecteur qui va servir
dans la suite de l'execution pour lurette (inside).
* Signaler les approximations faites (en dimension > 1)
- volumes des polyhedres pas calculés (=> pb d'equité)
- pour le choix des entiers, on travaille dans les reels,
puis on tronque (truncate) => l'entier tiré n'est alors parfois
meme pas solution des contraintes !!! (cf brrr)
* dire dans la doc que on ne peut avoir qu'au plus une transition sortante
avec un poids infini (ca n'a pas un sens bien clair et on peut toujours
faire autrement). Dire aussi que 2 transitions ne peuvent a la fois avoir
meme origine et arrivée.
* expliquer la difference entre avoir f et f' sur 2 transitions differentes,
et avoir "f or f'" sur une seule transition, du point de vue des probas.
par ex, si f=(0<c<3) et f'=(3<c<4), on a respectivement 50% de chances d'etre
dans ]0;3[ dans le 1er contre 75% dans le 2eme.
* Il faut aussi documenter les probas de f=1.0 vs 0<f<1. Avec un pas de 10,
ca donne 10% vs 90% en mode <<efficient draw>>
Faire remarquer que dans certain cas, le fair draw peut etre plus rapide ...
mais que dans d'autre, il peut etre trs tres cher !
(2) Faire une doc utilisateur pour lurette (moins urgent depuis qu'il y
a lurettetop et xlurette...)
*********** A faire
* Mettre des iterateurs de tableaux
* reporter le contenu de la nouvelle section de d1.1-v2 dans les entetes de modules
* autoriser plusieurs automates dans le meme fichier
* rajouter une option --reactive ou lucky rend ses valeurs precedentes
si aucune formule n'est satisfiable (ainsi que --reactive-no-warning)
* Rajouter la precision comme un parametre externe de xlurette (deja dispo
dans lurettetop)
* il faudrait au moins pouvoir avoir des pre sur des var de types structurés
* mettre les fichiers de test dans un repertoire exemple et faire des liens symbo
* En fait, il faudrait ecrire les regles de typage des expressions
* Finir le lustre2lucky avec Yussef
* autoriser plusieurs automates dans le meme fichier
* Faire un lustre2lucky comme TP avec Yussef
*********** A faire aussi (moins urgent (?))
* ZZZ Changer le epsilon en 1/10^p !!!!!
* Portage Reluc
* faire un passage sur map vs rev_map
(1) Portage Reluc
* ajouter les options --product-mode {multiply | arbiter}
qui disent comment on multiplie 2 automates (cf papier)
* Rajouter un mode ecexe dans lurette
* Chercher a detecter des egalites lors de l'ajout d'une inegalité.
pour les contraintes de dimension > 1 (cf code commenté dans store.ml)
* compiler sim2chrogtk sous cygwin
* 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
* le losange ne passe pas avec polkai et passe avec polkag.
Regarder pourquoi et dire à Bertrand
* Faire un gestionnaire de sessions dans xlurette comme le propose Pascal
* zipper et dezipper les .rif a la vollée (cf zlib et camlzip)
* 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
* Rajouter les pragmas suivants :
* RIF : Rajouter les pragmas suivants :
-> #locals v* (pour pouvoir les mettre en vert)
-> #lucky_seed
-> #test_failure
* autoconf :
-> tester si gtk est la
*********** A faire ???
* xlurette :
- bouton sim2chro: mettre les locales en vert -> pragma dans sim2chro !!
* ajouter les options --product-mode {multiply | arbiter}
qui disent comment on multiplie 2 automates (cf papier)
* Trouver un controlleur non buggé pour pouvoir mettre un oracle
qui n'arrete pas le processus...
* 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
* zipper et dezipper les .rif a la vollée (cf zlib et camlzip)
* Si jamais on a à faire a des polyedres trop gros, on pourrait
peut-etre chercher a remettre en cause les choix qui ont été faits
......@@ -167,20 +92,12 @@ et je ne suis plus oblig
toutes les possibilités), mais au moins, ca donnerait une solution
dans des cas ou les polyedres peteraient...
* Réfléchir à une version d'un tireur sans bdd ou les choix seraient
effectués pendant le parcours de la formule (pas d'équité, mais bon) +
backtracking quand ca n'est pas satisfiable. Le gros pb a priori
est que les probas vont dépendre de la structure de la formule.
* Tirage équitable dans un polyèdre ; projeter dans un espace de
meme dimension que le polyhedre (quitte à faire un changement de
variable) puis tirer dans le cube enveloppant.
* dans gne.ml, rajouter partout assertion <<is_a_partition>>
......@@ -42,11 +42,11 @@ ICFLAGS = \
# XCFLAGS should be the same than the one with which CUDD is compiled
#
# i386-linux
# 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
# 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
......
/* $Id: cuddaux.h 1.1 Mon, 07 Oct 2002 17:53:39 +0200 jahier $ */
/* $Id: cuddaux.h 1.2 Fri, 13 Feb 2004 16:03:37 +0100 jahier $ */
#ifndef __CUDDAUX_H__
#define __CUDDAUX_H__
......@@ -7,7 +7,7 @@
struct list_t {
struct list_t* next;
DdNode* node;
DdNode* node
};
typedef struct list_t list_t;
......
inputs {
Heat_on %this_a_label:this is a pragma%
%this_is_another_label: "and this is another pragma"%
: bool
Heat_on : bool
}
outputs {
U:real ~min 1.0 ~max 60.0
}
locals {
Dudt %scr:15,2,16,2% %foo:bar%
: float ~min -100.0 ~max 100.0
Dudt : float ~min -100.0 ~max 100.0
}
nodes {
nodes { 0 : stable; 1 : stable
}
start_node { 0 }
transitions {
0 -> %titi: transition pragma %
1 ~cond ((U = 17.0) and (Dudt = 0.0)) ;
0 -> 1 ~cond ((U = 17.0) and (Dudt = 0.0)) ;
1 -> 1 ~cond
%toto:this is a formula pragma%
-- %titi: this is an other one %
((U = pre(U) + pre(Dudt)) and
(Dudt > (if Heat_on then 0.0 else -5.0))
......
--
-- A fault-tolerant heater controller with 3 sensors.
--
-- To guess the temperature (T),
--
-- (1) It compares the value of the 3 sensors 2 by 2 to determine
-- which ones seem are broken -- we consider then broken if they
-- differ too much.
--
-- (2) then, it performs a vote:
-- o If the tree sensors are broken, it does not heat;
-- o If the temperature is bigger than TMAX, it heats;
-- o If the temperature is smaller than TMIN, it does not heat;
-- o Otherwise, it keeps its previous state.
const FAILURE = - 999.0; -- a fake temperature given when all sensors are broken
const TMIN = 6.0;
const TMAX = 9.0;
const DELTA = 0.5;
-----------------------------------------------------------------------
-----------------------------------------------------------------------
node heater_control(T, T1, T2, T3 : real) returns (Heat_on:bool);
-- T is supposed to be the real temperature and is not
-- used in the controller; we add it here in oder to test the
-- controller to be able to write a sensible oracle.
var
V12, V13, V23 : bool;
Tguess : real;
let
V12 = abs(T1-T2) < DELTA; -- Are T1 and T2 valid?
V13 = abs(T1-T3) < DELTA; -- Are T1 and T3 valid?
V23 = abs(T2-T3) < DELTA; -- Are T2 and T3 valid?
Tguess =
if noneoftree(V12, V13, V23) then FAILURE else
if oneoftree(V12, V13, V23) then Median(T1, T2, T3) else
if alloftree(V12, V13, V23) then Median(T1, T2, T3) else
-- 2 among V1, V2, V3 are false
if V12 then Average(T1, T2) else
if V13 then Average(T1, T3) else
-- V23 is necessarily true, hence T1 is wrong
Average(T2, T3) ;
Heat_on = true ->
if Tguess = FAILURE then false else
if Tguess < TMIN then true else
if Tguess > TMAX then false else
pre Heat_on;
tel
-----------------------------------------------------------------------
-----------------------------------------------------------------------
node not_a_sauna(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool);
let
ok = true -> pre T < TMAX + 1.0 ;
tel
-----------------------------------------------------------------------
-----------------------------------------------------------------------
-- returns the absolute value of 2 reals
node abs (v : real) returns (a : real) ;
let
a = if v >= 0.0 then v else -v ;
tel
-- returns the average values of 2 reals
node Average(a, b: real) returns (z : real);
let
z = (a+b)/2.0 ;
tel
-- returns the median values of 3 reals
node Median(a, b, c : real) returns (z : real);
let
z = a + b + c - min2 (a, min2(b,c)) - max2 (a, max2(b,c)) ;
tel
-- returns the maximum values of 2 reals
node max2 (one, two : real) returns (m : real) ;
let
m = if one > two then one else two ;
tel
-- returns the minimum values of 2 reals
node min2 (one, two : real) returns (m : real) ;
let
m = if one < two then one else two ;
tel
node noneoftree (f1, f2, f3 : bool) returns (r : bool)
let
r = not f1 and not f2 and not f3 ;
tel
node alloftree (f1, f2, f3 : bool) returns (r : bool)
let
r = f1 and f2 and f3 ;
tel
node oneoftree (f1, f2, f3 : bool) returns (r : bool)
let
r = f1 and not f2 and not f3 or
f2 and not f1 and not f3 or
f3 and not f1 and not f2 ;
tel
-- Automatically generated from /tmp/lurette1/heater_control_env.h by gen_fake_lucky.
inputs {
Heat_on : bool}
outputs {
T : real;
T1 : real;
T2 : real;
T3 : real}
nodes { 0 : stable }
start_node { 0 }
transitions {
0 -> 0 ~ cond true and (0.0 < T) and (T < 1.0)
and (0.0 < T1) and (T1 < 1.0)
and (0.0 < T2) and (T2 < 1.0)
and (0.0 < T3) and (T3 < 1.0)
;
}
-- Simulate perfect sensors that never get worn
inputs {
Heat_on : bool
}
outputs {
T : float ~min 0.0 ~max 50.0;
T1 : real;
T2 : real;
T3 : real
}
locals {
eps1 : real ~min -0.1 ~max 0.1;
eps2 : real ~min -0.1 ~max 0.1;
eps3 : real ~min -0.1 ~max 0.1;
}
nodes { 0 : stable }
start_node { 0 }
transitions {
0 -> 1 ~cond T = 7.0
and T1 = T + eps1
and T2 = T + eps2
and T3 = T + eps3
;
1 -> 1 ~ cond T = pre T + (if Heat_on then 0.2 else -0.2)
and T1 = T + eps1
and T2 = T + eps2
and T3 = T + eps3
;
}
--
inputs { Heat_on : bool }
outputs {
T : float ~min 0.0 ~max 50.0;
T1 : real; T2 : real; T3 : real
}
locals {
eps : float ~min 0.0 ~max 0.2;
eps1 : float ~min -0.1 ~max 0.1;
eps2 : float ~min -0.1 ~max 0.1;
eps3 : float ~min -0.1 ~max 0.1;
cpt : int ;
invariant : bool ~alias (cpt = pre cpt + 1)
and ( T = pre T + (if Heat_on then eps else -eps));
new_T1 : bool ~alias T1 = T + eps1 ;
new_T2 : bool ~alias T2 = T + eps2 ;
new_T3 : bool ~alias T3 = T + eps3
}
nodes {
s1, s2, s3 : stable ;
s4 : final ;
t0, t1, t2, t3, t4 : transient ;
}
start_node { t0 }
transitions {
-- initialisation
t0 -> s1 ~cond T = 7.0 and cpt = 0 and T1 = T and T2 = T and T3 = T;
-- 3 sensors are working properly
t1 -> s1 ~cond invariant and new_T1 and new_T2 and new_T3 ;
s1 -> t1 ~weight 1000 ;
s1 -> t2 ~weight pre cpt;
-- One sensor is broken
t2 -> s2 ~cond invariant and new_T1 and new_T2 and T3 = pre T3 ;
s2 -> t2 ~weight 1000 ;
s2 -> t3 ~weight pre cpt;
-- Two sensors are broken
t3 -> s3 ~cond invariant and new_T1 and T2 = pre T2 and T3 = pre T3;
s3 -> t3 ~weight 1000 ;
s3 -> t4 ~weight pre cpt;
-- Tree sensors are broken
t4 -> s4 ~cond invariant and T1 = pre T1 and T2 = pre T2 and T3 = pre T3;
s4 -> t0; -- start again from the beginning
}
......@@ -23,10 +23,10 @@ xlurette_exe: dummy
| sed -e 's/\"pixmaps\//((Unix.getenv \"PIXMAP_DIR\") \^ \"/' \
| 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
ocamlc $(THREAD) \
ocamlc.opt -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlc.opt -c -I +lablgtk -labels -c xlurette_glade_callbacks.ml
ocamlc.opt -c -pp "camlp4o" -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
ocamlc.opt $(THREAD) \
-I +lablgtk -I +str -o xlurette_exe$(EXE) str.cma unix.cma lablgtk.cma gtkInit.cmo \
xlurette_glade_callbacks.cmo xlurette_glade_interface.cmo xlurette_glade_main.cmo
......@@ -37,12 +37,25 @@ opt: dummy
| sed -e 's/\"pixmaps\//((Unix.getenv \"PIXMAP_DIR\") \^ \"/' \
| sed -e 's/.xpm\"/.xpm\")/' \
> xlurette_glade_interface.ml
ocamlopt -verbose -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlopt -verbose -c -I +lablgtk -labels -c xlurette_glade_callbacks.ml
ocamlopt -verbose -c -pp "camlp4o" -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
ocamlopt -verbose -I +lablgtk -I +str -labels -o xlurette_exe$(EXE) str.cmxa unix.cmxa lablgtk.cmxa gtkInit.cmx \
ocamlopt.opt -verbose -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlopt.opt -verbose -c -I +lablgtk -labels -c xlurette_glade_callbacks.ml
ocamlopt.opt -verbose -c -pp "camlp4o" -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
ocamlopt.opt -verbose -I +lablgtk -I +str -labels -o xlurette_exe$(EXE) str.cmxa unix.cmxa lablgtk.cmxa gtkInit.cmx \
xlurette_glade_callbacks.cmx xlurette_glade_interface.cmx xlurette_glade_main.cmx
opt_static: dummy
mlglade xlurette.glade
mv xlurette_glade_interface.ml xlurette_glade_interface.ml0
cat xlurette_glade_interface.ml0 \
| sed -e 's/\"pixmaps\//((Unix.getenv \"PIXMAP_DIR\") \^ \"/' \
| sed -e 's/.xpm\"/.xpm\")/' \
> xlurette_glade_interface.ml
ocamlopt.opt -verbose -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlopt.opt -verbose -c -I +lablgtk -labels -c xlurette_glade_callbacks.ml
ocamlopt.opt -verbose -c -pp "camlp4o" -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
ocamlopt.opt -verbose -I +lablgtk -I +str -labels -o xlurette_exe$(EXE) str.cmxa unix.cmxa lablgtk.cmxa gtkInit.cmx \
-cclib -ldl -cclib -lm -cclib -lc -ccopt -static xlurette_glade_callbacks.cmx xlurette_glade_interface.cmx xlurette_glade_main.cmx
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -73,10 +73,10 @@ ICFLAGS = \
# XCFLAGS should be the same than the flags with which CUDD has been compiled
# i386-linux
# XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
# sparc-sun
XCFLAGS = -mcpu=ultrasparc -DHAVE_IEEE_754 -DUNIX100
# 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
......
/*% $Id: cherni.c 1.3 Fri, 19 Dec 2003 15:39:58 +0100 jahier $ */
/*% $Id: cherni.c 1.4 Fri, 13 Feb 2004 16:03:37 +0100 jahier $ */
/*% Conversion from one representation to the dual one. */
......@@ -204,7 +204,7 @@ int cherni_conversion(matrix_t* con, const int start,
}
if (!redundant){ /* if not */
if (nbrows==matrix_get_maxrows(ray)){
fprintf(stderr, "Chernikova: out of table space\n"); exit(1);
failwith(stderr, "Chernikova: out of table space\n");
}
/* Compute the new ray and put it at end */
matrix_combine_rows(ray,j,i,nbrows,0);
......
......@@ -41,7 +41,7 @@ profg:
doc:
(cd documentation; make)
install: