- 17 Mar, 2010 40 commits
-
-
Erwan Jahier authored
Parent-Version: 1.18 Version-Log: Add support for structured types in lurette. source/type.ml/.mli: New file containing lucky var type definition (moved from var.ml). source/gen_stubs_*.ml: source/parse_c*.ml: Project-Description: Lurette
-
Erwan Jahier authored
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
-
Erwan Jahier authored
Parent-Version: 1.16 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). 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. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.15 Version-Log: source/lucky.ml: Fix a bug (revealed by Claude) that was appering when several automata were run in parallel: the symptom was that several values were generated for some outputs. The bug was due to the fact that the order of the list of paths (used to, among other things, to retreive the current node) was wrong: the consequence was that the automata order was different from the one of expected variables, hence it was also generated values for those extra variables for automata where it was not necessary. source/lurette.ml: launch the oracle checking for the outputs of the step also... test/*: Add non reg test for that bug and the previous one. source/luc_exe.ml: input and output rif declaration where intertwined. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.14 Version-Log: source/util.ml: Redirect third party tools error msgs in the main windows rather than in the misc. source/lucky.ml: source/run_aut.ml: Indicate the removed paths in the verbose mode only. source/run_aut.ml: Fix a bug where the execution was looping when no more formula were satisfiable (when all formula mode was on). source/fair_bddd.ml: Raise No_numeric_solution if the polyhedron volume is smaller then epsilon. source/lurettetop.ml: Recompile the Lustre program if necessary. source/gen_fake_lutin.ml: Declare the variables in the same order as in the sut program. source/store.ml: source/polyhedron.ml: Fix a bug signaled by Claude where lurette was aborting when solving integer constraints. It was due to a bad implementation of is_point_in_poly which did not convert floats to ints when necessary (this bug was introduced rather recently when i provided my own version of is_point_in_poly... and of course i have non reg-test with integer constraints...). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.13 Version-Log: gen_stubs_scade.ml: fix a bug which was causing a bus error: to fix it, i simply delete a couple a extras &... Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.12 Version-Log: aesthetic changes in mli files so that the automatically generated doc looks ok. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.11 Version-Log: Various fixes in the C scade parsing. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.10 Version-Log: No more side effects are done via the Env_state module. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.9 Version-Log: removing of Env_state module -- part 1 Now env_step and env_try are fully functionnal (no side-effects). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.8 Version-Log: A lot (too much...) of changes, mainly renaming files, and types, and functions, change the interface, move from one module to another, etc. Bref, a lot of cleanning. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.7 Version-Log: Implement a new drawing policy in polyhedron. The idea is to base the base (which is not so expensive), and to draw in othogonal hypercube that is as small as possible until a point in the polyhedron is found. However, it may happens in high dimension (>4) that the volume of the cube is much bigger. In that case, after a few tries, i call the old (unfair) method. polyDram.ml/mli: new module containing all the thing related to the drawing inside a convex polyhedron. Give up the idea of random walk (not clear what should be the default step and length in big dimension). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.6 Version-Log: source/fair_bddd.ml: [new] source/fair_bddd.mli: [new] The same as bddd, but taking polyhedron volume into account. source/bddd.ml: It is useless to store both bdd and not bdd, because it is just so easy to recompute the sol nb of not bdd (by switchinf the pair of sol numbers!). source/lurettetop.ml: source/lurette.ml: source/luc_exe.ml: add a --compute-poly-volume option that makes lurette use fair_bddd instead of bddd. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.5 Version-Log: source/solver.ml: source/bddd.ml: source/env_state.ml: Deal with the solution number table global var at the bddd module level, not at the env_state level. The rationale is that it makes it possible to have a abstract snt type that can be easily change after. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.4 Version-Log: Split up solver.ml into 3: solver.ml, formula_to_bdd.ml, and bddd.ml. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.3 Version-Log: source/store.ml: source/solver.ml: use map instead as hashtbl for the range base store. It is much less error-prone (evil side effect!), leads to clearer code (no need to copy the store, which was particularly bad when done outside that module...), and is as efficient. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.2 Version-Log: source/store.ml: source/store.ml: source/solver.ml: Add a numeric thickness at the numeric level. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 1.1 Version-Log: share/ Do not use the lucky_init.sh to set up env var anymore but wrap executables by scripts that set them. test/ Add more test cases. source/lurettetop.ml: lauch gnuplot via an xterm to turn around a buggy behavior of gnuplot (this fix is far from ideal however, because the xterm window have to be killed manually, which is boring). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.143 Version-Log: Major change in the lucky syntax. Also add structured types (in lucky only, for the time being). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.142 Version-Log: share/*.sh.in: use set instead of export for sh scripts (export is a bashism that does not work for sun). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.141 Version-Log: source/show_luc.ml: source/show_env.ml: Add a command line option to set the max nb of char before truncate formula. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.140 Version-Log: source/lurette.ml source/luc_exe.ml source/env_state.ml: Infer that environments share controllable vars instead of asking it to users. Also allow any string to be a valid node name. Also fix a bug where, when several env were provided, the Env_state.file_name was not returning the rigth file name. Actually it was not really a bug since it could not be triggered before this change ... It just happen to work correctly by chance. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.139 Version-Log: ihm/xlurette/xlurette_main.ml: Change the current dir when the sut changes so that the current dir is the dir of the sut. source/lurettetop.ml: Add a change_dir command. Make user_dir and tmp_lurette global vars. share/configure.in: create .bat and sh scripts take set env vars and run tools (xlurette and lurettetop) so that sourcing lucky_init.cs is no longer necessary. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.138 Version-Log: Make it work under cygwin. Add the possibility of setting extra env var to link external libs or c files. Project-Description: Lurette
-
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
-