1. 17 Mar, 2010 40 commits
    • Erwan Jahier's avatar
      lurette 1.28 Wed, 21 Apr 2004 09:38:03 +0200 by jahier · 6de2c0e9
      Erwan Jahier authored
      Parent-Version:      1.27
      Version-Log:
      
      Add #locs pragmas so that sim2chro is able to print local var in green.
      
      Project-Description: Lurette
      6de2c0e9
    • Erwan Jahier's avatar
      lurette 1.27 Fri, 26 Mar 2004 09:48:21 +0100 by jahier · 1df63c5e
      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
      1df63c5e
    • Erwan Jahier's avatar
      lurette 1.26 Tue, 16 Mar 2004 14:41:14 +0100 by jahier · 5a559772
      Erwan Jahier authored
      Parent-Version:      1.25
      Version-Log:
      
      source/parse_luc.ml:
         Check that 2 vars are not defined twice.
      
      source/parse_luc.ml:
      source/lustreExp.ml:
      source/var.ml:
         Rename local vars to avoid clashed if 2 automata uses common
         local var names.
      
      Project-Description: Lurette
      5a559772
    • Erwan Jahier's avatar
      lurette 1.25 Fri, 12 Mar 2004 10:44:00 +0100 by jahier · 94617a93
      Erwan Jahier authored
      Parent-Version:      1.24
      Version-Log:
      
      source/lustreExp.ml:
         Change the vut type from a list to a Map indexed by strings.
      
      source/parse_luc.ml:
         Use Lexing.buffer instead of my home made lucky_buff one. It is
         simpler, cleaner (especially AFA the ~ stuff is concerned) and probably
         more efficient.
      
      Project-Description: Lurette
      94617a93
    • Erwan Jahier's avatar
      lurette 1.24 Thu, 11 Mar 2004 15:19:19 +0100 by jahier · fa741106
      Erwan Jahier authored
      Parent-Version:      1.23
      Version-Log:
      
      source/lustreExp.ml:
         use a map indexed by the var name instead of a list of
         variables as the search in such a list is done very often
         during the type checking.
      
      Project-Description: Lurette
      fa741106
    • Erwan Jahier's avatar
      lurette 1.23 Mon, 08 Mar 2004 14:10:38 +0100 by jahier · 18e59b0d
      Erwan Jahier authored
      Parent-Version:      1.22
      Version-Log:
      
      source/*.ml*:
         perform a sed 's/[ ]*$//' on all files to remove
         trailing space.
      
      Project-Description: Lurette
      18e59b0d
    • Erwan Jahier's avatar
      lurette 1.22 Mon, 08 Mar 2004 13:46:15 +0100 by jahier · ceac869e
      Erwan Jahier authored
      Parent-Version:      1.21
      Version-Log:
      
      Add a couple of scade files in the distrib so that it is easier
      to test scade programs under linux using the generated c files.
      
      source/value.ml
         use T and F instead of t and f for booleans (more visible under xlurette).
      
      share/Makefile.lurette.in:
         Reorganize (clean-up) the file
      
      xlurette/xlurette_glade_main.ml:
      share/plot:
         Fix the gnuplot problems (+ <<set mouse>> in share/plot).
      
      source/util.ml:
      source/lurettetop.ml:
         Move the gnuplot stuff into lurettetop.
      
      Project-Description: Lurette
      ceac869e
    • Erwan Jahier's avatar
      lurette 1.21 Fri, 13 Feb 2004 18:25:56 +0100 by jahier · d115d326
      Erwan Jahier authored
      Parent-Version:      1.20
      Version-Log:
      
      source/lurette.ml:
      source/command_line.ml:
      source/command_line.mli:
      source/lurettetop.ml:
         Plug the step mode stuff into xlurette.
      
         Repair the step_by_step mode that was broken under xlurette
         (still do not know why though...).
      
      Project-Description: Lurette
      d115d326
    • Erwan Jahier's avatar
      lurette 1.20 Fri, 13 Feb 2004 16:03:37 +0100 by jahier · b3d4d2c7
      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
      b3d4d2c7
    • Erwan Jahier's avatar
      lurette 1.19 Mon, 19 Jan 2004 14:36:43 +0100 by jahier · caa32faa
      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
      caa32faa
    • Erwan Jahier's avatar
      lurette 1.18 Thu, 08 Jan 2004 16:02:52 +0100 by jahier · c3756573
      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
      c3756573
    • Erwan Jahier's avatar
      lurette 1.17 Thu, 08 Jan 2004 09:06:39 +0100 by jahier · 06abf72c
      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
      06abf72c
    • Erwan Jahier's avatar
      lurette 1.16 Tue, 06 Jan 2004 16:06:21 +0100 by jahier · 6e015db3
      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
      6e015db3
    • Erwan Jahier's avatar
      lurette 1.15 Mon, 05 Jan 2004 17:46:15 +0100 by jahier · e1350c78
      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
      e1350c78
    • Erwan Jahier's avatar
      lurette 1.14 Fri, 19 Dec 2003 15:39:58 +0100 by jahier · d534db9c
      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
      d534db9c
    • Erwan Jahier's avatar
      lurette 1.13 Fri, 12 Dec 2003 14:21:26 +0100 by jahier · 21390374
      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
      21390374
    • Erwan Jahier's avatar
      lurette 1.12 Tue, 09 Dec 2003 15:44:28 +0100 by jahier · c3ab83b6
      Erwan Jahier authored
      Parent-Version:      1.11
      Version-Log:
      
      Various fixes in the C scade parsing.
      
      Project-Description: Lurette
      c3ab83b6
    • Erwan Jahier's avatar
      lurette 1.11 Wed, 26 Nov 2003 08:52:30 +0100 by jahier · b3c5c602
      Erwan Jahier authored
      Parent-Version:      1.10
      Version-Log:
      
      No more side effects are done via the Env_state module.
      
      Project-Description: Lurette
      b3c5c602
    • Erwan Jahier's avatar
      lurette 1.10 Thu, 20 Nov 2003 10:09:54 +0100 by jahier · 540ee1f9
      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
      540ee1f9
    • Erwan Jahier's avatar
      lurette 1.9 Tue, 18 Nov 2003 11:17:12 +0100 by jahier · 67c17ef7
      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
      67c17ef7
    • Erwan Jahier's avatar
      lurette 1.8 Wed, 22 Oct 2003 18:30:52 +0200 by jahier · a3e8a67b
      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
      a3e8a67b
    • Erwan Jahier's avatar
      lurette 1.7 Fri, 10 Oct 2003 14:01:43 +0200 by jahier · 79b18f3b
      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
      79b18f3b
    • Erwan Jahier's avatar
      lurette 1.6 Thu, 25 Sep 2003 17:49:07 +0200 by jahier · 7189e37a
      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
      7189e37a
    • Erwan Jahier's avatar
      lurette 1.5 Wed, 24 Sep 2003 16:54:55 +0200 by jahier · fcdb446e
      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
      fcdb446e
    • Erwan Jahier's avatar
      lurette 1.4 Wed, 24 Sep 2003 15:48:02 +0200 by jahier · 5bf375a5
      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
      5bf375a5
    • Erwan Jahier's avatar
      lurette 1.3 Tue, 23 Sep 2003 16:56:51 +0200 by jahier · d66521bd
      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
      d66521bd
    • Erwan Jahier's avatar
      lurette 1.2 Wed, 17 Sep 2003 10:09:24 +0200 by jahier · 36ab3ebb
      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
      36ab3ebb
    • Erwan Jahier's avatar
      lurette 1.1 Mon, 08 Sep 2003 16:02:09 +0200 by jahier · 4aed6dc3
      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
      4aed6dc3
    • Erwan Jahier's avatar
      lurette 0.143 Thu, 26 Jun 2003 16:50:35 +0200 by jahier · 2b40538c
      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
      2b40538c
    • Erwan Jahier's avatar
      lurette 0.142 Thu, 26 Jun 2003 11:17:53 +0200 by jahier · 8d11bd37
      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
      8d11bd37
    • Erwan Jahier's avatar
      lurette 0.141 Thu, 26 Jun 2003 10:38:20 +0200 by jahier · ed63acb4
      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
      ed63acb4
    • Erwan Jahier's avatar
      lurette 0.140 Mon, 23 Jun 2003 15:19:23 +0200 by jahier · 45dee352
      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
      45dee352
    • Erwan Jahier's avatar
      lurette 0.139 Wed, 18 Jun 2003 10:59:43 +0200 by jahier · 445b2ff0
      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
      445b2ff0
    • Erwan Jahier's avatar
      lurette 0.138 Fri, 13 Jun 2003 09:05:17 +0200 by jahier · 30692c60
      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
      30692c60
    • Erwan Jahier's avatar
      lurette 0.137 Tue, 03 Jun 2003 15:32:29 +0200 by jahier · 5a9bb52c
      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
      5a9bb52c
    • Erwan Jahier's avatar
      lurette 0.136 Mon, 19 May 2003 11:40:43 +0200 by jahier · fe6d609c
      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
      fe6d609c
    • Erwan Jahier's avatar
      lurette 0.135 Tue, 06 May 2003 15:51:08 +0200 by jahier · 124c55f1
      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
      124c55f1
    • Erwan Jahier's avatar
      lurette 0.134 Tue, 22 Apr 2003 17:18:57 +0200 by jahier · 4bc90dac
      Erwan Jahier authored
      Parent-Version:      0.133
      Version-Log:
      
      Various changes related to the packaging of lurette.
      
      Project-Description: Lurette
      4bc90dac
    • Erwan Jahier's avatar
      lurette 0.133 Thu, 17 Apr 2003 13:22:44 +0200 by jahier · dbc00f74
      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
      dbc00f74
    • Erwan Jahier's avatar
      lurette 0.132 Tue, 15 Apr 2003 17:38:13 +0200 by jahier · 557de1e9
      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
      557de1e9