- 17 Mar, 2010 40 commits
-
-
Erwan Jahier authored
Parent-Version: 0.137 Version-Log: AND NOW IT WORKS WITH SCADE !!! (no array neither struct though) source/gen_stubs.ml: source/gen_stubs_common.ml [new file]: source/gen_stubs_common.mli [new file]: source/parse_c_scade.ml [new file]: source/parse_c_scade.mli [new file]: source/*.ml: Add a scade port to lurette. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.136 Version-Log: source/gen_stubs: Fix a bug where the var name ok was clashing with user vars in the generated always true oracle. now i use the name weird_name_to_avoid_clash__ok source/lurettetop.ml: Make sure that the .lus files is less recent than the .c file before running. source/lurettetop.ml: source/gen_stubs.ml: ihm/xlurette/*.ml: Add support for future handling of the scade compiler. Currently, returns a msg saying it that the scade port is not implemented. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.135 Version-Log: source/parse_env.ml: source/formula.ml: source/formula.mli: source/env_state.ml: source/env_state.mli: source/automata.ml: Change the format of pragma to stick with how they are defined in the DC ref man. Also take into account programs that were added by yvan that let one know which control point in the source lutin program each lucky node correspond to. source/lurette.ml: Display a better error msg when the sut and env vars do not match. source/sim2chro.ml: Variables were not display in the same order as in their declaration (bug introduced in the previous change). source/lurettetop.ml: The clean command does not remove everything in the tmp dir but only the generated files. ihm/xlurette/xlurette_*.ml: The naming of rif files was not working properly. Add a clean-up button. user-rules: <various other makefiles>: Abstract away a few hard-code env var so that its works on cygwin Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.134 Version-Log: Implement a check_assertion rule that checks every programs assertions. source/*.ml: Consistently display the help msg on stderr if something bad happened, and on stdout if --help is provided at the command line. source/lurette.ml: source/sim2chro.ml: Fix a bug (found by Nicolas Dervaux) where the sut output var were not in the same order than in their declaration. Also, interchange input by output in the produced rif file, since it is more sensible this way from the tester point of view. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.133 Version-Log: Various changes related to the packaging of lurette. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.132 Version-Log: source/gen_stubs.ml: source/ocaml2C.idl: use double instead of floats at the C level. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.131 Version-Log: Fix 3 bugs discovered by Pascal. one was due to a confusion with variable starting with _pre during formula_to_string. another one was in store.ml: i was not reinjecting the solutions when retriving values from store.substl a third one was due to the fact that I was not applying substitution rigth-to-left whereas I should. source/luc_exe.ml: Add 2 options --help and --step-number that let one set a bound on the number of steps to perform. source/env.ml: source/parse_env.ml: Provide a mean to give default values to pre variables. ihm/xlurette/xlurette_glade_main.ml ihm/xlurette/xlurette.glade: Add Combo boxes to browse lustre file nodes. source/ Add the possibility to give default vales to pre variables. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.130 Version-Log: Remove the need of the ocaml compilers to be able to use lurette. The idea is to link the final executable withh the C compiler instead of using ocamlopt. source/lurette.ml: source/gen_stubs.ml: The stubs files that are generated are ow completely different. The process is much more simple BTW. Now, idl files are no more generated dynamically. The only files that are generated are C files that interfaces the sut and the oracle with lurette. /source/lurettetop.ml: Add the USER_TESTING_DIR env variable. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.129 Version-Log: empty Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.128 Version-Log: source/parse_env.ml: Enhance parsing error messages. source/util.ml: source/lurettetop.ml: check for LURETTE_PATH only in lurettetop because it is the only one that really needs it. Also moves show_luc, gen_stubs, and co there for the same reason. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.127 Version-Log: source/parse_env.ml: source/env_state.ml: source/env_state.mli: Add support for transient /recurrent nodes (not plugged yet). source/parse_env.ml: source/solver.ml: source/formula.ml source/formula.mli: test/*.luc: Add the possibity to define formula and num expr aliases (a request from Bertrand). test/losange.luc: [new file] test/losange-3d.luc: [new file] test/test_losange.lus: [new file] user-rules: Add the losange in the non-regression test source/luc_exe.ml: source/command_line_luc_exe.ml: Add an option that lets one see local vars in lucky output. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.126 Version-Log: source/command_line_luc_exe.ml: source/command_line_luc_exe.mli: source/luc_exe.ml: source/store.ml: source/lurette.ml: source/lurettetop.ml: Put back the verteces draw. It was not such a great idea to remove after all... Also change verteces into vertices (oops...). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.125 Version-Log: source/command_line_luc_exe.ml: source/command_line_luc_exe.mli: source/command_line.ml: source/command_line.mli: source/luc_exe.ml: source/lurette.ml: source/lurettetop.ml: Add the possibility to set the precision from lucky and lurette command lines. Remove the draw-vertices stuff. source/command_line_luc_exe.ml: source/command_line_luc_exe.mli: source/luc_exe.ml: Also add the --edges and the inside options for lucky. source/parse_env.ml: Allow to forget empty fields in the automata format. source/store.ml: Plug the new drawing heuristic Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.124 Version-Log: source/parse_env.ml: Make most fields of the automata syntax optional so that people are not obliged to refer to empty list of, eg, formula. Also add a field formula that let one defines global formula. This field is currently unplugged (ie, it parses, but the information contained in that fied in ignored). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.123 Version-Log: Implement the polyhedron drawing primitives. source/util.ml.in: Change my_string_of_float so that it truncates floats 4 digits after the dot. The rational is that, for testing, we do not care the extra precision and too much precision may kill Polka. This precison ougth to be a parameter though. source/solver.ml: source/polyhedron.ml: source/store.ml: Implement the polyhedron drawing primitives. source/store.ml: Apply the substitutions in store.subtsl to the cstr to add. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.122 Version-Log: source/rnumsolver.mli: source/rnumsolver.ml: source/store.mli: source/store.ml: Rename rnumsolver into store. source/solver.ml: source/parse_env.ml: Do not explicitely handle dis-equalities but transform it using not and = instead. The rational for this change is to avoid code duplication (which was buggy !!!), but also to allow handle dis-equalities with the optimized algorithm I had for eqalities (for free) ! Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.121 Version-Log: When delayed constraints are remaining at bdd leaves, we were printing a message saying that one shoud use a polyhedron solver based instead. Now, I really call such a polyhedron solver in order to solve those constraints. This means that I use to different solvers to handle interval and polyhedron of dimension > 1. It also means that the satisfiability of constraints over polyhedra is only checked at bdd leaves, which, in some circumstances, migth be inefficient. The point is that, if we chose to check the formula satisfiability during the bdd traversal, we take the risk that a very polyhedron is created whereas it was not necessary (because of forthcoming equalities). And creating polyhedron with big (>15) dimension simply runs forever, which is really bad. nb : drawing in poyhedron not yet plugged. source/polyhedron.ml: source/polyhedron.mli: (new files) misc functions over polyhedra. The rational for creating that file is that rnumsolver is already much too big (and should be splitted some more btw). source/solver.ml: One of the main change is that now, draw_in_bdd returns 2 stores. One is Range based, the other one is polyhedron-based. source/rnumsolver.mli: source/rnumsolver.ml: Add the function switch_to_polyhedron_representation which handle delayed constraint if necessary. It is meant to be called at bdd leaves. source/solver.ml: source/rnumsolver.ml: Also do not use split_store anymore but add_constraint. This allows a much more elegant and efficient implementation of draw_in_bdd and draw_in_bdd_eq (Now the store is buid when and only when a new branch should be tried because of backtracking). It is also more efficient. source/constraint.mli source/constraint.ml source/ne.mli source/ne.ml Implement get_vars that retreive the variables occuring in a contraint or an expression. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.120 Version-Log: source/pnumsolver.ml: source/pnumsolver.mli: [new files] Implements a numeric solver based on Polka. (not plugged yet). source/rnumsolver.ml: Reimplement split_store so that it uses 2 calls of add_constraint instead of doing the work twice inside split_store (in order to avoid code duplication). Also, whenever delayed constraints becomes of dimension 1, when a add_constraint binds a value, add them to the store. Enhance error msgs whenever int and float are mixed in the same lucky expressions. source/rnumsolver.ml: source/ne.ml: rename Ne.resolve_triangular_system into get_subst_from_solved_system and move it into rnumsolver. The rational is that is was not really solving any triangular system: the system ougth to be already solved. source/parce_env.ml: Set the max_float to max_int, otherwise, the conversion into polka rational fails... Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.119 Version-Log: source/solver.ml: source/rnumsolver.ml: replace split_store_eq by add_eq_to_store as split_store_eq was simply calling split store and appendind its result, it is simplier to just call slipt_store from solver.ml ... Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.118 Version-Log: user-rules: Add the name of the host in the timing result files. Also runs the timing tests on ecrins. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.117 Version-Log: source/command_line_luc_exe.ml: Various minor fixes in printed messages. remark. The increasing of minor page faults is due to the fact that ossau kernel has been upgraded ... Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.116 Version-Log: Various minor fixes in the documentation + Use a version of ocaml-3.06 that has been configured with -no-curses, which make things sligthly slower, but that avoid the need to find the curses lib... source/ne.ml: source/*.ml: Ne.find now returns an option value instead of raising a Not_found exp, which was not trap in some circumstances... source/ne.ml: Also, fix a couple of bugs where the code was supposing (falsely) that the constant (empty string) was always in the Map. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.115 Version-Log: source/solver.ml: Give a better error message when users do not initialize pre vars. source/parse_env.ml: source/formula.ml: source/prevar.ml/mli: (new files) Put here everything that handles the internal representation of pre var names. Pretty print internal pre var names. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.114 Version-Log: source/automata.ml: Fix a bug where esp loops were not always cutted properly in some cases. source/show_env.ml: Truncate too long for in the dot output (which bugs dot or gv). ihm/xlurette/xlurette_glade_main.ml: Accept both .lut or .lut files as anv files, and make the show buttons behave properly in both cases. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.113 Version-Log: source/parse_env.ml: When floats output vars are not constraint, use [-10^11, 10^11] as default domain. The rational for this change is that sim2chro does not seem to be able to print bigger floats (probably because it does not understand the 123e+234 notation. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.112 Version-Log: source/show_luc.ml: source/lurette.ml: source/parse_env.ml: Enhance error msgs during the .luc parsing. Add the line number. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.111 Version-Log: source/parse_poc.ml: (new file) source/gen_stubs.ml: put everything that is related to poc parsing into parse_poc.ml. source/gen_fake_lutin.ml: (new file) source/parse_poc.ml: (new file) source/Makefile.gen_fake_lutin: (new file) When no .lut is provided, we generate a fake one. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.110 Version-Log: source/util.ml: source/formula.ml: source/lurette.ml: Only print one counter example if the test failed. source/lurettetop.ml: source/gen_stubs.ml: try to guess the node name in lurettetop rather than in gen_stubs if not given. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.109 Version-Log: source/util.ml: source/lurettetop.ml: source/gen_stubs.ml: ihm/xlurette/xlurette_glade_main.ml: ihm/xlurette/xlurette.glade: Add the possibility to specify te sut and the oracle main node (to feed the lustre compiler). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.108 Version-Log: ihm/xlurette/xlurette_glade_main.ml: source/lurettetop.ml: Retreive and print the pid of lurette to be able in xlurette to kill the current run. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.107 Version-Log: source/lurette.ml: source/command_line.ml source/command_line.mli source/util.ml: source/lurettetop.ml: use crete_process instead un sys.command to call lurette from lurettetop ihm/xlurette/xlurette_glade_main.ml: Put the newly generated random seed into the manual text box. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.106 Version-Log: source/lurettetop.ml: ihm/xlurette/.ml: fix a bug when reading the .lurette_rc where the the env were added instead of beinf overrided when they were both specified in the rc file and as a comd line option. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.105 Version-Log: source/lurettetop.ml: Add a --prefix <string> option that is added before the call to lurette (usefull, eg, for timing purpuses). source/lurettetop.ml: source/lurette.ml: source/command_line.ml: ihm/xlurette/* Add a ---show-step options that let one control whether or not the step number is printed. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.104 Version-Log: ihm/xlurette/*: Look up the pipe every 1/10 sec. instead of reading it after each command until a certain string is encoutered. It make the code more robust (no protocol), it avoid that xlurette is blocked during the process. Moreover, it let the progress bar works gently. Add a stop button that sends a sigint to lurettetop that ougth to stop the current execution (does not work, why?). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.103 Version-Log: source/lurettetop.ml: source/util.ml: use explicit file name so that, e.g., show_luc, is always able to find the file it is supposed to show. Allow users to put extension or not for the sut or oracle files, being at the prompt or at the invocation. cp lurette.ml and lurette.mli in the temp dir and compile it there to avoid that everyone is writing on the source dir which prevent the next user to use lurette... Makefile.common.in: INCDIRS Ocamlmakeke file var is not supposed to contains path to .h C files to include but .mli ocml ones !!! Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.102 Version-Log: Add autoconf aupport. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.101 Version-Log: Add cuddaux and mlcuddidl to the project. Also clean-up Makefiles etc in order to make the installation process as automatic as possible. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.100 Version-Log: Rename any occurence of ima by luc or lucky. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.99 Version-Log: source/gen_stubs: Make sure we are in the rigth directory we calling lus2ec and ec2c. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.98 Version-Log: source/solver.ml: source/rnumsolver.mli,.ml: source/constraint.ml,.mli: Split the Constraint.t type into t and ineq where inequalities are in ineq. The rational is that most operations on constaint.t are actually done on ineq. This change therefore avoid pattern like <<_ -> assert false>> and let the type checher check that sort of things. Project-Description: Lurette
-