Commit ed63acb4 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.141 Thu, 26 Jun 2003 10:38:20 +0200 by jahier

Parent-Version:      0.140
Version-Log:

source/lurette.ml
source/luc_exe.ml
source/env_state.ml:
   Infer that environments share controllable vars instead of asking it to
users.

   Also allow any string to be a valid node name.

   Also fix a bug where, when several env were provided, the
Env_state.file_name
   was not returning the rigth file name. Actually it was not really a bug
since
   it could not be triggered before this change ... It just happen to work
   correctly by chance.

Project-Description: Lurette
parent 45dee352
This diff is collapsed.
#!/bin/sh
#
CURRENT_DIR=$PWD
CURRENT_DIR=`pwd`
cd share
rm -f config.cache
./configure --prefix $CURRENT_DIR
......
......@@ -67,10 +67,15 @@ Les transitions :
(2) Faire une doc utilisateur pour lurette (moins urgent depuis qu'il y
a lurettetop et xlurette...)
* rajouter une option qui dit si les formules doivent etre tronquees
dans show_luc
* mettre qques part que j'utilise ocaml, camlidl cuddaux, mlcuddidl,
polka, gmp,autoconf, make, gcc, emacs, latex, dot, gtk, sim2chro, ...
* La notion d'epaisseur est mal branlée, surtout en presence de var
numériques. Il faudrait un 3eme parametre sui dit le nombre
de tirage que l'on fait dans chaque polyedres.
-> remplacer l'epaisseur de formules par un taux de couverture
* Utiliser l'ordre des parametres plutot que leur noms
Quoique, quand on fait le produit de plusieurs automates,
......@@ -82,16 +87,6 @@ Les transitions :
* le losange ne passe pas avec polkai et passe avec polkag.
Regarder pourquoi et dire à Bertrand
* Inferer la croix, plutot que de verifier !!!
* La notion d'epaisseur est mal branlée, surtout en presence de var
numériques. Il faudrait un 3eme parametre sui dit le nombre
de tirage que l'on fait dans chaque polyedres.
-> remplacer l'epaisseur de formules par un taux de couverture
* rajouter une option qui dit si les formules doivent etre tronquees
dans show_luc
* Faire un gestionnaire de sessions comme le propose Pascal
......@@ -100,7 +95,7 @@ Les transitions :
peut-etre chercher a remettre en cause les choix qui ont été faits
lors des egalités (ie, le choix de la variable à substituer). Ce calcul
coute peut-etre un peu cher (car, comment faire autrement qu'essayer
toutes les possibilités), mais au moins, ca donnerais une solution
toutes les possibilités), mais au moins, ca donnerait une solution
dans des cas ou les polyedres peteraient...
......@@ -109,7 +104,7 @@ Les transitions :
* 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 plus realiste
-> En faire un envt plus realiste
* Rajouter les pragmas suivants :
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 140)
(Parent-Version lurette 0 139)
(Project-Version lurette 0 141)
(Parent-Version lurette 0 140)
(Version-Log "
source/lurette.ml
source/luc_exe.ml
source/env_state.ml:
Infer that environments share controllable vars instead of asking it to users.
Also allow any string to be a valid node name.
ihm/xlurette/xlurette_main.ml:
Change the current dir when the sut changes so that the current dir is the
dir of the sut.
source/lurettetop.ml:
Add a change_dir command.
Make user_dir and tmp_lurette global vars.
share/configure.in:
create .bat and sh scripts take set env vars and run tools
(xlurette and lurettetop) so that sourcing lucky_init.cs is
no longer necessary.
Also fix a bug where, when several env were provided, the Env_state.file_name
was not returning the rigth file name. Actually it was not really a bug since
it could not be triggered before this change ... It just happen to work
correctly by chance.
")
(New-Version-Log ""
)
(Checkin-Time "Mon, 23 Jun 2003 15:19:23 +0200")
(Checkin-Time "Thu, 26 Jun 2003 10:38:20 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -36,16 +30,16 @@ share/configure.in:
;; 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.32 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.33 644))
(source/command_line_luc_exe.ml (lurette/b/33_command_li 1.15 644))
(source/command_line_luc_exe.ml (lurette/b/33_command_li 1.16 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.70 644))
(source/lurette.ml (lurette/12_lurette.ml 1.71 644))
(source/command_line.ml (lurette/b/20_command_li 1.13 644))
(source/command_line.ml (lurette/b/20_command_li 1.14 644))
(source/command_line.mli (lurette/b/21_command_li 1.11 644))
;; Sources files common to lurette and luc_exe
......@@ -55,12 +49,12 @@ share/configure.in:
(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.50 644))
(source/util.ml (lurette/35_util.ml 1.51 644))
(source/solver.mli (lurette/38_solver.mli 1.14 644))
(source/solver.ml (lurette/39_solver.ml 1.48 644))
(source/solver.ml (lurette/39_solver.ml 1.49 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.5 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.6 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.1 644))
(source/store.mli (lurette/b/26_rnumsolver 1.16 644))
......@@ -69,14 +63,14 @@ share/configure.in:
(source/pnumsolver.ml (lurette/d/23_pnumsolver 1.2 644))
(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.45 644))
(source/parse_env.mli (lurette/40_parse_env. 1.15 644))
(source/parse_env.ml (lurette/41_parse_env. 1.46 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))
(source/show_env.mli (lurette/42_show_env.m 1.9 644))
(source/show_env.ml (lurette/43_show_env.m 1.17 644))
(source/formula.mli (lurette/44_formula.ml 1.23 644))
(source/formula.ml (lurette/45_formula.ml 1.29 644))
(source/formula.mli (lurette/44_formula.ml 1.24 644))
(source/formula.ml (lurette/45_formula.ml 1.30 644))
(source/print.mli (lurette/46_print.mli 1.13 644))
(source/print.ml (lurette/47_print.ml 1.23 644))
......@@ -84,11 +78,11 @@ share/configure.in:
(source/eval.mli (lurette/48_eval.mli 1.11 644))
(source/eval.ml (lurette/49_eval.ml 1.14 644))
(source/env_state.mli (lurette/50_env_state. 1.30 644))
(source/env_state.ml (lurette/51_env_state. 1.44 644))
(source/env_state.mli (lurette/50_env_state. 1.31 644))
(source/env_state.ml (lurette/51_env_state. 1.45 644))
(source/automata.mli (lurette/b/46_automata.m 1.3 644))
(source/automata.ml (lurette/b/47_automata.m 1.9 644))
(source/automata.ml (lurette/b/47_automata.m 1.10 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.7 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.18 644))
......@@ -96,7 +90,7 @@ share/configure.in:
(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.37 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.38 644))
(source/draw.mli (lurette/f/1_draw.mli 1.1 644))
(source/draw.ml (lurette/f/2_draw.ml 1.1 644))
......@@ -130,7 +124,7 @@ share/configure.in:
(source/parse_poc.mli (lurette/d/29_parse_poc. 1.2 644))
(source/gen_fake_lutin.ml (lurette/d/16_gen_fake_l 1.5 644))
(source/show_luc.ml (lurette/e/25_show_luc.m 1.3 644))
(source/show_luc.ml (lurette/e/25_show_luc.m 1.4 644))
(source/ocaml2c.idl (lurette/e/26_ocaml2c.id 1.2 644))
(source/lurette_exe.c (lurette/e/27_lurette_ex 1.2 644))
(source/call_lurette_main.c (lurette/e/28_call_luret 1.1 644))
......@@ -138,7 +132,7 @@ share/configure.in:
;; Make files
(share/lucky.el (lurette/f/7_lucky.el 1.2 644))
(share/lucky.el (lurette/f/7_lucky.el 1.3 644))
(share/pixmaps/stop.xpm (lurette/f/8_stop.xpm 1.1 644))
(share/pixmaps/stock_save.xpm (lurette/f/9_stock_save 1.1 644))
(share/pixmaps/stock_exec.xpm (lurette/f/10_stock_exec 1.1 644))
......@@ -157,13 +151,13 @@ share/configure.in:
(share/pixmaps/chrono.xpm (lurette/f/23_chrono.xpm 1.1 644))
(share/pixmaps/button-close.xpm (lurette/f/24_button-clo 1.1 644))
(share/config.guess (lurette/f/25_config.gue 1.1 755))
(share/configure.in (lurette/d/11_configure. 1.10 644))
(share/configure.in (lurette/d/11_configure. 1.11 644))
(share/Makefile.common.in (lurette/d/12_Makefile.c 1.5 644))
(Makefile.common.source (lurette/e/33_Makefile.c 1.5 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.51 644))
(share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.25 644))
(user-rules (lurette/c/14_myrules 1.38 644))
(share/Makefile.test (lurette/c/25_user-rules 1.6 644))
(share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.26 644))
(user-rules (lurette/c/14_myrules 1.39 644))
(share/Makefile.test (lurette/c/25_user-rules 1.7 644))
(Makefile (lurette/d/13_Makefile 1.4 644))
(source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.3 644))
......@@ -172,7 +166,7 @@ share/configure.in:
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.21 644))
(source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.7 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.20 644))
(source/Makefile (lurette/c/20_Makefile 1.20 644))
(source/Makefile (lurette/c/20_Makefile 1.21 644))
;; Documentation
(doc/Interface_draft (lurette/19_Interface_ 1.1 644))
......@@ -185,21 +179,21 @@ share/configure.in:
;; Misc
(README (lurette/10_README 1.10 644))
(ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644))
(INSTALL (lurette/f/26_INSTALL 1.1 744))
(INSTALL (lurette/f/26_INSTALL 1.2 744))
(TAGS (lurette/21_TAGS 1.6 644))
(TODO (lurette/d/22_TODO 1.19 644))
(TODO (lurette/d/22_TODO 1.20 644))
(share/lucky_init.csh.in (lurette/e/23_lucky_init 1.6 644))
(share/lucky_init.sh.in (lurette/e/24_lucky_init 1.8 644))
(share/gnuplot-rif (lurette/e/34_gnuplot-ri 1.2 744))
(share/plot (lurette/e/35_plot 1.3 744))
(test/time-ossau.exp (lurette/b/48_time.exp 1.45 644))
(test/time-ossau.res (lurette/b/49_time.res 1.48 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.22 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.22 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.4 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.4 644))
(test/time-ossau.exp (lurette/b/48_time.exp 1.46 644))
(test/time-ossau.res (lurette/b/49_time.res 1.49 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.23 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.23 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.5 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.5 644))
;; Various files used for testing purposes
(test/cudd_gc_problem.luc (lurette/e/29_cudd_gc_pr 1.1 644))
......@@ -227,7 +221,7 @@ share/configure.in:
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.13 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.15 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.16 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.15 644))
(test/heater_int.lus (lurette/b/43_heater_int 1.1 644))
(test/heater_float.lus (lurette/b/44_heater_flo 1.2 644))
......@@ -246,7 +240,7 @@ share/configure.in:
(test/sparc-scade/Direction_D1.saofd (lurette/e/51_Direction_ 1.1 644))
(test/sparc-scade/scade.rif.exp (lurette/f/0_scade.rif. 1.1 644))
(test/cygwin-scade/test-scade-cygwin.res (lurette/f/28_test-scade 1.1 644))
(test/test-scade-cygwin.res (lurette/f/28_test-scade 1.1 644))
(test/cygwin-scade/.lurette_rc (lurette/f/29_.lurette_r 1.1 644))
(test/cygwin-scade/.lurette_rc~ (lurette/f/30_.lurette_r 1.1 644))
(test/cygwin-scade/det_mvt_mode_env.luc (lurette/f/31_det_mvt_mo 1.1 644))
......@@ -387,6 +381,11 @@ share/configure.in:
;; Files added by populate at Tue, 17 Jun 2003 15:16:25 +0200,
;; to version 0.138(w), by jahier:
;; Files added by populate at Wed, 25 Jun 2003 18:18:57 +0200,
;; to version 0.140(w), by jahier:
(test/cygwin-scade/scade.rif.exp (lurette/g/7_scade.rif. 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
......@@ -65,7 +65,7 @@ CFLAGS_0= #-Xc -DSIM
MEMORIES=$(SCADE_INSTALL_DIR)/lib/memories.c
LIB_GC=$(SCADE_INSTALL_DIR)@LIB_GC@
LIB_GC=@LIB_GC@
LIB_OS= -lm
......
......@@ -5,36 +5,45 @@
test1:
rm -f ControleurPorte.rif0; \
$(LURETTE_PATH)/$(HOST_TYPE)/bin/lurettetop --sut ControleurPorte.lus -msn ControleurPorte -l 100 -tf 10 -td 10 \
--do-not-show-step -o ControleurPorte.rif0 --seed 1013219512 -ns2c -go \
../$(HOST_TYPE)/bin/lurettetop.sh --sut ControleurPorte.lus -msn ControleurPorte -l 100 -tf 10 -td 10 \
--do-not-show-step -o ControleurPorte.rif0 \
--seed 1013219512 -ns2c -go \
tram.luc usager.luc porte.luc passerelle.luc ;\
grep -v "lurette chronogram" ControleurPorte.rif0 > ControleurPorte.rif ;\
grep -v "lurette chronogram" ControleurPorte.rif0 | sed -e "s/^M//" > ControleurPorte.rif ;\
rm -f test1.res; diff -u ControleurPorte.rif.exp ControleurPorte.rif > test1.res
test2:
rm -f heater_int.rif0; \
$(LURETTE_PATH)/$(HOST_TYPE)/bin/lurettetop -l 30 -tf 10 -td 10 --sut heater_int -msn heater_int --seed 1013219512 \
--do-not-show-step -ns2c -go -o heater_int.rif0 -go temp_int ;\
grep -v "lurette chronogram" heater_int.rif0 > heater_int.rif ;\
../$(HOST_TYPE)/bin/lurettetop.sh -l 30 -tf 10 -td 10 --sut heater_int -msn heater_int --seed 1013219512 \
--do-not-show-step -ns2c -go -o heater_int.rif0 \
-go temp_int ;\
grep -v "lurette chronogram" heater_int.rif0 | sed -e "s/^M//" > heater_int.rif ;\
rm -f test2.res; diff -u heater_int.rif.exp heater_int.rif > test2.res
test3:
rm -f heater_float.rif0; \
$(LURETTE_PATH)/$(HOST_TYPE)/bin/lurettetop --precision 4 -go -l 30 -tf 10 -td 10 -msn heater_float --sut heater_float --seed 1013219512 \
--do-not-show-step -ns2c -o heater_float.rif0 temp_float;\
grep -v "lurette chronogram" heater_float.rif0 > heater_float.rif ;\
../$(HOST_TYPE)/bin/lurettetop.sh --precision 4 -go -l 30 -tf 10 -td 10 -msn heater_float --sut heater_float --seed 1013219512 \
--do-not-show-step -ns2c -o heater_float.rif0 \
temp_float;\
grep -v "lurette chronogram" heater_float.rif0 | sed -e "s/^M//"> heater_float.rif ;\
rm -f test3.res; diff -u heater_float.rif.exp heater_float.rif > test3.res
test4 :
$(LURETTE_PATH)/$(HOST_TYPE)/bin/lucky -seed 1014504087 -l 100 cudd_gc_problem.luc > cudd_gc_problem.rif
../$(HOST_TYPE)/bin/lucky.sh -seed 1014504087 -l 100 cudd_gc_problem.luc | sed -e "s/^M//" > cudd_gc_problem.rif
rm -f test4.res; diff -u cudd_gc_problem.rif.exp cudd_gc_problem.rif > test4.res
test5 :
$(LURETTE_PATH)/$(HOST_TYPE)/bin/lucky -seed 834966010 -l 100 losange-3d2.luc > losange-3d.rif
../$(HOST_TYPE)/bin/lucky.sh -seed 834966010 -l 100 losange-3d2.luc | sed -e "s/^M//" > losange-3d.rif
rm -f test5.res; diff -u losange-3d.rif.exp losange-3d.rif > test5.res
test6 :
rm -f gyro.rif0; \
../$(HOST_TYPE)/bin/lurettetop.sh --precision 4 -go -l 50 -tf 1 -td 1 -msn onlyroll --sut onlyroll --seed 1013219512 \
--do-not-show-step -ns2c -o gyro.rif0 giro;\
grep -v "lurette chronogram" gyro.rif0 | sed -e "s/^M//" > gyro.rif ;\
rm -f test6.res; diff -u gyro.rif.exp gyro.rif > test6.res
test: test1 test2 test3 test4 test5
ls -l *.res
test: test1 test2 test3 test4 test5 test6
ls -l *.res
......@@ -302,12 +302,6 @@ case "$HOST_TYPE" in
;;
esac
echo " "
echo " if you want to install tools anywhere else than lurette-XXX/$HOST_TYPE/{bin,lib}"
echo " you can type "
echo " cd share "
echo " ./configure --prefix <where to install bins and libs>"
echo
echo " bye!"
......@@ -20,7 +20,7 @@
(setq lucky-font-lock-keywords
'(
("\\(*.*$" . font-lock-comment-face)
;;("*$" . font-lock-comment-face)
("\\<\\(weight\\|max\\|min\\|default\\|cond\\|max\\|With\\)\\>" . font-lock-string-face)
("\\<\\(IfThenElse\\|IfThenElseNum\\|Dec\\|Return_not_sig\\|Return_sig\\|Draw_between\\|Draw_gauss\\|Set\\|Set_between\\|+\\|*\\|-\\|/\\|mod\\)\\>"
......
......@@ -105,6 +105,35 @@ liblurette_lib_dc.a:
ar r liblurette_lib_dc.a *.o ; rm *.o ;\
cp liblurette_lib_dc.a ..
liblurette_lib_pbc.a:
cd lurette_util ;rm * ;\
ar rcs liblurette_lib_pbc.a ../lurette_lib.o$(EXE) ;\
ar x $(HOME)/$(HOST_TYPE)/lib/libcudd_caml.a ;\
ar r liblurette_lib_pbc.a *.o ; rm *.o ;\
ar x $(HOME)/$(HOST_TYPE)/lib/libcuddaux.a ;\
ar r liblurette_lib_pbc.a ../lurette_lib.o *.o ; rm *.o ;\
ar x $(HOME)/$(HOST_TYPE)/lib/libcudd.a ;\
ar r liblurette_lib_pbc.a *.o ; rm *.o ;\
ar x $(HOME)/$(HOST_TYPE)/lib/libpolkag_caml.a ;\
ar r liblurette_lib_pbc.a *.o ; rm *.o ;\
ar x $(HOME)/$(HOST_TYPE)/lib/libpolkag.a ;\
ar r liblurette_lib_pbc.a *.o ; rm *.o ;\
ar x $(HOME)/$(HOST_TYPE)/lib/libcamlidl.a ;\
ar r liblurette_lib_pbc.a *.o ; rm *.o ;\
ar x $(HOME)/$(HOST_TYPE)/lib/libmtr.a ;\
ar r liblurette_lib_pbc.a *.o ; rm *.o ;\
ar x $(HOME)/$(HOST_TYPE)/lib/libst.a ;\
ar r liblurette_lib_pbc.a *.o ; rm *.o ;\
ar x $(HOME)/$(HOST_TYPE)/lib/libepd.a ;\
ar r liblurette_lib_pbc.a *.o ; rm *.o ;\
ar x $(HOME)/$(HOST_TYPE)/lib/libutil.a ;\
ar r liblurette_lib_pbc.a *.o ; rm *.o ;\
ar x $(HOME)/$(HOST_TYPE)/lib/ocaml/libstr.a ;\
ar r liblurette_lib_pbc.a *.o ; rm *.o ;\
ar x $(HOME)/$(HOST_TYPE)/lib/libcamlrun.a ;\
ar r liblurette_lib_pbc.a *.o ; rm *.o ;\
cp liblurette_lib_pbc.a ..
libnc:
make clean -f Makefile.lurette_lib
make nc -f Makefile.lurette_lib OCAMLFLAGS="-noassert -unsafe"
......@@ -125,6 +154,13 @@ libdc:
make liblurette_lib_dc.a
libpbc:
rm -f lurette_lib.o
make pbc -f Makefile.lurette_lib OCAMLFLAGS=""
rm -f liblurette_lib_pbc.a
make liblurette_lib_pbc.a
lib_gprof:liblurette_lib_gprof.a
......
This diff is collapsed.
......@@ -116,7 +116,7 @@ let usage_options =
(List.rev (group_common_options string_to_option))
let usage =
("usage: ./lurette length n p [options]* <file>.env ([x] <file>.env)* \n" ^
("usage: ./lurette length n p [options]* (<file>.luc)+ \n" ^
" where: \n\t o `length' is the number of steps that will be run " ^
"\n\t o `n' is the number of formula that are drawn at each step" ^
......@@ -131,11 +131,7 @@ let usage =
"\n\t o `options' is a list of options. The available options are: " ^
usage_options ^ "\n\n" ^
"Example: ./lurette 1000 3 4 env1.env x env2.env x env3.env env4\n\t" ^
"will run during 1000 steps; at each step, it will draw 3 formula in the \n\t" ^
"automata, and it will draw 4 times in each formula (leading to a thickness of 12). \n\t" ^
"The environment `env1', `env2', and `env3' will be run as a product, \n\t" ^
"and `env4' in parallel.\n\n ")
"Example: ./lurette 1000 3 4 env1.luc env2.luc env3.luc env4.luc\n\n ")
let cmd_line_string_to_int str errmsg =
......
......@@ -27,6 +27,7 @@ let (string_to_option: (string * cmd_line_optionT) list) = [
("-b", Boot);
("--with-seed", Seed);
("--seed", Seed);
("-seed", Seed);
("--step-number", StepNb);
......@@ -50,6 +51,7 @@ let (string_to_option: (string * cmd_line_optionT) list) = [
("-v", Verbose);
("--help", Help);
("-help", Help);
("-h", Help)
]
......@@ -93,16 +95,14 @@ let usage_options =
(List.rev (group_common_options string_to_option))
let usage =
("usage: lucky [options]* <file>.luc ([x] <file>.luc)* \n" ^
" where `<file>.luc contains an environment automata. Environments " ^
"\n\t separated by `x' will executed as if their automata where " ^
"\n\t multiplied (necessary if they have common output variables).\n " ^
("usage: lucky [options]* (<file>.luc)+ \n" ^
" where `<file>.luc contains a lucky atomaton description. Environments " ^
"\n\t that shares output variables are executed as if their automata where " ^
"\n\t multiplied.\n " ^
"\n options: \n " ^ usage_options ^ "\n\n" ^
"Example: lucky env1.luc x env2.luc x env3.luc env4\n\t" ^
"will run the environment `env1', `env2', and `env3' as a product, \n\t" ^
"and `env4' in parallel.\n\n ")
"Example: lucky env1.luc env2.luc env3.luc env4\n\n ")
let cmd_line_string_to_int str errmsg =
......
......@@ -34,7 +34,7 @@ type env_stateT = {
mutable output_var_names: vnt list;
(** Output var names and types. *)
node_to_file_name: (int, string) Hashtbl.t;
node_to_file_name: (node, string) Hashtbl.t;
(** Associates each node in the environment automata with its
origin file name (i.e., the [.env] file it comes from).
......@@ -46,7 +46,7 @@ type env_stateT = {
we need to be able to know what variables are still to be drawn.
*)
node_to_source_info : (int, Formula.source_info) Hashtbl.t;
node_to_source_info : (node, Formula.source_info) Hashtbl.t;
(** associates to some nodes information related to the source lutin
file: file name, line and col number *)
......@@ -66,12 +66,12 @@ type env_stateT = {
formula which content does npt depend on input nor pre variables.
We need to maitain those two kinds of tables because unlike the
latter, the former needs to be cleared at each step. *)
(** Counters used to manage the indexes above. *)
mutable index_cpt: int;
(** Counters used to manage the indexes above. *)
(** List of currently unused bdd var indexes *)
mutable free_index_list: int list;
(** List of currently unused bdd var indexes *)
mutable bdd_manager: Manager.t;
(** bdd engine internal state. *)
......@@ -139,7 +139,7 @@ let (env_state:env_stateT) = {
pre_var_names = [];
output_var_names = [];
node_to_file_name = Hashtbl.create 0 ;
node_to_source_info = Hashtbl.create 0 ;
node_to_source_info = Hashtbl.create 0 ;
bdd_manager = init_manager ();
graph = Graph.create () ;
......@@ -170,7 +170,9 @@ let (env_state:env_stateT) = {
(****************************************************************************)
let (var_names: string -> vnt list * vnt list * vnt list) =
fun file ->
Hashtbl.find env_state.var_names file
try
Hashtbl.find env_state.var_names file
with Not_found -> assert false
let (set_var_names : string -> vnt list * vnt list * vnt list -> unit) =
fun file vntl ->
......@@ -225,8 +227,10 @@ let (set_pre_var_names: (var_name * Value.t option) list -> unit) =
(****************************************************************************)
let (file_name: Formula.node -> string) =
fun node ->
Hashtbl.find env_state.node_to_file_name node
try
Hashtbl.find env_state.node_to_file_name node
with Not_found -> assert false
let (set_file_name: Formula.node -> string -> unit) =
fun node file ->
Hashtbl.replace env_state.node_to_file_name node file
......@@ -380,7 +384,6 @@ let (clear_bdd: unit -> unit) =
let (bdd_global : formula -> Bdd.t) =
fun f ->
Hashtbl.find env_state.bdd_tbl_global f
let (set_bdd_global : formula -> Bdd.t -> unit) =
fun f bdd ->
Hashtbl.replace env_state.bdd_tbl_global f bdd
......@@ -441,8 +444,10 @@ let (linear_constraint_to_index : Constraint.t -> bool -> int) =
let (index_to_linear_constraint : int -> Constraint.t) =
fun i ->
try Hashtbl.find env_state.index_to_global_linear_constraint i
with Not_found ->
Hashtbl.find env_state.index_to_linear_constraint i
with Not_found ->
(* try *)
Hashtbl.find env_state.index_to_linear_constraint i
(* with Not_found -> assert false *)
(* exported *)
......@@ -542,6 +547,7 @@ let _ = assert ( (add_missing_pre ["_pre3toto",None; "_pre2titi",None; "_pre2tot
content of [file]. *)
let (read_env_state_one_file : string -> node) =
fun file ->
(* XXX bien compliqué tout ca... a simplifier !!! *)
let ic = try open_in file with
_ ->
(
......@@ -553,7 +559,7 @@ let (read_env_state_one_file : string -> node) =
in
let
(* Parses the content of [file]. *)
Parse_env.Automata(init_node, list_in, list_out, list_loc,
Parse_env.Automata(init_node_str, list_in, list_out, list_loc,
list_pre, list_ce, trans_nodes_list,
adl, list_arcs) =
......@@ -582,20 +588,52 @@ let (read_env_state_one_file : string -> node) =
let list_pre_vn = add_missing_pre list_pre in
(* Sets the [graph] field of [env_state]. *)
let node_nb = (List.length (Graph.get_all_nodes (graph ()))) in
let (label_to_node : string -> node) =
fun label0 ->
(* avoid node label clashes *)
let
file1 = try Filename.chop_extension (Filename.basename file)
with _ -> file
in
let label = (file1 ^ ":" ^ label0) in
label
in
let (add_arc: Parse_env.read_arc -> unit) =
fun arc ->
match arc with
Parse_env.Arc(node_from, arc_info, node_to) ->
(add_trans
(graph ())
(node_from+node_nb)
arc_info
(node_to+node_nb));
Parse_env.Arc(node_from_str, arc_info, node_to_str) ->
let node_from = label_to_node (node_from_str) in
let node_to = label_to_node (node_to_str) in
(add_trans (graph ()) node_from arc_info node_to);
in
let all_nodes =
fold_left
(fun acc (Parse_env.Arc(nf0, _, nt0)) ->
let nt = label_to_node nt0
and nf = label_to_node nf0 in
let acc1 = if mem nf acc then acc else nf::acc in
if mem nt acc then acc1 else nt::acc1
)
[]
list_arcs
in
let init_node = label_to_node init_node_str in
if
not (mem init_node all_nodes)
then
(
print_string (
"\n*** The node " ^ init_node ^ " which is declared as being " ^
" initial does not appear in the list of transitions.\n"
);
exit 1
);
(* Set the transient_nodes field of [env_state]. *)
set_transient_nodes trans_nodes_list;
set_transient_nodes (List.map label_to_node trans_nodes_list);
(* Set the formula and expr alias tables *)
List.iter
......@@ -609,9 +647,10 @@ let (read_env_state_one_file : string -> node) =
Hashtbl.mem env_state.ce_label id
then
(
print_string ("*** The control expression " ^ id ^
" has been defined twice, which is bad." ^
" Please fix it.\n");
print_string (
"*** The control expression " ^ id ^
" has been defined twice, which is bad." ^