1. 24 May, 2004 3 commits
  2. 21 May, 2004 3 commits
  3. 18 May, 2004 1 commit
  4. 17 May, 2004 8 commits
  5. 14 May, 2004 9 commits
  6. 13 May, 2004 3 commits
    • martinez's avatar
      * src/ltlvisit/Makefile.am: Copyright 2004. · 4cd10c3d
      martinez authored
      * src/ltltest/inf.test: More test.
      * src/ltlvisit/basereduc.cc, src/ltlvisit/forminf.cc (spot):
      Use dynamic_cast.
      * src/ltlvisit/reducform.cc, src/ltlvisit/reducform.hh,
      src/ltltest/reduc.test, src/ltltest/reduc.cc: Add an option
      to choose which rules applies to simplify the formula.
      4cd10c3d
    • Alexandre Duret-Lutz's avatar
      * src/ltltest/reduc.test: Typo. · f7e5fe08
      Alexandre Duret-Lutz authored
      f7e5fe08
    • Alexandre Duret-Lutz's avatar
      * src/ltlparse/ltlparse.yy (OP_POST_NEG, OP_POST_POS): New tokens. · 60a3b4ed
      Alexandre Duret-Lutz authored
      (subformula): Recognize `ATOMIC_PROP OP_POST_POS' and
      `ATOMIC_PROP OP_POST_NEG'.
      * src/ltlparse/ltlscan.ll: Introduce the not_prop start condition,
      to restrict the set of atomic propositions allowed in places
      where they are not expected.  Make `true' and `false' case insensitive.
      * src/ltltest/parse.test, src/ltltest/tostring.test: More cases.
      * src/ltlvisit/tostring.cc (to_string_visitor): Quote atomic
      propositions equal to "true" or "false".
      60a3b4ed
  7. 11 May, 2004 2 commits
  8. 10 May, 2004 8 commits
    • Alexandre Duret-Lutz's avatar
      * src/sanity/style.test: New file. · c4a5b325
      Alexandre Duret-Lutz authored
      * src/sanity/Makefile.am (check-local): Run it.
      * src/ltlvisit/nenoform.cc, src/ltlvisit/tostring.cc,
      src/tgba/bdddict.cc, src/tgba/bddprint.cc, src/tgba/tgba.cc,
      src/tgba/tgbaproduct.cc, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/magic.cc, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/reachiter.cc, src/tgbaalgos/gtec/ce.cc,
      src/tgbaalgos/gtec/gtec.cc, src/tgbatest/ltl2tgba.cc: Fix style
      issues reported by style.test.
      c4a5b325
    • Alexandre Duret-Lutz's avatar
      * src/ltltest/inf.cc, src/ltltest/inf.test, src/ltltest/reduc.test, · 69169970
      Alexandre Duret-Lutz authored
      src/ltlvisit/formlength.cc, src/ltlvisit/reducform.cc,
      src/ltlvisit/reducform.hh: Fix copyright year, these files were
      created in 2004.
      69169970
    • Alexandre Duret-Lutz's avatar
      * src/sanity/80columns.test: New file. · 83de4264
      Alexandre Duret-Lutz authored
      * src/sanity/Makefile.am (check-local): Run it.
      * src/ltltest/equals.test, src/ltltest/lunabbrev.test,
      src/ltltest/nenoform.test, src/ltltest/parseerr.test
      src/ltltest/tunabbrev.test, src/ltlvisit/forminf.cc,
      src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
      src/tgbatest/explprod.test, src/tgbatest/spotlbtt.test,
      src/tgbatest/tripprod.test: Wrap long lines.
      83de4264
    • martinez's avatar
    • martinez's avatar
      * src/ltltest/formules.ltl: A pattern of 2000 formulas. · 61e7d4e2
      martinez authored
      * src/ltltest/inf.test: Test some case of implies.
      * src/ltltest/inf.cc: Test some case of implies.
      * src/ltltest/reduc.test: Test reduction of a file of formula.
      * src/ltltest/reduc.cc: Test reduction of a formula.
      
      * src/ltlvisit/formlength.cc: Gives the lenght of a formula.
      * src/ltlvisit/forminf.cc: To know if a formula implies an other.
      * src/ltlvisit/basereduc.cc: Implement only basic reduction.
      * src/ltlvisit/reducform.cc: Implement reduction.
      * src/ltlvisit/reducform.hh: To reduce a formula.
      61e7d4e2
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Refine · faf4a2af
      Alexandre Duret-Lutz authored
      fair_loop_approximation when branching postponement is not used.
      faf4a2af
    • Alexandre Duret-Lutz's avatar
      Cache formula translations, and canonize formulae before doing · 040f8bee
      Alexandre Duret-Lutz authored
      branching postponement.
      * src/tgbaalgos/ltl2tgba_fm.cc (formula_canonizer): New class, with
      bits extracted from fill_dests and ltl_to_tgba_fm.
      (fill_dests, ltl_to_tgba_fm): Adjust to use formula_canonizer.
      040f8bee
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument · aa5cef3c
      Alexandre Duret-Lutz authored
      fair_loop_approx.
      * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Implement the
      fair_loop_approx optimization.
      (ltl_promise_visitor, ltl_possible_fair_loop_visitor,
      possible_fair_loop_checker): New classes.
      * src/tgbatest/ltl2tgba.cc: Add the -L option.
      * src/tgbatest/spotlbtt.test: Exercise fair_loop_approx.
      * wrap/python/cgi/ltl2tgba.in: Make it an option.
      aa5cef3c
  9. 07 May, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument · 6b06e28f
      Alexandre Duret-Lutz authored
      branching_postponement.
      * src/tgbaalgos/ltl2tgba_fm.cc (fill_dests): New function, extracted
      from ltl_to_tgba_fm().
      (ltl_to_tgba_fm): Implement the branching_postponement optimization.
      * src/tgbatest/ltl2tgba.cc: Add the -p option.
      * src/tgbatest/spotlbtt.test: Exercise branching postponement.
      * wrap/python/cgi/ltl2tgba.in: Make it an option.
      6b06e28f
  10. 04 May, 2004 2 commits