Commit d534db9c authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 1.14 Fri, 19 Dec 2003 15:39:58 +0100 by jahier

Parent-Version:      1.13
Version-Log:

gen_stubs_scade.ml:
   fix a bug which was causing a bus error: to fix it, i simply delete
   a couple a extras &...

Project-Description: Lurette
parent 21390374
This diff is collapsed.
......@@ -8,9 +8,8 @@
# INCDIRS = $(HOME)/$(HOST_TYPE)/lib
# LIBDIRS = $(HOME)/$(HOST_TYPE)/lib
INCDIRS = $(HOME)/$(HOST_TYPE)/lib $(SCADE_INSTALL_DIR)/lib \
$(SCADE_INSTALL_DIR)/SimulinkGateway/include \
$(SCADE_INSTALL_DIR)/include
INCDIRS = $(HOME)/$(HOST_TYPE)/lib $(SCADE_INSTALL_DIR)/lib
LIBDIRS = $(HOME)/$(HOST_TYPE)/lib $(SCADE_INSTALL_DIR)/lib
OCAMLMAKEFILE = $(HOME)/lurette/OcamlMakefile
......
......@@ -7,8 +7,8 @@
The lurette V2 package is a set of tools that let one test and
simulate reactive programs (e.g., written in lustre). Its heart is
made of an engine that draws (boolean, integers and real) values
according to a non-deterministic specification written in the lutin
made of an engine that draws (Boolean, integer and real) values
according to a non-deterministic specification written in the Lutin
language.
The provided tools are:
......@@ -87,5 +87,5 @@ Nicolas Halbwachs
o ocaml, camlidl by the ocaml INRIA team
o polka, cuddaux and mlcuddidl by B. Jeannet, IRISA
o sim2chro by Y. Rémond - Vérimag
o autoconf, make, emacs, latex, dot, gtk, ... by other gnu-riders
o autoconf, make, emacs, latex, dot, gtk, ...
......@@ -11,10 +11,23 @@ de HS
*********** BUGS
* gen_fake_* : les variables sont declarées dans l'ordre inverse
de celui su sut...
* xlurette: le .lus n'est pas recompilé si on le change.
* xlurette : rediriger les erreurs de compil dans la fenetre principale.
d'une maniere generale, refaire un passage sur le comportement
de l'outil quand un maillon de la chaine foire.
* quand une formule s'avere fausse du point de vue des variables
numeriques, il ne faut pas repartir du haut du graphe, mais backtraker
depuis la branche qui s'avere fausse. Sinon, les probabilités induites
par les poids sont un peu contre-intuitives.
En plus, en backtraquant ainsi, je n'ai plus de problemes de dag2three !
et je ne suis plus obligé de
* en mode fair, certaines requetes aboutissent a qque chose de vraiment
......@@ -75,6 +88,11 @@ par les poids sont un peu contre-intuitives.
*********** A faire
* reporter le contenu de la nouvelle section de d1.1-v2 dans les entetes de modules
* rajouter une option --reactive ou lucky rend ses valeurs precedentes
si aucune formule n'est satisfiable (ainsi que --reactive-no-warning)
* Rajouter la precision comme un parametre externe
* Integrer la possibilité d'utiliser des types structurés avec lurette et scade
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 1 13)
(Parent-Version lurette 1 12)
(Project-Version lurette 1 14)
(Parent-Version lurette 1 13)
(Version-Log "
aesthetic changes in mli files so that
the automatically generated doc looks ok.
gen_stubs_scade.ml:
fix a bug which was causing a bus error: to fix it, i simply delete
a couple a extras &...
")
(New-Version-Log ""
)
(Checkin-Time "Fri, 12 Dec 2003 14:21:26 +0100")
(Checkin-Time "Fri, 19 Dec 2003 15:39:58 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -22,42 +23,42 @@ the automatically generated doc looks ok.
;; 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.41 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.42 644))
(source/command_line_luc_exe.ml (lurette/b/33_command_li 1.21 644))
(source/command_line_luc_exe.mli (lurette/b/34_command_li 1.14 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.15 644))
(source/lurette.ml (lurette/12_lurette.ml 1.81 644))
(source/lurette.mli (lurette/11_lurette.ml 1.16 644))
(source/lurette.ml (lurette/12_lurette.ml 1.82 644))
(source/command_line.ml (lurette/b/20_command_li 1.17 644))
(source/command_line.mli (lurette/b/21_command_li 1.14 644))
;; Sources files common to lurette and luc_exe
(source/graph.mli (lurette/13_graph.mli 1.12 644))
(source/graph.ml (lurette/14_graph.ml 1.10 644))
(source/graph.mli (lurette/13_graph.mli 1.13 644))
(source/graph.ml (lurette/14_graph.ml 1.11 644))
(source/lucky.mli (lurette/15_env.mli 1.23 644))
(source/lucky.ml (lurette/16_env.ml 1.37 644))
(source/lucky.mli (lurette/15_env.mli 1.24 644))
(source/lucky.ml (lurette/16_env.ml 1.38 644))
(source/util.ml (lurette/35_util.ml 1.60 644))
(source/util.ml (lurette/35_util.ml 1.61 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.4 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.5 644))
(source/formula_to_bdd.mli (lurette/g/35_formula_to 1.6 644))
(source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.5 644))
(source/fair_bddd.mli (lurette/g/39_fair_bddd. 1.5 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.7 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.8 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.9 644))
(source/solver.mli (lurette/38_solver.mli 1.22 644))
(source/solver.mli (lurette/38_solver.mli 1.23 644))
(source/solver.ml (lurette/39_solver.ml 1.60 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.13 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.7 644))
(source/store.mli (lurette/b/26_rnumsolver 1.24 644))
(source/store.mli (lurette/b/26_rnumsolver 1.25 644))
(source/store.ml (lurette/b/27_rnumsolver 1.33 644))
(source/parse_luc.mli (lurette/40_parse_env. 1.19 644))
......@@ -69,11 +70,11 @@ the automatically generated doc looks ok.
(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.38 644))
(source/env_state.ml (lurette/51_env_state. 1.52 644))
(source/env_state.mli (lurette/50_env_state. 1.39 644))
(source/env_state.ml (lurette/51_env_state. 1.53 644))
(source/run_aut.mli (lurette/b/46_automata.m 1.9 644))
(source/run_aut.ml (lurette/b/47_automata.m 1.19 644))
(source/run_aut.mli (lurette/b/46_automata.m 1.10 644))
(source/run_aut.ml (lurette/b/47_automata.m 1.20 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.10 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.23 644))
......@@ -88,7 +89,7 @@ the automatically generated doc looks ok.
(source/gen_stubs_poc.ml (lurette/f/3_gen_stubs_ 1.1 644))
(source/gen_stubs_poc.mli (lurette/f/4_gen_stubs_ 1.1 644))
(source/gen_stubs_scade.ml (lurette/f/5_gen_stubs_ 1.1 644))
(source/gen_stubs_scade.ml (lurette/f/5_gen_stubs_ 1.2 644))
(source/gen_stubs_scade.mli (lurette/f/6_gen_stubs_ 1.1 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.51 644))
(source/gen_stubs_common.ml (lurette/e/39_gen_stubs_ 1.2 644))
......@@ -108,7 +109,7 @@ the automatically generated doc looks ok.
(source/value.ml (lurette/c/23_value.ml 1.7 644))
(source/value.mli (lurette/c/24_value.mli 1.6 644))
(source/prevar.ml (lurette/d/18_prevar.ml 1.4 644))
(source/prevar.ml (lurette/d/18_prevar.ml 1.5 644))
(source/prevar.mli (lurette/d/19_prevar.mli 1.5 644))
(source/parse_poc.ml (lurette/d/15_parse_poc. 1.5 644))
......@@ -142,21 +143,21 @@ the automatically generated doc looks ok.
(share/pixmaps/chrono.xpm (lurette/f/23_chrono.xpm 1.1 644))
(share/pixmaps/button-close.xpm (lurette/f/24_button-clo 1.1 644))
(share/config.guess (lurette/f/25_config.gue 1.1 755))
(share/configure.in (lurette/d/11_configure. 1.14 644))
(Makefile.common.source (lurette/e/33_Makefile.c 1.9 644))
(share/configure.in (lurette/d/11_configure. 1.15 644))
(Makefile.common.source (lurette/e/33_Makefile.c 1.10 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.51 644))
(share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.28 644))
(share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.29 644))
(user-rules (lurette/c/14_myrules 1.50 644))
(share/Makefile.test.in (lurette/c/25_user-rules 1.10 644))
(share/Makefile.test.in (lurette/c/25_user-rules 1.11 644))
(Makefile (lurette/d/13_Makefile 1.4 644))
(source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.5 644))
(source/Makefile.gen_fake_lutin (lurette/d/17_Makefile.g 1.4 644))
(source/Makefile.show_luc (lurette/b/40_Makefile.s 1.12 644))
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.28 644))
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.29 644))
(source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.8 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.26 644))
(source/Makefile (lurette/c/20_Makefile 1.27 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.27 644))
(source/Makefile (lurette/c/20_Makefile 1.28 644))
;; Documentation
(doc/Interface_draft (lurette/19_Interface_ 1.1 644))
......@@ -167,23 +168,23 @@ the automatically generated doc looks ok.
(doc/ocamldoc.hva (lurette/b/13_ocamldoc.h 1.1 644))
;; Misc
(README (lurette/10_README 1.10 644))
(README (lurette/10_README 1.11 644))
(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.32 644))
(TODO (lurette/d/22_TODO 1.33 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/lucky_init.sh.in (lurette/e/24_lucky_init 1.12 644))
(share/gnuplot-rif (lurette/e/34_gnuplot-ri 1.5 744))
(share/plot (lurette/e/35_plot 1.6 744))
(test/time-ossau.exp (lurette/b/48_time.exp 1.55 644))
(test/time-ossau.res (lurette/b/49_time.res 1.58 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.35 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.34 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.13 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.14 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.36 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.35 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.14 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.15 644))
;; Various files used for testing purposes
(test/cudd_gc_problem.luc (lurette/e/29_cudd_gc_pr 1.2 644))
......@@ -303,76 +304,76 @@ the automatically generated doc looks ok.
;; mlcuddidl
(mlcuddidl/session.ml (lurette/c/37_session.ml 1.1 644))
(mlcuddidl/session.ml (lurette/c/37_session.ml 1.1 600))
(mlcuddidl/sedscript (lurette/c/38_sedscript 1.1 644))
(mlcuddidl/rdd.mli (lurette/c/40_rdd.mli 1.1 640))
(mlcuddidl/rdd.ml (lurette/c/41_rdd.ml 1.1 640))
(mlcuddidl/rdd.idl (lurette/c/42_rdd.idl 1.1 644))
(mlcuddidl/mtbdd.mli (lurette/c/43_mtbdd.mli 1.1 644))
(mlcuddidl/mtbdd.ml (lurette/c/44_mtbdd.ml 1.1 644))
(mlcuddidl/rdd.idl (lurette/c/42_rdd.idl 1.1 600))
(mlcuddidl/mtbdd.mli (lurette/c/43_mtbdd.mli 1.1 600))
(mlcuddidl/mtbdd.ml (lurette/c/44_mtbdd.ml 1.1 600))
(mlcuddidl/manager.mli (lurette/c/46_manager.ml 1.1 640))
(mlcuddidl/manager.ml (lurette/c/47_manager.ml 1.1 640))
(mlcuddidl/manager.idl (lurette/c/48_manager.id 1.1 644))
(mlcuddidl/macros.m4 (lurette/c/49_macros.m4 1.1 644))
(mlcuddidl/manager.idl (lurette/c/48_manager.id 1.2 600))
(mlcuddidl/macros.m4 (lurette/c/49_macros.m4 1.2 600))
(mlcuddidl/idd.mli (lurette/c/51_idd.mli 1.1 640))
(mlcuddidl/idd.ml (lurette/d/0_idd.ml 1.1 640))
(mlcuddidl/idd.idl (lurette/d/1_idd.idl 1.1 644))
(mlcuddidl/cudd_caml.h (lurette/d/2_cudd_caml. 1.1 644))
(mlcuddidl/cudd_caml.c (lurette/d/3_cudd_caml. 1.1 644))
(mlcuddidl/bdd.mli (lurette/d/5_bdd.mli 1.1 640))
(mlcuddidl/bdd.ml (lurette/d/6_bdd.ml 1.1 640))
(mlcuddidl/bdd.idl (lurette/d/7_bdd.idl 1.1 644))
(mlcuddidl/README (lurette/d/8_README 1.1 644))
(mlcuddidl/Makefile (lurette/d/9_Makefile 1.9 644))
(mlcuddidl/Changes (lurette/d/10_Changes 1.1 644))
(mlcuddidl/idd.idl (lurette/d/1_idd.idl 1.1 600))
(mlcuddidl/cudd_caml.h (lurette/d/2_cudd_caml. 1.2 600))
(mlcuddidl/cudd_caml.c (lurette/d/3_cudd_caml. 1.2 600))
(mlcuddidl/bdd.mli (lurette/d/5_bdd.mli 1.2 640))
(mlcuddidl/bdd.ml (lurette/d/6_bdd.ml 1.2 640))
(mlcuddidl/bdd.idl (lurette/d/7_bdd.idl 1.2 600))
(mlcuddidl/README (lurette/d/8_README 1.1 600))
(mlcuddidl/Makefile (lurette/d/9_Makefile 1.10 600))
(mlcuddidl/Changes (lurette/d/10_Changes 1.2 600))
;; polka
(polka/Makefile.depend (lurette/d/30_Makefile.d 1.1 644))
(polka/tmp () :directory)
(polka/sedscript (lurette/d/31_sedscript 1.1 644))
(polka/caml/Makefile.depend (lurette/d/32_Makefile.d 1.4 644))
(polka/caml/poly.idl (lurette/d/33_poly.idl 1.1 644))
(polka/caml/matrix.idl (lurette/d/34_matrix.idl 1.2 644))
(polka/caml/vector.idl (lurette/d/35_vector.idl 1.2 644))
(polka/caml/polka_caml.h (lurette/d/36_polka_caml 1.1 644))
(polka/caml/polka_caml.c (lurette/d/37_polka_caml 1.1 644))
(polka/caml/polka.mli (lurette/d/38_polka.mli 1.1 644))
(polka/caml/polka.ml (lurette/d/39_polka.ml 1.1 644))
(polka/caml/polka_parser.mly (lurette/d/40_polka_pars 1.1 644))
(polka/caml/polka_lexer.mli (lurette/d/41_polka_lexe 1.1 644))
(polka/caml/polka_lexer.mll (lurette/d/42_polka_lexe 1.1 644))
(polka/caml/polkaIO.mli (lurette/d/43_polkaIO.ml 1.1 644))
(polka/caml/polkaIO.ml (lurette/d/44_polkaIO.ml 1.1 644))
(polka/caml/Makefile (lurette/d/45_Makefile 1.3 644))
(polka/caml/Makefile.depend (lurette/d/32_Makefile.d 1.5 644))
(polka/caml/poly.idl (lurette/d/33_poly.idl 1.2 600))
(polka/caml/matrix.idl (lurette/d/34_matrix.idl 1.3 600))
(polka/caml/vector.idl (lurette/d/35_vector.idl 1.3 600))
(polka/caml/polka_caml.h (lurette/d/36_polka_caml 1.2 600))
(polka/caml/polka_caml.c (lurette/d/37_polka_caml 1.2 600))
(polka/caml/polka.mli (lurette/d/38_polka.mli 1.2 600))
(polka/caml/polka.ml (lurette/d/39_polka.ml 1.2 600))
(polka/caml/polka_parser.mly (lurette/d/40_polka_pars 1.1 600))
(polka/caml/polka_lexer.mli (lurette/d/41_polka_lexe 1.1 600))
(polka/caml/polka_lexer.mll (lurette/d/42_polka_lexe 1.1 600))
(polka/caml/polkaIO.mli (lurette/d/43_polkaIO.ml 1.1 600))
(polka/caml/polkaIO.ml (lurette/d/44_polkaIO.ml 1.2 600))
(polka/caml/Makefile (lurette/d/45_Makefile 1.4 600))
(polka/C/Makefile.depend (lurette/d/46_Makefile.d 1.1 644))
(polka/C/vector.h (lurette/d/47_vector.h 1.1 644))
(polka/C/satmat.h (lurette/d/48_satmat.h 1.1 644))
(polka/C/poly.h (lurette/d/49_poly.h 1.1 644))
(polka/C/polka.h (lurette/d/50_polka.h 1.1 644))
(polka/C/matrix.h (lurette/d/51_matrix.h 1.1 644))
(polka/C/internal.h (lurette/e/0_internal.h 1.1 644))
(polka/C/cherni.h (lurette/e/1_cherni.h 1.1 644))
(polka/C/bit.h (lurette/e/2_bit.h 1.1 644))
(polka/C/vector.c (lurette/e/3_vector.c 1.1 644))
(polka/C/satmat.c (lurette/e/4_satmat.c 1.1 644))
(polka/C/poly.c (lurette/e/5_poly.c 1.1 644))
(polka/C/polka.c (lurette/e/6_polka.c 1.1 644))
(polka/C/matrix.c (lurette/e/7_matrix.c 1.1 644))
(polka/C/internal.c (lurette/e/8_internal.c 1.1 644))
(polka/C/cherni.c (lurette/e/9_cherni.c 1.2 644))
(polka/C/bit.c (lurette/e/10_bit.c 1.1 644))
(polka/C/essai.c (lurette/e/11_essai.c 1.1 644))
(polka/C/pkint.h (lurette/e/12_pkint.h 1.1 644))
(polka/C/config.h (lurette/e/13_config.h 1.1 644))
(polka/C/main.tex (lurette/e/14_main.tex 1.1 644))
(polka/C/Makefile (lurette/e/15_Makefile 1.1 644))
(polka/documentation/texinfo.tex (lurette/e/16_texinfo.te 1.1 644))
(polka/documentation/polka.texi (lurette/e/17_polka.texi 1.1 644))
(polka/documentation/Makefile (lurette/e/18_Makefile 1.1 644))
(polka/README (lurette/e/19_README 1.1 644))
(polka/Makefile.config (lurette/e/20_Makefile.c 1.5 644))
(polka/Makefile (lurette/e/21_Makefile 1.1 644))
(polka/Changes (lurette/e/22_Changes 1.1 644))
(polka/C/vector.h (lurette/d/47_vector.h 1.2 600))
(polka/C/satmat.h (lurette/d/48_satmat.h 1.1 600))
(polka/C/poly.h (lurette/d/49_poly.h 1.2 600))
(polka/C/polka.h (lurette/d/50_polka.h 1.2 600))
(polka/C/matrix.h (lurette/d/51_matrix.h 1.2 600))
(polka/C/internal.h (lurette/e/0_internal.h 1.2 600))
(polka/C/cherni.h (lurette/e/1_cherni.h 1.2 600))
(polka/C/bit.h (lurette/e/2_bit.h 1.2 600))
(polka/C/vector.c (lurette/e/3_vector.c 1.2 600))
(polka/C/satmat.c (lurette/e/4_satmat.c 1.1 600))
(polka/C/poly.c (lurette/e/5_poly.c 1.2 600))
(polka/C/polka.c (lurette/e/6_polka.c 1.2 600))
(polka/C/matrix.c (lurette/e/7_matrix.c 1.2 600))
(polka/C/internal.c (lurette/e/8_internal.c 1.2 600))
(polka/C/cherni.c (lurette/e/9_cherni.c 1.3 600))
(polka/C/bit.c (lurette/e/10_bit.c 1.2 600))
(polka/C/essai.c (lurette/e/11_essai.c 1.1 600))
(polka/C/pkint.h (lurette/e/12_pkint.h 1.1 600))
(polka/C/config.h (lurette/e/13_config.h 1.2 600))
(polka/C/main.tex (lurette/e/14_main.tex 1.1 600))
(polka/C/Makefile (lurette/e/15_Makefile 1.2 600))
(polka/documentation/texinfo.tex (lurette/e/16_texinfo.te 1.1 600))
(polka/documentation/polka.texi (lurette/e/17_polka.texi 1.2 600))
(polka/documentation/Makefile (lurette/e/18_Makefile 1.1 600))
(polka/README (lurette/e/19_README 1.1 600))
(polka/Makefile.config (lurette/e/20_Makefile.c 1.6 600))
(polka/Makefile (lurette/e/21_Makefile 1.1 600))
(polka/Changes (lurette/e/22_Changes 1.2 600))
......@@ -470,17 +471,17 @@ the automatically generated doc looks ok.
;; Files added by populate at Fri, 14 Nov 2003 14:32:53 +0100,
;; to version 1.8(w), by jahier:
(source/var.ml (lurette/g/49_var.ml 1.3 644))
(source/var.ml (lurette/g/49_var.ml 1.4 644))
;; Files added by populate at Fri, 14 Nov 2003 14:32:55 +0100,
;; to version 1.8(w), by jahier:
(source/var.mli (lurette/g/50_var.mli 1.3 644))
(source/var.mli (lurette/g/50_var.mli 1.4 644))
;; Files added by populate at Wed, 26 Nov 2003 08:47:27 +0100,
;; to version 1.10(w), by jahier:
(source/thickness.ml (lurette/g/51_thickness. 1.2 644))
(source/thickness.ml (lurette/g/51_thickness. 1.3 644))
)
(Merge-Parents)
(New-Merge-Parents)
MLCuddIDL 1.1:
-------------
Function Bdd.is_complement added.
MLCuddIDL 1.0:
-------------
......
......@@ -53,7 +53,7 @@ OCAMLDEP = ocamldep
OCAMLLEX = ocamllex.opt
OCAMLYACC = ocamlyacc
OCAMLINC =
OCAMLFLAGS =
OCAMLFLAGS = -g
OCAMLOPTFLAGS = -inline 20
CAMLIDL = camlidl
......@@ -68,8 +68,7 @@ CC = gcc
ICFLAGS = \
-I$(CUDDINCDIR) -I$(CUDDAUXINCDIR) \
-I$(CAMLLIBDIR) -I$(CAMLIDLLIBDIR) \
-Winline -Wimplicit-function-declaration
-Winline -Wimplicit-function-declaration
#
# XCFLAGS should be the same than the flags with which CUDD has been compiled
......@@ -104,7 +103,7 @@ CCMODULES = cudd_caml $(IDLMODULES:%=%_caml)
CCSRC = cudd_caml.h $(CCMODULES:%=%.c)
CCBIN_TOINSTALL = cuddrun
CCLIB_TOINSTALL = libcudd_caml.a libcudd_caml_debug.a libcudd_caml_prof.a
CCLIB_TOINSTALL = libcudd_caml.a libcudd_caml_debug.a libcudd_caml_prof.a
CCINC_TOINSTALL = cudd_caml.h
#---------------------------------------
......@@ -112,7 +111,7 @@ CCINC_TOINSTALL = cudd_caml.h
#---------------------------------------
# Global rules
all: $(MLINT) $(MLOBJx) cudd.cma cudd.cmxa libcudd_caml.a
all: $(MLINT) $(MLOBJ) $(MLOBJx) cudd.cma cudd.cmxa libcudd_caml.a
debug: all libcudd_caml_debug.a
prof: all libcudd_caml_prof.a
......@@ -147,7 +146,8 @@ mostlyclean: clean
/bin/rm -f mlcuddidl.?? mlcuddidl.??? mlcuddidl.info sedscript
clean:
/bin/rm -f *.[ao] *.cm[ioxa] *.cmxa cuddrun cuddtop
/bin/rm -f cuddrun cuddtop
/bin/rm -f *.[ao] *.cm[ioxa] *.cmxa
tar: $(IDLMODULES:%=%.idl) macros.m4 $(MLSRC) $(CCSRC) Makefile README Changes main.tex tutorial.ml session.ml
(cd ..; tar zcvf $(HOME)/mlcuddidl.tgz $(^:%=mlcuddidl/%))
......@@ -199,7 +199,7 @@ mlcuddidl.html: mlcuddidl.texi
# IMPLICIT RULES AND DEPENDENCIES
#--------------------------------------------------------------
.SUFFIXES: .tex .fig .c .h .o .ml .mli .cmi .cmo .cmx .idl
.SUFFIXES: .tex .fig .c .h .o .ml .mli .cmi .cmo .cmx .idl _debug.o _prof.o _caml.c
#-----------------------------------
# IDL
......
/* -*- mode: c -*- */
/* $Id: bdd.idl 1.1 Mon, 07 Oct 2002 17:53:39 +0200 jahier $ */
/* $Id: bdd.idl 1.2 Fri, 19 Dec 2003 15:39:58 +0100 jahier $ */
quote(C, "
#include \"caml/custom.h\"
......@@ -14,7 +14,7 @@ import "manager.idl";
typedef [abstract,c2ml(bdd_c2ml),ml2c(node_ml2c)] struct node__t bdd__t;
quote(MLMLI,"
type bdd =
type bdd =
| Bool of bool
| Ite of int * t * t
")
......@@ -28,8 +28,9 @@ quote(MLMLI,"(* ====================================================== *)")
manager__t manager(bdd__t no) quote(call, "_res=no.man;");
boolean is_cst(bdd__t no) quote(call, "_res = Cudd_IsConstant(no.node);");
boolean is_complement(bdd__t no) quote(call, "_res = Cudd_IsComplement(no.node);");
int topvar(bdd__t no) quote(call, "_res = Cudd_Regular(no.node)->index;");
bdd__t dthen(bdd__t no)
bdd__t dthen(bdd__t no)
quote(call, "
_res.man = no.man;
_res.node = Cudd_T(no.node);
......@@ -43,8 +44,8 @@ if (Cudd_IsComplement(no.node)) _res.node = Cudd_Not(_res.node);
");
void cofactors(int var, bdd__t no, [out] bdd__t noa, [out] bdd__t nob)
quote(call,
" {
quote(call,
" {
DdNode* cof;
noa.man = nob.man = no.man;
Begin_roots1(_v_no);
......@@ -59,20 +60,22 @@ bdd__t cofactor(bdd__t no1, bdd__t no2) NO_OF_MAN_NO12(Cudd_Cofactor);
quote(MLMLI,"external inspect: bdd__t -> bdd = \"camlidl_bdd_inspect\"")
/* \section{Supports} %====================================================== */
quote(MLMLI,"(* ====================================================== *)")
quote(MLMLI,"(* Supports *)")
quote(MLMLI,"(* ====================================================== *)")
bdd__t support(bdd__t no)
bdd__t support(bdd__t no)
NO_OF_MAN_NO(Cudd_Support);
int supportsize(bdd__t no)
quote(call, "_res = Cudd_SupportSize(no.man,no.node);");
boolean is_var_in(int var, bdd__t no)
boolean is_var_in(int var, bdd__t no)
quote(call, "
Begin_roots1(_v_no);
{
DdNode* v = Cudd_bddIthVar(no.man,var);
DdNode* v = Cudd_bddIthVar(no.man,var);
_res = Cuddaux_IsVarIn(no.man, no.node, v);
}
End_roots();
......@@ -85,7 +88,7 @@ quote(MLMLI,"(* ====================================================== *)")
quote(MLMLI,"(* Manipulation of supports *)")
quote(MLMLI,"(* ====================================================== *)")
bdd__t support_inter(bdd__t no1, bdd__t no2)
bdd__t support_inter(bdd__t no1, bdd__t no2)
NO_OF_MAN_NO12(Cudd_bddLiteralSetIntersection);
quote(MLMLI, "
......@@ -99,15 +102,15 @@ quote(MLMLI,"(* ====================================================== *)")
quote(MLMLI,"(* Constants and Variables *)")
quote(MLMLI,"(* ====================================================== *)")
bdd__t dtrue(manager__t man)
bdd__t dtrue(manager__t man)
quote(call, "_res.man = man; _res.node = DD_ONE(man);");
bdd__t dfalse(manager__t man)
bdd__t dfalse(manager__t man)
quote(call, "_res.man = man; _res.node = Cudd_Not(DD_ONE(man));");
bdd__t ithvar(manager__t man, int var)
quote(call, "_res.man = man; _res.node = Cudd_bddIthVar(man,var);");
bdd__t newvar(manager__t man)
bdd__t newvar(manager__t man)
quote(call, "_res.man = man; _res.node = Cudd_bddNewVar(man);");
bdd__t newvar_at_level(manager__t man, int level)
bdd__t newvar_at_level(manager__t man, int level)
quote(call, "_res.man = man; _res.node = Cudd_bddNewVarAtLevel(man,level);");
quote(ML,"let dummy = dtrue Manager.dummy")
......@@ -121,11 +124,11 @@ boolean is_true(bdd__t no)
quote(call, "_res = (no.node == DD_ONE(no.man));");
boolean is_false(bdd__t no)
quote(call, "_res = (no.node == Cudd_Not(DD_ONE(no.man)));");
boolean is_equal(bdd__t no1, bdd__t no2)
boolean is_equal(bdd__t no1, bdd__t no2)
quote(call, "CHECK_MAN2; _res = (no1.node==no2.node);");
boolean is_leq(bdd__t no1, bdd__t no2)
boolean is_leq(bdd__t no1, bdd__t no2)
quote(call, "CHECK_MAN2; _res = Cudd_bddLeq(no1.man, no1.node, no2.node);");
boolean is_inter_empty(bdd__t no1, bdd__t no2)
boolean is_inter_empty(bdd__t no1, bdd__t no2)
quote(call, "CHECK_MAN2; _res = Cudd_bddLeq(no1.man, no1.node, Cudd_Not(no2.node));");
boolean is_equal_when(bdd__t no1, bdd__t no2,bdd__t no3)
quote(call,"CHECK_MAN3; _res=Cudd_EquivDC(no1.man,no1.node,no2.node,Cudd_Not(no3.node));");
......@@ -151,16 +154,16 @@ quote(call,
}
");
boolean is_var_dependent(int var, bdd__t no)
boolean is_var_dependent(int var, bdd__t no)
quote(call, "
Begin_roots1(_v_no);
{
DdNode* v = Cudd_bddIthVar(no.man,var);
DdNode* v = Cudd_bddIthVar(no.man,var);
_res = Cudd_bddVarIsDependent(no.man, no.node, v);
}
End_roots();
");
boolean is_var_essential(int index, int phase, bdd__t no)
boolean is_var_essential(int index, int phase, bdd__t no)
quote(call, "_res = Cudd_bddIsVarEssential(no.man,no.node,index,phase);");
/* \section{Structural information} %======================================== */
......@@ -169,7 +172,7 @@ quote(MLMLI,"(* Structural information *)")
quote(MLMLI,"(* ====================================================== *)")
int size(bdd__t no) quote(call, "_res = Cudd_DagSize(no.node);");
double nbpaths(bdd__t no)
double nbpaths(bdd__t no)
quote(call,
"_res = Cudd_CountPath(no.node); \
if (_res==(double)CUDD_OUT_OF_MEM){ \
......@@ -206,9 +209,9 @@ quote(MLMLI,"external eq: bdd__t -> bdd__t -> bdd__t = \"camlidl_bdd_nxor\"")
bdd__t ite(bdd__t no1, bdd__t no2, bdd__t no3) NO_OF_MAN_NO123(Cudd_bddIte);
bdd__t compose(int var, bdd__t no1, bdd__t no2)
quote(call, "
CHECK_MAN2;
CHECK_MAN2;
Begin_roots2(_v_no1,_v_no2);
_res.man = no1.man;
_res.man = no1.man;
_res.node = Cudd_bddCompose(no1.man, no2.node, no1.node, var);
End_roots();
");
......@@ -240,18 +243,18 @@ quote(MLMLI,"(* ====================================================== *)")
quote(MLMLI,"(* Quantifications *)")
quote(MLMLI,"(* ====================================================== *)")
bdd__t exist(bdd__t no1, bdd__t no2)
bdd__t exist(bdd__t no1, bdd__t no2)
NO_OF_MAN_NO21(Cudd_bddExistAbstract);
bdd__t forall(bdd__t no1, bdd__t no2)
bdd__t forall(bdd__t no1, bdd__t no2)
NO_OF_MAN_NO21(Cudd_bddUnivAbstract);
bdd__t existand(bdd__t no1, bdd__t no2, bdd__t no3)
bdd__t existand(bdd__t no1, bdd__t no2, bdd__t no3)
NO_OF_MAN_NO231(Cudd_bddAndAbstract);
bdd__t existxor(bdd__t no1, bdd__t no2, bdd__t no3)
bdd__t existxor(bdd__t no1, bdd__t no2, bdd__t no3)
NO_OF_MAN_NO231(Cudd_bddXorExistAbstract);
bdd__t booleandiff(bdd__t no, int index)
bdd__t booleandiff(bdd__t no, int index)
quote(call, "
Begin_roots1(_v_no);
_res.man = no.man;
_res.man = no.man;
_res.node = Cudd_bddBooleanDiff(no.man,no.node,index);
End_roots();
");
......@@ -261,7 +264,7 @@ external cube_of_bdd: t -> t = \"camlidl_dd_cube_of_bdd\"
external list_of_cube: t -> (int*bool) list = \"camlidl_dd_list_of_cube\"
")
bdd__t cube_union(bdd__t no1, bdd__t no2)
bdd__t cube_union(bdd__t no1, bdd__t no2)
NO_OF_MAN_NO12(Cuddaux_bddCubeUnion);
......@@ -313,7 +316,7 @@ End_roots();
bdd__t overapprox(int nvars, int threshold, int safe, double quality, bdd__t no)
quote(call,"
Begin_roots1(_v_no);
_res.man=no.man;
_res.man=no.man;
_res.node=Cudd_OverApprox(no.man,no.node,nvars,threshold,safe,quality);
End_roots();