2004-12-15 Alexandre Duret-Lutz * src/tgbaparse/tgbaparse.yy: Cache parsed formulae to speedup reading of TGBAs with lots of identical conditions. * src/tgba/bdddict.hh (bdd_dict) : Redeclare as std::map, instead of Sgi::hash_map. It proved to be faster. * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict) : Use the same definition as in bdd_dict. * tgbaalgos/reachiter.hh, tgbaalgos/replayrun.cc: Explicitly include misc/hash.hh. Adjust Swig rules for Swig 1.3.24 (and probably 1.3.23 too). Compiling the runtime in a separate modules is no longer required, and actually it does not work anymore... * wrap/python/swigpy.i: Remove. * wrap/python/Makefile.am (_swigpy.la): Remove all references. ($(srcdir)/spot_wrap.cxx, $(srcdir)/buddy_wrap.cxx): Do not use -noruntime. 2004-12-14 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc: Add option -P. 2004-12-14 Denis Poitrenaud * src/tgbaalgos/ndfs_result.hh: Define the trace output stream. 2004-12-13 Denis Poitrenaud * src/tgbaalgos/ndfs_result.hh: New file factorizing the computation of accepting runs for ndfs emptiness check algoritms. * src/tgbaalgos/Makefile.am: Add it. * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Remove the old result classes and use the new one. 2004-12-10 Alexandre Duret-Lutz * src/tgbaalgos/gtec/status.hh (couvreur99_check_status::cycle_seed): New attribute. * src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check, couvreur99_check_shy::check): Fill cycle_seed. * src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/ce.cc: (couvreur99_check_result::accepting_run, couvreur99_check_result::accepting_cycle): Revamp to compute a cycle from the cycle_start, and then the shortest prefix to this cycle. * iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh, iface/gspn/ssp.cc: Disable the functions that were using the interface I have just broken. * src/tgbaalgos/gtec/nsheap.hh (numbered_state_heap::find): Clarify comment. * src/tgba/tgbareduc.hh: Include tgbaalgos/gtec/nsheap.hh, not tgbaalgos/gtec/status.hh. 2004-12-10 Denis Poitrenaud * src/misc/timer.cc, src/tgbatest/randtgba.cc: Format the statistics. 2004-12-10 Alexandre Duret-Lutz * src/tgbatest/emptchkr.test: Tune the "big degeneralized" test so it actually explore some accepting automata. * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc (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; * src/tgbaalgos/randomgraph.cc (random_graph): Do not use the pointer of the state created as keys in sets; otherwise the graph created depends on the memory layout. 2004-12-09 Alexandre Duret-Lutz * src/tgba/tgbaexplicit.cc (tgba_explicit::create_transition): Make sure to create the source state before the destination state. 2004-12-08 Denis Poitrenaud * src/tgbaalgos/emptiness.cc: Suppress a horrible space before a ')'. 2004-12-08 Denis Poitrenaud * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc (set_init_state): Return a pointer to the initial state. * src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness.cc (tgba_run_to_tgba): New function. * src/tgbatest/ltl2tgba.cc: Add option -G. 2004-12-08 Alexandre Duret-Lutz * src/tgbaalgos/replayrun.cc (replay_tgba_run): More comments. * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh (tgba_explicit::create_transition(state*, const state*)): New function. * src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh: (random_graph): Revamp the algorithm to call rand() less often. * src/tgbatest/randtgba.cc: Add option -0 to easy profiling. * src/misc/random.hh: Add include guard. 2004-12-07 Alexandre Duret-Lutz * src/misc/random.hh (nrand, bmrand, prand): New functions. (barand): New class. * src/misc/random.cc (nrand, bmrand, prand): New functions. * wrap/python/spot.i: Process src/misc/random.hh. * src/misc/timer.cc: Do not include cassert, then. 2004-12-07 Denis Poitrenaud * src/tgbaalgos/tau03opt.cc: Fix a memory leak in the computation of accepting runs * src/misc/timer.hh: Include cassert. 2004-12-01 Alexandre Duret-Lutz * src/misc/timer.cc: Include cassert. 2004-11-29 Alexandre Duret-Lutz * src/misc/timer.hh, src/misc/timer.cc: New files. * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them. * src/tgbatest/randtgba.cc: Use time_map to measure the algorithms. Add the -R option. * src/sanity/style.sh: Let me use `for (.*;;)'. 2004-11-29 Denis Poitrenaud * src/tgbaalgos/tau03opt.cc: Add a first version of the computation of accepting runs 2004-11-29 Alexandre Duret-Lutz * src/tgbaalgos/minimizerun.cc, src/tgbaalgos/minimizerun.hh (minimize_run): Rename as ... * src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh: (reduce_run): ... this. * src/tgbaalgos/Makefile.am, src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Adjust all references. * src/tgbatest/emptchkr.test: Try degeneralized automata. * src/tgbatest/randtgba.cc (main): Pass the correct automaton to minimize_run(). 2004-11-28 Alexandre Duret-Lutz * src/ltltest/equals.cc (main): Add option -E. * src/ltltest/parseerr.test: Use `equals -E' instead of `readltl' to check the parsing of erroneous strings without being sensible to the ordering for formulae in memory. * src/tgbatest/randtgba.cc (to_float): Use strtod() instead of strtof() to please Solaris 9. * configure.ac (AM_INIT_AUTOMAKE): Use option tar-ustar, we have filenames longer than 99 bytes. * wrap/python/tests/run.in: Do not override PYTHONPATH, just add to it. Report from Akim Demaille. * src/sanity/style.test: Make sure grep supports the options put into GREP_OPTIONS. * wrap/python/tests/run.in: Define DYLD_LIBRARY_PATH so that Darwin finds non-installed libraries. Report from Akim Demaille. * src/tgbatest/ltl2tgba.cc (syntax): Mention gv04 in help text. 2004-11-27 Alexandre Duret-Lutz * src/tgbaalgos/minimizerun.cc: Shut up a GCC warning when assert are disabled. 2004-11-27 Alexandre Duret-Lutz Denis Poitrenaud * src/tgbaalgos/minimizerun.hh, src/tgbaalgos/minimizerun.cc: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them/ * src/tgbatest/randtgba.cc, src/tgbatest/ltl2tgba.cc: Add option -m. * src/tgbatest/emptchkr.test: Use -m. 2004-11-25 Denis Poitrenaud * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: Fix comments and debug traces * src/tgbatest/randtgba.cc: Adjust names of algorithms. 2004-11-25 Alexandre Duret-Lutz * src/tgbatest/randtgba.cc: Add option -D. * src/tgbaalgos/emptiness.hh (emptiness_check, emptiness_check_result): Add the TGBA considered as a protected attribute, and provide an automaton() accessor. * src/tgbaalgos/gv04.cc, src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc, src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/gtec.cc: Adjust to follow this new interface. 2004-11-24 Alexandre Duret-Lutz * src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: Revert previous change (bfs_steps_with_path_conditions turned up useless), and document bfs_step. * src/tgbaalgos/bfssteps.hh (bfs_steps_with_path_conditions): New class. * src/tgbaalgos/bfssteps.cc: Remove includes that are now superfluous. * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run, couvreur99_check_result::accepting_cycle): Rewrite the BFSs using the bfs_steps class. * src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them. * src/tgbaalgos/gv04.cc (gv04::result::accepting_run): Use the new bfs_steps class. 2004-11-23 Alexandre Duret-Lutz * src/tgbaalgos/gv04.cc (gv04::result): New struct to compute counter examples. (gv04:check): Return a gv04::result. 2004-11-23 Denis Poitrenaud * src/tgbaalgos/tau03opt.cc: Fix a warning. 2004-11-22 Alexandre Duret-Lutz * src/tgbaalgos/gv04.cc (gv04): Inherit from ec_statistics. (gv04::check, gv04::push, gv04::pop): Update the statistics for randtgba. (gv04::print_stats): Print them here too. * src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check, couvreur99_check_shy::check): Compute more statistics for randtgba. (couvreur99_check::print_stats): Print these here too. * src/sanity/style.test: Allow "'" after ",". * src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh: New files, partly 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. 2004-11-22 Denis Poitrenaud * src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/weight.cc, src/tgbaalgos/weight.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh, : Add emptiness check statistics capability. * src/tgbatest/randtgba.cc: Print these statistics. * src/tgbatest/ltl2tgba.cc: tau03opt search can deal without acceptance condition. * src/tgbatest/emptchk.test: Test tau03opt search. 2004-11-19 Alexandre Duret-Lutz * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc, src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: Fix copyright year, and do not include . 2004-11-18 Alexandre Duret-Lutz * src/tgbatest/randtgba.cc (main): Add options -z and -Z for statistics. (ce_stat): New struct. 2004-11-17 Denis Poitrenaud * src/tgbaalgos/se05.hh, src/tgbaalgos/tau03.hh: Typo. * src/tgbaalgos/tau03.cc: Suppress optimisations, the algorithm is now the original one. * src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: New files implementing most of all the optimisations of tau03. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Make them public. * src/tgbatest/tba_samples_from_spin.test: Test them. 2004-11-17 Alexandre Duret-Lutz * src/tgba/tgba.hh, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/stats.hh: Typos. * src/tgbatest/Makefile.am (EXTRA_DIST): Distribute the files from tba_samples_from_spin. * src/tgbatest/tba_samples_from_spin.test: Get these example files from $srcdir, for the sake of VPATH builds. (light_run): Remove, not needed. * src/misc/bareword.hh, src/misc/bddalloc.hh, src/misc/bddlt.hh, 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. 2004-11-17 Denis Poitrenaud * src/tgbaalgos/magic.hh: Fix a comment and remove se05 interface. * src/tgbaalgos/magic.cc: Fix a comment. * src/tgbaalgos/se05.hh: New file. * src/tgbaalgos/se05.cc: Fix a comment. * src/tgbaalgos/tau03.hh: New file. * src/tgbaalgos/tau03.cc: New file. * src/tgbaalgos/Makefile.am: Add it. * src/tgbatest/ltl2tgba.cc: Add tau03 new emptiness check. * src/tgbatest/randtgba.cc: Add tau03 new emptiness check. * src/tgbatest/emptchkr.test: Fix a comment. * src/tgbatest/tba_samples_from_spin/explicit1_1.tba, src/tgbatest/tba_samples_from_spin/explicit1_2.tba, src/tgbatest/tba_samples_from_spin/explicit1_3.tba, src/tgbatest/tba_samples_from_spin/explicit1_4.tba, src/tgbatest/tba_samples_from_spin/explicit1_5.tba, src/tgbatest/tba_samples_from_spin/explicit1_6.tba, src/tgbatest/tba_samples_from_spin/explicit1_7.tba, src/tgbatest/tba_samples_from_spin/explicit1_8.tba, src/tgbatest/tba_samples_from_spin/explicit1_9.tba, src/tgbatest/tba_samples_from_spin/explicit2_1.tba, src/tgbatest/tba_samples_from_spin/explicit2_2.tba, src/tgbatest/tba_samples_from_spin/explicit2_3.tba, src/tgbatest/tba_samples_from_spin/explicit2_4.tba, src/tgbatest/tba_samples_from_spin/explicit2_5.tba, src/tgbatest/tba_samples_from_spin/explicit2_6.tba, src/tgbatest/tba_samples_from_spin/explicit2_7.tba, src/tgbatest/tba_samples_from_spin/explicit2_8.tba, src/tgbatest/tba_samples_from_spin/explicit2_9.tba: New files * src/tgbatest/tba_samples_from_spin.test : New test. * src/tgbatest/Makefile.am: Add it. 2004-11-17 Alexandre Duret-Lutz * src/tgba/tgba.hh, src/tgbaalgos/dotty.hh, 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. * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/multop.hh, src/ltlast/refformula.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/declenv.hh, src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh, src/ltlparse/public.hh, src/ltlvisit/apcollect.hh, src/ltlvisit/basicreduce.hh, src/ltlvisit/clone.hh, src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh, src/ltlvisit/length.hh, src/ltlvisit/lunabbrev.hh, src/ltlvisit/nenoform.hh: Add Doxygen groups for LTL algorithms and types. * doc/Makefile.am (fast-doc): New target. * src/misc/hashfunc.hh: Include cstddef to define size_t, and guard the file for multiple inclusions. * src/tgba/bdddict.hh, src/tgba/state.hh, src/tgba/statebdd.hh, 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/. 2004-11-16 Alexandre Duret-Lutz * src/tgba/tgbatba.hh (tgba_sba_proxy): New class, with the 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(). * src/tgba/tgbatba.cc (state_tba_proxy::hash): Use wang32_hash. * src/tgba/tgbaproduct.cc (state_product::hash): Likewise. * src/misc/hashfunc.hh (wang32_hash): New file and function, extracted from... * src/evtgba/product.cc (evtgba_product_state::hash): ... here. * src/misc/Makefile.am (misc_HEADERS): Add hashfunc.hh. 2004-11-15 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (main): For non-generalized emptiness check, degeneralize the automaton only if it has too much acceptance conditions. This makes it easier to reproduce runs of randtgba. * src/tgbatest/emptchk.test: Adjust. 2004-11-15 Denis Poitrenaud * src/tgbaalgos/magic.cc: Fix a stupid bug. * src/tgbaalgos/se05.cc: Fix the same bug. * src/tgbatest/Makefile.am: Signify that emptchkr.test pass. 2004-11-15 Alexandre Duret-Lutz * tgbatest/randtgba.cc: Add options -e and -r. * tgbatest/emptchkr.test: New file. * src/tgbatest/Makefile.am (TESTS, XFAIL_TESTS): Add emptchkr.test. * src/tgbaalgos/replayrun.cc (replay_tgba_run): Fix a memory leak if debug==false. * src/tgbaalgos/randomgraph.cc (random_graph): Do declare all the acceptance conditions in the produced automaton, in case they are not actually used. * src/tgbaalgos/replayrun.cc (replay_tgba_run): Write to the supplied stream, not std::cout. 2004-11-15 Denis Poitrenaud * src/tgbaalgos/magic.cc: Add a bit state hashing version. * src/tgbaalgos/se05.cc: Add a bit state hashing version. * src/tgbaalgos/magic.hh: Make them public. * src/tgbatest/ltl2tgba.cc: Add the two new emptiness checks. * src/tgbatest/emptchk.test: Incorporate tests of src/tgbatest/dfs.test. * src/tgbatest/dfs.test: Introduce new characteristic explicit tests. 2004-11-14 Alexandre Duret-Lutz * wrap/python/cgi/ltl2tgba.in: Add options to check the produced automata for emptiness, using the existing algorithms. * wrap/python/spot.i: Declare spot::explicit_magic_search, and spot::explicit_se05_search as allocating their output. 2004-11-12 Alexandre Duret-Lutz * configure.ac: Check for srand48 and drand48. * src/misc/random.cc (srand, drand): Use srand48 and drand48 if available. * src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS) (libtgbaalgos_la_SOURCES): Add them. * src/tgba/tgbaexplicit.hh (tgba_explicit::add_state): Make it public. * src/tgbatest/randtgba.cc: New file. * src/tgbatest/Makefile.am (noinst_PROGRAMS, readsave_SOURCES): Add it. * src/tgbatest/readsave.test: Check a random graph. * misc/random.cc, misc/random.hh: New files. * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them. 2004-11-10 Alexandre Duret-Lutz * src/evtgbaparse/public.hh (evtgba_parse): Fix doxygen comments. * src/tgbaalgos/projrun.hh (project_tgba_run): Likewise. * src/tgbaalgos/emptiness.hh (print_tgba_run): Document it. * src/tgbaalgos/replayrun.hh, src/tgbaalgos/replayrun.cc (replay_tgba_run): Take a `debug' option to decide whether the output should look like that of print_tgba_run() or a complete debug trace. * src/tgbatest/ltl2tgba.cc (main): Call replay_tgba_run() with debug=true. * iface/gspn/ltlgspn.cc (main): Adjust to recent changes to src/tgbaalgos/magic.cc, call explicit_magic_search() instead of building a spot::magic_search. * iface/gspn/udcseltl.test: Adjust to new output of print_tgba_run(). 2004-11-09 Alexandre Duret-Lutz * src/tgbatest/Makefile.am (TESTS): Remove non-existing magic.test and se05.test. * src/tgbatest/ltl2tgba.cc (syntax): Fix old typos and reword some help strings. 2004-11-09 Denis Poitrenaud * src/tgbaalgos/magic.cc: rewrite to externalize the heap and prepare it to a bit state hashing version. * src/tgbaalgos/magic.hh: adapt to the new interface of magic_search and se05_search. * src/tgbaalgos/se05.cc: new file. * src/tgbaalgos/Makefile.am: Add it. * src/tgbatest/ltl2tgba.cc: Add new emptiness check. * src/tgbatest/emptchk.test: more tests. * src/tgbatest/dfs.test: new file. * src/tgbatest/Makefile.am: Add it. 2004-11-09 Alexandre Duret-Lutz * src/tgbaalgos/emptiness.cc (print_tgba_run): Output the labels as formulae rather than bdd sets. 2004-11-08 Alexandre Duret-Lutz * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_path): Rewrite as ... (couvreur99_check_result::accepting_cycle): ... this less complex implementation. (couvreur99_check_result::complete_cycle): Delete. * src/tgbatest/emptchke.test: More explicit examples. * src/tgbaalgos/replayrun.cc (replay_tgba_run): Do not leak the initial state when no valid outgoing transition is found. * src/tgbaparse/tgbaparse.yy: Add `%destructor's so the parser does not leak on errors. * src/tgbatest/ltl2tgba.cc: Free the automata if it could not be fully parsed. * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run): Remove spurious FIXME. 2004-11-05 Alexandre Duret-Lutz * src/evtgbaalgos/save.cc (save_bfs::output_acc_set): Sort acceptance conditions in the output. * src/evtgbatest/readsave.test, src/evtgbatest/product.test: Adjust. * src/tgbaalgos/rundotdec.cc (tgba_run_dotty_decorator::link_decl): Typo. 2004-11-04 Alexandre Duret-Lutz * src/tgbaalgos/neverclaim.cc (never_claim_bfs::process_link): Adjust prototype. * src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::number_of_acceptance_conditions): New method. * src/tgbaalgos/lbtt.cc (lbtt_bfs::lbtt_bfs): Use it. * wrap/python/spot.i: Generate bindings for tgbaalgos/dottydec.hh, tgbaalgos/emptiness.hh, tgbaalgos/gtec/gtec.hh, and tgbaalgos/rundotdec.hh. * src/tgbaalgos/lbtt.cc (lbtt_bfs::process_link): Adjust prototype. 2004-11-03 Alexandre Duret-Lutz * src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh, src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them. * src/tgbaalgos/dotty.hh (dotty_reachable): Take a dotty_decorator as third parameter. * src/tgbaalgos/dotty.cc (dotty_bfs::process_state, dotty_bfs::process_link): Use the decorator. * src/tgbatest/ltl2tgba.cc: Graph the accepting run if the -g option is given. * src/tgbatest/emptchk.test: Exercise -g. * src/tgbaalgos/replayrun.cc (replay_tgba_run): Add missing std::endl. * tgbaalgos/reachiter.hh, tgbaalgos/reachiter.cc (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. 2004-11-02 Alexandre Duret-Lutz * src/ltlvisit/reduce.hh (is_eventual, is_universal): More doc. * src/tgbaalgos/projrun.hh, src/tgbaalgos/projrun.cc: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them. * iface/gspn/ltlgspn.cc (main): Call project_tgba_run if -P. * src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh (print_tgba_run): Take the tgba* argument before the tgba_run* argument (for consistency with replay_tgba_run). * src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc: Adjust calls to print_tgba_run(). * src/ltlast/formula.hh (ltl::formula::~formula): Make it protected. 2004-10-29 Alexandre Duret-Lutz A tgba can now annotate a transition (i.e., the position of a tgba_succ_iterator) with some string. This comes handy to associate that transition to its high-level name. * src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::transition_annotation): New method. * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc (tgba_product::transition_annotation): Implement it. * src/tgba/tgbatba.hh, src/tgba/tgbatba.cc (tgba_tba_proxy::transition_annotation): Likewise. * src/tgbaalgos/replayrun.cc (print_annotation): New function. (replay_tgba_run): Use it. * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh (couvreur99_check::print_stats): New. * src/tgbatest/ltl2tgba.cc: Print emptiness-check statistics. * src/sanity/style.test: Diagnose superfluous constructs such as `if (x) delete x;'. * iface/gspn/gspn.cc, iface/gspn/ssp.cc, src/ltlvisit/basicreduce.cc, src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgbaalgos/magic.cc, src/tgbatest/ltl2tgba.cc: Remove such constructs. * src/tgbatest/ltl2tgba.cc: Replace -e, -E, -m, -M, and -n by -eALGO and -EALGO to ease the addition of new algorithms. * src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust. * src/misc/version.cc: Fix trailing whitespace. * src/sanity/style.test: Diagnose trailing whitespace. * src/tgbatest/ltl2tgba.cc: Fix lines longer than 80 chars. * src/sanity/80columns.test: Use expand to untabify, the previous recipe was incomplete. * src/tgbaalgos/replayrun.cc (replay_tgba_run): Note duplicate states. * src/tgbaalgos/replayrun.cc (replay_tgba_run): Verify the run is accepting. * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_path): Initialize best_end to remove a spurious warning. * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run, couvreur99_check_result::complete_cycle, couvreur99_check_result::accepting_path): Record conditions and acceptance conditions in the accepting run. Simplify the todo BFS stack for accepting_run and complete_cycle. * src/tgbatest/ltl2tgba.cc (main): Do use replay_tgba_run now everything works. * src/tgbaalgos/replayrun.cc (replay_tgba_run): Be more verbose when an outgoing transition is not found. 2004-10-28 Alexandre Duret-Lutz * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc (magic_search): Record the acceptance conditions in the accepting run. * src/tgbaalgos/replayrun.cc (replay_tgba_run): Fix logic. * src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh: New files. Cannot test them because the run returned by the emptiness checks are currently incomplete (they lack the acceptance conditions, and sometimes even the labels in the prefix). * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them. * src/tgbatest/ltl2tgba.cc (main): Prepare to use replay_tgba_run when the emptiness checks are fixed. 2004-10-27 Alexandre Duret-Lutz Introduce an emptiness-check interface, and modify the existing algorithms to conform to it, uniformly. This will unfortunately break third-party code that were using these algorithms. * src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: New files. * src/tgbaalgos/Makefile.am: New files. * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh: Adjust to conform to the new emptiness-check interface. * src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh: Likewise. The classes have been renamed are as following emptiness_check -> couvreur99_check emptiness_check_shy -> couvreur99_check_shy emptiness_check_status -> couvreur99_check_status counter_example -> couvreur99_check_result * src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh, iface/gspn/ssp.cc: Adjust to renaming and new interface. * src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaalgos/tgba2evtgba.hh: New files. * src/evtgbaalgos/Makefile.am (evtgbaalgos_HEADERS, libevtgbaalgos_la_SOURCES): Add them. * src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/ltl2evtgba.test: New files. * src/evtgbatest/Makefile.am (check_PROGRAMS, TESTS): Add them. (ltl2evtgba_SOURCES): New variable. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Do not assert that the true state has only one link when unobs is used. 2004-10-23 Alexandre Duret-Lutz * src/evtgbatest/Makefile.am (CLEANFILES): New variable. 2004-10-22 Alexandre Duret-Lutz Preliminary support for Event-based GBA. * src/evtgba/Makefile.am, src/evtgba/evtgba.cc, src/evtgba/evtgba.hh, src/evtgba/evtgbaiter.hh, src/evtgba/explicit.cc, src/evtgba/explicit.hh, src/evtgba/product.cc, src/evtgba/product.hh, src/evtgba/symbol.cc, src/evtgba/symbol.hh, src/evtgbaalgos/Makefile.am, src/evtgbaalgos/dotty.cc, src/evtgbaalgos/dotty.hh, src/evtgbaalgos/reachiter.cc, src/evtgbaalgos/reachiter.hh, src/evtgbaalgos/save.cc, src/evtgbaalgos/save.hh, src/evtgbaparse/Makefile.am, src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll, src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh, src/evtgbaparse/public.hh, src/evtgbatest/Makefile.am, src/evtgbatest/defs.in, src/evtgbatest/explicit.cc, src/evtgbatest/explicit.test, src/evtgbatest/product.cc, src/evtgbatest/product.test, src/evtgbatest/readsave.cc, src/evtgbatest/readsave.test: New files. * configure.ac: Create the Makefiles in these new subdirectories. * src/Makefile.am: Recurse them. * src/misc/bareword.hh, src/misc/bareword.cc (quote_unless_bare_word): New function. * src/ltlvisit/tostring.cc (to_spin_string_visitor): Move to anonymous namespace. 2004-10-21 Alexandre Duret-Lutz * wrap/python/Makefile.am (_spot_la_SOURCES): Add spot_wrap.h. 2004-10-20 Alexandre Duret-Lutz * src/misc/modgray.hh (loopless_modular_mixed_radix_gray_code::done, loopless_modular_mixed_radix_gray_code::last): Declare as const. * src/misc/bareword.hh, src/misc/bareword.cc: New files. * src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them. * src/misc/modgray.hh, src/misc/modgray.cc: New files. * src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them. * wrap/python/spot.i: Activate directors, and interface modgray.hh. * wrap/python/tests/modgray.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add it. 2004-10-18 Alexandre Duret-Lutz * iface/gspn/gspn.cc, src/ltlvisit/basicreduce.cc, src/ltlvisit/destroy.cc, src/ltlvisit/dotty.cc, src/ltlvisit/dump.cc, src/ltlvisit/length.cc, src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc, src/tgba/tgbabddconcreteproduct.cc, src/tgba/tgbatba.cc, src/tgbaalgos/dotty.cc, src/tgbaalgos/dupexp.cc, src/tgbaalgos/lbtt.cc, src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/save.cc, src/tgbaalgos/stats.cc, src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh: Declare private classes and helper function in anonymous namespaces. * HACKING, src/sanity/style.test: Document and check this. Also check for trailing { after namespace or class. * src/ltlast/predecl.hh, src/ltlast/visitor.hh, src/tgba/tgbareduc.hh: Fix trailing {. 2004-10-15 Alexandre Duret-Lutz * src/tgbaalgos/gtec/ce.cc: Reinstall change from 2004-09-21. Back out all Thomas's changes on emptiness checks since 2004-08-23. Some of these will need to be reintegrated more slowly and cleanly. * src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh, src/tgbatest/Makefile.am, src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc: Revert. * src/tgbaalgos/colordfs.cc, src/tgbaalgos/colordfs.hh, src/tgbaalgos/minimalce.cc, src/tgbaalgos/minimalce.hh, src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/nesteddfsgen.cc, src/tgbaalgos/nesteddfsgen.hh, src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh: Delete. 2004-10-14 Alexandre Duret-Lutz * src/ltltest/reduc.test: Do source ./defs. Revert mistaken change from 2004-09-13. * src/tgbatest/explicit.test: Typo. 2004-10-13 Alexandre Duret-Lutz The computation of the counter example fails the valgrind tests and is wrong into two ways: the search stack is generally not a path, and does not run until the end of the STL container. Remove it. * src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh (tarjan_on_fly): Do not inherit from the emptiness_search class, because the check method will no longer return a counter example. (tarjan_on_fly::check): Return only a boolean. (tarjan_on_fly::build_counter): Delete. * src/tgbatest/ltl2tgba.cc: Adjust. * src/tgba/tgbaexplicit.cc (tgba_explicit_succ_iterator::current_state, tgba_explicit_succ_iterator::current_condition, tgba_explicit_succ_iterator::current_accepting_conditions): Assert the iteration is not finished. 2004-10-12 Alexandre Duret-Lutz * wrap/python/tests/run.in: Typo. From Akim Demaille. 2004-10-11 Alexandre Duret-Lutz * configure.ac: Empty CFLAGS and CXXFLAGS. * m4/debug.m4: Update CXXFLAGS too. 2004-10-08 Alexandre Duret-Lutz * doc/Doxyfile.in: Upgrade to Doxygen 1.3.9. 2004-09-27 Alexandre Duret-Lutz * src/sanity/style.test: Suggest using "x->y", not "(*x).y". * src/tgbaalgos/tarjan_on_fly.cc: Fix. 2004-09-23 Alexandre Duret-Lutz * src/sanity/style.test: Suggest ++i over i++ when it does not matter, for consistency. * src/tgbaalgos/tarjan_on_fly.cc, iface/gspn/ssp.cc, src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/minimalce.cc, src/tgba/tgbareduc.cc: Adjust. * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): New unobs argument. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Handle unobs. * src/tgbatest/ltl2tgba.cc (syntax, main): New -U option. 2004-09-21 Alexandre Duret-Lutz * src/tgbaalgos/colordfs.hh, src/tgbaalgos/minimalce.cc, src/tgbaalgos/minimalce.hh, src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/tarjan_on_fly.hh, src/tgbatest/ltl2tgba.cc: Rename emptyness_search to emptiness_search. * src/sanity/style.test: Warn about places where size() is used instead of empty(). * src/misc/bddalloc.cc (bdd_allocator::extend): Use empty() rather than size() when checking emptiness of lists. * src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/minimalce.cc, src/ltlvisit/basicreduce.cc, src/ltlvisit/reduce.cc, src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/misc/minato.cc: Likewise. * src/ltlast/multop.cc (multop::instance): Call ->size() only once. 2004-09-20 Alexandre Duret-Lutz Update to SWIG 1.3.22. * wrap/python/libpy.c: Delete. * wrap/python/swigpy.i: New file. * wrap/python/Makefile.am (swigpy_wrap.c): Build this from swigpy.i and use it instead of libpy.c. * INSTALL, lbtt/INSTALL: New upstream version. 2004-09-14 Thomas Martinez * src/tgbatest/emptchk.test src/tgbaalgos/tarjan_on_fly.hh, src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/minimalce.hh, src/tgbaalgos/minimalce.cc: To correct a bug. * src/ltltest/reduc.test (FICH): bad file name. 2004-09-13 Thomas Martinez * src/tgbaalgos/nesteddfsgen.hh src/tgbaalgos/nesteddfsgen.cc: New algorithm for emptiness check. * src/tgbatest/spotlbtt.test, src/tgbatest/reductgba.cc, src/tgbatest/ltl2tgba.cc: Add option for reduction of TGBA. * src/tgbatest/emptchk.test, src/tgbaalgos/Makefile.am, src/tgbaalgos/tarjan_on_fly.hh, src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/minimalce.hh, src/tgbaalgos/minimalce.cc, src/tgbaalgos/colordfs.hh, src/tgbaalgos/colordfs.cc: Remove some bugs. src/tgbaalgos/gtec/ce.cc: Modification of construction of counter example. * src/tgbaalgos/reductgba_sim.hh src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim_del.cc, src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc: Modification for delayed simulation. 2004-08-23 Thomas Martinez * src/tgbaalgos/tarjan_on_fly.hh, src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/minimalce.hh, src/tgbaalgos/minimalce.cc, src/tgbaalgos/colordfs.hh, src/tgbaalgos/colordfs.cc: four new algorithms for emptiness check. * src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/ce.cc: Adapt the counter exemple for the ce object in minimalce.hh. * src/tgbatest/ltl2tgba.cc, src/tgbatest/emptchk.test, src/tgbaalgos/Makefile.am: Add files for emptiness-check. 2004-08-23 Thomas Martinez * src/tgbaalgos/reductgba_sim_del.cc: Restrict to degeneralize automata. * src/tgba/tgbareduc.hh: src/tgba/tgbareduc.cc: Merge transition for scc reduce. 2004-08-13 Alexandre Duret-Lutz * configure.ac, NEWS: Bump version to 0.0y. * configure.ac, NEWS: Bump version to 0.0x. 2004-08-12 Alexandre Duret-Lutz * doc/Doxyfile.in (GENERATE_TAGFILE): Build spot.tag. * doc/Makefile.am (dist_pkgdata_DATA): Add spot.tag. * src/tgbatest/ltl2tgba.cc (syntax): Typo. * doc/Doxyfile.in (STRIP_FROM_PATH): Strip @srcdir@ so its does not appear when listing mainpage.dox. 2004-08-11 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh: Typos in Doxygen comments. 2004-08-10 Alexandre Duret-Lutz * src/ltlvisit/apcollect.hh: Fix include guard. Report from Denis. * src/sanity/includes.test: Include files twice to check include guards. * src/tgbatest/ltl2tgba.cc (main): Fix another gcc warning in case assert() is disabled. * src/Makefile.am (nodist_EXTRA_libspot_la_SOURCES): New variable, to force C++ linking. * iface/gspn/ltlgspn.cc: Fix a gcc warning in case assert() is disabled. 2004-08-09 Alexandre Duret-Lutz * src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh: New files, based on code from . * src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES, ltlvisit_HEADERS): Add them. * iface/gspn/common.cc, iface/gspn/common.hh, src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh, src/ltlparse/fmterror.cc, src/ltlparse/public.hh, src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh, src/ltlvisit/dump.cc, src/ltlvisit/dump.hh, src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh, src/misc/escape.cc, src/misc/escape.hh, src/tgba/bdddict.cc, src/tgba/bdddict.hh, src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh, src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh, src/tgbaalgos/save.cc, src/tgbaalgos/save.hh, src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh, src/tgbaparse/fmterror.cc, src/tgbaparse/public.hh: Include in headers, and prefer in the body whenever possible. * src/sanity/style.test, HACKING: Check and document this. * src/ltlast/allnodes.hh, src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/multop.hh, src/ltlast/predecl.hh, src/ltlast/refformula.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh: Use \file to introduce each file. * doc/Doxyfile.in (STRIP_FROM_INC_PATH): Define, so that the `#include' references are correct. * README: Update. * m4/gccoptim.m4: Compute optimization flags for CXX too. * m4/ndebug.m4: Update CPPFLAGS, not CFLAGS. * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Document all parameters. * src/tgbaalgos/ltl2tgba_lacim.hh (ltl_to_tgba_lacim): Likewise. 2004-08-07 Alexandre Duret-Lutz * configure.ac: Call AC_PROG_CC and AM_PROG_CC_C_O. * wrap/python/Makefile.am (_buddy_la_LDFLAGS): Move libspotswigpy.la ... (_buddy_la_LIBADD): ... here. 2004-08-02 Alexandre Duret-Lutz * lbtt/: Merge lbtt 1.1.2. 2004-07-30 Alexandre Duret-Lutz * lbtt/: Merge lbtt 1.1.1. 2004-07-26 Alexandre Duret-Lutz * doc/Doxyfile.in: Update for Doxygen 1.3.8. 2004-07-23 Alexandre Duret-Lutz * configure.ac: Call AC_LIBTOOL_WIN32_DLL * src/Makefile.am (libspot_la_LDFLAGS): Add -no-undefined. 2004-07-22 Alexandre Duret-Lutz * src/tgbatest/explicit.test: Do not use `-i', it's not needed and it is wrong to put it after `-e'. Caught by Denis too. * src/ltltest/reduc.test: Use `test a = b' not `test a == b'. Reported by (failure on Cygwin). 2004-07-20 Alexandre Duret-Lutz * src/tgbatest/defs.in (VALGRIND): Specify --tool=memcheck for compatibility with valgrind 2.1.x. * src/ltltest/defs.in (VALGRIND): Likewise. 2004-07-16 Alexandre Duret-Lutz * m4/gccwarn.m4: Do not check nor use -Wstrict-prototypes. g++-3.4 complains it makes no sense in C++. * iface/gspn/ssp.cc: Typos. * iface/gspn/gspn.cc (tgba_succ_iterator_gspn::tgba_succ_iterator_gspn): Set size_ to 1 when stuttering is needed, so that done() does not return true immediately. 2004-07-12 Alexandre Duret-Lutz * src/tgbaalgos/gtec/gtec.hh: Typos in comments. 2004-07-09 Alexandre Duret-Lutz * src/tgba/state.hh (state_ptr_equal, state_ptr_hash): Fix Doxygen example. * src/tgbaalgos/reductgba_sim.hh (parity_game_graph_delayed, reduc_tgba_sim): Fix warnings about Doxygen comment. * src/ltlvisit/reduce.hh (reduce): Likewise. * doc/footer.html: New file, link to RefDocComments on the wiki. * doc/Doxyfile.in (HTML_FOOTER): Use footer.html. * doc/Makefile.am (EXTRA_DIST): Add footer.html. * THANKS: Fill in. * src/tgbatest/ltl2baw.pl: Do not use -T anymore. Fix comments. 2004-07-08 Alexandre Duret-Lutz lbtt 1.1.0 supports TGBAs, use that and remove old workarounds. * src/tgbaalgos/lbtt.cc (state_acc_pair, state_acc_pair_equal, state_acc_pair_hash, acp_seen_map, todo_set, seen_map, fill_todo lbtt_reachable): Remove. (nonacceptant_lbtt_bfs): Rename as ... (lbtt_bfs): ... this, and adjust to output acceptance conditions on transitions. (nonacceptant_lbtt_reachable): Rename as ... (lbtt_reachable): ... this. * src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): Delete. * src/tgbatest/ltl2tgba.cc: Suppress option "-T". Patch from Heikki Tauriainen . * src/tgbaalgos/gtec/ce.cc (counter_example::counter_example): Do not parenthesize the type after the new operator (g++ 3.4 complains). * src/tgbaalgos/dupexp.cc (dupexp_iter::process_state, dupexp_iter::declare_state): Use this->automata_ instead of automata_. Local protected member automata_ inherited from template base class must be prefixed or g++ 3.4 will not look it up (conforming to §14.6.2.3). 2004-07-07 Alexandre Duret-Lutz * lbtt/: Merge lbtt 1.1.0. * src/tgbatest/spotlbtt.test: Adjust config file syntax to please lbtt 1.1.0. * src/tgbaalgos/gtec/gtec.hh (emptiness_check_shy::find_state): Add comments. * iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Likewise. Soheib and I had a hard time figuring why we did this... 2004-07-02 Thomas Martinez * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim_del.cc: Remove some comments. * src/tgbatest/ltl2tgba.cc, src/tgbatest/reductgba.cc: Adjust ... * src/tgbatest/spotlbtt.test: More test (delayed simulation) 2004-06-29 Alexandre Duret-Lutz * configure.ac, NEWS: Bump version to 0.0w. * configure.ac, NEWS: Bump version to 0.0v. 2004-06-28 Thomas Martinez * src/tgbatest/reduccmp.test: Bug. * src/tgbatest/reductgba.test: More Test. * src/tgbatest/ltl2tgba.cc: Adjust ... * src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc: try to optimize. * src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc: Scc reduction and we remove some acceptance condition in scc which are not accepting. * src/ltlvisit/syntimpl.cc : Some case wasn't detect. * src/ltlvisit/basicreduce.cc: Case FGa || FGb = F(Ga | Gb) added. * src/ltltest/syntimpl.test: More Test. * src/ltltest/syntimpl.cc: Put the formula in negative normal form. 2004-06-28 Alexandre Duret-Lutz * buddy/: Merge buddy-2-3. 2004-06-25 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (main): Degeneralize before the simulations. 2004-06-23 Alexandre Duret-Lutz * src/ltlvisit/tostring.cc (is_bare_word): New function. (to_string_visitor::visitor(const atomic_prop*)): Use is_bare_word to better check which atomic proposition need to be quoted. * src/ltlparse/ltlscan.ll: Do not allow identifiers starting with F_ or G_. * src/ltltest/equals.test, src/ltltest/tostring.test: More tests. * src/tgba/tgbatba.cc (tgba_tba_proxy::format_state): Use bdd_format_accset to print the acceptance condition part of the state. That produces more readable output. * wrap/python/cgi/ltl2tgba.in: Add "Formula Simplications" options. * wrap/python/spot.i: Wrap src/ltlvisit/reduce.hh. * src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh: New files, extracted from ... * src/ltlvisit/lunabbrev.cc: ... this one, which now work as documented again. * src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc: Adjust to call simplify_f_g() in addition to unabbreviate_logic(). * src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES): Add simpfg.cc and simpfg.hh. * src/ltlvisit/reducform.hh, src/ltlvisit/reducform.cc: Rename to ... * src/ltlvisit/reduce.hh, src/ltlvisit/reduce.cc: ... this, to match the function name. * ltltest/equals.cc, ltltest/reduc.cc, ltlvisit/Makefile.am, tgbatest/ltl2tgba.cc, tgbatest/reductgba.cc: Adjust filenames. * src/ltlvisit/basicreduce.cc (basic_reduce_visitor::visit(binop*)): Factorize. * src/ltlvisit/basicreduce.hh: New file, extracted from ... * src/ltlvisit/reducform.hh: ... here. * src/ltlvisit/basereduc.cc: Rename as ... * src/ltlvisit/basicreduce.cc: ... this, to match the function name. * src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES): Adjust filenames. * src/ltlvisit/reducform.cc: Adjust includes. * src/ltlvisit/lunabbrev.hh: Revert superfluous change from 2004-05-10. 2004-06-22 Thomas Martinez * src/ltlvisit/reducform.cc, src/tgba/tgbareduc.cc, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh src/tgbaalgos/reductgba_sim_del.cc, src/tgbatest/reduccmp.test, src/tgbatest/reductgba.cc: 80 columns and style. 2004-06-22 Alexandre Duret-Lutz * src/sanity/style.test: Typo. 2004-06-22 Thomas Martinez * src/tgbatest/ltl2tgba.cc, src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc: bug in delayed simulation. * src/tgbatest/reduccmp.test, src/tgbatest/reductgba.test, src/tgba/tgbareduc.cc: bug in scc reduction. 2004-06-21 Thomas Martinez * src/tgbatest/reductgba.test, src/tgba/tgbareduc.cc: There is bug in reduction with scc. * src/tgbatest/reduccmp.test: More test. 2004-06-17 Thomas Martinez * src/tgbatest/reductgba.test: Wrong test are removed. 2004-06-17 Thomas Martinez * src/tgbatest/spotlbtt.test: We don't check the post-reduction 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/reduc.cc: Thinko * src/ltltest/equals.cc: Reduction compare 2004-06-17 Alexandre Duret-Lutz * iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Free s. This fixes a memory leak observed by Soheib Baarir. 2004-06-16 Thomas Martinez * src/tgbatest/reductgba.cc, src/tgbatest/reductgba.test: Test for reduction of tgba. 2004-06-15 Thomas Martinez * src/tgbatest/ltl2tgba.cc: Add some option for the reduction of 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. 2004-06-02 Alexandre Duret-Lutz * iface/gspn/common.cc, iface/gspn/common.hh: Remove the class gspn_environment, and move it to ... * src/ltlenv/declenv.cc, src/ltlenv/declenv.hh: .. this new file as class declarative_environment. * src/ltlenv/Makefile.am (ltlenv_HEADERS): Add declenv.hh. (libltlenv_la_SOURCES): Add declenv.cc. * iface/gspn/dottygspn.cc, iface/gspn/dottyssp.cc, iface/gspn/gspn.cc, iface/gspn/gspn.hh, iface/gspn/ltlgspn.cc, iface/gspn/ssp.cc, iface/gspn/ssp.hh: Adjust references to declarative_environment. * HACKING, src/sanity/style.test: NULL is not portable, prohibit it. * iface/gspn/ssp.cc, src/ltltest/reduc.cc, src/ltltest/syntimpl.cc, src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc, src/ltlvisit/syntimpl.cc: Use 0 instead of NULL. 2004-06-01 Alexandre Duret-Lutz * src/ltltest/inf.cc, src/ltltest/inf.test: Rename as ... * 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. 2004-05-30 Alexandre Duret-Lutz * src/ltlvisit/forminf.cc (form_eventual_universal_visitor, 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. 2004-05-26 Alexandre Duret-Lutz * src/ltlvisit/reducform.cc (reduce_form_visitor::visit(constant)): Simplify. * src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc: Use dynamic_cast instead of node_type_form_visitor, this is usually smaller. * src/ltlvisit/reducform.hh, src/ltlvisit/forminf.cc (node_type_form_visitor): Delete. * src/sanity/style.test: Two more checks. 2004-05-25 Alexandre Duret-Lutz * src/ltlvisit/formlength.cc: Rename as ... * src/ltlvisit/length.cc: ... this. * src/ltlvisit/length.hh: New file, extracted from ... * src/ltlvisit/reducform.hh: ... here. * src/ltlvisit/Makefile.am (ltlvisit_HEADERS): Add length.hh. (libltlvisit_la_SOURCES): Rename formlength.cc as length.cc. * src/ltltest/reduc.cc: Include length.hh. * src/ltlvisit/formlength.cc (length_form_vistor): Rename as .. (length_visitor): ... this. (form_length): Rename as ... (length): ... this. * src/ltlvisit/reducform.hh (form_length): Rename as ... (length): ... this. * src/ltltest/reduc.cc: Adjust. * src/ltlvisit/basereduc.cc, src/ltlvisit/formlength.cc: Remove useless includes. * AUTHORS: Update. * src/ltlvisit/reducform.hh: Update Doxygen comments for previous change. * src/ltlvisit/reducform.hh (option): Rename as ... (reduce_options): ... this, and use it as a bit field so option can be combined easily. (reduce): Adjust argument. (reduce_form): Remove, not needed anymore. * src/ltlvisit/reducform.cc, src/ltltest/reduc.cc, src/tgbatest/ltl2tgba.cc: Adjust. * src/sanity/style.test: Catch {.*{ and }.*}. * src/sanity/80columns.test: Untabify files. * iface/gspn/ltlgspn.cc, src/ltlvisit/basereduc.cc: Fix long lines. * src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc, src/ltlvisit/forminf.cc: Remove superfluous spot::ltl:: prefixes. * wrap/python/cgi/ltl2tgba.in: Typos. 2004-05-24 Alexandre Duret-Lutz * src/sanity/style.test: Catch `;'-not-followed-by-space. * src/ltlvisit/reducform.cc, src/ltlvisit/forminf.cc: Fix style. * src/ltlvisit/reducform.hh: Fix some Doxygen comments. * src/tgbatest/ltl2tgba.cc (syntax): Keep options sorted. * src/sanity/Makefile.am (EXTRA_DIST): Distribute 80columns.test and style.test. * src/ltltest/Makefile.am (EXTRA_DIST): Distribute formulae.txt. * src/ltltest/formulae.txt: New file (2200 LTL formulea generated by Wring). * src/ltltest/formules.ltl: Delete. * src/reduc.test: Read formulae.txt. 2004-05-24 Soheib Baarir * iface/gspn/ssp.hh (gspn_ssp_interface::gspn_ssp_interface): Add the `inclusion' flag. * iface/gspn/ssp.cc (gspn_ssp_interface::gspn_ssp_interface): Call inclusion_version when inclusion is set. * iface/gspn/ltlgspn.cc (main) [SSP]: Turn on inclusion for -e3, -e4, and -e5. 2004-05-21 Alexandre Duret-Lutz * iface/gspn/gspn.cc (tgba_gspn_private_): Define alive_prop, and dead_prop from the dead argument passed to the constructor. (tgba_succ_iterator_gspn): Stutter on dead transitions. (tgba_gspn::tgba_gspn): Hand dead to tgba_gspn_private_. (gspn_interface::gspn_interface): Hand dead to tgba_gspn. * iface/gspn/gspn.hh (gspn_interface::gspn_interface): Take a dead argument. * iface/gspn/ltlgspn.cc [!SSP]: Add a option -d to specify the dead property. * iface/gspn/udcseltl.test: Try option -d. * src/sanity/style.test: Check the iface/ tree too. * iface/gspn/gspn.cc, iface/gspn/ssp.cc: Fix style. * src/sanity/80columns.test: Check the iface/ tree too. * iface/gspn/dcswaveltl.test, iface/gspn/dcswavefm.test, iface/gspn/dcswaveeltl.test, iface/gspn/udcsltl.test, iface/gspn/udcseltl.test, iface/gspn/udcsfm.test, iface/gspn/udcsefm.test: Wrap to fit 80 columns. 2004-05-18 Alexandre Duret-Lutz * doc/Makefile.am (EXTRA_DIST, spot.html): Built the html documentation in $(srcdir) since it is distributed. * doc/Doxyfile.in (HTML_OUTPUT): Likewise. Upgrade to Doxygen 1.3.7. 2004-05-17 Thomas Martinez * src/ltlvisit/basereduc.cc, src/ltltest/inf.cc (main): Style. * src/ltlvisit/basereduc.cc (spot): 80 columns. * src/ltlvisit/reducform.cc (spot), src/ltltest/inf.cc, src/ltltest/reduc.cc (main), src/ltlvisit/reducform.hh, src/tgbatest/ltl2tgba.cc (main): More option. * src/ltltest/inf.test: More test. 2004-05-17 Alexandre Duret-Lutz * wrap/python/buddy.i: Define typemap for input_buf and use it for fdd_extdomain. Define const_int_ptr and use it for fdd_vars. * src/misc/bddalloc.cc (bdd_allocator::varnum): Suppress. (bdd_allocator::bdd_allocator): Adjust. (bdd_allocator::extvarnum): Always call bdd_varnum(), so that it doesn't matter if the number of variable has been augmented externally. * src/misc/bddalloc.hh (bdd_allocator::varnum): Suppress. * src/ltlvisit/formlength.cc: Fix style to please sanity checks. * src/ltlvisit/lunabbrev.cc: Fix style to please sanity checks. * src/tgbaalgos/neverclaim.cc: Fix them. * sanity/style.test: Diagnose semicolons with leading spaces. * src/ltlvisit/forminf.cc: Fix style to please sanity checks. Also avoid node_type_form_visitor where a dynamic_cast is done. 2004-05-14 Alexandre Duret-Lutz * wrap/python/buddy.i: Preliminary bindings for FDD and BVEC. * ltltest/inf.cc, ltltest/reduc.cc, ltlvisit/reducform.cc: Fix style. * sanity/style.test: More tests. * src/tgbatest/ltl2tgba.cc (main): Fix style. * HACKING: Mention `else if'. * src/tgbaalgos/neverclaim.cc (never_claim_bfs): Do not output space before colon, and do not output the top-level formula using Spin's syntax. 2004-05-14 Thomas Martinez * src/tgbatest/ltl2tgba.cc (main): Thinko. * src/ltlvisit/basereduc.cc (spot): Correct some mistakes. * src/ltlvisit/lunabbrev.cc (spot): Nothing change. * src/tgbatest/ltl2tgba.cc (main): More option to reduce formula. * src/tgbatest/spotlbtt.test: One more test. 2004-05-14 Alexandre Duret-Lutz * src/ltlvisit/tostring.cc (to_spin_string_visitor, to_string_visitor): Do not parenthesize the top-level formula. * tgbatest/explicit.test, tgbatest/explpro2.test, tgbatest/explpro3.test, tgbatest/explprod.test, tgbatest/readsave.test, tgbatest/tgbaread.test, tgbatest/tripprod.test: Adjust expected output. * sanity/style.test: Fix regexes to catch an error seen in tostring.cc. * src/tgbaalgos/gtec/gtec.cc (emptiness_check::remove_component): Do not try to erase state that are not found in H. Report from Soheib Baarir. * src/ltltest/reduc.test: Use ./defs and clean result.data. * src/ltltest/Makefile.am (CLEANFILES): Clean result.data. 2004-05-13 Thomas Martinez * src/ltlvisit/Makefile.am: Copyright 2004. * 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. 2004-05-13 Alexandre Duret-Lutz * src/ltltest/reduc.test: Typo. * src/ltlparse/ltlparse.yy (OP_POST_NEG, OP_POST_POS): New tokens. (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". 2004-05-11 Alexandre Duret-Lutz * src/ltltest/Makefile.am (TESTS): Run inf.test and reduc.test last. * src/ltltest/reduc.test: POSIXify. 2004-05-10 Alexandre Duret-Lutz * src/sanity/style.test: New file. * 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. * src/ltltest/inf.cc, src/ltltest/inf.test, src/ltltest/reduc.test, src/ltlvisit/formlength.cc, src/ltlvisit/reducform.cc, src/ltlvisit/reducform.hh: Fix copyright year, these files were created in 2004. * src/sanity/80columns.test: New file. * 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/ltltest/reduc.cc, 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. 2004-05-10 Thomas MARTINEZ * src/tgbatest/ltl2tgba.cc (main): Add a option for reduce the formula. * src/ltltest/formules.ltl: A pattern of 2000 formulas. * 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. 2004-05-10 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Refine fair_loop_approximation when branching postponement is not used. Cache formula translations, and canonize formulae before doing 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. * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument 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. 2004-05-07 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument 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. 2004-05-04 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.cc: Add a superfluous return to pacify some GCC version. Report from Denis Poitrenaud. * wrap/python/cgi/ltl2tgba.in: Fix output HTML. 2004-05-03 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Clone and then free all formulae entered into canonical_succ, to avoid errors when a formula is entered into canonical_succ but not into formulae_seen. * src/tgbatest/ltl2tgba.test: Add a new test, and check with -f. Report from Thomas Martinez. 2004-04-23 Alexandre Duret-Lutz * configure.ac, NEWS: Bump version to 0.0u. * configure.ac, NEWS: Bump version to 0.0t. * HACKING: Update tools requirements. * src/sanity/Makefile.am (EXTRA_DIST): Distribute includes.test. * src/sanity/Makefile.am, src/sanity/includes.test: New files. * src/Makefile.am (SUBDIRS): Add sanity. * configure.ac: Output src/sanity/Makefile.in. * src/tgbatest/Makefile.am (check_PROGRAMS): Move ltl2tgba ... (noinst_PROGRAMS): ... here. * iface/gspn/Makefile.am (check_PROGRAMS): Rename as ... (noinst_PROGRAMS): ... this. 2004-04-22 Alexandre Duret-Lutz * src/tgbatest/explicit.test: Reorder bdd variables in output. Report from Denis Poitrenaud. * wrap/python/cgi/ltl2tgba.in: Print degeneralized statistics when show_never_claim. Change the title to LTL-to-TGBA. Suggested by Denis Poitrenaud. 2004-04-21 Alexandre Duret-Lutz * wrap/python/cgi/ltl2tgba.in (print_footer): Make ltl2tgba.py's version a separate variable. * wrap/python/cgi/ltl2tgba.in: Pass the formula to never_claim_reachable, and cgi.escape its output. Lighten the color a bit. * src/tgbaalgos/gtec/ce.hh, src/misc/freelist.hh, src/tgba/bddprint.hh: Fix Doxygen comments. * src/tgbaalgos/neverclaim.hh (never_claim_reachable): Document arguments. * src/tgbaalgos/neverclaim.cc (never_claim_bfs::state_is_accepting): New method. (never_claim_bfs::get_state_label, never_claim_bfs::process_state): Use it. * wrap/python/cgi/ltl2tgba.in: Use darker color and introduce the new variable dot_bgcolor. * wrap/python/cgi/ltl2tgba.in (add_options): Revamp options output using this new function. * wrap/python/spot.i: Process tgbaalgos/neverclaim.hh. * wrap/python/cgi/ltl2tgba.in: Display the never claim on demand. 2004-04-21 Denis Poitrenaud * src/ltlvisit/tostring.hh (to_spin_string): New function. 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. 2004-04-20 Alexandre Duret-Lutz * src/ltltest/defs.in, src/tgbatest/defs.in: Correctly set exitcode when valgrind is not used. Reported by Denis Poitrenaud. * src/tgba/tgba.hh (tgba::succ_iter): Doco. * src/tgba/tgbatba.hh (tgba_tba_proxy::state_is_accepting): Document it. Reported by Denis Poitrenaud. 2004-04-17 Alexandre Duret-Lutz * iface/gspn/ltlgspn.cc (main) [SSP]: Use the standard counter-example computation for -e5 too. * iface/gspn/ltlgspn.cc (main) [!SSP]: Do not accept -e3, -e4, or -e5. (main) [SSP]: Use the standard counter-example computation for -e and -e1. 2004-04-15 Soheib Baarir Alexandre Duret-Lutz Rename EESRG as SSP. * iface/gspn/eesrg.cc, iface/gspn/eesrg.hh, iface/gspn/dottyeesrg.cc: Rename as ... * iface/gspn/ssp.cc, iface/gspn/ssp.hh, iface/gspn/dottyssp.cc: ... these. Adjust all classes and function names. * iface/gspn/ltlgspn.cc, iface/gspn/Makefile.am: Adjust all classes filenames and function names. * m4/gspnlib.m4: Define WITH_GSPN_SSP and LIBGSPNSSP_LDFLAGS. * src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map::find): Rewrite. (numbered_state_heap_hash_map::index): New functions. (numbered_state_heap_hash_map::filter): Delete. * src/tgbaalgos/gtec/nsheap.hh (numbered_state_heap_hash_map::index): New functions. (numbered_state_heap_hash_map::filter): Delete. * iface/gspn/eesrg.cc (numbered_state_heap_eesrg_semi::find, numbered_state_heap_eesrg_semi::index): Rewrite. (numbered_state_heap_eesrg_semi::filter): Remove. * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/ce.cc: Adjust to use find() and index() instead of filter().. * iface/gspn/eesrg.cc (connected_component_eesrg::has_state): Free filtered states. (emptiness_check_shy_eesrg): New class. (emptiness_check_eesrg_shy): New function. * iface/gspn/eesrg.hh (emptiness_check_eesrg_shy): New function. * iface/gspn/ltlgspn.cc (main) [EESRG]: Handle -e3, -e4, and -e5. * * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc (emptiness_check_shy::check): Move arc, num, succ_queue, and todo as attributes. (emptiness_check_shy::find_state): New virtual function. 2004-04-14 Soheib Baarir Alexandre Duret-Lutz * iface/gspn/ltlgspn.cc (connected_component_eesrg, connected_component_eesrg_factory, numbered_state_heap_eesrg_semi, numbered_state_heap_eesrg_const_iterator, numbered_state_heap_eesrg_factory_semi): New classes. (emptiness_check_eesrg_semi, emptiness_check_eesrg_shy_semi, counter_example_eesrg): New functions. * iface/gspn/eesrg.hh (emptiness_check_eesrg_semi, emptiness_check_eesrg_shy_semi, counter_example_eesrg): New functions. * iface/gspn/ltlgspn.cc [EESRG]: Adjust to call these new functions. 2004-04-14 Soheib Baarir * iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg, state_gspn_eesrg): Compute the array of all successors of the right state beforehand, pass it to Greatspn (left automata) at once, let it compute the resulting synchronized arcs, and iterate on that result. 2004-04-14 Alexandre Duret-Lutz * src/tgbaalgos/gtec/nsheap.hh (numbered_state_heap_factory, numbered_state_heap_hash_map_factory): New class. * src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map_factory): Implement it. * src/tgbaalgos/gtec/gtec.hh (emptiness_check::emptiness_check, emptiness_check_shy::emptiness_check_shy): Take a numbered_state_heap_factory argument. * tgbaalgos/gtec/status.hh (emptiness_check_status::emptiness_check_status): Likewise. (emptiness_check_status::h): Make it a numbered_state_heap*. * src/tgbaalgos/gtec/ce.cc, tgbaalgos/gtec/gtec.cc, tgbaalgos/gtec/status.cc: Adjust uses of ecs_->h. * src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc: Delete and split into ... * src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh, src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh: ... these new files. * src/tgbaalgos/gtec/Makefile.am: New file. * src/tgbaalgos/Makefile.am (SUBDIRS, libtgbaalgos_la_LIBADD): Recurse into gtec and link gtec/libgtec.la. (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Remove emptinesscheck.hh and emptinesscheck.cc. * configure.ac: Output src/tgbalagos/gtec/Makefile. * iface/gspn/ltlgspn.cc, src/tgbatest/ltl2tgba.cc: Update includes. * README: Update tree description. 2004-04-13 Alexandre Duret-Lutz * src/tgbaalgos/emptinesscheck.hh (numbered_state_heap_const_iterator, numbered_state_heap, numbered_state_heap_hash_map): New classes. * src/tgbaalgos/emptinesscheck.cc (numbered_state_heap_hash_map_const_iterator): New class. (numbered_state_heap_hash_map): Implement it. * src/tgbaalgos/emptinesscheck.hh (explicit_connected_component_factory, connected_component_hash_set_factory): New classes. (counter_example::counter_example): Take an explicit_connected_component_factory factory argument. * src/tgbaalgos/emptinesscheck.cc: Adjust. * src/tgbaalgos/emptinesscheck.hh (explicit_connected_component): New class. (counter_example::connected_component_set): Rename as ... (connected_component_hash_set): ... this, and inherit from explicit_connected_component. (counter_example::accepting_path, counter_example::complete_cycle): Take an explicit_connected_component argument instead of a connected_component_set. * src/tgbaalgos/emptinesscheck.cc: Adjust. * src/tgbaalgos/emptinesscheck.hh (counter_example::connected_component_set::has_state): Return a const state* and behave like h_filt. * src/tgbaalgos/emptinesscheck.cc: Adjust. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::check2): Move into ... (emptiness_check_shy): This new subclass of emptiness_check. * src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc: Adjust. * src/tgba/bdddict.hh (bdd_dict::annon_free_list): Hide from Swig. * src/tgbaalgo/semptinesscheck.hh (counter_example): New class, extracted from ... (emptiness_check): ... here. * src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc: Adjust. * wrap/python/Makefile.am ($(srcdir)/spot_wrap.cxx) ($(srcdir)/buddy_wrap.cxx): Use -noruntime instead of -c. * src/tgbaalgo/semptinesscheck.hh (emptiness_check_status): New class, extracted from ... (emptiness_check): ... here. * src/tgbaalgos/emptinesscheck.cc: Adjust. * src/tgbaalgo/semptinesscheck.hh (scc_stack): New class, extracted from ... (emptiness_check): ... here. (emptiness_check::root): Redefined as a scc_stack object. * src/tgbaalgos/emptinesscheck.cc: Adjust. 2004-04-05 Alexandre Duret-Lutz * src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle): Do not visit a state more than once. Report from Soheib Baarir. 2004-03-25 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict): Reuse Acc and Var variables from a shared bdd_dict. Register Next variables as anonymous variables. (translate_dict::translate_dict, translate_dict::~translate_dict, translate_dict::register_proposition, translate_dict::register_a_variable, translate_dict::register_next_variable, translate_dict::dump, translate_dict::var_to_formula, ltl_to_tgba_fm): Adjust. (translate_dict::dict): New attribute. (translate_dict::a_map, translate_dict::a_formula_map, translate_dict::var_map, translate_dict::var_formula_map): Delete. * src/misc/freelist.cc (free_list::remove): Work around invalidated iterators. * tgba/bdddict.cc (unregister_variable): New methods, extracted from ... (bdd_dict::unregister_all_my_variables): ... here. * tgba/bdddict.hh (unregister_variable): Declare them. 2004-03-23 Alexandre DURET-LUTZ * src/misc/freelist.hh (free_list::remove, free_list::insert): New methods. * src/misc/freelist.cc (free_list::register_n, free_list::releases_n): Rewrite using free_list::remove and free_list::insert. (free_list::remove, free_list::insert): New methods. * src/tgba/bdddict.hh (bdd_dict::register_anonymous_variables): New method. (bdd_dict::annon_free_list): New subclass. (bdd_dict::free_annonymous_list_of_type_of): New attribute. * src/tgba/bdddict.cc (bdd_dict::register_all_variables_of, bdd_dict::unregister_all_my_variables): Handle anonymous variables too. (bdd_dict::register_anonymous_variables, bdd_dict::annon_free_list::annon_free_list, bdd_dict::annon_free_list::extend): New methods. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::accepting_path) Fix handling of PATH when backtracking. Report from Soheib Baarir. 2004-03-18 Alexandre Duret-Lutz Move the free_list management into a separate class for reuse. * src/misc/freelist.hh, src/misc/freelist.cc: New files. * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them. * src/misc/bddalloc.hh (bdd_allocator): Inherit from free_list and make dump_free_list visible. * src/misc/bddalloc.cc (bdd_allocator::allocate_variables): Move all the code into free_list::register_n() and bdd_allocator::extend(), and call the former. (bdd_allocator::release_variables): Move all the code into free_list::release_n() and call it. (bdd_allocator::extend): New method. * src/tgba/bdddict.cc (bdd_dict::dump): Call dump_free_list; 2004-03-09 Alexandre Duret-Lutz * configure.ac, NEWS: Bump version to 0.0s. 2004-03-08 Alexandre Duret-Lutz * configure.ac, NEWS: Bump version to 0.0r. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm) : Do not blindly enumerate all combinations of atomic properties; initially set all_props to the set of all possibly satisfiable combinations. 2004-02-21 Alexandre Duret-Lutz * lbtt/src/Makefile.am (lbtt_translate_SOURCES): Fix leftover from 1.0.3 merge. * wrap/python/cgi/ltl2tgba.in: Process ltl2tgba.opt if it exists. * wrap/python/cgi/ltl2tgba.in: Color translators and their options. 2004-02-20 Alexandre Duret-Lutz * wrap/python/cgi/ltl2tgba.in: Present the options in a table. * wrap/python/cgi/ltl2tgba.in: Remove the "print dot" options, add a "dot source" source behind each picture instead. Do not run `dot' on big automata. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Fix example in comment. Skip false transitions, and do not compute sub-formulae reachable only via false transitions. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Revert yesterday's change. This optimization is NOT covered by exprop. In fact it could be generalized. 2004-02-19 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Remove the cond_for_true optimization. It is covered by exprop. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::current_state): Fix reference to Oddoux's thesis. 2004-02-16 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add the symb_merge argument. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Likewise. * src/tgbatest/ltl2tgba.cc (main): Rename -fx as -x, and add -y to unset symb_merge. * wrap/python/cgi/ltl2tgba.in: Remove the exprop version of the FM translator, make exprop and symb_merge options. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit) : suppress the GFy optimisation introduced on 2003-11-26, it is generalized by the identification of states with same symbolic rewriting introduced on 2004-02-02. * lbtt/: Merge lbtt 1.0.3. 2004-02-13 Alexandre Duret-Lutz * src/tgbatest/ltl2baw.pl (END): Ensure LTL2TGBA is always closed. 2004-02-11 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (syntax): Recognize "-" as input filename for the formula. Merge the transitions of automata read with -X. * src/tgbatest/spotlbtt.test: Add many disabled algorithms. It is convenient to reuse the `config' file created by this test when making statistics. * src/tgbatest/ltl2baw.pl: New file. * src/tgbatest/Makefile.am (EXTRA_DIST): Add ltl2baw.pl. 2004-02-10 Alexandre Duret-Lutz * wrap/python/libpy.c: Update from Swig 1.3.21. * HACKING: Update versions. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Take an exprop argument. Consider all possible combinations of propositions when generating arcs. Suggested by Jean-Michel Couvreur. * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Adjust. * src/tgbatest/ltl2tgba.cc: Honor -fx. * src/tgbatest/spotlbtt.test: Exercise -fx. * wrap/python/cgi/ltl2tgba.in: Support Couvreur/FM with exploded properties. 2004-02-09 Alexandre Duret-Lutz * src/ltlparse/ltlparse.yy: Typo. * wrap/python/cgi/ltl2tgba.in: Use render_dot when showing formula. * wrap/python/cgi/README: Mention unique_id. 2004-02-08 Alexandre Duret-Lutz This should help getting accurate statistics (on both the formula automaton and the synchronized product) from LBTT. Idea from Jean-Michel Couvreur. * src/tgbaalgos/lbtt.cc (nonacceptant_lbtt_bfs): New class. (nonacceptant_lbtt_reachable): New function. * src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): New function. * src/tgbatest/ltl2tgba.cc (main): Call nonacceptant_lbtt_reachable if the -T option is used. * src/tgbatest/spotlbtt.test: Setup the -T variants, disabled by default. 2004-02-05 Alexandre Duret-Lutz * src/tgbaalgos/lbtt.hh: Typos. * src/tgbatest/spotlbtt.test: Typo. * wrap/python/spot.i (unblock_signal): New function. * wrap/python/cgi/ltl2tgba.in (print_footer, alarm_handler) (reset_alarm): New functions. Kill the script and its children if it runs for too long. (render_dot): Call reset_alarm. 2004-02-03 Alexandre Duret-Lutz * configure.ac, NEWS: Bump version to 0.0q. * configure.ac, NEWS: Bump version to 0.0p. * wrap/python/cgi/ltl2tgba.in: Fix setting to cope with IE, Safari, konqueror, ... None of these support rules="groups" frame="border" properly (Mozilla is OK). 2004-02-02 Alexandre Duret-Lutz * wrap/python/cgi/ltl2tgba.in: Output a description of the syntax. * wrap/python/cgi/ltl2tgba.in: Import spot and redirect stderr to stdout early. * wrap/python/cgi/ltl2tgba.in (print_stats): Compute and display the number of acceptance conditions. * wrap/python/tests/bddnqueen.py, wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py: Specify coding system to accommodate newer Python versions. * src/misc/bddalloc.hh: Make all methods public. * wrap/python/spot.i: Include misc/bddalloc.hh and misc/minato.hh. * wrap/python/tests/minato.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add minato.py. * src/tgbatest/explicit.cc, src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc, src/tgbatest/readsave.cc, src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Add missing copyright license. * wrap/python/cgi/ltl2tgba.in (render_dot): Render .png directly with dot, without using convert. * wrap/python/cgi/README: Do not mention convert. * wrap/python/cgi/ltl2tgba.in (render_dot, render_automaton) (render_bdd): New functions, extracted from the rest of the code. * wrap/python/cgi/ltl2tgba.in (default_translator): Default to trans_fm. (translators): Show trans_fm before trans_lacim. * wrap/python/cgi/ltl2tgba.in (print_stats): New function. Call it to display the size of the generalized and degeneralized automata. * src/tgbalagos/stats.hh, src/tgbalagos/stats.cc: New files. * src/tgbalagos/Makefile.am: Add them. * wrap/python/spot.i: Include src/tgbalagos/dupexp.hh and src/tgbalagos/stats.hh * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Identify states with identical successors. This optimizes the translation of `a R (b R c)', for instance. * src/tgbatest/ltl2tgba.test: Add two new tests. Hide the tgba_gspn and tgba_gspn_eesrg classes. Offer the corresponding automaton via the automaton() method of the gspn_interface and gspn_eesrg_interface classes. * iface/gspn/gspn.hh (gspn_interface::gspn_interface): Take dict and env arguments. (gspn_interface::automaton): New method. (tgba_gspn): Move all the declaration ... * iface/gspn/gspn.cc (tgba_gspn): ... here. (gspn_interface::automaton): Implement it. * iface/gspn/eesrg.hh (gspn_eesrg_interface::gspn_eesrg_interface): Take dict and env arguments. (gspn_eesrg_interface::automaton): New method. (tgba_gspn_eesrg): Move all the declaration ... * iface/gspn/gspn.cc (tgba_gspn_eesrg): ... here. (gspn_eesrg_interface::automaton): Implement it. * iface/gspn/dottygspn.cc, iface/gspn/dottyeesrg.cc, iface/gspn/ltlgspn.cc: Adjust. 2004-01-30 Alexandre Duret-Lutz * src/ltlvisit/tostring.cc: Fix output of F0, F1, G0, G1, X0, and X1. * src/ltltest/tostring.test: Test these. 2004-01-29 Alexandre Duret-Lutz * src/tgba/tgbaexplicit.cc (tgba_explicit::get_acceptance_condition): Do not treat true and false specially. Otherwise it breaks translation of F(false). * src/tgbatest/explprod.test, src/tgbatest/tripprod.test: Do not use true as acceptance condition. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor): Use Acc[b] as acceptance condition for Fb, not Acc[Fb]. After this change, degeneralized automata are 40% smaller in LBTT's statistics. * src/tgba/tgbatba.cc (state_tba_proxy): Store an iterator, pointing somewhere into the acceptance conditions list, instead of an acceptance condition. (state_tba_proxy::acceptance_iterator): New method. (tgba_tba_proxy_succ_iterator): Adjust to use iterators too. (tgba_tba_proxy_succ_iterator::current_state): If the current transition is in several consecutive acceptance steps after the expected one, advance many steps at once. (tgba_tba_proxy::tgba_tba_proxy): Build the acceptance cycle as a list, not a map. (tgba_tba_proxy::get_init_state, tgba_tba_proxy::succ_iter): Adjust. * src/tgba/tgbatba.hh (tgba_tba_proxy::acc_cycle_): Declare as a list, not a map. 2004-01-26 Alexandre Duret-Lutz * src/tgbaalgos/magic.cc (magic_search::~magic_search): Release all iterators on the stack. (magic_search::check): Release iterators that are popped off the stack. * src/tgbatest/explpro2.test: Fix reordering regex. * src/tgbatest/defs.in (run): Use libtool --mode=execute. 2004-01-23 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Merge transitions with same destination and acceptance conditions directly, without calling a->merge_transition(). If one transitions goes to "True", subtract its conditions from all other transitions; this optimizes a U b. * src/ltlast/refformula.hh (ref_formula::ref_count_): New method. * src/ltlast/refformula.cc (ref_formula::ref_count_): New method. * src/ltlast/atomic_prop.hh (atomic_prop::dump_instance): New method. * src/ltlast/atomic_prop.cc (atomic_prop::dump_instance): New method. * src/tgbaalgos/ltl2tgba_fm.cc: Typos in comments. 2004-01-13 Alexandre Duret-Lutz * configure.ac, NEWS: Bump version to 0.0o. * configure.ac: Bump version to 0.0n. * NEWS: Update. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::check, emptiness_check::check2): Document them. 2004-01-12 Alexandre Duret-Lutz * iface/gspn/ltlgspn.cc (main): Typo, use MIN_ARG. 2004-01-09 Alexandre Duret-Lutz * iface/gspn/dcswaveeltl.test, iface/gspn/udcsefm.test, iface/gspn/udcseltl.test: Exercize -e2. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::check2): New function, variant of emptiness_check::check(). * src/tgbaalgos/emptinesscheck.hh (emptiness_check::check2): Likewise. * src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Exercize -e2. * src/tgbatest/ltl2tgba.cc: Support -e2, for emptiness_check::check2(). * iface/gspn/Makefile.am [WITH_GSPN_EESRG] (check_PROGRAMS): Compile ltlgspn-eesrg instead of ltleesrg. (ltleesrg_SOURCES, ltleesrg_LDADD): Replace by... (ltlgspn_eesrg_SOURCES, ltlgspn_eesrg_LDADD, LIBGSPNESRG_LDFLAGS): ... these. * iface/gspn/ltleesrg.cc: Delete. * iface/gspn/ltlgspn.cc [EESRG]: Support EESRG conditionally. Support -e2. * src/tgbaalgos/ltl2tgba_lacim.cc: Typo in comment. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::check): Typos in comments. * m4/gspnlib.m4 (AX_CHECK_GSPNLIB): Do not warn about a missing library for eesrg. Define the WITH_GSPN_EESRG conditional. * iface/gspn/Makefile.am (gspn_HEADERS, check_PROGRAMS): Add the eesrg items in condition WITH_GSPN_EESRG. (libspotgspneesrg_la_LIBADD, libspotgspneesrg_la_CPPFLAGS) (libspotgspneesrg_la_SOURCES): Define only in condition WITH_GSPN_EESRG. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_stats): New function. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::print_stats): Likewise. * iface/gspn/ltlgspn.cc (main) : Call print_stats(). * iface/gspn/ltleesrg.cc (main): Likewise. * iface/gspn/ltlgspn.cc: Add option -P. 2004-01-08 Alexandre Duret-Lutz Run valgrind in test cases. * src/tgbatest/defs.in (VALGRIND, run): Define. * src/tgbatest/bddprod.test, 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/tgbaread.test, src/tgbatest/tripprod.test: Use run(). 2004-01-06 Alexandre Duret-Lutz * iface/gspn/eesrg.cc (format_state): Do not rewrite \n's, just strip the last one. Escaping must be done at output. * iface/gspn/gspm.cc (format_state): Likewise. * src/misc/escape.hh, src/misc/escape.cc: New files. * src/misc/Makefile.am: Add them. * src/tgba/bddprint.cc (bdd_format_accset): New function. * src/tgba/bddprint.hh (bdd_format_accset): New function. * src/tgbaalgos/dotty.cc (dotty_bfs::process_state): Escape the state name using escape_str(). (dotty_bfs::process_link): Escape conditions and acceptance conditions using escape_str(). * src/tgbaalgos/save.cc (save_bfs::start): Call print_acc(). (save_bfs::print_acc): New function extracted from save_bfs::start(). Escape each acceptance condition. (save_bfs::process_state): Use escape_str() and print_acc() * src/ltlvisit/tostring.cc (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. * src/tgbaalgos/reachiter.hh: Typos in comments. * iface/gspn/eesrg.cc (tgba_gspn_eesrg::all_acceptance_conditions, tgba_gspn_eesrg::neg_acceptance_conditions): Forward to data_->operand. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle): Do not skip this computation if from == to but the period is empty. * iface/gspn/eesrg.cc (state_gspn_eesrg::clone): Clone the right state. * iface/gspn/ltleesrg.cc: Emptinesscheck the full product, not the control automaton. * iface/gspn/eesrg.cc (tgba_gspn_eesrg::project_state): New method. * iface/gspn/eesrg.hh: Likewise. 2004-01-05 Alexandre Duret-Lutz * src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatest/powerset.cc: New file. * src/tgbatest/Makefile.am: Construct powerset and expldot from powerset.cc. * src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::run) Reuse s->second to avoid a hash lookup. * src/tgbaalgos/save.cc (save_bfs::process_state): Delete dest. * src/ltlparse/Makefile.am ($(FROM_LTLPARSE_YY_MAIN)): Use $(FROM_LTLPARSE_YY_MAIN), not $@, because $@ can contains VPATH and we do not want Bison to see absolute paths. * src/tgbaparse/Makefile.am ($(FROM_TGBAPARSE_YY_MAIN)): Likewise. * src/ltltest/parseerr.test: Adjust. * src/ltlparse/ltlparse.yy: Simplify error handling now that Bison will call destructors. Give each operator a full name, so that Bison uses it in error messages. 2003-12-30 Alexandre Duret-Lutz * iface/gspn/ltleesrg.cc: New file. * iface/gspn/Makefile.am (check_PROGRAMS): Add ltleesrg. (ltleesrg_LDADD, ltleesrg_SOURCES): New variables. * src/ltltest/defs.in (run): Rerun valgrind with --leak-check=yes. * src/ltlparse/ltlparse.yy: Add `%destructor's. 2003-12-29 Alexandre Duret-Lutz * src/ltltest/defs.in (run): New function, run valgrind. * src/ltltest/equals.test, src/ltltest/lunabbrev.test, src/ltltest/nenoform.test, src/ltltest/parse.test, src/ltltest/parseerr.test, src/ltltest/tostring.test, src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test: Use run(). * Makefile.am (EXTRA_DIST): Don't list the m4/*.m4 files, Automake 1.8 find them automatically. * configure.ac: Require Automake 1.8, in gnits mode, and check for valgrind. * THANKS: New empty file. * doc/Doxyfile.in: Upgrade to Doxygen 1.3.5. Build documentation for iface/. * dox/mainpage.dox: Fix reference to ltl_to_tgba. * src/ltlenv/environment.hh: Typo. 2003-12-03 Alexandre Duret-Lutz * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh (tgba_explicit::merge_transitions): New method. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Factorize all variables (not just Next and A) when computing prime implicants, and then call merge_transitions(). 2003-12-01 Alexandre Duret-Lutz * configure.ac: Bump version to 0.0m. * configure.ac, NEWS: Bump version to 0.0l. * doc/Makefile.am ($(srcdir)/spotref.pdf): Do not assume spot.latex is in the srcdir. 2003-11-28 Alexandre Duret-Lutz * src/tgbaparse/tgbaparse.yy (cond_list): Simplify into... (condition): ... this. We now accept only one condition, which is a formula. * src/tgba/tgbaexplicit.hh (tgba_explicit::add_neg_condition, tgba_explicit::get_condition): Remove, unused. * src/tgba/tgbaexplicit.cc: Likewise. * iface/gspn/eesrg.cc, iface/gspn/eesrg.hh, iface/gspn/gspn.cc, iface/gspn/gspn.hh, src/tgba/bdddict.cc, src/tgba/bdddict.hh, src/tgba/bddprint.hh, src/tgba/succiter.hh, src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.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/dotty.cc, src/tgbaalgos/dupexp.cc, src/tgbaalgos/emptinesscheck.cc, src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/save.cc, src/tgbatest/explicit.cc, src/tgbatest/ltl2tgba.cc, src/tgbaparse/tgbaparse.yy, wrap/python/tests/ltl2tgba.py: Rewrite `accepting condition' as `acceptance condition'. The symbols which have been renamed are: tgba::all_accepting_conditions tgba::neg_accepting_conditions succ_iterator::current_accepting_conditions bdd_dict::register_accepting_variable bdd_dict::register_accepting_variables bdd_dict::is_registered_accepting_variable tgba_bdd_concrete_factory::declare_accepting_condition tgba_bdd_core_data::accepting_conditions tgba_bdd_core_data::all_accepting_conditions tgba_explicit::declare_accepting_condition tgba_explicit::complement_all_accepting_conditions tgba_explicit::has_accepting_condition tgba_explicit::get_accepting_condition tgba_explicit::add_accepting_condition tgba_explicit::all_accepting_conditions tgba_explicit::neg_accepting_conditions state_tba_proxy::acceptance_cond accepting_cond_splitter 2003-11-26 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit) : Optimize translation of GFy. * src/tgba/bddprint.cc (print_accset_handler, bdd_print_accset): New functions. * src/tgba/bddprint.cc (bdd_print_accset): Declare it. * src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use it. * src/tgbatest/tgbaread.test, src/tgbatest/explicit.test: Adjust expected output. 2003-11-25 Alexandre Duret-Lutz * src/tgbaparse/tgbaparse.yy: Remove a random character. * src/tgba/formula2bdd.cc: Include cassert. 2003-11-24 Alexandre Duret-Lutz Explicit automata can now have arbitrary logic formula on their arcs. ltl2tgba_fm benefits from this and join multiple arcs with the same destination and acceptance conditions. * src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh: New files. * src/tgba/Makefile.am (tgba_HEADERS, libtgba_la_SOURCES): Add them. * src/tgba/bddprint.cc, src/tgba/bddprint.hh (bdd_pring_formula, bdd_format_formula): New functions. * src/tgba/tgbaexplicit.hh (tgba_explicit::get_condition, tgba_explicit::add_condition, tgba_explicit::add_neg_condition, tgba_explicit::declare_accepting_condition, tgba_explicit::has_accepting_condition, tgba_explicit::get_accepting_condition, tgba_explicit::add_accepting_condition): Take a const formula*. * src/tgba/tgbaexplicit.cc (tgba_explicit::add_condition): Rewrite using formula_to_bdd. * src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use bdd_print_formula to display conditions. * src/tgbaalgos/save.cc (save_bfs::process_state): Likewise. * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::bdd_to_formula): New function. (translate_dict::conj_bdd_to_atomic_props): Remove. (ltl_to_tgba_fm): Factor successors on accepting conditions and destinations, not conditions. Use bdd_to_formula to translate the conditions. * src/tgbaparse/tgbaparse.yy: Expect conditions as a formula in a string, call the LTL parser for this. * src/tgbaparse/tgbascan.ll: Process \" and \\ escapes in strings. * src/tgbatest/emptchke.test, src/tgbatest/explicit.test, src/tgbatest/explpro2.test, src/tgbatest/explpro3.test, src/tgbatest/explprod.test, src/tgbatest/mixprod.test, src/tgbatest/readsave.test, src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Adjust to new syntax for explicit automata. * src/misc/minato.hh (minato_isop(bdd,bdd)): New constructor variant. (minato_isop::local_vars::vars): New attribute. (minato_isop::local_vars::local_vars): Add the vars arguments. (minato_isop::todo, minato_isop::cube, minato_isop::ret): Rename as ... (minato_isop::todo_, minato_isop::cube_, minato_isop::ret_): ... these. * src/misc/minato.cc: Adjust to factorize only variables in vars. * m4/devel.m4: Fix quoting and simplify default setting of enable_devel. 2003-11-21 Alexandre Duret-Lutz * AUTHORS: New file. * configure.ac (AM_INIT_AUTOMAKE): Remove `foreign' option. * COPYING: New file. * 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. * src/misc/minato.cc: Include cassert. * src/misc/minato.cc, src/misc/minato.hh: New files. * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Use minato_isop. 2003-11-14 Alexandre Duret-Lutz * src/ltltest/Makefile.am (AM_CXXFLAGS): New variable. * tgba/bdddict.hh (bdd_dict::register_propositions, bdd_dict::register_accepting_variables): New methods. * src/bdddict.cc: Likewise. * tgba/tgbaexplicit.cc (tgba_explicit::add_conditions, tgba_explicit::add_accepting_conditions): New methods. (tgba_explicit::get_init_state): Add an "empty" initial state to empty automata. * tgba/tgbaexplicit.hh: (tgba_explicit::add_conditions, tgba_explicit::add_accepting_conditions): New methods. * tgbaalgos/Makefiles.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add dupexp.hh and dupexp.cc. * tgbaalgos/dupexp.hh, tgbaalgos/dupexp.cc: New files. * tgbatest/Makefile.am (AM_CXXFLAGS): New variable. (check_SCRIPTS): Add dupexp.test. (CLEANFILES): Add output1 and output2. * tgbatest/dupexp.test: New file. * tgbatest/ltl2tgba.cc: Handle -s and -S. * tgbatest/tgbaread.cc: Remove unused variable exit_code. * src/ltlparse/ltlscan.ll: Include ltlparse/parsedecl.hh, not parsedecl.hh. * src/tgbaparse/tgbascan.ll: Likewise, include tgbaparse/parsedecl.hh. 2003-11-13 Alexandre Duret-Lutz * src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle): Check whether the state is in the current SCC before passing it to h_filt(). 2003-11-07 Alexandre Duret-Lutz * iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg::first_): New attribute. (tgba_succ_iterator_gspn_eesrg::step): Use first_. Loop until succ returns some successors. Report from Soheib Baarir. 2003-11-06 Alexandre Duret-Lutz * iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg::step): Fix the iteration logic. (tgba_succ_iterator_gspn_eesrg::tgba_succ_iterator_gspn_eesrg): Make sure not to free successors_ twice. (tgba_succ_iterator_gspn_eesrg::done): Fix definition. * iface/gspn/eesrg.cc (tgba_gspn_eesrg::get_init_state): Do not call get_init_state(), use 0 instead. (tgba_gspn_eesrg::format_state): Handle the case where s->left() == 0. Reported by Soheib Baarir. * src/ltlparse/ltlscan.ll: Cosmetics. * configure.ac: Bump version to 0.0k. 2003-11-03 Alexandre Duret-Lutz * iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg::step): Really Skip unknown variables. * configure.ac, NEWS: Bump version to 0.0j. * iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg::step): Skip unknown variables. * iface/gspn/gspn.cc (tgba_gspn_eesrg_private_::tgba_gspn_eesrg_private_): Show prop_index() and prop_kind() arguments on error. * iface/gspn/eesrg.cc (tgba_gspn_eesrg_private_::tgba_gspn_eesrg_private_): Show prop_index() argument on error. * src/ltlparse/Makefile.am ($(FROM_LTLPARSE_YY_MAIN)): cd into $(srcdir) before running bison, so that bison does not put absolute filenames in generated files. * src/tgbaparse/Makefile.am ($(FROM_TGBAPARSE_YY_MAIN)): Likewise. Reported by Soheib Baarir. * iface/gspn/Makefile.am (gspn_HEADERS): Add eesrg.hh. Reported by Soheib Baarir. 2003-10-31 Alexandre Duret-Lutz * README: More build instructions. * HACKING: Update. * doc/Makefile.am ($(srcdir)/spotref.pdf): Make sure to work in $(srcdir). 2003-10-30 Alexandre Duret-Lutz * m4/gspnlib.m4: Define LIBGSPNESRG_LDFLAGS. * iface/gspn/Makefile.am (gspn_HEADERS): Add common.hh. (libspotgspn_la_SOURCES): Add common.cc. (libspotgspneesrg_la_LIBADD, libspotgspneesrg_la_CPPFLAGS) (libspotgspneesrg_la_SOURCES, ltlgspn_eesrg_SOURCES) (dotty_eesrg_LDADD, dotty_eesrg_CPPFLAGS): New variables. (lib_LTLIBRARIES): Add libspotgspneesrg.la. (check_PROGRAMS): Add dottygspn-eesrg. * iface/gspn/gspn.hh, iface/gspn/gspn.cc (gspn_exeption, operator<<(gspn_exeption), gspn_environment): Move ... * iface/gspn/common.hh, iface/gspn/common.cc: ... in these new files. * iface/gspn/eesrg.hh, iface/gspn/eesrg.cc, iface/gspn/dottyeesrg.cc: New files. 2003-10-28 Alexandre Duret-Lutz * src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle): Simplify, comment, and free memory. * src/tgbaalgos/emptinesscheck.cc (triplet): New class. (emptiness_check::accepting_path): Simplify, comment, derecursive, and free memory... 2003-10-27 Alexandre Duret-Lutz * src/tgbaalgos/emptinesscheck.cc (connected_component): Split into ... (emptiness_check::connected_component, emptiness_check::connected_component_set): ... these. * src/tgbaalgos/emptinesscheck.cc: Adjust. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::h_filt, emptiness_check::~emptiness_check) New methods. (emptiness_check::check): Release all iterators in todo on exit. (emptiness_check::counter_example): Rewrite the BFS logic. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::h_filt, emptiness_check::~emptiness_check): New methods. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::~tgba_tba_proxy_succ_iterator): Delete the proxied iterator. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::counter_example): Remove unused tmp_last, best_lst, and tmp_acc variables. 2003-10-24 Alexandre Duret-Lutz * src/tgbaalgos/emptinesscheck.cc (emptiness_check::counter_example): Rewrite initialization. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_result): Fix memory leak. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::check): Simplify, reorganize, and comment. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::root_component): Rename as ... (emptiness_check::root): ... this, to follow the paper. * src/tgbaalgos/emptinesscheck.cc: Remove some superfluous `emptiness_check::'. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::remove_component): Rewrite. 2003-10-23 Alexandre Duret-Lutz * src/tgbaalgos/emptinesscheck.cc (emptiness_check::check, emptiness_check::counter_example): Simplify access to hashes after calls to find() for the same element.. * src/tgbaalgos/emptinesscheck.hh (connected_component::set_of_state): Rename as ... (connected_component::set_type): ... this, and define as a hash_set. (connected_component::has_state): New method. * src/tgbaalgos/emptinesscheck.cc (connected_component::has_state): New method. (emptiness_check::counter_example, emptiness_check::complete_cycle, emptiness_check::accepting_path): Simplify using has_state(). * src/tgbaalgos/emptinesscheck.hh (emptiness_check::seen_state_num): Rename as ... (emptiness_check::h): ... this, and define as a hash_map. (emptiness_check::remove_component): Remove superfluous state_map argument. * src/tgbaalgos/emptinesscheck.cc: Adjust. * src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc: Remove superfluous includes. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::emptiness_check): New, take the automaton to work on, and store it ... (emptiness_check::aut_): ... in this new attribute. (emptiness_check::tgba_emptiness_check): Rename as ... (emptiness_check::check): ... this, and remove the automata argument. (emptiness_check::counter_example, emptiness_check::print_result, emptiness_check::remove_component, emptiness_check::accepting_path, emptiness_check::complete_cycle): Remove the automata argument. * src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc: Adjust. * src/tgbaalgos/emptinesscheck.hh (connected_component::not_null, connected_component::transition_acc, connected_component::nb_transition, connected_component::nb_state): Remove these unused attributes. (connected_component::connected_component): Merge the two definitions into one. (connected_component::~connected_component): Remove. (connected_component::isAccepted): Delete, unused. * src/tgbaalgos/emptinesscheck.cc (connected_component::connected_component, connected_component::~connected_component): Adjust. (connected_component::isAccepted): Delete. (spot): * src/tgbatest/emptchk.test: Typo. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::remove_component, emptiness_check::root_component, emptiness_check::seen_state_num, emptiness_check::suffix): Move in private part. (emptiness_check::arc_accepting, emptiness_check::todo): Move ... * src/tgbaalgos/emptinesscheck.cc (emptiness_check::tgba_emptiness_check): ... as local variables of this function. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::vec_component): Move ... (emptiness_check::counter_example): ... as local variable of this function. * src/tgbaalgos/emptinesscheck.hh (pair_state_iter, triplet): Move ... * src/tgbaalgos/emptinesscheck.cc (pair_state_iter, triplet): ... here. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_result): Indent output as in the magic search. * src/tgbatest/spotlbtt.test: Add notice about long run time. Merge emptinesscheckexplicit into ltl2tgba. * src/tgbatest/Makefile.am (check_PROGRAMS): Remove emptinesscheckexplicit. (emptinesscheckexplicit_SOURCES): Remove. (TESTS): Replace emptinesscheckexplicit.test by emptchke.test. * src/tgbatest/emptinesscheckexplicit.cc, src/tgbatest/emptinesscheckexplicit.test: Delete. * src/tgbatest/empchke.test: New file. * src/tgbatest/ltl2tgba.cc: Add support for -X. Merge emptiness-checks tests into ltl2tgba. * src/tgbatest/Makefile (check_PRORGRAMS): Remove emptinesscheck and ltlmagic. (emptinesscheck_SOURCES, ltlmagic_SOURCES): Remove. (TESTS): Replace emptinesscheck.test and ltlmagic.test by emptchk.test. * src/tgbatest/emptinesscheck.test, src/tgbatest/ltlmagic.test: Delete. * src/tgbatest/emptchk.test: New file. * src/tgbatest/emptinesscheck.cc, src/tgbatest/ltlmagic.cc: Delete. * src/tgbatest/ltl2tgba.cc: Add support for -e, -E, -m, -M, and -n. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::tgba_emptiness_check): Do not print anything. (emptiness_check::counter_example): Assume that tgba_emptiness_check has already been called. 2003-10-22 Alexandre Duret-Lutz * src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc (emptiness_check::seq_counter, emptiness_check::periode): Rename as ... (emptiness_check::prefix, emptiness_check::period): ... these. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::tgba_emptiness_check, emptiness_check::accepting_path): Simplify BDD operations. * src/tgbaalgos/emptinesscheck.cc, src/tgbaalgos/emptinesscheck.hh: Reindent. (emptiness_check::~emptiness_check, emptiness_check::emptiness_check): Remove, unused. 2003-10-15 Alexandre Duret-Lutz * iface/gspn/ltlgspn.cc (main): Allow invocations with only one atomic proposition. 2003-10-14 Alexandre Duret-Lutz * src/misc/bddalloc.cc (bdd_allocator::initialize): Augment bdd_init()'s arguments. 2003-10-08 Alexandre Duret-Lutz * iface/gspn/ltlgspn.cc: Use command-line options to select algorithms, not #defines. * iface/gspn/Makefile.am (check_PROGRAMS): Remove eltlgspn-srg, efmgspn-srg, fmgspn-rg, and fmgspn-srg and their associated source variables. These are all replaced by ltlgspn-rg and ltlgspn-srg. * iface/gspn/dcswavefm.test, iface/gspn/dcswaveltl.test, iface/gspn/dcswaveeltl.test, iface/gspn/udcsefm.test, iface/gspn/udcseltl.test, iface/gspn/udcsfm.test, iface/gspn/udcsltl.test: Adjust calls to ltlgspn-srg. * iface/gspn/Makefile.am (XFAIL_TESTS): Remove. 2003-10-06 Rachid REBIHA * iface/gspn/ltlgspn.cc: We call tgba_emptiness_check before counter_example. And we print the prefix and the periode of counter_example's result. * src/tgbatest/emptinesscheckexplicit.cc (main): We call tgba_emptiness_check before counter_example. * src/tgbatest/emptinesscheck.cc (main): We call tgba_emptiness_check before counter_example. * src/tgbaalgos/emptinesscheck.hh (spot): (spot::print_result): New methode to print the prefix and the periode of counter_example's result. * src/tgbaalgos/emptinesscheck.cc (spot): counter_example doesn't call tgba_emptiness_check. counter_example must be executed after calling tgba_emptiness_check. Remove tgba_emptiness_check calls. (print_result): New methode to print the prefix and the periode of counter_example's result. Remove most of all std::cout during execution of emptiness_check's methodes. 2003-10-02 Alexandre Duret-Lutz * iface/gspn/udcsfm.test, iface/gspn/udcsefm.test: New files. * iface/gspn/Makefile.am (TESTS) Add them. (check_PROGRAMS): Add emgspn-srg. (efmgspn_srg_SOURCES, efmgspn_srg_LDADD, efmgspn_srg_CPPFLAGS): New variables. * iface/gspn/udcsltl.test, iface/gspn/udcseltl.test: Complete. * src/ltlparse/ltlscan.ll: Allow doubly quoted atomic propositions. 2003-10-01 Alexandre Duret-Lutz * iface/gspn/udcsltl.test, iface/gspn/udcseltl.test, iface/gspn/dcswaveltl.test, iface/gspn/dcswaveeltl.test, iface/gspn/dcswavefm.test: Do not accept $? = 0 when a failure is expected. * iface/gspn/udcsltl.test, iface/gspn/udcseltl.test: New files * iface/gspn/Makefile.am (TESTS): Add them. (XFAIL_TESTS): Add udcseltl.test. * iface/gspn/example/udcs/udcs.net, iface/gspn/example/udcs/udcs.def iface/gspn/example/udcs/udcs.tobs: New files. * iface/gspn/Makefile.am (EXTRA_DIST): Add them. * iface/gspn/Makefile.am (check_PROGRAMS): Add eltlgspn-srg. (eltlgspn_srg_SOURCES, eltlgspn_srg_LDADD, eltlgspn_srg_CPPFLAGS): New variables. (TESTS): Add dcswaveeltl.test. * iface/gspn/dcswaveeltl.test: New file. * iface/gspn/ltlgspn.cc [CEC]: Use emptiness_check. * m4/debug.m4, m4/devel.m4, m4/gccoptim.m4, m4/ndebug.m4: New files. * Makefile.am (EXTRA_DIST): Add them. * configure.ac: Call adl_ENABLE_DEVEL, adl_ENABLE_DEBUG, ad_GCC_OPTIM, and adl_NDEBUG. 2003-09-30 Alexandre Duret-Lutz * src/tgba/state.hh (state_ptr_less_than, state_ptr_equal): Declare as std::binary_function. (state_ptr_hash): Declare as std::unary_function. * src/tgbaalgos/lbtt.cc (state_acc_pair_equal, state_acc_pair_hash): Likewise. * src/misc/bddlt.hh (bdd_less_than): Likewise. * src/misc/hash.hh (ptr_hash, string_hash): Likewise. 2003-09-25 Rachid REBIHA * src/tgbatest/emptinesscheckexplicit.test, src/tgbatest/emptinesscheckexplicit.cc src/tgbatest/emptinesscheck.test, src/tgbatest/emptinesscheck.cc, src/tgbaalgos/emptinesscheck.cc, src/tgbaalgos/emptinesscheck.hh: New files. 2003-09-22 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh: Rename as ... * src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/ltl2tgba_lacim.hh: ... this, and rename ltl_to_tgba() as ltl_to_tgba_lacim as well. * iface/gspn/ltlgspn.cc, src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlmagic.cc, src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc, src/tgbatest/tripprod.cc, wrap/python/spot.i, wrap/python/cgi/ltl2tgba.in, wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py: Adjust. 2003-09-11 Alexandre Duret-Lutz * src/tgba/state.hh: Include cassert. 2003-08-29 Alexandre Duret-Lutz * src/tgba/state.hh (state::hash): New method. (state_ptr_equal, state_ptr_hash): New functors. * src/tgba/statebdd.hh, src/tgba/statebdd.cc (state_bdd::hash): New method. * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc (state_explicit::hash): New method. (ns_map, sn_map): Use Sgi::hash_map instead of std::map. * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc (state_product::hash): New method. * src/tgba/tgbatba.cc (state_tba_proxy::hash): New method. * src/tgbaalgos/lbtt.cc (acp_seen, todo_set, seen_map): Redefine using Sgi::hash_map or Sgi::hash_set. (lbtt_reachable): Don't erase a key that is pointed to by an iterator. * src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::~tgba_reachable_iterator): Likewise. * src/tgbaalgos/magic.cc (magic_search::~magic_search()): Likewise. * src/tgbaalgos/magic.hh (hash_type): Redefine using Sgi::hash_map. * src/tgbaalgos/reachiter.hh (seen_map): Redefine using Sgi::hash_map. * iface/gspn/gspn.cc (state_gspn::hash): New method. * src/misc/hash.hh (string_hash): New functor. * src/tgba/tgbaexplicit.cc (tgba_explicit::all_accepting_conditions) Compute all_accepting_conditions_ from neg_accepting_conditions_, not by browsing the dictionary. The dictionary also contains accepting conditions from other automata... This bug was a consequence of the change from 2003-07-14. * src/tgbaalgos/save.cc (save_bfs::start()): Likewise, do not browse the dictionary to print accepting conditions. Call ->all_accepting_conditions() instead. * src/tgba/tgbaproduct.cc (tgba_product::tgba_product): Typo from 2003-08-22 in the computation of all_accepting_conditions_. * src/tgbatest/explpro3.test: New file. * src/tgbatest/Makefile.am (TESTS): Add explpro3.test. * src/tgbatest/explprod.test, src/tgbatest/explpro2.test, src/tgbatest/tripprod.test: Sort the output using Perl. 2003-08-28 Alexandre Duret-Lutz Rewrite all std::map as Sgi::hash_map. * 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 . 2003-08-25 Alexandre Duret-Lutz * src/tgba/state.hh (state_ptr_less_than): Make sure left is non-null. Suggested by Denis Poitreneaud. 2003-08-23 Alexandre Duret-Lutz * wrap/python/Makefile.am (MAINTAINERCLEANFILES): Add buddy_wrap.cxx and buddy.py. 2003-08-22 Alexandre Duret-Lutz * src/tgbaalgos/magic.cc (seen_with_magic, seen_without_magic): Remove. * wrap/python/cgi/ltl2tgba.in: Fix display of relations for tgba_bdd_concrete automata. Fix computation of product acceptance conditions, when the two operands share some acceptance conditions. * src/tgba/tgbaproduct.hh (tgba_product::left_acc_complement_, tgba_product::right_acc_complement_): New attribute. * src/tgba/tgbaproduct.cc (tgba_product::tgba_product): Set them. (tgba_product::succ_iter): Use them. * src/tgba/explpro2.test: New file. * src/tgba/Makefile.am (TESTS): Add it. 2003-08-20 Alexandre Duret-Lutz * tgba/tgbaproduct.cc, tgba/tgbaproduct.hh: (state_bdd_product, tgba_product_succ_iterator): Rename as ... (state_product, tgba_succ_iterator_product): ... these. * iface/gspn/dcswavefm.test: New file. * iface/gspn/Makefile.am (check_PROGRAMS): Add fmgspn-rg and fmgspn-srg. (fmgspn_rg_SOURCES, fmgspn_rg_CPPFLAGS, fmgspn_rg_LDADD, fmgspn_srg_SOURCES, fmgspn_srg_CPPFLAGS, fmgspn_srg_LDADD): New variables. (TESTS): Add dcswavefm.test. 2003-08-19 Alexandre Duret-Lutz * src/ltlast/formula.hh: Make it clear that ref() and unref() deals with one node, not a entire formula. 2003-08-18 Alexandre Duret-Lutz * configure.ac: Bump version to 0.0i. * configure.ac, NEWS: Bump version to 0.0h. * wrap/python/cgi/Makefile.am (CLEANFILES): Clean ltl2tgba.py. * wrap/python/tests/ltl2tgba.test: Run $srcdir/ltl2tgba.py, not ltl2tgba.py. 2003-08-15 Alexandre Duret-Lutz This implements Couvreur's FM'99 ltl2tgba translation. * src/tgba/bdddict.cc (bdd_dict::is_registered): Split as ... (bdd_dict::is_registered_proposition, bdd_dict::is_registered_state, bdd_dict::is_registered_accepting_variable): ... these. * src/tgba/bdddict.hh: Likewise. * src/tgba/tgbaexplicit.cc (tgba_explicit::set_init_state): New method. (tgba_explicit::declare_accepting_condition): Arrange so that this function can be called during the construction of the automaton. (tgba_explicit::complement_all_accepting_conditions): New method. (tgba_explicit::has_accepting_condition): Adjust to call bdd_dict::is_registered_accepting_variable. * src/tgba/tgbaexplicit.hh (tgba_explicit::set_init_state, tgba_explicit::complement_all_accepting_conditions): New methods. * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them. * src/tgbaalgos/ltl2tgba.hh: Add bibtex entry in comment. * src/tgbatest/Makefile.am (check_PROGRAMS): Remove spotlbtt and tbalbtt. (tbalbtt_SOURCES, tbalbtt_CXXFLAGS, spotlbtt_SOURCES): Remove. * src/tgbatest/spotlbtt.cc: Delete, superseded by "ltl2tgba -F -t". * src/tgbatest/ltl2tgba.cc: Implement the -f and -F options. * src/tgbatest/spotlbtt.test: Use "ltl2tgba -F -t" instead of "spotlbtt", "ltl2tgba -F -t -D" instead of "tbalbtt", and add also check the ltl2tgba_fm translator. * wrap/python/spot.i: Wrap ltl2tgba_fm. * wrap/python/cgi/ltl2tgba.in: Add radio buttons to select between ltl2tgba and ltl2tgba_fm. * wrap/python/tests/ltl2tgba.py: Add support for the -f option. * wrap/python/tests/ltl2tgba.test: Try the -f option. varnum can be augmented by other allocator. Keep track of a local varnum (lvarnum) in each allocator. * src/misc/bddalloc.cc (bdd_allocator::bdd_allocator): Initialize lvarnum. (bdd_allocator::extvarnum): New method. (bdd_allocator::allocate_variables): Use lvarnum and extvarnum. * src/misc/bddalloc.hh (bdd_allocator::extvarnum): New mathod. (bdd_allocator::lvarnum): New variable. 2003-08-14 Alexandre Duret-Lutz * src/tgba/state.hh, src/tgba/statebdd.hh, src/tgba/statebdd.cc: Remove the translate() method. Useless since 2003-07-14. 2003-08-11 Alexandre Duret-Lutz * wrap/python/Makefile.am (SUBDIRS): Build `.' first. * wrap/python/cgi/Makefile.am (ltl2tgba.py): Depend on Makefile. 2003-08-10 Alexandre Duret-Lutz Revamp the multop interface to allow some basic optimizations like 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. * src/tgba/succiterconcrete.cc, src/tgba/tgbaexplicit.cc, src/tgba/tgbatba.cc, src/tgbaalgos/lbtt.cc: Use `-' instead of `& !' between two BDDs. That's one less call to BuDDy. * src/tgbatest/tgbaread.test, src/tgbatest/explicit.test: Adjust expected output after 2003-08-07's change. * src/tgba/bdddict.hh: Typo in comments. * src/ltlenv/environment.hh: Typo in comments. 2003-08-08 Alexandre Duret-Lutz * src/ltlparse/ltlparse.yy: Handle and diagnose mismatched parentheses. * src/ltltest/parseerr.test: Add some examples. 2003-08-07 Alexandre Duret-Lutz * wrap/python/cgi/ltl2tgba.in: Convert GIFs to PNGs. Restrict the size of dot's output to 1024x1024. * src/tgbaalgos/dotty.cc (dotty_bfs::start): Do not preset the size of the graph. Set height=0 for the invisible state. 2003-08-06 Alexandre Duret-Lutz * src/ltlparse/ltlparse.yy: Fix precedence OP_OR < OP_XOR < OP_AND. * src/ltlast/binop.cc (binop::instance): Order operands for associative operators, so that e.g. "a xor b" and "b xor a" are mapped to the same formula. * src/ltltest/equals.test: Check this. * src/ltlvisit/dotty.cc (draw_node_): s/shabe/shape/. (visit): Draw rectangular nodes for atomic propositions and constant. This is an attempt to mimic BuDDy's output. * wrap/python/cgi/ltl2tgba.in: Handle show_formula_dot and show_formula_gif. * src/ltlvisit/dotty.hh (dotty): Move the ostream argument first. * src/ltlvisit/dump.hh (dump): Likewise. * src/ltltest/equals.cc, src/ltltest/readltl.cc, src/ltlvisit/dotty.cc, src/ltlvisit/dump.cc: Adjust. 2003-08-05 Alexandre Duret-Lutz * src/misc/version.hh, src/misc/version.cc: New files. * src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them. * wrap/python/spot.i: Include misc/version.hh. * wrap/python/cgi/ltl2tgba.in: Print spot.version(). * README: Update layout. * wrap/python/cgi/Makefile.am, wrap/python/cgi/ltl2tgba.in, wrap/python/cgi/README: New files. * wrap/python/Makefile.am (SUBDIRS): Add cgi. * configure.ac: Output wrap/python/cgi/Makefile. * wrap/python/spot.i: Add an ostringstream emulation. 2003-08-04 Alexandre Duret-Lutz * wrap/python/spot.i: Add an ofstream emulation. * wrap/python/spot.i: Declare spot::tgba::get_init_state, spot::tgba::succ_iter, and spot::tgba_succ_iterator::current_state as constructors. * wrap/python/Makefile.am (lib_LTLIBRARIES) (libspotswigpy_la_SOURCES, libspotswigpy_la_CFLAGS) (libspotswigpy_la_LDFLAGS): New variables. (_spot_la_LIBADD, _buddy_la_LDFLAGS): Link with libspotswigpy.la ($(srcdir)/spot_wrap.cxx, $(srcdir)/buddy_wrap.cxx): Run swig with -c. * wrap/python/tests/libpy.c: New file. * wrap/python/tests/run.in: Run python if no arguments are given. * wrap/python/tests/interdep.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add interdep.py. * wrap/python/spot.i: Declare spot::ltl_to_tgba as a constructor. * wrap/python/tests/ltl2tgba.py: Do not force `thisown=1' on tgba objects. * wrap/python/spot.i: Include headers from tgba/ and tgbaalgos/. * wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test: New files. * wrap/python/tests/Makefile.am (TESTS): Add ltl2tgba.test. (EXTRA_DIST): Add ltl2tgba.py. * wrap/python/tests/run.in: Distinguish *.py and *.test. * wrap/python/tests/ltlparse.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add it. 2003-08-01 Alexandre Duret-Lutz * wrap/python/buddy.i: New file. * wrap/python/Makefile.am (EXTRA_DIST): Add it. (python_PYTHON, MAINTAINERCLEANFILES): Add buddy.py. (pyexec_LTLIBRARIES): Add _buddy.la. (_buddy_la_SOURCES, _buddy_la_LDFLAGS, $(srcdir)/buddy_wrap.cxx) ($(srcdir)/buddy.py): New. * wrap/python/tests/bddnqueen.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add it. * src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: Merge the two unabbreviate_logic definitions (const and non-const) into a function that takes a const formula* and return a non-const formula*. Since formula* is convertible to const formula*, and the const version of the function just called the non-onst one, it makes no sense to keep both. Also, it confused Swig. * src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh: Likewise for negative_normal_form. * src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh: Likewise for unabbreviate_ltl. * src/ltlvisit/clone.cc, src/ltlvisit/clone.hh: Likewise for clone. * src/ltlvisit/destroy.cc, src/ltlvisit/destroy.hh: Likewise for destroy. * configure.ac: Bump version to 0.0g. * configure.ac, NEWS: Bump version to 0.0f. * iface/gspn/simple.test, iface/gspn/dcswave.test, iface/gspn/dcswaveltl.test: Make sure the example directory is writable. * m4/lbtt.m4, m4/buddy.m4: Always configure buddy/ and lbtt/, regardless of the --with-included-buddy and --with-included-lbtt settings. * wrap/python/Makefile.am (python_PYTHON, _spot_la_SOURCES): Explicitely refer to spot_wrap.cxx and spot.py as $(srcdir)/spot_wrap.cxx and $(srcdir)/spot.py. (spot_wrap.cxx, spot.py): * wrap/python/Makefile.am (spot_wrap.cxx, spot.py): Lookup spot.i in $(srcdir). 2003-07-31 Alexandre Duret-Lutz * configure.ac: Output wrap/python/tests/Makefile and wrap/python/tests/run. * wrap/python/Makefile.am (SUBDIRS): New variable. * wrap/python/spot.i: Include all formulae headers from ltlast/, as well as ltlvisit/destroy.hh. (spot::ltl::formula::__cmp__, spot::ltl::formula::__str__): New functions. * wrap/python/tests/Makefile.am, wrap/python/tests/ltlsimple.py, wrap/python/tests/run.in: New files. * wrap/python/ltihooks.py: New file. * wrap/python/Makefile.am (EXTRA_DIST): Add ltihooks.py. * wrap/Makefile.am, wrap/spot.i: Move ... * wrap/python/Makefile.am, wrap/python/spot.i: ... here. * wrap/Makefile.am: New file. * configure.ac: Output wrap/python/Makefile. * src/misc/const_sel.hh: Delete. * src/misc/Makefile.am (misc_HEADERS): Remove const_sel.hh. * src/tgbaalgos/magic.cc, src/tgbaalgos/reachiter.cc: Include cassert. * iface/Makefile.am (SUBDIRS): Recurse in gspn only if condition WITH_GSPN. 2003-07-30 Alexandre Duret-Lutz * iface/gspn/gspn.cc (tgba_gspn::format_state): Call gspn's print_state. * iface/gspn/dcswaveltl.test: Check for a false formula too. * iface/gspn/dcswaveltl.test, iface/gspn/ltlgspn.cc: New files. * iface/gspn/Makefile.am (TESTS): Add dcswaveltl.test. (ltlgspn_rg_LDADD, ltlgspn_srg_LDADD, ltlgspn_rg_SOURCES) (ltlgspn_srg_SOURCES): New variables. (check_PROGRAMS): Add ltlgspn-rg and ltlgspn-srg. * iface/gspn/Makefile.am (gspn_HEADERS, gspndir): Install gspn.hh. * src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::project_state): New method. * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc (tgba_product::project_state): New method. * src/tgba/tgbabta.hh, src/tgba/tgbabta.cc (tgba_bta_proxy::project_state): New method. * src/tgbaalgos/magic.cc (magic_search::print_result): Take a restrict argument. 2003-07-29 Alexandre Duret-Lutz * src/ltlparse/ltlscan.ll: Allow /\, \/, and xor, used in LBTT. * src/ltltest/parse.test: Test them. * src/tgbaalgos/lbtt.cc: Typos. * lbtt/: Upgrade to lbtt 1.0.2. * src/tgbatest/Makefile.am (check_PROGRAMS): Add tbalbtt. (tbalbtt_SOURCES, tbalbtt_CXXFLAGS): New variables. * src/tgbatest/spotlbtt.cc [TBA]: Build tba proxies conditionally. * src/tgbatest/spotlbtt.test: Include tbalbtt in the tests. 2003-07-28 Alexandre Duret-Lutz * src/tgba/tgbatba.hh, src/tgba/tgbatba.cc (tgba_tba_proxy::state_is_accepting): New method. * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc: New files. * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES, tgbaalgos_HEADERS): Add them. * src/tgbatest/ltlmagic.cc, src/tgbatest/ltlmagic.test: New files. * src/tgbatest/Makefile.am (TESTS, ltlmagic_SOURCES, check_PROGRAMS): Add them. 2003-07-25 Alexandre Duret-Lutz * src/tgba/tgba.hh (tgba::~tgba): Make it public. * src/tgba/tgbatba.cc, src/tgba/tgbatba.hh: New files. * src/tgba/Makefile.am (tgba_HEADERS): Add tgbatba.hh. (libtgba_la_SOURCES): Add tgbatba.cc. * src/tgbatest/ltl2tgba.cc: Add option -D. * src/tgbaalgos/lbtt.cc (bdd_less_than): Move ... * src/misc/bddlt.hh: ... in this new file. * src/misc/Makefile.am (misc_HEADERS): Add bddlt.hh. * iface/gspn/dcswave.test: Comment state space sizes. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add reachiters.hh. (libtgbaalgos_la_SOURCES): Add reachiters.cc. * src/tgbaalgos/dotty.cc, src/tgbaalgos/save.cc: Rewrite using spot::tgba_reachable_iterator_breadth_first. * src/tgbatest/explicit.test, src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Adjust expected output. 2003-07-24 Alexandre Duret-Lutz * configure.ac: Output iface/gspn/defs. * iface/gspn/Makefile.am (EXTRA_DIST): Add $(TESTS). (TESTS, check_SCRIPTS, distclean-local): New. * iface/gspn/dcswave.test, iface/gspn/simple.test, iface/gspn/defs.in: New files. * iface/gspn/dottygspn.cc (main): Take the list of properties of interest in argument. 2003-07-23 Alexandre Duret-Lutz * iface/gspn/examples/DCSwave/DCSWave.def, iface/gspn/examples/DCSwave/DCSWave.net iface/gspn/examples/DCSwave/DCSWave.tobs, iface/gspn/examples/simple/simple.def, iface/gspn/examples/simple/simple.net, iface/gspn/examples/simple/simple.tobs: New files, from Yann Thierry-Mieg. * iface/gspn/Makefile.am (EXTRA_DIST): New variables. * iface/gspn/gspn.cc (tgba_gspn_private_::tgba_gspn_private_): Rethrow caught expections. 2003-07-22 Alexandre Duret-Lutz * m4/gspnlib.m4: Check for libgspnRG.a and libgspnSRG.a. Define LIBGSPNRG_LDFLAGS and LIBGSPNSRG_LDFLAGS, not LIBGSPN_LDFLAGS. * iface/gspn/Makefile.am: Adjust, build dottygspn-rg and dottygspn-srg instead of dottygspn. * iface/gspn/gspn.cc (EVENT_TRUE): Undefine. (tgba_gspn_private_::~tgba_gspn_private_): Free all_indexes. * iface/gspn/dottygspn.cc (main): Destroy the automaton before its dictionary. 2003-07-17 Alexandre Duret-Lutz Now succ_iter() can fetch extra information from the root of a product to reduce its number of successors. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgba.cc. * src/tgba/tgba.hh (tgba::succ_iter): Add the global_state and global_automaton arguments. (tgba::support_conditions, tgba::support_variables, tgba::compute_support_conditions, tgba::compute_support_variables): New functions. (tgba::last_support_conditions_input_, tgba::last_support_conditions_output_, tgba::last_support_variables_input_, tgba::last_support_variables_output_): New attributes. * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::succ_iter): Handle the two new arguments. (tgba_bdd_concrete::compute_support_conditions, tgba_bdd_concrete::compute_support_variables): Implement them. * src/tgba/tgbabddconcrete.hh: Adjust. * src/tgba/tgbaexplicit.cc (tgba_explicit::succ_iter): Ignore the two new arguments. (tgba_explicit::compute_support_conditions, tgba_explicit::compute_support_variables): Implement them. * src/tgba/tgbaexplicit.hh: Adjust. * src/tgba/tgbaproduct.cc (tgba_product::succ_iter): Handle the two new arguments. (tgba_product::compute_support_conditions, tgba_product::compute_support_variables): Implement them. * src/tgba/tgbaproduct.hh: Adjust. * iface/gspn/gspn.cc (tgba_gspn_private_::last_state_cond_input, tgba_gspn_private_::last_state_cond_output, (tgba_gspn_private_::tgba_gspn_private_): Set last_state_cond_input. (tgba_gspn_private_::~tgba_gspn_private_): Delete last_state_cond_input. (tgba_gspn_private_::state_conds): New function, eved out from tgba_gspn::succ_iter. (tgba_gspn::succ_iter): Use it. Use the two new arguments. (tgba_gspn::compute_support_conditions, tgba_gspn::compute_support_variables): New functions. * iface/gspn/gspn.hh: Adjust. * iface/gspn/gspn.cc (EVENT_TRUE): Override temporarily. (tgba_gspn::succ_iter): Fix usage of cube. 2003-07-16 Alexandre Duret-Lutz * m4/gspnlib.m4: New file. * configure.ac: Call AX_CHECK_GSPNLIB. * Makefile.am (EXTRA_DIST): Add m4/gspnlib.m4. * iface/gspn/Makefile.am (AM_CPPFLAGS): Add $(LIBGSPN_CPPFLAGS). (libspotgspn_la_LIBADD, check_PROGRAMS, dottygspn_SOURCES, dottygspn_LDADD): New variables. * iface/gspn/gspn.hh (gspn_interface): New class. (gspn_exeption): Take a string argument and adjust all callers. (operator<<): Define for gspn_exeption. * iface/gspn/gspn.cc (gspn_interface::gspn_interface, gspn_interface::~gspn_interface): New. * iface/gspn/gspnlib.h: Delete, it belongs to GSPN. * iface/gspn/dottygspn.cc: New file. 2003-07-15 Alexandre Duret-Lutz * m4/lbtt.m4 (AX_CHECK_LBTT): Set LBTT and LBTT_TRANSLATE when using an already installed lbtt. Homogenize passing of automata as pointers, not references. Disallow copy for security. * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Disallow copy. * src/tgba/tgbaexplicit.hh (tgba_explicit): Likewise. * src/tgba/tgbaexplicit.cc (tgba_explicit::operator=, tgba_explicit::tgba_explicit(tgba_explicit)): Remove. * src/tgba/tgbabddconcreteproduct.cc (tgba_bdd_concrete_product_factory::tgba_bdd_concrete_product_factory, product): Take operand automata as pointers. * src/tgba/tgbabddconcreteproduct.hh (product): Likewise. * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: (tgba_product): Disallow copy. (tgba_product::tgba_product): Take operand automata as pointers. * src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty_reachable): Take tgba arguments as pointer. * src/tgbaalgos/dotty.hh (dotty_reachable): Likewise. * src/tgbaalgos/lbtt.cc (fill_todo, lbtt_reachable): Likewise. * src/tgbaalgos/lbtt.hh (lbtt_reachable): Likewise. * src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh (ltl_to_tgba): Likewise. * src/tgbaalgos/save.cc (save_rec, tgba_save_reachable): Likewise. * src/tgbaalgos/save.hh (save): Likewise. * src/tgbatest/explicit.cc, src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc, src/tgbatest/readsave.cc, src/tgbatest/spotlbtt.cc, src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Likewise. 2003-07-14 Alexandre Duret-Lutz Before this change, all automata would construct their own dictionaries (map of BDD variables to LTL formulae). This was cumbersome, because to multiply two automata we had to build a common dictionary (the union of the two LTL formula spaces), and install wrappers to translate each automaton's BDD answers into the common dictionary. This translation, that had to be repeated when several products were nested, was time consuming and was a hindrance for some optimizations. In the new scheme, all automata involved in a product must share the same dictionary. An empty dictionary should be constructed by the user and passed to the automaton' constructors as necessary. This huge change removes more code than it adds. * src/Makefile.am (libspot_la_LIBADD): Add misc/libmisc.la. * src/misc/bddalloc.hh, src/misc/bddalloc.cc: New files. These partly replace src/tgba/bddfactory.hh and src/tgba/bddfactory.cc. * src/misc/Makefile.am: Adjust to build bddalloc.hh and bddalloc.cc. * src/tgba/bddfactory.hh, src/tgba/bddfactory.cc, src/tgba/dictunion.hh, src/tgba/dictunion.cc, src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc, src/tgba/tgbabddtranslatefactory.hh, src/tgba/tgbabddtranslatefactory.cc, src/tgba/tgbatranslateproxy.hh, src/tgba/tgbatranslateproxy.cc: Delete. * src/tgba/bdddict.hh, src/tgba/bdddict.cc: New files. These replaces tgbabdddict.hh and tgbabdddict.cc, and also part of bddfactory.hh and bddfactory.cc. * src/tgba/bddprint.cc, src/tgba/bddprint.hh: Adjust to use bdd_dict* instead of tgba_bdd_dict&. * src/tgba/succiterconcrete.cc (succ_iter_concrete::next()): Get next_to_now from the dictionary. * src/tgba/tgba.hh (tgba::get_dict): Return a bdd_dict*, not a const tgba_bdd_dict*. * src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh: Adjust to use the new dictionary, stored in data_. * src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbabddconcretefactory.hh: Likewise. Plus now_to_next_ is now also stored in the dictionary. * src/tgba/tgbabddconcreteproduct.cc: Likewise. Now that both operand share the same product, there is not point in using tgba_bdd_translate_factory. * src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh: Store a bdd_dict (taken as constructor argument). (tgba_bdd_core_data::~tgba_bdd_core_data): Remove. (tgba_bdd_core_data::translate): Remove. (tgba_bdd_core_data::next_to_now): Remove (now in dict). (tgba_bdd_core_data::dict): New pointer. * src/tgba/tgbabddfactory.hh: (tgba_bdd_factory::get_dict): Remove. * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Adjust to use the new dictionary. * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Likewise. Do not use tgba_bdd_dict_union and tgba_bdd_translate_proxy anymore. * src/tgbaalgos/lbtt.cc, src/tgbaalgos/save.cc: Adjust to use bdd_dict* instead of tgba_bdd_dict&. * src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.cc: Likewise. (ltl_to_tgba): Take a dict argument. * src/tgbaparse/public.hh (tgba_parse): Take a dict argument. * src/tgbaparse/tgbaparse.yy (tgba_parse): Take a dict argument. * src/tgbatest/explicit.cc, src/tgbatest/explprod.cc, src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc, src/tgbatest/readsave.cc, src/tgbatest/spotlbtt.cc, src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Instantiate a dictionary, and pass it to the automata' constructors. * src/tgbatest/ltl2tgba.cc: Likewise, and remove the -o (defrag) option. * iface/gspn/gspn.hh (tgba_gspn::tgba_gspn): Take a bdd_dict argument. (tgba_gspn::get_dict): Adjust return type. * iface/gspn/gspn.cc: Do not use bdd_factory, adjust to use the new dictionary instead. 2003-07-13 Alexandre Duret-Lutz * configure.ac: Bump version to 0.0e. * configure.ac: Bump version to 0.0d. * NEWS, README: New files. 2003-07-12 Alexandre Duret-Lutz * m4/lbtt.m4: Run lbtt-translate, not lbtt. * iface/gspn/gspn.cc: Include cassert. 2003-07-10 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(multop)): Forward root_ to children of And. (ltl_trad_visitor::recurse): Take a root argument. * src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory::add_relation): Rename as ... (tgba_bdd_concrete_factory::constrain_relation): ... this. * src/tgba/tgbabddconcretefactory.cc, src/tgbaalgos/ltl2tgba.cc: Adjust. * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::G)): Do not create Now/Next variable when G is the root of the formula. (ltl_trad_visitor::ltl_trad_visitor): Take a root argument. (ltl_trad_visitor::recurse): Create a new visitor, do not copy the current one. (ltl_to_tgba): Build ltl_trad_visitor with root = true. * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::X)): Remove FIXME about handling X(a U b) and X(a R b) better, it's done naturally. * src/tgbatest/spotlbtt.test: Make 100 rounds. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Fix so that !p.!Acc[g].Acc[f] + p.!Acc[g].Acc[f] + p.Acc[g].!Acc[f] is factored as !p.!Acc[g].Acc[f] + p.(!Acc[g].Acc[f] + Acc[g].!Acc[f]), not !Acc[g].Acc[f] + p.Acc[g].!Acc[f]. 2003-07-09 Alexandre Duret-Lutz * lbtt/: New directory. Contains a patched version of lbtt 1.0.1. * Makefile.am (MAYBE_LBTT): New variables. (SUBDIRS): Add $(MAYBE_LBTT). (EXTRA_DIST): Add m4/lbtt.m4. * configure.ac: Call AX_CHECK_LBTT. * m4/lbtt.m4: New file. * src/tgbatest/Makefile.am (check_PROGRAMS): Add spotlbtt. (spotlbtt_SOURCES): New variables. (TESTS): Add spotlbtt.test. (CLEANFILE): Add config. * src/tgbatest/defs.in (top_builddir, LBTT, LBTT_TRANSLATE): New substitutions. * src/tgbatest/spotlbtt.cc, src/tgbatest/spotlbtt.test: New files. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Fix computation of states sharing the same accepting set. Make sure we only output one initial state in LBTT's output. * src/tgbaalgos/lbtt.cc (fill_todo): Add the 'first' argument to designate initial states. (lbtt_reachable): Adjust calls to fill_todo. Handle the fake initial state accepting conditions specially. * src/tgbaalgos/lbtt.hh: Update comments. * src/tgbaalgos/lbtt.cc (lbtt_reachable): Do not end transitions guards with -1 in output. 2003-07-08 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc: Add option -t to output the LBTT automata. * src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add lbtt.hh. (libtgbaalgos_la_SOURCES): Add lbtt.cc. * src/tgba/bddprint.cc (print_sat_handler): Put a space after "!". * src/tgbatest/readsave.test: Adjust spaces after "!". * src/ltlvisit/dump.cc: Strip useless spot::ltl:: prefixes. 2003-07-07 Alexandre Duret-Lutz First sketch of the GSPN wrapper objects. * iface/gspn/gspn.cc, iface/gspn/gspn.hh: New files. * iface/gspn/Makefile.am (libspotgspn_la_SOURCES): Add them. * src/tgba/succiter.hh (current_state, current_conditions current_accepting_conditions): Mark as const. * src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh, src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh, src/tgba/tgbatranslateproxy.cc, src/tgba/tgbatranslateproxy.hh: Likewise. * iface/gspn/gspnlib.h: Fit 80 columns. [__cplusplus]: Wrap everything under extern "C". * src/tgba/succiterconcrete.hh (tgba_succ_iterator_concrete::current_acc_): New attribute. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Set current_acc_. (tgba_succ_iterator_concrete::current_accepting_conditions): Simply return it. * configure.ac: Output iface/Makefile and iface/gspn/Makefile. * iface/Makefile.am, iface/gspn/Makefile.am: New files. * Makefile.am (SUBDIRS): Add iface. * iface/gspn/gspnlib.h: New file, from Yann and Souheib. * src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::tgba_bdd_core_data, tgba_bdd_core_data::translate): Handle all_accepting_conditions. * src/tgba/tgbabddconcretefactory.cc (tgba_bdd_concrete_factory::finish): Fill all_accepting_conditions. 2003-07-04 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit): Declare accepting conditions w.r.t. to Now variables, not Next. 2003-07-03 Alexandre Duret-Lutz * src/tgba/tgbaproduct.cc (tgba_product_succ_iterator::first): Simplify, do not call next_non_false_() if either side is done. * src/tgba/succiter.hh (tgba_succ_iterator::current_condition): State that this is a boolean function. * src/tgba/succiterconcrete.hh (tgba_succ_iterator_concrete::trans_dest_, tgba_succ_iterator_concrete::trans_set_, tgba_succ_iterator_concrete::trans_set_left_, tgba_succ_iterator_concrete::neg_trans_set_): Remove. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::tgba_succ_iterator_concrete, tgba_succ_iterator_concrete::first): Adjust to removed members. (tgba_succ_iterator_concrete::next): Simplify, transitions are no labelled by boolean functions, not only conjunctions. Suggested by Denis Poitrenaud. 2003-07-02 Alexandre Duret-Lutz * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New function. * src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate): Likewise. * src/tgba/tgbabddtranslatefactory.cc (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use tgba_bdd_core_data::translate. * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::nownext_set): New attribute. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Handle nownext_set. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Use nownext_set to simplify. Rewrite tgba_succ_iterator_concrete::next for the fourth time (or is it the fifth?). * src/tgba/succiterconcrete.hh (tgba_succ_iterator_concrete::trans_dest_, tgba_succ_iterator_concrete::trans_set_, tgba_succ_iterator_concrete::trans_set_left_, tgba_succ_iterator_concrete::neg_trans_set_): New attributes. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::tgba_succ_iterator_concrete): Initialize new members. (tgba_succ_iterator_concrete::first): Likewise. (tgba_succ_iterator_concrete::next): Rewrite. * tgba/tgbabddcoredata.hh (tgba_bdd_core_data::acc_set): New attribute. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Handle acc_set. 2003-07-01 Alexandre Duret-Lutz * src/tgba/tgbabddtranslatefactory.cc (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Translate varandnext_set. 2003-06-30 Alexandre Duret-Lutz * src/tgbaparse/tgbaparse.yy (lines): Expect at last one line. * doc/Doxyfile.in (HAVE_DOT): Set to YES to output collaboration diagrams. * doc/mainpage.dox: Typo. * src/tgba/state.hh (state::as_bdd): Delete. * src/tgba/tgbaproduct.hh (state_bdd_product): Inherit from state, not state_bdd. (state_bdd_product::state_bdd_product): Adjust. * src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product): Adjust. * src/tgba/succiter.hh (tgba_bdd_succ_iterator::done): Mark as const. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::done): Likewise. * src/tgba/succiterconcrete.hh (tgba_succ_iterator_concrete::done): Likewise. * src/tgba/tgbaexplicit.cc (tgba_explicit_succ_iterator::done): Likewise. * src/tgba/tgbaexplicit.hh (tgba_explicit_succ_iterator::done): Likewise. * src/tgba/tgbaproduct.cc (tgba_product_succ_iterator::done): Likewise. * src/tgba/tgbaproduct.hh (tgba_product_succ_iterator::done): Likewise. * src/tgba/tgbatranslateproxy.hh (tgba_translate_proxy_succ_iterator::done): Likewise. * src/tgba/tgbatranslateproxy.cc (tgba_translate_proxy_succ_iterator::done): Likewise. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Call bdd_satoneset on data_.varandnext_set. The previous implementation was wrong for GFa. * src/tgba/tgbabddcoredata.hh: Declare varandnext_set. * src/tgba/tgbabddcoredata.cc: Handle varandnext_set. * doc/Doxygen.in: Enable LaTeX output. * doc/Makefile.am (spotref.pdf): New rule. (EXTRA_DIST): Add spotref.pdf. * src/tgba/tgbabddconcretefactory.cc: (tgba_bdd_concrete_factory::tgba_bdd_concrete_factory): New. (tgba_bdd_concrete_factory::create_state): Update now_to_next_. (tgba_bdd_concrete_factory::finish): Constraint Next variables in the relation. * src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory::now_to_next_): New variable. 2003-06-28 Alexandre Duret-Lutz Fix errors reported by ICC. * src/tgba/state.hh (state_ptr_less_than::operator()): Make it const. * src/tgba/tgbaproduct.cc: Include string.hh. * src/ltlast/multop.hh (multop::add, multop::add_sorted): Do not use qualified names in declarations. * m4/gccwarn.m4 (CF_GXX_WARNINGS): Fix GXX test. * src/ltlenv/defaultenv.hh, src/ltlenv/defaultenv.cc, src/ltlenv/environment.hh: Add virtual destructors. 2003-06-26 Alexandre Duret-Lutz * Makefile.am (EXTRA_DIST): Add HACKING. * configure.ac: Bump version to 0.0c. * configure.ac: Bump version to 0.0b. * INSTALL: New file. * src/tgba/ltl2tgba.hh, src/tgba/ltl2tgba.cc: Move ... * src/tgbaalgos/ltl2tgba.hh, src/tgbaalgos/ltl2tgba.cc: ... here. * src/tgba/Makefile.am, src/tgbaalgos/Makefile.am: Adjust. * src/tgba/public.hh: Do not include ltl2tgba.hh. * src/tgbatests/explprod.cc, src/tgbatests/ltl2tgba.cc, src/tgbatests/ltlprod.cc, src/tgbatests/mixprod.cc, src/tgbatests/reach.cc, src/tgbatests/tripprod.cc: Adjust inclusions. * src/tgba/tgbabddcoredata.hh: Fix some Doxygen comments. * src/ltlast/formula.hh: More Doxygen comments. * src/tgba/tgba.hh: Use in Doxygen comments. * doc/mainpage.dox: New file. * doc/Makefile.am (EXTRA_DIST): Add mainpage.dox. * doc/Doxyfile.in (INPUT): Add @srcdir@/mainpage.dox * src/tgba/succiter.hh: Adjust comments about promises to refer to accepting conditions. * src/tgba/tgbabddconcretefactory.hh: Likewise. * src/tgba/tgbabddcoredata.hh: Likewise. * src/tgba/dictunion.cc: Likewise. * src/tgba/tgba.hh: Likewise. * doc/Makefile.am (doc): Typo. * src/ltlvisit/tostring.hh (to_string): Add doxygen comments. * src/ltlast/multop.hh (multop::paircmp): Add doxygen comments. * src/tgba/tgbaexplicit.hh (tgba_explicit::transtion, state_explicit, tgba_explicit_succ_iterator): Add doxygen comments. * src/ltlvisit/postfix.hh: Typo. * src/ltlast/Makefile.am (ltlastdir, ltlast_HEADERS): New variables. (libltlast_la_SOURCES): Move all headers to ltlast_HEADERS. * src/ltlenv/Makefile.am (ltlenvdir, ltlenv_HEADERS): New variables. (libltlenv_la_SOURCES): Move all headers to ltlenv_HEADERS. * src/ltlparse/Makefile.am (ltlparsedir, ltlparse_HEADERS): New variables. (libltlparse_la_SOURCES): Move all public headers to ltlparse_HEADERS. * src/ltlvisit/Makefile.am (ltlvisitdir, ltlvisit_HEADERS): New variables. (libltlvisit_la_SOURCES): Move all headers to ltlparse_HEADERS. * src/misc/Makefile.am (include_HEADERS): Rename as .. (misc_HEADERS): ... this. (miscdir): New variable. * src/tgba/Makefile.am (tgbadir, tgba_HEADERS): New variables. (libtgba_la_SOURCES): Move all headers to tgba_HEADERS. * src/tgbaalgos/Makefile.am (tgbaalgosdir, tgbaalgos_HEADERS): New variables. (libtgbaalgos_la_SOURCES): Move all headers to tgbaalgos_HEADERS. * src/tgbaparse/Makefile.am (tgbaparsedir, tgbaparse_HEADERS): New variables. (libtgbaparse_la_SOURCES): Move all public headers to tgbaparse_HEADERS. * src/tgbaparse/public.hh: Include ltlparse/location.hh, not location.hh. * doc/Makefile.am (stamp): Prefix $(srcdir) explicitely. * m4/buddy.m4 (BUDDY_LDFLAGS): Use $(top_builddir), not $(top_srcdir). * src/tgbaparse/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS). * doc/Makefile.am: Rewrite to run Doxygen whenever Doxyfile.in or configure.ac changes. Distribute the html doc. * doc/Doxyfile.in (EXCLUDE_PATTERNS): Complete with useless Bison classes. (FILE_PATTERNS): Remove *.cc files. Distribute BuDDy. Compile and link with the included version if explicitely requested (--with-included-buddy) or if there is now stuitable version already installed. * buddy/: New directory. Contains a patched version of BuDDy 2.2. * m4/buddy.m4: Make sure the installed BuDDy supports bdd_mergepairs. Honor --with-included-buddy and --without-included-buddy. Define the BUDDY_LDFLAGS and BUDDY_CPPFLAGS output variables, and the WITH_INCLUDED_BUDDY Automake conditional * Makefile.am [WITH_INCLUDED_BUDDY] (MAYBE_SUBDIRS): New variable. (SUBDIRS): Prepend $(MAYBE_SUBDIRS). * src/Makefile.am (libspot_LDFLAGS): New variable. * src/tgba/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS). * src/tgbaalgos/Makefile.am (AM_CPPFLAGS): Likewise. * src/tgbatest/Makefile.am (AM_CPPFLAGS): Likewise. 2003-06-25 Alexandre Duret-Lutz * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Rewrite using bdd_satoneset. This time it's for real. (I hope.) * src/tgba/succiterconcrete.hh (current_base_, current_base_left_): Delete. * tgba/tgbabddcoredata.hh (next_set): New variable. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust to update next_set. * src/tgba/bddprint.hh, src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbaproduct.hh: Fix Doxygen comments. * src/tgba/succiterconcrete.hh (next_succ_set_): Rename as ... (succ_set_left_): ... this. (current_base_, current_base_left_): New variables. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::first): Reset current_. (tgba_succ_iterator_concrete::next): Rewrite. (tgba_succ_iterator_concrete::current_state): Simplify. (tgba_succ_iterator_concrete::current_accepting_conditions): Remove atomic proposition with universal quantification. * src/tgba/ltl2tgba.cc (ltl_to_tgba): Normalize the formula. * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::set_init_state): Complete the initial state. (tgba_bdd_concrete::succ_iter): Do not remove Now variable from the BDD passed to the iterator. * tgba/tgbabddcoredata.hh (notnow_set, var_set): New variables. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust to update notnow_set and var_set. * src/tgbatest/ltl2tgba.cc: Support -v. 2003-06-24 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (syntax): Fix usage message. * src/tgbatest/tripprod.test, src/tgbatest/explprod.test: Sort accepting conditions. * src/ltlvisit/nenoform.cc (negative_normal_form): New const variant. * src/ltlvisit/nenoform.hh (negative_normal_form): New const variant. * src/ltlvisit/lunabbrev.cc (unabbreviate_logic): New const variant. * src/ltlvisit/lunabbrev.hh (unabbreviate_logic): New const variant. * src/ltlvisit/tunabbrev.cc (unabbreviate_ltl): New const variant. * src/ltlvisit/tunabbrev.hh (unabbreviate_ltl): New const variant. 2003-06-23 Alexandre Duret-Lutz Switch from "promises" to "accepting sets". Fix the definitions of these accepting sets so that they are really useful. Provide an all_accepting_conditions() method for use in the emptiness check, and a neg_accepting_conditions() for products. Predeclare TGBA accepting conditions in the i/o. * src/tgba/bddprint.cc (want_prom): Rename as ... (want_prom): ... this. (print_handler): Adjust to display Acc[]. (print_acc_handler, bdd_print_acc): New functions. * src/tgba/bddprint.hh (print_acc_handler, bdd_print_acc): New functions. * src/tgba/succiter.hh (current_promise): Rename as ... (current_accepting_conditions): ... this. * src/tgba/succiterconcrete.cc (current_state): Rename next to now. (current_promise): Rename as ... (current_accepting_conditions): ... this, and compute the accepting conditions. * src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc, src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc, src/tgba/tgbabddtranslatefactory.cc, src/tgbaalgos/dotty.cc: Adjust to new names. * src/tgba/tgba.hh (all_accepting_conditions, neg_accepting_conditions): New functions. * src/tgba/tgbabddconcretefactory.cc: Adjust to new names, and record accepting conditions instead of promises. * src/tgba/tgbabddcoredata.hh (accepting_conditions, all_accepting_conditions, negacc_set): New variables. (notnow_set, notprom_set, declare_promise): Rename as ... (notnext_set, notacc_set, declare_accepting_condition): ... these. * src/tgba/tgbaexplicit.hh (tgba_explicit_succ_iterator::current_promise): Rename as ... (tgba_explicit_succ_iterator::current_accepting_conditions): ... this. (tgba_explicit::add_promise): Rename as ... (tgba_explicit::add_accepting_condition): ... this. (tgba_explicit::declare_accepting_condition, tgba_explicit::has_accepting_condition): New variables. (tgba_explicit::get_promise): Rename as ... (tgba_explicit::get_accepting_condition): ... this. (tgba_explicit::all_accepting_conditions, tgba_explicit::neg_accepting_conditions): Implement them. (all_accepting_conditions, neg_accepting_conditions, all_accepting_conditions): New variables. (tgba_explicit_succ_iterator): Embed all_accepting_conditions_. * src/tgba/tgbaexplicit.cc: Likewise. * src/tgba/tgbaproduct.hh (tgba_product_succ_uterator): Embed left_neg_ and right_neg_. (tgba_product::all_accepting_conditions, tgba_product::neg_accepting_conditions): Implement them. * src/tgba/tgbatranslateproxy.hh: (tgba_translate_proxy::all_accepting_conditions, tgba_translate_proxy::neg_accepting_conditions): Implement them. * src/tgba/tgbatranslateproxy.cc: Likewise. * src/tgbaalgos/save.cc (save_rec): Call bdd_print (tgba_save_reachable): Output the `acc =' line. * src/tgbaparse/tgbaparse.yy: Support the for accepting conditions definitions using an "acc =" line at the start. Later, use has_accepting_condition while parsing accepting conditions to ensure they were declared. Disallow !cond in accepting conditions. * src/tgbaparse/tgbascan.ll (ACC_DEF): New token. * src/tgbatest/explicit.cc (main): Declare accepting conditions. * src/tgbatest/ltl2tgba.cc (main): Add support for the -a, -A, and -R new options. * src/tgbatest/tgbaread.cc (main): Really exit on parse error. * src/tgbatest/explicit.test, src/tgbatest/explprod.test, src/tgbatest/mixprod.test, src/tgbatest/readsave.test, src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Reflect recent changes. 2003-06-22 Alexandre Duret-Lutz * src/tgbatest/tripprod.test, src/tgbatest/explprod.test: Sort out some possible inversions in the output. 2003-06-19 Alexandre Duret-Lutz * src/tgba/tgbabddconcretefactory.cc (tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory): destroy the formulae used as keys in prom_. (tgba_bdd_concrete_factory::create_promise): Delete. (tgba_bdd_concrete_factory::declare_promise, tgba_bdd_concrete_factory::finish): New functions. * src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory::create_promise): Delete. (tgba_bdd_concrete_factory::declare_promise, tgba_bdd_concrete_factory::finish): New functions. (tgba_bdd_concrete_factory::prom_): New map. * src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Adjust the Fx and aUb cases to register promises with tgba_bdd_concrete_factory::declare_promise(). (ltl2tgba): Call tgba_bdd_concrete_factory::finish(). * src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Revert the change from 2003-06-12, it needs more work (the automaton generated on Xa&(b U !a) was bogus, with that patch). * src/tgbatest/ltl2tgba.cc: Handle the -o and -r options. * src/tgbatest/tripprod.test, src/tgbatest/explprod.test, src/tgbatest/readsave.test: Adjust to reflect yesterday's bddprint.cc change. 2003-06-18 Alexandre Duret-Lutz * src/tgba/bddprint.cc (print_handler): Quote promises when !want_prom. * src/tgbaparse/tgbaparse.yy (prop_list): Accept strings or identifiers. Discard empty strings. * src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test: New file. * src/tgbatest/Makefile.am (check_PROGRAMS): Add mixprod. (mixprod_SOURCES): New variable. (TESTS): Add mixprod.test. 2003-06-17 Alexandre Duret-Lutz * src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product): New constructor. * src/tgba/tgbaproduct.hh (state_bdd_product::state_bdd_product): New constructor. * tgbatest/tripprod.cc, tgbatest/tripprod.test: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add explprod. (tripprod_SOURCES): New variable. (CLEANFILES): Add input3. (TESTS): Add tripprod.test. 2003-06-16 Alexandre Duret-Lutz * src/tgba/tgbabddprod.cc, src/tgba/tgbabddprod.hh: Rename as ... * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: ... these. (tgba_bdd_product, tgba_bdd_product_succ_iterator): Rename as ... (tgba_product, tgba_product_succ_iterator): ... these, and adjust all uses. * src/tgba/tgbabddtranslateproxy.cc, src/tgba/tgbabddtranslateproxy.hh: Rename as ... * src/tgba/tgbatranslateproxy.cc, src/tgba/tgbatranslateproxy.hh: ... these. (tgba_bdd_translate_proxy, tgba_bdd_translate_proxy_succ_iterator): Rename as ... (tgba_translate_proxy, tgba_translate_proxy_succ_iterator): ... these, and adjust all uses. Make sure we can multiply two tgba_explicit. * tgba/state.hh (state::translate, state::clone, state::as_bdd): New virtual methods. * tgba/stataebdd.cc (state::translate, state::clone): New methods. * tgba/stataebdd.hh (state::translate, state::clone): New methods. * tgba/tgbabddprod.cc (state_bdd_product::clone, tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator): New methods. (tgba_bdd_product_succ_iterator::first): Reset right_ if any of left_ or right_ is already done (i.e., is empty). (tgba_bdd_product_succ_iterator::done): Return true if right_ is NULL. (tgba_bdd_product_succ_iterator::current_state, tgba_bdd_product::get_init_state): Work directory with `state's. * tgba/tgbabddprod.hh (state_bdd_product::clone, tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator): New methods. * tgba/tgbabddtranslateproxy.cc (tgba_bdd_translate_proxy_succ_iterator:: tgba_bdd_translate_proxy_succ_iterator): Work on any kind of iteraator. (tgba_bdd_translate_proxy_succ_iterator:: ~tgba_bdd_translate_proxy_succ_iterator): New method. (tgba_bdd_translate_proxy_succ_iterator::current_state, tgba_bdd_translate_proxy::get_init_state, tgba_bdd_translate_proxy::succ_iter): Work on `state's and `tgba_succ_iterator's directlry. (tgba_bdd_translate_proxy::format_state): Delegate formating to the proxied automata. * tgba/tgbaexplicit.cc (state_explicit::clone): New method. * src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition, tgba_explicit::get_promise): Call ltl::destroy on existing formulae. * tgbatest/explprod.cc, tgbatest/explprod.test: New files. * tgbatest/Makefile.am (check_PROGRAMS): Add explprod. (explprod_SOURCES): New variable. (TESTS): Add explprod.test. (CLEANFILES): Add input1 and input2. 2003-06-12 Alexandre Duret-Lutz * src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Make sure to compute the status of the most Now variables possible. This helps to identify equivalant states. (tgba_bdd_concrete): Call set_init_state. 2003-06-10 Alexandre Duret-Lutz * src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Handle F and G. * src/tgbatest/ltl2tgba.test: Use F and G. 2003-06-06 Alexandre Duret-Lutz * src/tgbatest/bddprod.test: New file. * src/tgbatest/Makefile.am (check_PROGRAMS): Add bddprod. (bddprod_SOURCES, bddprod_CXXFLAGS): New variables. (TESTS): Add bddprod.test. * src/tgbatest/ltlprod.c: Handle BDD_CONCRETE_PRODUCT. * src/tgba/dictunion.cc (tgba_bdd_dict_union): Clone formulae while building new dictionary. * src/tgbatest/ltlprod.test, src/tgbatest/ltlprod.cc: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add ltlprod. (ltlprod_SOURCES): New variable. (TESTS): Add ltlprod.test. * src/ltlvisit/clone.cc (clone): New const version. * src/ltlvisit/clone.hh (clone): Likewise. * src/ltlvisit/destroy.cc (destroy): New const version. * src/ltlvisit/destroy.hh (destroy): Likewise. * src/tgba/tgbabddconcretefactory.cc (tgba_bdd_concrete_factory::create_state, tgba_bdd_concrete_factory::create_atomic_prop, tgba_bdd_concrete_factory::promise): Clone new formulae. * src/tgba/tgbabdddict.cc (tgba_bdd_dict::tgba_bdd_dict, tgba_bdd_dict::~tgba_bdd_dict, tgba_bdd_dict::operator=): New methods that clone and destroy formulae. * src/tgbatest/ltl2tgba.test, src/tgbatest/ltl2tgba.cc: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add ltl2tgba. (ltl2tgba_SOURCES): New variable. (TESTS): Add ltl2tgba.test. * src/ltltest/equals.cc, src/ltltest/readltl.cc, src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include . 2003-06-05 Alexandre Duret-Lutz * src/tgba/bddprint.cc (dict): Make this variable static. (want_prom): New global static variable. (print_handle): Honor want_prom. (print_sat_handler, bdd_print_sat, bdd_format_sat): New functions. (bdd_print_set, bdd_print_dot, bdd_print_table): Set want_prom. * src/tgba/bddprint.hh (bdd_print_sat, bdd_format_sat): New functions. * src/tgbaalgos/save.cc, src/tgbaalgos/save.hh, src/tgbatest/readsave.cc, src/tgbatest/readsave.test: New files. * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add save.cc and save.hh. * src/tgbatest/Makefile.am (check_PROGRAMS): Add readsave. (readsave_SOURCES): New variable. (TESTS): Add readsave.test. * configure.ac: Output src/tgbaparse/Makefile. * src/Makefile.am (SUBDIRS): Add tgbaparse. (libspot_la_LDADD): Add tgbaparse/libtgbaparse.la. * src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition, tgba_explicit::get_promise, tgba_explicit::add_neg_condition, tgba_explicit::add_neg_promise): New methods. * src/tgba/tgbaexplicit.hh: Declare them. * 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/tgbaread.cc, src/tgbatest/tgbaread.test: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add tgbaread. (TESTS): Add tgbaread.cc. (CLEANFILES): Add input. (tgbaread_SOURCES): New variable. * src/ltlparse/ltlparse.yy: Typo in comment. * configure.ac: Output src/tgbatest/Makefile and src/tgbatest/defs. * src/Makefile.am (SUBDIRS): Add tgbatest. * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc: New file. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgbaexplicit.cc and tgbaexplicit.hh. * src/tgbatest/Makefile.am, src/tgbatest/defs.in, src/tgbatest/explicit.cc, src/tgbatest/explicit.test: New files. 2003-06-04 Alexandre Duret-Lutz * src/ltlparse/ltlparse.yy (result): Suppress unused definition. * src/Makefile.am (SUBDIRS): Build `ltltest' after `.'. * src/ltlparse/ltlscan.ll: Use ltlyy as %prefix. * src/ltlparse/parsedecl.hh (YY_DECL): Rename yylex to ltlyylex. * src/ltlparse/ltlparse.yy: Define yylex as ltlyylex. 2003-06-03 Alexandre Duret-Lutz * src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc, src/tgba/succiterconcrete.cc, src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddprod.cc, src/tgba/tgbabddtranslatefactory.cc, src/tgba/tgbabddtranslateproxy.cc: Include . 2003-06-02 Alexandre Duret-Lutz * src/tgba/tgbabdddict.cc, src/tgba/tgbabdddict.hh: New files. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add them. * src/tgba/tgbabdddict.cc (tgba_bdd_dict::contains): New function. * src/tgba/tgbabdddict.hh (tgba_bdd_dict::contains): Likewise. 2003-05-28 Alexandre Duret-Lutz * src/tgba/statebdd.hh (state_bdd::as_bdd): Add non-const variant. * src/tgba/tgbabddtranslateproxy.cc, src/tgba/tgbabddtranslateproxy.hh: New files. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add them. 2003-05-27 Alexandre Duret-Lutz * src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh, src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbabddconcreteproduct.cc, src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddfactory.hh, src/tgba/tgbabddtranslatefactory.hh, src/tgbaalgos/dotty.cc: Add Doxygen comments. * src/tgba/bddfactory.hh, src/tgba/statebdd.hh, src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add Doxygen comments. * src/tgba/bddprint.hh (bdd_format_set): New function. * src/tgba/bddprint.cc (bdd_format_set): Likewise. * src/tgba/state.hh: Add Doxygen comments. (state::compare): Take a state*, not a state&. (state_ptr_less_than): New functor. * src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a state&. * src/tgba/statebdd.cc (state_bdd::compare): Likewise. * src/tgba/succiter.hh: Add Doxygen comments. * src/tgba/tgba.hh: Mention promises. (tgba::formate_state): New pure virtual method. * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::formate_state): New method. * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::formate_state): Likewise. * src/tgbaalgos/dotty.cc: Adjust to use state_ptr_less_than and tgba::formate_state. * src/tgba/succiter.hh (tgba_succ_iterator::current_state): Return a state*, not a state_bdd. * src/tgba/succiterconcrete.hh (tgba_succ_iterator_concrete::current_state): Return a state_bdd*, not a state_bdd. * src/tgba/tgba.hh: Add Doxygen comments. (tgba::succ_iter, tgba::get_init_state): Use state*, not state_bdd. * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::get_init_state): Return a state_bdd*, not a state_bdd. (tgba_bdd_concrete::get_init_bdd): New method. (tgba_bdd_concrete::succ_uter): Take a state* as argument. * src/tgba/tgbabddconcrete.cc: Likewise. * src/tgba/tgbabddtranslatefactory.cc (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use tgba_bdd_concrete::get_init_bdd. * src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty): Adjust to use state* instead of state_bdd. * src/tgba/succlist.hh: Delete. (Leftover from a previous draft.) 2003-05-26 Alexandre Duret-Lutz * src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files. * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them. * src/tgba/tgbabddtranslatefactory.cc (tgba_bdd_translate_factory::compute_pairs): Be quiet. * src/Makefile.am (SUBDIRS): Add tgbaalgos. (libspot_la_LIBADD): Add tgba/libtgbaalgos. * src/tgbaalgos/Makefile.am: New file. * configure.ac: Output src/tgbaalgos/Makefile. * src/tgba/bddprint.hh, src/tgba/bddprint.cc: New files. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add them. * src/tgba/public.hh: Include bddprint.hh. * src/tgba/tgba.hh: Rename as ... * src/tgba/public.hh: .. this. * src/tgba/tgba.hh: New file. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add public.hh. * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Inherit from tgba. (tgba_bdd_concrete::init_iter): Delete. (tgba_bdd_concrete::succ_iter): Take a state_bdd as argument, not a bdd. * src/tgba/tgbabddconcrete.cc: Likewise. Initial code for TGBA (Transition Generalized Büchi Automata). Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba, a LTL-to-TGBA translator using Couvreur's algorithm. * src/Makefile.am (SUBDIRS): Add tgba. (libspot_la_LIBADD): Add tgba/libtgba.la. * configure.ac: Output src/tgba/Makefile. * src/tgba/Makefile.am, src/tgba/bddfactory.cc, src/tgba/bddfactory.hh, src/tgba/dictunion.cc, src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.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/succlist.hh, 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/tgbabdddict.cc, src/tgba/tgbabdddict.hh, src/tgba/tgbabddfactory.hh, src/tgba/tgbabddtranslatefactory.cc, src/tgba/tgbabddtranslatefactory.hh: New files. 2003-05-23 Alexandre Duret-Lutz * m4/gccwarn.m4: Do not use -Winline, this is inappropriate with STL. * src/ltlast/atomic_prop.cc, src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc: Include . 2003-05-16 Alexandre Duret-Lutz * src/ltlvisit/dotty.cc: Rewrite to display formulae as graphs rather than trees, to show how nodes are shared. * src/ltlvisit/dump.hh (dump): Return the passed ostream. * src/ltlvisit/dump.cc (dump): Likewise. * src/ltlvisit/dotty.hh (dotty): Likewise. * src/ltlvisit/dotty.cc (dotty): Likewise. * src/ltlvisit/tostring.hh (to_string): Likewise. * src/ltlvisit/tostring.cc (to_string): Likewise. * src/ltlvisit/dump.hh (dump): Take a formula* as argument, not a formula&. This is more homogeneous. * src/ltlvisit/dump.cc (dump): Likewise. * src/ltlvisit/dotty.hh (dotty): Likewise. * src/ltlvisit/dotty.cc (dotty): Likewise. * src/ltlvisit/tostring.hh (to_string): Likewise. * src/ltlvisit/tostring.cc (to_string): Likewise. * src/ltltest/readltl.cc, src/ltltest/equals.cc, src/ltltest/tostring.cc: Adjust usage. Check trivial multop equality at build time. This makes the equal visitor useless, since two equals formulae will now share the same address. * src/ltlast/multop.hh (add_sorted): New function. (paircmp): New comparison functor. (map): Use paircmp, we want to compare the vectors' contents, not their addresses. * src/ltlast/multop.cc (add_sorted): New function. (add): Use it. * src/ltltest/equals.cc, src/ltltest/tostring.cc: Compare pointers instead of calling equal. * src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: Delete. * src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Remove equals.cc and equals.hh. * wrap/spot.i: Do not include equals.hh. 2003-05-15 Alexandre Duret-Lutz Implement spot::ltl::destroy() and exercise it. * src/ltlast/atomic_prop.hh: Declare instance_count(). * src/ltlast/binop.hh, src/ltlast/unop.hh, src/ltlast/multop.hh: Likewise. Also, really inherit for ref_formula this time. * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, src/ltlast/unop.cc, src/ltlast/multop.cc: On destruction, suppress the instance from the instance map. Implement instance_count(). * src/ltlast/formula.cc, src/ltlast/formula.hh, src/ltlast/ref_formula.cc, src/ltlast/ref_formula.hh: Add virtual destructors. * src/ltlparse/ltlparse.yy: Recover from binary operators with missing right hand operand (the point is just to destroy the the left hand operand). * src/ltltest/equals.cc, src/ltltest/readltl.cc, src/ltltest/tostring.cc: Destroy used formulae. Make sure instance_count()s are null are the end. * src/ltltest/parseerr.test: Adjust expected result, now that the parser lnows about missing right hand operands. * src/ltlvisit/destroy.hh, src/ltlvisit/destroy.cc, src/ltlvisit/postfix.hh, src/ltlvisit/postfix.cc: New files. * src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Add them. * src/ltlvisit/lunabbrev.cc (Xor, Equiv): Clone formulae occurring twice in the rewritten expression. Massage the AST so that identical sub-formula share the same reference-counted formula*. One can't call constructors for AST items anymore, everything need to be acquired through instance() class methods. * src/ltlast/formula.cc, src/ltlast/refformula.cc, src/ltlast/refformula.hh: New files. * src/ltlast/Makefile.am (libltlast_la_SOURCES): Add them. * src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlast/binop.cc, src/ltlast/binop.hh: Make the constructor and destructor protected. Define a static function `instance()' to get an instance with specific argument. Use a map called `instances' to store all known instances. Inherit from ref_formula. * src/ltlast/constant.hh, src/ltlast/constant.cc: Protect the constructor and destructor. Provide the false_instance() and true_instance() functions instead. * src/formula.hh (ref, unref, ref_, unref_): New methods. * src/ltlast/multop.cc, src/ltlast/multop.hh: Protect the constructor, destructor, as well as the add() method. Provides the instance(), and add() class methods instead. Store children_ as a pointer. * src/ltlenv/defaultenv.cc (require): Adjust to call atomic_prop::instance. * src/ltlparse/ltlparse.yy: Adjust to call instance() functions instead of constructors. * src/ltltest/Makefile.am (LDADD): Tweak library ordering. * src/ltlvisit/clone.hh (clone_visitor): Inherit from visitor, not const_visitor, and adjust all prototypes appropriately. * src/ltlvisit/clone.cc (clone_visitor): Likewise. Call ref() or instance() methods instead of copy constructors. * src/ltlvisit/equals.cc: Simplify atomic_prop and constant cases. * src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc, src/ltlvisit/tunabbrev.hh, src/ltlvisit/tunabbrev.cc, src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: Use instance() methods instead of constructor. Make these children of visitor, not const_visitor. * src/ltltest/readltl.c (main): Do not delete the formula. * src/ltlparse/ltlscan.ll (to_parse_size): Declare as size_t to remove a warning with newer versions of Flex. * src/ltlparse/ltlparse.yy (error_list, parse_environment, result): CVS Bison now supports %parse-param for the C++ skeleton; pass these variables as arguments to the Parser::Parser constructor instead of using globals. (parse): Adjust Parser::Parser call. 2003-05-12 Alexandre Duret-Lutz * src/ltlvisit/tostring.cc: Reindent and strip out superfluous spot::ltl:: prefixes. (to_string(formula)): New function. * src/ltlvisit/tostring.hh (to_string(formula)): Likewise. * src/ltltest/tostring.cc: Use this new to_string function to simplify. 2003-05-05 Alexandre Duret-Lutz * m4/buddy.m4: New file. * Makefile.am (EXTRA_DIST): Add m4/buddy.m4. * configure.ac: Call AX_CHECK_BUDDY. 2003-04-30 Alexandre Duret-Lutz * src/ltlvisit/Makefile.am (lib_LTLIBRARIES): Rename as ... (noinst_LTLIBRARIES): ... this. * src/ltlenv/Makefile.am, src/ltlast/Makefile.am, src/ltlparse/Makefile.am: Likewise. * src/Makefile.am (lib_LTLIBRARIES, libspot_la_SOURCES, libspot_la_LIBADD): New variable. Build a libspot.la library from all the sub-libraries. * m4/pypath.m4: New file. * Makefile.am (SUBDIRS): Add wrap. * wrap/Makefile.am: New file. * wrap/spot.i: New file. Preliminary bindings for Python. * configure.ac: Call adl_CHECK_PYTHON and output wrap/Makefile. 2003-04-29 Alexandre Duret-Lutz * configure.ac: Call AC_PROG_LIBTOOL. * src/ltlast/Makefile.am, src/ltlenv/Makefile.am, src/ltlparse/Makefile.am, src/ltltest/Makefile.am, src/ltlvisit/Makefile.am: Adust to build libtool libraries. * src/ltlenv/defaultenv.hh: Do not include atomic_prop.hh here... * src/ltlenv/defaultenv.cc: ... but here. * src/ltltest/tostring.test: Simplify with set -e. Move the description of the test ... * src/ltltest/tostring.cc: ... here, where it is actually coded. * src/ltltest/lunabbrev.test, src/ltltest/tunabbrev.test, src/ltltest/nenoform.test, src/ltltest/tunenoform.test: Simplify with set -e. * configure.ac (AM_INIT_AUTOMAKE): Use nostdinc, to make sure we always use paths relative to src/ in src/'s subdirectories. 2003-04-28 Alexandre Duret-Lutz * src/ltlparse/Makefile.am (CXXFLAGS): Turn on GCC warnings now that CVS Bison is fixed. * src/ltlparse/ltlscan.ll: Use yyunput to shut up a GCC warning. 2003-04-24 Rachid REBIHA * src/ltltest/tostring.test: New file. * src/ltltest/tostring.cc: New files. * src/ltlvisit/tostring.hh: From ast to string New files. * src/ltlvisit/tostring.cc: From ast to string New files. 2003-04-18 Alexandre Duret-Lutz * src/ltlparse/Makefile.am (EXTRA_DIST): Distribute ltlparse.yy. * src/ltlast/Makefile.am (libltlast_a_SOURCES): Add visitor.hh. * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/multop.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh, src/ltlparse/public.hh, src/ltlvisit/clone.hh, src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh, src/ltlvisit/equals.hh, src/ltlvisit/lunabbrev.hh, src/ltlvisit/nenoform.hh, src/ltlvisit/tunabbrev.hh: Add Doxygen comments. * src/visitor.hh: Do not use const_sel. This clarifies the code and helps Doxygen. * configure.ac: Output doc/Doxyfile and doc/Makefile. * doc/Makefile.am, doc/Doxyfile.in: New files. * Makefile.am (SUBDIRS): Add doc. * src/ltlparse/ltlscan.ll: Recognize && and ||. * src/ltltest/parse.test, src/ltltest/parseerr.test, src/ltltest/equals.test: Use these operators.. 2003-04-17 Alexandre Duret-Lutz * src/ltltest/readltl.cc, src/ltltest/equals.cc: Cosmetics. * src/ltlenv/environment.hh (require): Return a formula, not an atomic_prop. * src/ltlast/atomic_prop.hh (atomic_prop): New argument env. (environment_): New member. (env): New method. * src/ltlast/atomic_prop.cc (atomic_prop, env): Likewise. * src/ltlenv/defaultenv.cc (require): Pass *this as the environment argument to atomic_prop. * src/ltlvisit/clone.cc (visit(const atomic_prop*)): Also copy the environment. * src/ltlvisit/nenoform.cc (visit(const atomic_prop*)): Likewise. * configure.ac: Output src/ltlenv/Makefile. * src/ltlenv/Makefile.am, src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh: New files. * src/ltlparse/public.hh (parse): Take an environment as third argument. * src/ltlparse/ltlparse.yy (ATOMIC_PROP, parse): Require the atomic proposition via the environment. * src/ltltest/readltl.cc (main): Adjust the call to parse(). * src/ltltest/Makefile.am (LDADD): Add ../ltlenv/libltlenv.a. * src/ltlvisit/clone.hh, src/ltlvisit/clone.cc: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Inherit from clone_visitor and remove all useless methods (now inherited). * src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltltest/equals.cc (main) [NENOFORM]: Call negative_normal_form. * src/ltltest/nenoform.test, src/ltltest/tunenoform.test: New files. * src/ltltest/Makefile.am (check_PROGRAMS): Add nenoform and tunenoform. (nenoform_SOURCES, nenoform_CPPFLAGS, tunenoform_SOURCES, tunenoform_CPPFLAGS): New variables. (TESTS): Add nenoform.test and tunenoform.test. * src/ltlvisit/lunabbrev.hh: Fix include guard. 2003-04-16 Alexandre Duret-Lutz * src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltltest/tunabbrev.test: New file. * src/ltltest/lunabbrev.test: Fix comment. * src/ltltest/Makefile.am (TESTS): Add tunabbrev.test. (check_PROGRAMS): Add tunabbrev. (tunabbrev_SOURCES, tunabbrev_CPPFLAGS): New variables. * src/ltltest/equals.cc (main) [TUNABBREV]: Call unabbreviate_ltl. * src/ltlvisit/lunabbrev.hh (unabbreviate_logic_visitor::recurse): New virtual function. * src/ltlvisit/lunabbrev.cc (unabbreviate_logic_visitor::recurse): Likewise. (unabbreviate_logic_visitor::visit): Use it instead of calling unabbreviate_logic directly. * src/ltlvisit/lunabbrev.hh: Add missing include guard. * src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltlast/multop.cc (multop::multop(type)): New constructor. * src/ltlast/multop.hh (multop::multop(type)): New constructor. * src/ltltest/lunabbrev.test: New file. * src/ltltest/Makefile.am (TESTS): Add lunabbrev.test. (check_PROGRAMS): Add lunabbrev. (lunabbrev_SOURCES, lunabbrev_CPPFLAGS): New variables. * src/ltltest/equals.cc (main) [LUNABBREV]: Call unabbreviate_logic. * src/ltltest/equals.test (check0, check1): Remove. Use check 0, and check 1 instead. * src/ltlast/formulae.hh: Rename as ... * src/ltlast/formula.hh: ... this. * src/ltlast/Makefile.am (libltlast_a_SOURCES): Adjust. * src/ltlast/formula.hh (formulae): Rename as ... (formula): ... this. Adjust all uses. * src/ltlparse/public.hh (format_parse_errors): New function. * src/ltlparse/fmterror.cc: New file. * src/ltlparse/Makefile.am (libltlparse_a_SOURCES): Add fmterror.cc. * src/ltltests/equals.cc, src/ltltests/readltl.cc: Simplify using format_parse_errors. * src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add equals.hh and equals.cc. * src/ltltest/equals.cc, src/ltltest/equals.test: New files. * src/ltltest/Makefile.am (check_PROGRAMS): Add equals. (equals_SOURCES): New variable. (TESTS): Add equals.test. * src/ltlast/multop.cc (multop::multop): Use multop::add. (multop::add): If the formulae we add is itself a multop for the same operator, merge its children with ours. * src/ltltest/parseerr.test: Add two tests for multop merging. 2003-04-15 Alexandre Duret-Lutz * src/ltlast/formulae.hh (formulae::equals): Remove. * src/ltlast/unop.hh (unop::equals): Remove. * src/ltlast/unop.cc (unop::equals): Remove. * src/ltlast/binop.hh (binop::equals): Remove. * src/ltlast/binop.cc (binop::equals): Remove. * src/ltlast/multop.hh (multop::equals): Remove. * src/ltlast/multop.cc (multop::equals): Remove. * src/ltlast/atomic_prop.hh (atomic_prop::equals): Remove. * src/ltlast/atomic_prop.cc (atomic_prop::equals): Remove. * src/ltlast/constant.hh (constant::equals): Remove. * src/ltlast/constant.cc (constant::equals): Remove. * HACKING, Makefile.am, configure.ac, m4/gccwarn.m4, 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/formulae.hh, src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/predecl.hh, src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh, src/ltlparse/public.hh, src/ltlvisit/Makefile.am, src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh, src/ltlvisit/dump.cc, src/ltlvisit/dump.hh, src/ltlvisit/rewrite.cc, src/ltlvisit/rewrite.hh, src/ltltest/Makefile.am, src/ltltest/defs.in, src/ltltest/readltl.cc, src/ltltest/parse.test, src/ltltest/parseerr.test, src/misc/Makefile.am, src/misc/const_sel.hh: New files.