1. 17 Mar, 2010 40 commits
    • Erwan Jahier's avatar
      lurette 0.68 Fri, 17 May 2002 17:59:13 +0200 by jahier · 8c24cdb7
      Erwan Jahier authored
      Parent-Version:      0.67
      Version-Log:
      
      Add a verbose option in ima_exe.
      
      Fix a bug in show_env.ml introduced in the previuos pci.
      
      Add support to dynamically load another ima from ima_exe (will usefull for
      Ludic).
      
      Project-Description: Lurette
      8c24cdb7
    • Erwan Jahier's avatar
      lurette 0.67 Thu, 16 May 2002 13:51:48 +0200 by jahier · a092979c
      Erwan Jahier authored
      Parent-Version:      0.66
      Version-Log:
      
      Draw loop nodes as circles and other nodes as boxes in the dot output
      of the ima files.
      
      Project-Description: Lurette
      a092979c
    • Erwan Jahier's avatar
      lurette 0.66 Thu, 16 May 2002 10:54:38 +0200 by jahier · 66e00627
      Erwan Jahier authored
      Parent-Version:      0.65
      Version-Log:
      
      solver.ml:
              Fix a bug is draw_in_bdd where it was unable to draw in a true
              formula when it was a top level one. The reason was that the
              tossing of remaining vars was not done at draw_in_bdd top level,
              which is wrong since true can appear on ima transitions.
      
      Project-Description: Lurette
      66e00627
    • Erwan Jahier's avatar
      lurette 0.65 Fri, 10 May 2002 16:54:24 +0200 by jahier · ee70bc48
      Erwan Jahier authored
      Parent-Version:      0.64
      Version-Log:
      
      Outputs error message on stderr rather than on stdout.
      
      Project-Description: Lurette
      ee70bc48
    • Erwan Jahier's avatar
      lurette 0.64 Fri, 10 May 2002 16:32:32 +0200 by jahier · 458e1508
      Erwan Jahier authored
      Parent-Version:      0.63
      Version-Log:
      
      Add support for loop Gauss.
      
      Fix a bug in the handling of loops where lurette (and ima_exe) was
      stopping whenever the body of a loop contains no satisfiable formula
      whereas the endLoop branch should be taken in that case.
      
      Project-Description: Lurette
      458e1508
    • Erwan Jahier's avatar
      lurette 0.63 Tue, 07 May 2002 15:12:50 +0200 by jahier · 9d1e0221
      Erwan Jahier authored
      Parent-Version:      0.62
      Version-Log:
      
      Reimplement the rif parsing in ima_exe.ml so that it is correct wrt the BLA-RIF
      doc.
      
      Project-Description: Lurette
      9d1e0221
    • Erwan Jahier's avatar
      lurette 0.62 Fri, 03 May 2002 15:21:42 +0200 by jahier · c88a7a6f
      Erwan Jahier authored
      Parent-Version:      0.61
      Version-Log:
      
      Reorganise things a little bit so that show_ima does not depend on
      cudd, etc.
      
      Project-Description: Lurette
      c88a7a6f
    • Erwan Jahier's avatar
      lurette 0.61 Fri, 03 May 2002 12:08:34 +0200 by jahier · 6b362e07
      Erwan Jahier authored
      Parent-Version:      0.60
      Version-Log:
      
      Add support for handling loops. This is based on the use of dynamic
      weigths. The idea is to compute the dynamic weigths before the trees
      are constructed.
      
      Add a --show-aut option for ima_exe.
      
      Also, Add the command lise args hashed to the end of the name of the dot file
      that is used to visualize the ima file.
      
      Project-Description: Lurette
      6b362e07
    • Erwan Jahier's avatar
      lurette 0.60 Mon, 29 Apr 2002 10:16:48 +0200 by jahier · b425173e
      Erwan Jahier authored
      Parent-Version:      0.59
      Version-Log:
      
      Add an make release rule to package a lurette.tgz ready to distribute.
      
      Create a bin dir where all the biniries (except lurette) will live.
      
      Create a show_ima executable that lets one (Yvan actually) display
      .env (or .ima) files off-line.
      
      Move read_env_state from env.ml to env_state.ml.
      
      Add support for lutin loops in the parser (not yet handled tough).
      
      In gen_stubs.ml, try to automatically call lustre whenever no C poc
      file exists for the invoked program.
      
      Project-Description: Lurette
      b425173e
    • Erwan Jahier's avatar
      lurette 0.59 Mon, 22 Apr 2002 14:40:46 +0200 by jahier · 74c46a98
      Erwan Jahier authored
      Parent-Version:      0.58
      Version-Log:
      
      Change the env parser so that :
      1) lists can end with a semi-column
      2) We can deal with dynamic weigths (for loops). The support
      for handling them is not written yet tough.
      
      Project-Description: Lurette
      74c46a98
    • Erwan Jahier's avatar
      lurette 0.58 Fri, 19 Apr 2002 11:15:07 +0200 by jahier · 03ffa20e
      Erwan Jahier authored
      Parent-Version:      0.57
      Version-Log:
      
      Clean up Makefiles for lurette and ima_exe.
      
      Make sure that gen_stubs does not recompile the fake oracle
      (always_true.lus) if it is not necessary.
      
      Project-Description: Lurette
      03ffa20e
    • Erwan Jahier's avatar
      lurette 0.57 Thu, 04 Apr 2002 16:06:30 +0200 by jahier · da601f66
      Erwan Jahier authored
      Parent-Version:      0.56
      Version-Log:
      
      Add a --output options to specify the output file name.
      
      Project-Description: Lurette
      da601f66
    • Erwan Jahier's avatar
      lurette 0.56 Wed, 03 Apr 2002 16:14:26 +0200 by jahier · 662e3694
      Erwan Jahier authored
      Parent-Version:      0.55
      Version-Log:
      
      Change the env format sligthly again :
       - adds the arcs and node numbers.
       - allows lists to end by a ;
       - add xor's
      
      Project-Description: Lurette
      662e3694
    • Erwan Jahier's avatar
      lurette 0.55 Wed, 03 Apr 2002 14:41:43 +0200 by jahier · f570cc25
      Erwan Jahier authored
      Parent-Version:      0.54
      Version-Log:
      
      Allow equalities between formula by translating [A = B] into
      [Or(And(A,B), And(Not(A), Not(B)))].
      
      Fix a bug where lurette had a bad behaviour whenever a toss
      was performed on a domain which size was bigger than max_int
      or max_float.
      
      Fix a bug where lurette was not handling env with both boolean and
      numerical as output vars.  Also add a few comments in solver.ml along
      the way.
      Adds a local bool as an output of heater in order to test the fix
      above.
      
      Project-Description: Lurette
      f570cc25
    • Erwan Jahier's avatar
      lurette 0.54 Tue, 02 Apr 2002 14:25:12 +0200 by jahier · f0aff2da
      Erwan Jahier authored
      Parent-Version:      0.53
      Version-Log:
      
      Cosmetic change:
      
      Encapsulates the various fields of Env_state.
      
      Project-Description: Lurette
      f0aff2da
    • Erwan Jahier's avatar
      lurette 0.53 Fri, 29 Mar 2002 11:04:44 +0100 by jahier · 1347da63
      Erwan Jahier authored
      Parent-Version:      0.52
      Version-Log:
      
      Add a --verbose and a --help options to the command line.
      
      Also clean up a little bit comments in various places.
      
      Project-Description: Lurette
      1347da63
    • Erwan Jahier's avatar
      lurette 0.52 Thu, 28 Mar 2002 18:10:42 +0100 by jahier · edc79032
      Erwan Jahier authored
      Parent-Version:      0.51
      Version-Log:
      
      Remove the necessity to provide an oracle when the user does
      not have any assertion to check. To do that, I parse the sut
      file and automatically generates a fake oracle that answers always
      true.
      
      Project-Description: Lurette
      edc79032
    • Erwan Jahier's avatar
      lurette 0.51 Wed, 27 Mar 2002 17:46:03 +0100 by jahier · 6f6168b0
      Erwan Jahier authored
      Parent-Version:      0.50
      Version-Log:
      
      Change the way pre are translated in the .env file. Now
      instead of writting "_pre2toto", one writes "pre(2,toto)".
      
      But internally, it is handled the same way as before (i.e., the first
      thing I do when parsing the env file is to transform "pre(2,toto)"
      into "_pre2toto" (it makes the hangling of pre vars much more
      homogeneous with the way the other vars are handled.
      
      Also fix a bug where it was not possible to have a pre on input
      vars because the update_pre was failing to proceed quietly  whenever
      one of its var was not computable because its pre does have a value.
      Also give an appropriate error message whenever the user wrongly
      use a pre on a var that can not be computed.
      
      Project-Description: Lurette
      6f6168b0
    • Erwan Jahier's avatar
      lurette 0.50 Wed, 27 Mar 2002 13:36:39 +0100 by jahier · c699a9b3
      Erwan Jahier authored
      Parent-Version:      0.49
      Version-Log:
      
      Add the possibility to put pragmas in the .env files.
      
      Project-Description: Lurette
      c699a9b3
    • Erwan Jahier's avatar
      lurette 0.49 Tue, 26 Mar 2002 16:22:45 +0100 by jahier · 94d83c01
      Erwan Jahier authored
      Parent-Version:      0.48
      Version-Log:
      
      Clean up a little bit the ima format to make it sipler to parse
      and to avoid reducing  the naming space as much as possible.
      
      Project-Description: Lurette
      94d83c01
    • Erwan Jahier's avatar
      lurette 0.48 Fri, 22 Mar 2002 14:29:17 +0100 by jahier · 1c7769db
      Erwan Jahier authored
      Parent-Version:      0.47
      Version-Log:
      
      Add support for (boolean and numeric) if-then-else.
      
      Remove the eval.ml module as the replacement of pre and input
      vars is now done in Solver.formula_to_bdd.
      
      Add a new module gne.ml that provides a garded normal expressions
      data structure that is used to handle if-then-elses.
      
      Also introduce a new field to env_state called bdd_tbl_global which
      is used to cache the result of formula_to_bdd for bdds that do not
      depend on pre nor input vars. The field bdd_tbl which cache the other
      reults is now cleared at each step because it is useless to store results
      that depends on pre and inputs.
      
      Project-Description: Lurette
      1c7769db
    • Erwan Jahier's avatar
      lurette 0.47 Thu, 14 Mar 2002 18:45:50 +0100 by jahier · 606164a8
      Erwan Jahier authored
      Parent-Version:      0.46
      Version-Log:
      
      Implement an ima_exe that lets one imterprets .env automata offline
      via a rif dialogue (e.g., to be used from lulu).
      
      Project-Description: Lurette
      606164a8
    • Erwan Jahier's avatar
      lurette 0.46 Wed, 13 Mar 2002 14:51:14 +0100 by jahier · ee264c20
      Erwan Jahier authored
      Parent-Version:      0.45
      Version-Log:
      
      Clean up a little bit lurette.ml
      
      Project-Description: Lurette
      ee264c20
    • Erwan Jahier's avatar
      lurette 0.45 Wed, 13 Mar 2002 13:59:01 +0100 by jahier · a23032bf
      Erwan Jahier authored
      Parent-Version:      0.44
      Version-Log:
      
      Comment out all the stuff related to the heap initialisation
      of cudd since it is unused for the moment.
      
      Project-Description: Lurette
      a23032bf
    • Erwan Jahier's avatar
      lurette 0.44 Wed, 13 Mar 2002 13:53:40 +0100 by jahier · dc7ea4b5
      Erwan Jahier authored
      Parent-Version:      0.43
      Version-Log:
      
      Add the possibility to specify the min lower and upper bounds
      in the env automata for output and local vars.
      
      Project-Description: Lurette
      dc7ea4b5
    • Erwan Jahier's avatar
      lurette 0.43 Wed, 13 Mar 2002 10:57:11 +0100 by jahier · 189430ac
      Erwan Jahier authored
      Parent-Version:      0.42
      Version-Log:
      
      Checks that nodes in .env files are contiguous as the code suppose they are.
      
      Also cleanup a little bit the code in env.ml as (I was reinventing map ...)
      
      Project-Description: Lurette
      189430ac
    • Erwan Jahier's avatar
      lurette 0.42 Wed, 13 Mar 2002 10:29:08 +0100 by jahier · 46927269
      Erwan Jahier authored
      Parent-Version:      0.41
      Version-Log:
      
      Make sure that n formula are drawn when even numeric failure occurs.
      To do that, I recursively call draw_n_p_formula until the required
      number of outputs have been generated.
      
      Also fix a bug where my code was not handling cases where several
      formulas corresponding to the same origin and target nodes (Lutin
      probably won't generate such arcs explicitely, but it does
      implicitely via epsilon transitions). The fix consist in adding
      formula in wtree types instead of maintaining a table of formula
      indexed by node list pairs. The env_state.formula_table is thus no
      longer needed.
      
      Project-Description: Lurette
      46927269
    • Erwan Jahier's avatar
      lurette 0.41 Fri, 08 Mar 2002 17:30:37 +0100 by jahier · 801c2882
      Erwan Jahier authored
      Parent-Version:      0.40
      Version-Log:
      
      Change sligthly the ima format to make it more consistent.
      
      Project-Description: Lurette
      801c2882
    • Erwan Jahier's avatar
      lurette 0.40 Thu, 07 Mar 2002 16:26:47 +0100 by jahier · 9d1241f6
      Erwan Jahier authored
      Parent-Version:      0.39
      Version-Log:
      
      Change the naming convention of prevars. Now, _pretoto is noted
      _pre1toto, and _pre_pre_pretoto is noted _pre3toto.
      
      Also fix a bug in the default initialization of ranges : min_float
      is the smallest positive float, not the smallet one !!
      
      Project-Description: Lurette
      9d1241f6
    • Erwan Jahier's avatar
      lurette 0.39 Thu, 07 Mar 2002 13:36:27 +0100 by jahier · 4579cc26
      Erwan Jahier authored
      Parent-Version:      0.38
      Version-Log:
      
      Use the new cudd interface based on camlidl (mlcuddidl).
      
      Now, bdds do not leaks anymore.  Remove debugging stuff that was used
      to track that problem.
      
      Project-Description: Lurette
      4579cc26
    • Erwan Jahier's avatar
      lurette 0.38 Wed, 06 Mar 2002 10:50:34 +0100 by jahier · c3c5f045
      Erwan Jahier authored
      Parent-Version:      0.37
      Version-Log:
      
      With this change, lurette is now able to handle numeric variables
      over intervals !
      
      Project-Description: Lurette
      c3c5f045
    • Erwan Jahier's avatar
      lurette 0.37 Mon, 04 Mar 2002 14:58:15 +0100 by jahier · cdeda709
      Erwan Jahier authored
      Parent-Version:      0.36
      Version-Log:         Various cosmetic changes in comments.
      Project-Description: Lurette
      cdeda709
    • Erwan Jahier's avatar
      lurette 0.36 Mon, 04 Mar 2002 13:50:13 +0100 by jahier · 8b44df60
      Erwan Jahier authored
      Parent-Version:      0.35
      Version-Log:
      
      Add support to handle numerical contraints. The numerical stuff is
      untested, but the boolean part works as before.
      
      source/rnumsolver.mli:
      source/rnumsolver.ml:
          New files implementing a numeric solver based on intervals.
      
      source/*.ml:
          Change the var_type type from a string to a sum type containing
          the lower and upper bounds of numeric domains.
      
          Do not maintain a var_name to index correspondance, but a formula to
          index one. This is to be able to handle numerical constraint in bdds.
          This field is not set at init time anymore, but in formula_to_bdd.
      
          Add <>, <, and <= to the type of formula.
      
      Project-Description: Lurette
      8b44df60
    • Erwan Jahier's avatar
      lurette 0.35 Tue, 19 Feb 2002 16:27:14 +0100 by jahier · 429604ce
      Erwan Jahier authored
      Parent-Version:      0.34
      Version-Log:
       Use Hashtbl instead of assoc list to store env_in
      items as eval needs to search in it very often, it might be an issue
      when there is a lot of input variables.
      
      Project-Description: Lurette
      429604ce
    • Erwan Jahier's avatar
      lurette 0.34 Tue, 19 Feb 2002 10:40:58 +0100 by jahier · dba4992a
      Erwan Jahier authored
      Parent-Version:      0.33
      Version-Log:
      
      Fix a bug when computing the power of two.
      
      Project-Description: Lurette
      dba4992a
    • Erwan Jahier's avatar
      lurette 0.33 Mon, 18 Feb 2002 17:52:34 +0100 by jahier · ee4eb63d
      Erwan Jahier authored
      Parent-Version:      0.32
      Version-Log:
      
      Avoid recomputing everytime the list of output vars by storing it
      in an env_state field.
      
      Project-Description: Lurette
      ee4eb63d
    • Erwan Jahier's avatar
      lurette 0.32 Mon, 18 Feb 2002 17:06:16 +0100 by jahier · af07708a
      Erwan Jahier authored
      Parent-Version:      0.31
      Version-Log:
      
      Add an option --no-oracle to prevent that lurette calls the oracle.
      
      The solution number counting function was wrong.
      
      Also, make it easy to switch to float, or to big_int, to store
      the number of solution numbers.
      
      Project-Description: Lurette
      af07708a
    • Erwan Jahier's avatar
      lurette 0.31 Tue, 12 Feb 2002 14:10:11 +0100 by jahier · e682b1ff
      Erwan Jahier authored
      Parent-Version:      0.30
      Version-Log:
      
      Various fixes so that lurette can be build from scratch.
      
      Project-Description: Lurette
      e682b1ff
    • Erwan Jahier's avatar
      lurette 0.30 Tue, 12 Feb 2002 13:42:18 +0100 by jahier · c6197659
      Erwan Jahier authored
      Parent-Version:      0.29
      Version-Log:
      
      gen_stubs.ml:
          Updates the stubs files (lurette_stub.ml, sut_stub.c,
          sut_idl_stub.idl, oracle_stub.c, oracle_idl_stub.idl) iff they have
          changed to avoid unnecessary recompilations.
      
      Makefile:
          Minor cosmetic changes.
      
      wtree.ml,mli:
      env.ml:
      
          Also remove a loop in the dependencies that was confusing
          ocamldot (but how could it work before with that loop ?). To do that,
          pass Solver.is_satisfiable as a argument of Wtree.choose_n_formula so
          that Wtree does not depend on Solver anymore.
      
      Project-Description: Lurette
      c6197659
    • Erwan Jahier's avatar
      lurette 0.29 Tue, 12 Feb 2002 09:58:15 +0100 by jahier · 454bc141
      Erwan Jahier authored
      Parent-Version:      0.28
      Version-Log:
      
      Put the names of the environements in the sim2chro window title.
      
      Project-Description: Lurette
      454bc141