1. 23 Jun, 2004 1 commit
  2. 22 Jun, 2004 1 commit
  3. 17 Jun, 2004 1 commit
    • martinez's avatar
      * src/tgbatest/spotlbtt.test: We don't check the post-reduction · c769f747
      martinez authored
      with scc and delayed simulation.
      
      * src/tgbatest/ltl2tgba.cc: Adjust parameters.
      * src/tgbatest/reductgba.cc, src/tgbatest/Makefile.am: More Test.
      * src/tgbaalgos/reductgba_sim_del.cc: Not finish, lot of bugs.
      * src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc:
      Remove some useless comments.
      * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: Bug in SCC.
      
      * src/ltlvisit/reducform.cc: Correct some bug for multop.
      * src/ltltest/reduccmp.test: More Test.
      * src/ltltest/reduc.cc: Thinko
      * src/ltltest/equals.cc: Reduction compare
      c769f747
  4. 15 Jun, 2004 1 commit
    • martinez's avatar
      * src/tgbatest/ltl2tgba.cc: Add some option for the reduction of · 8d3606ff
      martinez authored
      automata.
      * src/tgbatest/spotlbtt.test, src/tgbatest/Makefile.am: Add some
      test for reduction of automata.
      * src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc,
      src/tgbaalgos/reductgba_sim.hh: Compute some simulation relation
      to reduce a tgba.
      * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: A implementation
      of tgba for the reduction.
      * src/tgbaalgos/Makefile.am, src/tgba/Makefile.am:
      Add the reduction of automata.
      * src/ltlvisit/syntimpl.cc, src/ltlvisit/basereduc.cc:
      Lot of mistake are corrected.
      * src/ltlvisit/syntimpl.hh, src/ltlvisit/reducform.cc,
      src/ltlvisit/reducform.hh, src/ltltest/reduc.cc: Adjust.
      * src/ltltest/equals.cc, src/ltltest/reduccmp.test,
      src/ltltest/Makefile.am: Add a test for reduction.
      8d3606ff
  5. 02 Jun, 2004 1 commit
  6. 01 Jun, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/ltltest/inf.cc, src/ltltest/inf.test: Rename as ... · 6e3fd873
      Alexandre Duret-Lutz authored
      * src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test: ... these.
      * src/ltltest/Makefile.am: Adjust.
      * src/ltlvisit/forminf.cc: Rename as...
      * src/ltlvisit/syntimpl.cc: ... this.
      * src/ltlvisit/syntimpl.hh: New file with definitions extracted
      from ...
      * src/ltlvisit/reducform.hh: ... this one.
      * src/ltlvisit/Makefile.am, src/ltlvisit/reducform.cc: Adjust.
      6e3fd873
  7. 30 May, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/ltlvisit/forminf.cc (form_eventual_universal_visitor, · 121a55c4
      Alexandre Duret-Lutz authored
      inf_form_right_recurse_visitor, inf_form_left_recurse_visitor): Rename
      as ...
      (eventual_universal_visitor, inf_right_recurse_visitor,
      inf_left_recurse_visitor): ... these.
      (is_GF, is_FG): Move ...
      * src/ltlvisit/basereduc.cc (is_GF, is_FG): ... here, since they
      are only used here.
      (basic_reduce_form, basic_reduce_form_visitor): Rename as ...
      (basic_reduce, basic_reduce_visitor): ... these.
      * src/ltlvisit/reducform.cc (reduce_form_visitor): Rename as ...
      (reduce_visitor): ... this.
      * src/ltltest/inf.cc: Adjust calls.
      * src/sanity/style.test: Improve missing-space after coma detection.
      121a55c4
  8. 26 May, 2004 3 commits
  9. 25 May, 2004 7 commits
  10. 24 May, 2004 2 commits
  11. 17 May, 2004 5 commits
  12. 14 May, 2004 3 commits
  13. 13 May, 2004 2 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/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
  14. 10 May, 2004 4 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
      *** empty log message *** · bafc92d0
      martinez authored
      bafc92d0
  15. 21 Apr, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/ltlvisit/tostring.hh (to_spin_string): New function. · 8d8af2e5
      Alexandre Duret-Lutz authored
      Convert a formula into a string parsable by Spin.
      * src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: New files.
      Print the never claim in Spin format of a degeneralized TGBA.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgbatest/ltl2tgba.cc: Add the option -N which outputs the
      never claim in Spin format of a degeneralized TGBA.
      * src/tgbatest/ltl2neverclaim.test: New file.
      * src/tgbatest/Makefile.am: Add it.
      8d8af2e5
  16. 30 Jan, 2004 1 commit
  17. 06 Jan, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/ltlvisit/tostring.cc · 8008deed
      Alexandre Duret-Lutz authored
      (to_string_visitor::visit(const atomic_prop*)): Quote propositions
      that start with F, G, or X.
      * src/ltltest/tostring.test: Test quoted propositions.
      * src/tgbaalgos/save.cc (save_bfs::process_state): Escape " and +	characters in formulae.
      * src/tgbatest/readsave.test: Test for this.
      8008deed
  18. 21 Nov, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * COPYING: New file. · 43a91a15
      Alexandre Duret-Lutz authored
      * Makefile.am, configure.ac, doc/Makefile.am, iface/Makefile.am,
      iface/gspn/Makefile.am, iface/gspn/common.cc,
      iface/gspn/common.hh, iface/gspn/dottyeesrg.cc,
      iface/gspn/dottygspn.cc, iface/gspn/eesrg.cc, iface/gspn/eesrg.hh,
      iface/gspn/gspn.cc, iface/gspn/gspn.hh, iface/gspn/ltlgspn.cc,
      src/Makefile.am, src/ltlast/Makefile.am, src/ltlast/allnodes.hh,
      src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
      src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc,
      src/ltlast/constant.hh, src/ltlast/formula.cc,
      src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/multop.hh,
      src/ltlast/predecl.hh, src/ltlast/refformula.cc,
      src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh,
      src/ltlast/visitor.hh, src/ltlenv/Makefile.am,
      src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh,
      src/ltlenv/environment.hh, src/ltlparse/Makefile.am,
      src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy,
      src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
      src/ltlparse/public.hh, src/ltltest/Makefile.am,
      src/ltltest/defs.in, src/ltltest/equals.cc,
      src/ltltest/equals.test, src/ltltest/lunabbrev.test,
      src/ltltest/nenoform.test, src/ltltest/parse.test,
      src/ltltest/parseerr.test, src/ltltest/readltl.cc,
      src/ltltest/tostring.cc, src/ltltest/tostring.test,
      src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test,
      src/ltlvisit/Makefile.am, src/ltlvisit/clone.cc,
      src/ltlvisit/clone.hh, src/ltlvisit/destroy.cc,
      src/ltlvisit/destroy.hh, src/ltlvisit/dotty.cc,
      src/ltlvisit/dotty.hh, src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
      src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh,
      src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh,
      src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
      src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
      src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
      src/misc/Makefile.am, src/misc/bddalloc.cc, src/misc/bddalloc.hh,
      src/misc/bddlt.hh, src/misc/hash.hh, src/misc/minato.cc,
      src/misc/minato.hh, src/misc/version.cc, src/misc/version.hh,
      src/tgba/Makefile.am, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
      src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/public.hh,
      src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh,
      src/tgba/succiter.hh, src/tgba/succiterconcrete.cc,
      src/tgba/succiterconcrete.hh, src/tgba/tgba.cc, src/tgba/tgba.hh,
      src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
      src/tgba/tgbabddconcretefactory.cc,
      src/tgba/tgbabddconcretefactory.hh,
      src/tgba/tgbabddconcreteproduct.cc,
      src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc,
      src/tgba/tgbabddcoredata.hh, src/tgba/tgbabddfactory.hh,
      src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
      src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
      src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
      src/tgbaalgos/Makefile.am, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/dotty.hh, src/tgbaalgos/dupexp.cc,
      src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptinesscheck.cc,
      src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/magic.cc,
      src/tgbaalgos/magic.hh, src/tgbaalgos/reachiter.cc,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/save.cc,
      src/tgbaalgos/save.hh, src/tgbaparse/Makefile.am,
      src/tgbaparse/fmterror.cc, src/tgbaparse/parsedecl.hh,
      src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
      src/tgbaparse/tgbascan.ll, src/tgbatest/Makefile.am,
      src/tgbatest/bddprod.test, src/tgbatest/defs.in,
      src/tgbatest/dupexp.test, src/tgbatest/emptchk.test,
      src/tgbatest/emptchke.test, src/tgbatest/explicit.test,
      src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
      src/tgbatest/explprod.test, src/tgbatest/ltl2tgba.test,
      src/tgbatest/ltlprod.test, src/tgbatest/mixprod.test,
      src/tgbatest/readsave.test, src/tgbatest/spotlbtt.test,
      src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test,
      wrap/Makefile.am, wrap/python/Makefile.am, wrap/python/buddy.i,
      wrap/python/spot.i, wrap/python/cgi/Makefile.am,
      wrap/python/cgi/ltl2tgba.in, wrap/python/tests/Makefile.am,
      wrap/python/tests/bddnqueen.py, wrap/python/tests/interdep.py,
      wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test,
      wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py,
      wrap/python/tests/run.in: Add Copyright license.
      43a91a15
  19. 28 Aug, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      Rewrite all std::map<const formula*, ...> as · 19551509
      Alexandre Duret-Lutz authored
      Sgi::hash_map<const formula*, ...>.
      
      * src/misc/hash.hh: New file.
      * src/misc/Makefile.am (misc_HEADERS): Add it.
      * src/ltlvisit/dotty.cc (dotty_visitor::map): Use a hash_map instead
      of a map.
      * src/tgba/bdddict.hh (bdd_dict::fv_map, bdd_dict::vf_map,
      bdd_dict::ref_set, bdd_dict::var_map): Define as hash_map or
      hash_set.
      * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::fv_map,
      translate_dict::vf_map): Likewise.
      * src/tgba/tgbabddconcretefactory.hh
      (tgba_bdd_concrete_factory::acc_map_): Likewise.
      * src/tgba/tgbatba.hh, src/tgbaalgos/reachiter.hh: Include <map>.
      19551509
  20. 10 Aug, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      Revamp the multop interface to allow some basic optimizations like · de6314ed
      Alexandre Duret-Lutz authored
      not constructing a single-child multop.
      * src/ltlast/multop.hh (multop::instance(type)): Remove.
      (multop::instance(type, formula*, formula*)): Return a formula*.
      (multop::instance(type, vec*)): Make it public and return a formula*.
      (multop::add_sorted, multop::add):
      * src/ltlast/multop.cc (multop::instance(type, vec*)): Rewrite.
      (multop::instance(type)): Delete.
      (multop::instance(type, formula*, formula*)): Adjust.
      (multop::add_sorted, multop::add): Remove.
      * src/ltlvisit/clone.cc (clone_visitor::visit(multop*)) Adjust.
      * src/ltlvisit/nenoform.cc
      (negative_normal_form_visitor::::visit(multop*)) Adjust.
      * src/ltltest/equals.test: Make sure `a & a' and `a' are equals.
      * wrap/python/tests/ltlsimple.py: Adjust.
      de6314ed
  21. 06 Aug, 2003 1 commit