1. 28 Feb, 2011 1 commit
    • Erwan Jahier's avatar
      Various improvements in displayed information (stdout/stderr) · 884d2fbb
      Erwan Jahier authored
      - put the seed and the lutin version on stdour (as stderr) so that it appears in the .rif file
      - add a '#' before "The oracle returned false at step" in the rif file
      - Replace every occurence of "the oracle is violated" by "the oracle returned false".
      - Display more information in lutin and check-rif when an oracle returned false.
  2. 24 Feb, 2011 2 commits
    • Erwan Jahier's avatar
      Do not delete existing rif files. · 5099f5dc
      Erwan Jahier authored
      Instead, add an integer suffix to the file name, e.g.,
        lutin -rif toto.rif (...)
      will generate the file toto-2.rif if toto.rif and toto-1.rif already
    • Erwan Jahier's avatar
      Add a --oracle-ec option to lutin. · 69ac49f9
      Erwan Jahier authored
      This was done by moving most of the code from checkRif.ml to
      lustreRun.ml (new module) and coverage.ml, so that checkRif only
      contains administration stuff (dealing with options) plus a simple
      top-level loop.
      I've added some tests in exemple/lutin/oracle.
  3. 21 Feb, 2011 1 commit
    • Erwan Jahier's avatar
      Some work on check-rif. · 2d1cd4ed
      Erwan Jahier authored
      Try to push the reusable part of the code in the coverage and
      LustreRun modules, so that chekRif.ml only contains administration
      stuff (dealing with options) plus a simple top-level loop.
      The rationale would be to be able to reuse that stuff from lutin for
  4. 17 Feb, 2011 1 commit
  5. 16 Feb, 2011 3 commits
    • Pascal Raymond's avatar
      Merge /home/jahier/lurette · 32f5edd6
      Pascal Raymond authored
    • Pascal Raymond's avatar
      lutexe: first usable version · b311ed64
      Pascal Raymond authored
      full tail rec algo abandoned (for the time being)
    • Erwan Jahier's avatar
      Some work on the Alice backend. · 826aa62e
      Erwan Jahier authored
      - Add an option to specify the dir where to put generated C files in.
      - Propagate all lutin options in the C part that fork the lutin interpreter
      (-rif, -precision, -node, -boot)
      - use the Sys.argv.(0) as the lutin interpreter to be called (to make sure
      the same lutin is used and to be able to specify the full path in the C
      file if needed).
  6. 15 Feb, 2011 1 commit
    • Erwan Jahier's avatar
      Some work on check-rif. · 4743771d
      Erwan Jahier authored
      - Split check-rif.ml into check-rif.ml and coverage.ml.
      - Add a section dedicated to check-rif in the Lutin manual, in the tool section.
      - Use the ocaml Arg module to deal with command-line args.
      - Take advantage of the fact that an ec file only have one node.
      - Store/update the corevage info in a .cov file
  7. 11 Feb, 2011 4 commits
  8. 08 Feb, 2011 5 commits
  9. 06 Feb, 2011 1 commit
  10. 05 Feb, 2011 1 commit
  11. 03 Feb, 2011 4 commits
  12. 01 Feb, 2011 1 commit
  13. 31 Jan, 2011 1 commit
  14. 26 Jan, 2011 2 commits
  15. 20 Jan, 2011 1 commit
  16. 15 Jan, 2011 1 commit
    • Pascal Raymond's avatar
      AutoExplore with partial eval no longer used, · 561ba995
      Pascal Raymond authored
      in order to avoid strange "assert" behavior.
      Simu is based on standard AutoGen, thus
      the behavior is the same with simu and compiled luc.
      Warning: the experience of AutoExplore raised
      important problems between Lutin and Lucky semantics:
      should be fixed in a later version !
  17. 14 Jan, 2011 2 commits
  18. 13 Jan, 2011 6 commits
  19. 05 Jan, 2011 2 commits