Commit e1350c78 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.15 Mon, 05 Jan 2004 17:46:15 +0100 by jahier

Parent-Version:      1.14
Version-Log:

source/util.ml:
   Redirect third party tools error msgs in the main windows rather than in the
misc.

source/lucky.ml:
source/run_aut.ml:
   Indicate the removed paths in the verbose mode only.

source/run_aut.ml:
   Fix a bug where the execution was looping when no more formula
   were satisfiable (when all formula mode was on).

source/fair_bddd.ml:
   Raise No_numeric_solution if the polyhedron volume
   is smaller then epsilon.

source/lurettetop.ml:
   Recompile the Lustre program if necessary.

source/gen_fake_lutin.ml:
   Declare the variables in the same order as in the sut program.

source/store.ml:
source/polyhedron.ml:
   Fix a bug signaled by Claude where lurette was aborting
   when solving integer constraints. It was due to a bad
   implementation of is_point_in_poly which did not
   convert floats to ints when necessary (this bug was introduced
   rather recently when i provided my own version of
   is_point_in_poly... and of course i have non reg-test
   with integer constraints...).

Project-Description: Lurette
parent d534db9c
......@@ -3,15 +3,15 @@
(Created-By-Prcs-Version 1 3 3)
(cuddaux/cuddauxGenCof.c 12011 1034006019 c/29_cuddauxGen 1.1)
(source/show_env.mli 1160 1069150632 42_show_env.m 1.11)
(source/util.ml 22946 1071844798 35_util.ml 1.61)
(source/util.ml 23034 1073321175 35_util.ml 1.62)
(test/cygwin-scade/lib_pilot.vsp 1433 1055926783 f/47_lib_pilot. 1.1)
(source/constraint.mli 1706 1069150632 c/18_constraint 1.8)
(test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1)
(mlcuddidl/Changes 129 1071844798 d/10_Changes 1.2)
(TODO 6694 1071844798 d/22_TODO 1.33)
(TODO 8582 1073321175 d/22_TODO 1.34)
(share/gen_fake_lutin.sh.in 115 1063786164 g/30_gen_fake_l 1.1)
(mlcuddidl/rdd.mli 7174 1034006019 c/40_rdd.mli 1.1)
(source/fair_bddd.ml 20626 1069833150 g/38_fair_bddd. 1.5)
(source/fair_bddd.ml 20532 1073321175 g/38_fair_bddd. 1.6)
(source/ne.mli 2259 1069150632 c/22_ne.mli 1.9)
(share/config.guess 39153 1055926783 f/25_config.gue 1.1)
(polka/documentation/polka.texi 119837 1071844798 e/17_polka.texi 1.2)
......@@ -51,7 +51,7 @@
(test/test9.rif.exp 2322 1064411282 g/17_test9.rif. 1.2)
(source/exp.ml 5911 1071235286 g/47_exp.ml 1.2)
(cuddaux/cuddauxMisc.c 13842 1034006019 c/27_cuddauxMis 1.1)
(source/polyhedron.ml 12951 1071235286 d/25_polyhedron 1.13)
(source/polyhedron.ml 13574 1073321175 d/25_polyhedron 1.14)
(source/Makefile.gen_fake_lucky 528 1063786164 g/9_Makefile.g 1.2)
(polka/C/poly.c 53392 1071844798 e/5_poly.c 1.2)
(source/luc_exe.mli 449 1069150632 b/31_ima_exe.ml 1.3)
......@@ -91,8 +91,8 @@
(test/cygwin-scade/Command.saofd 4147 1055926783 g/6_Command.sa 1.1)
(test/cygwin-scade/lib_pilot.err 119 1055926783 f/49_lib_pilot. 1.1)
(test/losange.luc 410 1046768487 d/27_losange.lu 1.2)
(test/gyro.rif.exp 10964 1069150632 e/36_gyro.rif.e 1.7)
(test/time-ecrins.exp 9333 1071844798 d/21_time-ecrin 1.35)
(test/gyro.rif.exp 10955 1073321175 e/36_gyro.rif.e 1.8)
(test/time-ecrins.exp 9332 1073321175 d/21_time-ecrin 1.36)
(source/value.ml 2534 1071235286 c/23_value.ml 1.7)
(source/gne.ml 3467 1063029729 b/37_gne.ml 1.6)
(test/cygwin-scade/Pilot.vsp 2075 1055926783 f/40_Pilot.vsp 1.1)
......@@ -142,7 +142,7 @@
(source/sim2chro.mli 1549 1069833150 b/23_sim2chro.m 1.10)
(share/lucky_init.csh.in 150 1063786164 e/23_lucky_init 1.8)
(source/lustreExp.ml 21259 1071235286 g/45_lustreExp. 1.2)
(source/gen_fake_lucky.ml 4626 1070981068 g/8_gen_fake_l 1.3)
(source/gen_fake_lucky.ml 4648 1073321175 g/8_gen_fake_l 1.4)
(polka/C/vector.h 2367 1071844798 d/47_vector.h 1.2)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(share/pixmaps/stock_exec.xpm 3788 1055926783 f/10_stock_exec 1.1)
......@@ -153,7 +153,7 @@
(share/pixmaps/save.xpm 867 1055926783 f/12_save.xpm 1.1)
(source/solver.mli 1793 1071844798 38_solver.mli 1.23)
(test/passerelle.luc 963 1063786164 b/17_passerelle 1.12)
(source/store.ml 35209 1071235286 b/27_rnumsolver 1.33)
(source/store.ml 34781 1073321175 b/27_rnumsolver 1.34)
(mlcuddidl/mtbdd.mli 4395 1034006019 c/43_mtbdd.mli 1.1)
(test/sparc-scade/exo1.vsp 2089 1055487917 e/49_exo1.vsp 1.1)
(polka/C/satmat.h 1254 1047029868 d/48_satmat.h 1.1)
......@@ -165,7 +165,7 @@
(mlcuddidl/session.ml 603 1034006019 c/37_session.ml 1.1)
(demo-xlurette/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1)
(share/Makefile.lurette.in 4495 1071844798 b/38_Makefile.l 1.29)
(source/lucky.ml 8937 1071844798 16_env.ml 1.38)
(source/lucky.ml 8968 1073321175 16_env.ml 1.39)
(source/graph.mli 2370 1071844798 13_graph.mli 1.13)
(source/store.mli 3823 1071844798 b/26_rnumsolver 1.25)
(test/time-ossau.res 9336 1070981068 b/49_time.res 1.58)
......@@ -185,22 +185,22 @@
(source/print.ml 5904 1069150632 47_print.ml 1.25)
(test/heater_int.rif.exp 824 1065787303 b/28_heater_int 1.16)
(test/sparc-scade/scade.rif.exp 1164 1065787303 f/0_scade.rif. 1.4)
(source/parse_poc.ml 4443 1070981068 d/15_parse_poc. 1.5)
(source/parse_poc.ml 4430 1073321175 d/15_parse_poc. 1.6)
(test/cygwin-scade/det_center.saofd 4993 1055926783 g/0_det_center 1.1)
(share/pixmaps/stock_save.xpm 3420 1055926783 f/9_stock_save 1.1)
(polka/C/bit.h 1424 1071844798 e/2_bit.h 1.2)
(source/parse_c_scade.mli 651 1070981068 e/42_parse_c_sc 1.2)
(demo-xlurette/chaudiere/chaudiere.luc 681 1064329011 c/11_chaudiere. 1.8)
(test/giro/allocator.lus 1087 1031732392 c/5_allocator. 1.1)
(source/run_aut.ml 22249 1071844798 b/47_automata.m 1.20)
(source/run_aut.ml 22599 1073321175 b/47_automata.m 1.21)
(cuddaux/README 1427 1034006019 c/34_README 1.1)
(mlcuddidl/bdd.ml 11038 1071844798 d/6_bdd.ml 1.2)
(source/lurettetop.ml 47197 1070981068 c/1_lurettetop 1.44)
(source/lurettetop.ml 47255 1073321175 c/1_lurettetop 1.45)
(source/constraint.ml 3180 1069150632 c/19_constraint 1.10)
(test/structured_type.luc 2224 1063786164 g/32_structured 1.1)
(source/formula_to_bdd.ml 17748 1071844798 g/34_formula_to 1.5)
(test/cygwin-scade/counter.saofd 587 1055926783 g/2_counter.sa 1.1)
(test/test7.rif.exp 269 1063786164 g/12_test7.rif. 1.1)
(test/test7.rif.exp 328 1073321175 g/12_test7.rif. 1.2)
(polka/caml/Makefile.depend 767 1071844798 d/32_Makefile.d 1.5)
(source/bddd.ml 18277 1070981068 g/36_bddd.ml 1.7)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
......@@ -237,7 +237,7 @@
(share/configure.in 8623 1071844798 d/11_configure. 1.15)
(test/tram.luc 1325 1063786164 b/15_tram.env 1.12)
(demo-xlurette/chaudiere/buggy_chaudiere_ctrl.lus 219 1031732392 c/10_buggy_chau 1.1)
(source/run_aut.mli 4465 1071844798 b/46_automata.m 1.10)
(source/run_aut.mli 4481 1073321175 b/46_automata.m 1.11)
(polka/C/matrix.h 3846 1071844798 d/51_matrix.h 1.2)
(cuddaux/cuddaux.h 2381 1034006019 c/33_cuddaux.h 1.1)
(share/lurettetop.bat.in 672 1063786164 g/26_lurettetop 1.1)
......@@ -262,7 +262,7 @@
(source/Makefile.gen_stubs 741 1063786164 b/42_Makefile.g 1.8)
(test/temp_float.luc 680 1063786164 b/51_temp_float 1.10)
(polka/C/polka.c 5608 1071844798 e/6_polka.c 1.2)
(source/polyhedron.mli 1493 1071235286 d/26_polyhedron 1.7)
(source/polyhedron.mli 1749 1073321175 d/26_polyhedron 1.8)
(test/test_losange.lus 88 1055926783 f/27_test_losan 1.1)
(mlcuddidl/bdd.mli 8638 1071844798 d/5_bdd.mli 1.2)
(test/cygwin-scade/compute_path.saofd 1662 1055926783 g/5_compute_pa 1.1)
......@@ -270,12 +270,12 @@
(polka/C/polka.h 1791 1071844798 d/50_polka.h 1.2)
(share/pixmaps/ediff-quit.xpm 494 1055926783 f/20_ediff-quit 1.1)
(test/cygwin-scade/Pilot.saofd 3645 1055926783 f/42_Pilot.saof 1.1)
(test/time-moucherotte.exp 6278 1071844798 e/37_time-mouch 1.14)
(test/time-moucherotte.exp 6283 1073321175 e/37_time-mouch 1.15)
(source/command_line_luc_exe.ml 3804 1069833150 b/33_command_li 1.21)
(source/lurette_exe.c 220 1050421093 e/27_lurette_ex 1.2)
(share/pixmaps/close.xpm 803 1055926783 f/21_close.xpm 1.1)
(test/time-CHAILLOL.res 8235 1063029729 g/11_time-CHAIL 1.1)
(test/time-ecrins.res 9332 1071844798 d/20_time-ecrin 1.36)
(test/time-ecrins.res 9346 1073321175 d/20_time-ecrin 1.37)
(source/value.mli 1181 1071235286 c/24_value.mli 1.6)
(polka/Makefile.config 1803 1071844798 e/20_Makefile.c 1.6)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
......@@ -292,7 +292,7 @@
(source/luc_exe.ml 14018 1071844798 b/32_ima_exe.ml 1.42)
(source/gne.mli 1853 1063029729 b/36_gne.mli 1.6)
(test/cygwin-scade/Direction_D1.saofd 1298 1055926783 f/50_Direction_ 1.1)
(source/lurette.ml 18801 1071844798 12_lurette.ml 1.82)
(source/lurette.ml 18790 1073321175 12_lurette.ml 1.83)
(polka/C/Makefile.depend 1081 1047029868 d/46_Makefile.d 1.1)
(share/lucky.bat.in 584 1063786164 g/28_lucky.bat. 1.1)
(share/lucky.sh.in 106 1063786164 g/27_lucky.sh.i 1.1)
......@@ -300,7 +300,7 @@
(share/pixmaps/step.xpm 864 1055926783 f/11_step.xpm 1.1)
(cuddaux/cuddauxCompose.c 13638 1034006019 c/30_cuddauxCom 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/gen_fake_lutin.ml 4709 1055487917 d/16_gen_fake_l 1.5)
(source/gen_fake_lutin.ml 4731 1073321175 d/16_gen_fake_l 1.6)
(test/heater_float.lus 177 1034351455 b/44_heater_flo 1.2)
(share/set_env_var.in 949 1063786164 g/23_set_env_va 1.1)
(source/formula_to_bdd.mli 1270 1071235286 g/35_formula_to 1.6)
......
****** A faire vite *******
* Les structures et les tableaux pour scade/lurette
* faire un passage pour verifier que je ne cree pas de hash tbl que
n'utilise plus apres, auquel cas
-> soit je nettoie
-> soit j'utilise des map.
* Portage pour TNI
* essayer les versions precedentes de scade sous sparcs avec les programmes
de HS
* Ajouter un test de non reg avec des constraintes entieres.
Prendre par ex l'exemple de claude.
*********** BUGS
* no comment ...
-----------------------------------------------------------------------------
cervin:bug[17:31]% ../source/lucky_exe poly.luc poly.luc
*** The variable xx has 2 different min definition, which is forbidden.
-----------------------------------------------------------------------------
* On Wed, 24 Dec 2003, Claude Helmstetter wrote:
-----------------------------------------------------------------------------
> Sous Xlurette,
>
> Quand on est sur une machine ou il n'y a pas gnuplot, on obtient bien un
> message d'erreur clair par contre xlurette ne veut plus lancer d'autres
> actions apres.
-----------------------------------------------------------------------------
* On Wed, 2 Jan 2004, Claude Helmstetter wrote:
-----------------------------------------------------------------------------
le SUT voit double
Avec l'environement par defaut, tout est normal.
Les fichiers sont dans :
/home/helmstet/exemple/tramway/vbug
sut : tramway.lus controleur
env : tramway.luc passager.luc porte.luc passerelle.luc
oracle : tramway.lus spec
--Pollux Version 2.1
No controleur.c or no controleur.h exist(s), so I try to compile
/home/helmstet/exemple/tramway/vbug/tramway.lus with node controleur
with the lus2ec and ec2c...
No spec.c or no spec.h exist(s), so I try to compile
/home/helmstet/exemple/tramway/vbug/tramway.lus with node spec with the
lus2ec and ec2c...
*** An assertion of the oracle has been violated at step 2 with the
following values:
* sut inputs:
attention_depart = f
attention_depart = t
demande_pass = f
demande_porte = t
en_station = f
en_station = f
pass_sortie = t
pass_sortie = f
porte_ouverte = f
porte_ouverte = f
* sut outputs:
porte_pass_oo = f
fermer_porte = f
sortir_pass = f
ouvrir_porte = f
rentrer_pass = f
* pre:
*** Lurette stops because the oracle has been violated at step 2.
The execution lasted 0.01 second.
********************************************************************
--------------------------------------------------------------------------
* gen_fake_* : les variables sont declarées dans l'ordre inverse
de celui su sut...
* xlurette: le .lus n'est pas recompilé si on le change.
* xlurette : rediriger les erreurs de compil dans la fenetre principale.
d'une maniere generale, refaire un passage sur le comportement
de l'outil quand un maillon de la chaine foire.
* quand une formule s'avere fausse du point de vue des variables
......@@ -26,7 +90,7 @@ numeriques, il ne faut pas repartir du haut du graphe, mais backtraker
depuis la branche qui s'avere fausse. Sinon, les probabilités induites
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
et je ne suis plus obligé de ...
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 1 14)
(Parent-Version lurette 1 13)
(Project-Version lurette 1 15)
(Parent-Version lurette 1 14)
(Version-Log "
gen_stubs_scade.ml:
fix a bug which was causing a bus error: to fix it, i simply delete
a couple a extras &...
source/util.ml:
Redirect third party tools error msgs in the main windows rather than in the misc.
source/lucky.ml:
source/run_aut.ml:
Indicate the removed paths in the verbose mode only.
source/run_aut.ml:
Fix a bug where the execution was looping when no more formula
were satisfiable (when all formula mode was on).
source/fair_bddd.ml:
Raise No_numeric_solution if the polyhedron volume
is smaller then epsilon.
source/lurettetop.ml:
Recompile the Lustre program if necessary.
source/gen_fake_lutin.ml:
Declare the variables in the same order as in the sut program.
source/store.ml:
source/polyhedron.ml:
Fix a bug signaled by Claude where lurette was aborting
when solving integer constraints. It was due to a bad
implementation of is_point_in_poly which did not
convert floats to ints when necessary (this bug was introduced
rather recently when i provided my own version of
is_point_in_poly... and of course i have non reg-test
with integer constraints...).
")
(New-Version-Log ""
)
(Checkin-Time "Fri, 19 Dec 2003 15:39:58 +0100")
(Checkin-Time "Mon, 05 Jan 2004 17:46:15 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -30,7 +57,7 @@ gen_stubs_scade.ml:
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.16 644))
(source/lurette.ml (lurette/12_lurette.ml 1.82 644))
(source/lurette.ml (lurette/12_lurette.ml 1.83 644))
(source/command_line.ml (lurette/b/20_command_li 1.17 644))
(source/command_line.mli (lurette/b/21_command_li 1.14 644))
......@@ -40,14 +67,14 @@ gen_stubs_scade.ml:
(source/graph.ml (lurette/14_graph.ml 1.11 644))
(source/lucky.mli (lurette/15_env.mli 1.24 644))
(source/lucky.ml (lurette/16_env.ml 1.38 644))
(source/lucky.ml (lurette/16_env.ml 1.39 644))
(source/util.ml (lurette/35_util.ml 1.61 644))
(source/util.ml (lurette/35_util.ml 1.62 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.5 644))
(source/formula_to_bdd.mli (lurette/g/35_formula_to 1.6 644))
(source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.5 644))
(source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.6 644))
(source/fair_bddd.mli (lurette/g/39_fair_bddd. 1.5 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.7 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.9 644))
......@@ -55,11 +82,11 @@ gen_stubs_scade.ml:
(source/solver.mli (lurette/38_solver.mli 1.23 644))
(source/solver.ml (lurette/39_solver.ml 1.60 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.13 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.7 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.14 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.8 644))
(source/store.mli (lurette/b/26_rnumsolver 1.25 644))
(source/store.ml (lurette/b/27_rnumsolver 1.33 644))
(source/store.ml (lurette/b/27_rnumsolver 1.34 644))
(source/parse_luc.mli (lurette/40_parse_env. 1.19 644))
(source/parse_luc.ml (lurette/41_parse_env. 1.51 644))
......@@ -73,8 +100,8 @@ gen_stubs_scade.ml:
(source/env_state.mli (lurette/50_env_state. 1.39 644))
(source/env_state.ml (lurette/51_env_state. 1.53 644))
(source/run_aut.mli (lurette/b/46_automata.m 1.10 644))
(source/run_aut.ml (lurette/b/47_automata.m 1.20 644))
(source/run_aut.mli (lurette/b/46_automata.m 1.11 644))
(source/run_aut.ml (lurette/b/47_automata.m 1.21 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.10 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.23 644))
......@@ -82,7 +109,7 @@ gen_stubs_scade.ml:
(source/gne.mli (lurette/b/36_gne.mli 1.6 644))
(source/gne.ml (lurette/b/37_gne.ml 1.6 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.44 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.45 644))
(source/draw.mli (lurette/f/1_draw.mli 1.2 644))
(source/draw.ml (lurette/f/2_draw.ml 1.3 644))
......@@ -112,9 +139,9 @@ gen_stubs_scade.ml:
(source/prevar.ml (lurette/d/18_prevar.ml 1.5 644))
(source/prevar.mli (lurette/d/19_prevar.mli 1.5 644))
(source/parse_poc.ml (lurette/d/15_parse_poc. 1.5 644))
(source/parse_poc.ml (lurette/d/15_parse_poc. 1.6 644))
(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/gen_fake_lutin.ml (lurette/d/16_gen_fake_l 1.6 644))
(source/show_luc.ml (lurette/e/25_show_luc.m 1.7 644))
(source/ocaml2c.idl (lurette/e/26_ocaml2c.id 1.2 644))
......@@ -172,7 +199,7 @@ gen_stubs_scade.ml:
(ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644))
(INSTALL (lurette/f/26_INSTALL 1.2 744))
(TAGS (lurette/21_TAGS 1.6 644))
(TODO (lurette/d/22_TODO 1.33 644))
(TODO (lurette/d/22_TODO 1.34 644))
(share/lucky_init.csh.in (lurette/e/23_lucky_init 1.8 644))
(share/lucky_init.sh.in (lurette/e/24_lucky_init 1.12 644))
......@@ -181,9 +208,9 @@ gen_stubs_scade.ml:
(test/time-ossau.exp (lurette/b/48_time.exp 1.55 644))
(test/time-ossau.res (lurette/b/49_time.res 1.58 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.36 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.35 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.14 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.37 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.36 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.15 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.15 644))
;; Various files used for testing purposes
......@@ -206,7 +233,7 @@ gen_stubs_scade.ml:
(test/test_losange.lus (lurette/f/27_test_losan 1.1 644))
(test/losange-3d2.luc (lurette/e/32_losange-3d 1.5 644))
(test/onlyroll.lus (../demo-xlurette/Gyro/onlyroll.lus) :symlink)
(test/gyro.rif.exp (lurette/e/36_gyro.rif.e 1.7 644))
(test/gyro.rif.exp (lurette/e/36_gyro.rif.e 1.8 644))
(test/giro.luc (../demo-xlurette/Gyro/giro.luc) :symlink)
(test/allocator.lus (../demo-xlurette/Gyro/allocator.lus) :symlink)
......@@ -272,7 +299,7 @@ gen_stubs_scade.ml:
(test/losange-3d.luc (lurette/d/28_losange-3d 1.4 644))
(test/losange-3d.rif.exp (lurette/e/31_losange-3d 1.5 644))
(test/test7.rif.exp (lurette/g/12_test7.rif. 1.1 644))
(test/test7.rif.exp (lurette/g/12_test7.rif. 1.2 644))
(test/infinite_weight.luc (lurette/g/13_infinite_w 1.1 644))
(test/dynamic_weight.luc (lurette/g/14_dynamic_we 1.1 644))
(test/window.luc (lurette/g/15_window.luc 1.1 644))
......@@ -385,7 +412,7 @@ gen_stubs_scade.ml:
;; Files added by populate at Tue, 26 Aug 2003 15:45:55 +0200,
;; to version 0.143(w), by jahier:
(source/gen_fake_lucky.ml (lurette/g/8_gen_fake_l 1.3 644))
(source/gen_fake_lucky.ml (lurette/g/8_gen_fake_l 1.4 644))
;; Files added by populate at Tue, 26 Aug 2003 15:46:03 +0200,
;; to version 0.143(w), by jahier:
......
......@@ -88,14 +88,8 @@ let (sol_number : Bdd.t -> sol_nb * sol_nb) =
let (add_snt_entry : Bdd.t -> sol_nb * sol_nb -> unit) =
fun bdd (n,m) ->
(*
Ougth to be called iff No_numeric_solution is raised during the draw,
which means it should never occur in the fair mode.
*)
Bdd.print string_of_int Format.std_formatter bdd;
Format.print_string (
" -> (" ^ (string_of_float n) ^ ", " ^ (string_of_float n) ^ ")\n");
assert false
assert ((n,m) = (sol_number bdd));
() (* we already know that in this mode. *)
let (init_snt : unit -> unit) =
fun _ -> ()
......@@ -678,5 +672,9 @@ and (draw_in_bdd_rec_eq: Var.env_in -> Env_state.t -> Ne.t ->
let rec (draw_in_bdd: Var.env_in -> Env_state.t -> var list -> Bdd.t ->
Bdd.t -> Var.subst list * Store.t' * Store.p) =
fun input state num_vars bdd comb ->
build_sol_nb_table num_vars bdd comb;
draw_in_bdd_rec input state ([], Store.create num_vars) bdd comb
build_sol_nb_table num_vars bdd comb;
let (g,d) = sol_number bdd in
if (abs_float(g) < !(Util.eps)) && (abs_float(d) < !(Util.eps)) then
raise No_numeric_solution
else
draw_in_bdd_rec input state ([], Store.create num_vars) bdd comb
......@@ -172,7 +172,7 @@ let rec (main : unit -> unit) =
" convention not supported sorry (should verimag or scade).\n");
exit 1
in
generate_lucky compiler (mod_name ^ "_env") vo vi dir
generate_lucky compiler (mod_name ^ "_env") (List.rev vo) (List.rev vi) dir
;;
......
......@@ -175,7 +175,7 @@ let rec (main : unit -> unit) =
" convention not supported sorry (should verimag or scade).\n");
exit 1
in
generate_lutin compiler (mod_name ^ "_env") vo vi dir
generate_lutin compiler (mod_name ^ "_env") (List.rev vo) (List.rev vi) dir
;;
......
......@@ -16,6 +16,7 @@ open Solver
open Parse_luc
open Exp
open Var
open Env_state
(****************************************************************************)
(****************************************************************************)
......@@ -54,13 +55,14 @@ let (solve_formula: Var.env_in -> Env_state.t -> int -> Thickness.numeric ->
Solver.solve_formula input state p num_thickness f bool_vars_to_gen_f
num_vnt_to_gen
with
None -> ([], Run_aut.remove_formula a path)
None -> ([], Run_aut.remove_formula a path state.d.verbose)
(* No solution for that formula ; we remove it and returns
an empty list *)
| Some(x) -> (x, a)
in
let res =
let res =
(* Adds the target nodes to the drawn substitutions *)
if
acc = []
......
......@@ -96,9 +96,9 @@ let (check_var_decl_consistency : Env_state.t -> (Var.name * string) list ->
let diff1 = diff_list_as_set in_env2 out_sut in
let diff2 = diff_list_as_set out_sut in_env2 in
(
output_string stdout
"\n*** env outputs and sut inputs should be the same.\n";
if diff1 <> [] then
output_string stdout
"\n*** env inputs and sut outputs should be the same.\n";
if diff1 <> [] then
(
print_string "\n\nAppears in the sut outputs, but not in the env inputs:";
print_vn_str stdout diff1
......@@ -311,7 +311,7 @@ let check_oracle inputs sut_outputs memory t rif state =
output_string stdout "\n* sut outputs:\n\t" ;
print_env_in o stdout
(* XXX Should I print them all? *)
(* print_failures (List.tl i, List.tl o, List.tl r) *)
(* print_failures (List.tl i, List.tl o, List.tl r) *)
)
else
print_failures (List.tl li) (List.tl lo) (List.tl lr)
......
......@@ -1341,47 +1341,50 @@ let (read_commands : string -> (unit -> string) -> bool) =
else
()
else
(*
We need to rebuild iff the generated c files are older
then flag.sut
*)
if
(*
We need to rebuild iff the generated c files are older
then flag.sut
*)
let gen_c_file =
(Filename.concat flag.user_dir (flag.sut_node ^ ".c"))
in
let stat1 = Unix.stat (Filename.concat flag.user_dir flag.sut)
and stat2 = Unix.stat gen_c_file
in
(stat1.Unix.st_mtime > stat2.Unix.st_mtime)
then
(
Sys.remove (Filename.concat flag.user_dir (flag.sut ^ ".c"));
Sys.remove (Filename.concat flag.user_dir (flag.sut ^ ".h"));
flag.to_build := true
)
(Filename.concat flag.tmp_dir (flag.sut_node ^ ".c"))
and gen_h_file =
(Filename.concat flag.tmp_dir (flag.sut_node ^ ".h"))
in
if
let stat1 = Unix.stat (Filename.concat flag.user_dir flag.sut)
and stat2 = Unix.stat gen_c_file
in
(stat1.Unix.st_mtime > stat2.Unix.st_mtime)
then
(
Sys.remove gen_c_file;
Sys.remove gen_h_file;
Sys.remove (Filename.concat flag.tmp_dir "lurette");
flag.to_build := true
);
with
_ ->
(*
Ougth to occur if c files do not exist (but then the
to_build ougth to be true already ...). Anyway, it is
safe to recompile if something bad happened.
*)
(*
Ougth to occur if c files do not exist (but then the
to_build ougth to be true already ...). Anyway, it is
safe to recompile if something bad happened here.
*)
flag.to_build := true
);
if (not !(flag.to_build) or (build lurette_path))
then
(
flag.to_build := false;
Unix.chdir flag.user_dir;
let result = run () in
if
result <> 0
then
output_string stdout "\n*** Can not run lurette, sorry.\n"
else
(output_string stderr " ... lurette ok.\n"; flush stderr)
)
(
flag.to_build := false;
Unix.chdir flag.user_dir;
let result = run () in
if
result <> 0
then
output_string stdout "\n*** Can not run lurette, sorry.\n"
else
(output_string stderr " ... lurette ok.\n"; flush stderr)
)
else
print_string "\n*** Cannot build lurette, sorry.\n";
flush stdout;
......
(*-----------------------------------------------------------------------
** Copyright (C) 2002 - Verimag.
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -72,7 +72,7 @@ let (replace_bool_representation: alias list -> alias list) =
(****************************************************************************)
let rec (get_vn_and_ct_list2: file -> vn_ct list * vn_ct list) =
let (get_vn_and_ct_list2: file -> vn_ct list * vn_ct list) =
fun file ->
let str = Util.readfile file in
let (_, ni, no, str_ptr1) = find_module_name str in
......@@ -90,7 +90,7 @@ let rec (get_vn_and_ct_list2: file -> vn_ct list * vn_ct list) =
)
(* exported *)
let rec (get_vn_and_ct_list: file -> vn_ct list * vn_ct list) =
let (get_vn_and_ct_list: file -> vn_ct list * vn_ct list) =
fun file ->
try
let _ = output_string stderr
......
......@@ -413,6 +413,32 @@ let (get_vertices : Poly.t -> (int -> string) -> point list) =
(****************************************************************************)
(****************************************************************************)
(* exported *)
let (point_to_subst_list : Var.vnt list -> (int -> string) -> point ->
Var.num_subst list) =
fun vntl rank_to_name p ->
snd
(List.fold_left
(fun (j, sl) x ->
let vn = rank_to_name j in
let vt = List.assoc vn vntl in
let s =
match vt with
| Var.FloatT -> (vn, F(x))
| Var.IntT ->
(* XXX brrrr, this is wrong !! *)
(vn, I(truncate x))
| _ ->
assert false
in
(j+1, s::sl)
)
(0, [])
p
)
(****************************************************************************)
(****************************************************************************)
......@@ -440,14 +466,10 @@ let (point_to_vector : point -> Vector.t) =
(* exported *)
let (point_is_in_poly : point -> (int -> string) -> Constraint.ineq list -> bool) =
fun p r2n cstrl ->
let s =
snd (List.fold_left
(fun (i, acc) x -> (i+1,(r2n i, F x)::acc))
(0, [])
p)
in
let (point_is_in_poly : Var.vnt list -> point -> (int -> string) ->
Constraint.ineq list -> bool) =
fun varl p r2n cstrl ->
let s = point_to_subst_list varl r2n p in
List.for_all (Constraint.eval_ineq s) cstrl