1. 28 May, 2009 1 commit
  2. 26 Mar, 2009 1 commit
    • Damien Lefortier's avatar
      Add support for ELTL (AST & parser), and an adaptation of LaCIM · 2fbcd7e5
      Damien Lefortier authored
      for ELTL.  This is a new version of the work started in 2008 with
      LTL and ELTL formulae now sharing the same class hierarchy.
      
      * configure.ac: Adjust for src/eltlparse/ and src/eltltest/
      directories, and call AX_BOOST_BASE.
      * m4/boost.m4: New file defining AX_BOOST_BASE([MINIMUM-VERSION]).
      * src/Makefile.am: Add eltlparse and eltltest.
      * src/eltlparse/: New directory.  Contains the ELTL parser.
      * src/eltltest/: New directory.  Contains tests related to
      ELTL (parser and AST).
      * src/ltlast/Makefile.am: Adjust for ELTL AST files.
      * src/ltlast/automatop.cc, src/ltlast/automatop.hh: New files.
      Represent automaton operators nodes used in ELTL ASTs.
      * src/ltlast/nfa.cc, src/ltlast/nfa.hh: New files.  Represent
      simple NFAs used internally by automatop nodes.
      * src/ltlast/allnode.hh, src/ltlast/predecl.hh,
      src/ltlast/visitor.hh: Adjust for automatop.
      * src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc,
      src/ltlvisit/clone.hh, src/ltlvisit/contain.cc,
      src/ltlvisit/dotty.cc, src/ltlvisit/nenoform.cc,
      src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
      src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
      src/ltlvisit/tostring.cc: Because LTL and ELTL formulae share the
      same class hierarchy, LTL visitors need to handle automatop nodes
      to compile.  When it's meaningful the visitor applies on automatop
      nodes or simply assert(0) otherwise.
      * src/tgba/tgbabddconcretefactory.cc (create_anonymous_state),
      src/tgba/tgbabddconcretefactory.hh (create_anonymous_state): New
      function used by the LaCIM translation algorithm for ELTL.
      * src/tgbaalgos/Makefile.am: Adjust for eltl2tgba_lacim* files.
      * src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/eltl2tgba_lacim.hh: New files.  Implementation of
      the LaCIM translation algorithm for ELTL.
      * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
      Handle automatop nodes in the translation by an assert(0).
      * src/tgbatest/Makefile.am: Adjust for eltl2tgba.* files.
      * src/src/tgbatest/eltl2tgba.cc, src/tgbatest/eltl2tgba.test: New
      files
      2fbcd7e5
  3. 25 Mar, 2009 1 commit
  4. 23 Feb, 2009 2 commits
  5. 18 Feb, 2009 1 commit
  6. 19 Dec, 2008 1 commit
  7. 18 Dec, 2008 1 commit
  8. 20 Jun, 2008 1 commit
  9. 12 Jun, 2008 1 commit
  10. 17 Apr, 2008 1 commit
  11. 14 Apr, 2008 1 commit
    • Alexandre Duret-Lutz's avatar
      Kill some FIXMEs. · 21c98c0a
      Alexandre Duret-Lutz authored
      * src/ltlenv/environment.hh, src/ltlvisit/basicreduce.cc: Remove
      useless FIXMEs.
      * src/ltlvisit/reduce.cc (reduce_visitor::visit(binop)): Compute
      syntactic implications only when needed.
      * src/tgbaalgos/reductgba_sim_del.cc
      (build_recurse_successor_spoiler): Remplace the FIXME by an assert.
      * src/tgba/tgbareduc.cc: Reword some comments, discard old
      commented code.
      21c98c0a
  12. 14 Mar, 2008 2 commits
    • Alexandre Duret-Lutz's avatar
      Make sure Spot compiles with g++-4.3. · d3b702a9
      Alexandre Duret-Lutz authored
      * src/ltlast/formula.hh (hash): Remove const from return type.
      This kills a g++-4.3 warning.
      * src/misc/hash.hh: Adjust to use unordered_set and unordered_map
      from TR1 when g++-4.3 is used.
      * src/evtgba/product.cc, src/ltltest/randltl.cc,
      src/ltlvisit/randomltl.cc, src/ltlvisit/tostring.cc,
      src/misc/freelist.hh, src/misc/optionmap.cc,
      src/tgba/tgbareduc.hh, src/tgbaalgos/gv04.cc,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/randomgraph.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc,
      src/ltltest/equals.cc, src/ltltest/readltl.cc,
      src/ltltest/reduc.cc, src/ltltest/syntimpl.cc,
      src/ltltest/tostring.cc, src/tgbatest/ltlprod.cc,
      src/tgbatest/powerset.cc, src/tgbatest/explprod.cc,
      src/tgbatest/mixprod.cc, src/tgbatest/readsave.cc,
      src/tgbatest/reductgba.cc, src/tgbatest/tgbaread.cc,
      src/tgbatest/tripprod.cc, src/evtgbatest/product.cc,
      src/evtgbatest/readsave.cc, src/evtgbatest/ltl2evtgba.cc,
      src/evtgbatest/readsave.cc: Add missing includes.
      * src/tgbatest/explicit.test, src/tgbatest/explprod.test,
      src/tgbatest/explpro2.test, src/tgbatest/troprod.test,
      src/tgbatest/emptchk.test: Cope with different outputs.
      d3b702a9
    • Alexandre Duret-Lutz's avatar
      Add .gitignore files · 5ef7084b
      Alexandre Duret-Lutz authored
      5ef7084b
  13. 25 Feb, 2008 7 commits
  14. 25 May, 2005 1 commit
  15. 04 May, 2005 1 commit
  16. 20 Feb, 2005 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/sanity/style.test: Catch occurrences of "accepting condition". · a2cbe9ca
      Alexandre Duret-Lutz authored
      * bench/emptchk/ltl-human.sh, bench/emptchk/ltl-random.sh,
      src/sanity/style.test, src/tgba/bdddict.cc,
      src/tgba/succiterconcrete.hh, src/tgba/tgbabddcoredata.hh,
      src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
      src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh,
      src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
      src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
      src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
      src/tgbatest/dfs.test: Replace them by "acceptance condition".
      a2cbe9ca
  17. 18 Feb, 2005 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgbatest/ltl2tgba.cc: Simplify using · 3b3a1965
      Alexandre Duret-Lutz authored
      emptiness_check_instantiator.
      * src/tgba/tgba.cc, src/tgba/tgba.hh
      (tgba::number_of_acceptance_conditions): Return an unsigned.
      * bench/emptchk/algorithms, bench/emptchk/README,
      src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust
      references to algorithms.
      * bench/emptchk/pml-clserv.sh, bench/emptchk/pml-eeaean.sh: Quote
      variables properly.
      3b3a1965
  18. 03 Jan, 2005 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/evtgba/evtgbaiter.hh, src/ltlast/formula.hh, · 000c041a
      Alexandre Duret-Lutz authored
      src/ltlast/refformula.hh, src/ltlenv/defaultenv.hh,
      src/misc/bareword.hh, src/tgba/succiter.hh,
      src/tgba/tgbabddfactory.hh, src/tgba/tgbareduc.hh,
      src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness_stats.hh,
      src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh,
      src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/tau03opt.hh: Add
      or fix include guards.
      * src/sanity/includes.test: Check the presence of the include
      guard.
      000c041a
  19. 15 Dec, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgba/bdddict.hh (bdd_dict) <fv_map, vf_map, ref_set, · 752d4afc
      Alexandre Duret-Lutz authored
      vr_map, free_annonymous_list_of_type>: Redeclare as std::map,
      instead of Sgi::hash_map.  It proved to be faster.
      * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict) <fv_map, vf_map>:
      Use the same definition as in bdd_dict.
      * tgbaalgos/reachiter.hh, tgbaalgos/replayrun.cc: Explicitly
      include misc/hash.hh.
      752d4afc
  20. 10 Dec, 2004 1 commit
  21. 09 Dec, 2004 1 commit
  22. 08 Dec, 2004 2 commits
  23. 17 Nov, 2004 4 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgba.hh, src/tgbaalgos/ltl2tgba_fm.hh, · 32117733
      Alexandre Duret-Lutz authored
      src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/stats.hh: Typos.
      32117733
    • Alexandre Duret-Lutz's avatar
      * src/misc/bareword.hh, src/misc/bddalloc.hh, src/misc/bddlt.hh, · 2a3d638a
      Alexandre Duret-Lutz authored
      src/misc/escape.hh, src/misc/freelist.hh, src/misc/hash.hh,
      src/misc/hashfunc.hh, src/misc/minato.hh, src/misc/modgray.hh,
      src/misc/random.hh, src/misc/version.hh, src/tgba/state.hh: More
      Doxygen groups.
      2a3d638a
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgba.hh, src/tgbaalgos/dotty.hh, · c3e399c8
      Alexandre Duret-Lutz authored
      src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh,
      src/tgbaalgos/emptiness.hh, src/tgbaalgos/lbtt.hh,
      src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh,
      src/tgbaalgos/neverclaim.hh, src/tgbaalgos/powerset.hh,
      src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.hh,
      src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh
      src/tgbaalgos/save.hh, src/tgbaalgos/stats.hh,
      src/tgbaparse/public.hh: Add Doxygen groups for TGBA algorithms.
      c3e399c8
    • Alexandre Duret-Lutz's avatar
      * src/tgba/bdddict.hh, src/tgba/state.hh, src/tgba/statebdd.hh, · 2cd298e4
      Alexandre Duret-Lutz authored
      src/tgba/succiter.hh, src/tgba/succiterconcrete.hh,
      src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
      src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbaexplicit.hh,
      src/tgba/tgbaproduct.hh, src/tgba/tgbareduc.hh,
      src/tgba/tgbatba.hh, src/tgbaalgos/emptiness.hh,
      src/tgbaalgos/magic.hh, src/tgbaalgos/replayrun.hh,
      src/tgbaalgos/gtec/gtec.hh, iface/gspn/ssp.hh: Introduce Doxygen
      groups in the documentation.  Presently this only covers the
      tgba/ directory, and the emptiness-check algorithms.
      * doc/Doxyfile.in (EXCLUDE_PATTERNS): Skip Bison-generated files
      in src/evtgbaparse/.
      2cd298e4
  24. 16 Nov, 2004 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgbatba.hh (tgba_sba_proxy): New class, with the · cac85dbc
      Alexandre Duret-Lutz authored
      functionality of the old tgba_tba_proxy.
      * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator,
      tgba_tba_proxy): Rewrite to produce TBA with at most N copies of
      each state, skipping the `bddtrue' stage now used only in
      tgba_sba_proxy.  Doing so removes approximately 6% of states in
      the degeneralized tests of spotlbtt.test.
      (tgba_sba_proxy): Implement it.
      * src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: Adjust
      to take a tgba_sba_proxy.
      * src/tgbatest/ltl2tgba.cc: Add option -DS and adjust call to
      never_claim_reachable().
      cac85dbc
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgbatba.cc (state_tba_proxy::hash): Use wang32_hash. · ee546210
      Alexandre Duret-Lutz authored
      * src/tgba/tgbaproduct.cc (state_product::hash): Likewise.
      ee546210
  25. 12 Nov, 2004 1 commit
  26. 04 Nov, 2004 1 commit
  27. 03 Nov, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * tgbaalgos/reachiter.hh, tgbaalgos/reachiter.cc · 42b05c7a
      Alexandre Duret-Lutz authored
      (tgba_reachable_iterator::process_link): Take the state* as arguments
      in addition to the state numbers.
      * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
      (tgba_explicit::copy_acceptance_conditions_of): New method.
      * tgbaalgos/dupexp.cc (dupexp_iter::dupexp_iter): Call
      copy_acceptance_conditions_of.
      (dupexp_iter::process_state, duplex_iter::declare_state,
      dupexp_iter::name_): Remove.
      (dupexp_iter::process_link): Adjust prototype, and format
      the state here rather than in process_state.
      * tgbaalgos/stats.cc, tgbaalgos/dotty.cc: Adjust prototype
      of process_link.
      42b05c7a