Add a lurette-nocaml directory, which mimich the behavior of 'rdbg -lurette'

with lustre-v6 and lutin rdbg-plugins statically linked.

Add rdbg as a submodule, to be able to share files in lurette-nocaml/src/

.gitignore

@@ -153,6 +153,8 @@ renault/
 sim2chrogtk
 source/examples/
 source_save
+lutin-utils/src/lutinUtils.ml
+lutin-utils/src/lutinUtils.mli
 OcamlMakefile.orig
 doc/lurette-man/touch.tex
 examples/not_distributed/
@@ -162,6 +164,12 @@ idees_lutin_lurette.ml
 install/autom4te.cache/requests
 install/config.status
 ocaml-make-release-6.29.3/
+polka/matrix.ml
+polka/matrix.mli
+polka/poly.ml
+polka/poly.mli
+polka/vector.ml
+polka/vector.mli
 polka/caml/matrix.ml
 polka/caml/matrix.mli
 polka/caml/polka_lexer.ml
@@ -252,15 +260,16 @@ RUN_ME
 README-*
 LIMITATIONS.portage_scade
 TODO.SCADEGUI
-
+src
 doc/lutin-tuto/mes_styles.css
 doc/lutin-tuto/my-rdbg-tuning.ml
 doc/lutin-tuto/theme-bigblow.setup
 doc/lutin-tuto/worg-classic.css
 doc/lutin-tuto/worg-r1.css
 doc/lutin-tuto/worg-zenburn.css
-
-examples/lutin/xlurette/call-luciole/my-rdbg-tuning.ml
+doc/lutin-man/lutParser.tex
+doc/lutin-tuto/lutin-tuto-html.html
+doc/lutin-man/main.bbl
 install/
 lnsw
 lnsw-clean
@@ -269,3 +278,8 @@ polka/C/
 polka/caml/
 source/
 Makefile.version
+archive
+my-rdbg-tuning.ml
+rdbg-session.ml
+README.md
+INSTALL.txt
\ No newline at end of file

.gitmodules

+[submodule "rdbg"]
+	path = rdbg
+	url = https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/rdbg.git

AUTHORS.txt

+(* OASIS_START *)
+(* DO NOT EDIT (digest: 92cce301c349ffd5db07434c1bfe26ec) *)
+
+Authors of Lutin:
+
+* Erwan Jahier
+* Pascal Raymond
+* Bertrand Jeannnet (polka)
+* Yvan Roux
+
+Current maintainers of Lutin:
+
+* erwan.jahier@univ-grenoble-alpes.fr
+
+(* OASIS_STOP *)

Lutin.install

@@ -7,7 +7,6 @@ etc: [
 bin: [
   "utils/simec_trap"
   "utils/read-rif.sh"
-  "utils/lurette"
 ]
 
 doc: [

_oasis

 OASISFormat: 0.4
 Name:        Lutin
-Version:     2.47
+Version:     2.48
 Authors:     Erwan Jahier, Pascal Raymond, Bertrand Jeannnet (polka), Yvan Roux
 Maintainers: erwan.jahier@univ-grenoble-alpes.fr  
 License:     CeCILL
@@ -14,7 +14,7 @@ Description:
      automated testing of reactive systems with Lurette.
 BuildTools: ocamlbuild
 PreBuildCommand: make lutin/src/version.ml
-PostInstallCommand: cp utils/simec_trap $exec_prefix/bin; cp utils/read-rif.sh $exec_prefix/bin; cp utils/lurette $exec_prefix/bin
+PostInstallCommand: cp utils/simec_trap $exec_prefix/bin; cp utils/read-rif.sh $exec_prefix/bin
 
 SourceRepository "master"
   Type: git
@@ -64,9 +64,21 @@ Library "lutin-utils"
   CSources: lutinUtils.h,lutinUtils_c.c,lutinUtils_stubs.c,myuid.h,myuid.c
   CCOpt: -fPIC -I$pkg_camlidl -I/usr/local/include/ 
 
+# mimick the behavior of 'rdbg -lurette', but without the dependency on ocaml
+# The drawback is that the lutin and lustre lib are statically part of it
+Executable lurette
+  Path:       lurette-nocaml/src
+  MainIs:     lurette.ml
+  BuildDepends: str,unix,num,dynlink,extlib,camlp4,lutils (>= 1.9),lutin-utils,ezdl,gbddml,polka,camlp4,camlidl,gmp,rdbg-plugin,lustre-v6,lutin
+  NativeOpt: -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind?
+  Install:true
+  CompiledObject: native
+  Install: true
+  CClib: -lcamlidl
+
 # The old lurette. Remove ?
 # it create a weird dependancies on lustre-v6
-Executable lurettetop_exe
+Executable lurette_old
   Path:       ltop/src
   MainIs:     lurettetop.ml 
   BuildDepends: num,str,unix,dynlink,lustre-v6,lutin,ezdl,gbddml,polka,camlp4,camlidl

_tags

 # OASIS_START
-# DO NOT EDIT (digest: 8f1d12a4517d69af223ed101aa5e4c82)
+# DO NOT EDIT (digest: 3085b54b9feb3f809be8464ac1e6da02)
 # Ignore VCS directories, you can use the same kind of rule outside
 # OASIS_START/STOP if you want to exclude directories that contains
 # useless stuff for the build process
@@ -72,11 +72,11 @@ true: annot, bin_annot
 "lutin/src/lutin.cmxs": use_lutin
 "lutin/src/lutin.cmxa": oasis_library_lutin_dlllib
 <lutin/src/*.ml{,i,y}>: package(lutils)
-# Executable lurettetop_exe
-<ltop/src/*.ml{,i,y}>: oasis_executable_lurettetop_exe_ccopt
-"ltop/src/lurettetop.native": oasis_executable_lurettetop_exe_cclib
-"ltop/src/lurettetop.native": oasis_executable_lurettetop_exe_native
-<ltop/src/*.ml{,i,y}>: oasis_executable_lurettetop_exe_native
+# Executable lurette_old
+<ltop/src/*.ml{,i,y}>: oasis_executable_lurette_old_ccopt
+"ltop/src/lurettetop.native": oasis_executable_lurette_old_cclib
+"ltop/src/lurettetop.native": oasis_executable_lurette_old_native
+<ltop/src/*.ml{,i,y}>: oasis_executable_lurette_old_native
 "ltop/src/lurettetop.native": package(camlidl)
 "ltop/src/lurettetop.native": package(camlp4)
 "ltop/src/lurettetop.native": package(dynlink)
@@ -99,6 +99,42 @@ true: annot, bin_annot
 <ltop/src/*.ml{,i,y}>: use_lutin
 <ltop/src/*.ml{,i,y}>: use_lutin-utils
 <ltop/src/*.ml{,i,y}>: use_polka
+# Executable lurette
+"lurette-nocaml/src/lurette.native": oasis_executable_lurette_cclib
+"lurette-nocaml/src/lurette.native": oasis_executable_lurette_native
+<lurette-nocaml/src/*.ml{,i,y}>: oasis_executable_lurette_native
+"lurette-nocaml/src/lurette.native": package(camlidl)
+"lurette-nocaml/src/lurette.native": package(camlp4)
+"lurette-nocaml/src/lurette.native": package(dynlink)
+"lurette-nocaml/src/lurette.native": package(extlib)
+"lurette-nocaml/src/lurette.native": package(gmp)
+"lurette-nocaml/src/lurette.native": package(lustre-v6)
+"lurette-nocaml/src/lurette.native": package(lutils)
+"lurette-nocaml/src/lurette.native": package(num)
+"lurette-nocaml/src/lurette.native": package(rdbg-plugin)
+"lurette-nocaml/src/lurette.native": package(str)
+"lurette-nocaml/src/lurette.native": package(unix)
+"lurette-nocaml/src/lurette.native": use_ezdl
+"lurette-nocaml/src/lurette.native": use_gbddml
+"lurette-nocaml/src/lurette.native": use_lutin
+"lurette-nocaml/src/lurette.native": use_lutin-utils
+"lurette-nocaml/src/lurette.native": use_polka
+<lurette-nocaml/src/*.ml{,i,y}>: package(camlidl)
+<lurette-nocaml/src/*.ml{,i,y}>: package(camlp4)
+<lurette-nocaml/src/*.ml{,i,y}>: package(dynlink)
+<lurette-nocaml/src/*.ml{,i,y}>: package(extlib)
+<lurette-nocaml/src/*.ml{,i,y}>: package(gmp)
+<lurette-nocaml/src/*.ml{,i,y}>: package(lustre-v6)
+<lurette-nocaml/src/*.ml{,i,y}>: package(lutils)
+<lurette-nocaml/src/*.ml{,i,y}>: package(num)
+<lurette-nocaml/src/*.ml{,i,y}>: package(rdbg-plugin)
+<lurette-nocaml/src/*.ml{,i,y}>: package(str)
+<lurette-nocaml/src/*.ml{,i,y}>: package(unix)
+<lurette-nocaml/src/*.ml{,i,y}>: use_ezdl
+<lurette-nocaml/src/*.ml{,i,y}>: use_gbddml
+<lurette-nocaml/src/*.ml{,i,y}>: use_lutin
+<lurette-nocaml/src/*.ml{,i,y}>: use_lutin-utils
+<lurette-nocaml/src/*.ml{,i,y}>: use_polka
 # Executable lutin
 "lutin/src/main.native": oasis_executable_lutin_cclib
 "lutin/src/main.native": oasis_executable_lutin_native

doc/lutin-man/bib.bib

+@article{esterel,
+  title={The Esterel synchronous programming language: Design, semantics, implementation},
+  author={Berry, G{\'e}rard and Gonthier, Georges},
+  journal={Science of computer programming},
+  volume={19},
+  number={2},
+  pages={87--152},
+  year={1992},
+  publisher={Elsevier}
+}
+
+@article{signal,
+  title={Implementation of the data-flow synchronous language signal},
+  author={Amagb{\'e}gnon, Pascalin and Besnard, Lo{\"\i}c and Le Guernic, Paul},
+  journal={ACM SIGPLAN Notices},
+  volume={30},
+  number={6},
+  pages={163--173},
+  year={1995},
+  publisher={ACM}
+}
+@inproceedings{sies,
+    title = {Engineering Functional Requirements of Reactive Systems using Synchronous Languages },
+    author = {Jahier, Erwan and Halbwachs, Nicolas and Raymond, Pascal},
+    year = {2013},
+    shortbooktitle = {SIES},
+    booktitle = {Int. Symp. on Industrial Embedded Systems},
+    address = {Porto, Portugal},
+    team = {SYNC},
+} 
+@inproceedings{tacas,
+    title = {Environment-Model Based Testing of Control Systems: Case Studies },
+    author = {Jahier, Erwan and Djoko-Djoko, Simplice and Maiza, Chaouki and Lafont, Eric},
+    month = {April},
+    year = {2014},
+    hidebooktitle = {TACAS},
+    booktitle = {Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems},
+    optbooktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014), Held as Part of ETAPS 2014.},
+    address = {Grenoble},
+    optpublisher = {LNCS},
+    team = {SYNC},
+} 
+
+@article{RRJ08,
+    title = { Lutin: a language for specifying and executing reactive scenarios },
+    author = {Raymond, Pascal and Roux, Yvan and Jahier, Erwan},
+    year = {2008},
+    journal = {EURASIP Journal on Embedded Systems},
+    team = {SYNC},
+} 
+@ARTICLE{lustre,
+AUTHOR={N. Halbwachs and P. Caspi and P. Raymond and D. Pilaud},
+TITLE={The synchronous dataflow programming language {L}ustre},
+JOURNAL={Proceedings of the IEEE},
+VOLUME={79},
+NUMBER={9},
+PAGES={1305-1320},
+MONTH=sep ,
+YEAR={1991}
+}
+
+@article{lurette,
+   title = {Case Studies with Lurette V2},
+   author = {Jahier, Erwan and Raymond, Pascal and Baufreton, Philippe},
+   journal = {Software Tools for Technology Transfer},
+   month = nov,
+   number = {6},
+   pages = {517--530},
+   opturl = {http://www.springerlink.com/content/u02131123x856227/fulltext.pdf},
+   volume = {8},
+   team = {SYNC},
+   year = {2006}
+}
+@inproceedings{jahier-cstva06,
+   title = {Generating Random Values Using Binary Decision Diagrams and Convex Polyhedra},
+   author = {Jahier, Erwan and Raymond, Pascal},
+   booktitle = {CSTVA},
+   longbooktitle = {Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA'06)},
+   address = {{N}antes, {F}rance},
+   opturl = {http://www.irisa.fr/manifestations/2006/CSTVA06/},
+   pdf = {http://www-verimag.imag.fr/~jahier/cstva06-jahier-raymond.pdf}, 
+  team = {SYNC},
+   year = {2006}
+}

examples/lutin/call-luciole/Makefile

@@ -5,7 +5,7 @@ LURETTE=lurette  \
 	  -oracle "lus2lic heater_control.lus -n not_a_sauna"  \
 	  -env "lutin env.lut -n main -seed 3 -p 2" 
 
-EXPDIR=`lurette --ocaml-version`
+EXPDIR=`rdbg --ocaml-version`
 $(EXPDIR):
 	[ -d $(EXPDIR) ] || (mkdir -p $(EXPDIR) ; make utest)
 

examples/lutin/crazy-rabbit/Makefile

 export OCAMLOPT=ocamlopt
-LTOP=lurettetop_exe
+LTOP=lurette_old
 LIB= `ocamlfind query -r rdbg-plugin -i-format` \
 	  `ocamlfind query -r lutin -i-format`  
 
@@ -25,27 +25,50 @@ clean:
 	rm -rf *.ec *.cm* *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp $(MAIN).opt
 
 
-test.rif:$(EXPDIR) rabbit.cmxs
-	rm -f test.rif0 .lurette_rc
-	$(LURETTETOP) -go  --output test.rif0  \
+test_old.rif:$(EXPDIR) rabbit.cmxs
+	rm -f test_old.rif0 .lurette_rc
+	$(LURETTETOP) -go  --output test_old.rif0  \
 	  -rp "sut:ocaml:rabbit.cmxs:" \
 	  -rp 'env:lutin:rabbit.lut:-main:rabbit:-seed:34:-L:libm.so.6:-loc' && \
-	grep -v "lurette chronogram" test.rif0  | \
+	grep -v "lurette chronogram" test_old.rif0  | \
 	grep -v "lurette Version"   | \
 	grep -v "#seed"   | \
-	grep -v "The execution lasted"| sed -e "s/^M//" > test.rif 
-
+	grep -v "The execution lasted"| sed -e "s/^M//" > test_old.rif 
+
+
+test_old: test_old.rif $(EXPDIR)
+	rm -f test_old1.res
+	diff -B -u -i  $(EXPDIR)/test_old.rif.exp test_old.rif > test_old.res || true
+	cat test_old.res
+	[ ! -s test_old.res ]  && make clean
+
+utest_old:test_old.rif
+	cp test_old.rif $(EXPDIR)/test_old.rif.exp
+
+#XXX do the same as in ~/rdbg/exemples/ocaml/Makefile or extend rdbg so that it
+# handle ocaml plugins ans generates files that looks like ~/rdbg/exemples/ocaml/test.ml
+test_new.rif:$(EXPDIR) rabbit.cmxs
+	rm -f test_new.rif0 .lurette_rc
+	rdbg -lurette  --output test_new.rif0  \
+	  -sut "ocaml:rabbit.cmxs:" \
+	  -env "lutin rabbit.lut -main rabbit -seed 34 -L libm.so.6 -loc" && \
+	grep -v "lurette chronogram" test_new.rif0  | \
+	grep -v "lurette Version"   | \
+	grep -v "#seed"   | \
+	grep -v "The execution lasted"| sed -e "s/^M//" > test_new.rif 
 
-test: test.rif $(EXPDIR)
-	rm -f test1.res
-	diff -B -u -i  $(EXPDIR)/test.rif.exp test.rif > test.res || true
-	cat test.res
-	[ ! -s test.res ]  && make clean
 
-utest:test.rif
-	cp test.rif $(EXPDIR)/test.rif.exp
+test_new: test_new.rif $(EXPDIR)
+	rm -f test_new_old.res
+	diff -B -u -i  $(EXPDIR)/test_new.rif.exp test_new.rif > test_new.res || true
+	cat test_new.res
+	[ ! -s test_new.res ]  && make clean
 
+utest_new:test_new.rif
+	cp test_new.rif $(EXPDIR)/test_new.rif.exp
 
+test: test_old # test_new
+utest: utest_old # utest_new
 
 
 # A FAIRE

examples/lutin/lurettetop/Makefile

 
-LTOP=lurettetop_exe
+LTOP=lurette_old
 
 LURETTETOP=$(LTOP)    \
 	   --test-length 100 --thick-draw 1 \

gbddml/README.org

+A BDD library in C + an ocaml wrapper, by Pascal Raymond.

lurette-nocaml/src/extTool.ml

+../../rdbg/src/extTool.ml
\ No newline at end of file

lurette-nocaml/src/lucioleRun.ml

+../../rdbg/src/lucioleRun.ml
\ No newline at end of file

lurette-nocaml/src/lucioleRun.mli

+../../rdbg/src/lucioleRun.mli
\ No newline at end of file

lurette-nocaml/src/lurette.ml

+(* Time-stamp: <modified the 03/05/2018 (at 15:39) by Erwan Jahier> *)
+(* Mimick the behavior of 'rdbg -lurette', but without the dependency
+   on ocaml *)
+open Event
+
+open RdbgWrapperArgs
+
+let url_doc="http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/"
+
+let _ =
+  lurette := true;
+  usage := (Sys.argv.(0) ^
+               " is equivalent to 'rdbg -lurette', except that the lustre-v6
+and the lutin plugins are statically linked to it, to avoid the need of an 
+ocaml compiler. One can not use other language plugins as 'rdbg -lurette'
+would allow.
+cf also "^url_doc^"
+
+usage: "^ Sys.argv.(0) ^" [<options>] 
+     where <options> are:")
+
+             
+let get_extension f =
+  try
+    let bf = Filename.chop_extension f in
+    let lf,lbf = String.length f, String.length bf in
+    String.sub f (lbf+1) (lf - lbf - 1)
+  with _ -> ""
+
+let args= ref []
+let ml_files = ref []
+
+let add_args arg = 
+  if get_extension arg = "ml" 
+  then 
+    ml_files := arg::!ml_files 
+  else
+    args := (arg::!args)
+
+let others = ref []
+let (add_other : string -> unit) =
+  fun s -> 
+    others := s:: !others
+
+let other_args:string =
+  mkoptab ();
+  Arg.parse_argv Sys.argv !arg_options add_args !usage;
+  String.concat " " (List.rev !others)
+
+(**********************************************************************************)
+let (gen_reactive_program : string -> RdbgArg.reactive_program) =
+  fun str -> 
+  let args = Str.split (Str.regexp "[ \t]+") str in
+  let tool = Filename.basename (List.hd args) in
+  let plugin =
+    match tool with
+    | "lutin"   -> LutinRun.make (Array.of_list args)
+    | "lv6" | "lus2lic" -> Lv6Run.make  (Array.of_list (args@["--expand-io-type"]))
+    | _ -> StdioRun.make str
+  in
+  Ocaml(plugin)
+
+open RdbgArg    
+let _ =        
+  let sut_plugins = List.map gen_reactive_program (!suts @ !suts_nd) in
+  let env_plugins = List.map gen_reactive_program (!envs @ !envs_nd) in
+  let oracle_plugins = List.map gen_reactive_program (!oracles @ !oracles_nd) in
+
+  args.suts <- sut_plugins;
+  args.envs <- env_plugins;
+  args.oracles <- oracle_plugins;
+
+  args.step_nb <- !test_length;
+  args.display_sim2chro <- !display_sim2chro ;
+  args.display_gnuplot <- !display_gnuplot ;
+  args.verbose <- if !verbose then 1 else 0 ;
+  args.output <- !output_file ;
+  
+  args.debug_rdbg <- !drdbg;
+  args.rdbg <- false;
+
+  args.cov_file <- "lurette.cov";
+
+  ()
+
+(**********************************************************************************)
+
+   
+
+let _ =
+  try RdbgRun.lurette_start()
+  with
+  | RdbgRun.OracleError str ->
+     Printf.printf "\027[35m %s \027[00m\n"  str;
+     flush stdout
+                     
+  | Dynlink.Error msg -> (* deadcode *)
+     Printf.eprintf "\n*** error in lurette (Dynlink.loadfile %s).\n*** %s.\n" 
+       (List.fold_left (fun acc x -> acc^" "^x) "" args._others)
+       (Dynlink.error_message msg);
+     RdbgRun.clean_terminate(); 
+     flush stderr;
+     exit 2
+  | Event.End(i) ->
+     RdbgRun.clean_terminate();
+     exit i
+  | pb ->
+     RdbgRun.clean_terminate();
+     output_string args.ocr (Printexc.to_string pb);
+     Printf.printf "bye\n"; flush stdout; exit 2
+;;
+
+let _ =
+  Printf.printf "lurette: bye\n"; flush stdout; exit 0
+

lurette-nocaml/src/rdbgArg.ml

+../../rdbg/src/rdbgArg.ml
\ No newline at end of file

lurette-nocaml/src/rdbgRun.ml

+../../rdbg/src/rdbgRun.ml
\ No newline at end of file

lurette-nocaml/src/rdbgRun.mli

+../../rdbg/src/rdbgRun.mli
\ No newline at end of file

lurette-nocaml/src/rdbgWrapperArgs.ml

+../../rdbg/src/rdbgWrapperArgs.ml
\ No newline at end of file