• Erwan Jahier's avatar
    lurette 1.42 Fri, 20 Jan 2006 15:06:27 +0100 by jahier · 04e06981
    Erwan Jahier authored
    Parent-Version:      1.41
    Version-Log:
    
    source/luc_exe.ml
    source/command_line_luc_exe.ml
    source/lurette.ml
    source/graph.ml
    source/lucky.mli
    source/lucky.ml
    source/util.ml
    source/formula_to_bdd.ml
    source/formula_to_bdd.mli
    source/fair_bddd.ml
    source/fair_bddd.mli
    source/bddd.ml
    source/bddd.mli
    source/solver.mli
    source/solver.ml
    source/polyhedron.ml
    source/polyhedron.mli
    source/store.mli
    source/store.ml
    source/parse_luc.mli
    source/parse_luc.ml
    source/show_env.ml
    source/env_state.mli
    source/env_state.ml
    source/run_aut.mli
    source/run_aut.ml
    source/lurettetop.ml
    source/draw.mli
    source/draw.ml
    source/gen_stubs.ml
    source/parse_c_scade.ml
    source/ne.ml
    source/prevar.ml
    source/prevar.mli
    source/show_luc.ml
    utils/lucky.el
    install/configure.in
    Makefile.common.source
    install/Makefile.lurette.in
    user-rules
    source/Makefile.lurettetop
    source/Makefile.gen_fake_lutin
    source/Makefile.show_luc
    source/Makefile.lucky
    source/Makefile.gen_stubs
    source/Makefile.lurette_lib
    source/Makefile
    RUN_ME
    TODO
    test/time-joly.exp
    test/time-joly.res
    test/time-ecrins.exp
    ihm/xlurette/xlurette_glade_main.ml
    ihm/xlurette/xlurette_glade_interface.ml
    ihm/xlurette/makefile
    polka/caml/Makefile
    polka/Makefile.config
    source/Makefile.gen_fake_lucky
    install/xlurette_sh.in
    install/xlurette.sh.in
    install/xlurette.bat.in
    install/set_env_var.in
    install/lurettetop_sh.in
    install/lurettetop.sh.in
    install/lurettetop.bat.in
    install/gen_stubs.sh.in
    source/poly_draw.ml
    source/poly_draw.mli
    source/lustreExp.ml
    source/lustreExp.mli
    source/exp.ml
    source/var.ml
    source/type.mli
    examples/xlurette/fault-tolerant-heater/degradable-sensors.luc
    examples/xlurette/fault-tolerant-heater/heater_control_env.luc
    examples/xlurette/fault-tolerant-heater/sensors.luc
    source/parser.mly
    doc/lurette-man/lurette-man.tex
    source/parse_sildex.ml
    test/time-asti.exp
    RELEASE-NOTES
    FAQ
    source/gnuplot-socket.ml
    source/luc4ocaml.ml
    source/luc4ocaml.mli
    source/Makefile.gnuplot-rif
    source/gnuplot-rif.ml
    source/luckyDraw.mli
    source/luckyDraw.ml
    source/luc4ocaml_nolbl.mli
    source/luc4ocaml_nolbl.ml
    source/lucky2lus.ml
    source/Makefile.luc4ocaml
    source/Makefile.lurette_ocaml_lib
    source/Makefile.lurette_debug
    source/Makefile.luckyDraw
    source/Makefile.lucky2lus
    xlurette/Scade/GenMake_l4sim.tcl
    examples/lucky/external_code/call_external_c_code.luc
    examples/lucky/external_code/Makefile
    VERSION
    install/configure
    install/set_env_var.bat.in
    
    Quite a lot of changes this time... far too much...
    
    Fix a at least 5 bugs, and re-organize directories, in particular
    the test dir. too much to say...
    
     * pre pre x was always equal to pre x (bugs introduced in 1.39 or something
    I think...).
     * ...
    
    One big improvment is that I have completely changed the way runtime automaton
    are handled, using continuations instead of maitaining an explicit
    data-structure.
    This let me reduce the run_aut module by 75 percent, resulting in much clearer
    code, and less buggy, and more efficient. ouaw!
    
    thanks to that, I support DAG now (was rejected before).
    
    The executable that do not need env var are no more called via a script that
    call set_env_var, so that they are fully stand-alone: show_luc, lucky,
    gen_fake_lucky. This is why util was splitted (util+util2)
    
    source/var.ml
    source/lucaml.ml  -> luc4ocaml.ml
    source/lucaml.mli -> luc4ocaml.mli
    
    source/run_aut.ml:
       Fix a bug during the backtraking in the dynamic tree.
    
    source/env_state.ml
    
    source/formula_to_bdd.ml
       sort the list of free index, because the first order of variable is
    generally
       better.
    
    source/bddd.ml
    source/bddd.mli
    source/solver.mli
    source/solver.ml
    source/polyhedron.ml
    source/polyhedron.mli
    source/store.mli
       Add the verbosity level in a few functions.
    
    source/store.ml
       FIX A BUG in the bdd traversal. Some branches were never visited because
       I was raising a No_numeric_solution exception instead od returning an empty
       store when adding a constraint... This embarassing bug is there from the
       begining... Ouille!
    
       Also, when a valid integer cannot be found, return a wrong one, which is a
       bug really. But is it better than the current state were raising the no_num
       expt would cut some branches in the bdd. I will fix that problem later.
    
    source/parse_luc.ml
    source/lustreExp.ml
    source/lustreExp.mli
       The list of pre vars was computed with a ref, which is bad. Moreover,
       the same pre var was created with different indexes, which did not lead
       to incorrect behavior, but still...
    
    source/exp.ml
    test/bj.luc
    examples/lucky/external_code/call_external_c_code.luc
    examples/lucky/external_code/Makefile
    
    Project-Description: Lurette
    04e06981
time-joly.res 12.8 KB