- 04 May, 2018 1 commit
-
-
erwan authored
-
- 27 Apr, 2018 1 commit
-
-
erwan authored
-
- 16 May, 2012 1 commit
-
-
Erwan Jahier authored
Add a --ocamlc-version option to lurettetop and lutin. The idea is to put all the .exp files into a `lurettetop/lutin --ocamlc-version` dir so that I have an .exp file for each ocaml version. If the `lurettetop --ocaml-version`/*.exp does not exist, I generate it. Also, don't non-reg test lucky dirs anymore (because they are boring). Aldo, don't rely on the HOSTTYPE env var, but use Sys.os_type instead.
-
- 07 Mar, 2012 1 commit
-
-
Erwan Jahier authored
-
- 24 Jun, 2011 1 commit
-
-
Erwan Jahier authored
Also, add the oracle outputs in the '.rif'.
-
- 17 Mar, 2010 6 commits
-
-
Erwan Jahier authored
Parent-Version: 1.42 Parent-Version: 1.42 Parent-Version: unstable_1_43.6 Parent-Version: unstable_1_43.10 Parent-Version: unstable_1_43.11 Version-Log: Some progress in the scade tcl gui connection. Add code to be able to parse type definitions that are coming from the Scade tcl Gui. Thanks to that, we do not need to parse generated C header files anymore. Not yet finished. Add a lot of files that were not prcs-ed. source/util.ml source/parse_luc.ml source/lustreExp.ml «from_char_pos_to_line_and_col» that is useg to guess the line and col number from the char number, was returning bad line numbers because cpp adds lines preceeded by «#». Therefore, we add boolean flag to this function so that it does not count such lines if the flag is set to true. source/lurettetop.ml: Sim2chro and gnuplot were called with a bad arg in some cases (i do not remember which ones. Probably on win32. source/parse_c_scade.ml: Enhance the debug messages wrt line numbers. source/lurette_exe.c Add ifdef-ed debug dump (in a log file). install/configure.in: Makefile.common.source: Makefile source/Makefile.show_luc source/Makefile.lucky source/Makefile Minor changes. polka/caml/polka_lexer.mll: Allow ident starting by «_». polka/Makefile.config install/set_env_var.in install/lurettetop.bat.in Minor changes. xlurette/Scade/LuretteGUILauncher.tcl xlurette/Scade/GenMake_l4sim.tcl The lurette dir in the Scade hierarchie is now «lurette/bin» instead of «lurette/win32/bin» (ditto for «lib», and «include»). Some fix after my visit to Esterel (thanks to Aubanel). source/Makefile.luc4ocaml Add mli files. xlurette/Scade/Makefile Add a few rules to copy various files at various places. source/liblutin_c.c This a change from Pascal : « The interval algorithm was completely false ». examples/Makefile Typo. examples/ocaml/crazy-rabbit/rabbit.out examples/lucky/other/test4.rif examples/lucky/other/test4.res examples/xlurette/heater/test3.rif0 A few non-reg tests broke because of the changes to lutin_lib.c. examples/luckyDraw/ocaml/Makefile examples/xlurette/Gyro/Makefile source/Makefile.release Some changes. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.41 Version-Log: source/luc_exe.ml source/command_line_luc_exe.ml source/lurette.ml source/graph.ml source/lucky.mli source/lucky.ml source/util.ml source/formula_to_bdd.ml source/formula_to_bdd.mli source/fair_bddd.ml source/fair_bddd.mli source/bddd.ml source/bddd.mli source/solver.mli source/solver.ml source/polyhedron.ml source/polyhedron.mli source/store.mli source/store.ml source/parse_luc.mli source/parse_luc.ml source/show_env.ml source/env_state.mli source/env_state.ml source/run_aut.mli source/run_aut.ml source/lurettetop.ml source/draw.mli source/draw.ml source/gen_stubs.ml source/parse_c_scade.ml source/ne.ml source/prevar.ml source/prevar.mli source/show_luc.ml utils/lucky.el install/configure.in Makefile.common.source install/Makefile.lurette.in user-rules source/Makefile.lurettetop source/Makefile.gen_fake_lutin source/Makefile.show_luc source/Makefile.lucky source/Makefile.gen_stubs source/Makefile.lurette_lib source/Makefile RUN_ME TODO test/time-joly.exp test/time-joly.res test/time-ecrins.exp ihm/xlurette/xlurette_glade_main.ml ihm/xlurette/xlurette_glade_interface.ml ihm/xlurette/makefile polka/caml/Makefile polka/Makefile.config source/Makefile.gen_fake_lucky install/xlurette_sh.in install/xlurette.sh.in install/xlurette.bat.in install/set_env_var.in install/lurettetop_sh.in install/lurettetop.sh.in install/lurettetop.bat.in install/gen_stubs.sh.in source/poly_draw.ml source/poly_draw.mli source/lustreExp.ml source/lustreExp.mli source/exp.ml source/var.ml source/type.mli examples/xlurette/fault-tolerant-heater/degradable-sensors.luc examples/xlurette/fault-tolerant-heater/heater_control_env.luc examples/xlurette/fault-tolerant-heater/sensors.luc source/parser.mly doc/lurette-man/lurette-man.tex source/parse_sildex.ml test/time-asti.exp RELEASE-NOTES FAQ source/gnuplot-socket.ml source/luc4ocaml.ml source/luc4ocaml.mli source/Makefile.gnuplot-rif source/gnuplot-rif.ml source/luckyDraw.mli source/luckyDraw.ml source/luc4ocaml_nolbl.mli source/luc4ocaml_nolbl.ml source/lucky2lus.ml source/Makefile.luc4ocaml source/Makefile.lurette_ocaml_lib source/Makefile.lurette_debug source/Makefile.luckyDraw source/Makefile.lucky2lus xlurette/Scade/GenMake_l4sim.tcl examples/lucky/external_code/call_external_c_code.luc examples/lucky/external_code/Makefile VERSION install/configure install/set_env_var.bat.in Quite a lot of changes this time... far too much... Fix a at least 5 bugs, and re-organize directories, in particular the test dir. too much to say... * pre pre x was always equal to pre x (bugs introduced in 1.39 or something I think...). * ... One big improvment is that I have completely changed the way runtime automaton are handled, using continuations instead of maitaining an explicit data-structure. This let me reduce the run_aut module by 75 percent, resulting in much clearer code, and less buggy, and more efficient. ouaw! thanks to that, I support DAG now (was rejected before). The executable that do not need env var are no more called via a script that call set_env_var, so that they are fully stand-alone: show_luc, lucky, gen_fake_lucky. This is why util was splitted (util+util2) source/var.ml source/lucaml.ml -> luc4ocaml.ml source/lucaml.mli -> luc4ocaml.mli source/run_aut.ml: Fix a bug during the backtraking in the dynamic tree. source/env_state.ml source/formula_to_bdd.ml sort the list of free index, because the first order of variable is generally better. source/bddd.ml source/bddd.mli source/solver.mli source/solver.ml source/polyhedron.ml source/polyhedron.mli source/store.mli Add the verbosity level in a few functions. source/store.ml FIX A BUG in the bdd traversal. Some branches were never visited because I was raising a No_numeric_solution exception instead od returning an empty store when adding a constraint... This embarassing bug is there from the begining... Ouille! Also, when a valid integer cannot be found, return a wrong one, which is a bug really. But is it better than the current state were raising the no_num expt would cut some branches in the bdd. I will fix that problem later. source/parse_luc.ml source/lustreExp.ml source/lustreExp.mli The list of pre vars was computed with a ref, which is bad. Moreover, the same pre var was created with different indexes, which did not lead to incorrect behavior, but still... source/exp.ml test/bj.luc examples/lucky/external_code/call_external_c_code.luc examples/lucky/external_code/Makefile Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.36 Version-Log: source/lurettetop.ml source/gen_stubs.ml Call the automatically generated oracle <node_name>_always_true.lus instead of always_true. user-rules Put the tgz for the release in joly to save disk space ihm/xlurette/xlurette_glade_main.ml fix a bug where xlurettte was crashing down when the seed field (spin button) was empty. ihm/xlurette/makefile ihm/xlurette/xlurette_glade_main.ml Put a fake min and max value and transform it with sed at the makefile level in order to turn around a bug in glade where one cannot put negative values in spin buttons. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.29 Version-Log: Begin to add an interfacing code for sildex. It seems tp parse sildex-C header files ok, but the C code generator is simply a copy of the poc version.... Begin to move from the use of reg expr to Stream base parser in order to parce header file to get var names and types. source/luc_exe.ml: source/lurettetop.ml: source/command_line_exe.ml: source/command_line_exe.mli: source/command_line_luc_exe.ml: source/command_line_luc_exe.mli: source/util.ml: source/parse_luc.ml: Call a pre-processor on Lucky files before doing anything else via the -pp option Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.26 Version-Log: Add support for a stdin/stdout pipe based mode in lurette. Also make sure that the variable order is the same as in the source .luc file. source/rif.mli: source/rif.ml: New files: move from luc_exe.ml all the stuff that is related to rif input and output. source/sut.mli: source/sut.ml: source/oracle.mli: source/oracle.ml: New files -- code moved from lurette.ml + stuff for handling the pipe mode. source/luc_exe.ml: Add the possibility to launch an oracle from lucky using pipes. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.19 Version-Log: source/store.ml: Fix a bug found by Bertrand where it was necessary to apply substitutions each time a constraint is added Maybe it is sometimes overkill, but it is safe, and performance does not seem to suffer that much. source/parse_luc.ml: Do not open the .luc file twice, and keep the whole file in a string to call the lustre expression parser. This was an attempt to make the debbuger work again with big .luc file, but it fails... The Stream lib really seems to suck AFA ocamldebug is concerned. Also shout when a wrong flag is used. source/lurette.ml: when an assertion is violated, put the corresponding vector in the .rif file. Project-Description: Lurette
-