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 86a22707 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.84 Wed, 11 Sep 2002 10:19:52 +0200 by jahier

Parent-Version:      0.83
Version-Log:         empty
Project-Description: Lurette
parent dad7b1f2
......@@ -6,15 +6,17 @@
(source/env_state.ml 20128 1031053030 51_env_state. 1.26)
(source/graph.ml 2563 1027066799 14_graph.ml 1.7)
(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 14262 1030614411 35_util.ml 1.24)
(test/time.exp 5577 1030614411 b/48_time.exp 1.3)
(source/solver.ml 24432 1031053030 39_solver.ml 1.26)
(myrules 9937 1031732392 c/14_myrules 1.1)
(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 12371 1031053030 12_lurette.ml 1.49)
(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 1028297733 b/30_heater_flo 1.5)
(test/heater_float.rif.exp 1456 1031732392 b/30_heater_flo 1.6)
(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)
......@@ -31,13 +33,16 @@
(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 33416 1031053030 24_generate_l 1.31)
(source/parse_env.ml 22235 1030975671 41_parse_env. 1.22)
(source/gen_stubs.ml 33416 1031732392 24_generate_l 1.32)
(source/parse_env.ml 22510 1031732392 41_parse_env. 1.23)
(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)
(source/sim2chro.ml 2719 1031732392 b/24_sim2chro.m 1.11)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 3638 1027066799 44_formula.ml 1.14)
(demo/chaudiere/chaudiere.ima 442 1031732392 c/11_chaudiere. 1.1)
(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)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/command_line.mli 1442 1031053030 b/21_command_li 1.7)
......@@ -45,35 +50,40 @@
(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)
(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 25248 1030975671 17_OcamlMakef 1.37)
(source/command_line_ima_exe.ml 2792 1021651153 b/33_command_li 1.4)
(OcamlMakefile 21240 1031732392 17_OcamlMakef 1.38)
(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 609 1030614411 b/38_Makefile.l 1.8)
(Makefile.lurette 642 1031732392 b/38_Makefile.l 1.9)
(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 15814 1030975671 b/47_automata.m 1.3)
(ihm/xlurette/xlurette_glade_main.ml 5032 1031732392 c/12_xlurette_g 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(bin/Makefile.lurette_lib 1765 1030525986 c/2_Makefile.l 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)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
(source/show_env.mli 1091 1027066799 42_show_env.m 1.7)
(test/Makefile 104 1030614411 c/0_Makefile 1.3)
(test/Makefile 105 1031732392 c/0_Makefile 1.4)
(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/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)
(source/print.mli 773 1027066799 46_print.mli 1.10)
(source/lurettetop.ml 19952 1031053030 c/1_lurettetop 1.6)
(source/lurettetop.ml 21120 1031732392 c/1_lurettetop 1.7)
(ihm/xlurette/xlurette.glade 24095 1031732392 c/13_xlurette.g 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 1028297733 b/28_heater_int 1.6)
(source/formula.ml 7287 1027066799 45_formula.ml 1.16)
(source/formula.ml 7281 1031732392 45_formula.ml 1.17)
(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)
......
#
# Makefile for lurette based on OcamlMakefile
#
LURETTE_PATH=/home/jahier/lurette
OCAMLMAKEFILE = $(LURETTE_PATH)/OcamlMakefile
OCAMLNCFLAGS = -inline 10 -noassert -unsafe
......
This diff is collapsed.
......@@ -47,7 +47,7 @@ SOURCES = \
RESULT = lurette_lib
all: ncl
all: ncl bcl
-include $(OCAMLMAKEFILE)
node buggy_chaudiere_ctrl(U:real) returns (Heat_on:bool);
let
Heat_on = true -> not pre Heat_on;
-- if U < 15.
-- then false
-- else if U > 20.
-- then true
-- else pre Heat_on;
tel
inputs = (Heat_on , bool),
outputs = (U,float),
locals = (Dudt ,float),
pre = (pre(1,U),float); (pre(1, Dudt), float) ,
ctrl_expr = ,
start_node = 0,
arcs_nb = 0,
nodes_nb = 0,
arcs =
From 0 To 1 With 1:((U = 17.5) && (Dudt = 0.1)) ;
From 1 To 1 With
1:
((U = pre(1,U) + pre(1, Dudt))
&&
( Dudt > (IfThenElseNum Heat_on 0. -5.))
&&
( Dudt < (IfThenElseNum Heat_on 2. 0.))) .
node chaudiere_ctrl(U:real) returns (Heat_on:bool);
let
Heat_on = true ->
if U < 16.
then true
else if U > 19.
then false
else pre Heat_on;
tel
node chaudiere_oracle(U:real; Heat_on:bool) returns (ok:bool);
let
ok = (U < 25.) and (U > 4.);
tel
This diff is collapsed.
open GMain
open GEdit
let pid = ref 0
let (pipe_in, pipe_out) = Unix.pipe ()
let ic = Unix.in_channel_of_descr pipe_in
let oc = Unix.out_channel_of_descr pipe_out
let _ = set_binary_mode_in ic false
let _ = set_binary_mode_out oc false
class customized_callbacks = object(self)
inherit Xlurette_glade_callbacks.default_callbacks
method quit () =
prerr_endline "bye! " ;
Unix.kill !pid 9;
exit 0
method draw_mode_menu_clicked () =
let draw_mode = self#top_xlurette#draw_mode_menu in
(* let draw_mode_list = draw_mode_lbl#children in *)
(* let draw_mode = (List.hd draw_mode_list)#text in *)
(* let cmd_draw_mode = ("set_draw_mode " ^ draw_mode ^ "\n") in *)
let (item_list : GMenu.menu_item list) =
draw_mode#get_menu#children
in
let menu_to_widget menu = (menu:Gtk.menu_item Gtk.obj :> Gtk.widget Gtk.obj) in
let (item_list2 : (Gtk.widget Gtk.obj) list) =
List.map
(fun a -> menu_to_widget a#as_item)
item_list
in
let (active_item : Gtk.widget Gtk.obj) =
(GtkMenu.Menu.get_active (draw_mode#get_menu#as_menu))
in
prerr_endline (GtkBase.Widget.get_name active_item);
if List.mem active_item item_list2
then prerr_endline "oui !!!!!!!!!"
else prerr_endline "non !!!!!!!!!"
method run_lurette () =
let sut_lbl= self#top_xlurette#sut_name in
let sut = sut_lbl#text in
let cmd_sut = ("set_sut \"" ^ sut ^ "\"\n") in
let env_lbl= self#top_xlurette#env_name in
let env = env_lbl#text in
let cmd_env = ("set_env " ^ env ^ "\n") in
let oracle_lbl= self#top_xlurette#oracle_name in
let oracle = oracle_lbl#text in
let cmd_oracle =
if oracle = "" then ""
else ("set_oracle \"" ^ oracle ^ "\"\n") in
let test_length_lbl= self#top_xlurette#test_length in
let test_length = test_length_lbl#text in
let cmd_test_length = ("set_test_length " ^ test_length ^ "\n") in
let formula_nb_lbl= self#top_xlurette#formula_nb in
let formula_nb = formula_nb_lbl#text in
let cmd_formula_nb = ("set_formula_nb " ^ formula_nb ^ "\n") in
let draw_nb_lbl= self#top_xlurette#draw_nb in
let draw_nb = draw_nb_lbl#text in
let cmd_draw_nb = ("set_draw_nb " ^ draw_nb ^ "\n") in
let rif_file_lbl= self#top_xlurette#rif_file in
let rif_file = rif_file_lbl#text in
let cmd_rif_file = ("set_output " ^ rif_file ^ "\n") in
let cmd = "run\n" in
output_string oc cmd_oracle ;
flush oc;
prerr_endline cmd_oracle;
output_string oc cmd_test_length ;
flush oc;
prerr_endline cmd_test_length;
output_string oc cmd_formula_nb ;
flush oc;
prerr_endline cmd_formula_nb;
output_string oc cmd_draw_nb ;
flush oc;
prerr_endline cmd_draw_nb;
output_string oc cmd_rif_file ;
flush oc;
prerr_endline cmd_rif_file;
output_string oc cmd_env ;
flush oc;
prerr_endline cmd_env;
output_string oc cmd_sut ;
flush oc;
prerr_endline cmd_sut;
output_string oc cmd ;
flush oc;
prerr_endline cmd
method save_session () =
output_string oc "pack lurette\n";
flush oc;
prerr_endline "save session ...";()
method save_session2 () =
(*
void
on_button1_clicked (GtkButton *button,
gpointer user_data)
{
GtkWidget *option_menu, *menu, *active_item;
gint active_index;
option_menu = lookup_widget (GTK_WIDGET (button), "optionmenu1");
menu = GTK_OPTION_MENU (option_menu)->menu;
active_item = gtk_menu_get_active (GTK_MENU (menu));
active_index = g_list_index (GTK_MENU_SHELL (menu)->children, active_item);
g_print ("Active index: %i\n", active_index);
}
*)
let (draw_mode : GMenu.option_menu) = self#top_xlurette#draw_mode_menu in
let (menu : GMenu.menu) = draw_mode#get_menu in
let (active_item : Gtk.widget Gtk.obj) =
(GtkMenu.Menu.get_active (menu#as_menu))
in
let (item_list : GMenu.menu_item list) = menu#children in
let menu_to_widget menu = (menu:Gtk.menu_item Gtk.obj :> Gtk.widget Gtk.obj) in
let (item_list2 : (Gtk.widget Gtk.obj) list) =
List.map
(fun a -> menu_to_widget a#as_item)
item_list
in
if List.memq active_item item_list2
then prerr_endline "oui !!!!!!!!!"
else prerr_endline "non !!!!!!!!!";
prerr_endline (GtkBase.Widget.get_name active_item)
end
let main () =
let callbacks = new customized_callbacks in
let xlurette = new Xlurette_glade_interface.top_xlurette callbacks in
(* You should probably remove the next line if you want to use the event masks from glade *)
let _ = GtkBase.Widget.add_events xlurette#xlurette#as_widget [`ALL_EVENTS] in
let _ = xlurette#xlurette#show() in
pid := Unix.create_process "lurettetop" (Array.make 0 "") pipe_in Unix.stdout Unix.stderr ;
Main.main ()
let _ = Printexc.print main ()
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 83)
(Parent-Version lurette 0 82)
(Version-Log "
source/lurette.ml:
source/lurettetop.ml:
source/command_line.ml, .mli:
source/solver.ml:
source/env_state.ml:
source/rnumsolver.ml:
Add 2 news options, --draw-edges ans --draw-verteces that makes
lurette draw among the verteces or on the edges of the convex hull
of solutons.
")
(Project-Version lurette 0 84)
(Parent-Version lurette 0 83)
(Version-Log "")
(New-Version-Log "")
(Checkin-Time "Tue, 03 Sep 2002 13:37:10 +0200")
(Checkin-Time "Wed, 11 Sep 2002 10:19:52 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -32,7 +19,7 @@ source/rnumsolver.ml:
(source/ima_exe.mli (lurette/b/31_ima_exe.ml 1.1 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.17 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.4 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.5 644))
(source/command_line_ima_exe.mli (lurette/b/34_command_li 1.3 644))
;; Sources files for lurette only
......@@ -58,13 +45,13 @@ source/rnumsolver.ml:
(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.22 644))
(source/parse_env.ml (lurette/41_parse_env. 1.23 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.14 644))
(source/formula.ml (lurette/45_formula.ml 1.16 644))
(source/formula.ml (lurette/45_formula.ml 1.17 644))
(source/print.mli (lurette/46_print.mli 1.10 644))
(source/print.ml (lurette/47_print.ml 1.18 644))
......@@ -79,13 +66,13 @@ source/rnumsolver.ml:
(source/automata.ml (lurette/b/47_automata.m 1.3 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.5 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.10 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.11 644))
(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.6 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.31 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.7 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.32 644))
(source/control.mli (lurette/c/3_control.ml 1.2 644))
(source/control.ml (lurette/c/4_control.ml 1.3 644))
......@@ -94,13 +81,13 @@ source/rnumsolver.ml:
(make_lurette (lurette/27_make_luret 1.15 755))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.37 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.8 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.38 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.9 644))
(bin/Makefile.show_ima (lurette/b/40_Makefile.s 1.4 644))
(bin/Makefile.ima_exe (lurette/b/41_Makefile.i 1.3 644))
(bin/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.2 644))
(bin/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.1 644))
(bin/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.2 644))
;; Documentation
(doc/Interface_draft (lurette/19_Interface_ 1.1 644))
......@@ -138,13 +125,39 @@ source/rnumsolver.ml:
(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_float.rif.exp (lurette/b/30_heater_flo 1.6 644))
(test/heater_int.lus (lurette/b/43_heater_int 1.1 644))
(test/heater_float.lus (lurette/b/44_heater_flo 1.1 644))
(test/test_gen_stubs.h (lurette/b/45_test_gen_s 1.1 644))
(test/Makefile (lurette/c/0_Makefile 1.3 644))
(test/Makefile (lurette/c/0_Makefile 1.4 644))
;; Files added by populate at Wed, 04 Sep 2002 09:46:46 +0200,
;; to version 0.83(w), by jahier:
(test/giro/allocator.lus (lurette/c/5_allocator. 1.1 644))
(test/giro/giro.ima (lurette/c/6_giro.ima 1.1 644))
(test/giro/onlyroll.lus (lurette/c/7_onlyroll.l 1.1 644))
;; Files added by populate at Wed, 04 Sep 2002 09:47:29 +0200,
;; to version 0.83(w), by jahier:
(demo/chaudiere/chaudiere_oracle.lus (lurette/c/8_chaudiere_ 1.1 644))
(demo/chaudiere/chaudiere_ctrl.lus (lurette/c/9_chaudiere_ 1.1 644))
(demo/chaudiere/buggy_chaudiere_ctrl.lus (lurette/c/10_buggy_chau 1.1 644))
(demo/chaudiere/chaudiere.ima (lurette/c/11_chaudiere. 1.1 644))
;; Files added by populate at Wed, 04 Sep 2002 09:48:05 +0200,
;; to version 0.83(w), by jahier:
(ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.1 644))
(ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.1 644))
;; Files added by populate at Wed, 04 Sep 2002 17:24:47 +0200,
;; to version 0.83(w), by jahier:
(myrules (lurette/c/14_myrules 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
-include /home/jahier/lurette/VERSION
# Generates emacs tags
tags:
$(OTAGS) -v $(SOURCES) ; cp TAGS ../source
# Generates the modules dependency graph using ocamldot
# (results in lurette.dep.ps and lurette.depfull.ps).
dot:
pushd ../source ; touch $(RESULT).dep.dot ; touch $(RESULT).dep.ps ; \
\rm $(RESULT).dep.ps $(RESULT).dep.dot ; \
touch $(RESULT).depfull.dot ; touch $(RESULT).depfull.ps ; \
\rm $(RESULT).depfull.ps $(RESULT).depfull.dot ; \
ocamldep $(SOURCES_OCAML) | $(OCAMLDOT) -fullgraph -lr > $(RESULT).depfull.dot ; \
ocamldep $(SOURCES_OCAML) | $(OCAMLDOT) > $(RESULT).dep.dot ; \
dot -Tps $(RESULT).depfull.dot > $(RESULT).depfull.ps ; \
dot -Tps $(RESULT).dep.dot > $(RESULT).dep.ps ; \
cp $(RESULT).dep.ps ../doc ; cp $(RESULT).depfull.ps ../doc ; popd
try:
lustre tram_oracle.lus tram_oracle ; \
ec2c tram_oracle.ec ; \
lurettetop --sut ControleurPorte --oracle tram_oracle \
-l 10 -tf 2 -td 2 -go tram usager porte passerelle
yvan:
lurettetop --sut heater --oracle Heater_vrai -l 50 -go Heater
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
vroum2:
/usr/bin/time -v lurettetop -seed 1015403953 -ns2c -sut ControleurPorte \
-l 10000 -tf 1 -td 1 -go tram usager porte passerelle
giro:
lurettetop -sut onlyroll 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 ;\
echo " " >> time.res;\
/usr/bin/time -o time.res -a -v ./lurette 10 100 100 tram.env usager.env porte.env \
passerelle.env -seed 1015403953 -ns2c --no-oracle ;\
echo " " >> time.res;\
/usr/bin/time -o time.res -a -v ./lurette 100 50 50 tram.env usager.env porte.env \
passerelle.env -seed 1015403953 -ns2c --no-oracle ;\
echo " " >> time.res;\
../make_lurette heater_float always_true_heaterf nc; \
/usr/bin/time -o time.res -a -v ./lurette 10000 1 1 temp_float.env -seed 1015403953 \
-ns2c --no-oracle ;\
echo " " >> time.res;\
/usr/bin/time -o time.res -a -v ./lurette 10 100 100 temp_float.env -seed 1015403953 \
-ns2c --no-oracle ;\
echo " " >> time.res;\
../make_lurette heater_int always_true_heater nc; \
/usr/bin/time -o time.res -a -v ./lurette 10000 1 1 temp_int.env -seed 1015403953 \
-ns2c --no-oracle ;\
echo " " >> time.res;\
/usr/bin/time -o time.res -a -v ./lurette 10 100 100 temp_int.env -seed 1015403953 \
-ns2c --no-oracle ;\
\rm -f time.diff; diff -u time.exp time.res >> time.diff; cat time.diff
# Non regression test
test1:
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:
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:
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
ls -l test1.res test2.res test3.res
lib:
pushd ~/lurette/bin ; make -f Makefile.lurette_lib OCAMLFLAGS=""; popd
ima:
pushd ~/lurette/bin ; make -k dc -f Makefile.ima_exe OCAMLFLAGS=""; popd
ltop:
pushd ~/lurette/bin ; make -k dc -f Makefile.lurettetop 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
show:
pushd ~/lurette/bin ; make -k dc -f Makefile.show_ima OCAMLFLAGS=""; popd
heater_make:
$(LURETTE_PATH)/make_lurette heater_int
heater:
lurettetop -l 30 -go --sut heater_int temp_int
heaterf:
lurettetop -l 30 -go --sut heater_float temp_float
# 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 -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 \
-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 \
-ns2c --no-oracle ;\
gprof ./lurette > lurette.gprof3 ; \
echo " ---> The result of the profiling is in the lurette.gprof file"
# In order to time profile lurette
ocamlprof:
$(LURETTE_PATH)/make_lurette heater_float -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 ; \
ocamlprof ../source/env.ml > prof/env.count.ml ; \
ocamlprof ../source/eval.ml > prof/eval.count.ml ; \
ocamlprof ../source/util.ml > prof/util.count.ml ; \
ocamlprof ../source/lurette_stub.ml > prof/lurette_stub.count.ml ; \
ocamlprof ../source/sim2chro.ml > prof/sim2chro.count.ml ; \
ocamlprof ../source/env_state.ml > prof/env_state.count.ml ; \
ocamlprof ../source/lurette.ml > prof/lurette.count.ml ; \
ocamlprof ../source/graph.ml > prof/graph.count.ml ; \
echo " ---> The results of the profiling are in the prof/*.count.ml files"
# Produces an html version of the lurette documentation