Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

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

lurette 0.93 Wed, 25 Sep 2002 09:56:41 +0200 by jahier

Parent-Version:      0.92
Version-Log:

source/formula.ml:
source/solver.ml:
source/parse_env.ml:
   Handle boolean equalities with Bdd.eq instead of manually
   converting it with <<and>>, <<not>> and <<or>>.

Project-Description: Lurette
parent 350840f5
......@@ -8,9 +8,9 @@
(bin/Makefile.ima_exe 2013 1027066799 b/41_Makefile.i 1.3)
(test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1)
(source/util.ml 15446 1032510467 35_util.ml 1.26)
(test/time.exp 5577 1030614411 b/48_time.exp 1.3)
(source/solver.ml 24432 1031053030 39_solver.ml 1.26)
(myrules 10432 1032510467 c/14_myrules 1.3)
(test/time.exp 5580 1032940601 b/48_time.exp 1.4)
(source/solver.ml 24592 1032940601 39_solver.ml 1.27)
(myrules 10429 1032940601 c/14_myrules 1.4)
(test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1)
(source/command_line.ml 4625 1031053030 b/20_command_li 1.8)
(source/lurette.ml 13388 1032510467 12_lurette.ml 1.52)
......@@ -19,51 +19,52 @@
(test/heater_float.rif.exp 1459 1032362091 b/30_heater_flo 1.7)
(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)
(make_lurette 1303 1032940601 27_make_luret 1.16)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
(test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(test/porte.ima 1021 1027066799 b/16_porte.env 1.7)
(test/porte.ima 1050 1032789516 b/16_porte.env 1.8)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/rnumsolver.ml 11348 1031053030 b/27_rnumsolver 1.7)
(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)
(ihm/xlurette/xlurette_glade_interface.ml 28245 1032531447 c/15_xlurette_g 1.3)
(test/passerelle.ima 972 1027066799 b/17_passerelle 1.7)
(test/passerelle.ima 984 1032789516 b/17_passerelle 1.8)
(source/ima_exe.ml 12101 1032355637 b/32_ima_exe.ml 1.18)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/control.ml 4416 1030975996 c/4_control.ml 1.3)
(source/eval.ml 7755 1027066799 49_eval.ml 1.13)
(source/gen_stubs.ml 34392 1032355637 24_generate_l 1.34)
(source/parse_env.ml 23768 1032532488 41_parse_env. 1.26)
(source/parse_env.ml 24436 1032940601 41_parse_env. 1.28)
(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 2716 1032355637 b/24_sim2chro.m 1.12)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 3665 1032510467 44_formula.ml 1.15)
(demo/chaudiere/chaudiere.ima 450 1032532488 c/11_chaudiere. 1.4)
(source/formula.mli 3694 1032940601 44_formula.ml 1.16)
(demo/chaudiere/chaudiere.ima 446 1032789516 c/11_chaudiere. 1.5)
(demo/chaudiere/buggy_chaudiere_ctrl.lus 219 1031732392 c/10_buggy_chau 1.1)
(demo/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1)
(test/time.res 5577 1030614411 b/49_time.res 1.6)
(test/time.res 5580 1032940601 b/49_time.res 1.7)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/command_line.mli 1442 1031053030 b/21_command_li 1.7)
(source/env_state.mli 6729 1032355637 50_env_state. 1.23)
(source/rnumsolver.mli 1736 1031053030 b/26_rnumsolver 1.4)
(source/ima_exe.mli 447 1016127950 b/31_ima_exe.ml 1.1)
(source/eval.mli 1395 1027066799 48_eval.mli 1.10)
(test/giro/giro.ima 2800 1031732392 c/6_giro.ima 1.1)
(test/usager.ima 493 1027066799 b/14_usager.env 1.8)
(test/giro/giro.ima 2828 1032789516 c/6_giro.ima 1.2)
(test/usager.ima 495 1032789516 b/14_usager.env 1.9)
(README 74 1011881677 10_README 1.2)
(demo/chaudiere/chaudiere_ctrl.lus 177 1031732392 c/9_chaudiere_ 1.1)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 22378 1032510467 17_OcamlMakef 1.39)
(OcamlMakefile 22373 1032940601 17_OcamlMakef 1.40)
(source/command_line_ima_exe.ml 2792 1031732392 b/33_command_li 1.5)
(test/ControleurPorte.rif.exp 4756 1028297733 b/29_Controleur 1.8)
(Makefile.lurette 678 1031736584 b/38_Makefile.l 1.10)
(test/ControleurPorte.rif.exp 4756 1032789516 b/29_Controleur 1.9)
(Makefile.lurette 698 1032940601 b/38_Makefile.l 1.11)
(source/show_env.ml 3603 1030532285 43_show_env.m 1.12)
(source/gne.mli 1079 1027066799 b/36_gne.mli 1.2)
(source/automata.ml 15818 1032355637 b/47_automata.m 1.4)
(ihm/xlurette/xlurette_glade_main.ml 16664 1032531447 c/12_xlurette_g 1.5)
(ihm/xlurette/xlurette_glade_main.ml 16705 1032789516 c/12_xlurette_g 1.6)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(bin/Makefile.lurette_lib 1768 1031732392 c/2_Makefile.l 1.2)
(bin/Makefile.gen_stubs 472 1030532285 b/42_Makefile.g 1.2)
......@@ -71,11 +72,11 @@
(source/show_env.mli 1091 1027066799 42_show_env.m 1.7)
(test/Makefile 105 1031732392 c/0_Makefile 1.4)
(ihm/xlurette/makefile 783 1032355637 c/16_makefile 1.1)
(test/temp_int.ima 647 1027066799 b/50_temp_int.e 1.1)
(test/temp_int.ima 686 1032789516 b/50_temp_int.e 1.2)
(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 729 1032531447 b/51_temp_float 1.2)
(test/tram.ima 1038 1027066799 b/15_tram.env 1.7)
(test/temp_float.ima 728 1032789516 b/51_temp_float 1.3)
(test/tram.ima 1079 1032789516 b/15_tram.env 1.8)
(test/giro/allocator.lus 1087 1031732392 c/5_allocator. 1.1)
(test/heater_float.lus 175 1020068208 b/44_heater_flo 1.1)
(test/vrai_tram.c 3060 1027066799 b/8_vrai_tram. 1.3)
......@@ -85,7 +86,7 @@
(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 1028297733 b/28_heater_int 1.6)
(source/formula.ml 7305 1032362091 45_formula.ml 1.18)
(source/formula.ml 7428 1032940601 45_formula.ml 1.19)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/print.ml 5883 1030532285 47_print.ml 1.18)
(test/vrai_tram.h 2468 1027066799 b/7_vrai_tram. 1.3)
......
......@@ -10,7 +10,7 @@ ifndef OCAMLFLAGS
OCAMLFLAGS := -noassert -unsafe
endif
LIBS = str lurette_lib # mlpoly
LIBS = str $(LURETTE_PATH)/bin/lurette_lib # mlpoly
INCDIRS = /home/jahier/include
LIBDIRS = /home/jahier/lib
......
......@@ -5,7 +5,7 @@
# For updates see:
# http://www.oefai.at/~markus/ocaml_sources
#
# $Id: OcamlMakefile 1.39 Fri, 20 Sep 2002 10:27:47 +0200 jahier $
# $Id: OcamlMakefile 1.40 Wed, 25 Sep 2002 09:56:41 +0200 jahier $
#
###########################################################################
......@@ -689,7 +689,7 @@ pdfdoc: doc/latex/doc.pdf
doc: htdoc ladoc psdoc pdfdoc
-include /home/jahier/lurette/myrules
-include $(LURETTE_PATH)/myrules
###########################################################################
# LOW LEVEL RULES
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 92)
(Parent-Version lurette 0 91)
(Project-Version lurette 0 93)
(Parent-Version lurette 0 92)
(Version-Log "
source/formula.ml:
source/solver.ml:
source/parse_env.ml:
Allow expr a the lhs of comparison operators.
Make comparison operators prefix instead on infix as
it considerably simplifies the parsing.
Also introduce a == keyword that operates over bool
to disambiguate things (= is the equality for nums,
and == the one for bool. Now the lucky grammar
is truely LL(1), which is nice.
Handle boolean equalities with Bdd.eq instead of manually
converting it with <<and>>, <<not>> and <<or>>.
")
(New-Version-Log ""
)
(Checkin-Time "Mon, 23 Sep 2002 15:58:36 +0200")
(Checkin-Time "Wed, 25 Sep 2002 09:56:41 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -53,19 +47,19 @@ source/parse_env.ml:
(source/util.ml (lurette/35_util.ml 1.26 644))
(source/solver.mli (lurette/38_solver.mli 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.26 644))
(source/solver.ml (lurette/39_solver.ml 1.27 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.4 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.7 644))
(source/parse_env.mli (lurette/40_parse_env. 1.9 644))
(source/parse_env.ml (lurette/41_parse_env. 1.27 644))
(source/parse_env.ml (lurette/41_parse_env. 1.28 644))
(source/show_env.mli (lurette/42_show_env.m 1.7 644))
(source/show_env.ml (lurette/43_show_env.m 1.12 644))
(source/formula.mli (lurette/44_formula.ml 1.15 644))
(source/formula.ml (lurette/45_formula.ml 1.18 644))
(source/formula.mli (lurette/44_formula.ml 1.16 644))
(source/formula.ml (lurette/45_formula.ml 1.19 644))
(source/print.mli (lurette/46_print.mli 1.10 644))
(source/print.ml (lurette/47_print.ml 1.18 644))
......@@ -92,11 +86,11 @@ source/parse_env.ml:
(source/control.ml (lurette/c/4_control.ml 1.3 644))
; little script that sets env vars and starts the lurette build
(make_lurette (lurette/27_make_luret 1.15 755))
(make_lurette (lurette/27_make_luret 1.16 755))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.39 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.10 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.40 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.11 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))
......@@ -118,8 +112,8 @@ source/parse_env.ml:
(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.3 644))
(test/time.res (lurette/b/49_time.res 1.6 644))
(test/time.exp (lurette/b/48_time.exp 1.4 644))
(test/time.res (lurette/b/49_time.res 1.7 644))
;; Various files used for testing purposes
(test/usager.ima (lurette/b/14_usager.env 1.9 644))
......@@ -171,10 +165,15 @@ source/parse_env.ml:
(myrules (lurette/c/14_myrules 1.3 644))
(myrules (lurette/c/14_myrules 1.4 644))
;; Files added by populate at Tue, 24 Sep 2002 15:30:27 +0200,
;; to version 0.92(w), by jahier:
(test/ControleurPorte.lus (lurette/c/17_Controleur 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
......@@ -17,8 +17,6 @@ lurette Makefile.
"
LURETTE_PATH=/home/jahier/lurette/
export LURETTE_PATH
case $# in
##############################################################
......
-include /home/jahier/lurette/VERSION
-include $(LURETTE_PATH)/VERSION
ifndef OCAMLDOT
OCAMLDOT := ocamldot
......@@ -38,8 +38,8 @@ yvan:
vroum:
../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
/usr/bin/time -v ./lurette 10000 1 1 tram.ima usager.ima porte.ima \
passerelle.ima -seed 1015403953 -ns2c --no-oracle
vroum2:
/usr/bin/time -v lurettetop -seed 1015403953 -ns2c -sut ControleurPorte \
......@@ -53,27 +53,27 @@ giro:
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 ;\
/usr/bin/time -o time.res -a -v ./lurette 10000 1 1 tram.ima usager.ima porte.ima \
passerelle.ima -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 ;\
/usr/bin/time -o time.res -a -v ./lurette 10 100 100 tram.ima usager.ima porte.ima \
passerelle.ima -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 ;\
/usr/bin/time -o time.res -a -v ./lurette 100 50 50 tram.ima usager.ima porte.ima \
passerelle.ima -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 \
/usr/bin/time -o time.res -a -v ./lurette 10000 1 1 temp_float.ima -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 \
/usr/bin/time -o time.res -a -v ./lurette 10 100 100 temp_float.ima -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 \
/usr/bin/time -o time.res -a -v ./lurette 10000 1 1 temp_int.ima -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 \
/usr/bin/time -o time.res -a -v ./lurette 10 100 100 temp_int.ima -seed 1015403953 \
-ns2c --no-oracle ;\
\rm -f time.diff; diff -u time.exp time.res >> time.diff; cat time.diff
......@@ -131,19 +131,19 @@ heaterf:
# In order to time profile lurette
gprof:
$(LURETTE_PATH)/make_lurette ControleurPorte -oracle vrai_tram pnc; \
./lurette 10000 1 1 tram.env usager.env porte.env passerelle.env \
./lurette 10000 1 1 tram.ima usager.ima porte.ima passerelle.ima \
-seed 1014422484 -ns2c ;\
gprof ./lurette > lurette.gprof ; \
echo " ---> The result of the profiling is in the lurette.gprof file"
gprof2:
make clean; ../make_lurette -sut heater_float -oracle always_true_heaterf pnc; \
./lurette 10000 1 1 temp_float.env -seed 1015403953 \
./lurette 10000 1 1 temp_float.ima -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 -oracle always_true_heaterf pnc; \
./lurette 1000 1 1 temp_float.env -seed 1015403953 \
./lurette 1000 1 1 temp_float.ima -seed 1015403953 \
-ns2c --no-oracle ;\
gprof ./lurette > lurette.gprof3 ; \
echo " ---> The result of the profiling is in the lurette.gprof file"
......@@ -151,7 +151,7 @@ gprof3:
# In order to time profile lurette
ocamlprof:
$(LURETTE_PATH)/make_lurette heater_float -oracle vrai_heater_float pbc; \
./lurette 10 10 10 temp_float.env -ns2c ;\
./lurette 10 10 10 temp_float.ima -ns2c ;\
ocamlprof ../source/solver.ml > prof/solver.count.ml ; \
ocamlprof ../source/automata.ml > prof/automata.count.ml ; \
ocamlprof ../source/env.ml > prof/env.count.ml ; \
......@@ -225,12 +225,12 @@ release:
cp $(LURETTE_PATH)/myrukes lurette-release/ ;\
cp $(LURETTE_PATH)/OcamlMakefile lurette-release/ ;\
cp $(LURETTE_PATH)/Makefile lurette-release/ ;\
cp $(LURETTE_PATH)/test/usager.env lurette-release/test/;\
cp $(LURETTE_PATH)/test/temp_int.env lurette-release/test/;\
cp $(LURETTE_PATH)/test/temp_float.env lurette-release/test/;\
cp $(LURETTE_PATH)/test/tram.env lurette-release/test/;\
cp $(LURETTE_PATH)/test/porte.env lurette-release/test/;\
cp $(LURETTE_PATH)/test/passerelle.env lurette-release/test/;\
cp $(LURETTE_PATH)/test/usager.ima lurette-release/test/;\
cp $(LURETTE_PATH)/test/temp_int.ima lurette-release/test/;\
cp $(LURETTE_PATH)/test/temp_float.ima lurette-release/test/;\
cp $(LURETTE_PATH)/test/tram.ima lurette-release/test/;\
cp $(LURETTE_PATH)/test/porte.ima lurette-release/test/;\
cp $(LURETTE_PATH)/test/passerelle.ima lurette-release/test/;\
cp $(LURETTE_PATH)/test/heater_int.lus lurette-release/test/;\
cp $(LURETTE_PATH)/test/heater_float.lus lurette-release/test/;\
cp $(LURETTE_PATH)/test/ControleurPorte.ec lurette-release/test/;\
......
......@@ -29,6 +29,7 @@ and
| Or of formula * formula
| IteB of formula * formula * formula
| Not of formula
| EqB of formula * formula
| True
| False
......@@ -84,6 +85,7 @@ end
(* exported *)
type n_expr = num_value NeMap.t
(* exported *)
type atomic_formula =
| Bv of string
| GZ of n_expr (** expr > 0 *)
......@@ -134,6 +136,7 @@ and
(formula_to_string f2) ^ " else " ^
(formula_to_string f3) ^ ")")
| Not(f1) -> ("!(" ^ (formula_to_string f1) ^ ")")
| EqB(f1, f2) -> ((formula_to_string f1) ^ " = " ^ (formula_to_string f2))
| True -> "true"
| False -> "false"
| Bvar(str) -> str
......
......@@ -32,6 +32,7 @@ and
| Or of formula * formula
| IteB of formula * formula * formula
| Not of formula
| EqB of formula * formula
| True
| False
......
......@@ -599,7 +599,9 @@ and (parse_formula: vnt list -> aut_token -> formula) =
f1 = parse_formula vars;
f2 = parse_formula vars
>]
-> Or(And(f1, f2), And(Not(f1), Not(f2)))
->
EqB(f1, f2)
(* Or(And(f1, f2), And(Not(f1), Not(f2))) *)
|
[< 'Genlex.Kwd "true" ; pl = parse_pragma_list
>]
......
......@@ -61,6 +61,12 @@ let rec (formula_to_bdd : env_in -> formula -> Bdd.t * bool) =
in
(Bdd.dand bdd1 bdd2, dep1 || dep2)
| EqB(f1, f2) ->
let (bdd1, dep1) = (formula_to_bdd input f1)
and (bdd2, dep2) = (formula_to_bdd input f2)
in
(Bdd.eq bdd1 bdd2, dep1 || dep2)
| IteB(f1, f2, f3) ->
let (bdd1, dep1) = (formula_to_bdd input f1)
and (bdd2, dep2) = (formula_to_bdd input f2)
......
node ControleurPorte
(demande_pass: bool;
demande_porte: bool;
pass_baissee: bool;
pass_rentree: bool;
porte_ouverte: bool;
porte_fermee: bool;
en_marche: bool;
debut_ramassage: bool;
fin_ramassage: bool)
returns
(baisser_pass: bool;
rentrer_pass: bool;
ouvrir_porte: bool;
fermer_porte: bool;
porte_et_pass_ok: bool);
var
V16_V16_V161_porte_demandee: bool;
V17_V17_V162_pass_demandee: bool;
V18_V18_V163_accepter_demande_porte: bool;
V19_V19_V164_accepter_demande_pass: bool;
V20_V20_V165_en_station: bool;
V21_V21_V166_etat_porte: bool;
V22_V22_V167_etat_pass: bool;
V23_V23_V168_attente_ouverture_porte: bool;
V24_V24_V169_depart_imminent: bool;
V25_V25_V170_depart: bool;
V26_V26_V381_X: bool;
V27_V27_V418_X: bool;
let
baisser_pass = (V27_V27_V418_X and (false -> (pre (not V27_V27_V418_X))));
rentrer_pass = (V17_V17_V162_pass_demandee and porte_fermee);
ouvrir_porte = (if V17_V17_V162_pass_demandee then (pass_baissee and (false
-> (pre (not pass_baissee)))) else (V26_V26_V381_X and (false -> (pre (not
V26_V26_V381_X)))));
fermer_porte = (if V24_V24_V169_depart_imminent then (if
V23_V23_V168_attente_ouverture_porte then porte_ouverte else ((
V17_V17_V162_pass_demandee or V16_V16_V161_porte_demandee) and fin_ramassage)
) else false);
porte_et_pass_ok = (if (not (true -> (pre porte_et_pass_ok))) then (not (
V22_V22_V167_etat_pass or V21_V21_V166_etat_porte)) else (not (baisser_pass
or ouvrir_porte)));
V16_V16_V161_porte_demandee = (if (not (false -> (pre
V16_V16_V161_porte_demandee))) then (demande_porte and
V18_V18_V163_accepter_demande_porte) else (not V25_V25_V170_depart));
V17_V17_V162_pass_demandee = (if (not (false -> (pre
V17_V17_V162_pass_demandee))) then (demande_pass and
V18_V18_V163_accepter_demande_porte) else (not V25_V25_V170_depart));
V18_V18_V163_accepter_demande_porte = (if (not (true -> (pre
V18_V18_V163_accepter_demande_porte))) then V25_V25_V170_depart else (not (
fin_ramassage or (false -> (pre (ouvrir_porte or baisser_pass))))));
V19_V19_V164_accepter_demande_pass = (if (not (true -> (pre
V19_V19_V164_accepter_demande_pass))) then V25_V25_V170_depart else (not (
fin_ramassage or (false -> (pre (ouvrir_porte or baisser_pass))))));
V20_V20_V165_en_station = (if (not (false -> (pre V20_V20_V165_en_station)))
then debut_ramassage else (not V25_V25_V170_depart));
V21_V21_V166_etat_porte = (if (not (false -> (pre V21_V21_V166_etat_porte)))
then porte_ouverte else (not porte_fermee));
V22_V22_V167_etat_pass = (if (not (false -> (pre V22_V22_V167_etat_pass)))
then pass_baissee else (not pass_rentree));
V23_V23_V168_attente_ouverture_porte = (if (not (false -> (pre
V23_V23_V168_attente_ouverture_porte))) then ouvrir_porte else (not
porte_ouverte));
V24_V24_V169_depart_imminent = (if (not (false -> (pre
V24_V24_V169_depart_imminent))) then fin_ramassage else (not
V25_V25_V170_depart));
V25_V25_V170_depart = (en_marche and (false -> (pre (not en_marche))));
V26_V26_V381_X = (V20_V20_V165_en_station and V16_V16_V161_porte_demandee);
V27_V27_V418_X = (V20_V20_V165_en_station and V17_V17_V162_pass_demandee);
tel.
Command being timed: "./lurette 10000 1 1 tram.env usager.env porte.env passerelle.env -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 9.13
System time (seconds): 0.08
Percent of CPU this job got: 92%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:09.91
Command being timed: "./lurette 10000 1 1 tram.ima usager.ima porte.ima passerelle.ima -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 10.44
System time (seconds): 0.10
Percent of CPU this job got: 93%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:11.32
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 187
Minor (reclaiming a frame) page faults: 2452
Major (requiring I/O) page faults: 194
Minor (reclaiming a frame) page faults: 2454
Voluntary context switches: 0
Involuntary context switches: 0
Swaps: 0
......@@ -22,19 +22,19 @@
Page size (bytes): 4096
Exit status: 0
Command being timed: "./lurette 10 100 100 tram.env usager.env porte.env passerelle.env -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 19.03
System time (seconds): 0.10
Command being timed: "./lurette 10 100 100 tram.ima usager.ima porte.ima passerelle.ima -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 23.38
System time (seconds): 0.26
Percent of CPU this job got: 95%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:19.94
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:24.79
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 187
Minor (reclaiming a frame) page faults: 5033
Major (requiring I/O) page faults: 194
Minor (reclaiming a frame) page faults: 17650
Voluntary context switches: 0
Involuntary context switches: 0
Swaps: 0
......@@ -46,19 +46,19 @@
Page size (bytes): 4096
Exit status: 0
Command being timed: "./lurette 100 50 50 tram.env usager.env porte.env passerelle.env -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 42.59
System time (seconds): 0.04
Percent of CPU this job got: 93%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:45.83
Command being timed: "./lurette 100 50 50 tram.ima usager.ima porte.ima passerelle.ima -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 52.13
System time (seconds): 0.86
Percent of CPU this job got: 95%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:55.65
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 187
Minor (reclaiming a frame) page faults: 3099
Major (requiring I/O) page faults: 194
Minor (reclaiming a frame) page faults: 37767
Voluntary context switches: 0
Involuntary context switches: 0
Swaps: 0
......@@ -70,19 +70,19 @@
Page size (bytes): 4096
Exit status: 0
Command being timed: "./lurette 10000 1 1 temp_float.env -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 3.62
System time (seconds): 0.09
Percent of CPU this job got: 88%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.19
Command being timed: "./lurette 10000 1 1 temp_float.ima -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 3.77
System time (seconds): 0.07
Percent of CPU this job got: 89%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.28
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 203
Minor (reclaiming a frame) page faults: 2447
Major (requiring I/O) page faults: 210
Minor (reclaiming a frame) page faults: 2450
Voluntary context switches: 0
Involuntary context switches: 0
Swaps: 0
......@@ -94,19 +94,19 @@
Page size (bytes): 4096
Exit status: 0
Command being timed: "./lurette 10 100 100 temp_float.env -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 7.14
System time (seconds): 0.06
Percent of CPU this job got: 95%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:07.55
Command being timed: "./lurette 10 100 100 temp_float.ima -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 7.90
System time (seconds): 0.26
Percent of CPU this job got: 94%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:08.63
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 203
Minor (reclaiming a frame) page faults: 3453
Major (requiring I/O) page faults: 210
Minor (reclaiming a frame) page faults: 7424
Voluntary context switches: 0
Involuntary context switches: 0
Swaps: 0
......@@ -118,19 +118,19 @@
Page size (bytes): 4096
Exit status: 0
Command being timed: "./lurette 10000 1 1 temp_int.env -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 3.26
System time (seconds): 0.09
Percent of CPU this job got: 84%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:03.97
Command being timed: "./lurette 10000 1 1 temp_int.ima -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 3.24
System time (seconds): 0.08
Percent of CPU this job got: 74%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.43
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 200
Minor (reclaiming a frame) page faults: 2448
Major (requiring I/O) page faults: 207
Minor (reclaiming a frame) page faults: 2450
Voluntary context switches: 0
Involuntary context switches: 0
Swaps: 0
......@@ -142,19 +142,19 @@
Page size (bytes): 4096
Exit status: 0
Command being timed: "./lurette 10 100 100 temp_int.env -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 8.13
System time (seconds): 0.08
Command being timed: "./lurette 10 100 100 temp_int.ima -seed 1015403953 -ns2c --no-oracle"
User time (seconds): 8.83
System time (seconds): 0.23
Percent of CPU this job got: 95%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:08.58