Commit 135fe2d5 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.69 Fri, 19 Jul 2002 10:19:59 +0200 by jahier

Parent-Version:      0.68
Version-Log:

wtree.ml,mli:   (deleted)
automa.ml,mli:  (new files)
control.ml,mli: (new files)

   Replace the [wtree] module by an [automata] module, that basically
   does the same job, but in a different way. Namely, it no more uses
   the [wtree] DS to use [graph]s instead.  Indeed, the product of
   wtrees introduces some problems, in particular to ensure its
   correctness wrt to the automata run concurrently. Now, everything a
   dead-simple wrt product: we simply perform a quasi-classical automata
   product (well, at least, much closer from a classical product, cf
   paper).

   The way loop counters are handled has also changed. Now, counters are
   handled via expressions of a simple arithmetic language that
   basically lets one initialise a variable to an exact or a random
   value (uniform or normal draw) and decrement it. Arcs are now
   labelled by a formula plus 2 expressions of that mini-language (no
   more weigth nor cpt_init stuff). The 1st expression is evaluated
   during the draw, basically performs any operations on counters, and
   returns a positive int that is used as the formula weigth. The second
   expression (a kind of post-condition) is evaluated if its arc is the
   one that has been elected to perform the step.

At several locations long lines (< 80) are reindented.

parse_env.ml:
   In the ima format, IfThenElseExpr becomes IfThenElseNum.
   Also, parse list more cleanly.

graph.ml,mli:
    Add a function that test whether a transition is in the graph.

    Do not sort list of transitions anymore (what was the point?).
    Also do not sort nodes in any way.

show_env_env.ml,mli:
   Abstract away nodes and arcs data types (so that I can display
   Automata graphs). rename generate_env_graph into ima_to_dot.

lurette.ml:
ima_exe.ml:
   Fix a bug where bbd table were filled by asserted non regression expr.

lurette.ml:
   Fix a bug where incorrect data was sent to sim2chro (ie, the output of the
   previous step instead of the ones of the current step.

env_state.ml:
solver.ml:
gne.ml:
   Fix a performance bug where I was storing formula indexes even if
   they were depending on inputs or pre, which is stupid as they generally
   won't be used again. In order to fix that, I introduced  new
   atomic_formula <-> indexes table to stote the ones that do not depend
   on inputs apart. It was also necassery to propogate the <<depend on pre>>
   flag inside Gne.gn_expr (which i renamed Gne.t BTW).

Project-Description: Lurette
parent 8c24cdb7
;; This file is automatically generated, editing may cause PRCS to do
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(test/usager.env 523 1019479246 b/14_usager.env 1.7)
(test/usager.env 493 1027066799 b/14_usager.env 1.8)
(source/command_line_ima_exe.mli 1082 1021651153 b/34_command_li 1.3)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 13591 1021651153 51_env_state. 1.22)
(source/graph.ml 1822 1021539278 14_graph.ml 1.6)
(bin/Makefile.ima_exe 1926 1020420514 b/41_Makefile.i 1.2)
(source/util.ml 13368 1021041152 35_util.ml 1.20)
(source/wtree.ml 13340 1021539278 b/1_wtree.ml 1.13)
(source/solver.ml 24391 1021539278 39_solver.ml 1.22)
(source/env_state.ml 18696 1027066799 51_env_state. 1.23)
(source/graph.ml 2563 1027066799 14_graph.ml 1.7)
(bin/Makefile.ima_exe 2013 1027066799 b/41_Makefile.i 1.3)
(source/util.ml 13725 1027066799 35_util.ml 1.21)
(test/time.exp 5583 1027066799 b/48_time.exp 1.1)
(source/solver.ml 24576 1027066799 39_solver.ml 1.23)
(test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1)
(source/command_line.ml 4388 1019207707 b/20_command_li 1.7)
(source/lurette.ml 12133 1021651153 12_lurette.ml 1.39)
(source/solver.mli 1138 1020432102 38_solver.mli 1.11)
(source/env.mli 2077 1020420514 15_env.mli 1.13)
(test/heater_float.rif.exp 1461 1015514807 b/30_heater_flo 1.2)
(source/lurette.ml 12622 1027066799 12_lurette.ml 1.40)
(test/temp_int.env 647 1027066799 b/50_temp_int.e 1.1)
(source/solver.mli 1071 1027066799 38_solver.mli 1.12)
(source/env.mli 2024 1027066799 15_env.mli 1.14)
(test/heater_float.rif.exp 1453 1027066799 b/30_heater_flo 1.3)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 8348 1021539278 16_env.ml 1.27)
(make_lurette 1242 1020420514 27_make_luret 1.12)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(source/env.ml 8305 1027066799 16_env.ml 1.28)
(make_lurette 1243 1027066799 27_make_luret 1.13)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(test/passerelle.env 1105 1019479246 b/17_passerelle 1.6)
(test/passerelle.env 972 1027066799 b/17_passerelle 1.7)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/rnumsolver.ml 10783 1017837703 b/27_rnumsolver 1.6)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/parse_env.mli 906 1021651153 40_parse_env. 1.8)
(source/parse_env.mli 1025 1027066799 40_parse_env. 1.9)
(source/sim2chro.mli 1429 1017929190 b/23_sim2chro.m 1.4)
(source/ima_exe.ml 11622 1021651153 b/32_ima_exe.ml 1.12)
(source/ima_exe.ml 12058 1027066799 b/32_ima_exe.ml 1.13)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7749 1016803757 49_eval.ml 1.12)
(source/eval.ml 7755 1027066799 49_eval.ml 1.13)
(source/gen_stubs.ml 36621 1021042464 24_generate_l 1.26)
(source/parse_env.ml 18459 1021041152 41_parse_env. 1.19)
(source/parse_env.ml 22104 1027066799 41_parse_env. 1.20)
(test/temp_float.env 719 1027066799 b/51_temp_float 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/automata.mli 3395 1027066799 b/46_automata.m 1.1)
(source/sim2chro.ml 2653 1020777170 b/24_sim2chro.m 1.8)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 3640 1021041152 44_formula.ml 1.13)
(source/formula.mli 3638 1027066799 44_formula.ml 1.14)
(test/time.res 5578 1027066799 b/49_time.res 1.1)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/command_line.mli 1421 1017929190 b/21_command_li 1.6)
(source/wtree.mli 3320 1021539278 b/0_wtree.mli 1.11)
(test/porte.env 1130 1019479246 b/16_porte.env 1.6)
(source/env_state.mli 5986 1021651153 50_env_state. 1.19)
(test/porte.env 1021 1027066799 b/16_porte.env 1.7)
(source/env_state.mli 6423 1027066799 50_env_state. 1.20)
(source/rnumsolver.mli 1764 1017335442 b/26_rnumsolver 1.3)
(source/ima_exe.mli 447 1016127950 b/31_ima_exe.ml 1.1)
(source/eval.mli 1389 1016803757 48_eval.mli 1.9)
(source/eval.mli 1395 1027066799 48_eval.mli 1.10)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 22550 1021041152 17_OcamlMakef 1.29)
(OcamlMakefile 24344 1027066799 17_OcamlMakef 1.30)
(source/command_line_ima_exe.ml 2792 1021651153 b/33_command_li 1.4)
(test/ControleurPorte.rif.exp 4746 1016803757 b/29_Controleur 1.4)
(test/tram.env 1149 1019479246 b/15_tram.env 1.6)
(Makefile.lurette 1866 1020420514 b/38_Makefile.l 1.3)
(source/show_env.ml 3768 1021651153 43_show_env.m 1.9)
(source/gne.mli 1107 1016803757 b/36_gne.mli 1.1)
(test/ControleurPorte.rif.exp 4756 1027066799 b/29_Controleur 1.5)
(test/tram.env 1038 1027066799 b/15_tram.env 1.7)
(Makefile.lurette 1953 1027066799 b/38_Makefile.l 1.4)
(source/show_env.ml 3629 1027066799 43_show_env.m 1.10)
(source/gne.mli 1079 1027066799 b/36_gne.mli 1.2)
(source/automata.ml 14972 1027066799 b/47_automata.m 1.1)
(bin/Makefile.gen_stubs 467 1020068208 b/42_Makefile.g 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
(source/show_env.mli 775 1020432102 42_show_env.m 1.6)
(source/gne.ml 8204 1016803757 b/37_gne.ml 1.1)
(source/show_env.mli 1091 1027066799 42_show_env.m 1.7)
(test/Makefile 146 1027066799 c/0_Makefile 1.1)
(source/gne.ml 8173 1027066799 b/37_gne.ml 1.2)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(test/heater_float.lus 175 1020068208 b/44_heater_flo 1.1)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 844 1021041152 46_print.mli 1.9)
(test/vrai_tram.c 3060 1027066799 b/8_vrai_tram. 1.3)
(source/print.mli 773 1027066799 46_print.mli 1.10)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(source/graph.mli 1494 1021539278 13_graph.mli 1.8)
(test/heater_int.rif.exp 858 1017837703 b/28_heater_int 1.2)
(source/formula.ml 7387 1021041152 45_formula.ml 1.15)
(source/graph.mli 2218 1027066799 13_graph.mli 1.9)
(test/heater_int.rif.exp 857 1027066799 b/28_heater_int 1.3)
(source/formula.ml 7287 1027066799 45_formula.ml 1.16)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/print.ml 6771 1021041152 47_print.ml 1.16)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
(bin/Makefile.show_ima 958 1020432102 b/40_Makefile.s 1.3)
(source/print.ml 5954 1027066799 47_print.ml 1.17)
(test/vrai_tram.h 2468 1027066799 b/7_vrai_tram. 1.3)
(bin/Makefile.show_ima 1039 1027066799 b/40_Makefile.s 1.4)
......@@ -29,13 +29,14 @@ SOURCES_OCAML = \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/control.mli $(LURETTE_PATH)/source/control.ml \
$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/rnumsolver.mli $(LURETTE_PATH)/source/rnumsolver.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/wtree.mli $(LURETTE_PATH)/source/wtree.ml \
$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/automata.mli $(LURETTE_PATH)/source/automata.ml \
$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/sim2chro.mli $(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/env.mli $(LURETTE_PATH)/source/env.ml \
lurette_stub.ml \
......
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.29 Fri, 10 May 2002 16:32:32 +0200 jahier $
# $Id: OcamlMakefile 1.30 Fri, 19 Jul 2002 10:19:59 +0200 jahier $
#
###########################################################################
# Set these variables to the names of the sources to be processed and
......@@ -493,28 +493,54 @@ dot:
try:
../make_lurette ControleurPorte vrai_tram; \
lustre tram_oracle.lus tram_oracle ; \
ec2c tram_oracle.ec ; \
../make_lurette ControleurPorte tram_oracle; \
./lurette 10 2 2 tram.env usager.env porte.env passerelle.env
yvan:
$(LURETTE_PATH)/make_lurette heater Heater_vrai; \
./lurette 50 1 1 Heater.env \
vroum:
../make_lurette ControleurPorte vrai_tram nc; \
time ./lurette 4500 1 1 tram.env usager.env porte.env passerelle.env -seed 1015403953 -ns2c --no-oracle
time:
make clean; ../make_lurette ControleurPorte vrai_tram nc; \
\rm -f time.res; touch time.res ; \
/usr/bin/time -o time.res -a -v ./lurette 10000 1 1 tram.env usager.env porte.env \
passerelle.env -seed 1015403953 -ns2c --no-oracle ;\
echo " " >> time.res;\
/usr/bin/time -o time.res -a -v ./lurette 10 100 100 tram.env usager.env porte.env \
passerelle.env -seed 1015403953 -ns2c --no-oracle ;\
echo " " >> time.res;\
/usr/bin/time -o time.res -a -v ./lurette 100 50 50 tram.env usager.env porte.env \
passerelle.env -seed 1015403953 -ns2c --no-oracle ;\
echo " " >> time.res;\
../make_lurette heater_float always_true_heaterf nc; \
/usr/bin/time -o time.res -a -v ./lurette 10000 1 1 temp_float.env -seed 1015403953 \
-ns2c --no-oracle ;\
echo " " >> time.res;\
/usr/bin/time -o time.res -a -v ./lurette 10 100 100 temp_float.env -seed 1015403953 \
-ns2c --no-oracle ;\
echo " " >> time.res;\
../make_lurette heater_int always_true_heater nc; \
/usr/bin/time -o time.res -a -v ./lurette 10000 1 1 temp_int.env -seed 1015403953 \
-ns2c --no-oracle ;\
echo " " >> time.res;\
/usr/bin/time -o time.res -a -v ./lurette 10 100 100 temp_int.env -seed 1015403953 \
-ns2c --no-oracle ;\
\rm -f time.diff; diff -u time.exp time.res >> time.diff; cat time.diff
# Non regression test
test:
$(LURETTE_PATH)/make_lurette ControleurPorte; rm -f tram.rif; touch tram.rif; \
../make_lurette ControleurPorte; rm -f tram.rif; touch tram.rif; \
./lurette 100 10 10 -o tram.rif tram.env usager.env porte.env passerelle.env -seed 1013219512 -ns2c ;\
diff -u ControleurPorte.rif.exp tram.rif > test1.res ;\
\
$(LURETTE_PATH)/make_lurette heater_int; rm -f heater_int.rif; touch heater_int.rif; \
../make_lurette heater_int; rm -f heater_int.rif; touch heater_int.rif; \
./lurette 30 10 10 temp_int.env --no-oracle -seed 1013219512 -ns2c -o heater_int.rif ;\
diff -u heater_int.rif.exp heater_int.rif > test2.res ; \
\
$(LURETTE_PATH)/make_lurette heater_float; rm -f heater_float.rif; touch heater_float.rif; \
../make_lurette heater_float; rm -f heater_float.rif; touch heater_float.rif; \
./lurette 30 10 10 temp_float.env --no-oracle -seed 1013219512 -ns2c -o heater_float.rif;\
diff -u heater_float.rif.exp heater_float.rif > test3.res ; \
\
......@@ -524,10 +550,10 @@ ima:
pushd ~/lurette/bin ; make -k dc -f Makefile.ima_exe OCAMLFLAGS=""; popd
ima_nc:
pushd ~/lurette/bin ; make -k clean -f Makefile.ima_exe ; make -k nc -f Makefile.ima_exe ; popd
pushd ~/lurette/bin ; make -k clean -f Makefile.ima_exe ; make -k nc -f Makefile.ima_exe OCAMLFLAGS="-noassert -unsafe"; popd
show:
pushd ~/lurette/bin ; make -k dc -f Makefile.sho_ima OCAMLFLAGS=""; popd
pushd ~/lurette/bin ; make -k dc -f Makefile.show_ima OCAMLFLAGS=""; popd
heater:
$(LURETTE_PATH)/make_lurette heater_int; \
......@@ -540,16 +566,28 @@ heaterf:
# In order to time profile lurette
gprof:
$(LURETTE_PATH)/make_lurette ControleurPorte vrai_tram pnc; \
./lurette 4500 1 1 tram.env usager.env porte.env passerelle.env -seed 1014422484 -ns2c ;\
./lurette 10000 1 1 tram.env usager.env porte.env passerelle.env -seed 1014422484 -ns2c ;\
gprof ./lurette > lurette.gprof ; \
echo " ---> The result of the profiling is in the lurette.gprof file"
gprof2:
make clean; ../make_lurette heater_float always_true_heaterf pnc; \
./lurette 10000 1 1 temp_float.env -seed 1015403953 \
-ns2c --no-oracle ;\
gprof ./lurette > lurette.gprof2 ; \
echo " ---> The result of the profiling is in the lurette.gprof file"
gprof3:
make clean; $(LURETTE_PATH)/make_lurette heater_float always_true_heaterf pnc; \
./lurette 1000 1 1 temp_float.env -seed 1015403953 \
-ns2c --no-oracle ;\
gprof ./lurette > lurette.gprof3 ; \
echo " ---> The result of the profiling is in the lurette.gprof file"
# In order to time profile lurette
ocamlprof:
$(LURETTE_PATH)/make_lurette heater_float vrai_heater_float pbc; \
./lurette 10 10 10 temp_float.env -ns2c ;\
ocamlprof ../source/solver.ml > prof/solver.count.ml ; \
ocamlprof ../source/wtree.ml > prof/wtree.count.ml ; \
ocamlprof ../source/automata.ml > prof/automata.count.ml ; \
ocamlprof ../source/env.ml > prof/env.count.ml ; \
ocamlprof ../source/eval.ml > prof/eval.count.ml ; \
ocamlprof ../source/util.ml > prof/util.count.ml ; \
......@@ -602,7 +640,7 @@ release:
$(LURETTE_PATH)/source/rnumsolver.mli $(LURETTE_PATH)/source/rnumsolver.ml \
$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/wtree.mli $(LURETTE_PATH)/source/wtree.ml \
$(LURETTE_PATH)/source/automata.mli $(LURETTE_PATH)/source/automata.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/sim2chro.mli $(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/env.mli $(LURETTE_PATH)/source/env.ml \
......
......@@ -31,13 +31,14 @@ SOURCES_OCAML = \
$(LURETTE_PATH)/source/command_line_ima_exe.mli $(LURETTE_PATH)/source/command_line_ima_exe.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/control.mli $(LURETTE_PATH)/source/control.ml \
$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/rnumsolver.mli $(LURETTE_PATH)/source/rnumsolver.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/wtree.mli $(LURETTE_PATH)/source/wtree.ml \
$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/automata.mli $(LURETTE_PATH)/source/automata.ml \
$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/sim2chro.mli $(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/env.mli $(LURETTE_PATH)/source/env.ml \
$(LURETTE_PATH)/source/ima_exe.mli $(LURETTE_PATH)/source/ima_exe.ml
......
......@@ -25,6 +25,7 @@ SOURCES_OCAML = \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/control.mli $(LURETTE_PATH)/source/control.ml \
$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/show_ima.ml
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 68)
(Parent-Version lurette 0 67)
(Version-Log "
Add a verbose option in ima_exe.
(Project-Version lurette 0 69)
(Parent-Version lurette 0 68)
(Version-Log "
wtree.ml,mli: (deleted)
automa.ml,mli: (new files)
control.ml,mli: (new files)
Replace the [wtree] module by an [automata] module, that basically
does the same job, but in a different way. Namely, it no more uses
the [wtree] DS to use [graph]s instead. Indeed, the product of
wtrees introduces some problems, in particular to ensure its
correctness wrt to the automata run concurrently. Now, everything a
dead-simple wrt product: we simply perform a quasi-classical automata
product (well, at least, much closer from a classical product, cf
paper).
The way loop counters are handled has also changed. Now, counters are
handled via expressions of a simple arithmetic language that
basically lets one initialise a variable to an exact or a random
value (uniform or normal draw) and decrement it. Arcs are now
labelled by a formula plus 2 expressions of that mini-language (no
more weigth nor cpt_init stuff). The 1st expression is evaluated
during the draw, basically performs any operations on counters, and
returns a positive int that is used as the formula weigth. The second
expression (a kind of post-condition) is evaluated if its arc is the
one that has been elected to perform the step.
At several locations long lines (< 80) are reindented.
parse_env.ml:
In the ima format, IfThenElseExpr becomes IfThenElseNum.
Also, parse list more cleanly.
graph.ml,mli:
Add a function that test whether a transition is in the graph.
Do not sort list of transitions anymore (what was the point?).
Also do not sort nodes in any way.
show_env_env.ml,mli:
Abstract away nodes and arcs data types (so that I can display
Automata graphs). rename generate_env_graph into ima_to_dot.
lurette.ml:
ima_exe.ml:
Fix a bug where bbd table were filled by asserted non regression expr.
lurette.ml:
Fix a bug where incorrect data was sent to sim2chro (ie, the output of the
previous step instead of the ones of the current step.
env_state.ml:
solver.ml:
gne.ml:
Fix a performance bug where I was storing formula indexes even if
they were depending on inputs or pre, which is stupid as they generally
won't be used again. In order to fix that, I introduced new
atomic_formula <-> indexes table to stote the ones that do not depend
on inputs apart. It was also necassery to propogate the <<depend on pre>>
flag inside Gne.gn_expr (which i renamed Gne.t BTW).
Fix a bug in show_env.ml introduced in the previuos pci.
Add support to dynamically load another ima from ima_exe (will usefull for Ludic).
")
(New-Version-Log "")
(Checkin-Time "Fri, 17 May 2002 17:59:13 +0200")
(Checkin-Time "Fri, 19 Jul 2002 10:19:59 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -23,71 +82,71 @@ Add support to dynamically load another ima from ima_exe (will usefull for Ludic
;; Sources files for ima_exe
(source/ima_exe.mli (lurette/b/31_ima_exe.ml 1.1 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.12 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.13 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.4 644))
(source/command_line_ima_exe.mli (lurette/b/34_command_li 1.3 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.39 644))
(source/lurette.ml (lurette/12_lurette.ml 1.40 644))
(source/command_line.ml (lurette/b/20_command_li 1.7 644))
(source/command_line.mli (lurette/b/21_command_li 1.6 644))
;; Sources files common to lurette and ima_exe
(source/graph.mli (lurette/13_graph.mli 1.8 644))
(source/graph.ml (lurette/14_graph.ml 1.6 644))
(source/graph.mli (lurette/13_graph.mli 1.9 644))
(source/graph.ml (lurette/14_graph.ml 1.7 644))
(source/env.mli (lurette/15_env.mli 1.13 644))
(source/env.ml (lurette/16_env.ml 1.27 644))
(source/env.mli (lurette/15_env.mli 1.14 644))
(source/env.ml (lurette/16_env.ml 1.28 644))
(source/util.ml (lurette/35_util.ml 1.20 644))
(source/util.ml (lurette/35_util.ml 1.21 644))
(source/solver.mli (lurette/38_solver.mli 1.11 644))
(source/solver.ml (lurette/39_solver.ml 1.22 644))
(source/solver.mli (lurette/38_solver.mli 1.12 644))
(source/solver.ml (lurette/39_solver.ml 1.23 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.3 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.6 644))
(source/parse_env.mli (lurette/40_parse_env. 1.8 644))
(source/parse_env.ml (lurette/41_parse_env. 1.19 644))
(source/parse_env.mli (lurette/40_parse_env. 1.9 644))
(source/parse_env.ml (lurette/41_parse_env. 1.20 644))
(source/show_env.mli (lurette/42_show_env.m 1.6 644))
(source/show_env.ml (lurette/43_show_env.m 1.9 644))
(source/show_env.mli (lurette/42_show_env.m 1.7 644))
(source/show_env.ml (lurette/43_show_env.m 1.10 644))
(source/formula.mli (lurette/44_formula.ml 1.13 644))
(source/formula.ml (lurette/45_formula.ml 1.15 644))
(source/formula.mli (lurette/44_formula.ml 1.14 644))
(source/formula.ml (lurette/45_formula.ml 1.16 644))
(source/print.mli (lurette/46_print.mli 1.9 644))
(source/print.ml (lurette/47_print.ml 1.16 644))
(source/print.mli (lurette/46_print.mli 1.10 644))
(source/print.ml (lurette/47_print.ml 1.17 644))
(source/eval.mli (lurette/48_eval.mli 1.9 644))
(source/eval.ml (lurette/49_eval.ml 1.12 644))
(source/eval.mli (lurette/48_eval.mli 1.10 644))
(source/eval.ml (lurette/49_eval.ml 1.13 644))
(source/env_state.mli (lurette/50_env_state. 1.19 644))
(source/env_state.ml (lurette/51_env_state. 1.22 644))
(source/env_state.mli (lurette/50_env_state. 1.20 644))
(source/env_state.ml (lurette/51_env_state. 1.23 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.11 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.13 644))
(source/automata.mli (lurette/b/46_automata.m 1.1 644))
(source/automata.ml (lurette/b/47_automata.m 1.1 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.4 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.8 644))
(source/gne.mli (lurette/b/36_gne.mli 1.1 644))
(source/gne.ml (lurette/b/37_gne.ml 1.1 644))
(source/gne.mli (lurette/b/36_gne.mli 1.2 644))
(source/gne.ml (lurette/b/37_gne.ml 1.2 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.26 644))
; little script that sets env vars and starts the lurette build
(make_lurette (lurette/27_make_luret 1.12 744))
(make_lurette (lurette/27_make_luret 1.13 744))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.29 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.3 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.30 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.4 644))
(bin/Makefile.show_ima (lurette/b/40_Makefile.s 1.3 644))
(bin/Makefile.ima_exe (lurette/b/41_Makefile.i 1.2 644))
(bin/Makefile.show_ima (lurette/b/40_Makefile.s 1.4 644))
(bin/Makefile.ima_exe (lurette/b/41_Makefile.i 1.3 644))
(bin/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.1 644))
;; Documentation
......@@ -105,27 +164,35 @@ Add support to dynamically load another ima from ima_exe (will usefull for Ludic
(lurette.depfull.dot (lurette/b/5_lurette.de 1.2 644))
(TAGS (lurette/21_TAGS 1.6 644))
(test/time.exp (lurette/b/48_time.exp 1.1 644))
(test/time.res (lurette/b/49_time.res 1.1 644))
;; Various files used for testing purposes
(test/usager.env (lurette/b/14_usager.env 1.7 644))
(test/tram.env (lurette/b/15_tram.env 1.6 644))
(test/porte.env (lurette/b/16_porte.env 1.6 644))
(test/passerelle.env (lurette/b/17_passerelle 1.6 644))
(test/usager.env (lurette/b/14_usager.env 1.8 644))
(test/tram.env (lurette/b/15_tram.env 1.7 644))
(test/porte.env (lurette/b/16_porte.env 1.7 644))
(test/passerelle.env (lurette/b/17_passerelle 1.7 644))
(test/temp_int.env (lurette/b/50_temp_int.e 1.1 644))
(test/temp_float.env (lurette/b/51_temp_float 1.1 644))
(test/ControleurPorte.h (lurette/b/18_Controleur 1.1 644))
(test/ControleurPorte.c (lurette/b/19_Controleur 1.1 644))
(test/vrai_tram.lus (lurette/b/6_vrai_tram. 1.1 644))
(test/vrai_tram.h (lurette/b/7_vrai_tram. 1.2 644))
(test/vrai_tram.c (lurette/b/8_vrai_tram. 1.2 644))
(test/vrai_tram.lus (lurette/b/6_vrai_tram. 1.2 644))
(test/vrai_tram.h (lurette/b/7_vrai_tram. 1.3 644))
(test/vrai_tram.c (lurette/b/8_vrai_tram. 1.3 644))
(test/tram_simple.h (lurette/b/25_tram_simpl 1.1 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.2 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.4 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.2 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.3 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.5 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.3 644))
(test/heater_int.lus (lurette/b/43_heater_int 1.1 644))
(test/heater_float.lus (lurette/b/44_heater_flo 1.1 644))
(test/test_gen_stubs.h (lurette/b/45_test_gen_s 1.1 644))
(test/Makefile (lurette/c/0_Makefile 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
......@@ -39,7 +39,7 @@ case $# in
echo "... make"
shift 1
make $@ dc
make $@ dc
;;
##############################################################
*)
......
(*-----------------------------------------------------------------------
** Copyright (C) 2001, 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: automata.ml
** Author: jahier@imag.fr
**
*)
open Formula
open List
open Util
(****************************************************************************)
(** Set of integers *)
module IntSet = struct
include Set.Make(struct type t = int let compare = compare end)
end
let (intset_to_string : IntSet.t -> string) =
fun set ->
let elt = IntSet.max_elt set in
let set1 = IntSet.remove elt set in
IntSet.fold
(fun i acc -> ((string_of_int i) ^ ", " ^ acc))
set1
(string_of_int elt)
(****************************************************************************)
type arc_info_static = int * formula_eps * string list
(* We call it static in the sense that weights are no more dynamic. *)
let (arc_info_static_to_string : arc_info_static -> string) =
fun (w, formula_eps, pcl) ->
let pc_str = fold_left (fun acc str -> (acc^":"^str)) "" pcl in
( (string_of_int w) ^ " " ^
(formula_eps_to_string formula_eps) ^ " " ^ pc_str)
type lnode = IntSet.t
(* We need node to be set of [int]s so that the product of an
automata is still an automata. *)
type transition = lnode * arc_info_static * lnode
type dyn_trans_list = (node, arc_info) Graph.t
type stat_trans_list = (lnode, arc_info_static) Graph.t
type t = lnode * stat_trans_list
(****************************************************************************)
let (get_origin_nodes_from_trans_list : transition list -> lnode list) =
fun tl ->
(* collect all the starting nodes of the transitions in [tl] *)
fold_left (fun nl (n,_,_) -> if mem n nl then nl else n::nl) [] tl
let (is_epsilon : formula_eps -> bool) =
fun f ->
match f with
Eps -> true
| Form(_) -> false
(* exported *)
let rec (remove_formula : t -> formula -> t) =
fun (n, g) f ->
let all_trans = Graph.get_all_trans g in
let trans_to_rm =
fst (partition (fun (_,(_,fe,_),_) -> fe = Form(f)) all_trans)
in
let nodes_to_rm = get_origin_nodes_from_trans_list trans_to_rm in
iter (Graph.remove_trans g) trans_to_rm;
iter (rm_useless_eps_trans g) nodes_to_rm;
(n, g)
and
(rm_useless_eps_trans : stat_trans_list -> lnode -> unit) =
fun g node ->
(* recursively remove epsilon transitions that comes to [node] if it
has no successor. *)
if (Graph.get_list_of_target_nodes g node) = [] then
let (l, _) = partition
(fun (nf, (_,fe,_), nt) -> nt = node && is_epsilon fe)
(Graph.get_all_trans g)
in
iter (Graph.remove_trans g) l;
iter (rm_useless_eps_trans g) (get_origin_nodes_from_trans_list l)
(****************************************************************************)
(*
When I build sub-automata, I must remove loop bodies from the
automata iff its weight is 0 *AND* it has been obtained from the draw
(loop_between v min max) and [v] in bound to [max] (1) (ie, we can
not loop once more without violating te user spec). We say that [v]
is not recoverable.
Indeed, if I do that, then whenever no non-O-weighted branches exist,
then they can safely be taken; if it is a loop body branch, then it
corresponds to the recovery case; if it is a loop end one, then it