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

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

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

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

Parent-Version:      0.76
Version-Log:

source/lurettetop.ml:
   Building every temporary files in /tmp/lurette2313/.

Project-Description: Lurette

Parent-Version:      0.75
Version-Log:

*.ml:
    Avoid using Sys.command  when possible.

Project-Description: Lurette

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

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

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

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

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

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

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

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

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

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

Parent-Version:      0.64
Version-Log:

Outputs error message on stderr rather than on stdout.

Project-Description: Lurette

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

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

Parent-Version:      0.61
Version-Log:

Reorganise things a little bit so that show_ima does not depend on
cudd, etc.

Project-Description: Lurette

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

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

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

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

Parent-Version:      0.56
Version-Log:

Add a --output options to specify the output file name.

Project-Description: Lurette

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

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

Parent-Version:      0.53
Version-Log:

Cosmetic change:

Encapsulates the various fields of Env_state.

Project-Description: Lurette

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

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

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

Parent-Version:      0.49
Version-Log:

Add the possibility to put pragmas in the .env files.

Project-Description: Lurette

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

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

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

Parent-Version:      0.45
Version-Log:

Clean up a little bit lurette.ml

Project-Description: Lurette

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

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

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

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