1. 17 Mar, 2010 40 commits
    • Erwan Jahier's avatar
      lurette 1.41 Mon, 26 Sep 2005 13:51:19 +0200 by jahier · 98380cec
      Erwan Jahier authored
      Parent-Version:      1.40
      Version-Log:
      
      source/luc_exe.ml
      source/lurette.ml
      source/util.ml
      source/formula_to_bdd.ml
      source/bddd.ml
      source/solver.ml
      source/store.ml
      source/parse_luc.mli
      source/parse_luc.ml
      source/env_state.mli
      source/env_state.ml
      source/run_aut.ml
      source/gne.mli
      source/gne.ml
      source/lurettetop.ml
      source/gen_stubs_poc.ml
      source/ne.ml
      source/ne.mli
      share/lucky.el
      share/configure.in
      Makefile.common.source
      OcamlMakefile
      user-rules
      source/Makefile.show_luc
      source/Makefile.lucky
      source/Makefile.gen_stubs
      source/Makefile.lurette_lib
      source/Makefile
      test/time-joly.res
      test/temp_int.luc
      ihm/xlurette/xlurette.glade
      ihm/xlurette/makefile
      source/Makefile.gen_fake_lucky
      source/lustreExp.ml
      source/lustreExp.mli
      source/exp.ml
      source/exp.mli
      source/parser.mly
      doc/lucky-man/lucky-man.tex
      source/gnuplot-socket.ml
      source/gnuplot-rif.ml
      source/luckyDraw.mli
      source/luckyDraw.ml
      source/essai-maitre.ml
      source/essai-esclave.ml
      source/Makefile.ocaml
      source/Makefile.luckyDraw
      
      Add the possibility to call external code via dyn lib.
      
      The generation of default lucky files from Lurette was broken.
      
      Fix warning generated by gcc4.
      
      Fix a bug where variables with default values were generated twice
      (bug only visible in assert mode ; in the other mode, one of the value
      was taken, but I am not sure which one...)
      
      Project-Description: Lurette
      98380cec
    • Erwan Jahier's avatar
      lurette 1.40 Fri, 22 Jul 2005 17:06:41 +0200 by jahier · b1a40b56
      Erwan Jahier authored
      Parent-Version:      1.39
      Version-Log:
      
      source/luc_exe.ml
      source/command_line_luc_exe.ml
      source/command_line_luc_exe.mli
      source/lurette.ml
      source/command_line.ml
      source/command_line.mli
      source/lucky.ml
      source/rif.ml
      source/env_state.mli
      source/env_state.ml
      source/run_aut.mli
      source/run_aut.ml
      source/lurettetop.ml
      ihm/xlurette/xlurette_glade_main.ml
        Add a reactive mode where the output of the previous cycle is returned
        when the Lucky environment is blocked (because no transition from
        the current node(s) is labelled by a satisfiable constraint.
      
      Remove the dependence on cygwin to run it under windows.
      
      In particular, to be able to do that, I now use socket instead of pipes
      in order to communicate between lurettetop and xlurette.
      
      Also, define proper, cp, rm, etc instead of doing them by sys calls.
      
      A lot of changes to make it work with the scade gui
      
      Project-Description: Lurette
      b1a40b56
    • Erwan Jahier's avatar
      lurette 1.39 Tue, 14 Dec 2004 11:29:46 +0100 by jahier · 3a6425a6
      Erwan Jahier authored
      Parent-Version:      1.38
      Version-Log:
      
      source/run_aut.mli
      source/run_aut.ml:
        Fix a bug when drawing transitions in the automata that made the distribution
        wrong wrt weights (oups)...
      
      source/lucky.ml
      source/run_aut.mli
      run_aut.ml:
        Fix a bug where the repartition wrt the automata transitions was wrong in
        case of backtracking.
      
      source/lurette.ml
        Fix a bug related to the thickness (when only all the vertices where
      required).
      
      demo-xlurette/fault-tolerant-heater/heater_control_env.luc
      share/show_luc.sh
      share/show_luc.bat
      
      source/gen_fake_lucky.ml
      source/lurettetop.ml
      source/util.ml
      ihm/xlurette/xlurette_glade_main.ml
      ihm/xlurette/xlurette.glade
         Add a button in xlurette that generates default environments.
         Add a buildenv command for lurettetop to do it.
      
      Project-Description: Lurette
      3a6425a6
    • Erwan Jahier's avatar
      lurette 1.38 Tue, 09 Nov 2004 08:50:49 +0100 by jahier · 1d4d5e4c
      Erwan Jahier authored
      Parent-Version:      1.37
      Version-Log:
      
      source/util.ml:
         put the C_GENERATOR_FLAG at the end of the list of options of lustre2C
         so that the -name_lenght lustre2C option can be taken into account.
      
      source/Makefile.lucky
      source/Makefile.lurette_lib
      source/fair_bddd.ml
      source/fair_bddd.mli
      source/bddd.ml
      source/bddd.mli
      source/solver.ml
      source/sol_nb.ml [new] :
         put all the stuff related to the counting of the solution number in a
      dedicated
         module.
      
         Make the representation of solution numbers abstract.
      
         Use the log-based coding instead of the real value so that it does not
      overflow,
         which was the case when the programs have more than 1200 variables.
      
      source/parse_c_scade.ml
         Fix a bug when parsing C scade files due to the fact that not all
         variable name start with '_' (one start with 'SYNCHRO_')
      
      source/gen_fake_lucky.ml
        When no environment is provided, also generate a file named
        <node>_env_UD in addition to the fake env in <node>_env. That one
        is more elaborated and contraints the output variables so that they
        move up and down.
      
      ihm/xlurette/xlurette.glade
      ihm/xlurette/xlurette_glade_interface.ml
      
      share/Makefile.lurette.in
         include user test dir before scade dir, otherwise, inconsistent definitions
         of reals may coexist.
      
      Project-Description: Lurette
      1d4d5e4c
    • Erwan Jahier's avatar
      lurette 1.37 Wed, 29 Sep 2004 15:37:07 +0200 by jahier · d3946417
      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
      d3946417
    • Erwan Jahier's avatar
      lurette 1.36 Tue, 31 Aug 2004 09:43:25 +0200 by jahier · d7a68d0b
      Erwan Jahier authored
      Parent-Version:      1.35
      Version-Log:
      
      * A better error msg is displayed when one try to write something like
        <<x : int ^ 3 ~default pre x ^ 3>>, which is currently not supported.
      
      * Fix a bug in gen_fake_lucky that was introduced in V1.33
       (incorrect environment were generated).
      
      Project-Description: Lurette
      d7a68d0b
    • Erwan Jahier's avatar
      lurette 1.35 Tue, 27 Jul 2004 10:39:06 +0200 by jahier · a7a16d1b
      Erwan Jahier authored
      Parent-Version:      1.34
      Version-Log:         empty
      Project-Description: Lurette
      a7a16d1b
    • Erwan Jahier's avatar
      lurette 1.34 Thu, 22 Jul 2004 15:47:05 +0200 by jahier · 2b554dc7
      Erwan Jahier authored
      Parent-Version:      1.33
      Version-Log:
      
      A first steps toward an interface to sildex is done. Its seems
      to work. It has to be tested more though.
      
      Project-Description: Lurette
      2b554dc7
    • Erwan Jahier's avatar
      lurette 1.33 Tue, 20 Jul 2004 15:29:42 +0200 by jahier · 2880f23d
      Erwan Jahier authored
      Parent-Version:      1.32
      Version-Log:
      
      source/lurette.ml:
      source/command_line_luc_exe.mli:
      source/command_line_luc_exe.ml:
      source/command_line.ml:
      source/command_line.mli:
         Random seed was encoded by a seed of 0, which is unfortunate
         when the user set the seed to 0...
      
      source/util.ml:
      xlurette/xlurette.glade:
         Add a C_GENERATOR_FLAG to let users add options to lustre2c and ec2C.
      
      source/parse_luc.ml:
         Issue a Warning when a node is not declared before being used.
      
      Project-Description: Lurette
      2880f23d
    • Erwan Jahier's avatar
      lurette 1.32 Wed, 30 Jun 2004 14:03:33 +0200 by jahier · da9a1255
      Erwan Jahier authored
      Parent-Version:      1.31
      Version-Log:
      
      source/fair_bddd.ml:
         Fix a bug where the distribution was not correct according
        to the solution number
      
      Project-Description: Lurette
      da9a1255
    • Erwan Jahier's avatar
      lurette 1.31 Mon, 28 Jun 2004 16:29:58 +0200 by jahier · 693db19e
      Erwan Jahier authored
      Parent-Version:      1.30
      Version-Log:
      
      source/run_aut.ml:
      source/graph.ml:
      source/env_state.ml
      source/lucky.ml:
      source/env_state.ml:
         Graph.t in now a side effet-free DT.
      
      source/lurettetop.ml:
      xlurette/xlurette.glade:
         provide an error msg to xlurette when gnuplot is not installed.
      
      Project-Description: Lurette
      693db19e
    • Erwan Jahier's avatar
      lurette 1.30 Mon, 28 Jun 2004 10:44:36 +0200 by jahier · f9d45610
      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
      f9d45610
    • Erwan Jahier's avatar
      lurette 1.29 Fri, 30 Apr 2004 16:43:39 +0200 by jahier · 1c8385d0
      Erwan Jahier authored
      Parent-Version:      1.28
      Version-Log:
      
      source/ocaml2c.idl:
      source/lurette.ml:
      source/gen_stubs_poc.ml:
      source/gen_stubs_scade.ml:
        Fix a bug where the step and the tries in the sut were completely
        wrong.
      
      source/store.ml
        Fix a bug where, if only the ~min or the ~max options were used,
        they were ignored ...
      
      source/parse_luc.ml:
        Make sure that ~min and ~max are fed with values, not complex expressions.
      
        pre-process lucky files with cpp.
      
      source/sim2chro.ml:
        put the locals after the outputs because it is the order into
        which their values appear.
      
      source/gen_stubs.ml:
        Do not change the oracle compiler if it is provided.
      
      Project-Description: Lurette
      1c8385d0
    • 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