Skip to content

GitLab

Commit 540ee1f9 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 1.10 Thu, 20 Nov 2003 10:09:54 +0100 by jahier 

Parent-Version:      1.9
Version-Log:

removing of Env_state module -- part 1

Now env_step and env_try are fully functionnal (no side-effects).

Project-Description: Lurette
parent 67c17ef7
Hide whitespace changes
Inline Side-by-side
.lurette.prcs_aux
View file @ 540ee1f9
......@@ -8,10 +8,10 @@
(source/constraint.mli 1706 1069150632 c/18_constraint 1.8)
(test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1)
(mlcuddidl/Changes 64 1034006019 d/10_Changes 1.1)
(TODO 5329 1069150632 d/22_TODO 1.28)
(TODO 5574 1069319394 d/22_TODO 1.29)
(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 19809 1069150632 g/38_fair_bddd. 1.3)
(source/fair_bddd.ml 20308 1069319394 g/38_fair_bddd. 1.4)
(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 109061 1047029868 e/17_polka.texi 1.1)
......@@ -22,7 +22,7 @@
(share/pixmaps/open.xpm 782 1055926783 f/17_open.xpm 1.1)
(source/parse_luc.mli 3106 1069150632 40_parse_env. 1.17)
(polka/C/internal.c 699 1047029868 e/8_internal.c 1.1)
(source/solver.ml 7780 1069150632 39_solver.ml 1.57)
(source/solver.ml 8003 1069319394 39_solver.ml 1.58)
(ihm/xlurette/makefile 1853 1063786164 c/16_makefile 1.17)
(share/gen_fake_lucky.sh.in 115 1063786164 g/31_gen_fake_l 1.1)
(test/test_losange-10d.lus 108 1065787303 g/41_test_losan 1.1)
......@@ -32,7 +32,7 @@
(test/sparc-scade/libpwlinear.saofdm 1379 1055487917 e/43_libpwlinea 1.1)
(test/cygwin-scade/ConfAnnot.aty 13661 1055926783 g/4_ConfAnnot. 1.1)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(source/bddd.mli 1435 1069150632 g/37_bddd.mli 1.4)
(source/bddd.mli 1472 1069319394 g/37_bddd.mli 1.5)
(share/lucky_init.sh.in 1061 1063786164 e/24_lucky_init 1.11)
(test/heater.lus 176 1063786164 g/33_heater.lus 1.1)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
......@@ -57,7 +57,7 @@
(source/luc_exe.mli 449 1069150632 b/31_ima_exe.ml 1.3)
(doc/ocamldoc.sty 1732 1069150632 b/12_ocamldoc.s 1.2)
(polka/C/cherni.c 28868 1065787303 e/9_cherni.c 1.2)
(source/command_line_luc_exe.mli 1325 1065787303 b/34_command_li 1.12)
(source/command_line_luc_exe.mli 1306 1069319394 b/34_command_li 1.13)
(polka/C/poly.h 4314 1047029868 d/49_poly.h 1.1)
(polka/C/cherni.h 2217 1047029868 e/1_cherni.h 1.1)
(share/pixmaps/chrono.xpm 703 1055926783 f/23_chrono.xpm 1.1)
......@@ -92,7 +92,7 @@
(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 9551 1069150632 d/21_time-ecrin 1.30)
(test/time-ecrins.exp 9332 1069319394 d/21_time-ecrin 1.31)
(source/value.ml 2539 1063786164 c/23_value.ml 1.6)
(source/gne.ml 3467 1063029729 b/37_gne.ml 1.6)
(test/cygwin-scade/Pilot.vsp 2075 1055926783 f/40_Pilot.vsp 1.1)
......@@ -110,10 +110,10 @@
(test/cygwin-scade/Pilot.vsw 431 1055926783 f/39_Pilot.vsw 1.1)
(share/pixmaps/open_plus.xpm 787 1055926783 f/16_open_plus. 1.1)
(share/xlurettetop.bat.in 613 1063786164 g/19_xluretteto 1.1)
(source/env_state.ml 15958 1069150632 51_env_state. 1.50)
(source/env_state.ml 14477 1069319394 51_env_state. 1.51)
(test/test8.rif.exp 341 1065787303 g/18_test8.rif. 1.2)
(polka/caml/matrix.idl 5301 1047029868 d/34_matrix.idl 1.1)
(source/fair_bddd.mli 2855 1069150632 g/39_fair_bddd. 1.3)
(source/fair_bddd.mli 2892 1069319394 g/39_fair_bddd. 1.4)
(cuddaux/cuddauxAddIte.c 12812 1034006019 c/32_cuddauxAdd 1.1)
(source/gen_stubs_scade.mli 641 1055926783 f/6_gen_stubs_ 1.1)
(share/pixmaps/clean-up.xpm 1565 1055926783 f/22_clean-up.x 1.1)
......@@ -124,7 +124,7 @@
(share/lurettetop_sh.in 781 1063786164 g/24_lurettetop 1.1)
(mlcuddidl/manager.mli 7912 1034006019 c/46_manager.ml 1.1)
(share/pixmaps/run.xpm 369 1055926783 f/13_run.xpm 1.1)
(source/prevar.mli 1023 1063029729 d/19_prevar.mli 1.4)
(source/prevar.mli 1018 1069319394 d/19_prevar.mli 1.5)
(mlcuddidl/idd.mli 5470 1034006019 c/51_idd.mli 1.1)
(source/call_lurette_main.c 322 1050421093 e/28_call_luret 1.1)
(polka/C/vector.c 13780 1047029868 e/3_vector.c 1.1)
......@@ -139,7 +139,7 @@
(source/gen_stubs.ml 13933 1063029729 24_generate_l 1.50)
(polka/caml/vector.idl 8669 1047029868 d/35_vector.idl 1.1)
(mlcuddidl/README 1574 1034006019 d/8_README 1.1)
(source/sim2chro.mli 1547 1069150632 b/23_sim2chro.m 1.8)
(source/sim2chro.mli 1534 1069319394 b/23_sim2chro.m 1.9)
(share/lucky_init.csh.in 150 1063786164 e/23_lucky_init 1.8)
(source/lustreExp.ml 21223 1069150632 g/45_lustreExp. 1.1)
(source/gen_fake_lucky.ml 4631 1063786164 g/8_gen_fake_l 1.2)
......@@ -151,7 +151,7 @@
(mlcuddidl/manager.ml 8017 1034006019 c/47_manager.ml 1.1)
(share/plot 11416 1069150632 e/35_plot 1.5)
(share/pixmaps/save.xpm 867 1055926783 f/12_save.xpm 1.1)
(source/solver.mli 1510 1069150632 38_solver.mli 1.19)
(source/solver.mli 1554 1069319394 38_solver.mli 1.20)
(test/passerelle.luc 963 1063786164 b/17_passerelle 1.12)
(source/store.ml 35278 1069150632 b/27_rnumsolver 1.30)
(mlcuddidl/mtbdd.mli 4395 1034006019 c/43_mtbdd.mli 1.1)
......@@ -164,7 +164,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 4414 1063029729 b/38_Makefile.l 1.27)
(source/lucky.ml 8591 1069150632 16_env.ml 1.34)
(source/lucky.ml 10445 1069319394 16_env.ml 1.35)
(source/graph.mli 2339 1069150632 13_graph.mli 1.12)
(source/store.mli 3313 1069150632 b/26_rnumsolver 1.22)
(test/time-ossau.res 9334 1069150632 b/49_time.res 1.56)
......@@ -178,7 +178,7 @@
(cuddaux/Makefile 3326 1053337243 c/35_Makefile 1.7)
(polka/C/bit.c 3026 1047029868 e/10_bit.c 1.1)
(source/draw.mli 452 1065787303 f/1_draw.mli 1.2)
(test/time-ossau.exp 9556 1069150632 b/48_time.exp 1.52)
(test/time-ossau.exp 9334 1069319394 b/48_time.exp 1.53)
(polka/caml/polkaIO.ml 1652 1047029868 d/44_polkaIO.ml 1.1)
(mlcuddidl/macros.m4 11290 1034006019 c/49_macros.m4 1.1)
(source/print.ml 5904 1069150632 47_print.ml 1.25)
......@@ -191,24 +191,24 @@
(source/parse_c_scade.mli 656 1055487917 e/42_parse_c_sc 1.1)
(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 20964 1069150632 b/47_automata.m 1.16)
(source/run_aut.ml 21568 1069319394 b/47_automata.m 1.17)
(cuddaux/README 1427 1034006019 c/34_README 1.1)
(mlcuddidl/bdd.ml 10889 1034006019 d/6_bdd.ml 1.1)
(source/lurettetop.ml 47330 1065787303 c/1_lurettetop 1.42)
(source/lurettetop.ml 47330 1069319394 c/1_lurettetop 1.43)
(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 17305 1069150632 g/34_formula_to 1.2)
(source/formula_to_bdd.ml 17652 1069319394 g/34_formula_to 1.3)
(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)
(polka/caml/Makefile.depend 744 1063029729 d/32_Makefile.d 1.3)
(source/bddd.ml 16703 1069150632 g/36_bddd.ml 1.4)
(source/bddd.ml 17144 1069319394 g/36_bddd.ml 1.5)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(ihm/xlurette/xlurette_glade_interface.ml 76320 1065787303 c/15_xlurette_g 1.22)
(INSTALL 101 1056616700 f/26_INSTALL 1.2)
(test/cygwin-scade/MyConsts.saofd 153 1055926783 f/44_MyConsts.s 1.1)
(test/losange-3d2.luc 371 1066840252 e/32_losange-3d 1.5)
(test/Makefile 2729 1064411282 c/0_Makefile 1.14)
(user-rules 34447 1069150632 c/14_myrules 1.47)
(user-rules 34486 1069319394 c/14_myrules 1.48)
(test/infinite_weight.luc 889 1063786164 g/13_infinite_w 1.1)
(mlcuddidl/cudd_caml.c 22890 1034006019 d/3_cudd_caml. 1.1)
(polka/C/config.h 77 1047029868 e/13_config.h 1.1)
......@@ -236,14 +236,14 @@
(share/configure.in 8503 1064329011 d/11_configure. 1.14)
(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 3452 1069150632 b/46_automata.m 1.6)
(source/run_aut.mli 3575 1069319394 b/46_automata.m 1.7)
(polka/C/matrix.h 3461 1047029868 d/51_matrix.h 1.1)
(cuddaux/cuddaux.h 2381 1034006019 c/33_cuddaux.h 1.1)
(share/lurettetop.bat.in 672 1063786164 g/26_lurettetop 1.1)
(share/lucky.el 1934 1063786164 f/7_lucky.el 1.5)
(mlcuddidl/sedscript 203 1034006019 c/38_sedscript 1.1)
(test/cygwin-scade/.lurette_rc 551 1063029729 f/29_.lurette_r 1.2)
(source/env_state.mli 4208 1069150632 50_env_state. 1.35)
(source/env_state.mli 3307 1069319394 50_env_state. 1.36)
(test/ControleurPorte.rif.exp 4688 1065787303 b/29_Controleur 1.19)
(source/show_luc.ml 4292 1069150632 e/25_show_luc.m 1.7)
(share/pixmaps/quit.xpm 494 1055926783 f/14_quit.xpm 1.1)
......@@ -265,33 +265,33 @@
(test/test_losange.lus 88 1055926783 f/27_test_losan 1.1)
(mlcuddidl/bdd.mli 8573 1034006019 d/5_bdd.mli 1.1)
(test/cygwin-scade/compute_path.saofd 1662 1055926783 g/5_compute_pa 1.1)
(source/lucky.mli 1946 1069150632 15_env.mli 1.20)
(source/lucky.mli 1001 1069319394 15_env.mli 1.21)
(polka/C/polka.h 1478 1047029868 d/50_polka.h 1.1)
(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 285 1069150632 e/37_time-mouch 1.10)
(source/command_line_luc_exe.ml 3832 1065787303 b/33_command_li 1.19)
(test/time-moucherotte.exp 4857 1069319394 e/37_time-mouch 1.11)
(source/command_line_luc_exe.ml 3812 1069319394 b/33_command_li 1.20)
(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 1069150632 d/20_time-ecrin 1.31)
(test/time-ecrins.res 9333 1069319394 d/20_time-ecrin 1.32)
(source/value.mli 1172 1069150632 c/24_value.mli 1.5)
(polka/Makefile.config 1683 1053337243 e/20_Makefile.c 1.5)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
(source/Makefile 9349 1069150632 c/20_Makefile 1.25)
(source/Makefile 9476 1069319394 c/20_Makefile 1.26)
(source/graph.ml 3494 1069150632 14_graph.ml 1.10)
(test/cudd_gc_problem.luc 208372 1063029729 e/29_cudd_gc_pr 1.2)
(test/time-CHAILLOL.exp 8235 1063029729 g/10_time-CHAIL 1.1)
(demo-xlurette/chaudiere/chaudiere_ctrl.lus 178 1063786164 c/9_chaudiere_ 1.2)
(test/losange-3d.rif.exp 27445 1066840252 e/31_losange-3d 1.5)
(polka/documentation/Makefile 476 1047029868 e/18_Makefile 1.1)
(source/sim2chro.ml 3110 1069150632 b/24_sim2chro.m 1.21)
(source/sim2chro.ml 3105 1069319394 b/24_sim2chro.m 1.22)
(source/poly_draw.ml 22086 1069150632 g/43_polyDraw.m 1.2)
(cuddaux/cuddauxTDGenCof.c 15712 1034006019 c/26_cuddauxTDG 1.1)
(source/luc_exe.ml 14927 1069150632 b/32_ima_exe.ml 1.39)
(source/luc_exe.ml 13915 1069319394 b/32_ima_exe.ml 1.40)
(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 20146 1069150632 12_lurette.ml 1.77)
(source/lurette.ml 18576 1069319394 12_lurette.ml 1.78)
(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)
......@@ -302,7 +302,7 @@
(source/gen_fake_lutin.ml 4709 1055487917 d/16_gen_fake_l 1.5)
(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 1221 1069150632 g/35_formula_to 1.3)
(source/formula_to_bdd.mli 1298 1069319394 g/35_formula_to 1.4)
(polka/Makefile 1636 1047029868 e/21_Makefile 1.1)
(test/dynamic_weight.luc 563 1063786164 g/14_dynamic_we 1.1)
(source/var.ml 5291 1069150632 g/49_var.ml 1.1)
......
TODO
View file @ 540ee1f9
......@@ -12,8 +12,14 @@ par les poids sont un peu contre-intuitives.
pas satisfaisant : pleins de polyhedres intermediaires inutiles
sont calcules, selon l'ordre dans lequel arrivent les contraintes...
* Le remplacement dynaique de .luc est tres surement cassé (les current_nodes
ne sont pas mis a jour)
****** Documentation
* il faut rajouter dans lurette une option --step-inside --step-edges
--step-vertices (et renommer --draw-inside par --try-inside ??)
* Rajouter un mode ecexe dans lurette
* documenter les options ~default, ~alias, etc.
......
lurette.prj
View file @ 540ee1f9
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 1 9)
(Parent-Version lurette 1 8)
(Project-Version lurette 1 10)
(Parent-Version lurette 1 9)
(Version-Log "
A lot (too much...) of changes, mainly renaming files, and types, and functions,
change the interface, move from one module to another, etc.
removing of Env_state module -- part 1
Bref, a lot of cleanning.
Now env_step and env_try are fully functionnal (no side-effects).
")
(New-Version-Log ""
)
(Checkin-Time "Tue, 18 Nov 2003 11:17:12 +0100")
(Checkin-Time "Thu, 20 Nov 2003 10:09:54 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -24,14 +23,14 @@ Bref, a lot of cleanning.
;; Sources files for luc_exe
(source/luc_exe.mli (lurette/b/31_ima_exe.ml 1.3 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.39 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.40 644))
(source/command_line_luc_exe.ml (lurette/b/33_command_li 1.19 644))
(source/command_line_luc_exe.mli (lurette/b/34_command_li 1.12 644))
(source/command_line_luc_exe.ml (lurette/b/33_command_li 1.20 644))
(source/command_line_luc_exe.mli (lurette/b/34_command_li 1.13 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.14 644))
(source/lurette.ml (lurette/12_lurette.ml 1.77 644))
(source/lurette.ml (lurette/12_lurette.ml 1.78 644))
(source/command_line.ml (lurette/b/20_command_li 1.16 644))
(source/command_line.mli (lurette/b/21_command_li 1.13 644))
......@@ -40,21 +39,21 @@ Bref, a lot of cleanning.
(source/graph.mli (lurette/13_graph.mli 1.12 644))
(source/graph.ml (lurette/14_graph.ml 1.10 644))
(source/lucky.mli (lurette/15_env.mli 1.20 644))
(source/lucky.ml (lurette/16_env.ml 1.34 644))
(source/lucky.mli (lurette/15_env.mli 1.21 644))
(source/lucky.ml (lurette/16_env.ml 1.35 644))
(source/util.ml (lurette/35_util.ml 1.58 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.2 644))
(source/formula_to_bdd.mli (lurette/g/35_formula_to 1.3 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.3 644))
(source/formula_to_bdd.mli (lurette/g/35_formula_to 1.4 644))
(source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.3 644))
(source/fair_bddd.mli (lurette/g/39_fair_bddd. 1.3 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.4 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.4 644))
(source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.4 644))
(source/fair_bddd.mli (lurette/g/39_fair_bddd. 1.4 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.5 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.5 644))
(source/solver.mli (lurette/38_solver.mli 1.19 644))
(source/solver.ml (lurette/39_solver.ml 1.57 644))
(source/solver.mli (lurette/38_solver.mli 1.20 644))
(source/solver.ml (lurette/39_solver.ml 1.58 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.11 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.6 644))
......@@ -71,19 +70,19 @@ Bref, a lot of cleanning.
(source/print.mli (lurette/46_print.mli 1.14 644))
(source/print.ml (lurette/47_print.ml 1.25 644))
(source/env_state.mli (lurette/50_env_state. 1.35 644))
(source/env_state.ml (lurette/51_env_state. 1.50 644))
(source/env_state.mli (lurette/50_env_state. 1.36 644))
(source/env_state.ml (lurette/51_env_state. 1.51 644))
(source/run_aut.mli (lurette/b/46_automata.m 1.6 644))
(source/run_aut.ml (lurette/b/47_automata.m 1.16 644))
(source/run_aut.mli (lurette/b/46_automata.m 1.7 644))
(source/run_aut.ml (lurette/b/47_automata.m 1.17 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.8 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.21 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.9 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.22 644))
(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.42 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.43 644))
(source/draw.mli (lurette/f/1_draw.mli 1.2 644))
(source/draw.ml (lurette/f/2_draw.ml 1.3 644))
......@@ -111,7 +110,7 @@ Bref, a lot of cleanning.
(source/value.mli (lurette/c/24_value.mli 1.5 644))
(source/prevar.ml (lurette/d/18_prevar.ml 1.4 644))
(source/prevar.mli (lurette/d/19_prevar.mli 1.4 644))
(source/prevar.mli (lurette/d/19_prevar.mli 1.5 644))
(source/parse_poc.ml (lurette/d/15_parse_poc. 1.4 644))
(source/parse_poc.mli (lurette/d/29_parse_poc. 1.2 644))
......@@ -148,7 +147,7 @@ Bref, a lot of cleanning.
(Makefile.common.source (lurette/e/33_Makefile.c 1.7 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.51 644))
(share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.27 644))
(user-rules (lurette/c/14_myrules 1.47 644))
(user-rules (lurette/c/14_myrules 1.48 644))
(share/Makefile.test.in (lurette/c/25_user-rules 1.10 644))
(Makefile (lurette/d/13_Makefile 1.4 644))
......@@ -158,7 +157,7 @@ Bref, a lot of cleanning.
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.27 644))
(source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.8 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.25 644))
(source/Makefile (lurette/c/20_Makefile 1.25 644))
(source/Makefile (lurette/c/20_Makefile 1.26 644))
;; Documentation
(doc/Interface_draft (lurette/19_Interface_ 1.1 644))
......@@ -173,18 +172,18 @@ Bref, a lot of cleanning.
(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.28 644))
(TODO (lurette/d/22_TODO 1.29 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.11 644))
(share/gnuplot-rif (lurette/e/34_gnuplot-ri 1.5 744))
(share/plot (lurette/e/35_plot 1.5 744))
(test/time-ossau.exp (lurette/b/48_time.exp 1.52 644))
(test/time-ossau.exp (lurette/b/48_time.exp 1.53 644))
(test/time-ossau.res (lurette/b/49_time.res 1.56 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.31 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.30 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.10 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.32 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.31 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.11 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.11 644))
;; Various files used for testing purposes
......
source/Makefile
View file @ 540ee1f9
......@@ -142,6 +142,10 @@ libnc:
make nc -f Makefile.lurette_lib OCAMLFLAGS="-noassert -unsafe"
rm -f liblurette_lib_nc.a
make liblurette_lib_nc.a
libncnc:
make nc -f Makefile.lurette_lib OCAMLFLAGS="-noassert -unsafe"
rm -f liblurette_lib_nc.a
make liblurette_lib_nc.a
libnc_assert:
make clean -f Makefile.lurette_lib
......
source/bddd.ml
View file @ 540ee1f9
......@@ -19,7 +19,7 @@ open Exp
open Value
open Constraint
open Store
open Env_state
type var_idx = int
......@@ -67,11 +67,9 @@ let (add_snt_entry : Bdd.t -> sol_nb * sol_nb -> unit) =
let (init_snt : unit -> unit) =
fun _ ->
let fake_env_in = (Hashtbl.create 0) in
(Hashtbl.add
!snt_ref (Formula_to_bdd.f fake_env_in True) (1.0, 0.0));
(Hashtbl.add
!snt_ref (Formula_to_bdd.f fake_env_in True) (0.0, 1.0))
let bdd_true = Bdd.dtrue !Formula_to_bdd.bdd_manager in
(Hashtbl.add !snt_ref (bdd_true) (1.0, 0.0));
(Hashtbl.add !snt_ref (bdd_true) (0.0, 1.0))
let (clear_snt: unit -> unit) =
fun _ ->
......@@ -209,8 +207,8 @@ let (toss_up_one_var: Var.name -> Var.subst) =
if (ran < 0.5) then (var, B(true)) else (var, B(false))
let (toss_up_one_var_index: var_idx -> Var.subst option) =
fun var_idx ->
let (toss_up_one_var_index: Var.env_in -> Env_state.lucky_state -> var_idx -> Var.subst option) =
fun input state var_idx ->
(* if [var_idx] is a index that corresponds to a boolean variable,
this fonction performs a toss and returns a substitution for
the corresponding boolean variable. It returns [None]
......@@ -225,7 +223,7 @@ let (toss_up_one_var_index: var_idx -> Var.subst option) =
Bv(v) -> (
match (Var.default v) with
Some (Formu f) ->
let bdd = Formula_to_bdd.f (Env_state.input ()) f in
let bdd = Formula_to_bdd.f input state f in
if Bdd.is_false bdd then Some((Var.name v), B false)
else if Bdd.is_true bdd then Some((Var.name v), B true)
else
......@@ -244,9 +242,9 @@ let (toss_up_one_var_index: var_idx -> Var.subst option) =
| _ -> None
let rec (draw_in_bdd_rec: Var.subst list * Store.t -> Bdd.t -> Bdd.t ->
Var.subst list * Store.t' * Store.p) =
fun (sl, store) bdd comb ->
let rec (draw_in_bdd_rec: Var.env_in -> Env_state.lucky_state -> Var.subst list * Store.t -> Bdd.t ->
Bdd.t -> Var.subst list * Store.t' * Store.p) =
fun input state (sl, store) bdd comb ->
(** Returns [sl] appended to a draw of all the boolean variables
bigger than the topvar of [bdd] according to the ordering
induced by the comb [comb]. Also returns the (non empty) store
......@@ -269,7 +267,7 @@ let rec (draw_in_bdd_rec: Var.subst list * Store.t -> Bdd.t -> Bdd.t ->
(
(List.append sl
(Util.list_map_option
toss_up_one_var_index
(toss_up_one_var_index input state)
(Bdd.list_of_support comb))
),
store_int,
......@@ -282,16 +280,16 @@ let rec (draw_in_bdd_rec: Var.subst list * Store.t -> Bdd.t -> Bdd.t ->
let cstr = (Formula_to_bdd.index_to_linear_constraint bddvar) in
match cstr with
| Bv(var) ->
draw_in_bdd_rec_bool var (sl, store) bdd comb snt
draw_in_bdd_rec_bool input state var (sl, store) bdd comb snt
| EqZ(e) ->
draw_in_bdd_rec_eq e (sl, store) bdd comb snt
draw_in_bdd_rec_eq input state e (sl, store) bdd comb snt
| Ineq(ineq) ->
draw_in_bdd_rec_ineq ineq (sl, store) bdd comb snt
draw_in_bdd_rec_ineq input state ineq (sl, store) bdd comb snt
and (draw_in_bdd_rec_bool: var -> Var.subst list * Store.t -> Bdd.t -> Bdd.t ->
snt -> Var.subst list * Store.t' * Store.p) =
fun var (sl, store) bdd comb snt ->
and (draw_in_bdd_rec_bool: Var.env_in -> Env_state.lucky_state -> var -> Var.subst list * Store.t ->
Bdd.t -> Bdd.t -> snt -> Var.subst list * Store.t' * Store.p) =
fun input state var (sl, store) bdd comb snt ->
let bddvar = Bdd.topvar bdd in
let topvar_comb = Bdd.topvar comb in
......@@ -302,11 +300,11 @@ and (draw_in_bdd_rec_bool: var -> Var.subst list * Store.t -> Bdd.t -> Bdd.t ->
boolean var; hence we toss it up, or we compute its default
value (cf "~default" flag). *)
let new_sl =
match toss_up_one_var_index topvar_comb with
match toss_up_one_var_index input state topvar_comb with
Some(s) -> s::sl
| None -> sl
in
draw_in_bdd_rec (new_sl, store) bdd (Bdd.dthen comb)
draw_in_bdd_rec input state (new_sl, store) bdd (Bdd.dthen comb)
else
(* bddvar = combvar *)
let (n, m) = sol_number_snt snt bdd in
......@@ -349,13 +347,13 @@ and (draw_in_bdd_rec_bool: var -> Var.subst list * Store.t -> Bdd.t -> Bdd.t ->
[res_opt] is bound to [None].
*)
try
draw_in_bdd_rec (sl1, store) bdd1 new_comb
draw_in_bdd_rec input state (sl1, store) bdd1 new_comb
with
No_numeric_solution ->
if Env_state.verbose () then
if state.verbose then
print_string "\n..................BACKTRACK!\n";
if not (eq_sol_nb sol_nb2 zero_sol)
then draw_in_bdd_rec (sl2, store) bdd2 new_comb
then draw_in_bdd_rec input state (sl2, store) bdd2 new_comb
(*
The second branch is now tried because no path in
the first bdd leaded to a satisfiable set of
......@@ -367,9 +365,10 @@ and (draw_in_bdd_rec_bool: var -> Var.subst list * Store.t -> Bdd.t -> Bdd.t ->
flush stdout;
assert false
and (draw_in_bdd_rec_ineq: Constraint.ineq -> Var.subst list * Store.t -> Bdd.t ->
and (draw_in_bdd_rec_ineq: Var.env_in -> Env_state.lucky_state -> Constraint.ineq ->
Var.subst list * Store.t -> Bdd.t ->
Bdd.t -> snt -> Var.subst list * Store.t' * Store.p) =
fun cstr (sl, store) bdd comb snt ->
fun input state cstr (sl, store) bdd comb snt ->
(*
When we add to the store an inequality constraint GZ(ne) or
GeqZ(ne) ([split_store]), 2 stores are returned. The first is a
......@@ -404,7 +403,7 @@ and (draw_in_bdd_rec_ineq: Constraint.ineq -> Var.subst list * Store.t -> Bdd.t
try
if not (is_store_satisfiable store1) then raise No_numeric_solution;
draw_in_bdd_rec (sl, store1) bdd1 comb
draw_in_bdd_rec input state (sl, store1) bdd1 comb
with
No_numeric_solution ->
let store2 = add_constraint store (Ineq cstr2) in
......@@ -417,7 +416,7 @@ and (draw_in_bdd_rec_ineq: Constraint.ineq -> Var.subst list * Store.t -> Bdd.t
(not (eq_sol_nb sol_nb2 zero_sol))
&& is_store_satisfiable store2
then
draw_in_bdd_rec (sl, store2) bdd2 comb
draw_in_bdd_rec input state (sl, store2) bdd2 comb
else
raise No_numeric_solution
| e ->
......@@ -425,9 +424,9 @@ and (draw_in_bdd_rec_ineq: Constraint.ineq -> Var.subst list * Store.t -> Bdd.t
flush stdout;
assert false
and (draw_in_bdd_rec_eq: Ne.t -> Var.subst list * Store.t -> Bdd.t -> Bdd.t -> snt ->
Var.subst list * Store.t' * Store.p) =
fun ne (sl, store) bdd comb snt ->
and (draw_in_bdd_rec_eq: Var.env_in -> Env_state.lucky_state -> Ne.t -> Var.subst list * Store.t ->
Bdd.t -> Bdd.t -> snt -> Var.subst list * Store.t' * Store.p) =
fun input state ne (sl, store) bdd comb snt ->
(*
We consider 3 stores:
- store + [ne = 0]
......@@ -506,7 +505,7 @@ and (draw_in_bdd_rec_eq: Ne.t -> Var.subst list * Store.t -> Bdd.t -> Bdd.t -> s
(not (is_store_satisfiable store1)) || (sol_nb1 = 0.0)
then
raise No_numeric_solution;
draw_in_bdd_rec (sl, store1) bdd1 comb
draw_in_bdd_rec input state (sl, store1) bdd1 comb
with
No_numeric_solution ->
(*
......@@ -519,7 +518,7 @@ and (draw_in_bdd_rec_eq: Ne.t -> Var.subst list * Store.t -> Bdd.t -> Bdd.t -> s
(not (is_store_satisfiable store2)) || (sol_nb2 = 0.0)
then
raise No_numeric_solution;
draw_in_bdd_rec (sl, store2) bdd2 comb
draw_in_bdd_rec input state (sl, store2) bdd2 comb
with
No_numeric_solution ->
let store3 = add_constraint store cstr3 in
......@@ -527,7 +526,7 @@ and (draw_in_bdd_rec_eq: Ne.t -> Var.subst list * Store.t -> Bdd.t -> Bdd.t -> s
(not (is_store_satisfiable store3)) || (sol_nb3 = 0.0)
then
raise No_numeric_solution;
draw_in_bdd_rec (sl, store3) bdd3 comb
draw_in_bdd_rec input state (sl, store3) bdd3 comb
| e ->
print_string ((Printexc.to_string e) ^ "\n");
flush stdout;
......@@ -535,7 +534,7 @@ and (draw_in_bdd_rec_eq: Ne.t -> Var.subst list * Store.t -> Bdd.t -> Bdd.t -> s
(* exported *)
let rec (draw_in_bdd: var list -> Bdd.t -> Bdd.t ->
let rec (draw_in_bdd: Var.env_in -> Env_state.lucky_state -> var list -> Bdd.t -> Bdd.t ->
Var.subst list * Store.t' * Store.p) =
fun store bdd comb ->
draw_in_bdd_rec ([], Store.create store) bdd comb
fun input state store bdd comb ->
draw_in_bdd_rec input state ([], Store.create store) bdd comb
source/bddd.mli
View file @ 540ee1f9
......@@ -21,8 +21,8 @@ val build_sol_nb_table : Exp.var list -> Bdd.t -> Bdd.t -> unit
variable to be generated (which migth not appear in [bdd]).
*)
val draw_in_bdd : Exp.var list -> Bdd.t -> Bdd.t ->
Var.subst list * Store.t' * Store.p
val draw_in_bdd : Var.env_in -> Env_state.lucky_state -> Exp.var list -> Bdd.t ->
Bdd.t -> Var.subst list * Store.t' * Store.p
(**
[draw_in_bdd varl bdd comb] returns a draw of the Boolean variables
as well as a range base and a polyhedron based representation of
......
source/command_line_luc_exe.ml
View file @ 540ee1f9
......@@ -9,16 +9,16 @@
*)
type draw_mode = | DmInside | DmEdges | DmVertices
type optionsT = {
mutable show_automata : bool ;
mutable boot : bool ;
mutable max_step_number : int option ;
mutable locals : bool ;
mutable draw_mode : draw_mode ;
mutable draw_mode : Lucky.step_mode ;
mutable compute_volume : bool;
mutable user_seed : int
mutable user_seed : int ;
mutable verbose : bool
}
type cmd_line_optionT =
......
source/command_line_luc_exe.mli
View file @ 540ee1f9
......@@ -11,16 +11,16 @@
(** Handles everything that is related to command line calls.
*)
type draw_mode = | DmInside | DmEdges | DmVertices
type optionsT = {
mutable show_automata : bool ;
mutable boot : bool ;
mutable max_step_number : int option ;
mutable locals : bool ;
mutable draw_mode : draw_mode ;
mutable draw_mode : Lucky.step_mode ;
mutable compute_volume : bool;
mutable user_seed : int
mutable user_seed : int ;
mutable verbose : bool
}
val usage : string
......
source/env_state.ml
View file @ 540ee1f9
......@@ -17,18 +17,23 @@ open Graph
(****************************************************************************)
type memory_box = string
type env_stateT = {