Skip to content

GitLab

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

lurette 1.18 Thu, 08 Jan 2004 16:02:52 +0100 by jahier 

Parent-Version:      1.17
Version-Log:

source/util.ml:
   Do not quit lurette when launch (Claude) gnuplot when it is not installed.
   More generally, do not abort when a tool launching fails, except
   for compilers (lus2ec an friends).

source/lurettetop.ml:
source/gen_stubs.ml:
source/lurette.ml:
   Make sure everything is recompiled properly when the oracle changes.

   Also add checks wrt its input variable name

Project-Description: Lurette
parent 06abf72c
Hide whitespace changes
Inline Side-by-side
.lurette.prcs_aux
View file @ c3756573
......@@ -3,12 +3,12 @@
(Created-By-Prcs-Version 1 3 3)
(cuddaux/cuddauxGenCof.c 12011 1034006019 c/29_cuddauxGen 1.1)
(source/show_env.mli 1160 1069150632 42_show_env.m 1.11)
(source/util.ml 23034 1073321175 35_util.ml 1.62)
(source/util.ml 23047 1073574172 35_util.ml 1.63)
(test/cygwin-scade/lib_pilot.vsp 1433 1055926783 f/47_lib_pilot. 1.1)
(source/constraint.mli 1706 1069150632 c/18_constraint 1.8)
(test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1)
(mlcuddidl/Changes 129 1071844798 d/10_Changes 1.2)
(TODO 7186 1073401581 d/22_TODO 1.35)
(TODO 5520 1073574172 d/22_TODO 1.36)
(share/gen_fake_lutin.sh.in 115 1063786164 g/30_gen_fake_l 1.1)
(mlcuddidl/rdd.mli 7174 1034006019 c/40_rdd.mli 1.1)
(source/fair_bddd.ml 20532 1073321175 g/38_fair_bddd. 1.6)
......@@ -86,7 +86,7 @@
(source/print.mli 1135 1069150632 46_print.mli 1.14)
(polka/caml/Makefile 6586 1071844798 d/45_Makefile 1.4)
(test/cygwin-scade/det_mvt_mode.saofd 4184 1055926783 f/51_det_mvt_mo 1.1)
(ihm/xlurette/xlurette_glade_main.ml 46762 1071235286 c/12_xlurette_g 1.31)
(ihm/xlurette/xlurette_glade_main.ml 46372 1073574172 c/12_xlurette_g 1.32)
(TAGS 9825 1007379917 21_TAGS 1.6)
(polka/C/main.tex 1961 1047029868 e/14_main.tex 1.1)
(ihm/xlurette/xlurette.glade 103402 1069833150 c/13_xlurette.g 1.25)
......@@ -95,7 +95,7 @@
(test/cygwin-scade/lib_pilot.err 119 1055926783 f/49_lib_pilot. 1.1)
(test/losange.luc 410 1046768487 d/27_losange.lu 1.2)
(test/gyro.rif.exp 10955 1073321175 e/36_gyro.rif.e 1.8)
(test/time-ecrins.exp 9316 1073549199 d/21_time-ecrin 1.38)
(test/time-ecrins.exp 9316 1073574172 d/21_time-ecrin 1.39)
(source/value.ml 2534 1071235286 c/23_value.ml 1.7)
(source/gne.ml 3467 1063029729 b/37_gne.ml 1.6)
(test/cygwin-scade/Pilot.vsp 2075 1055926783 f/40_Pilot.vsp 1.1)
......@@ -142,7 +142,7 @@
(test/cygwin-scade/Pilot.etp 2175 1055926783 f/43_Pilot.etp 1.1)
(polka/C/pkint.h 6036 1047029868 e/12_pkint.h 1.1)
(share/pixmaps/gnuplot-rif.xpm 645 1055926783 f/19_gnuplot-ri 1.1)
(source/gen_stubs.ml 14205 1070981068 24_generate_l 1.51)
(source/gen_stubs.ml 14323 1073574172 24_generate_l 1.52)
(polka/caml/vector.idl 9726 1071844798 d/35_vector.idl 1.3)
(mlcuddidl/README 1574 1034006019 d/8_README 1.1)
(source/sim2chro.mli 1549 1069833150 b/23_sim2chro.m 1.10)
......@@ -168,7 +168,7 @@
(source/ne.ml 10667 1069150632 c/21_ne.ml 1.11)
(source/gen_stubs_poc.ml 8873 1055926783 f/3_gen_stubs_ 1.1)
(source/thickness.ml 1387 1071844798 g/51_thickness. 1.3)
(test/tram/tramway.lus 4060 1073401581 h/1_tramway.lu 1.1)
(test/tram/tramway.lus 4279 1073574172 h/1_tramway.lu 1.2)
(mlcuddidl/session.ml 603 1034006019 c/37_session.ml 1.1)
(demo-xlurette/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1)
(share/Makefile.lurette.in 4495 1071844798 b/38_Makefile.l 1.29)
......@@ -186,7 +186,7 @@
(cuddaux/Makefile 3326 1070981068 c/35_Makefile 1.8)
(polka/C/bit.c 3301 1071844798 e/10_bit.c 1.2)
(source/draw.mli 452 1065787303 f/1_draw.mli 1.2)
(test/time-ossau.exp 9308 1073549199 b/48_time.exp 1.56)
(test/time-ossau.exp 9308 1073574172 b/48_time.exp 1.57)
(polka/caml/polkaIO.ml 1651 1071844798 d/44_polkaIO.ml 1.2)
(mlcuddidl/macros.m4 11392 1071844798 c/49_macros.m4 1.2)
(source/print.ml 5904 1069150632 47_print.ml 1.25)
......@@ -202,7 +202,7 @@
(source/run_aut.ml 22599 1073321175 b/47_automata.m 1.21)
(cuddaux/README 1427 1034006019 c/34_README 1.1)
(mlcuddidl/bdd.ml 11038 1071844798 d/6_bdd.ml 1.2)
(source/lurettetop.ml 47256 1073401581 c/1_lurettetop 1.46)
(source/lurettetop.ml 48342 1073574172 c/1_lurettetop 1.47)
(test/tram/tramway.luc 1015 1073401581 h/2_tramway.lu 1.1)
(source/constraint.ml 3180 1069150632 c/19_constraint 1.10)
(test/structured_type.luc 2224 1063786164 g/32_structured 1.1)
......@@ -280,12 +280,12 @@
(polka/C/polka.h 1791 1071844798 d/50_polka.h 1.2)
(share/pixmaps/ediff-quit.xpm 494 1055926783 f/20_ediff-quit 1.1)
(test/cygwin-scade/Pilot.saofd 3645 1055926783 f/42_Pilot.saof 1.1)
(test/time-moucherotte.exp 6283 1073549199 e/37_time-mouch 1.16)
(test/time-moucherotte.exp 6291 1073574172 e/37_time-mouch 1.17)
(source/command_line_luc_exe.ml 3804 1069833150 b/33_command_li 1.21)
(source/lurette_exe.c 220 1050421093 e/27_lurette_ex 1.2)
(share/pixmaps/close.xpm 803 1055926783 f/21_close.xpm 1.1)
(test/time-CHAILLOL.res 8235 1063029729 g/11_time-CHAIL 1.1)
(test/time-ecrins.res 9316 1073549199 d/20_time-ecrin 1.39)
(test/time-ecrins.res 9306 1073574172 d/20_time-ecrin 1.40)
(source/value.mli 1181 1071235286 c/24_value.mli 1.6)
(polka/Makefile.config 1803 1071844798 e/20_Makefile.c 1.6)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
......@@ -302,7 +302,7 @@
(source/luc_exe.ml 14018 1073549199 b/32_ima_exe.ml 1.44)
(source/gne.mli 1853 1063029729 b/36_gne.mli 1.6)
(test/cygwin-scade/Direction_D1.saofd 1298 1055926783 f/50_Direction_ 1.1)
(source/lurette.ml 18871 1073401581 12_lurette.ml 1.84)
(source/lurette.ml 19781 1073574172 12_lurette.ml 1.85)
(polka/C/Makefile.depend 1081 1047029868 d/46_Makefile.d 1.1)
(share/lucky.bat.in 584 1063786164 g/28_lucky.bat. 1.1)
(share/lucky.sh.in 106 1063786164 g/27_lucky.sh.i 1.1)
......
TODO
View file @ c3756573
......@@ -4,39 +4,10 @@
* Portage pour TNI
* Verifier les msgs d'erreurs qd un maillon de la chaine chie
- compilo lustre error
- outil pas installe (gnuplot, lustre, scade, ...)
- un oracle avec les mauvaises variables
- etc.
*********** BUGS
* no comment ...
-----------------------------------------------------------------------------
cervin:bug[17:31]% ../source/lucky_exe poly.luc poly.luc
*** The variable xx has 2 different min definition, which is forbidden.
-----------------------------------------------------------------------------
* On Wed, 24 Dec 2003, Claude Helmstetter wrote:
-----------------------------------------------------------------------------
> Sous Xlurette,
>
> Quand on est sur une machine ou il n'y a pas gnuplot, on obtient bien un
> message d'erreur clair par contre xlurette ne veut plus lancer d'autres
> actions apres.
-----------------------------------------------------------------------------
* xlurette: le .lus n'est pas recompilé si on le change.
* quand une formule s'avere fausse du point de vue des variables
numeriques, il ne faut pas repartir du haut du graphe, mais backtraker
depuis la branche qui s'avere fausse. Sinon, les probabilités induites
......@@ -50,26 +21,26 @@ et je ne suis plus oblig
pas satisfaisant : pleins de polyhedres intermediaires inutiles
sont calcules, selon l'ordre dans lequel arrivent les contraintes...
* Le remplacement dynaique de .luc est tres surement cassé (les current_nodes
ne sont pas mis a jour)
* Le remplacement dynamique de .luc est tres surement cassé (les current_nodes
ne sont pas mis a jour) -> le retester
****** 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)
* il faut rajouter dans lurette une option --step-inside --step-edges
--step-vertices (et renommer --draw-inside par --try-inside ??)
* le retour au source lutin est sans doute cassé (à voir quand le nouveau compilo
lutin sera la)
* Rajouter un mode ecexe dans lurette
* documenter les options ~default, ~alias, etc.
* Decrire l'heuristique utilisée pour choisir le vecteur qui va servir
dans la suite de l'execution ().
dans la suite de l'execution pour lurette (inside).
* Signaler les approximations faites (en dimension > 1)
- volumes des polyhedres pas calculés (=> pb d'equité)
......@@ -109,9 +80,8 @@ et je ne suis plus oblig
* rajouter une option --reactive ou lucky rend ses valeurs precedentes
si aucune formule n'est satisfiable (ainsi que --reactive-no-warning)
* Rajouter la precision comme un parametre externe
* Integrer la possibilité d'utiliser des types structurés avec lurette et scade
* Rajouter la precision comme un parametre externe de xlurette (deja dispo
dans lurettetop)
* il faudrait au moins pouvoir avoir des pre sur des var de types structurés
......@@ -122,9 +92,6 @@ et je ne suis plus oblig
* Faire un lustre2lucky comme TP avec Yussef
* Faire l'elimination des DAGS, ie,
finir la fonction duplicate_graph_from_node automata.ml
* ZZZ Changer le epsilon en 1/10^p !!!!!
......@@ -133,22 +100,15 @@ et je ne suis plus oblig
(1) Portage Reluc
* Verifier s'il existe des methodes approximatives assez rapides
pour calculer le volume d'un polyhedre
* ajouter les options --product-mode {multiply | arbiter}
qui disent comment on multiplie 2 automates (cf papier)
* Chercher a detecter des egalites lors de l'ajout d'une inegalité.
pour les contraintes de dimension > 1 (cf code commenté dans store.ml)
* compiler sim2chrogtk sous cygwin
* Utiliser l'ordre des parametres plutot que leur noms
Quoique, quand on fait le produit de plusieurs automates,
ca n'est guere pratique...
......@@ -159,11 +119,8 @@ pour calculer le volume d'un polyhedre
* le losange ne passe pas avec polkai et passe avec polkag.
Regarder pourquoi et dire à Bertrand
* Faire un gestionnaire de sessions comme le propose Pascal
* Faire un gestionnaire de sessions dans xlurette comme le propose Pascal
* zipper et dezipper les .rif a la vollée (cf zlib et camlzip)
* giro :
......@@ -183,7 +140,7 @@ pour calculer le volume d'un polyhedre
* xlurette :
- bouton sim2chro ; mettre les locales en vert -> pragma dans sim2chro !!
- bouton sim2chro: mettre les locales en vert -> pragma dans sim2chro !!
* Trouver un controlleur non buggé pour pouvoir mettre un oracle
......@@ -208,28 +165,8 @@ pour calculer le volume d'un polyhedre
variable) puis tirer dans le cube enveloppant.
* dans gne.ml, rajouter partout assertion <<is_a_partition>>
*********** Cosmétisme
* env_state devrait etre un objet ...
* changer le nom du type formula en Formula.t (faire pareil partout)
ce qui devrait permettre d'enlever tout plein de <<open Formula>>
* Le type node n'a rien a faire dans le module formula ...
de meme pour arc_info. Les mettre dans un module type par exemple.
***********************************************************************
*** ??? LIST
* Rajouter un parametre q pour spécifier le nombre de tirage pour
chaque variable numérique ??
ihm/xlurette/xlurette_glade_main.ml
View file @ c3756573
......@@ -178,22 +178,6 @@ let (remove_extension : string -> string) =
if dir = "." then file else (Filename.concat dir file)
let (gen_stubs : (string -> unit) -> string -> string -> string -> unit) =
fun display file node compiler ->
let cmd =
("gen_stubs " ^ (remove_extension file) ^ " " ^ node ^ " " ^ compiler)
in
display cmd;
if
((Sys.command cmd) <> 0)
then
display ("*** gen_stubs failed.\n")
else
display (" ... gen_stubs ok.\n")
(**************************************************************************)
(**************************************************************************)
(** returns the list of lines in ic *)
......@@ -340,6 +324,10 @@ class customized_callbacks = object(self)
str = ""
then
()
else if
str = " "
then
display "\n"
else if
str = "One more loop ? [type any char to stop, `CR' to continue]"
then
......
lurette.prj
View file @ c3756573
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 1 17)
(Parent-Version lurette 1 16)
(Project-Version lurette 1 18)
(Parent-Version lurette 1 17)
(Version-Log "
source/env_state.ml
Fix several bugs in the way automata run in parallel were handled.
(actually, i knew that this feature was broken).
source/util.ml:
Do not quit lurette when launch (Claude) gnuplot when it is not installed.
More generally, do not abort when a tool launching fails, except
for compilers (lus2ec an friends).
Also add support to handle cases where the same variable has
several min (take the max), max (take the min), alias, default,
init (abort) option values.
I am not sure if i should authorize that for min and max though.
source/lurettetop.ml:
source/gen_stubs.ml:
source/lurette.ml:
Make sure everything is recompiled properly when the oracle changes.
Also add checks wrt its input variable name
")
(New-Version-Log ""
)
(Checkin-Time "Thu, 08 Jan 2004 09:06:39 +0100")
(Checkin-Time "Thu, 08 Jan 2004 16:02:52 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -37,7 +38,7 @@ source/env_state.ml
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.16 644))
(source/lurette.ml (lurette/12_lurette.ml 1.84 644))
(source/lurette.ml (lurette/12_lurette.ml 1.85 644))
(source/command_line.ml (lurette/b/20_command_li 1.18 644))
(source/command_line.mli (lurette/b/21_command_li 1.14 644))
......@@ -49,7 +50,7 @@ source/env_state.ml
(source/lucky.mli (lurette/15_env.mli 1.24 644))
(source/lucky.ml (lurette/16_env.ml 1.40 644))
(source/util.ml (lurette/35_util.ml 1.62 644))
(source/util.ml (lurette/35_util.ml 1.63 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.5 644))
(source/formula_to_bdd.mli (lurette/g/35_formula_to 1.6 644))
......@@ -89,7 +90,7 @@ source/env_state.ml
(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.46 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.47 644))
(source/draw.mli (lurette/f/1_draw.mli 1.2 644))
(source/draw.ml (lurette/f/2_draw.ml 1.3 644))
......@@ -98,7 +99,7 @@ source/env_state.ml
(source/gen_stubs_poc.mli (lurette/f/4_gen_stubs_ 1.1 644))
(source/gen_stubs_scade.ml (lurette/f/5_gen_stubs_ 1.2 644))
(source/gen_stubs_scade.mli (lurette/f/6_gen_stubs_ 1.1 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.51 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.52 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.3 644))
......@@ -179,18 +180,18 @@ source/env_state.ml
(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.35 644))
(TODO (lurette/d/22_TODO 1.36 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.12 644))
(share/gnuplot-rif (lurette/e/34_gnuplot-ri 1.5 744))
(share/plot (lurette/e/35_plot 1.6 744))
(test/time-ossau.exp (lurette/b/48_time.exp 1.56 644))
(test/time-ossau.exp (lurette/b/48_time.exp 1.57 644))
(test/time-ossau.res (lurette/b/49_time.res 1.60 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.39 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.38 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.16 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.40 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.39 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.17 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.17 644))
;; Various files used for testing purposes
......@@ -290,7 +291,7 @@ source/env_state.ml
(test/Makefile (lurette/c/0_Makefile 1.14 644))
;; xlurette
(ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.31 644))
(ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.32 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.19 644))
......@@ -494,7 +495,7 @@ source/env_state.ml
;; to version 1.15(w), by jahier:
(test/tram/utiles.lus (lurette/h/0_utiles.lus 1.1 644))
(test/tram/tramway.lus (lurette/h/1_tramway.lu 1.1 644))
(test/tram/tramway.lus (lurette/h/1_tramway.lu 1.2 644))
(test/tram/tramway.luc (lurette/h/2_tramway.lu 1.1 644))
(test/tram/porte.luc (lurette/h/3_porte.luc 1.1 644))
(test/tram/passerelle.luc (lurette/h/4_passerelle 1.1 644))
......
source/gen_stubs.ml
View file @ c3756573
......@@ -72,6 +72,7 @@ let (gen_a_fake_oracle : string -> string -> string -> compiler -> unit) =
put "-- Automatically generated from ";
put sut_h ;
put " by bin/gen_stubs. \n" ;
put "-- Migth be overrided: rename it if you modify it." ;
put "\n";
put "node always_true(";
put (format_string_list "; \n\t" vn_lt_str_l) ;
......@@ -110,7 +111,8 @@ nb: gen_stubs is not meant to be used directly by end-users.
let compile_lustre_program_if_needed lustre_prog lustre_node compiler user_dir tmp_dir =
let compile_lustre_program_if_needed
lustre_prog lustre_node compiler user_dir tmp_dir =
let prog_dir = Filename.dirname lustre_prog in
let save_dir = Sys.getcwd () in
let (gen_c_file, gen_h_file) =
......@@ -121,29 +123,29 @@ let compile_lustre_program_if_needed lustre_prog lustre_node compiler user_dir t
(* | Scade -> *)
(* ((lustre_node ^ "_C/" ^ lustre_node ^ ".c"), *)
(* (lustre_node ^ "_C/" ^ lustre_node ^ ".h")) *)
in
in
let lustre_prog_stat = (Unix.stat lustre_prog) in
Sys.chdir prog_dir;
if
(Filename.check_suffix lustre_prog ".c")
then
(*
if users provide C files, we copy them (.c and .h) to the tmp dir
where c files are expected to be
if users provide C files for the sut and the oracle, we copy
them (.c and .h) to the tmp dir where they are expected to be
*)
let cmd = ("cp -f " ^ (Filename.chop_suffix lustre_prog ".c") ^ ".* " ^ tmp_dir) in
let cmd =
("cp -f " ^ (Filename.chop_suffix lustre_prog ".c") ^ ".* " ^ tmp_dir)
in
if
((Sys.command cmd) <> 0)
then
(
output_string stdout (cmd ^ "\n*** Error.\n") ;
output_string stdout (cmd ^ "\n*** Error: cp failed.\n") ;
flush stdout;
exit 2
)
else
(
output_string stderr (cmd ^ " ok\n");
flush stderr
)
( )
else if
(Filename.check_suffix lustre_prog ".saofdm")
&&
......@@ -151,6 +153,10 @@ let compile_lustre_program_if_needed lustre_prog lustre_node compiler user_dir t
not (Sys.file_exists gen_c_file)
||
not (Sys.file_exists gen_h_file)
||
((Unix.stat gen_c_file).Unix.st_mtime < lustre_prog_stat.Unix.st_mtime)
||
((Unix.stat gen_h_file).Unix.st_mtime < lustre_prog_stat.Unix.st_mtime)
)
then
(
......@@ -167,13 +173,17 @@ let compile_lustre_program_if_needed lustre_prog lustre_node compiler user_dir t
not (Sys.file_exists gen_c_file)
||
not (Sys.file_exists gen_h_file)
||
((Unix.stat gen_c_file).Unix.st_mtime > lustre_prog_stat.Unix.st_mtime)
||
((Unix.stat gen_h_file).Unix.st_mtime < lustre_prog_stat.Unix.st_mtime)
)
then
(* if no .h or .c exists, we try to generate them. *)
(* if no .h or .c exists, or if they are too old, we (re)generate them. *)
(
match compiler with
Verimag ->
output_string stdout (
output_string stderr (
"No " ^ lustre_node ^ ".c or no " ^ lustre_node ^
".h exist(s), so I try to compile " ^ lustre_prog ^
" with node " ^ lustre_node ^
......@@ -182,7 +192,7 @@ let compile_lustre_program_if_needed lustre_prog lustre_node compiler user_dir t
Util.ec2c lustre_node tmp_dir
| Scade ->
output_string stdout (
output_string stderr (
"No " ^ lustre_node ^ ".c or no " ^ lustre_node ^
".h exist(s), so I try to compile " ^ lustre_prog ^
" with node " ^ lustre_node ^
......@@ -221,18 +231,18 @@ let (check_var_type: vn_ct list -> vn_ct list -> vn_ct list -> res) =
if
vl = []
then
output_string stderr "\n"
output_string stdout "\n"
else
List.iter
(fun (v, t) ->
output_string stderr (v ^ " of type " ^ t ^ "; \n"))
output_string stdout (v ^ " of type " ^ t ^ "; \n"))
vl
in
if (not (sut_vars = or_vi)) then
(
output_string stderr "\n*** sut input and output vars are: ";
output_string stdout "\n*** sut input and output vars are: ";
print_var_list sut_vars;
output_string stderr "\n*** whereas oracle inputs are: ";
output_string stdout "\n*** whereas oracle inputs are: ";
print_var_list or_vi ;
print_string("\n*** sut inputs union sut outputs" ^
" should be the same as oracle inputs.\n");
......@@ -247,9 +257,9 @@ let (check_var_type: vn_ct list -> vn_ct list -> vn_ct list -> res) =
)
then
(
output_string stderr "\noracle outputs: ";
output_string stdout "\noracle outputs: ";
print_var_list or_vo ;
Error("\n*** The oracle should have exactly one boolean output.\n")
Error("\n*** The oracle should have exactly one Boolean output.\n")
)
else
Ok
......@@ -297,22 +307,9 @@ let (gen_stubs_file : string -> string -> compiler -> string -> compiler -> unit
Parse_c_scade.get_vn_and_ct_list oracle_h
in
(* Check sut and oracle var names and type consistency *)
let oracle_vi_ord = List.append sut_vi sut_vo in
(* sort vars according to the ordering in the sut (useless?) *)
let v_list_ref = append (fst (split sut_vi)) (fst (split sut_vo)) in
let oracle_vi_ord_decl = sort_vars v_list_ref oracle_vi in
let _ =
(
match check_var_type oracle_vi_ord oracle_vi_ord_decl oracle_vo with
Ok -> ()
| Error(err_msg) ->
(*
Aborts if the var names are inconsistent in the sut and in
the oracle.
*)
failwith err_msg
)
in
(* Generate stubs files "lurette__sut.c.new" and "lurette__oracle.c.new" *)
(
......@@ -327,10 +324,10 @@ let (gen_stubs_file : string -> string -> compiler -> string -> compiler -> unit
match oracle_compiler with
Verimag ->
(Gen_stubs_poc.go
oracle_m "lurette__oracle" oracle_vi_ord oracle_vo)
oracle_m "lurette__oracle" oracle_vi_ord_decl oracle_vo)
| Scade ->
(Gen_stubs_scade.go
oracle_m "lurette__oracle" oracle_vi_ord oracle_vo)
oracle_m "lurette__oracle" oracle_vi_ord_decl oracle_vo)
);
......@@ -450,7 +447,7 @@ let (main : unit -> 'a) =
(if
(oracle_node = "always_true") || (oracle_node = " ")
then
(* to be sure we use a compiler that is installed *)
(* make it sure we use a compiler that is installed *)
sut_compiler
else
oracle_compiler
......
source/lurette.ml
View file @ c3756573
......@@ -47,34 +47,42 @@ let (print_vn_str : out_channel -> (string * string) list -> unit) =
(** [check_var_decl_consistency out_env in_sut out_sut] checks the
consistency of variable declarations made in the environment and the
SUT. It raises an exception if the declarations are inconsistent.
Sut or the oracle.
It raises an exception if the declarations are inconsistent.
*)
let (check_var_decl_consistency : Env_state.t -> (Var.name * string) list ->
(Var.name * string) list -> unit) =
fun state in_sut out_sut ->
(Var.name * string) list -> (Var.name * string) list ->
(Var.name * string) list -> unit) =
fun state in_sut out_sut in_oracle out_oracle ->
(* Retreiving the environment list of variables from the state *)
let in_env_unsorted = state.s.in_vars in
let out_env_unsorted = state.s.out_vars in
let in_env =
List.sort
let in_env1 = List.sort
(fun v1 v2 -> compare (Var.name v1) (Var.name v2)) in_env_unsorted
in
let out_env =
List.sort
and out_env1 = List.sort
(fun v1 v2 -> compare (Var.name v1) (Var.name v2)) out_env_unsorted
in
let in_env =
List.map (fun v -> ((Var.name v), (Var.typ_to_string (Var.typ v)))) in_env1
and out_env =
List.map (fun v -> ((Var.name v), (Var.typ_to_string (Var.typ v)))) out_env1
in
let in_env2 =
List.map (fun v -> ((Var.name v), (Var.typ_to_string (Var.typ v)))) in_env
and out_env2 =
List.map (fun v -> ((Var.name v), (Var.typ_to_string (Var.typ v)))) out_env
(* In order to check the oracle variable decl *)
let all_sut_var = List.sort
(fun v1 v2 -> compare (fst v1) (fst v2)) (in_sut @ out_sut)
in
if not(list_are_equals out_env2 in_sut) then
if
not(list_are_equals out_env in_sut)
then
(
let diff1 = diff_list_as_set out_env2 in_sut in
let diff2 = diff_list_as_set in_sut out_env2 in
let diff1 = diff_list_as_set out_env in_sut in
let diff2 = diff_list_as_set in_sut out_env in
output_string stdout
"\n*** env outputs and sut inputs should be the same.\n";
if diff1 <> [] then
......@@ -92,20 +100,49 @@ let (check_var_decl_consistency : Env_state.t -> (Var.name * string) list ->
flush stdout ;
exit 2
)
else if not(list_are_equals in_env2 out_sut) then
let diff1 = diff_list_as_set in_env2 out_sut in
let diff2 = diff_list_as_set out_sut in_env2 in
else if
not(list_are_equals in_env out_sut)
then
let diff1 = diff_list_as_set in_env out_sut in
let diff2 = diff_list_as_set out_sut in_env in
(
output_string stdout
"\n*** env inputs and sut outputs should be the same.\n";
if diff1 <> [] then
(
print_string "\n\nAppears in the sut outputs, but not in the env inputs:";
print_string