Commit fa2dfd3a authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.117 Mon, 18 Nov 2002 14:26:30 +0100 by jahier

Parent-Version:      0.116
Version-Log:

Various minor fixes in the documentation

+ Use a version of ocaml-3.06 that has been configured with -no-curses,
which make things sligthly slower, but that avoid the need to find
the curses lib...

source/ne.ml:
source/*.ml:
   Ne.find now returns an option value instead of raising a Not_found
   exp, which was not trap in some circumstances...

source/ne.ml:
   Also, fix a couple of bugs where the code was supposing (falsely)
   that the constant (empty string) was always in the Map.

Project-Description: Lurette
parent aef52d9c
...@@ -19,16 +19,16 @@ ...@@ -19,16 +19,16 @@
(mlcuddidl/sedscript 203 1034006019 c/38_sedscript 1.1) (mlcuddidl/sedscript 203 1034006019 c/38_sedscript 1.1)
(source/automata.mli 3396 1033738731 b/46_automata.m 1.3) (source/automata.mli 3396 1033738731 b/46_automata.m 1.3)
(test/heater_int.rif.exp 886 1034951022 b/28_heater_int 1.10) (test/heater_int.rif.exp 886 1034951022 b/28_heater_int 1.10)
(source/ne.ml 9160 1037192189 c/21_ne.ml 1.2) (source/ne.ml 9371 1037625990 c/21_ne.ml 1.3)
(source/prevar.ml 981 1037192189 d/18_prevar.ml 1.1) (source/prevar.ml 981 1037192189 d/18_prevar.ml 1.1)
(source/value.mli 1101 1033723811 c/24_value.mli 1.1) (source/value.mli 1101 1033723811 c/24_value.mli 1.1)
(user-rules.skel 973 1034006019 c/25_user-rules 1.1) (user-rules.skel 973 1034006019 c/25_user-rules 1.1)
(source/Makefile.gen_stubs 212 1036048863 b/42_Makefile.g 1.5) (source/Makefile.gen_stubs 212 1036048863 b/42_Makefile.g 1.5)
(test/temp_int.luc 685 1033723811 b/50_temp_int.e 1.3) (test/temp_int.luc 685 1033723811 b/50_temp_int.e 1.3)
(source/luc_exe.ml 12191 1036675177 b/32_ima_exe.ml 1.22) (source/luc_exe.ml 12235 1037625990 b/32_ima_exe.ml 1.23)
(source/prevar.mli 623 1037192189 d/19_prevar.mli 1.1) (source/prevar.mli 623 1037192189 d/19_prevar.mli 1.1)
(test/heater_float.rif.exp 1485 1034951022 b/30_heater_flo 1.11) (test/heater_float.rif.exp 1485 1034951022 b/30_heater_flo 1.11)
(source/graph.ml 2563 1027066799 14_graph.ml 1.7) (source/graph.ml 2339 1037625990 14_graph.ml 1.8)
(ihm/xlurette/makefile 1583 1036048863 c/16_makefile 1.6) (ihm/xlurette/makefile 1583 1036048863 c/16_makefile 1.6)
(test/usager.luc 495 1032789516 b/14_usager.env 1.9) (test/usager.luc 495 1032789516 b/14_usager.env 1.9)
(mlcuddidl/manager.ml 8017 1034006019 c/47_manager.ml 1.1) (mlcuddidl/manager.ml 8017 1034006019 c/47_manager.ml 1.1)
...@@ -46,22 +46,22 @@ ...@@ -46,22 +46,22 @@
(source/parse_env.ml 31309 1037192189 41_parse_env. 1.32) (source/parse_env.ml 31309 1037192189 41_parse_env. 1.32)
(ihm/xlurette/xlurette_glade_main.ml 23620 1036675177 c/12_xlurette_g 1.15) (ihm/xlurette/xlurette_glade_main.ml 23620 1036675177 c/12_xlurette_g 1.15)
(demo/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1) (demo/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1)
(source/solver.ml 33352 1037192189 39_solver.ml 1.35) (source/solver.ml 30051 1037625990 39_solver.ml 1.36)
(test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1) (test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1)
(source/gen_fake_lutin.ml 3449 1036048863 d/16_gen_fake_l 1.1) (source/gen_fake_lutin.ml 3449 1036048863 d/16_gen_fake_l 1.1)
(source/lurette.ml 14219 1036675177 12_lurette.ml 1.60) (source/lurette.ml 14219 1036675177 12_lurette.ml 1.60)
(source/Makefile 1377 1036585364 c/20_Makefile 1.9) (source/Makefile 1377 1036585364 c/20_Makefile 1.9)
(source/util.ml 20779 1036675177 35_util.ml 1.35) (source/util.ml 20862 1037625990 35_util.ml 1.36)
(mlcuddidl/manager.mli 7912 1034006019 c/46_manager.ml 1.1) (mlcuddidl/manager.mli 7912 1034006019 c/46_manager.ml 1.1)
(test/time.res 6325 1037192189 b/49_time.res 1.24) (test/time.res 6326 1037625990 b/49_time.res 1.25)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1) (doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/sim2chro.mli 1455 1027943375 b/23_sim2chro.m 1.5) (source/sim2chro.mli 1524 1037625990 b/23_sim2chro.m 1.6)
(source/command_line_luc_exe.mli 1055 1036675177 b/34_command_li 1.6) (source/command_line_luc_exe.mli 1055 1036675177 b/34_command_li 1.6)
(test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1) (test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1)
(source/Makefile.lucky 2093 1037192189 b/41_Makefile.i 1.9) (source/Makefile.lucky 2091 1037625990 b/41_Makefile.i 1.10)
(TAGS 9825 1007379917 21_TAGS 1.6) (TAGS 9825 1007379917 21_TAGS 1.6)
(mlcuddidl/rdd.ml 8746 1034006019 c/41_rdd.ml 1.1) (mlcuddidl/rdd.ml 8746 1034006019 c/41_rdd.ml 1.1)
(source/Makefile.lurette_lib 1790 1037192189 c/2_Makefile.l 1.9) (source/Makefile.lurette_lib 1797 1037625990 c/2_Makefile.l 1.10)
(source/parse_env.mli 1028 1036511217 40_parse_env. 1.11) (source/parse_env.mli 1028 1036511217 40_parse_env. 1.11)
(source/gen_stubs.ml 27065 1036048863 24_generate_l 1.41) (source/gen_stubs.ml 27065 1036048863 24_generate_l 1.41)
(OcamlMakefile 22696 1037192189 17_OcamlMakef 1.46) (OcamlMakefile 22696 1037192189 17_OcamlMakef 1.46)
...@@ -77,10 +77,10 @@ ...@@ -77,10 +77,10 @@
(mlcuddidl/README 1574 1034006019 d/8_README 1.1) (mlcuddidl/README 1574 1034006019 d/8_README 1.1)
(cuddaux/README 1427 1034006019 c/34_README 1.1) (cuddaux/README 1427 1034006019 c/34_README 1.1)
(source/Makefile.lurettetop 368 1037192189 d/14_Makefile.l 1.2) (source/Makefile.lurettetop 368 1037192189 d/14_Makefile.l 1.2)
(source/ne.mli 2376 1033723811 c/22_ne.mli 1.1) (source/ne.mli 2414 1037625990 c/22_ne.mli 1.2)
(README 2264 1034951022 10_README 1.4) (README 2266 1037625990 10_README 1.5)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2) (test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
(source/env_state.ml 21094 1036675177 51_env_state. 1.32) (source/env_state.ml 21336 1037625990 51_env_state. 1.33)
(mlcuddidl/manager_caml.c 39233 1034006019 c/45_manager_ca 1.1) (mlcuddidl/manager_caml.c 39233 1034006019 c/45_manager_ca 1.1)
(mlcuddidl/mtbdd.mli 4395 1034006019 c/43_mtbdd.mli 1.1) (mlcuddidl/mtbdd.mli 4395 1034006019 c/43_mtbdd.mli 1.1)
(source/env.mli 2027 1033738731 15_env.mli 1.16) (source/env.mli 2027 1033738731 15_env.mli 1.16)
...@@ -103,7 +103,7 @@ ...@@ -103,7 +103,7 @@
(source/command_line.mli 1491 1035557853 b/21_command_li 1.9) (source/command_line.mli 1491 1035557853 b/21_command_li 1.9)
(ihm/xlurette/xlurette.glade 49433 1035885606 c/13_xlurette.g 1.9) (ihm/xlurette/xlurette.glade 49433 1035885606 c/13_xlurette.g 1.9)
(demo/chaudiere/chaudiere.luc 446 1032789516 c/11_chaudiere. 1.5) (demo/chaudiere/chaudiere.luc 446 1032789516 c/11_chaudiere. 1.5)
(source/graph.mli 2218 1027066799 13_graph.mli 1.9) (source/graph.mli 2185 1037625990 13_graph.mli 1.10)
(mlcuddidl/bdd_caml.c 57199 1034006019 d/4_bdd_caml.c 1.1) (mlcuddidl/bdd_caml.c 57199 1034006019 d/4_bdd_caml.c 1.1)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1) (test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(cuddaux/Changes 42 1034006019 c/36_Changes 1.1) (cuddaux/Changes 42 1034006019 c/36_Changes 1.1)
...@@ -113,7 +113,7 @@ ...@@ -113,7 +113,7 @@
(mlcuddidl/mtbdd.ml 10185 1034006019 c/44_mtbdd.ml 1.1) (mlcuddidl/mtbdd.ml 10185 1034006019 c/44_mtbdd.ml 1.1)
(demo/chaudiere/chaudiere_ctrl.lus 177 1031732392 c/9_chaudiere_ 1.1) (demo/chaudiere/chaudiere_ctrl.lus 177 1031732392 c/9_chaudiere_ 1.1)
(source/control.mli 3208 1036675177 c/3_control.ml 1.3) (source/control.mli 3208 1036675177 c/3_control.ml 1.3)
(source/formula.ml 5975 1037192189 45_formula.ml 1.23) (source/formula.ml 5977 1037625990 45_formula.ml 1.24)
(cuddaux/Makefile 3091 1034006019 c/35_Makefile 1.1) (cuddaux/Makefile 3091 1034006019 c/35_Makefile 1.1)
(test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1) (test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1) (doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
...@@ -126,7 +126,7 @@ ...@@ -126,7 +126,7 @@
(mlcuddidl/bdd.mli 8573 1034006019 d/5_bdd.mli 1.1) (mlcuddidl/bdd.mli 8573 1034006019 d/5_bdd.mli 1.1)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1) (doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/solver.mli 1003 1027092697 38_solver.mli 1.13) (source/solver.mli 1003 1027092697 38_solver.mli 1.13)
(source/rnumsolver.ml 21392 1037192189 b/27_rnumsolver 1.15) (source/rnumsolver.ml 21487 1037625990 b/27_rnumsolver 1.16)
(mlcuddidl/cudd_caml.c 22890 1034006019 d/3_cudd_caml. 1.1) (mlcuddidl/cudd_caml.c 22890 1034006019 d/3_cudd_caml. 1.1)
(source/print.ml 5807 1033723811 47_print.ml 1.21) (source/print.ml 5807 1033723811 47_print.ml 1.21)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1) (test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
...@@ -141,7 +141,7 @@ ...@@ -141,7 +141,7 @@
(source/command_line_luc_exe.ml 2759 1036675177 b/33_command_li 1.8) (source/command_line_luc_exe.ml 2759 1036675177 b/33_command_li 1.8)
(mlcuddidl/cudd_caml.h 1210 1034006019 d/2_cudd_caml. 1.1) (mlcuddidl/cudd_caml.h 1210 1034006019 d/2_cudd_caml. 1.1)
(source/value.ml 2355 1033723811 c/23_value.ml 1.1) (source/value.ml 2355 1033723811 c/23_value.ml 1.1)
(test/time.exp 6325 1037192189 b/48_time.exp 1.21) (test/time.exp 6326 1037625990 b/48_time.exp 1.22)
(test/giro/allocator.lus 1087 1031732392 c/5_allocator. 1.1) (test/giro/allocator.lus 1087 1031732392 c/5_allocator. 1.1)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2) (lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(mlcuddidl/idd.mli 5470 1034006019 c/51_idd.mli 1.1) (mlcuddidl/idd.mli 5470 1034006019 c/51_idd.mli 1.1)
......
...@@ -14,6 +14,8 @@ In order to install and use it, you need: ...@@ -14,6 +14,8 @@ In order to install and use it, you need:
http://caml.inria.fr/camlidl/ http://caml.inria.fr/camlidl/
Also, it is better if you also have dot (graph drawing), and gv Also, it is better if you also have dot (graph drawing), and gv
(post-script viewing). To use xlurette, you probably need GTK. (post-script viewing). To use xlurette, you probably need GTK.
......
;; -*- Prcs -*- ;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3) (Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette") (Project-Description "Lurette")
(Project-Version lurette 0 116) (Project-Version lurette 0 117)
(Parent-Version lurette 0 115) (Parent-Version lurette 0 116)
(Version-Log " (Version-Log "
source/solver.ml: Various minor fixes in the documentation
Give a better error message when users do not initialize pre vars.
source/parse_env.ml: + Use a version of ocaml-3.06 that has been configured with -no-curses,
source/formula.ml: which make things sligthly slower, but that avoid the need to find
source/prevar.ml/mli: (new files) the curses lib...
Put here everything that handles the internal representation of pre var names.
Pretty print internal pre var names. source/ne.ml:
source/*.ml:
Ne.find now returns an option value instead of raising a Not_found
exp, which was not trap in some circumstances...
source/ne.ml:
Also, fix a couple of bugs where the code was supposing (falsely)
that the constant (empty string) was always in the Map.
") ")
(New-Version-Log "" (New-Version-Log ""
) )
(Checkin-Time "Wed, 13 Nov 2002 13:56:29 +0100") (Checkin-Time "Mon, 18 Nov 2002 14:26:30 +0100")
(Checkin-Login jahier) (Checkin-Login jahier)
(Populate-Ignore ()) (Populate-Ignore ())
(Project-Keywords) (Project-Keywords)
...@@ -29,7 +34,7 @@ source/prevar.ml/mli: (new files) ...@@ -29,7 +34,7 @@ source/prevar.ml/mli: (new files)
;; Sources files for luc_exe ;; Sources files for luc_exe
(source/luc_exe.mli (lurette/b/31_ima_exe.ml 1.2 644)) (source/luc_exe.mli (lurette/b/31_ima_exe.ml 1.2 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.22 644)) (source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.23 644))
(source/command_line_luc_exe.ml (lurette/b/33_command_li 1.8 644)) (source/command_line_luc_exe.ml (lurette/b/33_command_li 1.8 644))
(source/command_line_luc_exe.mli (lurette/b/34_command_li 1.6 644)) (source/command_line_luc_exe.mli (lurette/b/34_command_li 1.6 644))
...@@ -42,19 +47,19 @@ source/prevar.ml/mli: (new files) ...@@ -42,19 +47,19 @@ source/prevar.ml/mli: (new files)
(source/command_line.mli (lurette/b/21_command_li 1.9 644)) (source/command_line.mli (lurette/b/21_command_li 1.9 644))
;; Sources files common to lurette and luc_exe ;; Sources files common to lurette and luc_exe
(source/graph.mli (lurette/13_graph.mli 1.9 644)) (source/graph.mli (lurette/13_graph.mli 1.10 644))
(source/graph.ml (lurette/14_graph.ml 1.7 644)) (source/graph.ml (lurette/14_graph.ml 1.8 644))
(source/env.mli (lurette/15_env.mli 1.16 644)) (source/env.mli (lurette/15_env.mli 1.16 644))
(source/env.ml (lurette/16_env.ml 1.29 644)) (source/env.ml (lurette/16_env.ml 1.29 644))
(source/util.ml (lurette/35_util.ml 1.35 444)) (source/util.ml (lurette/35_util.ml 1.36 444))
(source/solver.mli (lurette/38_solver.mli 1.13 644)) (source/solver.mli (lurette/38_solver.mli 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.35 644)) (source/solver.ml (lurette/39_solver.ml 1.36 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.9 644)) (source/rnumsolver.mli (lurette/b/26_rnumsolver 1.9 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.15 644)) (source/rnumsolver.ml (lurette/b/27_rnumsolver 1.16 644))
(source/parse_env.mli (lurette/40_parse_env. 1.11 644)) (source/parse_env.mli (lurette/40_parse_env. 1.11 644))
(source/parse_env.ml (lurette/41_parse_env. 1.32 644)) (source/parse_env.ml (lurette/41_parse_env. 1.32 644))
...@@ -63,7 +68,7 @@ source/prevar.ml/mli: (new files) ...@@ -63,7 +68,7 @@ source/prevar.ml/mli: (new files)
(source/show_env.ml (lurette/43_show_env.m 1.16 644)) (source/show_env.ml (lurette/43_show_env.m 1.16 644))
(source/formula.mli (lurette/44_formula.ml 1.19 644)) (source/formula.mli (lurette/44_formula.ml 1.19 644))
(source/formula.ml (lurette/45_formula.ml 1.23 644)) (source/formula.ml (lurette/45_formula.ml 1.24 644))
(source/print.mli (lurette/46_print.mli 1.12 644)) (source/print.mli (lurette/46_print.mli 1.12 644))
(source/print.ml (lurette/47_print.ml 1.21 644)) (source/print.ml (lurette/47_print.ml 1.21 644))
...@@ -72,12 +77,12 @@ source/prevar.ml/mli: (new files) ...@@ -72,12 +77,12 @@ source/prevar.ml/mli: (new files)
(source/eval.ml (lurette/49_eval.ml 1.13 644)) (source/eval.ml (lurette/49_eval.ml 1.13 644))
(source/env_state.mli (lurette/50_env_state. 1.25 644)) (source/env_state.mli (lurette/50_env_state. 1.25 644))
(source/env_state.ml (lurette/51_env_state. 1.32 644)) (source/env_state.ml (lurette/51_env_state. 1.33 644))
(source/automata.mli (lurette/b/46_automata.m 1.3 644)) (source/automata.mli (lurette/b/46_automata.m 1.3 644))
(source/automata.ml (lurette/b/47_automata.m 1.6 644)) (source/automata.ml (lurette/b/47_automata.m 1.6 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.5 644)) (source/sim2chro.mli (lurette/b/23_sim2chro.m 1.6 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.14 644)) (source/sim2chro.ml (lurette/b/24_sim2chro.m 1.14 644))
(source/gne.mli (lurette/b/36_gne.mli 1.4 644)) (source/gne.mli (lurette/b/36_gne.mli 1.4 644))
...@@ -92,8 +97,8 @@ source/prevar.ml/mli: (new files) ...@@ -92,8 +97,8 @@ source/prevar.ml/mli: (new files)
(source/constraint.mli (lurette/c/18_constraint 1.4 644)) (source/constraint.mli (lurette/c/18_constraint 1.4 644))
(source/constraint.ml (lurette/c/19_constraint 1.4 644)) (source/constraint.ml (lurette/c/19_constraint 1.4 644))
(source/ne.ml (lurette/c/21_ne.ml 1.2 644)) (source/ne.ml (lurette/c/21_ne.ml 1.3 644))
(source/ne.mli (lurette/c/22_ne.mli 1.1 644)) (source/ne.mli (lurette/c/22_ne.mli 1.2 644))
(source/value.ml (lurette/c/23_value.ml 1.1 644)) (source/value.ml (lurette/c/23_value.ml 1.1 644))
(source/value.mli (lurette/c/24_value.mli 1.1 644)) (source/value.mli (lurette/c/24_value.mli 1.1 644))
...@@ -119,9 +124,9 @@ source/prevar.ml/mli: (new files) ...@@ -119,9 +124,9 @@ source/prevar.ml/mli: (new files)
(source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.2 644)) (source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.2 644))
(source/Makefile.gen_fake_lutin (lurette/d/17_Makefile.g 1.1 644)) (source/Makefile.gen_fake_lutin (lurette/d/17_Makefile.g 1.1 644))
(source/Makefile.show_luc (lurette/b/40_Makefile.s 1.8 644)) (source/Makefile.show_luc (lurette/b/40_Makefile.s 1.8 644))
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.9 644)) (source/Makefile.lucky (lurette/b/41_Makefile.i 1.10 644))
(source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.5 644)) (source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.5 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.9 644)) (source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.10 644))
(source/Makefile (lurette/c/20_Makefile 1.9 644)) (source/Makefile (lurette/c/20_Makefile 1.9 644))
;; Documentation ;; Documentation
...@@ -133,14 +138,14 @@ source/prevar.ml/mli: (new files) ...@@ -133,14 +138,14 @@ source/prevar.ml/mli: (new files)
(doc/ocamldoc.hva (lurette/b/13_ocamldoc.h 1.1 644)) (doc/ocamldoc.hva (lurette/b/13_ocamldoc.h 1.1 644))
;; Misc ;; Misc
(README (lurette/10_README 1.4 644)) (README (lurette/10_README 1.5 644))
(ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644)) (ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644))
(lurette.dep.dot (lurette/b/4_lurette.de 1.2 644)) (lurette.dep.dot (lurette/b/4_lurette.de 1.2 644))
(lurette.depfull.dot (lurette/b/5_lurette.de 1.2 644)) (lurette.depfull.dot (lurette/b/5_lurette.de 1.2 644))
(TAGS (lurette/21_TAGS 1.6 644)) (TAGS (lurette/21_TAGS 1.6 644))
(test/time.exp (lurette/b/48_time.exp 1.21 644)) (test/time.exp (lurette/b/48_time.exp 1.22 644))
(test/time.res (lurette/b/49_time.res 1.24 644)) (test/time.res (lurette/b/49_time.res 1.25 644))
;; Various files used for testing purposes ;; Various files used for testing purposes
(test/usager.luc (lurette/b/14_usager.env 1.9 644)) (test/usager.luc (lurette/b/14_usager.env 1.9 644))
......
...@@ -16,7 +16,7 @@ LIBS = str nums # mlpoly ...@@ -16,7 +16,7 @@ LIBS = str nums # mlpoly
CLIBS = cudd_caml cuddaux cudd camlidl mtr st epd util # libppl libpolyi CLIBS = cudd_caml cuddaux cudd camlidl mtr st epd util # libppl libpolyi
USE_CAMLP4 = yes USE_CAMLP4 = yes
# STATIC = yes STATIC = yes
SOURCES_OCAML = \ SOURCES_OCAML = \
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
###################################################################### ######################################################################
OCAMLNCFLAGS = -inline 10 OCAMLNCFLAGS = -inline 10 -linkall
ifndef OCAMLFLAGS ifndef OCAMLFLAGS
OCAMLFLAGS := -noassert -unsafe OCAMLFLAGS := -noassert -unsafe
endif endif
...@@ -16,7 +16,7 @@ LIBS = str nums # mlpoly ...@@ -16,7 +16,7 @@ LIBS = str nums # mlpoly
CLIBS = cudd_caml cuddaux cudd mtr st epd util # libppl libpolyi CLIBS = cudd_caml cuddaux cudd mtr st epd util # libppl libpolyi
USE_CAMLP4 = yes USE_CAMLP4 = yes
# STATIC = yes STATIC = yes
SOURCES = \ SOURCES = \
......
...@@ -611,6 +611,15 @@ let (clear_all : unit -> unit) = ...@@ -611,6 +611,15 @@ let (clear_all : unit -> unit) =
(* Exported *) (* Exported *)
let (dump_env_state_stat : out_channel -> unit) = let (dump_env_state_stat : out_channel -> unit) =
fun res -> fun res ->
let (size_str : ('a, 'b) t -> string) =
fun g ->
let (n1, n2, n3) = Graph.size g in
(
"table size = " ^ (string_of_int n1) ^
", node nb = " ^ (string_of_int n2) ^
", trans nb = " ^ (string_of_int n3)
)
in
let dump x = output_string res x in let dump x = output_string res x in
dump "***************************************************************\n"; dump "***************************************************************\n";
dump "******************* A few statistics ... **********************\n"; dump "******************* A few statistics ... **********************\n";
...@@ -670,7 +679,7 @@ let (dump_env_state_stat : out_channel -> unit) = ...@@ -670,7 +679,7 @@ let (dump_env_state_stat : out_channel -> unit) =
(string_of_int (hashtbl_size env_state.snt))); (string_of_int (hashtbl_size env_state.snt)));
dump "\n"; dump "\n";
dump ("*** graph:" ^ (Graph.size_str env_state.graph)); dump ("*** graph:" ^ (size_str env_state.graph));
dump "\n"; dump "\n";
dump ("*** ce_label:" ^ dump ("*** ce_label:" ^
......
...@@ -92,8 +92,8 @@ let rec ...@@ -92,8 +92,8 @@ let rec
and and
(formula_to_string: formula -> string) = (formula_to_string: formula -> string) =
fun f -> match f with fun f -> match f with
And(f1, f2) -> ("" ^ (formula_to_string f1) ^ " ^ " ^ And(f1, f2) -> ("(" ^ (formula_to_string f1) ^ " ^ " ^
(formula_to_string f2) ^ "") (formula_to_string f2) ^ ")")
| Or(f1, f2) -> ("(" ^ (formula_to_string f1) ^ " || " ^ | Or(f1, f2) -> ("(" ^ (formula_to_string f1) ^ " || " ^
(formula_to_string f2) ^ ")") (formula_to_string f2) ^ ")")
| IteB(f1, f2, f3) -> ("(if " ^ (formula_to_string f1) ^ " then " ^ | IteB(f1, f2, f3) -> ("(if " ^ (formula_to_string f1) ^ " then " ^
......
...@@ -86,13 +86,3 @@ let (size : ('a, 'b) t -> int * int * int) = ...@@ -86,13 +86,3 @@ let (size : ('a, 'b) t -> int * int * int) =
(Util.hashtbl_size g.table, (Util.hashtbl_size g.table,
List.length g.nodes, List.length g.nodes,
List.length g.trans) List.length g.trans)
let (size_str : ('a, 'b) t -> string) =
fun g ->
let (n1, n2, n3) = size g in
(
"table size = " ^ (string_of_int n1) ^
", node nb = " ^ (string_of_int n2) ^
", trans nb = " ^ (string_of_int n3)
)
...@@ -8,9 +8,9 @@ ...@@ -8,9 +8,9 @@
** Author: jahier@imag.fr ** Author: jahier@imag.fr
*) *)
(** A graph data structure as well as various functions that operates (** A graph data structure as well as various functions that operate
over it. This ADT is optimized for get_* functions at the cost of an over it. This ADT is optimized for get_* functions at the cost of a
expensive add_trans. more expensive add_trans.
*) *)
...@@ -68,4 +68,3 @@ val get_all_trans: ('a, 'b) t -> ('a * 'b * 'a) list ...@@ -68,4 +68,3 @@ val get_all_trans: ('a, 'b) t -> ('a * 'b * 'a) list
val size : ('a, 'b) t -> int * int * int val size : ('a, 'b) t -> int * int * int
(** Return the number of nodes and the number of transitions of the graph. *) (** Return the number of nodes and the number of transitions of the graph. *)
val size_str : ('a, 'b) t -> string
...@@ -311,10 +311,10 @@ and ...@@ -311,10 +311,10 @@ and
else options.user_seed else options.user_seed
in in
Random.init seed ; Random.init seed ;
print_string "#The random engine was initialized with the seed "; output_string stderr "#The random engine was initialized with the seed ";
print_int seed; output_string stderr (string_of_int seed);
print_string "\n "; output_string stderr "\n ";
flush stdout ; flush stderr ;
if options.show_automata then ( if options.show_automata then (
......
...@@ -226,10 +226,10 @@ let (make : string -> Value.num -> t) = ...@@ -226,10 +226,10 @@ let (make : string -> Value.num -> t) =
(StringMap.add vn nval StringMap.empty) (StringMap.add vn nval StringMap.empty)
(* exported *) (* exported *)
let (find : string -> t -> Value.num) = let (find : string -> t -> Value.num option) =
fun vn ne -> fun vn ne ->
StringMap.find vn ne try Some(StringMap.find vn ne)
with Not_found -> None
(****************************************************************************) (****************************************************************************)
...@@ -264,7 +264,7 @@ let (nexpr_add : (Value.num * string) -> t -> t) = ...@@ -264,7 +264,7 @@ let (nexpr_add : (Value.num * string) -> t -> t) =
(* exported *) (* exported *)
let (apply_subst : t -> subst -> t) = let (apply_subst : t -> subst -> t) =
fun ne2 ((vn, b), ne1) -> fun ne2 ((vn, b), ne1) ->
try try
let a = StringMap.find vn ne2 in let a = StringMap.find vn ne2 in
let new_ne1 = let new_ne1 =
...@@ -294,9 +294,15 @@ let (apply_simple_subst : t -> string * Value.num -> t) = ...@@ -294,9 +294,15 @@ let (apply_simple_subst : t -> string * Value.num -> t) =
fun ne (vn, v) -> fun ne (vn, v) ->
try try
let a = StringMap.find vn ne in let a = StringMap.find vn ne in
let b = StringMap.find "" ne in
let ne2 = StringMap.remove vn ne in let ne2 = StringMap.remove vn ne in
StringMap.add "" ((Value.add_num b (Value.mult_num v a))) ne2 (
try
let b = StringMap.find "" ne in
StringMap.add "" ((Value.add_num b (Value.mult_num v a))) ne2
with
Not_found ->
StringMap.add "" (Value.mult_num v a) ne2
)
with with
Not_found -> ne Not_found -> ne
...@@ -310,20 +316,26 @@ let rec (resolve_triangular_system :((string * Value.num) * t) list -> ...@@ -310,20 +316,26 @@ let rec (resolve_triangular_system :((string * Value.num) * t) list ->
match sl with match sl with
[] -> [] [] -> []
| ((vn, v), ne)::tail -> | ((vn, v), ne)::tail ->
let cst = StringMap.find "" ne let s =
and ne2 = StringMap.remove "" ne in try
if let cst = StringMap.find "" ne in
ne2 <> StringMap.empty if
then (StringMap.remove "" ne) <> StringMap.empty
raise Not_triangular then
else raise Not_triangular
let s = (vn, Value.quot_num cst v) in else
let new_tail = (vn, Value.quot_num cst v)
List.map with Not_found ->
(fun (x, ne) -> x, apply_simple_subst ne s) match v with
tail I _ -> (vn, I 0)
in | F _ -> (vn, F 0.0)
s::(resolve_triangular_system new_tail) in
let new_tail =
List.map
(fun (x, ne) -> x, apply_simple_subst ne s)
tail
in
s::(resolve_triangular_system new_tail)
(****************************************************************************) (****************************************************************************)
......
...@@ -48,7 +48,7 @@ val make : string -> Value.num -> t ...@@ -48,7 +48,7 @@ val make : string -> Value.num -> t
(** [find var ne] returns the coef of the variable [var] in (** [find var ne] returns the coef of the variable [var] in
[ne]. Raises Not_found if [var] is not in [ne]. *) [ne]. Raises Not_found if [var] is not in [ne]. *)
val find : string -> t -> Value.num val find : string -> t -> Value.num option
(** [nexpr_add (a, x) ne] returns [ne + a.x]. *) (** [nexpr_add (a, x) ne] returns [ne + a.x]. *)
...@@ -66,7 +66,8 @@ val apply_simple_subst : t -> string * Value.num -> t ...@@ -66,7 +66,8 @@ val apply_simple_subst : t -> string * Value.num -> t
(** [resolve_triangular_system sl] solves the system defined by the (** [resolve_triangular_system sl] solves the system defined by the
list of equations [a.x_i -> Sum_{j=1,n_i}(a_j.x_i_j) + cst] if it list of equations [a.x_i -> Sum_{j=1,n_i}(a_j.x_i_j) + cst] if it
forms a triangular system. It raises [Not_triangular] otherwise. forms a triangular system (namely, its dimension is 1). It raises
[Not_triangular] otherwise.
*) *)
exception Not_triangular exception Not_triangular
val resolve_triangular_system :((string * Value.num) * t) list -> val resolve_triangular_system :((string * Value.num) * t) list ->
......
...@@ -330,11 +330,19 @@ and (split_store_do : store -> Constraint.ineq -> store * store) = ...@@ -330,11 +330,19 @@ and (split_store_do : store -> Constraint.ineq -> store * store) =
(* in *) (* in *)
( match cstr with ( match cstr with
GZ(ne) -> GZ(ne) ->
if Value.num_sup_zero (Ne.find "" ne) if
( match (Ne.find "" ne) with
Some v -> Value.num_sup_zero v
| None -> false
)
then store, {var=None ; substl = [] ; delay = []} then store, {var=None ; substl = [] ; delay = []}
else {var=None ; substl = [] ; delay = []}, store else {var=None ; substl = [] ; delay = []}, store
| GeqZ(ne) -> | GeqZ(ne) ->
if Value.num_supeq_zero (Ne.find "" ne) if
( match (Ne.find "" ne) with
Some v -> Value.num_supeq_zero v
| None -> true
)
then store, store then store, store
else raise No_numeric_solution else raise No_numeric_solution
) )
...@@ -652,26 +660,24 @@ and (split_store_eq : store -> Ne.t -> store * store * store ) = ...@@ -652,26 +660,24 @@ and (split_store_eq : store -> Ne.t -> store * store * store ) =
if if
dim = 0 dim = 0
then