Commit c3ab83b6 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.12 Tue, 09 Dec 2003 15:44:28 +0100 by jahier

Parent-Version:      1.11
Version-Log:

Various fixes in the C scade parsing.

Project-Description: Lurette
parent b3c5c602
This diff is collapsed.
......@@ -8,42 +8,15 @@
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
# LIBDIRS = $(HOME)/$(HOST_TYPE)/lib $(SCADE_INSTALL_DIR)/lib
OCAMLMAKEFILE = $(HOME)/lurette/OcamlMakefile
LURETTE_PATH = $(HOME)/lurette
# SOURCES_LURETTE_LIB = $(LURETTE_PATH)/source/util.ml \
# $(LURETTE_PATH)/source/genlex.mli $(LURETTE_PATH)/source/genlex.ml \
# $(LURETTE_PATH)/source/lexeme.mli $(LURETTE_PATH)/source/lexeme.ml \
# $(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.ml \
# $(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
# $(LURETTE_PATH)/source/polyDraw.mli \
# $(LURETTE_PATH)/source/polyDraw.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/ne.mli $(LURETTE_PATH)/source/ne.ml \
# $(LURETTE_PATH)/source/constraint.mli $(LURETTE_PATH)/source/constraint.ml \
# $(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
# $(LURETTE_PATH)/source/lustreExp.mli $(LURETTE_PATH)/source/lustreExp.ml \
# $(LURETTE_PATH)/source/parser.mly $(LURETTE_PATH)/source/lexer.mll \
# $(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
# $(LURETTE_PATH)/source/parse_luc.mli $(LURETTE_PATH)/source/parse_luc.ml \
# $(LURETTE_PATH)/source/polyhedron.mli $(LURETTE_PATH)/source/polyhedron.ml \
# $(LURETTE_PATH)/source/store.mli $(LURETTE_PATH)/source/store.ml \
# $(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
# $(LURETTE_PATH)/source/formula_to_bdd.mli \
# $(LURETTE_PATH)/source/formula_to_bdd.ml \
# $(LURETTE_PATH)/source/bddd.mli \
# $(LURETTE_PATH)/source/bddd.ml \
# $(LURETTE_PATH)/source/fair_bddd.mli \
# $(LURETTE_PATH)/source/fair_bddd.ml \
# $(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.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/lurette.ml
ALL_SOURCES = $(SOURCES) $(SOURCES_OCAML)
......
......@@ -17,6 +17,9 @@ par les poids sont un peu contre-intuitives.
****** Documentation
* Rajouter dans lurettetop les options qui permette d'acceder au step mode
(ie, le mode du tirage pour faire un step)
* le retour au source lutin est sans doute cassé (à voir quand le nouveau compilo
lutin sera la)
......
......@@ -46,10 +46,10 @@ ICFLAGS = \
# XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
# sparc-sun
# XCFLAGS = -mcpu=ultrasparc -DHAVE_IEEE_754 -DUNIX100
XCFLAGS = -mcpu=ultrasparc -DHAVE_IEEE_754 -DUNIX100
# Windows95/98/NT with Cygwin tools
XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DHAVE_GETRLIMIT=0 -DRLIMIT_DATA_DEFAULT=67108864
# XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DHAVE_GETRLIMIT=0 -DRLIMIT_DATA_DEFAULT=67108864
CFLAGS = $(ICFLAGS) $(XCFLAGS) -O3 -DNDEBUG
......
......@@ -16,7 +16,6 @@ THREAD=
# THREAD=-thread threads.cma
xlurette_exe: dummy
mlglade xlurette.glade
mv xlurette_glade_interface.ml xlurette_glade_interface.ml0
......@@ -38,10 +37,10 @@ opt: dummy
| sed -e 's/\"pixmaps\//((Unix.getenv \"PIXMAP_DIR\") \^ \"/' \
| sed -e 's/.xpm\"/.xpm\")/' \
> xlurette_glade_interface.ml
ocamlopt.opt -verbose -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlopt.opt -verbose -c -I +lablgtk -labels -c xlurette_glade_callbacks.ml
ocamlopt.opt -verbose -c -pp "camlp4o" -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
ocamlopt.opt -verbose -I +lablgtk -I +str -labels -o xlurette_exe$(EXE) str.cmxa unix.cmxa lablgtk.cmxa gtkInit.cmx \
ocamlopt -verbose -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlopt -verbose -c -I +lablgtk -labels -c xlurette_glade_callbacks.ml
ocamlopt -verbose -c -pp "camlp4o" -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
ocamlopt -verbose -I +lablgtk -I +str -labels -o xlurette_exe$(EXE) str.cmxa unix.cmxa lablgtk.cmxa gtkInit.cmx \
xlurette_glade_callbacks.cmx xlurette_glade_interface.cmx xlurette_glade_main.cmx
......
......@@ -168,6 +168,7 @@ let (update_rif_file_name : string -> string -> string -> string -> unit) =
(**************************************************************************)
let pre_sut_node = ref ""
let pre_oracle_node = ref ""
let (remove_extension : string -> string) =
fun str ->
......@@ -511,7 +512,9 @@ class customized_callbacks = object(self)
self#top_fileselection_env#fileselection_env#misc#hide ()
method ok_add_env_clicked () =
let env_file = self#top_fileselection_add_env#fileselection_add_env#get_filename in
let env_file =
self#top_fileselection_add_env#fileselection_add_env#get_filename
in
self#top_xlurette#env_name#entry#set_text
(self#top_xlurette#env_name#entry#text ^ " " ^ env_file) ;
self#top_fileselection_add_env#fileselection_add_env#misc#hide ()
......@@ -599,24 +602,18 @@ class customized_callbacks = object(self)
(* to quit xlurette *)
method quit () =
output_string oc "\nquit\n"; (* to kill lurettetop *)
output_string oc "\n\nquit\nquit\n"; (* to kill lurettetop *)
flush oc;
prerr_endline "bye bye! " ;
prerr_endline "xlurette: bye! " ;
(* let's make sure everyone is dead *)
(* (try Unix.kill (!gp_pid) Sys.sigkill with _ -> () ); *)
(try Unix.kill (!lpid) Sys.sigkill with _ -> () );
(try Unix.kill (!pid) Sys.sigkill with _ -> () );
exit 0
if !lpid <> 0 then (try Unix.kill (!lpid) Sys.sigkill with _ -> () );
if !pid <> 0 then (try Unix.kill (!pid) Sys.sigkill with _ -> () );
exit 0
method on_quit_xlurette_button_clicked () =
self#top_quit_window#quit_window#show ()
method on_quit_yes_clicked () =
output_string oc "\n \n q\n" ;
flush oc;
(* (try Unix.kill (!gp_pid) Sys.sigkill with _ -> () ); *)
(try Unix.kill (!lpid) Sys.sigkill with _ -> () );
(try Unix.kill (!pid) Sys.sigkill with _ -> () );
self#quit ()
method on_quit_no_clicked () =
......@@ -908,10 +905,31 @@ class customized_callbacks = object(self)
self#top_xlurette#env_name_entry#entry#set_text "" ;
self#top_xlurette#oracle_name_entry#entry#set_text "" ;
self#top_xlurette#oracle_node_entry#entry#set_text "" ;
pre_sut_node := sut_node
pre_sut_node := sut_node;
output_string oc ("clean \n");
flush oc
)
method on_oracle_node_changed () =
let oracle_node = self#top_xlurette#oracle_node_entry#entry#text in
if
oracle_node <> !pre_oracle_node
then
(
pre_oracle_node := oracle_node;
output_string oc ("clean \n");
flush oc
)
method on_oracle_name_changed () =
let oracle = self#top_xlurette#oracle_name#entry#text in
if oracle <> "" then
let nodes = (lusinfo oracle) in
if nodes <> [] then self#top_xlurette#oracle_node#set_popdown_strings nodes;
else
self#top_xlurette#oracle_node_entry#entry#set_text ""
......@@ -961,16 +979,10 @@ class customized_callbacks = object(self)
(* ) *)
method on_oracle_name_changed () =
let oracle = self#top_xlurette#oracle_name#entry#text in
if oracle <> "" then
let nodes = (lusinfo oracle) in
if nodes <> [] then self#top_xlurette#oracle_node#set_popdown_strings nodes;
else
self#top_xlurette#oracle_node_entry#entry#set_text ""
method run_lurette () =
self#top_xlurette#progressbar#set_percentage 0.0;
update_rif_file_name
self#top_xlurette#rif_file_basename#text
(remove_extension self#top_xlurette#sut_name_entry#entry#text)
......@@ -1003,7 +1015,10 @@ class customized_callbacks = object(self)
(
let node = self#top_xlurette#sut_node_entry#entry#text in
(* a fake env ougth to have been generated by lurettetop *)
self#top_xlurette#env_name#entry#set_text (node ^ "_env.luc");
if
Sys.file_exists (node ^ "_env.luc")
then
self#top_xlurette#env_name#entry#set_text (node ^ "_env.luc");
(* Fill the combo boxes again, since more files may have been created *)
self#read_env_files ()
);
......@@ -1166,6 +1181,7 @@ class customized_callbacks = object(self)
self#set_sut_node node
| [< 'Genlex.Ident "set_oracle" ; str = parse_ident_or_string ; node = parse_node >] ->
pre_oracle_node := node;
self#set_oracle str;
self#set_oracle_node node
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 1 11)
(Parent-Version lurette 1 10)
(Project-Version lurette 1 12)
(Parent-Version lurette 1 11)
(Version-Log "
No more side effects are done via the Env_state module.
Various fixes in the C scade parsing.
")
(New-Version-Log ""
)
(Checkin-Time "Wed, 26 Nov 2003 08:52:30 +0100")
(Checkin-Time "Tue, 09 Dec 2003 15:44:28 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -30,7 +28,7 @@ No more side effects are done via the Env_state module.
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.14 644))
(source/lurette.ml (lurette/12_lurette.ml 1.79 644))
(source/lurette.ml (lurette/12_lurette.ml 1.80 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))
......@@ -42,24 +40,24 @@ No more side effects are done via the Env_state module.
(source/lucky.mli (lurette/15_env.mli 1.22 644))
(source/lucky.ml (lurette/16_env.ml 1.36 644))
(source/util.ml (lurette/35_util.ml 1.59 644))
(source/util.ml (lurette/35_util.ml 1.60 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.4 644))
(source/formula_to_bdd.mli (lurette/g/35_formula_to 1.5 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.6 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.6 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.7 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.7 644))
(source/solver.mli (lurette/38_solver.mli 1.21 644))
(source/solver.ml (lurette/39_solver.ml 1.59 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.11 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.12 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.6 644))
(source/store.mli (lurette/b/26_rnumsolver 1.23 644))
(source/store.ml (lurette/b/27_rnumsolver 1.31 644))
(source/store.ml (lurette/b/27_rnumsolver 1.32 644))
(source/parse_luc.mli (lurette/40_parse_env. 1.18 644))
(source/parse_luc.ml (lurette/41_parse_env. 1.50 644))
......@@ -82,7 +80,7 @@ No more side effects are done via the Env_state module.
(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.43 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.44 644))
(source/draw.mli (lurette/f/1_draw.mli 1.2 644))
(source/draw.ml (lurette/f/2_draw.ml 1.3 644))
......@@ -91,11 +89,11 @@ No more side effects are done via the Env_state module.
(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.mli (lurette/f/6_gen_stubs_ 1.1 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.50 644))
(source/gen_stubs_common.ml (lurette/e/39_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))
(source/gen_stubs_common.mli (lurette/e/40_gen_stubs_ 1.1 644))
(source/parse_c_scade.ml (lurette/e/41_parse_c_sc 1.2 644))
(source/parse_c_scade.mli (lurette/e/42_parse_c_sc 1.1 644))
(source/parse_c_scade.ml (lurette/e/41_parse_c_sc 1.3 644))
(source/parse_c_scade.mli (lurette/e/42_parse_c_sc 1.2 644))
(source/control.mli (lurette/c/3_control.ml 1.3 644))
(source/control.ml (lurette/c/4_control.ml 1.5 644))
......@@ -112,7 +110,7 @@ No more side effects are done via the Env_state module.
(source/prevar.ml (lurette/d/18_prevar.ml 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.ml (lurette/d/15_parse_poc. 1.5 644))
(source/parse_poc.mli (lurette/d/29_parse_poc. 1.2 644))
(source/gen_fake_lutin.ml (lurette/d/16_gen_fake_l 1.5 644))
......@@ -144,9 +142,9 @@ No more side effects are done via the Env_state module.
(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.7 644))
(Makefile.common.source (lurette/e/33_Makefile.c 1.8 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.51 644))
(share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.27 644))
(share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.28 644))
(user-rules (lurette/c/14_myrules 1.49 644))
(share/Makefile.test.in (lurette/c/25_user-rules 1.10 644))
(Makefile (lurette/d/13_Makefile 1.4 644))
......@@ -157,7 +155,7 @@ No more side effects are done via the Env_state module.
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.28 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.26 644))
(source/Makefile (lurette/c/20_Makefile 1.27 644))
;; Documentation
(doc/Interface_draft (lurette/19_Interface_ 1.1 644))
......@@ -172,19 +170,19 @@ No more side effects are done via the Env_state module.
(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.30 644))
(TODO (lurette/d/22_TODO 1.31 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))
(share/plot (lurette/e/35_plot 1.6 744))
(test/time-ossau.exp (lurette/b/48_time.exp 1.53 644))
(test/time-ossau.res (lurette/b/49_time.res 1.57 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.33 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.32 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.11 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.12 644))
(test/time-ossau.exp (lurette/b/48_time.exp 1.54 644))
(test/time-ossau.res (lurette/b/49_time.res 1.58 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.34 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.33 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.12 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.13 644))
;; Various files used for testing purposes
(test/cudd_gc_problem.luc (lurette/e/29_cudd_gc_pr 1.2 644))
......@@ -283,10 +281,10 @@ No more side effects are done via the Env_state module.
(test/Makefile (lurette/c/0_Makefile 1.14 644))
;; xlurette
(ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.29 644))
(ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.30 644))
(ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.25 644))
(ihm/xlurette/xlurette_glade_interface.ml (lurette/c/15_xlurette_g 1.23 644))
(ihm/xlurette/makefile (lurette/c/16_makefile 1.17 644))
(ihm/xlurette/makefile (lurette/c/16_makefile 1.18 644))
;; cudaux
......@@ -299,7 +297,7 @@ No more side effects are done via the Env_state module.
(cuddaux/cuddauxAddIte.c (lurette/c/32_cuddauxAdd 1.1 644))
(cuddaux/cuddaux.h (lurette/c/33_cuddaux.h 1.1 644))
(cuddaux/README (lurette/c/34_README 1.1 644))
(cuddaux/Makefile (lurette/c/35_Makefile 1.7 644))
(cuddaux/Makefile (lurette/c/35_Makefile 1.8 644))
(cuddaux/Changes (lurette/c/36_Changes 1.1 644))
......@@ -324,17 +322,17 @@ No more side effects are done via the Env_state module.
(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.8 644))
(mlcuddidl/Makefile (lurette/d/9_Makefile 1.9 644))
(mlcuddidl/Changes (lurette/d/10_Changes 1.1 644))
;; 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.3 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.1 644))
(polka/caml/vector.idl (lurette/d/35_vector.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))
......@@ -344,7 +342,7 @@ No more side effects are done via the Env_state module.
(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.2 644))
(polka/caml/Makefile (lurette/d/45_Makefile 1.3 644))
(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))
......@@ -385,7 +383,7 @@ No more side effects are done via the Env_state module.
;; Files added by populate at Tue, 26 Aug 2003 15:45:55 +0200,
;; to version 0.143(w), by jahier:
(source/gen_fake_lucky.ml (lurette/g/8_gen_fake_l 1.2 644))
(source/gen_fake_lucky.ml (lurette/g/8_gen_fake_l 1.3 644))
;; Files added by populate at Tue, 26 Aug 2003 15:46:03 +0200,
;; to version 0.143(w), by jahier:
......
......@@ -74,13 +74,13 @@ ICFLAGS = \
# XCFLAGS should be the same than the flags with which CUDD has been compiled
# i386-linux
XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
# XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
# sparc-sun
# XCFLAGS = -mcpu=ultrasparc -DHAVE_IEEE_754 -DUNIX100
XCFLAGS = -mcpu=ultrasparc -DHAVE_IEEE_754 -DUNIX100
# Windows95/98/NT with Cygwin tools
XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DHAVE_GETRLIMIT=0 -DRLIMIT_DATA_DEFAULT=67108864
# XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DHAVE_GETRLIMIT=0 -DRLIMIT_DATA_DEFAULT=67108864
CFLAGS = $(ICFLAGS) $(XCFLAGS) -O3 -DNDEBUG
CFLAGS_DEBUG = $(ICFLAGS) $(XCFLAGS) -O0 -g
......
......@@ -172,7 +172,7 @@ polka_parser.ml polka_parser.mli: polka_parser.mly
%_caml.c %.ml %.mli: %.idl sedscript
mkdir -p tmp
cp $*.idl tmp
$(CAMLIDL) -I ${SRCDIR} tmp/$*.idl
$(CAMLIDL) -nocpp -I ${SRCDIR} tmp/$*.idl
cp tmp/$*_stubs.c $*_caml.c
sed -f sedscript tmp/$*.ml >$*.ml
sed -f sedscript tmp/$*.mli >$*.mli
......
......@@ -3,7 +3,7 @@ poly.cmi: matrix.cmi vector.cmi
polka.cmo: polka.cmi
polka.cmx: polka.cmi
vector.cmo: polka.cmi polka_lexer.cmi polka_parser.cmi vector.cmi
vector.cmx: polka.cmx polka_lexer.cmi polka_parser.cmx vector.cmi
vector.cmx: polka.cmx polka_lexer.cmx polka_parser.cmx vector.cmi
matrix.cmo: polka.cmi vector.cmi matrix.cmi
matrix.cmx: polka.cmx vector.cmx matrix.cmi
poly.cmo: matrix.cmi vector.cmi poly.cmi
......
/* -*- mode: c -*- */
/* $Id: matrix.idl 1.1 Fri, 07 Mar 2003 10:37:48 +0100 jahier $ */
/* $Id: matrix.idl 1.2 Tue, 09 Dec 2003 15:44:28 +0100 jahier $ */
/* IDL file for matrix */
......@@ -17,7 +17,7 @@ quote(MLI,"val dummy : t")
matrix__t matrix_make(int nbrows, int nbcolumns) quote(call,
" if (nbrows<0 || nbcolumns<0) {
fprintf(stderr,\"nbrows=%d, nbcolumns=%d\n\",nbrows,nbcolumns);
fprintf(stderr,\"nbrows=%d, nbcolumns=%d\",nbrows,nbcolumns);
invalid_argument(\"Matrix.make: at least one argument is negative !\");
}
_res = matrix_alloc(nbrows,nbcolumns,true);");
......@@ -34,7 +34,7 @@ int matrix_hash_sort(matrix__t mat);
int matrix_get(matrix__t mat, int row,int col)
quote(call,
" if (row<0 || col<0 || row>=mat->nbrows || col>=mat->nbcolumns){
fprintf(stderr,\"row=%d,col=%d,nbrows=%d,nbcols=%d\n\",
fprintf(stderr,\"row=%d,col=%d,nbrows=%d,nbcols=%d\",
row,col,mat->nbrows,mat->nbcolumns);
invalid_argument(\"Matrix.get: indices\");
}
......@@ -44,7 +44,7 @@ quote(call,
void matrix_set(matrix__t mat, int row,int col, int val)
quote(call,
" if (row<0 || col<0 || row>=mat->nbrows || col>=mat->nbcolumns) {
fprintf(stderr,\"row=%d,col=%d,nbrows=%d,nbcols=%d\n\",
fprintf(stderr,\"row=%d,col=%d,nbrows=%d,nbcols=%d\",
row,col,mat->nbrows,mat->nbcolumns);
invalid_argument(\"Matrix.set: indices\");
}
......@@ -54,7 +54,7 @@ quote(call,
vector__t matrix_get_row(matrix__t mat, int row)
quote(call,
" if (row<0 || row>=mat->nbrows){
fprintf(stderr,\"row=%d,mat->nbrows=%d\n\",
fprintf(stderr,\"row=%d,mat->nbrows=%d\",
row,mat->nbrows);
invalid_argument(\"Matrix.get_row: index\");
}
......@@ -64,7 +64,7 @@ quote(call,
void matrix_set_row(matrix__t mat, int row, vector__t vec)
quote(call,
" if (row<0 || row>=mat->nbrows || mat->nbcolumns != vec.size){
fprintf(stderr,\"row=%d,mat->nbrows=%d,mat->nbcolumns=%d,vec.size=%d\n\",
fprintf(stderr,\"row=%d,mat->nbrows=%d,mat->nbcolumns=%d,vec.size=%d\",
row,mat->nbrows,mat->nbcolumns,vec.size);
invalid_argument(\"Matrix.set_row: index or incompatible dimensions\");
}
......
/* -*- mode: c -*- */
/* $Id: vector.idl 1.1 Fri, 07 Mar 2003 10:37:48 +0100 jahier $ */
/* $Id: vector.idl 1.2 Tue, 09 Dec 2003 15:44:28 +0100 jahier $ */
/* IDL file for vector */
......@@ -14,13 +14,14 @@ struct dimsup_t { int pos; int nbdims; };
quote(MLI,"val dummy : t")
/* \section{External functions} %============================================ */
vector__t vector_make(int size) quote(call,
vector__t vector_make(int size) quote(call,
" if (size<0) invalid_argument(\"Vector.make: size is negative !\");
if (size==0)
_res.q = 0;
else
_res.q = vector_alloc(size);
_res.size = size;");
_res.size = size;
");
quote(ML,"let dummy = make 0")
......
......@@ -28,7 +28,7 @@ SOURCES_C = $(LURETTE_TMP_DIR)/ocaml2c_stubs.c $(EXTRA_CFILES) $(SUT_DIR)/$(SUT)
$(LURETTE_TMP_DIR)/lurette__oracle.c \
$(LURETTE_TMP_DIR)/lurette_exe.c $(LURETTE_TMP_DIR)/call_lurette_main.c
bc:
......@@ -53,8 +53,11 @@ all: nc
SCADE_LIB_DIR=$(SCADE_INSTALL_DIR)/lib
SCADE_LIBDIRS=-L$(SCADE_INSTALL_DIR)/lib $(LIBDIRS)
SCADE_INCLUDE_DIR=-I$(SCADE_INSTALL_DIR)/include $(INCLUDEDIRS) \
-I$(USER_TESTING_DIR)/$(SUT)_C
SCADE_INCLUDE_DIR= \
-I$(SCADE_INSTALL_DIR)/lib \
-I$(SCADE_INSTALL_DIR)/SimulinkGateway/include \
-I$(SCADE_INSTALL_DIR)/include $(INCLUDEDIRS) \
-I$(USER_TESTING_DIR)
SCADE_OS_NAME=@SCADE_OS_NAME@
......
#!/bin/sh
# $Id: plot 1.5 Tue, 18 Nov 2003 11:17:12 +0100 jahier $
# $Id: plot 1.6 Tue, 09 Dec 2003 15:44:28 +0100 jahier $
#
# pl: general wrapper script for plotting with gnuplot from shell cmdline
#
......@@ -70,7 +70,7 @@ HOME_RCFILE=$HOME/.plrc
if [ -f $CODE ]; then rm $CODE; fi
cat > $CODE << EOT
# defaults
set style data linespoints
set data style linespoints
set grid
set pointsize 0.1
EOT
......
......@@ -166,6 +166,7 @@ libbc:
libdc:
make clean -f Makefile.lurette_lib
rm -f lurette_lib.o
make dc -f Makefile.lurette_lib OCAMLFLAGS=""
rm -f liblurette_lib_dc.a
......@@ -210,7 +211,6 @@ lucky_debug_no_assert:
make -k dc -f Makefile.lucky OCAMLFLAGS="-noassert"
lurette_debug:
make -k clean -f Makefile.lurette_debug OCAMLFLAGS=""
make -k dc -f Makefile.lurette_debug OCAMLFLAGS=""
lurette_assert:
......
......@@ -49,13 +49,24 @@ let snt_build = ref false
let (sol_number_snt : snt -> Bdd.t -> sol_nb * sol_nb) =
fun snt bdd ->
try
Hashtbl.find snt bdd
with Not_found ->
let bdd_not = (Bdd.dnot bdd) in
let (st, se) = Hashtbl.find snt bdd_not in
Hashtbl.add snt bdd (se, st);
(se, st)
(* let sol_nb' = ((Bdd.nbminterms (Bdd.size comb) bdd) /. 2.0) in *)
(* if sol_nb <> sol_nb' then *)
(* ( *)
(* print_string (" @@@ " ^ (string_of_float sol_nb) ^ " " *)
(* ^ (string_of_float sol_nb') ^ " \n"); *)
(* flush stdout; *)
(* exit 1 *)
(* ) *)
(* else *)
try
Hashtbl.find snt bdd
with Not_found ->
let bdd_not = (Bdd.dnot bdd) in
let (st, se) = Hashtbl.find snt bdd_not in
Hashtbl.add snt bdd (se, st);
(se, st)
let (sol_number : Bdd.t -> sol_nb * sol_nb) =
(sol_number_snt !snt_ref)
......@@ -68,8 +79,9 @@ let (add_snt_entry : Bdd.t -> sol_nb * sol_nb -> unit) =
let (init_snt : unit -> unit) =
fun _ ->
let bdd_true = Bdd.dtrue !Formula_to_bdd.bdd_manager in
let bdd_false = Bdd.dfalse !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))
(Hashtbl.add !snt_ref (bdd_false) (0.0, 1.0))
let (clear_snt: unit -> unit) =
fun _ ->
......@@ -119,7 +131,16 @@ let rec (build_sol_nb_table_rec: Bdd.t -> Bdd.t -> snt -> sol_nb) =
Hashtbl.replace snt bdd (nt, ne);
(add_sol_nb nt ne)
in
sol_nb
(* let sol_nb' = ((Bdd.nbminterms (Bdd.size comb) bdd) /. 2.0) in *)
(* if sol_nb <> sol_nb' then *)
(* ( *)
(* print_string (" @@@ " ^ (string_of_float sol_nb) ^ " " *)
(* ^ (string_of_float sol_nb') ^ " \n"); *)
(* flush stdout; *)
(* exit 1 *)
(* ) *)
(* else *)
sol_nb
and
(compute_absolute_sol_nb: Bdd.t -> Bdd.t -> snt -> sol_nb) =
fun sub_bdd comb snt ->
......
......@@ -24,7 +24,7 @@ val draw_in_bdd : Var.env_in -> Env_state.t -> Exp.var list -> Bdd.t ->
*)
val sol_number : Bdd.t -> sol_nb * sol_nb
(** Returns an entry of the table *)
(** Returns the solution number in the then and else branches of the bdd *)
(**/**)
......
(*-----------------------------------------------------------------------