1. 09 Nov, 2009 2 commits
    • Alexandre Duret-Lutz's avatar
      Deprecate ltl::destroy(f) in favor of f->destroy() · 77df39b4
      Alexandre Duret-Lutz authored
      * src/ltlast/formula.cc, src/ltlast/formula.hh (formula::clone):
      Transform this static function into a member function.
      * src/ltlvisit/destroy.hh (destroy): Document and declare as
      deprecated.
      * bench/split-product/cutscc.cc, iface/gspn/ltlgspn.cc,
      src/eltlparse/eltlparse.yy, src/eltltest/acc.cc,
      src/evtgbaalgos/tgba2evtgba.cc, src/evtgbatest/ltl2evtgba.cc,
      src/ltlast/automatop.cc, src/ltlast/binop.cc,
      src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlenv/declenv.cc,
      src/ltlenv/declenv.hh, src/ltlparse/ltlparse.yy,
      src/ltltest/equals.cc, src/ltltest/randltl.cc,
      src/ltltest/readltl.cc, src/ltltest/reduc.cc,
      src/ltltest/syntimpl.cc, src/ltltest/tostring.cc,
      src/ltlvisit/destroy.cc src/ltlvisit/basicreduce.cc,
      src/ltlvisit/contain.cc, src/ltlvisit/reduce.cc,
      src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc,
      src/tgba/bddprint.cc, src/tgba/taa.cc,
      src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbaexplicit.cc,
      src/tgba/tgbafromfile.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/randomgraph.cc, src/tgbaparse/tgbaparse.yy,
      src/tgbatest/complementation.cc, src/tgbatest/eltl2tgba.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
      src/tgbatest/mixprod.cc, src/tgbatest/randtgba.cc,
      src/tgbatest/reductgba.cc, wrap/python/cgi/ltl2tgba.in,
      wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py,
      wrap/python/tests/ltlsimple.py: Adjust destroy() usage, and remove
      the #include "destroy.hh" when appropriate.
      77df39b4
    • Alexandre Duret-Lutz's avatar
      Add missing instance_count() in automatop and eltl2tgba. · f2e941cd
      Alexandre Duret-Lutz authored
      * src/ltlast/automatop.hh, src/ltlast/automatop.cc: Add missing
      instance_count() functions.
      * src/tgbatests/eltl2tgba.cc: Add missing instance_count()
      assertions at the end.
      * src/tgbatests/ltl2tgba.cc: Also call automatop::instance_count(),
      even if automatop are not used in ltl2tgba yet.  This way we won't
      forget once eltl2tgba and ltl2tgba are merged.
      f2e941cd
  2. 03 Nov, 2009 1 commit
  3. 22 Oct, 2009 1 commit
    • Damien Lefortier's avatar
      Improve ltl_to_taa. · 7ce27ef9
      Damien Lefortier authored
      * src/tgba/taa.cc, src/tgba/taa.hh: taa_succ_iterator is not
      on-the-fly anymore allowing some redundant transitions to be
      removed. Also a new function to output a TAA.
      * src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh: Add the
      refined rules from Tauriainen.
      * src/tgbatest/ltl2tgba.cc: Use -c to activate refined rules in
      ltl_to_taa.
      * src/tgbatest/spotlbtt.test: More tests.
      7ce27ef9
  4. 16 Oct, 2009 1 commit
    • Damien Lefortier's avatar
      Add a new algorithm (from Tauriainen) to translate LTL formulae to · 627b6677
      Damien Lefortier authored
      TGBA which uses TAA as an intermediate representation.  This is a
      basic version, optimizations and enhancements will come later.
      
      * src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh: The algortihm.
      * src/tgbaalgos/Makefile.am: Adjust.
      * src/tgbatest/ltl2tgba: New option: -taa, which uses this new
      translation algorithm.
      * src/tgbatest/spotlbtt.test: Add ltl2tgba -taa.
      627b6677
  5. 01 Oct, 2009 1 commit
  6. 28 May, 2009 2 commits
    • Alexandre Duret-Lutz's avatar
      Implement spot::future_conditions_collector. · d74578ef
      Alexandre Duret-Lutz authored
      * src/tgba/futurecondcol.hh, src/tgba/futurecondcol.cc:
      New files.
      * src/tgba/Makefile.am: Adjust.
      * src/tgbatest/ltl2tgba.cc: Add option -FC.
      d74578ef
    • Alexandre Duret-Lutz's avatar
      Keep track of conditions in SCC, and add a more verbose dump. · 07ead613
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/scc.hh (scc_map::scc_of_state,
      scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of):
      New functions.
      (scc_map::scc::conds): New attribute.
      (dump_scc_dot): Take an optional VERBOSE argument.
      * src/tgbaalgos/scc.cc (scc_map::scc_of_state,
      scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of):
      Implement these new functions.
      (dump_scc_dot): Display number of states, conditions and
      acceptance conditions, with VERBOSE is set.
      (build_map): Fill the new scc_map::scc::cond field.
      07ead613
  7. 25 Mar, 2009 1 commit
  8. 10 Dec, 2008 2 commits
  9. 12 Jun, 2008 1 commit
  10. 21 Mar, 2008 1 commit
  11. 14 Mar, 2008 1 commit
    • 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
  12. 25 Feb, 2008 7 commits
  13. 04 May, 2005 1 commit
  14. 14 Apr, 2005 1 commit
  15. 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
  16. 16 Feb, 2005 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/misc/optionmap.cc, src/misc/optionmap.hh (option_map::get, · f3effb9d
      Alexandre Duret-Lutz authored
      option_map::set): Handle default values.
      (anonymous::to_int): Do not print anything.
      * src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
      src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
      src/tgbaalgos/ce.cc, src/tgbaalgos/ce.hh: Take an option_map in
      the constructor.
      * src/tgbaalgos/gtec.cc, src/tgbaalgos/gtec.hh: Likewise.  Handle
      the "poprem", "group", and "shy" options via the option_map.
      Supply a couvreur99() wrapper to the shy/non-shy variant.
      * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc,
      iface/gspn/ssp.cc: Adjust.
      f3effb9d
  17. 29 Jan, 2005 1 commit
  18. 28 Jan, 2005 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptiness_stats.hh: Make sure depth() >= 0. · 5fb5b684
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/gtec/gtec.hh (couvreur99_check, couvreur99_check_shy):
      Add the poprem option.
      * src/tgbaalgos/gtec/gtec.cc: Implement it.
      * src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh
      (scc_stack::rem, scc_stack::clear_rem,
      scc_stack::connected_component::rem): New.
      * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Add rem variants.
      5fb5b684
    • Denis Poitrenaud's avatar
      * src/tgbatest/dfs.test, src/tgbatest/emptchk.test, · b1800e38
      Denis Poitrenaud authored
      src/tgbatest/emptchke.test, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/randtgba.cc, src/tgbatest/tba_samples_from_spin.test:
      Adjust names of emptiness check algorithms.
      b1800e38
  19. 25 Jan, 2005 1 commit
  20. 24 Jan, 2005 1 commit
  21. 10 Jan, 2005 2 commits
  22. 16 Dec, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/ltlparse/ltlscan.ll: Pass yyleng to the std::string constructor, · 0efca0f6
      Alexandre Duret-Lutz authored
      so it doesn't have to compute it.
      * src/tgbaparse/tgbascan.ll: Likewise.
      (YY_USER_INIT, current_file): Remove, it is too costly to use
      yy::Location::filename in the current implementation
      of yy::Location (this attribute is duplicated for each token).
      Leaving it empty divides the parsing time by 3.
      * src/tgbaparse/fmterror.cc, src/tgbaparse/public.hh
      (format_tgba_parse_errors): Take the filename as argument.
      * src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc,
      src/tgbatest/readsave.cc, src/tgbatest/reductgba.cc,
      src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc,
      iface/gspn/dottyssp.cc, iface/gspn/ltlgspn.cc: Adjust calls
      to format_tgba_parse_errors.
      0efca0f6
  23. 14 Dec, 2004 1 commit
  24. 10 Dec, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc · 9782b822
      Alexandre Duret-Lutz authored
      (couvreur99_check_shy::couvreur99_check_shy): Add the group option,
      and redefine todo as a list so it can be iterated over.
      * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Introduce
      couvreur99_shy- (for group=false) in addition to couvreur99_shy
      (for group=true).
      * iface/gspn/ssp.cc (couvreur99_check_ssp_shy_semi,
      couvreur99_check_ssp_shy): Use group=true;
      9782b822
  25. 08 Dec, 2004 1 commit
  26. 29 Nov, 2004 1 commit
  27. 28 Nov, 2004 1 commit
  28. 27 Nov, 2004 1 commit
  29. 22 Nov, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh: New files, partly · 6cce60be
      Alexandre Duret-Lutz authored
      based on Thomas Martinez's src/tgbaalgos/tarjan_on_fly.cc and
      src/tgbaalgos/tarjan_on_fly.hh former implementation.
      * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES,
      tgbaalgos_HEADERS): Add them.
      * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Bind the
      new algorithm.
      * src/tgbatest/emptchk.test: Test it.
      6cce60be