- 25 Feb, 2008 14 commits
-
-
Alexandre Duret-Lutz authored
Suggested by Akim.
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/emptiness_stats.hh (unsigned_statistics_copy): New class.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
heuristic.
-
Alexandre Duret-Lutz authored
(tau03_opt_search): Add option "ordering" (off by default). If enabled, initialize an explicit ordering for acceptance conditions into the new member "cond" (a vector of bdds). (project_acc): New helper function for projecting a set of acceptance conditions to a subset that maximizes the number of initial consecutive conditions covered by the set in the condition ordering. (dfs_blue): Implement the ordering heuristic. (dfs_red): Use a sentinel in condition_stack to avoid explicit checks for the stack's emptiness. Consider also the conditions in acc when checking for the completion of an accepting cycle. Fix the implementation of condition heuristic. Implement the ordering heuristic. Simplify the removal of elements from condition_stack (due to the way in which elements are pushed on the stack, there can be at most one element with a given depth in the stack at any one time).
-
Alexandre Duret-Lutz authored
Initialize tmp to suppress a GCC 4.0 warning. * src/ltltest/randltl.cc (main): Likewise with another variable.
-
Alexandre Duret-Lutz authored
virtual destructors. * src/tgba/tgbabddfactory.hh (tgba_bdd_factory): Likewise. * src/misc/hash.hh: Use the std namespace only with GCC 3.0, not with all compiler versions with minor version 0. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): Fix friend declaration of ::spot::tgba_tba_proxy.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
Conflicts: lbtt/INSTALL lbtt/doc/texinfo.tex lbtt/src/LbttAlloc.h Finish merge
-
Alexandre Duret-Lutz authored
-
- 31 Aug, 2005 2 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
- 06 Jun, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
(parity_game_graph_delayed::get_relation): Disable for generalized automata, it's wrong.
-
- 25 May, 2005 2 commits
-
-
Alexandre Duret-Lutz authored
(parity_game_graph_delayed::nb_set_acc_cond): Simplify.
-
Alexandre Duret-Lutz authored
* tgba/tgbareduc.hh, tgbaalgos/reductgba_sim.cc, tgbaalgos/reductgba_sim.hh, tgbaalgos/reductgba_sim_del.cc: Fix them.
-
- 16 May, 2005 1 commit
-
-
Denis Poitrenaud authored
-
- 14 May, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
-
- 12 May, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
-
- 04 May, 2005 2 commits
-
-
Alexandre Duret-Lutz authored
* src/misc/hash.hh (ptr_hash): Use knuth32_hash. * src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory): Use ltl::formula_ptr_hash for acc_map_.
-
Alexandre Duret-Lutz authored
the reduce_ltl argument. * src/tgbatest/ltl2tgba.cc: Add options -fr1, -fr2, -fr3, and -fr4. * src/tgbatest/spotlbtt.test, bench/ltl2tgba/algorithms: Test -fr4. * bench/ltl2tgba/parseout.pl: Suppress Perl warnings on disabled algorithms.
-
- 19 Apr, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
* bench/Makefile.am (SUBDIRS): Add ltl2tgba. * README: Mention bench/ltl2tgba.
-
- 15 Apr, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
bench/ltl2tgba/algorithms, bench/ltl2tgba/big, bench/ltl2tgba/defs.in, bench/ltl2tgba/formulae.ltl, bench/ltl2tgba/known, bench/ltl2tgba/parseout.pl, bench/ltl2tgba/small: New files. * src/tgbatest/ltl2baw.pl: Move ... * bench/ltl2tgba/ltl2baw.in: ... here. * src/tgbatest/Makefile.am: Adjust. * configure.ac: Adjust.
-
- 14 Apr, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
before the degeneralized automaton.
-
- 13 Apr, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
-
- 12 Apr, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
-
- 09 Apr, 2005 2 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
- 08 Apr, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
http://spot.lip6.fr/wiki/EmptinessCheckOptions for the syntax.
-
- 06 Apr, 2005 2 commits
-
-
Alexandre Duret-Lutz authored
an undeclared acceptance condition. * src/tgbaalgos/save.cc (print_acc): Unquote atomic propositions.
-
Alexandre Duret-Lutz authored
* bench/emptchk/pml2tgba.pl: Add option -r. * bench/emptchk/pml-clserv.sh, bench/emptchk/pml-eeaean.sh: Also run on reduced graphs (this is fast). * bench/emptchk/README: Adjust.
-
- 23 Feb, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
postfix_visitor.
-
- 22 Feb, 2005 2 commits
-
-
Alexandre Duret-Lutz authored
and "redweights" (on by default).
-
Alexandre Duret-Lutz authored
account for the size of condition_stack.
-
- 20 Feb, 2005 2 commits
-
-
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".
-
Alexandre Duret-Lutz authored
misc/optionmap.hh.
-
- 18 Feb, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
-