Commit aef52d9c authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.116 Wed, 13 Nov 2002 13:56:29 +0100 by jahier

Parent-Version:      0.115
Version-Log:

source/solver.ml:
   Give a better error message when users do not initialize pre vars.

source/parse_env.ml:
source/formula.ml:
source/prevar.ml/mli: (new files)
   Put here everything that handles the internal representation of pre var
names.

   Pretty print internal pre var names.

Project-Description: Lurette
parent 7c4feb61
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
;; REALLY bad things. ;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3) (Created-By-Prcs-Version 1 3 3)
(source/automata.ml 15954 1036675177 b/47_automata.m 1.6) (source/automata.ml 15954 1036675177 b/47_automata.m 1.6)
(source/formula.mli 2805 1033397911 44_formula.ml 1.18) (source/formula.mli 2806 1037192189 44_formula.ml 1.19)
(test/heater_float.lus 177 1034351455 b/44_heater_flo 1.2) (test/heater_float.lus 177 1034351455 b/44_heater_flo 1.2)
(test/passerelle.luc 984 1032789516 b/17_passerelle 1.8) (test/passerelle.luc 984 1032789516 b/17_passerelle 1.8)
(doc/synthese 2556 1007379917 b/2_synthese 1.1) (doc/synthese 2556 1007379917 b/2_synthese 1.1)
...@@ -19,12 +19,14 @@ ...@@ -19,12 +19,14 @@
(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 9140 1033723811 c/21_ne.ml 1.1) (source/ne.ml 9160 1037192189 c/21_ne.ml 1.2)
(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 12191 1036675177 b/32_ima_exe.ml 1.22)
(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 2563 1027066799 14_graph.ml 1.7)
(ihm/xlurette/makefile 1583 1036048863 c/16_makefile 1.6) (ihm/xlurette/makefile 1583 1036048863 c/16_makefile 1.6)
...@@ -35,34 +37,34 @@ ...@@ -35,34 +37,34 @@
(source/eval.ml 7755 1027066799 49_eval.ml 1.13) (source/eval.ml 7755 1027066799 49_eval.ml 1.13)
(source/env.ml 8013 1027349504 16_env.ml 1.29) (source/env.ml 8013 1027349504 16_env.ml 1.29)
(demo/chaudiere/buggy_chaudiere_ctrl.lus 219 1031732392 c/10_buggy_chau 1.1) (demo/chaudiere/buggy_chaudiere_ctrl.lus 219 1031732392 c/10_buggy_chau 1.1)
(source/Makefile.show_luc 937 1034351455 b/40_Makefile.s 1.7) (source/Makefile.show_luc 1026 1037192189 b/40_Makefile.s 1.8)
(source/env_state.mli 6791 1036675177 50_env_state. 1.25) (source/env_state.mli 6791 1036675177 50_env_state. 1.25)
(mlcuddidl/idd.ml 7061 1034006019 d/0_idd.ml 1.1) (mlcuddidl/idd.ml 7061 1034006019 d/0_idd.ml 1.1)
(source/print.mli 1145 1033397911 46_print.mli 1.12) (source/print.mli 1145 1033397911 46_print.mli 1.12)
(mlcuddidl/rdd.mli 7174 1034006019 c/40_rdd.mli 1.1) (mlcuddidl/rdd.mli 7174 1034006019 c/40_rdd.mli 1.1)
(test/Makefile 32 1035531408 c/0_Makefile 1.8) (test/Makefile 32 1035531408 c/0_Makefile 1.8)
(source/parse_env.ml 31317 1036585364 41_parse_env. 1.31) (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 32174 1036675177 39_solver.ml 1.34) (source/solver.ml 33352 1037192189 39_solver.ml 1.35)
(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 20779 1036675177 35_util.ml 1.35)
(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 6326 1036675177 b/49_time.res 1.23) (test/time.res 6325 1037192189 b/49_time.res 1.24)
(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 1455 1027943375 b/23_sim2chro.m 1.5)
(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 2003 1035531408 b/41_Makefile.i 1.8) (source/Makefile.lucky 2093 1037192189 b/41_Makefile.i 1.9)
(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 1741 1035531408 c/2_Makefile.l 1.8) (source/Makefile.lurette_lib 1790 1037192189 c/2_Makefile.l 1.9)
(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 22626 1034951022 17_OcamlMakef 1.45) (OcamlMakefile 22696 1037192189 17_OcamlMakef 1.46)
(source/command_line.ml 4914 1035557853 b/20_command_li 1.10) (source/command_line.ml 4914 1035557853 b/20_command_li 1.10)
(mlcuddidl/bdd.ml 10889 1034006019 d/6_bdd.ml 1.1) (mlcuddidl/bdd.ml 10889 1034006019 d/6_bdd.ml 1.1)
(mlcuddidl/idd_caml.c 15964 1034006019 c/50_idd_caml.c 1.1) (mlcuddidl/idd_caml.c 15964 1034006019 c/50_idd_caml.c 1.1)
...@@ -74,7 +76,7 @@ ...@@ -74,7 +76,7 @@
(source/lurettetop.ml 30402 1036048863 c/1_lurettetop 1.22) (source/lurettetop.ml 30402 1036048863 c/1_lurettetop 1.22)
(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 300 1035531408 d/14_Makefile.l 1.1) (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 2376 1033723811 c/22_ne.mli 1.1)
(README 2264 1034951022 10_README 1.4) (README 2264 1034951022 10_README 1.4)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2) (test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
...@@ -84,7 +86,7 @@ ...@@ -84,7 +86,7 @@
(source/env.mli 2027 1033738731 15_env.mli 1.16) (source/env.mli 2027 1033738731 15_env.mli 1.16)
(mlcuddidl/rdd_caml.c 41613 1034006019 c/39_rdd_caml.c 1.1) (mlcuddidl/rdd_caml.c 41613 1034006019 c/39_rdd_caml.c 1.1)
(Makefile.common.in 528 1034951022 d/12_Makefile.c 1.2) (Makefile.common.in 528 1034951022 d/12_Makefile.c 1.2)
(user-rules 14217 1036675177 c/14_myrules 1.18) (user-rules 14581 1037192189 c/14_myrules 1.19)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1) (doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12) (source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/gne.mli 1552 1033397911 b/36_gne.mli 1.4) (source/gne.mli 1552 1033397911 b/36_gne.mli 1.4)
...@@ -111,10 +113,10 @@ ...@@ -111,10 +113,10 @@
(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 5759 1035898240 45_formula.ml 1.22) (source/formula.ml 5975 1037192189 45_formula.ml 1.23)
(cuddaux/Makefile 3091 1034006019 c/35_Makefile 1.1) (cuddaux/Makefile 3091 1034006019 c/35_Makefile 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 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)
(mlcuddidl/idd.idl 10595 1034006019 d/1_idd.idl 1.1) (mlcuddidl/idd.idl 10595 1034006019 d/1_idd.idl 1.1)
(source/gne.ml 2767 1033397911 b/37_gne.ml 1.4) (source/gne.ml 2767 1033397911 b/37_gne.ml 1.4)
(cuddaux/cuddaux.h 2381 1034006019 c/33_cuddaux.h 1.1) (cuddaux/cuddaux.h 2381 1034006019 c/33_cuddaux.h 1.1)
...@@ -124,13 +126,13 @@ ...@@ -124,13 +126,13 @@
(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 20806 1036048863 b/27_rnumsolver 1.14) (source/rnumsolver.ml 21392 1037192189 b/27_rnumsolver 1.15)
(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)
(configure.in 5208 1034351455 d/11_configure. 1.1) (configure.in 5208 1034351455 d/11_configure. 1.1)
(cuddaux/cuddauxBridge.c 6099 1034006019 c/31_cuddauxBri 1.1) (cuddaux/cuddauxBridge.c 6099 1034006019 c/31_cuddauxBri 1.1)
(source/show_env.ml 3594 1036675177 43_show_env.m 1.15) (source/show_env.ml 3642 1037192189 43_show_env.m 1.16)
(mlcuddidl/Changes 64 1034006019 d/10_Changes 1.1) (mlcuddidl/Changes 64 1034006019 d/10_Changes 1.1)
(source/parse_poc.ml 7093 1036048863 d/15_parse_poc. 1.1) (source/parse_poc.ml 7093 1036048863 d/15_parse_poc. 1.1)
(cuddaux/cuddauxAddIte.c 12812 1034006019 c/32_cuddauxAdd 1.1) (cuddaux/cuddauxAddIte.c 12812 1034006019 c/32_cuddauxAdd 1.1)
...@@ -139,7 +141,7 @@ ...@@ -139,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 6326 1036675177 b/48_time.exp 1.20) (test/time.exp 6325 1037192189 b/48_time.exp 1.21)
(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)
......
...@@ -5,7 +5,7 @@ ...@@ -5,7 +5,7 @@
# For updates see: # For updates see:
# http://www.oefai.at/~markus/ocaml_sources # http://www.oefai.at/~markus/ocaml_sources
# #
# $Id: OcamlMakefile 1.45 Fri, 18 Oct 2002 16:23:42 +0200 jahier $ # $Id: OcamlMakefile 1.46 Wed, 13 Nov 2002 13:56:29 +0100 jahier $
# #
########################################################################### ###########################################################################
...@@ -16,6 +16,7 @@ ...@@ -16,6 +16,7 @@
SOURCES_LURETTE_LIB = \ SOURCES_LURETTE_LIB = \
$(LURETTE_PATH)/source/util.ml \ $(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \ $(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \ $(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \ $(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \
......
;; -*- 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 115) (Project-Version lurette 0 116)
(Parent-Version lurette 0 114) (Parent-Version lurette 0 115)
(Version-Log " (Version-Log "
source/automata.ml: source/solver.ml:
Fix a bug where esp loops were not always cutted properly in some cases. Give a better error message when users do not initialize pre vars.
source/show_env.ml: source/parse_env.ml:
Truncate too long for in the dot output (which bugs dot or gv). source/formula.ml:
source/prevar.ml/mli: (new files)
Put here everything that handles the internal representation of pre var names.
ihm/xlurette/xlurette_glade_main.ml: Pretty print internal pre var names.
Accept both .lut or .lut files as anv files, and make the show buttons
behave properly in both cases.
") ")
(New-Version-Log "" (New-Version-Log ""
) )
(Checkin-Time "Thu, 07 Nov 2002 14:19:37 +0100") (Checkin-Time "Wed, 13 Nov 2002 13:56:29 +0100")
(Checkin-Login jahier) (Checkin-Login jahier)
(Populate-Ignore ()) (Populate-Ignore ())
(Project-Keywords) (Project-Keywords)
...@@ -51,19 +51,19 @@ ihm/xlurette/xlurette_glade_main.ml: ...@@ -51,19 +51,19 @@ ihm/xlurette/xlurette_glade_main.ml:
(source/util.ml (lurette/35_util.ml 1.35 444)) (source/util.ml (lurette/35_util.ml 1.35 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.34 644)) (source/solver.ml (lurette/39_solver.ml 1.35 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.14 644)) (source/rnumsolver.ml (lurette/b/27_rnumsolver 1.15 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.31 644)) (source/parse_env.ml (lurette/41_parse_env. 1.32 644))
(source/show_env.mli (lurette/42_show_env.m 1.8 644)) (source/show_env.mli (lurette/42_show_env.m 1.8 644))
(source/show_env.ml (lurette/43_show_env.m 1.15 644)) (source/show_env.ml (lurette/43_show_env.m 1.16 644))
(source/formula.mli (lurette/44_formula.ml 1.18 644)) (source/formula.mli (lurette/44_formula.ml 1.19 644))
(source/formula.ml (lurette/45_formula.ml 1.22 644)) (source/formula.ml (lurette/45_formula.ml 1.23 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))
...@@ -92,12 +92,14 @@ ihm/xlurette/xlurette_glade_main.ml: ...@@ -92,12 +92,14 @@ ihm/xlurette/xlurette_glade_main.ml:
(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.1 644)) (source/ne.ml (lurette/c/21_ne.ml 1.2 644))
(source/ne.mli (lurette/c/22_ne.mli 1.1 644)) (source/ne.mli (lurette/c/22_ne.mli 1.1 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))
(source/prevar.ml (lurette/d/18_prevar.ml 1.1 644))
(source/prevar.mli (lurette/d/19_prevar.mli 1.1 644))
(source/parse_poc.ml (lurette/d/15_parse_poc. 1.1 644)) (source/parse_poc.ml (lurette/d/15_parse_poc. 1.1 644))
(source/gen_fake_lutin.ml (lurette/d/16_gen_fake_l 1.1 644)) (source/gen_fake_lutin.ml (lurette/d/16_gen_fake_l 1.1 644))
...@@ -108,18 +110,18 @@ ihm/xlurette/xlurette_glade_main.ml: ...@@ -108,18 +110,18 @@ ihm/xlurette/xlurette_glade_main.ml:
;; Make files ;; Make files
(configure.in (lurette/d/11_configure. 1.1 644)) (configure.in (lurette/d/11_configure. 1.1 644))
(Makefile.common.in (lurette/d/12_Makefile.c 1.2 644)) (Makefile.common.in (lurette/d/12_Makefile.c 1.2 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.45 644)) (OcamlMakefile (lurette/17_OcamlMakef 1.46 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.15 644)) (Makefile.lurette (lurette/b/38_Makefile.l 1.15 644))
(user-rules (lurette/c/14_myrules 1.18 644)) (user-rules (lurette/c/14_myrules 1.19 644))
(user-rules.skel (lurette/c/25_user-rules 1.1 644)) (user-rules.skel (lurette/c/25_user-rules 1.1 644))
(Makefile (lurette/d/13_Makefile 1.1 644)) (Makefile (lurette/d/13_Makefile 1.1 644))
(source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.1 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.7 644)) (source/Makefile.show_luc (lurette/b/40_Makefile.s 1.8 644))
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.8 644)) (source/Makefile.lucky (lurette/b/41_Makefile.i 1.9 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.8 644)) (source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.9 644))
(source/Makefile (lurette/c/20_Makefile 1.9 644)) (source/Makefile (lurette/c/20_Makefile 1.9 644))
;; Documentation ;; Documentation
...@@ -137,8 +139,8 @@ ihm/xlurette/xlurette_glade_main.ml: ...@@ -137,8 +139,8 @@ ihm/xlurette/xlurette_glade_main.ml:
(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.20 644)) (test/time.exp (lurette/b/48_time.exp 1.21 644))
(test/time.res (lurette/b/49_time.res 1.23 644)) (test/time.res (lurette/b/49_time.res 1.24 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))
...@@ -225,12 +227,6 @@ ihm/xlurette/xlurette_glade_main.ml: ...@@ -225,12 +227,6 @@ ihm/xlurette/xlurette_glade_main.ml:
(mlcuddidl/Changes (lurette/d/10_Changes 1.1 644)) (mlcuddidl/Changes (lurette/d/10_Changes 1.1 644))
;; Files added by populate at Thu, 24 Oct 2002 15:46:40 +0200,
;; to version 0.105(w), by jahier:
) )
(Merge-Parents) (Merge-Parents)
(New-Merge-Parents) (New-Merge-Parents)
...@@ -6,13 +6,13 @@ ...@@ -6,13 +6,13 @@
####################################################################### #######################################################################
OCAMLNCFLAGS = -inline 10 OCAMLNCFLAGS = -inline 10 -linkall
ifndef OCAMLFLAGS ifndef OCAMLFLAGS
OCAMLFLAGS := -noassert -unsafe OCAMLFLAGS := -noassert -unsafe
endif endif
# Requires cudd and mldd to be installed! # Requires cudd and mldd to be installed!
LIBS = str nums # mlpoly 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
...@@ -22,6 +22,7 @@ USE_CAMLP4 = yes ...@@ -22,6 +22,7 @@ USE_CAMLP4 = yes
SOURCES_OCAML = \ SOURCES_OCAML = \
$(LURETTE_PATH)/source/util.ml \ $(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \ $(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.ml \
$(LURETTE_PATH)/source/command_line_luc_exe.mli $(LURETTE_PATH)/source/command_line_luc_exe.ml \ $(LURETTE_PATH)/source/command_line_luc_exe.mli $(LURETTE_PATH)/source/command_line_luc_exe.ml \
$(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \ $(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \
$(LURETTE_PATH)/source/ne.mli $(LURETTE_PATH)/source/ne.ml \ $(LURETTE_PATH)/source/ne.mli $(LURETTE_PATH)/source/ne.ml \
......
...@@ -6,14 +6,11 @@ ...@@ -6,14 +6,11 @@
###################################################################### ######################################################################
OCAMLNCFLAGS = -inline 10
OCAMLNCFLAGS = -inline 10 -noassert -unsafe
ifndef OCAMLFLAGS ifndef OCAMLFLAGS
OCAMLFLAGS := -noassert -unsafe OCAMLFLAGS := -noassert -unsafe
endif endif
# Requires cudd and mldd to be installed! # Requires cudd and mldd to be installed!
LIBS = str nums # mlpoly 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
...@@ -24,6 +21,7 @@ USE_CAMLP4 = yes ...@@ -24,6 +21,7 @@ USE_CAMLP4 = yes
SOURCES = \ SOURCES = \
$(LURETTE_PATH)/source/util.ml \ $(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \ $(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \ $(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \ $(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \
......
...@@ -6,7 +6,10 @@ ...@@ -6,7 +6,10 @@
LIBS = unix str LIBS = unix str
CLIBS = CLIBS =
OCAMLNCFLAGS = -inline 10 OCAMLNCFLAGS = -inline 10 -linkall
ifndef OCAMLFLAGS
OCAMLFLAGS := -noassert -unsafe
endif
USE_CAMLP4 = yes USE_CAMLP4 = yes
......
...@@ -7,7 +7,7 @@ ...@@ -7,7 +7,7 @@
###################################################################### ######################################################################
OCAMLMAKEFILE = $(LURETTE_PATH)/OcamlMakefile OCAMLMAKEFILE = $(LURETTE_PATH)/OcamlMakefile
OCAMLNCFLAGS = -inline 10 OCAMLNCFLAGS = -inline 10 -linkall
LIBS = str LIBS = str
CLIBS = CLIBS =
...@@ -17,6 +17,7 @@ USE_CAMLP4 = yes ...@@ -17,6 +17,7 @@ USE_CAMLP4 = yes
SOURCES_OCAML = \ SOURCES_OCAML = \
$(LURETTE_PATH)/source/util.ml \ $(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.ml \
$(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \ $(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \ $(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \ $(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
......
...@@ -77,6 +77,11 @@ type env_loc = subst list ...@@ -77,6 +77,11 @@ type env_loc = subst list
(****************************************************************************) (****************************************************************************)
(* exported *)
let (formula_to_var_value: formula -> Value.t) = function
True -> B(true)
| False -> B(false)
| _ -> assert false
let rec let rec
...@@ -98,7 +103,7 @@ and ...@@ -98,7 +103,7 @@ and
| EqB(f1, f2) -> ((formula_to_string f1) ^ " = " ^ (formula_to_string f2)) | EqB(f1, f2) -> ((formula_to_string f1) ^ " = " ^ (formula_to_string f2))
| True -> "true" | True -> "true"
| False -> "false" | False -> "false"
| Bvar(str) -> str | Bvar(str) -> (Prevar.format str)
| Eq(e1, e2) -> ((expr_to_string e1) ^ " = " ^ (expr_to_string e2)) | Eq(e1, e2) -> ((expr_to_string e1) ^ " = " ^ (expr_to_string e2))
| Neq(e1, e2) -> ((expr_to_string e1) ^ " <> " ^ (expr_to_string e2)) | Neq(e1, e2) -> ((expr_to_string e1) ^ " <> " ^ (expr_to_string e2))
| SupEq(e1, e2) -> ((expr_to_string e1) ^ " >= " ^ (expr_to_string e2)) | SupEq(e1, e2) -> ((expr_to_string e1) ^ " >= " ^ (expr_to_string e2))
...@@ -118,8 +123,8 @@ and ...@@ -118,8 +123,8 @@ and
(expr_to_string e2) ^ ")") (expr_to_string e2) ^ ")")
| Mod(e1, e2) -> ("(" ^ (expr_to_string e1) ^ " mod " ^ | Mod(e1, e2) -> ("(" ^ (expr_to_string e1) ^ " mod " ^
(expr_to_string e2) ^ ")") (expr_to_string e2) ^ ")")
| Ivar(str) -> str | Ivar(str) -> (Prevar.format str)
| Fvar(str) -> str | Fvar(str) -> (Prevar.format str)
| Ival(i) -> string_of_int i | Ival(i) -> string_of_int i
| Fval(f) -> Util.my_string_of_float f | Fval(f) -> Util.my_string_of_float f
| Ite(f,e1,e2) -> ("(if " ^ (formula_to_string f) ^ " then " ^ | Ite(f,e1,e2) -> ("(if " ^ (formula_to_string f) ^ " then " ^
...@@ -177,7 +182,7 @@ let (print_subst_list : subst list -> out_channel -> unit) = ...@@ -177,7 +182,7 @@ let (print_subst_list : subst list -> out_channel -> unit) =
fun sl oc -> fun sl oc ->
List.iter List.iter
(fun (vn, e) -> (fun (vn, e) ->
output_string oc vn ; output_string oc (Prevar.format vn);
output_string oc " = "; output_string oc " = ";
Value.print oc e; Value.print oc e;
output_string oc "\n\t" output_string oc "\n\t"
...@@ -188,7 +193,7 @@ let (print_env_in : env_in -> out_channel -> unit) = ...@@ -188,7 +193,7 @@ let (print_env_in : env_in -> out_channel -> unit) =
fun tbl oc -> fun tbl oc ->
Hashtbl.iter Hashtbl.iter
(fun vn e -> (fun vn e ->
output_string oc vn ; output_string oc (Prevar.format vn) ;
output_string oc " = "; output_string oc " = ";
Value.print oc e; Value.print oc e;
output_string oc "\n\t" output_string oc "\n\t"
......
...@@ -102,3 +102,4 @@ val var_type_to_string : var_type -> string ...@@ -102,3 +102,4 @@ val var_type_to_string : var_type -> string
val var_type_to_string2 : var_type -> string val var_type_to_string2 : var_type -> string
val print_subst_list : subst list -> out_channel -> unit val print_subst_list : subst list -> out_channel -> unit
val print_env_in : env_in -> out_channel -> unit val print_env_in : env_in -> out_channel -> unit
...@@ -229,7 +229,7 @@ let (make : string -> Value.num -> t) = ...@@ -229,7 +229,7 @@ let (make : string -> Value.num -> t) =
let (find : string -> t -> Value.num) = let (find : string -> t -> Value.num) =
fun vn ne -> fun vn ne ->
StringMap.find vn ne StringMap.find vn ne
(****************************************************************************) (****************************************************************************)
...@@ -335,7 +335,7 @@ let (to_string : t -> string) = ...@@ -335,7 +335,7 @@ let (to_string : t -> string) =
(fun vn v acc -> (fun vn v acc ->
if vn = "" if vn = ""
then ((num_value_to_string v) ^ acc) then ((num_value_to_string v) ^ acc)
else (" + " ^ (num_value_to_string v ) ^ "*" ^ vn ^ acc )) else (" + " ^ (num_value_to_string v ) ^ "*" ^ ((Prevar.format vn) ^ acc)))
ne ne
"" ""
) )
......
...@@ -448,7 +448,7 @@ and (parse_prevar: in_channel -> aut_token -> vnt) = ...@@ -448,7 +448,7 @@ and (parse_prevar: in_channel -> aut_token -> vnt) =
'Genlex.Kwd ")"; pl = parse_pragma_list ic ; 'Genlex.Kwd ")"; pl = parse_pragma_list ic ;
'Genlex.Kwd ","; 'Genlex.Ident typ ; 'Genlex.Kwd ")" >] 'Genlex.Kwd ","; 'Genlex.Ident typ ; 'Genlex.Kwd ")" >]
-> ->
let pre_var = ("_pre" ^ (string_of_int i) ^ var) in let pre_var = Prevar.create_prevar_name i var in
( match typ with ( match typ with
"bool" -> (pre_var, BoolT) "bool" -> (pre_var, BoolT)
| "float" -> (pre_var, FloatT(-.default_max_float, default_max_float)) | "float" -> (pre_var, FloatT(-.default_max_float, default_max_float))
...@@ -783,7 +783,7 @@ and (parse_formula: in_channel -> vnt list -> aut_token -> formula) = ...@@ -783,7 +783,7 @@ and (parse_formula: in_channel -> vnt list -> aut_token -> formula) =
pl = parse_pragma_list ic pl = parse_pragma_list ic
>] >]
-> ->
let pre_id = ("_pre" ^ (string_of_int i) ^ id) in let pre_id = Prevar.create_prevar_name i id in
(* Ditto *) (* Ditto *)
let (_, vt) = List.find (fun (vn,vt) -> vn = pre_id) vars in let (_, vt) = List.find (fun (vn,vt) -> vn = pre_id) vars in
( match vt with ( match vt with
...@@ -907,7 +907,7 @@ and (parse_simple: in_channel -> vnt list -> aut_token -> expr) = ...@@ -907,7 +907,7 @@ and (parse_simple: in_channel -> vnt list -> aut_token -> expr) =
| [< 'Genlex.Ident "pre"; 'Genlex.Kwd "("; | [< 'Genlex.Ident "pre"; 'Genlex.Kwd "(";
'Genlex.Int i ; 'Genlex.Kwd "," ; 'Genlex.Ident id; 'Genlex.Int i ; 'Genlex.Kwd "," ; 'Genlex.Ident id;
'Genlex.Kwd ")"; pl = parse_pragma_list ic >] -> 'Genlex.Kwd ")"; pl = parse_pragma_list ic >] ->
let s = ("_pre" ^ (string_of_int i) ^ id) in let s = Prevar.create_prevar_name i id in
let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in
let var = let var =
match vt with match vt with
......
(*-----------------------------------------------------------------------
** Copyright (C) 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: prevar.ml
** Author: jahier@imag.fr
*)
(* exported *)
let (create_prevar_name : int -> string -> string) =
fun i str ->
("_pre" ^ (string_of_int i) ^ str)
let (is_pre_var : string -> bool) =
fun str ->
try (String.sub str 0 4) = "_pre"
with _ -> false
(* exported *)
let (format: string -> string) =
fun vn ->
try
let l = String.length vn in
let char_reg = Str.regexp "[^0-9]" in
let i = Str.search_forward char_reg vn 4 in
let pre_nb = (int_of_string (String.sub vn 4 (i-4))) in
let pre_list = Util.unfold (fun _ -> "pre ") () pre_nb in
("(" ^ (String.concat "" pre_list) ^ (String.sub vn i (l-i)) ^ ")")
with
| _ -> vn
(*-----------------------------------------------------------------------
** Copyright (C) 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: prevar.mli
** Author: jahier@imag.fr
*)
(** Internal representation of pre variables. *)
(** To give an internal name to pre var *)
val create_prevar_name : int -> string -> string
(** To pretty print pre var *)
val format: string -> string
(** [is_pre_va vn] returns iff [vn] is a pre variable. *)
val is_pre_var : string -> bool
This diff is collapsed.
...@@ -113,11 +113,13 @@ let (graph_to_dot: 'node list -> 'node list -> string -> ...@@ -113,11 +113,13 @@ let (graph_to_dot: 'node list -> 'node list -> string ->
(* Exported *) (* Exported *)
let max_label_size = 50