1. 17 Mar, 2010 40 commits
    • Erwan Jahier's avatar
      lurette 0.86 Wed, 18 Sep 2002 15:27:17 +0200 by jahier · 50ccf63a
      Erwan Jahier authored
      Parent-Version:      0.85
      Version-Log:
      
      Finish to implement xlurette.
      
      Project-Description: Lurette
      50ccf63a
    • Erwan Jahier's avatar
      lurette 0.85 Wed, 11 Sep 2002 11:29:44 +0200 by jahier · 87afe5b2
      Erwan Jahier authored
      Parent-Version:      0.84
      Version-Log:
      
      source/gen_stubs.ml:
         Add a lurette_stub__ prefix to most function names to make sure
         that there is no name clashes. In particular, oracle can now be
         called oracle.lus ... (but not lurette_stub__oracle.lus, which is not
         so bad...).
      
      Project-Description: Lurette
      87afe5b2
    • Erwan Jahier's avatar
      lurette 0.84 Wed, 11 Sep 2002 10:19:52 +0200 by jahier · 86a22707
      Erwan Jahier authored
      Parent-Version:      0.83
      Version-Log:         empty
      Project-Description: Lurette
      86a22707
    • Erwan Jahier's avatar
      lurette 0.83 Tue, 03 Sep 2002 13:37:10 +0200 by jahier · dad7b1f2
      Erwan Jahier authored
      Parent-Version:      0.82
      Version-Log:
      
      source/lurette.ml:
      source/lurettetop.ml:
      source/command_line.ml, .mli:
      source/solver.ml:
      source/env_state.ml:
      source/rnumsolver.ml:
         Add 2 news options, --draw-edges ans --draw-verteces that makes
         lurette draw among the verteces or on the edges of the convex hull
         of solutons.
      
      Project-Description: Lurette
      dad7b1f2
    • Erwan Jahier's avatar
      lurette 0.82 Mon, 02 Sep 2002 16:59:37 +0200 by jahier · e655b8de
      Erwan Jahier authored
      Parent-Version:      0.81
      Version-Log:
      
      source/lurette.ml:
      source/ima_exe.ml:
         Check that nodes did not changed before redrawing anything
      
         also add a <<q>> command to exit from ima_exe more gently.
      
      Project-Description: Lurette
      e655b8de
    • Erwan Jahier's avatar
      lurette 0.81 Mon, 02 Sep 2002 16:13:16 +0200 by jahier · 8773bbd9
      Erwan Jahier authored
      Parent-Version:      0.80
      Version-Log:
      
      source/control.ml:
         Give a proper error message when one uses a ctrl expr that
         is not defined.
      
      Project-Description: Lurette
      8773bbd9
    • Erwan Jahier's avatar
      lurette 0.80 Mon, 02 Sep 2002 16:07:51 +0200 by jahier · 7344d9ba
      Erwan Jahier authored
      Parent-Version:      0.79
      Version-Log:
      
      source/control.ml:
      source/parse_env.ml:
          Add a new ctrl expr (set_between) to let one set the value of a CE var
          in such a way that it is backtracable within an interval. One rational
          is that it let ones code infinite loops that can be exited when
          the formula is false.
      
      Project-Description: Lurette
      7344d9ba
    • Erwan Jahier's avatar
      lurette 0.79 Thu, 29 Aug 2002 16:55:47 +0200 by jahier · 0f7c0947
      Erwan Jahier authored
      Parent-Version:      0.78
      Version-Log:
      
      source/lurettetop.ml:
         Add a pack command and a --restore option to lurettetop that respectively
         save temporarily created files during a session and restore them
         later on.
      
         Also clean-up temporarily created files when lurettetop resumes.
      
      Project-Description: Lurette
      0f7c0947
    • Erwan Jahier's avatar
      lurette 0.78 Thu, 29 Aug 2002 15:19:15 +0200 by jahier · 98bd35d5
      Erwan Jahier authored
      Parent-Version:      0.77
      Version-Log:
      
      source/parse_env.ml:
         Fix a bug where empty ctrl expr labels were causing
         a parse error.
      
      source/control.ml,mli:
         Add those files to the project as should have been done for a while...
      
         Do not handle infinite values for ctrl expr counters anymore as it is
         useless (and not so easy to be handled properly).
      
      Project-Description: Lurette
      98bd35d5
    • Erwan Jahier's avatar
      lurette 0.77 Thu, 29 Aug 2002 11:46:51 +0200 by jahier · 5f2ead90
      Erwan Jahier authored
      Parent-Version:      0.76
      Version-Log:
      
      source/lurettetop.ml:
         Building every temporary files in /tmp/lurette2313/.
      
      Project-Description: Lurette
      5f2ead90
    • Erwan Jahier's avatar
      lurette 0.76 Wed, 28 Aug 2002 12:58:05 +0200 by jahier · 6298b284
      Erwan Jahier authored
      Parent-Version:      0.75
      Version-Log:
      
      *.ml:
          Avoid using Sys.command  when possible.
      
      Project-Description: Lurette
      6298b284
    • Erwan Jahier's avatar
      lurette 0.75 Wed, 28 Aug 2002 11:13:06 +0200 by jahier · e84a1e8e
      Erwan Jahier authored
      Parent-Version:      0.74
      Version-Log:
      
      makefile.lurette:
      bin/makefile.lurette_lib:
          put all files that do not depend on lurette_stubs into a lib.
      
      source/lurettetop.ml:
          Add a few new options (show, step, ...)
      
      Project-Description: Lurette
      e84a1e8e
    • Erwan Jahier's avatar
      lurette 0.74 Fri, 02 Aug 2002 16:15:33 +0200 by jahier · 105a7f85
      Erwan Jahier authored
      Parent-Version:      0.73
      Version-Log:
      
      source/lurettetop.ml: [new file]
         A top level loop for using lurette.
      
      also remame all .env files using .ima instead of .env as extension.
      
      Project-Description: Lurette
      105a7f85
    • Erwan Jahier's avatar
      lurette 0.73 Mon, 29 Jul 2002 13:49:35 +0200 by jahier · 3764e8b8
      Erwan Jahier authored
      Parent-Version:      0.72
      Version-Log:
      
      gen_stubs.ml:
      sim2chro.ml:
         Do not sort varialble lexicographically but according to
         sut order.
      
      gen_stubs.ml:
         When converting subst list to tuple, do not put fake values
         if the list is empty, but raise a failure (assert false).
      
         Do not parse idl output to guess the conversion between ml
         and C type but hard code it instead. The rational is that
         I was manually calling camlidl here which was confusing
         make sometimes.
      
      make_lurette:
         exit properly before running lurette whenever something bad
         happen during the make.
      
      Project-Description: Lurette
      3764e8b8
    • Erwan Jahier's avatar
      lurette 0.72 Tue, 23 Jul 2002 16:58:52 +0200 by jahier · d27d91fe
      Erwan Jahier authored
      Parent-Version:      0.71
      Version-Log:
      
      sim2cro.ml:
         switch inputs and output in the sim2chro display. The rational
         is that local vars, are closer from ima outputs than sut ones.
         and should then be displayed close to them.
      
      gen_stubs.ml:
         indent generated code better.
      
      Project-Description: Lurette
      d27d91fe
    • Erwan Jahier's avatar
      lurette 0.71 Mon, 22 Jul 2002 16:51:44 +0200 by jahier · 562a6ed5
      Erwan Jahier authored
      Parent-Version:      0.70
      Version-Log:
      
      automata.ml,mli:
      env.ml,mli:
      ima_exe.ml,mli:
      lurette.ml,mli:
         Fix a bug where the control expr were evaluated twice, which
         migth produce strange behavior whenever a CS var was drawn to 0
         in the place, and a value different from 0 in the second place.
         The fix consist in attaching the control.state at automata.t leaves,
         instead of the control expr labels (which was a bit silly BTW).
      
      show_env.ml:
         Fix a small bug in the dot output.
      
      Project-Description: Lurette
      562a6ed5
    • Erwan Jahier's avatar
      lurette 0.70 Fri, 19 Jul 2002 17:31:37 +0200 by jahier · da43be79
      Erwan Jahier authored
      Parent-Version:      0.69
      Version-Log:
      
      ima_exe.ml:
      lurette.ml:
      env_state.ml:
        Factoring out code into  two new functions, clear_step and clear_all.
      
      env_state.ml:
         Do not use to 2 ranges of indexes (one for atomic formula that depends on
      pre,
         one if it is not) but maintain a list a unused indexes instead.
      
      Project-Description: Lurette
      da43be79
    • Erwan Jahier's avatar
      lurette 0.69 Fri, 19 Jul 2002 10:19:59 +0200 by jahier · 135fe2d5
      Erwan Jahier authored
      Parent-Version:      0.68
      Version-Log:
      
      wtree.ml,mli:   (deleted)
      automa.ml,mli:  (new files)
      control.ml,mli: (new files)
      
         Replace the [wtree] module by an [automata] module, that basically
         does the same job, but in a different way. Namely, it no more uses
         the [wtree] DS to use [graph]s instead.  Indeed, the product of
         wtrees introduces some problems, in particular to ensure its
         correctness wrt to the automata run concurrently. Now, everything a
         dead-simple wrt product: we simply perform a quasi-classical automata
         product (well, at least, much closer from a classical product, cf
         paper).
      
         The way loop counters are handled has also changed. Now, counters are
         handled via expressions of a simple arithmetic language that
         basically lets one initialise a variable to an exact or a random
         value (uniform or normal draw) and decrement it. Arcs are now
         labelled by a formula plus 2 expressions of that mini-language (no
         more weigth nor cpt_init stuff). The 1st expression is evaluated
         during the draw, basically performs any operations on counters, and
         returns a positive int that is used as the formula weigth. The second
         expression (a kind of post-condition) is evaluated if its arc is the
         one that has been elected to perform the step.
      
      At several locations long lines (< 80) are reindented.
      
      parse_env.ml:
         In the ima format, IfThenElseExpr becomes IfThenElseNum.
         Also, parse list more cleanly.
      
      graph.ml,mli:
          Add a function that test whether a transition is in the graph.
      
          Do not sort list of transitions anymore (what was the point?).
          Also do not sort nodes in any way.
      
      show_env_env.ml,mli:
         Abstract away nodes and arcs data types (so that I can display
         Automata graphs). rename generate_env_graph into ima_to_dot.
      
      lurette.ml:
      ima_exe.ml:
         Fix a bug where bbd table were filled by asserted non regression expr.
      
      lurette.ml:
         Fix a bug where incorrect data was sent to sim2chro (ie, the output of the
         previous step instead of the ones of the current step.
      
      env_state.ml:
      solver.ml:
      gne.ml:
         Fix a performance bug where I was storing formula indexes even if
         they were depending on inputs or pre, which is stupid as they generally
         won't be used again. In order to fix that, I introduced  new
         atomic_formula <-> indexes table to stote the ones that do not depend
         on inputs apart. It was also necassery to propogate the <<depend on pre>>
         flag inside Gne.gn_expr (which i renamed Gne.t BTW).
      
      Project-Description: Lurette
      135fe2d5
    • 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