Commit 105a7f85 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.74 Fri, 02 Aug 2002 16:15:33 +0200 by jahier

Parent-Version:      0.73
Version-Log:

source/lurettetop.ml: [new file]
   A top level loop for using lurette.

also remame all .env files using .ima instead of .env as extension.

Project-Description: Lurette
parent 3764e8b8
;; This file is automatically generated, editing may cause PRCS to do
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(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 19663 1027092697 51_env_state. 1.24)
(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 14262 1027943375 35_util.ml 1.23)
(test/time.exp 5583 1027066799 b/48_time.exp 1.1)
(test/time.exp 5577 1028297733 b/48_time.exp 1.2)
(source/solver.ml 24274 1027436332 39_solver.ml 1.25)
(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 12222 1027943375 12_lurette.ml 1.43)
(test/temp_int.env 647 1027066799 b/50_temp_int.e 1.1)
(source/lurette.ml 12220 1028297733 12_lurette.ml 1.44)
(source/solver.mli 1003 1027092697 38_solver.mli 1.13)
(source/env.mli 2028 1027349504 15_env.mli 1.15)
(test/heater_float.rif.exp 1453 1027436332 b/30_heater_flo 1.4)
(test/heater_float.rif.exp 1453 1028297733 b/30_heater_flo 1.5)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 8013 1027349504 16_env.ml 1.29)
(make_lurette 1358 1027943375 27_make_luret 1.15)
(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 972 1027066799 b/17_passerelle 1.7)
(test/porte.ima 1021 1027066799 b/16_porte.env 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 1025 1027066799 40_parse_env. 1.9)
(source/sim2chro.mli 1455 1027943375 b/23_sim2chro.m 1.5)
(test/passerelle.ima 972 1027066799 b/17_passerelle 1.7)
(source/ima_exe.ml 11851 1027349504 b/32_ima_exe.ml 1.15)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7755 1027066799 49_eval.ml 1.13)
(source/gen_stubs.ml 33500 1027943375 24_generate_l 1.28)
(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 3397 1027349504 b/46_automata.m 1.2)
(source/sim2chro.ml 2720 1027943375 b/24_sim2chro.m 1.10)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 3638 1027066799 44_formula.ml 1.14)
(test/time.res 5576 1027943375 b/49_time.res 1.4)
(test/time.res 5577 1028297733 b/49_time.res 1.5)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/command_line.mli 1421 1017929190 b/21_command_li 1.6)
(test/porte.env 1021 1027066799 b/16_porte.env 1.7)
(source/env_state.mli 6453 1027092697 50_env_state. 1.21)
(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 1395 1027066799 48_eval.mli 1.10)
(test/usager.ima 493 1027066799 b/14_usager.env 1.8)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 25027 1027943375 17_OcamlMakef 1.33)
(OcamlMakefile 24994 1028297733 17_OcamlMakef 1.34)
(source/command_line_ima_exe.ml 2792 1021651153 b/33_command_li 1.4)
(test/ControleurPorte.rif.exp 4756 1027943375 b/29_Controleur 1.7)
(test/tram.env 1038 1027066799 b/15_tram.env 1.7)
(Makefile.lurette 1960 1027943375 b/38_Makefile.l 1.5)
(test/ControleurPorte.rif.exp 4756 1028297733 b/29_Controleur 1.8)
(Makefile.lurette 1846 1028297733 b/38_Makefile.l 1.6)
(source/show_env.ml 3653 1027349504 43_show_env.m 1.11)
(source/gne.mli 1079 1027066799 b/36_gne.mli 1.2)
(source/automata.ml 15708 1027349504 b/47_automata.m 1.2)
......@@ -62,14 +59,18 @@
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
(source/show_env.mli 1091 1027066799 42_show_env.m 1.7)
(test/Makefile 164 1027943375 c/0_Makefile 1.2)
(test/temp_int.ima 647 1027066799 b/50_temp_int.e 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/temp_float.ima 719 1027066799 b/51_temp_float 1.1)
(test/tram.ima 1038 1027066799 b/15_tram.env 1.7)
(test/heater_float.lus 175 1020068208 b/44_heater_flo 1.1)
(test/vrai_tram.c 3060 1027066799 b/8_vrai_tram. 1.3)
(source/print.mli 773 1027066799 46_print.mli 1.10)
(source/lurettetop.ml 15228 1028297733 c/1_lurettetop 1.1)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(source/graph.mli 2218 1027066799 13_graph.mli 1.9)
(test/heater_int.rif.exp 860 1027436332 b/28_heater_int 1.5)
(test/heater_int.rif.exp 860 1028297733 b/28_heater_int 1.6)
(source/formula.ml 7287 1027066799 45_formula.ml 1.16)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/print.ml 5954 1027066799 47_print.ml 1.17)
......
......@@ -23,27 +23,29 @@ SOURCES_C = $(SUT) sut_stub.c sut_idl_stub.idl \
# $(LURETTE_PATH)/source/pnumsolver.mli $(LURETTE_PATH)/source/pnumsolver.ml
SOURCES_OCAML_COMMON = \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/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/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
SOURCES_OCAML = \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/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/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 \
$(PWD)/lurette_stub.ml \
$(LURETTE_PATH)/source/lurette.mli $(LURETTE_PATH)/source/lurette.ml
$(PWD)/lurette_stub.ml \
$(LURETTE_PATH)/source/lurette.mli $(LURETTE_PATH)/source/lurette.ml
SOURCES = $(SOURCES_C) \
$(SOURCES_OCAML)
$(SOURCES_OCAML_COMMON) $(SOURCES_OCAML)
RESULT = lurette
......
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.33 Mon, 29 Jul 2002 13:49:35 +0200 jahier $
# $Id: OcamlMakefile 1.34 Fri, 02 Aug 2002 16:15:33 +0200 jahier $
#
###########################################################################
# Set these variables to the names of the sources to be processed and
......@@ -497,28 +497,27 @@ dot:
try:
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
lurettetop --sut ControleurPorte --oracle tram_oracle \
-l 10 -tf 2 -td 2 -go tram usager porte passerelle
yvan:
$(LURETTE_PATH)/make_lurette heater Heater_vrai; \
./lurette 50 1 1 Heater.env \
lurettetop --sut heater --oracle Heater_vrai -l 50 -go Heater
vroum:
../make_lurette ControleurPorte vrai_tram nc; \
../make_lurette -sut ControleurPorte -oracle vrai_tram nc; \
/usr/bin/time -v ./lurette 10000 1 1 tram.env usager.env porte.env \
passerelle.env -seed 1015403953 -ns2c --no-oracle
giro_make:
../../make_lurette onlyroll
../../make_lurette -sut onlyroll
giro: giro_make
./lurette 10 1 1 giro.ima
time:
make clean; ../make_lurette ControleurPorte vrai_tram nc; \
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 ;\
......@@ -529,14 +528,14 @@ time:
/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; \
../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; \
../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;\
......@@ -548,18 +547,22 @@ time:
# Non regression test
test1:
../make_lurette ControleurPorte; rm -f ControleurPorte.rif; touch ControleurPorte.rif; \
./lurette 100 10 10 -o ControleurPorte.rif tram.env usager.env porte.env passerelle.env -seed 1013219512 -ns2c ;\
rm -f ControleurPorte.rif; touch ControleurPorte.rif; \
lurettetop --sut ControleurPorte -l 100 -tf 10 -td 10 \
-o ControleurPorte.rif --seed 1013219512 -ns2c -go \
tram usager porte passerelle ;\
rm -f test1.res; diff -u ControleurPorte.rif.exp ControleurPorte.rif > test1.res
test2:
../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 ;\
rm -f heater_int.rif; touch heater_int.rif; \
lurettetop -l 30 -tf 10 -td 10 --sut heater_int --seed 1013219512 \
-ns2c -go -o heater_int.rif -go temp_int ;\
rm -f test3.res; diff -u heater_int.rif.exp heater_int.rif > test2.res
test3:
../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;\
rm -f heater_float.rif; touch heater_float.rif; \
lurettetop -go -l 30 -tf 10 -td 10 --sut heater_float --seed 1013219512 \
-ns2c -o heater_float.rif temp_float;\
rm -f test3.res; diff -u heater_float.rif.exp heater_float.rif > test3.res
test: test1 test2 test3
......@@ -569,7 +572,8 @@ 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 OCAMLFLAGS="-noassert -unsafe"; 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.show_ima OCAMLFLAGS=""; popd
......@@ -577,30 +581,27 @@ show:
heater_make:
$(LURETTE_PATH)/make_lurette heater_int
heater: heater_make
./lurette 30 1 1 temp_int.env --no-oracle
heater:
lurettetop -l 30 -go --sut heater_int temp_int
heaterf_make:
$(LURETTE_PATH)/make_lurette heater_float
heaterf: heaterf_make
./lurette 30 1 1 temp_float.env --no-oracle
heaterf:
lurettetop -l 30 -go --sut heater_float temp_float
# In order to time profile lurette
gprof:
$(LURETTE_PATH)/make_lurette ControleurPorte vrai_tram pnc; \
$(LURETTE_PATH)/make_lurette ControleurPorte -oracle vrai_tram pnc; \
./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; \
make clean; ../make_lurette -sut heater_float -oracle 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; \
make clean; $(LURETTE_PATH)/make_lurette heater_float -oracle always_true_heaterf pnc; \
./lurette 1000 1 1 temp_float.env -seed 1015403953 \
-ns2c --no-oracle ;\
gprof ./lurette > lurette.gprof3 ; \
......@@ -608,7 +609,7 @@ gprof3:
# In order to time profile lurette
ocamlprof:
$(LURETTE_PATH)/make_lurette heater_float vrai_heater_float pbc; \
$(LURETTE_PATH)/make_lurette heater_float -oracle vrai_heater_float pbc; \
./lurette 10 10 10 temp_float.env -ns2c ;\
ocamlprof ../source/solver.ml > prof/solver.count.ml ; \
ocamlprof ../source/automata.ml > prof/automata.count.ml ; \
......@@ -669,7 +670,8 @@ release:
$(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 \
$(LURETTE_PATH)/source/lurette.mli $(LURETTE_PATH)/source/lurette.ml \
$(LURETTE_PATH)/source/lurette.mli $(LURETTE_PATH)/source/lurette.ml \
$(LURETTE_PATH)/source/make_lurette.ml \
$(LURETTE_PATH)/lurette.prj \
lurette-release/source/ ;\
cp $(LURETTE_PATH)/OcamlMakefile lurette-release/ ;\
......@@ -688,7 +690,6 @@ release:
cp $(LURETTE_PATH)/test/ControleurPorte.rif.exp lurette-release/test/;\
cp $(LURETTE_PATH)/test/Makefile lurette-release/test/;\
cp $(LURETTE_PATH)/test/test_gen_stubs.h lurette-release/test/;\
cp $(LURETTE_PATH)/make_lurette lurette-release/ ;\
cp $(LURETTE_PATH)/Makefile.lurette lurette-release/ ;\
cp $(LURETTE_PATH)/bin/Makefile.show_ima lurette-release/bin/ ;\
cp $(LURETTE_PATH)/bin/Makefile.gen_stubs lurette-release/bin/ ;\
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 73)
(Parent-Version lurette 0 72)
(Project-Version lurette 0 74)
(Parent-Version lurette 0 73)
(Version-Log "
source/lurettetop.ml: [new file]
A top level loop for using lurette.
gen_stubs.ml:
sim2chro.ml:
Do not sort varialble lexicographically but according to
sut order.
gen_stubs.ml:
When converting subst list to tuple, do not put fake values
if the list is empty, but raise a failure (assert false).
Do not parse idl output to guess the conversion between ml
and C type but hard code it instead. The rational is that
I was manually calling camlidl here which was confusing
make sometimes.
make_lurette:
exit properly before running lurette whenever something bad
happen during the make.
also remame all .env files using .ima instead of .env as extension.
")
(New-Version-Log "")
(Checkin-Time "Mon, 29 Jul 2002 13:49:35 +0200")
(Checkin-Time "Fri, 02 Aug 2002 16:15:33 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -44,7 +30,7 @@ make_lurette:
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.43 644))
(source/lurette.ml (lurette/12_lurette.ml 1.44 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))
......@@ -91,14 +77,15 @@ make_lurette:
(source/gne.mli (lurette/b/36_gne.mli 1.2 644))
(source/gne.ml (lurette/b/37_gne.ml 1.2 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.1 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.28 644))
; little script that sets env vars and starts the lurette build
(make_lurette (lurette/27_make_luret 1.15 744))
(make_lurette (lurette/27_make_luret 1.15 755))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.33 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.5 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.34 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.6 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))
......@@ -119,16 +106,16 @@ make_lurette:
(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.4 644))
(test/time.exp (lurette/b/48_time.exp 1.2 644))
(test/time.res (lurette/b/49_time.res 1.5 644))
;; Various files used for testing purposes
(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/usager.ima (lurette/b/14_usager.env 1.8 644))
(test/tram.ima (lurette/b/15_tram.env 1.7 644))
(test/porte.ima (lurette/b/16_porte.env 1.7 644))
(test/passerelle.ima (lurette/b/17_passerelle 1.7 644))
(test/temp_int.ima (lurette/b/50_temp_int.e 1.1 644))
(test/temp_float.ima (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))
......@@ -138,9 +125,9 @@ make_lurette:
(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.5 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.7 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.4 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.6 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.8 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.5 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))
......
......@@ -98,7 +98,7 @@ let rec (main : unit -> 'a) =
let res = main2 s n p in
if (not options.step_by_step && options.display_sim2chro)
then Sim2chro.call_sim2chro options.output
else () ;
else () ;
res
with
Failure(errmsg) -> output_string stderr errmsg
......
(*pp camlp4o *)
(*-----------------------------------------------------------------------
** Copyright (C) 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: lurettetop.ml
** Main author: jahier@imag.fr
*)
(** lurette toplevel loop. *)
let usage = "
usage: lurettetop [<options>] [<env ([x] env)*>]
lurettetop is a small top level loop that let one use lurette.
Type help and/or man at the prompt for more info.
Command line <options> are:
"
type flagT = {
mutable sut : string ;
mutable oracle : string option ;
mutable env : string ;
mutable step_nb : int;
mutable formula_nb : int ;
mutable draw_nb : int ;
mutable step_by_step : bool ref ;
mutable display_local_var : bool ref ;
mutable display_sim2chro : bool ref;
mutable seed : int option ;
mutable verbose : bool ref ;
mutable output : string ;
mutable make_opt : string ;
mutable go : bool ref ;
(* a flag to know whether lurette_exe needs to be (re-)build *)
mutable to_build : bool ref
}
let (flag : flagT) = {
sut = "" ;
oracle = None ;
env = "";
make_opt = "" ;
step_nb = 10;
formula_nb = 1 ;
draw_nb = 1 ;
step_by_step = ref false ;
display_local_var = ref true ;
display_sim2chro = ref true ;
seed = None ;
verbose = ref false ;
output = "lurette.rif" ;
go = ref false ;
to_build = ref true
}
let rec speclist =
[
"--sut", Arg.String (fun s -> flag.sut <- s),
"<string>\tFile name of the system under test (without extension).";
"-sut", Arg.String (fun s -> flag.sut <- s), " <string>\n" ;
"--oracle", Arg.String (fun s -> flag.oracle <- Some s),
"<string>\tFile name of the oracle (without extension).";
"-oracle", Arg.String (fun s -> flag.oracle <- Some s), " <string>\n";
"--test-length", Arg.Int (fun i -> flag.step_nb <- i),
"<int>\tNumber of steps to be done";
"-l", Arg.Int (fun i -> flag.step_nb <- i),
("<int>\t\t(default=" ^ (string_of_int flag.step_nb) ^ ").\n");
"--thick-form", Arg.Int (fun i -> flag.formula_nb <- i),
"<int>\tNumber of formula to be drawn at each step";
"-tf", Arg.Int (fun i -> flag.formula_nb <- i),
("<int>\t\t(default=" ^ (string_of_int flag.formula_nb) ^ ").\n");
"--thick-draw", Arg.Int (fun i -> flag.draw_nb <- i),
"<int>\tNumber of draw to be done in each formula ";
"-td", Arg.Int (fun i -> flag.draw_nb <- i),
("<int>\t\tat each step (default=" ^
(string_of_int flag.draw_nb) ^ ").\n");
"--seed", Arg.Int (fun i -> flag.seed <- Some i),
"<int>\t\tSeed the random engine is init with." ;
"-seed", Arg.Int (fun i -> flag.seed <- Some i), " <int>\n";
"--make-opt", Arg.String (fun s -> flag.make_opt <- s),
("<string>\tOptions to call make with when building \n" ^
"\t\t\tlurette_exe (default=\"" ^ flag.make_opt ^ "\").\n");
"--output", Arg.String (fun s -> flag.output <- s),
("<string>\tSet the output file name (default is \"" ^
flag.output ^ "\").");
"-o", Arg.String (fun s -> flag.output <- s), "<string>\n";
"--go", Arg.Set flag.go,
"\t\t\tStart the testing process directly without prompting.";
"-go", Arg.Set flag.go, "\n";
"--step", Arg.Set flag.step_by_step, "\t\tRun lurette step by step." ;
"-s", Arg.Set flag.step_by_step, "\n";
"--verbose", Arg.Set flag.verbose,
"\t\tSet on the verbose mode.";
"-v", Arg.Set flag.verbose,"\n";
"--sim2chro", Arg.Set flag.display_sim2chro,
"\t\tCall sim2chro when lurette_exe resumes.\n";
"--no-sim2chro", Arg.Clear flag.display_sim2chro,
"\tDo not call sim2chro when lurette_exe resumes.";
"-ns2c", Arg.Clear flag.display_sim2chro, "\n";
"--local-var", Arg.Set flag.display_local_var,
"\t\tDisplay environment local variables in sim2chro (default).";
"--no-local-var", Arg.Clear flag.display_local_var,
"\tDo not display environment local variables in sim2chro.\n" ;
"--help", Arg.Unit (fun _ -> (Arg.usage speclist usage ; exit 0)),
"\t\tDisplay this list of options." ;
"-help", Arg.Unit (fun _ -> (Arg.usage speclist usage ; exit 0)),
"";
"-h", Arg.Unit (fun _ -> (Arg.usage speclist usage ; exit 0)),
""
]
(* let pwd = Sys.getcwd () *)
(* *)
(* let (get_fresh_dir : unit -> string) = *)
(* fun _ -> *)
(* let rec get_fresh_dir_rec n = *)
(* let dir = "/tmp/lurette" ^ (string_of_int n) in *)
(* if *)
(* not (Sys.file_exists dir) *)
(* then *)
(* dir *)
(* else *)
(* get_fresh_dir_rec (n+1) *)
(* in *)
(* get_fresh_dir_rec 1 *)
let (build : unit -> bool) =
fun _ ->
print_string " buiding lurette_exe ...\n";
if (flag.sut = "" or flag.env = "")
then
(
print_string "
Both the sut and the env fields should be filled
with set_sut and set_env commands respectively.\n ";
false
)
else
let (oracle, oracle2) =
match flag.oracle with None -> "", "always_true" | Some str -> str, str
in
let gen_stubs_cmd = ("gen_stubs " ^ flag.sut ^ " " ^ oracle ^ "\n")
and make_cmd = ("make " ^ flag.make_opt ^ "\n")
in
Unix.putenv "SUT" (flag.sut ^ ".c");
Unix.putenv "ORACLE" (oracle2 ^ ".c");
print_string gen_stubs_cmd ;
flush stdout ;
if ((Sys.command gen_stubs_cmd) <> 0)
then false
else
(
print_string make_cmd ;
flush stdout ;
if ((Sys.command make_cmd) <> 0)
then false
else true
)
let (run : unit -> bool) =
fun _ ->
let seed_str =
match flag.seed with
None -> ""
| Some i -> (" -seed " ^ (string_of_int i))
and verb_str = if !(flag.verbose) then " -v" else ""
and orac_str =
match flag.oracle with
None -> " --no-oracle"
| Some str -> ""
and outp_str = (" -o " ^ flag.output)
and step_str = if !(flag.step_by_step) then " -s" else ""
and sim2_str = if !(flag.display_sim2chro) then " --call-sim2chro" else " -ns2c"
and dlvr_str =
if !(flag.display_local_var) then " --display-local-var " else " -nlv "
in
let run_cmd =
("./lurette " ^
(string_of_int flag.step_nb) ^ " " ^
(string_of_int flag.formula_nb) ^ " " ^
(string_of_int flag.draw_nb) ^ " " ^
seed_str ^ verb_str ^ orac_str ^ outp_str ^ step_str ^
sim2_str ^ dlvr_str ^ flag.env
)
in
print_string (run_cmd ^ "\n");
(Sys.command run_cmd) = 0
type cmd =
Sut of string
| Oracle of string
| MakeOpt of string
| Env of string
| StepNb of int
| FormulaNb of int
| DrawNb of int
| Step of bool