1. 17 Mar, 2010 40 commits
    • Erwan Jahier's avatar
      lurette 0.126 Fri, 21 Feb 2003 18:49:20 +0100 by jahier · 5a165497
      Erwan Jahier authored
      Parent-Version:      0.125
      Version-Log:
      
      source/command_line_luc_exe.ml:
      source/command_line_luc_exe.mli:
      source/command_line.ml:
      source/command_line.mli:
      source/luc_exe.ml:
      source/lurette.ml:
      source/lurettetop.ml:
         Add the possibility to set the precision from lucky and lurette command
      lines.
      
         Remove the draw-vertices stuff.
      
      source/command_line_luc_exe.ml:
      source/command_line_luc_exe.mli:
      source/luc_exe.ml:
         Also add the --edges and the inside options for lucky.
      
      source/parse_env.ml:
        Allow to forget empty fields in the automata format.
      
      source/store.ml:
         Plug the new drawing heuristic
      
      Project-Description: Lurette
      5a165497
    • Erwan Jahier's avatar
      lurette 0.125 Fri, 21 Feb 2003 16:30:11 +0100 by jahier · 27272998
      Erwan Jahier authored
      Parent-Version:      0.124
      Version-Log:
      
      source/parse_env.ml:
         Make most fields of the automata syntax optional so that
         people are not obliged to refer to empty list of, eg,
         formula.
      
         Also add a field formula that let one defines global formula.
         This field is currently unplugged (ie, it parses, but the information
         contained in that fied in ignored).
      
      Project-Description: Lurette
      27272998
    • Erwan Jahier's avatar
      lurette 0.124 Fri, 21 Feb 2003 14:29:21 +0100 by jahier · 3ea22e95
      Erwan Jahier authored
      Parent-Version:      0.123
      Version-Log:
      
      Implement the polyhedron drawing primitives.
      
      source/util.ml.in:
         Change my_string_of_float so that it truncates floats 4 digits after the
      dot.
         The rational is that, for testing, we do not care the extra precision and
         too much precision may kill Polka. This precison ougth to be a parameter
         though.
      
      source/solver.ml:
      source/polyhedron.ml:
      source/store.ml:
          Implement the polyhedron drawing primitives.
      
      source/store.ml:
         Apply the substitutions in store.subtsl to the cstr to add.
      
      Project-Description: Lurette
      3ea22e95
    • Erwan Jahier's avatar
      lurette 0.123 Tue, 18 Feb 2003 09:49:47 +0100 by jahier · a13cc8e1
      Erwan Jahier authored
      Parent-Version:      0.122
      Version-Log:
      
      source/rnumsolver.mli:
      source/rnumsolver.ml:
      source/store.mli:
      source/store.ml:
         Rename rnumsolver into store.
      
      source/solver.ml:
      source/parse_env.ml:
         Do not explicitely handle dis-equalities but transform it using
         not and = instead. The rational for this change is to avoid code duplication
         (which was buggy !!!), but also to allow handle dis-equalities with
         the optimized algorithm I had for eqalities (for free) !
      
      Project-Description: Lurette
      a13cc8e1
    • Erwan Jahier's avatar
      lurette 0.122 Mon, 17 Feb 2003 14:50:50 +0100 by jahier · 78f40b65
      Erwan Jahier authored
      Parent-Version:      0.121
      Version-Log:
      
      When delayed constraints are remaining at bdd leaves, we were
      printing a message saying that one shoud use a polyhedron solver
      based instead.  Now, I really call such a polyhedron solver in order
      to solve those constraints.
      
      This means that I use to different solvers to handle interval and
      polyhedron of dimension > 1.
      
      It also means that the satisfiability of constraints over polyhedra
      is only checked at bdd leaves, which, in some circumstances, migth be
      inefficient. The point is that, if we chose to check the formula
      satisfiability during the bdd traversal, we take the risk that a very
      polyhedron is created whereas it was not necessary (because of
      forthcoming equalities). And creating polyhedron with big (>15)
      dimension simply runs forever, which is really bad.
      
      nb : drawing in poyhedron not yet plugged.
      
      source/polyhedron.ml:
      source/polyhedron.mli: (new files)
          misc functions over polyhedra. The rational for creating that file
          is that rnumsolver is already much too big (and should be splitted
          some more btw).
      
      source/solver.ml:
         One of the main change is that now, draw_in_bdd returns 2 stores.
         One is Range based, the other one is polyhedron-based.
      
      source/rnumsolver.mli:
      source/rnumsolver.ml:
         Add the function switch_to_polyhedron_representation which
         handle delayed constraint if necessary. It is meant to be called
         at bdd leaves.
      
      source/solver.ml:
      source/rnumsolver.ml:
         Also do not use split_store anymore but add_constraint. This allows
         a much more elegant and efficient implementation of draw_in_bdd and
         draw_in_bdd_eq (Now the store is buid when and only when a new branch
         should be tried because of backtracking). It is also more efficient.
      
      source/constraint.mli
      source/constraint.ml
      source/ne.mli
      source/ne.ml
         Implement get_vars that retreive the variables occuring in a contraint
         or an expression.
      
      Project-Description: Lurette
      78f40b65
    • Erwan Jahier's avatar
      lurette 0.121 Tue, 11 Feb 2003 11:20:37 +0100 by jahier · 34cdff0c
      Erwan Jahier authored
      Parent-Version:      0.120
      Version-Log:
      
      source/pnumsolver.ml:
      source/pnumsolver.mli: [new files]
         Implements a numeric solver based on Polka.
         (not plugged yet).
      
      source/rnumsolver.ml:
         Reimplement split_store so that it uses 2 calls of add_constraint
         instead of doing the work twice inside split_store (in order to avoid code
         duplication).
      
         Also, whenever delayed constraints becomes of dimension 1, when a
      add_constraint
         binds a value, add them to the store.
      
         Enhance error msgs whenever int and float are mixed in the same lucky
         expressions.
      
      source/rnumsolver.ml:
      source/ne.ml:
         rename Ne.resolve_triangular_system into get_subst_from_solved_system
         and move it into rnumsolver. The rational is that is was not
         really solving any triangular system: the system ougth to be already solved.
      
      source/parce_env.ml:
         Set the max_float to max_int, otherwise, the conversion into polka rational
         fails...
      
      Project-Description: Lurette
      34cdff0c
    • Erwan Jahier's avatar
      lurette 0.120 Thu, 19 Dec 2002 11:15:29 +0100 by jahier · d6a175bd
      Erwan Jahier authored
      Parent-Version:      0.119
      Version-Log:
      
      source/solver.ml:
      source/rnumsolver.ml:
         replace split_store_eq by add_eq_to_store as split_store_eq
         was simply calling split store and appendind its result,
         it is simplier to just call slipt_store from solver.ml ...
      
      Project-Description: Lurette
      d6a175bd
    • Erwan Jahier's avatar
      lurette 0.119 Thu, 19 Dec 2002 10:29:35 +0100 by jahier · 566a6b90
      Erwan Jahier authored
      Parent-Version:      0.118
      Version-Log:
      
      user-rules:
          Add the name of the host in the timing result files.
      
          Also runs the timing tests on ecrins.
      
      Project-Description: Lurette
      566a6b90
    • Erwan Jahier's avatar
      lurette 0.118 Wed, 18 Dec 2002 16:40:23 +0100 by jahier · 3b134c21
      Erwan Jahier authored
      Parent-Version:      0.117
      Version-Log:
      
      source/command_line_luc_exe.ml:
         Various minor fixes in printed messages.
      
      remark. The increasing of minor page faults is due to the fact that
      ossau kernel has been upgraded ...
      
      Project-Description: Lurette
      3b134c21
    • Erwan Jahier's avatar
      lurette 0.117 Mon, 18 Nov 2002 14:26:30 +0100 by jahier · fa2dfd3a
      Erwan Jahier authored
      Parent-Version:      0.116
      Version-Log:
      
      Various minor fixes in the documentation
      
      + Use a version of ocaml-3.06 that has been configured with -no-curses,
      which make things sligthly slower, but that avoid the need to find
      the curses lib...
      
      source/ne.ml:
      source/*.ml:
         Ne.find now returns an option value instead of raising a Not_found
         exp, which was not trap in some circumstances...
      
      source/ne.ml:
         Also, fix a couple of bugs where the code was supposing (falsely)
         that the constant (empty string) was always in the Map.
      
      Project-Description: Lurette
      fa2dfd3a
    • Erwan Jahier's avatar
      lurette 0.116 Wed, 13 Nov 2002 13:56:29 +0100 by jahier · aef52d9c
      Erwan Jahier authored
      Parent-Version:      0.115
      Version-Log:
      
      source/solver.ml:
         Give a better error message when users do not initialize pre vars.
      
      source/parse_env.ml:
      source/formula.ml:
      source/prevar.ml/mli: (new files)
         Put here everything that handles the internal representation of pre var
      names.
      
         Pretty print internal pre var names.
      
      Project-Description: Lurette
      aef52d9c
    • Erwan Jahier's avatar
      lurette 0.115 Thu, 07 Nov 2002 14:19:37 +0100 by jahier · 7c4feb61
      Erwan Jahier authored
      Parent-Version:      0.114
      Version-Log:
      
      source/automata.ml:
         Fix a bug where esp loops were not always cutted properly in some cases.
      
      source/show_env.ml:
         Truncate too long for in the dot output (which bugs dot or gv).
      
      ihm/xlurette/xlurette_glade_main.ml:
         Accept both .lut or .lut files as anv files, and make the show buttons
         behave properly in both cases.
      
      Project-Description: Lurette
      7c4feb61
    • Erwan Jahier's avatar
      lurette 0.114 Wed, 06 Nov 2002 13:22:44 +0100 by jahier · f55cbb26
      Erwan Jahier authored
      Parent-Version:      0.113
      Version-Log:
      
      source/parse_env.ml:
         When floats output vars are not constraint, use [-10^11, 10^11]
         as default domain. The rational for this change is that sim2chro
         does not seem to be able to print bigger floats (probably because
         it does not understand the 123e+234 notation.
      
      Project-Description: Lurette
      f55cbb26
    • Erwan Jahier's avatar
      lurette 0.113 Tue, 05 Nov 2002 16:46:57 +0100 by jahier · 4ef40634
      Erwan Jahier authored
      Parent-Version:      0.112
      Version-Log:
      
      source/show_luc.ml:
      source/lurette.ml:
      source/parse_env.ml:
         Enhance error msgs during the .luc parsing. Add the line
         number.
      
      Project-Description: Lurette
      4ef40634
    • Erwan Jahier's avatar
      lurette 0.112 Thu, 31 Oct 2002 08:21:03 +0100 by jahier · dc8f78dc
      Erwan Jahier authored
      Parent-Version:      0.111
      Version-Log:
      
      source/parse_poc.ml: (new file)
      source/gen_stubs.ml:
         put everything that is related to poc parsing into
         parse_poc.ml.
      
      source/gen_fake_lutin.ml: (new file)
      source/parse_poc.ml: (new file)
      source/Makefile.gen_fake_lutin: (new file)
         When no .lut is provided, we generate a fake one.
      
      Project-Description: Lurette
      dc8f78dc
    • Erwan Jahier's avatar
      lurette 0.111 Tue, 29 Oct 2002 14:30:40 +0100 by jahier · a5e54d03
      Erwan Jahier authored
      Parent-Version:      0.110
      Version-Log:
      
      source/util.ml:
      source/formula.ml:
      source/lurette.ml:
         Only print one counter example if the test failed.
      
      source/lurettetop.ml:
      source/gen_stubs.ml:
         try to guess the node name in lurettetop rather than in gen_stubs
         if not given.
      
      Project-Description: Lurette
      a5e54d03
    • Erwan Jahier's avatar
      lurette 0.110 Tue, 29 Oct 2002 11:00:06 +0100 by jahier · 4fe98e62
      Erwan Jahier authored
      Parent-Version:      0.109
      Version-Log:
      
      source/util.ml:
      source/lurettetop.ml:
      source/gen_stubs.ml:
      ihm/xlurette/xlurette_glade_main.ml:
      ihm/xlurette/xlurette.glade:
      
      Add the possibility to specify te sut and the oracle main node
      (to feed the lustre compiler).
      
      Project-Description: Lurette
      4fe98e62
    • Erwan Jahier's avatar
      lurette 0.109 Fri, 25 Oct 2002 17:48:01 +0200 by jahier · 3c9e4e59
      Erwan Jahier authored
      Parent-Version:      0.108
      Version-Log:
      
      ihm/xlurette/xlurette_glade_main.ml:
      source/lurettetop.ml:
         Retreive and print the pid of lurette to be able in xlurette
         to kill the current run.
      
      Project-Description: Lurette
      3c9e4e59
    • Erwan Jahier's avatar
      lurette 0.108 Fri, 25 Oct 2002 16:57:33 +0200 by jahier · 4063d2fa
      Erwan Jahier authored
      Parent-Version:      0.107
      Version-Log:
      
      source/lurette.ml:
      source/command_line.ml
      source/command_line.mli
      source/util.ml:
      source/lurettetop.ml:
         use crete_process instead un sys.command to call lurette from lurettetop
      
      ihm/xlurette/xlurette_glade_main.ml:
         Put the newly generated random seed into the manual text box.
      
      Project-Description: Lurette
      4063d2fa
    • Erwan Jahier's avatar
      lurette 0.107 Fri, 25 Oct 2002 10:51:52 +0200 by jahier · c53e9c14
      Erwan Jahier authored
      Parent-Version:      0.106
      Version-Log:
      
      source/lurettetop.ml:
      ihm/xlurette/.ml:
         fix a bug when reading the .lurette_rc where the the env were added
         instead of beinf overrided when they were both specified in the rc
         file and as a comd line option.
      
      Project-Description: Lurette
      c53e9c14
    • Erwan Jahier's avatar
      lurette 0.106 Fri, 25 Oct 2002 09:36:48 +0200 by jahier · 75100e28
      Erwan Jahier authored
      Parent-Version:      0.105
      Version-Log:
      
      source/lurettetop.ml:
         Add a --prefix <string> option that is added before the call
         to lurette (usefull, eg, for timing purpuses).
      
      source/lurettetop.ml:
      source/lurette.ml:
      source/command_line.ml:
      ihm/xlurette/*
        Add a ---show-step options that let one control whether or not
        the step number is printed.
      
      Project-Description: Lurette
      75100e28
    • Erwan Jahier's avatar
      lurette 0.105 Wed, 23 Oct 2002 13:50:03 +0200 by jahier · 8c181009
      Erwan Jahier authored
      Parent-Version:      0.104
      Version-Log:
      
      ihm/xlurette/*:
         Look up the pipe every 1/10 sec. instead of reading it after
         each command until a certain string is encoutered. It make
         the code more robust (no protocol), it avoid that xlurette
         is blocked during the process. Moreover, it let the progress
         bar works gently.
      
         Add a stop button that sends a sigint to lurettetop that
         ougth to stop the current execution (does not work, why?).
      
      Project-Description: Lurette
      8c181009
    • Erwan Jahier's avatar
      lurette 0.104 Fri, 18 Oct 2002 16:23:42 +0200 by jahier · 15c3bf1d
      Erwan Jahier authored
      Parent-Version:      0.103
      Version-Log:
      
      source/lurettetop.ml:
      source/util.ml:
         use explicit file name so that, e.g., show_luc, is always able to find
         the file it is supposed to show.
      
         Allow users to put extension or not for the sut or oracle files,
         being at the prompt or at the invocation.
      
         cp lurette.ml and lurette.mli in the temp dir and compile it there
         to avoid that everyone is writing on the source dir which
         prevent the next user to use lurette...
      
      Makefile.common.in:
         INCDIRS Ocamlmakeke file var is not supposed to contains path to .h C files
         to include but .mli ocml ones !!!
      
      Project-Description: Lurette
      15c3bf1d
    • Erwan Jahier's avatar
      lurette 0.103 Fri, 11 Oct 2002 17:50:55 +0200 by jahier · 70fca1e8
      Erwan Jahier authored
      Parent-Version:      0.102
      Version-Log:
      
      Add autoconf aupport.
      
      Project-Description: Lurette
      70fca1e8
    • Erwan Jahier's avatar
      lurette 0.102 Mon, 07 Oct 2002 17:53:39 +0200 by jahier · 9f892d0a
      Erwan Jahier authored
      Parent-Version:      0.101
      Version-Log:
      
      Add cuddaux and mlcuddidl to the project.
      
      Also clean-up Makefiles etc in order to make the installation
      process as automatic as possible.
      
      Project-Description: Lurette
      9f892d0a
    • Erwan Jahier's avatar
      lurette 0.101 Fri, 04 Oct 2002 15:38:51 +0200 by jahier · 47cf1f46
      Erwan Jahier authored
      Parent-Version:      0.100
      Version-Log:
      
      Rename any occurence of ima by luc or lucky.
      
      Project-Description: Lurette
      47cf1f46
    • Erwan Jahier's avatar
      lurette 0.100 Fri, 04 Oct 2002 14:21:28 +0200 by jahier · 6095ca23
      Erwan Jahier authored
      Parent-Version:      0.99
      Version-Log:
      
      source/gen_stubs:
         Make sure we are in the rigth directory we calling lus2ec and ec2c.
      
      Project-Description: Lurette
      6095ca23
    • Erwan Jahier's avatar
      lurette 0.99 Fri, 04 Oct 2002 13:49:58 +0200 by jahier · 3797df71
      Erwan Jahier authored
      Parent-Version:      0.98
      Version-Log:
      
      source/solver.ml:
      source/rnumsolver.mli,.ml:
      source/constraint.ml,.mli:
         Split the Constraint.t type into t and ineq where
         inequalities are in ineq. The rational is that most
         operations on constaint.t are actually done on ineq.
         This change therefore avoid pattern like
         <<_ -> assert false>> and let the type checher check
         that sort of things.
      
      Project-Description: Lurette
      3797df71
    • Erwan Jahier's avatar
      lurette 0.98 Fri, 04 Oct 2002 13:06:16 +0200 by jahier · b8ce1df2
      Erwan Jahier authored
      Parent-Version:      0.97
      Version-Log:
      
      source/rnumsolver.ml:
         Remove valI and ValF from the range type as now, when a var is bound,
         it is put into store.substl.
      
      Project-Description: Lurette
      b8ce1df2
    • Erwan Jahier's avatar
      lurette 0.97 Fri, 04 Oct 2002 11:30:11 +0200 by jahier · 5d9a1618
      Erwan Jahier authored
      Parent-Version:      0.96
      Version-Log:
      
      Handling equalities smartlier.    .
      
      Project-Description: Lurette
      5d9a1618
    • Erwan Jahier's avatar
      lurette 0.96 Mon, 30 Sep 2002 16:58:31 +0200 by jahier · 42c10bc1
      Erwan Jahier authored
      Parent-Version:      0.95
      Version-Log:
      
      source/ne.ml,mli:
      source/value.ml,mli:
         (new files) put everything that is related to normal expressions
         and values in thoses 2 new modules.
      
      source/ne.ml,mli:
      source/gne.ml,mli:
         Make the normal expressions and the guarded normal expression abstract.
      
      source/solver.ml:
         also fix a bug in the previous change (forgot to try make test ...)
      
      Project-Description: Lurette
      42c10bc1
    • Erwan Jahier's avatar
      lurette 0.95 Mon, 30 Sep 2002 09:32:45 +0200 by jahier · 9f11061a
      Erwan Jahier authored
      Parent-Version:      0.94
      Version-Log:
      
      Continue to prepare things for the next change (which will try to
      handle equalities smartly).
      
      test/test*.res:
         fix the expected results as this change adds a random toss
         that disturbs the random values.
      
      source/solver.ml:
      source/rnumsolver.ml:
         Add code to handle the fact that the negation of a equality
         is the disjunction of two inegalities, which can not be added
         to store as it is. So we first try with >, and if it fails,
         we try with < (or the other way aroung, depending on a fair toss).
      
         Also split up the code in Solver.draw_in_bdd depending on the
         fact that the current constraint is a boolean, an eq, or an ineg.
      
      source/solver.ml:
         split toss_up_one_var into toss_up_one_var and toss_up_one_var_index,
         one performing the the toss from a var, the other one from a var index.
      
      Project-Description: Lurette
      9f11061a
    • Erwan Jahier's avatar
      lurette 0.94 Fri, 27 Sep 2002 13:20:05 +0200 by jahier · f8219704
      Erwan Jahier authored
      Parent-Version:      0.93
      Version-Log:
      
      Prepare things for the next change (which will try to handle equalities
      smartly).
      
      source/solver.ml:
      source/rnumsolver.ml:
         atomic_formula do not need both < and > (ditto for <= and >=).
         Indeed, I just need to take the opposite, and everything is fine.
         One advantage is that there are less cases to handle. But the key
         advantage is that it make the representation of constraint normal,
         which is important at least when I will try to detect equalities.
      
         Also add a subst list and constraint list fields to the store
         that will ebe used in the forthcoming change. They will resp.
         be used for removeing a dimension when an equality is encountered
         and to delay constraint with more than one variable.
      
      source/constraint.ml,mli: (new files)
         Move there from formula.ml everything that is related to the internal
         representation of constraints.
      
         Also change the name of atomic_formula to linear_constraint, which is
         more informative.
      
      Project-Description: Lurette
      f8219704
    • Erwan Jahier's avatar
      lurette 0.93 Wed, 25 Sep 2002 09:56:41 +0200 by jahier · e9325bcf
      Erwan Jahier authored
      Parent-Version:      0.92
      Version-Log:
      
      source/formula.ml:
      source/solver.ml:
      source/parse_env.ml:
         Handle boolean equalities with Bdd.eq instead of manually
         converting it with <<and>>, <<not>> and <<or>>.
      
      Project-Description: Lurette
      e9325bcf
    • Erwan Jahier's avatar
      lurette 0.92 Mon, 23 Sep 2002 15:58:36 +0200 by jahier · 350840f5
      Erwan Jahier authored
      Parent-Version:      0.91
      Version-Log:
      
      source/parse_env.ml:
          Allow expr a the lhs of comparison operators.
      
          Make comparison operators prefix instead on infix as
          it considerably simplifies the parsing.
      
          Also introduce a == keyword that operates over bool
          to disambiguate things (= is the equality for nums,
          and == the one for bool. Now the lucky grammar
          is truely LL(1), which is nice.
      
      Project-Description: Lurette
      350840f5
    • Erwan Jahier's avatar
      lurette 0.91 Fri, 20 Sep 2002 16:34:48 +0200 by jahier · 1e5a2fe0
      Erwan Jahier authored
      Parent-Version:      0.90
      Version-Log:
      
      source/parse_env.ml:
          Allow a space between a '-' and a numeric value.
      
      Project-Description: Lurette
      1e5a2fe0
    • Erwan Jahier's avatar
      lurette 0.90 Fri, 20 Sep 2002 16:17:27 +0200 by jahier · a02a6397
      Erwan Jahier authored
      Parent-Version:      0.89
      Version-Log:
      
      source/parse_env.ml:
          Allow arbitrary expression in the lhs of boolean
          compararison operators (<,>,=,>=,<=).
      
      Project-Description: Lurette
      a02a6397
    • Erwan Jahier's avatar
      lurette 0.89 Fri, 20 Sep 2002 10:27:47 +0200 by jahier · 35a7ac64
      Erwan Jahier authored
      Parent-Version:      0.88
      Version-Log:
      
      Chech that automata run concurenty do not share any variables.
      
      Project-Description: Lurette
      35a7ac64
    • Erwan Jahier's avatar
      lurette 0.88 Wed, 18 Sep 2002 17:14:51 +0200 by jahier · 28055e17
      Erwan Jahier authored
      Parent-Version:      0.87
      Version-Log:
      
      Turn around the bug in sim2chro where it can not read floats such like 4.
      (pb cause there is not digits...).
      
      Project-Description: Lurette
      28055e17
    • Erwan Jahier's avatar
      lurette 0.87 Wed, 18 Sep 2002 16:50:33 +0200 by jahier · 426e2bb8
      Erwan Jahier authored
      Parent-Version:      0.86
      Version-Log:
      
      Save and restore sessions without messing up directory names
      (namely, avoid name clashes in the /tmp dir).
      
      Project-Description: Lurette
      426e2bb8