2011-08-28 Alexandre Duret-Lutz Fix errors reported by clang++-2.9. * src/evtgbaalgos/tgba2evtgba.cc (process_link): Fix prototype to match tgba_reachable_iterator::process_link. * src/ltlvisit/tunabbrev.hh: Add using super::visit, so that the other visit() method are in scope when we overload one. * src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc (start, end, process_link): Remove these empty methods. The default implementations are empty too, and process_link had the wrong prototype. * src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc (start, end, process_link): Likewise. 2011-08-27 Alexandre Duret-Lutz Improve SCC simplification by removing implied acceptance conditions. Spot 0.7.1 used to need 190 acceptance conditions to translate the 188 literature formulae. With this patch we are down to 185. That's not an impressive, but there are only ~20 formulae that require more than 1 acceptance conditions; hence little room for improvement. * src/misc/bddlt.hh (bdd_hash): New function. * src/misc/accconv.hh, src/misc/accconv.cc: New files. * src/misc/Makefile.am: Add them. * src/tgbaalgos/scc.cc (scc_map::build_map): Adjust to record all combination of acceptance conditions occurring in a SCC. * src/tgbaalgos/scc.hh (scc_map::scc::useful_acc): Update description. * src/tgbaalgos/sccfilter.cc (scc_filter): Simplify acceptance conditions that are always implied by another acceptance conditions. Previously, we only removed acceptance conditions that where always present in accepting SCCs. * src/tgbatest/sccsimpl.test: New file. * src/tgbatest/Makefile.am (TESTS): Add it. 2011-08-26 Alexandre Duret-Lutz Refine yesterday's change to the degeneralization. This avoids a small regression on the size of degeneralized automata of our usual list of literature formulae. * src/tgba/tgbatba.hh, src/tgba/tgbatba.cc (tgba_tba_proxy::union_acceptance_conditions_of_original_state): New method. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): In accepting states, ignore only the last expected acceptance condition if its common to all outgoing transitions AND if it is not used by any outgoing transitions of the destination. 2011-08-25 Alexandre Duret-Lutz Make sure the degeneralization is idempotent (up to renaming of states). * src/tgbaalgos/tgbatba.cc: When degeneralizing to SBA, remove the acceptance conditions that are common to all outgoing transitions of this state. This helps to make the degeneralization idempotent. * src/tgbatest/degenid.test: New test case. * src/tgbatest/Makefile.am: Add it. 2011-08-25 Alexandre Duret-Lutz Fix escaping of state name in save_reachable()'s output. * src/tgbaalgos/save.c (process_state): Escape quotes in the name of source and destination states. This fixes a side bug in the upcoming degenid.test test case. 2011-08-25 Alexandre Duret-Lutz Running `ltl2tgba -R1q -R1t -N` would degeneralize before and after the simulation-reduction. Report from Tomáš Babiak . * src/tgbaalgos/neverclaim.hh (never_claim_reachable): Take a tgba as input. * src/tgbaalgos/neverclaim.cc (never_claim_bfs): Call state_is_accepting() only if this tgba turns out to be a tgba_sba_proxy. Otherwise check the acceptance of one outgoing transition as we do in dotty_bfs since 2011-03-05. * src/tgbatest/ltl2tgba.cc: Do not redegeneralize before calling never_claim_reachable() if we know the automaton is degeneralized already. * src/tgbatest/ltl2tgba.test: Add a test case. 2011-08-17 Alexandre Duret-Lutz Please GCC 4.6. * src/tgbatest/complementation.cc (check, automaton): Remove these unused variables. 2011-08-17 Alexandre Duret-Lutz Fix a nondeterministic behavior of the degeneralization algorithm. Reported by Tomáš Babiak . * src/tgba/tgbatba.cc (tgba_tba_proxy): Replace the std::map used to record outgoing transitions by an Sgi::hash_map, and keep the order of these transitions in a separate list. * src/tgbatest/degendet.test: New file. * src/tgbatest/Makefile.am (TESTS): Add it. * THANKS: Add Tomáš and convert to utf8. 2011-08-17 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (syntax): -N implies -DS, not -D. 2011-07-26 Alexandre Duret-Lutz * iface/dve2/dve2check.cc: Add option -W and simplify formulae. 2011-07-26 Alexandre Duret-Lutz -e means we expect an accepting run. * iface/dve2/dve2check.cc: Reverse the value of expect_counter_example with respect to the -e/-E options. * iface/dve2/dve2check.test: Swap -e and -E. 2011-06-26 Alexandre Duret-Lutz Add some "drop shadow" in ltl2tgba.html. * wrap/python/ajax/ltl2tgba.html: Add shadow to all boxes. * wrap/python/ajax/css/ltl2tgba.css (.shadow): New class. 2011-06-25 Alexandre Duret-Lutz Revamp the ltl2tgba benchmark. * bench/ltl2tgba/algorithms: Reduce the number of Spot configuration tested. * bench/ltl2tgba/Makefile.am (run, small.txt, big.txt, known.txt): New rules. * bench/ltl2tgba/big, bench/ltl2tgba/small, bench/ltl2tgba/known: Add a 15min timeout to the lbtt configuration. * bench/ltl2tgba/defs.in: Adjust variable definitions to accept variable inderections. * bench/ltl2tgba/parseout.pl: Add an option to output the table in LaTeX. Also consider all formulae, not just the positive formulae. * bench/ltl2tgba/README: Update. 2011-06-16 Alexandre Duret-Lutz * src/ltlvisit/tostring.cc (to_spin_string_visitor): Add missing break. 2011-06-10 Alexandre Duret-Lutz * wrap/python/ajax/spot.in: Touch the directory containing the cached result for the requests. So that it survives the browser's cache. (finish): Prune the cache only once per hour, and only eraes files that are older than 2 hours. 2011-06-09 Alexandre Duret-Lutz * wrap/python/ajax/ltl2tgba.html: Add focus on the formula field on page load. 2011-06-08 Alexandre Duret-Lutz * NEWS: Update with recent changes. 2011-06-08 Alexandre Duret-Lutz Implement cache pruning in the CGI script. * wrap/python/ajax/spot.in (finish): Prune the cache once in a while. We rely on hardlinks for garbage collecting the pictures and dot sources that may be shared by different requests. 2011-06-08 Alexandre Duret-Lutz Cache dot sources in the CGI script. * wrap/python/ajax/spot.in (render_dot, render_dot_maybe) (render_automaton, render_formula): Cache the dot source, so that we do not have to regenerate two pictures from the same contents. * wrap/python/spot.i: Typo in the ostringstream declaration. 2011-06-08 Alexandre Duret-Lutz Output a "Cache-Control:" header in the CGI script. * wrap/python/ajax/spot.in: Output a cache-control header, so that browsers do no even send two identical requests. 2011-06-08 Alexandre Duret-Lutz Cache results of the spot.py CGI script. * wrap/python/ajax/spot.in: Use the QUERY_STRING as a hash key to cache the result of the script. Open stdout without buffering and redirect it to a file that we can dump later on cache hits. Parts of this change are extracted from code from Pierre Parutto . * AUTHORS: Add him. 2011-06-07 Alexandre Duret-Lutz * src/ltltest/genltl.cc (X_n): Fix assertion. 2011-06-06 Alexandre Duret-Lutz * src/ltlvisit/dotty.cc (dotty_visitor): Reorder attributes. 2011-06-06 Alexandre Duret-Lutz * src/ltltest/genltl.cc (fair_response): Typo. 2011-06-06 Alexandre Duret-Lutz DVE2: Do not display state variables with only one possible value. * iface/dve2/dve2.cc (dve2_kripke::dve2_kripke): Fill a format_filter_ array with boolean indicating whether each variable should be printed. Ignore variable with only one possible value. (dve2_kripke::~dve2_kripke): Destroy it. (dve2_kripke::format_state): Use it. * iface/dve2/finite.test: Adjust. 2011-06-06 Alexandre Duret-Lutz Remove Kristin Rozier's LTLcounter.pl scripts, now that we can generate these formulae with "genltl". * src/tgbatest/ltlcounter/: Remove this directory. * src/tgbatest/Makefile.am: Adjust. * src/tgbatest/ltlcounter.test, bench/ltlcounter/run: Use genltl to generate the formulae. * bench/ltlcounter/README: Do not mention src/tgbatest/ltlcounter/ anymore. 2011-06-06 Alexandre Duret-Lutz Better layout of the LTL formula parse tree. * src/ltlvisit/dotty.cc: Display "L" and "R" tail-labels for binary operators. Gather all constants and atomic propositions in a sub-graph with "rank=sink". 2011-06-06 Alexandre Duret-Lutz Add more formula families to genltl. * src/ltltest/genltl.cc (fair_response, ltl_counter) (ltl_counter_carry): New functions, constructing function from gastin.03.cav and rozier.07.cav. The LTL counter will replace the scripts in src/tgbatest/ltlcounter/. (X_n): New helper function. 2011-06-03 Alexandre Duret-Lutz Install a misc/_config.h to hide all the defines that clutter the built output. This is also a step towards better checks for things like __attribute__ or std::tr1. * m4/ax_prefix_config_h.m4: New file. * configure.ac: Call AC_CONFIG_HEADERS and AX_PREFIX_CONFIG_H. * src/misc/Makefile.am: Install misc/_config.h. * src/misc/random.cc, src/misc/version.cc: Include misc/_config.h. 2011-06-03 Alexandre Duret-Lutz Document the protocol used between ltl2tgba.html and spot.py. * wrap/python/ajax/protocol.txt: New file. * wrap/python/ajax/Makefile.am (EXTRA_DIST): Add it. 2011-06-02 Alexandre Duret-Lutz * iface/dve2/README: Document state compression. 2011-06-02 Alexandre Duret-Lutz Update jQuery and jQuery-UI. * wrap/python/ajax/ltl2tgba.html: Adjust to use jQuery 1.6.1 and jQuery-UI 1.8.13. Remove a useless check of $("#autoupdate").attr("checked") since this checkbox no longer exists. * wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.8.custom.css: Replace by ... * wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.13.custom.css: This. * wrap/python/ajax/Makefile.am (EXTRA_DIST): Adjust. 2011-05-30 Alexandre Duret-Lutz * iface/dve2/dve2.cc: Kill a spurious warning. 2011-05-30 Alexandre Duret-Lutz * bench/wdba/README: Typos. 2011-05-18 Alexandre Duret-Lutz Some intvcomp2 speedups. * src/misc/intvcmp2.cc (stream_compression_base::run): Implement a shift-less encoding for the 1-bit and 3-bit cases. Also declare offsets as size_t, to help 64-bit compilers. 2011-05-16 Alexandre Duret-Lutz * src/misc/intvcomp.hh, src/misc/intvcmp2.hh: Include stddef.h for size_t. 2011-05-05 Alexandre Duret-Lutz * src/misc/intvcmp2.cc: Cosmetics to please sanity checks. 2011-05-05 Alexandre Duret-Lutz Fix compilation error with g++ <= 4.3. * src/misc/intvcmp2.cc (int_array_array_compression): Specify full type of stream_compression_base in constructor to please g++ versions <= 4.3. 2011-05-02 Alexandre Duret-Lutz DVE2: Minor memory compaction. * iface/dve2/dve2.cc (dve2_state, dve2_compressed_state): Store size and count on 16 bits, and hash on 32 bits, to limit memory wasted. 2011-05-01 Alexandre Duret-Lutz DVE2: Optionally use the new compression. * iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc: Add a -Z option and pass it through. 2011-05-01 Alexandre Duret-Lutz Implement a new compression inspired from simple-9. * src/misc/intvcmp2.cc, src/misc/intvcmp2.hh: New files. * src/misc/Makefile.am: Add them. * src/tgbatest/intvcmp2.cc: New test. * src/tgbatest/Makefile.am: Add it. * src/tgbatest/intvcomp.test: Call it. 2011-04-15 Alexandre Duret-Lutz * src/misc/intvcomp.cc: Low-level fine-tuning. 2011-04-13 Alexandre Duret-Lutz Fix compression of large repetitions * src/misc/intvcomp.cc (stream_compression_base::run): Limit repeatitions to 40, not 42. (stream_decompression_base::refill): Refill the end of the stream with 0. (stream_decompression_base::look_n_bits): Add assertion. * src/tgbatest/intvcomp.cc: Add a new test case. 2011-04-12 Alexandre Duret-Lutz More interfaces to the int array compression routines. * src/misc/intvcomp.cc, src/misc/intvcomp.cc: Add interfaces to compress vector to vector. * src/tgbatest/intvcomp.cc: Test them. * src/sanity/style.test: Refine check to avoid a spurious report. 2011-04-11 Alexandre Duret-Lutz * iface/dve2/dve2.cc: Typo when handling dead==true. 2011-04-10 Alexandre Duret-Lutz Always pass --enable-devel or --disable-devel to BuDDy. * configure.ac: Do not add CXXFLAGS and CFLAGS in ac_configure_args, it causes problem when using config.cache. Instead ... * m4/devel.m4: Add --enable-devel or --disable-devel on ac_configure_args, now that BuDDy understands that. 2011-04-10 Alexandre Duret-Lutz * src/misc/escape.hh: Fix Doxygen documentation. * src/misc/intvcomp.hh: Likewise. 2011-04-09 Alexandre Duret-Lutz Move the compression routines into their own *.cc file. * src/misc/intvcomp.hh: Move all code... * src/misc/intvcomp.cc: ... in this new file. * src/misc/Makefile.am: Add invcomp.cc 2011-04-09 Alexandre Duret-Lutz DVE2: Use mspool for compressed states. * iface/dve2/dve2.cc: Adjust to use the new mspool allocator, and get rid of the std::vector used to store compressed states. * src/misc/intvcomp.hh: Add an "int* -> int*" interface in addition to the "int* -> vector*" interface. * src/tgbatest/intvcomp.cc: Test the two interfaces. 2011-04-09 Alexandre Duret-Lutz Add a multiple-size memory pool implementation. * src/misc/mspool.hh: New file. * src/misc/Makefile.am: Add it. 2011-04-08 Alexandre Duret-Lutz * src/misc/fixpool.hh: Typo in comment. 2011-04-08 Alexandre Duret-Lutz DVE2: preliminary implementation of compressed states. * iface/dve2/dve2.cc (dve2_compressed_state): New class. (callback_context): Deal with general state*s, not dve2_state*s. (transition_callback_compress): New function. (dve2_kripke): Take a compress option. (get_init_state, compute_state_condition, succ_iter, format_state, state_condition): Handle compressed states. (get_vars, compute_state_condition_aux): New helper methods. * iface/dve2/dve2.hh (load_dve2): Add a compress option. * iface/dve2/dve2check.cc: Add a -z option. * iface/dve2/finite.test, iface/dve2/dve2check.test: Add more tests. 2011-04-08 Alexandre Duret-Lutz Preliminary implementation of an int array compressor. * src/misc/intvcomp.hh: New file. * src/misc/Makefile.am: Add it. * src/tgbatest/intvcomp.cc, src/tgbatest/intvcomp.test: New files. * src/tgbatest/Makefile.am: Add them. 2011-04-09 Alexandre Duret-Lutz Fix two spurious segfaults in test cases for the Python interface. * wrap/python/tests/setxor.py, wrap/python/tests/bddnqueen.py: Clean all used bdd variables before calling bdd_done(), so that bdd_delref() is never called after bdd_done(). In NDEBUG builds, bdd_delref() does not check whether the BuDDy is running or not, and calling it after bdd_done() will crash. 2011-04-09 Alexandre Duret-Lutz * HACKING: Add an example for using callgrind. 2011-04-06 Alexandre Duret-Lutz * iface/dve2/dve2check.cc (main): Catch out-of-memory errors during emptiness check or counterexample generation. 2011-04-03 Alexandre Duret-Lutz * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc: Use a fixed-size memory pool for product_state instances. 2011-04-03 Alexandre Duret-Lutz * iface/dve2/dve2.cc: Use a fixed-size memory pool for dve2_state instances and their variables. 2011-04-03 Alexandre Duret-Lutz Add a fixed-size memory pool implementation. * src/misc/fixpool.hh: New file. * src/misc/Makefile.am (misc_HEADERS): Add fixpool.hh. 2011-04-03 Alexandre Duret-Lutz * HACKING (command): Some notes about link-time optimizations. 2011-04-03 Alexandre Duret-Lutz * configure.ac: Pass CXXFLAGS/CFLAGS/CPPFLAGS debug/optimization settings to sub configure. 2011-03-31 Alexandre Duret-Lutz Introduct a down_cast macro. * src/misc/casts.hh: New file. * src/misc/Makefile.am: Add it. * iface/dve2/dve2.cc, iface/gspn/gspn.cc, iface/gspn/ssp.cc, src/evtgba/explicit.cc, src/evtgba/product.cc, src/misc/casts.hh, src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgbabddconcrete.cc, src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh, src/tgba/tgbakvcomplement.cc, src/tgba/tgbaproduct.cc, src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc, src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc, src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim_del.cc: Use down_cast when appropriate. 2011-03-31 Alexandre Duret-Lutz Cosmetics. * src/sanity/style.test: Catch some binary operators not delimited with spaces. * src/tgbaalgos/bfssteps.cc, src/tgbaalgos/magic.cc, src/tgbaalgos/reducerun.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Fix these. 2011-03-31 Alexandre Duret-Lutz Make state_explicit instances persistent objects. * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Merge state_explicit and tgba_explicit::state. In the past, state_explicit was a small object encapsulating a pointer to the persistent tgba_explicit::state; and we used to clone() and destroy() a lot of state_explicit instance. Now state_explicit is persistent, and clone() and destroy() have no effects. * src/tgba/tgbareduce.cc: Adjust, since this inherits from tgbaexplicit and uses the internals of state_explicit. * src/tgbatest/reductgba.cc: Fix deletion order for automata. * src/tgba/tgba.hh (last_support_conditions_input_, last_support_variables_input_): Make these protected, so they can be zeroed by tgba_explicit. 2011-03-30 Alexandre Duret-Lutz Remove tgba_reduc::format_state(). * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh (format_state): Remove this useless copy of the tgba_explicit_string::format_state method. 2011-03-30 Alexandre Duret-Lutz Protect the state destructor. Client code should always call the destroy() method instead. (It was introduced in Spot 0.7.) * src/tgba/state.hh (state::~state): Make it protected. 2011-03-30 Alexandre Duret-Lutz Speedup tgba_product when one of the argument is a Kripke structure. The gain is not very impressive. The runtime of the first example in iface/dve2/README (also in dve2check.test) is 15% faster. * src/tgba/tgbaproduct.hh (tgba_succ_iterator_product): Move ... * src/tgba/tgbaproduct.cc (tgba_succ_iterator_product, tgba_succ_iterator_product_common): ... in these two classes. (tgba_succ_iterator_product_kripke): New class to speedup successor computation on Kripke structures. We can assume that all the transitions leaving the same state have the same label. (tgba_product::tgba_product, tgba_product::succ_iter): Use tgba_succ_iterator_product_kripke when appropriate. (tgba_product_init::tgba_product_init): Adjust for the case where tgba_product did reverse its operands. 2011-03-30 Alexandre Duret-Lutz * iface/dve2/dve2check.cc: Remove stray debug output. 2011-03-30 Alexandre Duret-Lutz * src/tgba/tgbaproduct.hh: Do not include statebdd.hh. 2011-03-29 Alexandre Duret-Lutz Include in python modules to workaround Swig bug. * wrap/python/spot.i, wrap/python/buddy.i: Include because Swig 2.0.2 uses ptrdiff_t and does not do the include itself. In g++ most libstdc++ standard headers have been changed to no longer include as an implementation detail, so the difference shows. 2011-03-20 Alexandre Duret-Lutz * THANKS: Add Michael Weber for his help on the DiVinE interface. 2011-03-18 Alexandre Duret-Lutz * src/ltltest/genltl.cc (syntax): Typos in the help text. 2011-03-17 Alexandre Duret-Lutz Improve a reduction rule for "a M b". * src/ltlvisit/reduce.cc (reduce_visitor): Always reduce "a M b" to "a & b" if "a" is a pure eventual formula, remove the constraint on "b". * src/ltltest/reduccmp.test: Add two tests. 2011-03-11 Alexandre Duret-Lutz * NEWS: Mention recent changes to dotty_reachable. 2011-03-10 Alexandre Duret-Lutz Add support for finite behaviors in the DVE interface. * iface/dve2/dve2.hh (load_dve2): Take a "dead" argument. * iface/dve2/dve2.cc (callback_context): Add a destructor to simplify... (dve2_succ_iterator::~dve2_succ_iterator) ... this one. (convert_aps): Skip the dead proposition. (dve2_kripke::dve2_kripke): Take a dead argument, and setup alive_prop and dead_prop. (compute_state_condition, get_succ): Use a cache for the conditions and successor of the last state, to share some work between these two function. Add loops on dead states. (load_dve2): Pass dead to dve2_kripke and convert_aps. * iface/dve2/dve2check.cc: Add a -dDEAD option. * iface/dve2/finite.test, iface/dve2/finite.dve: New file. * iface/dve2/Makefile.am: Declare them. 2011-03-10 Alexandre Duret-Lutz * iface/dve2/dve2.cc (convert_aps): Fix two typos while parsing >= and >, mistakenly registered as <= and <. 2011-03-07 Alexandre Duret-Lutz Remove the Nips interface. * NEWS: Mention it. * configure.ac, README: Remove it. * iface/Makefile.am (SUBDIRS): Remove nips. * iface/nips/: Delete this directory. 2011-03-07 Alexandre Duret-Lutz Accept "P_0 == CS" as synonym for "P_0.CS" in the dve2 interface. Suggested by Yann Thierry-Mieg. * iface/dve2/dve2.cc (convert_aps): Allow string on the right of operators, and look them up. * iface/dve2/dve2check.test: Test this syntax. 2011-03-07 Alexandre Duret-Lutz Add some tests for the DVE2 interface. * iface/dve2/defs.in, iface/dve2/dve2check.test, iface/dve2/beem-peterson.4.dve: New files. * iface/dve2/Makefile.am: Add them. * configure.ac: Generate iface/dve2/defs. 2011-03-07 Alexandre Duret-Lutz Clear the timer map to help valgrind. * src/misc/timer.hh (reset_all): New method. * iface/dve2/dve2check.cc: Use it to help valgrind. 2011-03-07 Alexandre Duret-Lutz Some documentation of about the dve2 interface. * iface/dve2/README: New file. * NEWS: Mention it. 2011-03-06 Alexandre Duret-Lutz * iface/dve2/dve2.cc, iface/dve2/dve2check.cc: Cosmetic changes to please sanity checks. 2011-03-06 Alexandre Duret-Lutz Call divine to compile dve models. * iface/dve2/dve2.cc (compile_dve2): New function. Compile the *.dve source if there is no newer *.dve2C already. (load_dve2): Call compile_dve2 when given a *.dve file. * iface/dve2/dve2.hh (load_dve2): Document it. 2011-03-06 Alexandre Duret-Lutz Allow atomic propositions and identifiers like `X.Y'. * src/ltlparse/ltlscan.ll: Do not recognize `.' as an AND. Allow it in atomic propositions. * src/evtgbaparse/evtgbascan.ll, src/tgbaparse/tgbascan.ll: Accept `.' in identifiers. * src/misc/bareword.cc (is_bareword): Accept `.' inside barewords, so that there is no need to quote `X.Y'. * src/ltltest/parse.test: Do not use `.' as and operator.. 2011-03-06 Alexandre Duret-Lutz Augment dve2check to perform LTL model checking. * iface/dve2/dve2check.cc: Add many option to perform emptiness check and other debugging tasks. 2011-03-05 Alexandre Duret-Lutz Teach the DVE2 interface about enumerated types. * iface/dve2/dve2.cc (convert_aps): Add support for enumerated types. E.g. an atomic proposition such as "P_0.CS" really means "P_0 == CS". 2011-03-05 Alexandre Duret-Lutz Teach the DVE2 interface about atomic propositions such as "a <= 10" or "b != 3". This only work for integer variables presently. * iface/dve2/dve2.hh (load_dve2): Take an atomic_prop_set argument to indicate the AP to observe. * iface/dve2/dve2.cc (convert_aps): New function. Parse the atomic propositions in format them in a prop_set structure that will allow fast generation of the state condition. (load_dve2): Call convert_aps, and pass the resulting prop_set structure to the kripke object. (dve2_kripke::dve2_kripke): Store the prop_set structure. (dve2_kripke::~dve2_kripke): Release the prop_set, and unregister the bdd_variable associated to it. (compute_state_condition): New method that uses the prop_set. (succ_iter, state_condition): Call compute_state_condition(). * iface/dve2/dve2check.cc: Adjust the call to load_dve2 to pass it atomic propositions read from the command line. 2011-03-05 Alexandre Duret-Lutz Display states variables in the state label. * iface/dve2/dve2.cc (dve2_kripke::dve2_kripke): Retrieve the name of all the state variables. (dve2_kripke::format_state): Use them to format the name of the state. 2011-03-05 Alexandre Duret-Lutz We can now explore a divine2 compiled model, but the atomic properties are still missing. * iface/dve2/dve2.cc, iface/dve2/dve2.hh: Add classes for presenting the DiVinE2 model as a kripke object. (load_dve2): Load the *.dve2C file using libltdl. * iface/dve2/Makefile.am: Add a dve2check program. * iface/dve2/dve2check.cc: New file. Currently it just outputs the reachability graph using dotty. 2011-03-05 Alexandre Duret-Lutz Setup libltdl in ltdl/, so we can use it in the dve2 interface. Don't keep it under version control since it is installed by autoreconf. * configure.ac: Call LT_CONFIG_LTDL_DIR and LTDL_INIT. * README: Mention ltdl/. * Makefile.am: Recurse into ldtl. * iface/dve2/Makefile.am: Link with it. 2011-03-05 Alexandre Duret-Lutz Setup build system for a new dve2 interface. * iface/dve2/dve2.cc, iface/dve2/dve2.hh: New dummy files. * iface/dve2/Makefile.am: New file. * iface/Makefile.am (SUBDIRS): Add dve2. * configure.ac: Build iface/dve2/Makefile. * README: Mention the new directory. 2011-03-05 Alexandre Duret-Lutz Using double borders for acceptance states in SBAs. * src/tgbaalgos/dotty.hh (dotty_reachable): Take a new assume_sba argument. * src/tgbaalgos/dotty.cc (dotty_bfs): Take a new mark_accepting_states arguments. (dotty_bfs::process_state): Check if a state is accepting using the state_is_accepting() method for tgba_sba_proxies, or by looking at the first outgoing transition of the state. Pass the result to the dectorator. (dotty_reachable): Adjust function. * src/tgbaalgos/dottydec.hh, src/tgbaalgos/dottydec.cc, src/tgbaalgos/rundotdec.hh, src/tgbaalgos/rundotdec.cc (state_decl): Add an "accepting" argument, and use it to decorate accepting states with a double border. * src/tgbatest/ltl2tgba.cc: Keep track of whether the output is an SBA or not, so that we can tell it to dotty(). * wrap/python/ajax/spot.in: Likewise. * wrap/python/cgi-bin/ltl2tgba.in: Likewise. 2011-03-05 Alexandre Duret-Lutz * src/ltltest/genltl.cc (GF_n): Really use "op". 2011-03-04 Alexandre Duret-Lutz * wrap/python/ajax/spot.in: Use the degeneralized automaton if available while computing the emptiness check. 2011-03-04 Alexandre Duret-Lutz Speedup build_result() called by minimize_dfa(). * src/tgbaalgos/minimize.cc (build_result): Speed it up by removing one useless loop, creating many duplicate transitions that had to be merged. 2011-03-01 Alexandre Duret-Lutz * src/ltltest/genltl.cc: Add 10 more LTL formula classes. 2011-02-21 Alexandre Duret-Lutz * src/tgba/bdddict.hh: Add more documentation. 2011-02-21 Alexandre Duret-Lutz * src/misc/escape.hh: Correct documentation. 2011-02-14 Alexandre Duret-Lutz Correct tgba_explicit::compute_support_conditions. * src/tgba/tgbaexplicit.cc (tgba_explicit::compute_support_conditions): Fix logic. This function has always been returning bddtrue instead of the actual computed value... 2011-02-10 Alexandre Duret-Lutz Enable VERBOSE logs for nips, greatspn, and python tests. * wrap/python/tests/run.in, iface/nips/nipstest/defs.in, iface/gspn/defs.in: Do not disable VERBOSE when running from "make check". Since we have started using parallel-check on 2009-08-31, we should always send verbose output to the log. 2011-02-10 Alexandre Duret-Lutz This should finally fix kv.test and dotty.test on the LIP6 buildfarm. * src/tgbatest/kv.test, iface/nips/nipstest/dotty.test: Don't rely on the ${DOT-...} syntax, because DOT is always set and might be set to the empty value. 2011-02-10 Alexandre Duret-Lutz * HACKING (Running coverage tests): New section. 2011-02-09 Alexandre Duret-Lutz Previous patch did not work on MacOS X, and I don't have shell access to that host. * src/tgbatest/kv.test: Use ${DOT-true} instead of ${DOT-:}. I don't know, the MacOS shell must be mixing the syntaxes for ${DOT:-} and ${DOT-:}. * iface/nips/nipstest/dotty.test: Likewise 2011-02-09 Alexandre Duret-Lutz Avoid running "dot" when it is not installed... * src/tgbatest/kv.test: Do not run dot if it is not installed. * iface/nips/nipstest/dotty.test: Likewise 2011-02-08 Alexandre Duret-Lutz Add some tricks into HACKING. * README: Typo. * HACKING: s/CVS/GIT/ and add some tricks about libtool and doxygen. 2011-02-08 Alexandre Duret-Lutz Adjust the WDBA test to count for sub-transitions. * bench/wdba/run: Use -kt to count sub-transitions. * bench/wdba/README: Adjust comments. 2011-02-08 Alexandre Duret-Lutz Fix a spurious g++ warning observed on Darwin builds. * src/tgba/taatgba.cc (taa_succ_iterator::taa_succ_iterator): Initialize iterator i to silence a spurious g++ warning on Darwin. 2011-02-07 Alexandre Duret-Lutz * configure.ac: s/gnit/gnu so that we can use 0.7.1a as a version. 2011-02-07 Alexandre Duret-Lutz * NEWS: Typos. 2011-02-07 Alexandre Duret-Lutz * NEWS, configure.ac: Bump version to 0.7.1a 2011-02-07 Alexandre Duret-Lutz Release Spot 0.7.1. * NEWS: Update for 0.7.1. * configure.ac: Bump version to 0.7.1. 2011-02-07 Alexandre Duret-Lutz Generalize patch from 2011-02-03 by allowing guards like "! (...)". * src/neverparse/neverclaimscan.ll: Allow space between ! and (. * src/tgbatest/neverclaimread.test: Add space for testing. 2011-02-06 Alexandre Duret-Lutz Speedup scc_filter on tgba_explicit_number automata. * src/tgbaalgos/sccfilter.cc (scc_filter): If the input automaton is an instance of tgba_explicit_number, create a similar automaton for output, instead of a tgba_explicit_string. 2011-02-06 Alexandre Duret-Lutz Document the new operators in the on-line tools. * wrap/python/ajax/ltl2tgba.html: Mention Goal's ~, -->, and <--> operators. * wrap/python/cgi-bin/ltl2tgba.in: Likewise. 2011-02-06 Alexandre Duret-Lutz Fix a segfault in WDBA minimization. * src/tgbaalgos/minimize.cc (build_result, minimize_dfa, minimize_wdba): Correctly handle (i.e. ignore) useless states. * src/tgbatest/ltl2tgba.test: Add two more tests. 2011-02-05 Alexandre Duret-Lutz Fix call to scc_filter in the CGI script. * wrap/python/ajax/spot.in: Do full scc_filter for TGBA (-R3f), and keep some extra acceptance conditions (-R3) when degeneralizing. The converse was done. 2011-02-04 Alexandre Duret-Lutz * wrap/python/cgi-bin/ltl2tgba.in: Fix python error occurring only when the user did not make any error... 2011-02-04 Alexandre Duret-Lutz Prevent Spot from using an installed BuDDy version that does not have the latest function we added. Reported by Kristin Rozier. * m4/buddy.m4 (AX_CHECK_BUDDY): Check for bdd_setxor. 2011-02-04 Alexandre Duret-Lutz Add a way to count the number of sub-transitions. * src/tgbaalgos/stats.hh (tgba_sub_statistics): New class. (sub_stats_reachable): New function. * src/tgbaalgos/stats.cc (sub_stats_bfs): New class. (tgba_sub_statistics::dump, sub_stats_reachable): New function. * src/tgbatest/ltl2tgba.cc (-kt): New option. * src/tgbatest/ltl2tgba.test: Use -kt. 2011-02-03 Alexandre Duret-Lutz Read guard of the form !(x) in neverclaims. So far all neverclaims encountered would use (!(x)), but the files from the Büchi store do not. * src/neverparse/neverclaimscan.ll: Accept ! in front of guard, so that we can read Promela files from Goal's Büchi store. * src/tgbatest/neverclaimread.test: Test it. 2011-02-03 Alexandre Duret-Lutz Recognize Goal's syntax for Boolean operators. * src/ltlparse/ltlscan.ll: Recognize ~, -->, and <--> operators from Goal, to ease the use of formulas provided by the Goal team. * src/ltltest/equals.test: Use these once, just to be on the safe side. 2011-02-03 Alexandre Duret-Lutz Minor fixes to ltl2tgba.html. * wrap/python/ajax/css/ltl2tgba.css, wrap/python/ajax/ltl2tgba.html: Tweak a few things for Firefox 3.0, and fix a tag. 2011-02-01 Alexandre Duret-Lutz * NEWS, configure.ac: Bump version to 0.7a. 2011-02-01 Alexandre Duret-Lutz Release Spot 0.7. * NEWS, configure.ac: Bump version to 0.7. 2011-02-01 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.test: Fix previous test case. 2011-01-28 Alexandre Duret-Lutz Fixup minimize_monitor(). * src/tgbaalgos/minimize.cc (minimize_monitor): Fix typo yielding incorrect monitor if the input tgba is not deterministic. * src/tgbatest/ltl2tgba.test: Add test case. 2011-01-27 Alexandre Duret-Lutz Report formulas that are both safety and guarantee. * src/tgbatest/ltl2tgba.cc (-O): Report formulas that are both safety and guarantee. * src/tgbatest/obligation.test: Add cases. 2011-01-27 Alexandre Duret-Lutz Rename is_safety_automaton() as is_guarantee_automaton() and implement is_safety_mwdba(). Note: I swapped the name of safety and guarantee when I implemented is_safety_automaton() on 2010-03-20. Fortunately, is_safety_automaton() was only used where is_guarantee_automaton() would have been correct. * src/tgbaalgos/safety.cc (is_guarantee_automaton): Rename as ... (is_guarantee_automaton): ... this. (is_safety_mwdba): New function. * src/tgbaalgos/safety.hh: Adjust and add documentation. * src/tgbaalgos/minimize.cc: Use is_guarantee_automaton() instead of is_safety_automaton(). * src/tgbatests/safety.test: Rename as ... * src/tgbatests/obligation.test: ... this, and augment the test. * src/tgbatest/Makefile.am: Adjust. * src/tgbatest/ltl2tgba.cc (-O): Display whether a formula represent a safety, guarantee, or obligation property. * NEWS: Adjust. 2011-01-27 Alexandre Duret-Lutz * NEWS: Minor rewritings. 2011-01-27 Alexandre Duret-Lutz Replace delete by destroy in comments dealing with states. * src/tgba/succiter.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbaunion.hh, src/tgbaalgos/bfssteps.hh, src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/explscc.hh, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/replayrun.cc, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh: Update comments to say that we "destroy" a state instead of "deleting" it. 2011-01-26 Alexandre Duret-Lutz Update gspn interface for recent tools. * iface/gspn/ssp.cc: Use the new destroy() interface, and fix a couple of recent g++ reports. * iface/gspn/gspn.cc: Adjust to newer g++. 2011-01-25 Alexandre Duret-Lutz Introduce a destroy() method on states, and use it instead of delete. Right now, destroy() just executes "delete this". But in a later version, we will rewrite tgba_explicit so that it does not allocate new states (and the destroy() method for explicit state will do nothing). * src/tgba/state.hh (state::destroy): New method, to replace state::~state() in the future. (shared_state_deleter): New function. * src/evtgba/product.cc, src/evtgbaalgos/reachiter.cc, src/evtgbaalgos/save.cc, src/evtgbaalgos/tgba2evtgba.cc, src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgba/tgbareduc.cc, src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc, src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc, src/tgbaalgos/cutscc.cc, src/tgbaalgos/emptiness.cc, src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gv04.cc, src/tgbaalgos/magic.cc, src/tgbaalgos/minimize.cc, src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/powerset.hh, src/tgbaalgos/reachiter.cc, src/tgbaalgos/reducerun.cc, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/replayrun.cc, src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc, src/tgbaalgos/scc.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Adjust to call "s->destroy()" instead of "delete s". * src/saba/sabacomplementtgba.cc, src/tgba/tgbakvcomplement.cc: Pass shared_state_deleter to the shared_ptr constructor, so that it calls destroy() instead of delete. 2011-01-26 Alexandre Duret-Lutz * wrap/python/ajax/ltl2tgba.html: Display the Spot version in the tooltip over the Spot logo. 2011-01-26 Alexandre Duret-Lutz * wrap/python/ajax/Makefile.am (EXTRA_DIST): Add icons/mail.png. 2011-01-26 Alexandre Duret-Lutz * NEWS: Mention the new on-line ltl2tgba version. 2011-01-26 Alexandre Duret-Lutz Updates to the ltl2tgba ajax version. * wrap/python/ajax/ltl2tgba.html: Remove the auto-update button, and enable auto-update automatically after the first submission. Add tools tips for the "Desired Output" tabs, and the Spot logo. Add a email icon to encourage feedback. * wrap/python/ajax/ltl2tgba.css: fix sizes of formula field and send button. Set position of mail icon. * wrap/python/ajax/logos/mail.png: New logo, based on a public domain SVG icon retrieved today from http://commons.wikimedia.org/wiki/File:Internet-mail.svg 2011-01-19 Alexandre Duret-Lutz * wrap/python/ajax/ltl2tgba.html: Disable the browser spellcheck on the input box. 2011-01-18 Alexandre Duret-Lutz Preliminary implementation of an ajax-based ltl2tgba translator. * configure.ac: Output wrap/python/ajax/Makefile. * wrap/python/Makefile.am (SUBDIRS): Add ajax. * wrap/python/ajax/Makefile.am, wrap/python/ajax/README, wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/spot.in: New files. * wrap/python/ajax/css/, wrap/python/ajax/js, wrap/python/ajax/logos: New directories. * README: Document wrap/python/ajax/. 2011-01-17 Alexandre Duret-Lutz Do not output empty parse error blocks in the CGI script. * wrap/python/spot.i: Provide a __nonzero__() method for parse_error_list. * wrap/python/cgi-bin/ltl2tgba.in: Do not call format_parse_errors() unconditionally. 2011-01-12 Alexandre Duret-Lutz Fix "unused function" warnings reported by clang++. * src/evtgbaparse/Makefile.am, src/ltlparse/Makefile.am, src/neverparse/Makefile.am, src/tgbaparse/Makefile.am (AM_CPPFLAGS): Define -DYY_NO_INPUT so that the unused yyinput() function does not get compiled. * src/eltlparse/Makefile.am (AM_CPPFLAGS): Likewise. (AM_CXXFLAGS): Also enable warnings. * src/eltlparse/eltlparse.yy: Move helper functions from the "%code requires" block to the "%code" block, so that they do not appear in the eltlparse.hh file (which is included in two places...). * iface/nips/nips.cc (search_error_callback_assert): Comment this unused function. 2011-01-12 Alexandre Duret-Lutz Fix segfault with g++-3.3. * src/tgbaalgos/minimize.cc (minimize_dfa): Fix deletion of the state_set_map. It led to a crash when compiled with g++-3.3. 2011-01-12 Alexandre Duret-Lutz Fix a compilation failure with g++-3.3. * src/misc/hash.hh (identity_hash): New function. * src/tgba/tgbaexplicit.hh (tgba_explicit_number): Use identity_hash instead of std::tr1::hash that does not exist with g++-3.3. 2011-01-07 Alexandre Duret-Lutz Fix usage of minimize_obligation in the CGI script. * wrap/python/cgi-bin/ltl2tgba.py (reduce_wdba): Use minimize_obligation_new a pass the formula. * wrap/python/spot.i (minimize_obligation_new): New function, to cope with the strange specification of spot::minimize_obligation() not always creating a new automaton. 2011-01-06 Alexandre Duret-Lutz * NEWS: Convert to utf-8 and fix a few typos. 2011-01-06 Alexandre Duret-Lutz '([]a && XXXX!a)' was not properly minimized because its translation contain useless SCCs that where not ignored for minimization. * src/tgbaalgos/minimize.cc (minimize_wdba): Strip useless SCCs before minimization. * src/tgbatest/ltl2tgba.test: Add a check. 2011-01-06 Alexandre Duret-Lutz The neverclaim output by spin -f '([]a && XXXX!a)' was not understood by Spot. * src/neverparse/neverclaimparse.yy: Support "if :: false fi;" instructions. Spin sometimes output these on dead states. Also rewrite the "transitions" rule as a left recursion. * src/tgbatest/neverclaimread.test: Adjust output because of the right->left recursion change, and add two more formula to submit to Spin to test its output. 2011-01-06 Alexandre Duret-Lutz Speed up computation of non_final states for minimize_wdba. * src/tgbaalgos/minimize.cc (minimize_dfa): Take final and non_final sets. (minimize_wdba): Fill in non_final at the same time as final. (minimize_monitor): Call state_set() to fill non_final. (init_sets): Simplify and rename as ... (state_set): ... this. 2011-01-06 Alexandre Duret-Lutz Introduce a class to complement a WDBA on-the-fly. * src/tgba/wdbacomp.hh, src/tgba/wdbacomp.cc: New file. * src/tgba/Makefile.am: Add them. * src/tgbaalgos/minimize.cc (minimize_obligation): Use wdba_complement(). 2011-01-05 Alexandre Duret-Lutz * src/tgbatest/Makefile.am: Remove the unused minimize program. * src/tgbatest/minimize.cc: Delete. 2011-01-05 Alexandre Duret-Lutz Cleanup the minimize.hh interface. * src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc (minimize): Split into ... (minimize_wdba, minimize_monitor): ... these two functions. * src/tgbatest/ltl2tgba.cc (main): Adjust the call to minimize_monitor. * wrap/python/cgi-bin/ltl2tgba.in: Adjust the calls to minimize_monitor and minimize_obligation. * wrap/python/spot.i: Declare minimize_monitor, minimize_wdba, minimize_obligations. * src/tgba/tgbaexplicit.hh (tgba_explicit_string) (tgba_explicit_formula, tgba_explicit_number): Add fake declarations so that SWIG can see they inherits from tgba. 2011-01-05 Alexandre Duret-Lutz Cleanup the DFA minimization algorithm. * src/tgbaalgos/minimize.cc (minimize): Move the minimization code into... (minimize_dfa): ... this new function, and fix the condition under which a partition is considered to be minimal. Also use a map instead of a list to lookup known formulae. 2011-01-05 Alexandre Duret-Lutz Speed up the obligation test. * src/tgbaalgos/minimize.cc (minimize_obligation): Do not minimize aut_neg_f, complement min_aut_f instead. * src/tgbaalgos/minimize.hh: Adjust description. 2011-01-05 Alexandre Duret-Lutz * src/tgbaalgos/minimize.cc (minimize): Use the Loeding algorithm to label transient states. 2011-01-04 Alexandre Duret-Lutz Rewrite the check of WDBA state acceptance in minimize(). * src/tgbaalgos/powerset.hh (power_map): New structure, allowing the caller to retrieve the set of original states corresponding to the set in the deterministic automaton. (power_set): Adjust prototype to take a power_map instead of the acc_list. * src/tgbaalgos/powerset.cc (power_set): Strip all code using acc_list, and update power_set. * src/tgbaalgos/minimize.cc (minimize): Rewrite, using an algorithm similar to the one in the Dax paper to check whether state of the minimized automaton should be accepting. 2011-01-04 Alexandre Duret-Lutz * src/tgbaalgos/scc.hh, src/tgbaalgos/scc.cc (scc_map::trivial, scc_map::one_state_of): Two new helper functions. 2011-01-04 Alexandre Duret-Lutz * src/tgba/tgbaunion.hh: Remove one useless include. 2011-01-04 Alexandre Duret-Lutz * README: Mention bench/wdba/. 2011-01-04 Alexandre Duret-Lutz Define tgba_product_init, a new kind of product with different initial states. * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc (tgba_product_init): New class. 2011-01-04 Alexandre Duret-Lutz * src/tgbatest/spotlbtt.test: Add test for -l -R3b, showing many failure because the minimization() algorithm is currently incorrect when applied to non-weak automata. 2011-01-04 Alexandre Duret-Lutz * src/tgbaalgos/scc.hh: Typo in documentation. 2011-01-04 Alexandre Duret-Lutz Move the logic for detecting when the minimize() algorithm is correct from ltl2tgba to the library. * src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc (minimize_obligation): New function. * src/tgbatests/ltl2tgba.cc (main): Fix constness of automata, and call minimize_obligation() for -R3b. 2010-12-26 Alexandre Duret-Lutz Make minimization of obligation properties and deterministic monitor available in the CGI script. * wrap/python/spot.i: Declare the minimize() interface. * wrap/python/cgi-bin/ltl2tgba.in: Add reduce_dmonitor and reduce_wdba options. 2010-12-14 Alexandre Duret-Lutz Add a WDBA benchmark. * bench/wdba/: New directory. * bench/Makefile.am (SUBDIRS): Add wdba. * NEWS: Mention it. * configure.ac: Output bench/wdba/defs and bench/wdba/Makefile. 2010-12-13 Alexandre Duret-Lutz * NEWS: Update the news about minimization. 2010-11-26 Alexandre Duret-Lutz Speed up wdba.test, it was too slow for our buildfarm. * src/tgbatest/wdba.test: Speed up execution by running only a couple of formula with valgrind. Half of those with`-l -R3b' and the other half with `-f -R3'. 2010-11-26 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (syntax): Regroup -M, -s, and -S option under the same heading "automaton conversion". 2010-11-25 Alexandre Duret-Lutz Preliminary support for monitors. * src/tgbatest/ltl2tgba.cc (-M): New option for building deterministic monitors. * src/tgbaalgos/minimize.cc (minimize): Take a monitor argument and adjust the code. * src/tgbaalgos/minimize.hh (minimize): Document it. 2010-11-25 Alexandre Duret-Lutz "ltl2tgba -Rm -X foo.tgba" would fail. * src/tgbatest/ltl2tgba.cc (main): Warn if -Rm is used without knowing the formula whose automaton is minimized. 2010-11-25 Alexandre Duret-Lutz Fix bugs in minimize(). * src/tgbaalgos/minimize.cc (init_sets, minimize): Fix memory leaks and a usage of the wrong automaton. * src/tgbatest/wdba.test: Try using -Rm with -R3 or -R3b, and with valgrind. This caught all the bugs fixed above. 2010-04-13 Alexandre Duret-Lutz Fix bugs in minimize(), caught by spotlbtt.test. * src/tgbaalgos/minimize.cc (minimize): Don't add acceptance conditions if the final set is empty. * src/tgbaalgos/powerset.cc (tgba_powerset): Add the initial state to acc_list if it is accepting. Also do not compute an SCC build map if we don't have to build acc_list. 2010-04-13 Alexandre Duret-Lutz "ltl2tgba -Rm" will apply WDBA-minimization only if correct. * src/tgbatest/ltl2tgba.cc (main): Use WDBA-minimization only when it is correct. Either we can quickly determine that a formula or its negation is a safety formula, or we can slowly check the equivalence of the WDBA-minimized automaton and the original automaton. * src/tgbatest/wdba.test: New test. * src/tgbatest/safety.test: Adjust comment. * src/tgbatest/spotlbtt.test: Use -Rm. * src/tgbatest/Makefile.am (TESTS): Add wdba.test. 2010-04-13 Alexandre Duret-Lutz Better resource handling in minimization. * src/tgbatest/ltl2tgba.cc (main): Delete the minimized automaton. * src/tgbaalgos/minimize.cc (minimize): Remove the call to unregister_variable() at the end. It was both wrong (unregistering only the first variable) and useless ("delete del_a" will unregister all these variables). Use a map and a set to keep track of free BDD variable and reuse them, otherwise the algorithm would sometimes use more variables than allocated. 2010-03-20 Alexandre Duret-Lutz Implement is_safety_automaton(). * src/tgbaalgos/safety.hh, src/tgbaalgos/safety.cc: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatests/ltl2tgba.cc: Add option "-O". * src/tgbaalgos/scc.hh: Update documentation. * src/tgbatest/Makefile.am (TESTS): Add safety.test. * src/tgbatest/safety.test: New file. 2010-03-26 Felix Abecassis * src/tgbaalgos/minimize.cc: Now use register_anonymous_variables. 2010-03-20 Felix Abecassis Small fixes. * src/tgbatest/minimize.cc: Delete useless includes. * src/tgbaalgos/minimize.cc: Delete useless includes, fixed acceptance conditions. * src/tgbatest/ltl2tgba.cc: Add -Rm option for minimization. * src/tgba/tgbaexplicit.cc: Fixed typo. 2010-03-20 Felix Abecassis Test program for the minimization algorithm. * src/tgbatest/minimize.cc: New file. Minimize an automaton from a LTL formula and compare the size of the initial automaton to the size of the minimized automaton. 2010-03-20 Felix Abecassis * src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh: New files. Algorithm to minimize an automaton using first the powerset construction to determinize the input automaton, the automaton is then minimized using the standard algorithm, using BDDs to check if states are equivalent. 2010-03-20 Felix Abecassis Modify the powerset algorithm to keep track of accepting states from the initial automaton. * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Added class tgba_explicit_number, a tgba_explicit where states are labelled by integers. * src/tgbaalgos/powerset.hh, src/tgbaalgos/powerset.cc: When building the deterministic automaton, keep track of which states were created from an accepting state in the initial automaton. The states are added to the new optional parameter (if not 0), acc_list. Use tgba_explicit_number instead of tgba_explicit_string to build the result. * src/tgbaalgos/scc.cc (spot): Small fix. Print everything on std::cout. 2011-01-05 Alexandre Duret-Lutz Fix computation of support_conditions for bdd-based TGBA. This fixes a bug in the powerset of such TGBA on the minimize branch. * src/tgba/tgbabddconcrete.cc (compute_support_conditions): Also account for the conditions from the acceptance relations. * rc/tgba/tgbabddconcretefactory.hh, rc/tgba/tgbabddconcretefactory.cc (acceptance_conditions_support): New variable to hold the value of bdd_support(acceptance_conditions_support). * src/tgba/tgbabddconcretefactory.cc (finish): Update data_.acceptance_conditions_support. 2010-12-26 Alexandre Duret-Lutz * wrap/python/cgi-bin/ltl2tgba.in: Remove all "new" markers. 2010-12-23 Alexandre Duret-Lutz Define SWIG_TYPE_TABLE as suggested by the SWIG documentation. * wrap/python/Makefile.am: Add -DSWIG_TYPE_TABLE=spot. 2010-12-23 Alexandre Duret-Lutz Use swig2.0 if available. * configure.ac: Search for swig2.0 and swig. * wrap/python/Makefile.am: Use $(SWIG). 2010-12-23 Alexandre Duret-Lutz Get rid of ltihooks.py. ltihooks.py apparently breaks the import mechanisms of Python 2.6, causes SWIG's runtime to fail to share a global type table, and yields various failures in our tests. * wrap/python/ltihooks.py: Delete. * wrap/python/Makefile.am (EXTRA_DIST): remove ltihooks.py. * 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, wrap/python/tests/minato.py, wrap/python/tests/modgray.py, wrap/python/tests/optionmap.py, wrap/python/tests/setxor.py: Do not use ltihooks. * wrap/python/tests/run.in (pypath): Include the .libs/ directories in the search path so that Python can find the *.so libraries. * wrap/python/cgi-bin/ltl2tgba.in: Insert the .libs/ directories into sys.path instead of importing ltihooks. 2010-12-12 Alexandre Duret-Lutz * NEWS: Summarize recent changes. 2010-12-11 Alexandre Duret-Lutz Merge transitions in tgba_tba_proxy. With this change the output of ltl2tgba -f -x -k -DS "GF(p_1) & ... & GF(p_n) uses less than (n+1)^2 transitions when it used exactly (n+1)*(2^n) transitions before. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): Merge transitions going to the same states if they are both accepting or if neither are. (state_ptr_bool_t, state_ptr_bool_less_than): Helper type to store a transition in tgba_tba_proxy_succ_iterator. * src/tgba/tgbatba.cc, src/tgba/tgbatba.hh (tgba_tba_proxy::transition_annotation): Remove. We cannot implement this method if transitions are merged. * src/tgbatest/ltl2tgba.test: Add a test. 2010-12-10 Alexandre Duret-Lutz Augment the size of the ltlclasses benchmark. * bench/ltlclasses/run: Augment the max size to 20. * bench/ltlcounter/run: Typo in comment. 2010-12-10 Alexandre Duret-Lutz Introduce -ks to print only the size of the automaton (without SCC information). * src/tgbatest/ltl2tgba.cc (syntax, main): Add a -ks option. * src/tgbatest/ltl2tgba.test, bench/ltlclasses/run, bench/ltlcounter/run: Use -ks instead of -k to speed things up. 2010-12-09 Alexandre Duret-Lutz Use a cache to speed up tgba_tba_proxy. tgba_tba_proxy used to spend a lot of time (re)computing the acceptance condition common to all outgoing transition of a state. * src/tgba/tgbatba.hh (accmap_): New cache. (common_acceptance_conditions_of_original_state): New method. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::~sync) Call common_acceptance_conditions_of_original_state() instead of computing the result. (~tgba_tba_proxy): Cleanup the cache. (common_acceptance_conditions_of_original_state): Implement it. 2010-12-07 Alexandre Duret-Lutz * src/ltltest/Makefile.am (genltl_SOURCES): Add missing variable. 2010-12-07 Alexandre Duret-Lutz * README: Mention bench/ltlclases/. 2010-12-04 Alexandre Duret-Lutz Preliminary benchmark using genltl, introduced earlier. * bench/ltlclasses/: New benchmark. * bench/Makefile.am: Add it. * configure.ac: Adjust. 2010-12-04 Alexandre Duret-Lutz * src/ltlvisit/syntimpl.cc: Reduce the number of dynamic_cast<>s. 2010-12-04 Alexandre Duret-Lutz Preliminary implementation of a tool to generate some interesting families of LTL formulae. * src/ltltest/genltl.cc: New file. Based on five classes of formulae defined in a paper by Cichón, Czubak, and Jasiński. * src/ltltest/Makefile.am (noinst_PROGRAMS): Build genltl. 2010-12-03 Alexandre Duret-Lutz Add full_parent support to to_spin_string(). * src/ltlvisit/tostrinc.hh (to_spin_string): Add a full_parent optional parameter, like for the to_string() function. * src/ltlvisit/tostrinc.cc (to_string_visitor): Fix the handling of full_parent. (to_spin_string_visitor): Handle full_parent. 2010-12-01 Alexandre Duret-Lutz Halve the number of application of eventual_universal_visitor in reduce_visitor::visit(binop). * src/ltlvisit/reduce.cc (eventual_universal_visitor::recurse_): Move this method... (recurse_eu): ... outside as a separate function. Likewise for the universal/eventual result struct. (reduce_visitor::visit(binop)): Call recurse_eu() once to replace two calls to is_eventual and is_universal, thus replacing two recursions by one. 2010-12-01 Alexandre Duret-Lutz Move the eventual-universal functions where the belong. * src/ltlvisit/syntimpl.cc (eventual_universal_visitor, is_eventual, is_universal): Move ... * src/ltlvisit/reduce.cc (eventual_universal_visitor, is_eventual, is_universal): ... here. 2010-11-30 Alexandre Duret-Lutz * src/ltlvisit/randomltl.cc (random_ltl::update_sums): Typo in string. 2010-11-30 Alexandre Duret-Lutz Remove a quadratic behavior in eventual_universal_visitor. * src/ltlvisit/syntimpl.cc (eventual_universal_visitor): Use a union to store the eventual and universal properties as two bit in a bit-field, and "AND" both of them at once. (eventual_universal_visitor::recurse_un, eventual_universal_visitor::recurse_ev): Replace these two functions by ... (eventual_universal_visitor::recurse_): ... this one, that returns both bits as an unsigned. 2010-12-01 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (main): Delete the accepting run even if it hasn't been printed. 2010-11-30 Alexandre Duret-Lutz Rationalize options for counter-example output. * src/tgbatest/ltl2tgba.cc (main): Either replay the accepting run or print it, but do not do both. * src/tgbatest/emptchk.test: Adjust. I.e. use -C instead of -CR when we expect the run to be displayed. 2010-11-30 Alexandre Duret-Lutz Fix a GCC 4.6 warning. * src/tgbatest/randtgba.cc (main): Remove the set but unused opt_A variable (the upcoming GCC 4.6 would warn about it) and set opt_ec to 1 if -A is used without -e. 2010-11-27 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (syntax): Typo. 2010-11-27 Alexandre Duret-Lutz Another Clang report. * iface/nips/nips.cc (format_state): Do not use a variable-sized array, this is not allowed in C++. 2010-11-27 Alexandre Duret-Lutz Fix more errors reported by Clang. * src/tgbaalgos/reducerun.hh (tgba_run): Predeclare as a struct since this is what it is. * src/tgbatest/randtgba.cc (main): Avoid using "i" with two different type in the same loop. 2010-11-26 Alexandre Duret-Lutz Finalize Kripke interface. * src/kripke/fairkripke.hh, src/kripke/fairkripke.cc, * src/kripke/kripke.hh, src/kripke/kripke.cc: Finalize and document the Kripke interface. I have tested it by updating checkpn to use it. 2010-11-25 Alexandre Duret-Lutz Never claim output used to print the degeneralized automaton before some optional operations (like more optimizations, or a product). * src/tgbatest/ltl2tgba.cc (-N, -NN): Make sure we print the last automaton computed, not just the automaton when we degeneralized it. We may have applied other algorithms since the original degeneralization. 2010-11-25 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.test: Test both -l and -f. This should have been done on 2010-01-30 when the default translation was changed from -l to -f. 2010-11-25 Alexandre Duret-Lutz * src/tgbaalgos/scc.hh: Typos in the documentation. 2010-11-24 Alexandre Duret-Lutz * src/tgbaalgos/sccfilter.hh: Fix some typos in the documentation. 2010-11-24 Alexandre Duret-Lutz Suggest using bddtrue and bddfalse instead of bdd_true() and bdd_false(). * src/sanity/style.test: Catch uses of bdd_true() or bdd_false(). 2010-11-20 Alexandre Duret-Lutz Fix some struct/class missmatches reported by clang. * src/ltlast/predecl.hh: Predeclare the LTL AST nodes as class, not struct. * src/ltlast/nfa.hh (formula_tree::node): Predeclare as struct, not class. 2010-11-07 Alexandre Duret-Lutz Add interface for and test the bdd_setxor() function added to Buddy. * wrap/python/buddy.i (bdd_setxor): New function. * wrap/python/tests/setxor.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add setxor.py. 2010-11-06 Alexandre Duret-Lutz * src/Makefile.am (libspot_la_LIBADD): Rename libneverclaimparse.la as libneverparse.la. * src/neverparse/Makefile.am: Install files in $(pkgincludedir)/neverparse, not $(pkgincludedir)/neverclaimparse. 2010-11-06 Alexandre Duret-Lutz Cosmetics to please sanity checks. * src/neverparse/public.hh, src/neverparse/parsedecl.hh: Fix inclusion guards. * src/tgba/tgbaexplicit.hh, src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc: Fix trailing whitespaces. 2010-11-06 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc: Clock the time spent reading -P file. 2010-11-06 Alexandre Duret-Lutz * src/tgbatest/neverclaimread.test: Check that Spot can read the neverclaims it outputs. 2010-11-06 Alexandre Duret-Lutz Do not output a counterexample by default in ltl2tgba, introduce options -C and -CR for that. * src/tgbatest/ltl2tgba.cc: Add option -C and -CR to control whether we want the accepting run to be printed or replayed. * src/tgbatest/dfs.test, src/tgbatest/eltl2tgba.test, src/tgbatest/emptchk.test, src/tgbatest/emptchke.test, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlcounter.test: Use -CR. 2010-11-06 Alexandre Duret-Lutz Make sure the neverclaim parser works on the output of spin and ltl2ba. * src/neverparse/neverclaimparse.yy: Accept multiple labels for the same state. Honor accepting states. Forward parse error from the parser used for guards. Accept "false" as a single instruction for a state. * src/neverparse/neverclaimscan.ll: Recognize "false" specifically, and remove the ";" hack. * src/tgba/tgbaexplicit.cc (tgba_explicit_string::~tgba_explicit_string): Adjust not to destroy a state twice. * src/tgba/tgbaexplicit.hh (tgba_explicit_string::add_state_alias): New function. * src/tgbatest/defs.in (SPIN, LTL2BA): New variables. * src/tgbatest/neverclaimread.test: Check error messages for syntax errors in guards. Make sure we can read the output of `spin -f' and `ltl2ba -f' on a few test formulae. 2010-11-06 Alexandre Duret-Lutz Cleanup neverclaim support. * src/neverclaimparse/: Shorthen as ... * src/neverparse/:... this. * src/Makefile.am: Adjust, and add back the directories mistakenly removed by previous patch. * README: Adjust, and keep the file's width under 80 columns. * configure.ac: Adjust. * src/neverparse/Makefile.am, src/neverparse/fmterror.cc, src/neverparse/neverclaimparse.yy, src/neverparse/neverclaimscan.ll, src/neverparse/public.hh: Fix copyright. * src/tgbatest/Makefile.am (check_PROGRAMS): Remove neverclaimread. * src/tgbatest/ltl2tgba.cc: Add option -XN to read a neverclaim. * src/tgbatest/readneverclaim.cc: Delete. * src/tgbatest/neverclaimread.test: Use ltl2tgba instead of neverclaimread. 2010-05-25 Felix Abecassis Add never claim parser. * src/neverclaimparse/: New directory. * src/neverclaimparse/fmterror.cc: New file. Print a formatted parse error on a output stream. * src/neverclaimparse/neverclaimparse.yy: New file. Parser declaration for Bison. * src/neverclaimparse/neverclaimscan.ll: New file. Scanner declaration for Flex. * src/neverclaimparse/public.hh: New file. Public header for external use. * src/neverclaimparse/parsedecl.hh: New file. Header file for Flex-Bison interaction. * src/neverclaimparse/Makefile.am: New Makefile. * src/tgbatest/neverclaimread.cc: New file. Test program for the never claim parser. * src/tgbatest/neverclaimread.test: New file. Test script for the never claim parser. * src/tgbatest/Makefile.am: Adjust. * configure.ac : Adjust. * README: Adjust. 2010-11-06 Alexandre Duret-Lutz Remove `readsave' and fix line numbers in tgbaparse error messages. * src/tgbaparse/tgbaparse.yy (line): Fix computation of line number for error messages when parsing conditions. * src/tgbatest/readsave.test: Check the syntax position of syntax errors in the diagnostics. Use ltl2tgba instead of readsave. * src/tgbatest/Makefile.am (check_PROGRAMS): Remove readsave. 2010-11-06 Alexandre Duret-Lutz * bench/emptchk/pml2tgba.pl: Adjust to work with Spin 5.2.5. 2010-10-07 Alexandre Duret-Lutz * configure.ac: Do not run CF_GXX_WARNINGS unless they are enabled. 2010-10-07 Alexandre Duret-Lutz Hide the safra_tree_automaton type from the public interface. We do that because the declaration of this type, which is local to src/tgba/tgbasafracomplement.cc has a member in an anonymous namespace, and some versions of g++-4.2 issue a very annoying warning about this legitimate code. See Bug 29365 on GCC's Bugzilla. Report by Silien Hong . * src/tgba/tgbasafracomplement.hh (safra_tree_automaton): Do not forward declare. (tgba_safra_complement): Use void* instead of safra_tree_automaton*. * src/tgba/tgbasafracomplement.cc: static_cast void* to safra_tree_automaton* anywhere needed. 2010-05-20 Alexandre Duret-Lutz Fix the --enable-optimizations check. * m4/gccoptim.m4: Add missing AC_LANG_PUSH/AC_LANG_POP around the C test. It was using the C++ compiler instead... 2010-04-16 Alexandre Duret-Lutz * NEWS: Typo. 2010-04-16 Alexandre Duret-Lutz * NEWS, configure.ac: Bump version to 0.6a. 2010-04-16 Alexandre Duret-Lutz Release Spot 0.6. * NEWS, configure.ac: Bump version to 0.6. 2010-04-15 Alexandre Duret-Lutz Reorder recent additions to reduccmp.test. * src/ltltest/reduccmp.test: Reorder the test added by the previous patches. Some are not supposed to be reduced by reductaustr. 2010-04-15 Alexandre Duret-Lutz Fix a long-standing bug in the stronger rule for R and its recent clone for M. * src/ltlvisit/contain.cc (reduce_tau03_visitor): Remove the stronger rules for R and M. They were wrong. * src/ltltest/reduccmp.test: Test a simpple counterexample. 2010-04-15 Alexandre Duret-Lutz More simplifications rules for M. * src/ltlvisit/reduce.cc (reduce_visitor): Add the following implication rewriting rules: a M (b M c) = a M c if a implies b. a M (b R c) = a M c if a implies b. a R (b R c) = a R c if a implies b. a R (b M c) = b M c if b implies a. a M (b M c) = b M c if b implies a. The latter rule was fixed from an incorrectly copied&pasted rule for a M (b R c) = b R c if b implies a (this is wrong). Also remove the wrong rule for a W (b U c) = b U c if a implies b. * src/ltltest/reduccmp.test: Add more tests. 2010-04-15 Alexandre Duret-Lutz Speed up syntactic_implication() for constants. * src/ltlvisit/syntimpl.cc (syntactic_implication): Do not create visitors if arguments are constant. 2010-04-15 Alexandre Duret-Lutz Fix simplification of "a M true" as Fa. * src/ltlvisit/simpfg.cc: Typo. * src/ltltest/reduccmp.test: Add more tests. 2010-04-15 Alexandre Duret-Lutz * HACKING: Bison 2.4.2 has a bugfix we rely on. 2010-04-15 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (syntax): Add missing black line in help output. 2010-04-14 Alexandre Duret-Lutz * NEWS: Mention W and M. 2010-04-14 Alexandre Duret-Lutz More LTL reductions for W and M. * src/ltlvisit/basicreduce.cc: Perform the following reductions: (a R b) | Gb = a R b (a M b) | Gb = a R b (a U b) & Fb = a U b (a W b) & Fb = a U b * src/ltltest/reduccmp.test: Test them. 2010-04-12 Alexandre Duret-Lutz * wrap/python/cgi-bin/ltl2tgba.in: Document W and M operators. 2010-04-12 Alexandre Duret-Lutz More LTL reductions for W and M. * src/ltlvisit/basicreduce.cc: Perform the following reductions: (a U b) & (c W b) = (a & c) U b (a W b) & (c W b) = (a & c) W b (a R b) | (c M b) = (a | c) R b (a M b) | (c M b) = (a | c) M b * src/ltltest/reduccmp.test: Test them. 2010-04-12 Alexandre Duret-Lutz Add LTL reductions for strong release. * src/ltlvisit/basicreduce.cc: Perform the following reductions. a R (b & F(a)) = a M b a M (b & F(a)) = a M b a R Fa = Fa a M Fa = Fa a R b & Fa = a M b a R b & a M c = a M (b & c) a M b & a M c = a M (b & c) * src/ltltest/reduccmp.test: More tests. 2010-04-12 Alexandre Duret-Lutz Add LTL reductions for weak until. * src/ltlvisit/basicreduce.cc: Perform the following reductions. a U (b | Ga) = a W b a W (b | Ga) = a W b a U b | Ga = a W b a U b | a W c = a W (b | c) a W b | a W c = a W (b | c) a U Ga = Ga a W Ga = Ga * src/ltltest/reduccmp.test: More tests. 2010-04-07 Alexandre Duret-Lutz Add support for W (weak until) and M (strong release) operators. * src/ltlast/binop.cc, src/ltlast/binop.cc: Add support for these new operators. * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse them. * src/ltltest/reduccmp.test: Add new tests for W and M. * src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc, src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc, src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.cc, src/ltlvisite/simpfg.cc, src/ltlvisit/simpfg.hh, src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc: Add support for W and M. * src/tgbatest/ltl2neverclaim.test: Test never claim output using LBTT, this is more thorough. Also we cannot use -N any more in the spotlbtt.test. * src/tgbatests/ltl2tgba.cc: Define M and W for ELTL. * src/tgbatest/ltl2neverclaim.test: Test W and M, and use -DS instead of -N, because lbtt-translate does not want to translate these operators for tools that masquerade as Spin. 2010-04-12 Alexandre Duret-Lutz Adjust ltl2tgba.py to call scc_filter() with the "full" option as appropriate. * wrap/python/spot.i (spot::scc_filter): Make it available. * wrap/python/cgi-bin/ltl2tgba.in (reduce_scc): Call scc_filter. Use the "full" option unless the show_degen_png or show_never_claim are set. Also reduce_scc the default. 2010-04-08 Alexandre Duret-Lutz * src/ltlvisit/basicreduce.cc: Typo in comment. 2010-04-08 Alexandre Duret-Lutz * NEWS: Summarize recent noteworthy changes. 2010-04-07 Alexandre Duret-Lutz Modernize Bison parsers. * src/ltlparse/ltlparse.yy, src/tgbaparse/tgbaparse.yy, src/evtgbaparse/evtgbaparse.yy, src/eltlparse/eltlparse.yy: Use token types for %destructor and %printer. Remove the yylex hack, since %name-prefix is now honored by Bison. Also remove the useless type. Suggested by Akim Demaille. 2010-03-10 Alexandre Duret-Lutz Fix column in LTL error messages, it was off by one. * src/ltlparse/fmterror.cc (format_parse_errors): Count columns starting at 1. Older Bison used to start at 0 but changed to match the GNU Coding Standards. * src/ltltest/parseerr.test: Add a test case. 2010-03-07 Alexandre Duret-Lutz Do not rewrite F(a & GF(b)) = F(a) & GF(b), this can be harmful. * src/ltlvisit/basicreduce.cc (basic_reduce_visitor::recurse): Disable this rule unconditionally. * src/ltltest/reduccmp.test: Adjust tests. 2010-03-06 Alexandre Duret-Lutz * src/tgba/tgbatba.cc: Fix English in comments. 2010-03-06 Alexandre Duret-Lutz Reverse the order of expected acceptance conditions in degeneralization. * src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_tba_proxy): Build the list of acceptance condition in the reverse order. The order is still arbitrary, but the bdd_satone() call seems to output the acceptance conditions that are more used first, and this helps the degeneralization process. 2010-03-06 Alexandre Duret-Lutz Tweak precedence of "->" and <->. * src/ltlparse/ltlparse.yy: Change the precedence of "->" and "<->" so that "a & b -> c" is interpreted as "(a & b) -> c" instead of "a & (b -> c)". The new interpretation is more intuitive, and matches that of LBTT. 2010-03-06 Alexandre Duret-Lutz * bench/ltl2tgba/formulae.ltl: Fix three formulae to match the original paper by Somenzi and Bloem. Reported by Ruediger Ehlers. 2010-03-06 Alexandre Duret-Lutz Fix memory leak introduced in yesterday's change. * src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_sba_proxy): Do not forget to free the initial state after usage. 2010-03-06 Alexandre Duret-Lutz Keep acceptance conditions on transitions going to accepting SCCs by default in scc_filter(). Doing so helps the degeneralization algorithm, because it will have more opportunity to be in an accepting level when it reaches the accepting SCCs. * src/tgbaalgos/sccfilter.cc (filter_iter::filter_iter): Take a remove_all_useless argument. (filter_iter::process_link): Use the flag to decide whether to filter acceptance conditions going to accepting SCCs. (scc_filter): Take a remove_all_useless argument and pass it to filter_iter. * src/tgbaalgos/sccfilter.hh (filter_iter): Add the new argument and document the function. * src/tgbatest/tgbatests/ltl2tgba.cc (main): Add option use -R3 for remove_all_useless=false and add -R3f for remove_all_useless=true. * src/tgbatest/ltl2tgba.test: Show one case where -R3f makes the degeneralization worse than -R3. 2010-03-05 Alexandre Duret-Lutz Simplify F(a)|F(b) as F(a|b). Add similar rule for G(a)&G(b). * src/ltlvisit/basicreduce.cc (basic_reduce_visitor): Replace the FG(a)|FG(b) == F(Ga|Gb) rule by the above more generic one. Add the dual rule for G(a)&G(b), as we had none (this one won't improve anything in the translation, but it is more symmetric this way). Also simplify some pointer checks. 2010-03-05 Alexandre Duret-Lutz Better selection of the acceptance of the initial state in SBA. * src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_sba_proxy): Set cycle_start_ to start in the accepting layer of the degeneralized automaton if the initial state has an accepting self-loop. Otherwise, starts at the level of the first acceptance condition as previously. (tgba_sba_proxy::get_init_state): Use cycle_start_. * src/tgba/tgbatba.hh (tgba_tba_proxy::a_): Make it protected so that we can use it in tgba_sba_proxy::tgba_sba_proxy. (tgba_sba_proxy::cycle_start_, tgba_sba_proxy::get_init_state): Declare. * src/tgbatest/ltl2tgba.test: More tests. 2010-03-05 Alexandre Duret-Lutz Generalize the previous patch to accepting states in SBA. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::sync_): Move the optimization step added by the previous patch outside the before the bddtrue check, so that it also applies to accepting states in SBA. 2010-03-03 Alexandre Duret-Lutz Optimize tgba_tba_proxy and tgba_sba_proxy for states that share an acceptance condition on all outgoing transitions. This was motivated by experiments from Rüdiger Ehlers, showing that "ltl2ba -f 'a U (b U c)'" outperformed "ltl2tgba -f -N -R3 'a U (b U c)'". With this change and the previous one, it is no longer the case. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::aut_): Store a pointer to the source automaton and... (tgba_tba_proxy_succ_iterator::sync_): ... use it in an extra optimization step to gather the acceptance conditions common to all outgoing transitions of the destination state, and pretend they are on the current (ingoing) transition. (tgba_tba_proxy::succ_iter): Pass the source automaton to the constructed iterator. * src/tgbatest/spotlbtt.test: Test -f -N -R3 -r7. * src/tgbatest/ltl2tgba.test: Add a test case for 'a U (b U c)'. 2010-03-03 Alexandre Duret-Lutz ltl2tgba: apply -R3 before -D or -DS. * src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the degeneralization, because it might remove useless acceptance conditions. I realized this while looking at experiments from Rüdiger Ehlers. 2010-02-24 Alexandre Duret-Lutz * src/sanity/style.test: Better fix for the previous error. 2010-02-23 Alexandre Duret-Lutz Work around a spurious style.test error. * src/saba/sabacomplementtgba.hh (spot): Rewrite Büchi as B\"uchi is the BibTex entry used as comment, because some version of sed will choke on non-ascii character and cause sanity/style.test to fail. 2010-02-23 Alexandre Duret-Lutz Fix random_graph() not to generate dead states. This is actually the third time I fix random_graph(). On 2007-02-06 I changed the function not to generated dead states, but in a way that made it non-deterministic. On 2010-01-20 I made the function deterministic again, but it started to generate dead states as a side effect. This time, I'm making sure that dead states won't come again with a test-case that we should have had from the beginning. * src/tgbaalgos/randomgraph.cc (random_graph): Add an extra indirection array, state_randomizer[], so that we can reorder states indices after a random selection without actually changing the value of the indices used by unreachable_states and nodes_to_process. * src/tgbatest/randtgba.test: New file. * src/tgbatest/Makefile.am: Add randtgba.test. 2010-02-17 Alexandre Duret-Lutz ltl2tgba cgi updates. * wrap/python/cgi-bin/ltl2tgba.in (dot): Use the value computed by configure. (os.system): Cleanup stale files only when the form has been submitted. (list options): Keep track of the selected value. (draw_acc_run|print_acc_run): set ec=0 to detect if it has been later set or not. Fix error message when using generalized automata with degeneralized emptiness checks. * wrap/python/cgi-bin/Makefile.am (ltl2tgba.py): Substitute @DOT@. 2010-02-02 Alexandre Duret-Lutz * wrap/python/cgi-bin/ltl2tgba.in: Reword description of svg_output. 2010-02-02 Alexandre Duret-Lutz Add SVG output and language containment options to the cgi script. * wrap/python/cgi-bin/ltl2tgba.in (new): Mark new options as new. (svg_output, reduce_langcout): Add these new options. (render_dot): Support svg_output. 2010-02-02 Alexandre Duret-Lutz * NEWS: Typo. 2010-02-01 Alexandre Duret-Lutz * NEWS, configure.ac: Bump version to 0.5a. 2010-02-01 Alexandre Duret-Lutz Release Spot 0.5. * NEWS, configure.in: Bump version to 0.5. 2010-01-31 Alexandre Duret-Lutz * doc/Makefile.am ($(srcdir)/stamp): Do not depend on dot explicitly, otherwise the documentation is always built and distcheck fails. 2010-01-31 Alexandre Duret-Lutz More Doxygen fixes. * src/sabaalgos/sabareachiter.hh (process_link): Document argument SI. * src/eltlparse/public.hh (format_parse_errors): Remove the non-existing eltl_string argument from the description. (parse_file): Fix name of parameters in documentation. 2010-01-31 Alexandre Duret-Lutz Build doxygen pictures with libgd to reduce their size. Doxygen only knows how to call dot with -Tpng, while using -Tpng:gd produces pictures that are 10 times smaller. Use a simple wrapper around dot to simplify this. * doc/dot.in: New file, that wrap the system's dot and replace -Tpng by -Tpng:gd. * doc/Makefile.am ($(srcdir)/stamp): Depend on dot. * doc/Doxyfile.in: Update to 1.6.2. (DOT_PATH): Set to @srcdir@ to use doc/dot instead of the system's dot. * configure.ac: Find the absolute path of dot, and generate the doc/dot script. 2010-01-31 Alexandre Duret-Lutz More Doxygen fixes. * src/tgba/tgbakvcomplement.hh: Use \verbatim around the bibtex entry. * src/saba/sabacomplementtgba.hh: Use latin1. 2010-01-30 Alexandre Duret-Lutz * bench/split-product/Makefile.am (nodist_noinst_DATA): Do not depend on files that cannot be built. 2010-01-30 Alexandre Duret-Lutz Replace spot::ltl_file by a rewritten spot::ltl::ltl_file. * src/tgba/tgbafromfile.cc, src/tgba/tgbafromfile.hh: Delete these files. * src/tgba/Makefile.am: Remove them. * src/ltl/ltlparse/ltlfile.hh, src/ltl/ltlparse/ltlfile.cc: New files. * src/ltl/ltlparse/Makefile.am: Add them. * bench/scc-stats/stats.cc, bench/split-product/cutscc.cc: Rewrite using the new class. 2010-01-30 Alexandre Duret-Lutz Check for missing Copyright blurbs, and add them. * src/sanity/style.test: Check for missing Copyrights blurbs. * src/sanity/Makefile.am: Run style.test before includes.test. * iface/gspn/dcswave.test, iface/gspn/dcswaveeltl.test, iface/gspn/dcswavefm.test, iface/gspn/dcswaveltl.test, iface/gspn/simple.test, iface/gspn/udcsefm.test, iface/gspn/udcseltl.test, iface/gspn/udcsfm.test, iface/gspn/udcsltl.test, iface/nips/nipstest/dotty.test, iface/nips/nipstest/emptiness.test, src/eltltest/acc.test, src/eltltest/nfa.test, src/saba/sabacomplementtgba.cc, src/sabatest/sabacomplementtgba.cc, src/tgbatest/eltl2tgba.test, src/tgbatest/taatgba.test: Add missing Copyright blurb. 2010-01-30 Alexandre Duret-Lutz * NEWS: More text. 2010-01-30 Alexandre Duret-Lutz Touch up some doxygen comments and copyrights. * eltlparse/public.hh, saba/saba.hh, tgba/tgbakvcomplement.hh, tgba/tgbasafracomplement.hh, tgbaalgos/eltl2tgba_lacim.cc, tgbaalgos/eltl2tgba_lacim.hh, tgbaalgos/ltl2taa.hh: Comment changes. 2010-01-30 Alexandre Duret-Lutz Add SCC pruning options to the CGI script. * wrap/python/cgi-bin/ltl2tgba.in: Add options to symbolically prune unaccepting SCCs in LaCIM, and explicitely pruns unaccepting SCCs in all algorithms. * src/tgbaalgos/reductgba_sim.hh: Conceal most of the file to SWIG. * wrap/python/spot.i: Include reductgba_sim.hh. 2010-01-30 Alexandre Duret-Lutz * src/evtgbatest/ltl2evtgba.test: Replace * by &. 2010-01-30 Alexandre Duret-Lutz Make it possible to use the cgi script without installing a web server. * wrap/python/cgi-bin/ltl2tgba.in: Starts a web server if the script is not called as a CGI. Arrange to load libraries from the build directory. Create the spotimg/ if needed when run as a web server. * wrap/python/cgi-bin/Makefile.am: Adjust build rule and clean the spotimg directory. * wrap/python/cgi-bin/README, NEWS: Update. 2010-01-30 Alexandre Duret-Lutz More * -> & replacements. * src/ltltest/parse.test, src/ltltest/syntimpl.test: Replace * by &. 2010-01-30 Alexandre Duret-Lutz Remove the theoretically bogus "containment" option of ltl2tgba_fm. * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh: Remove the containment option. * src/tgbafromfile.cc, src/tgbafromfile.hh: Remove the containment_ member. * src/tgbatest/ltl2tgba.cc (syntax): Remove -c option for FM algorithm, use it exclusively for TAA. 2010-01-30 Alexandre Duret-Lutz * src/tgba/tgbasafracomplement.hh: Add missing copyright and fix some comments. 2010-01-30 Alexandre Duret-Lutz Rename tgba_complement as tgba_kv_complement. * src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: Rename as... * src/tgba/tgbakvcomplement.hh, src/tgba/tgbakvcomplement.cc: ... these. It makes more sense since we also have tgba_safra_complement. * src/tgba/Makefile.am, src/tgbatest/complement.cc, NEWS: Adjust. 2010-01-30 Alexandre Duret-Lutz Do not recognize "*" as "and". This leaves room for an implementation of rational operators in a future version. * src/ltlparse/ltlscan.ll: Do not recognize "*". * wrap/python/cgi-bin/ltl2tgba.in: Undocument it. * NEWS: Mention this. * src/tgbatest/kv.test, src/tgbatest/ltl2tgba.test, src/tgbatest/reductgba.test: Replace "*" by "&". 2010-01-30 Alexandre Duret-Lutz Make Couvreur/FM the default translation. * src/tgbatest/ltl2tgba.cc (syntax, main): Do it. * NEWS: Mention it. * src/tgbatest/emptchk.test: Add missing -l. 2010-01-30 Alexandre Duret-Lutz Overhaul LaCIM's ELTL options. * src/tgbatest/ltl2tgba.cc (syntax, main): Introduce -le to select this algorithm and -lo to add the default LTL operators. This replace the undocumented hack to add LTL operators when the formula with read for command-line, or the automaton was output for LBTT. * src/tgbatest/eltl2tgba.test, src/tgbatest/spotlbtt.test: Update call syntax. * NEWS: Mention -le, -lo, and -taa. 2010-01-30 Alexandre Duret-Lutz Touch up -R3b handling. * src/tgbatest/ltl2tgba.cc (syntax): Move -R3b with the other LaCIM options. (main): Speak of "symbolic SCC pruning" instead of "deleting unaccepting SCC", and do that right after the translation, before degeneralization. Also error out when -R3b is used on non symbolic automata. 2010-01-29 Alexandre Duret-Lutz Update some text files for upcoming 0.5. * NEWS: Update for upcoming 0.5. * HACKING: Update Automake requirement. * README: Mention the mailing list. * bench/ltlcounter/README: More text. * configure.ac: Report bugs to spot@lrde.epita.fr. 2010-01-29 Alexandre Duret-Lutz Rename wrap/python/cgi/ as wrap/python/cgi-bin/. * wrap/python/cgi/: Rename as ... * wrap/python/cgi-bin/: ... this. * configure.ac, spot/wrap/python/Makefile.am, README: Adjust. 2010-01-29 Alexandre Duret-Lutz * src/tgbaalgos/gtec/gtec.hh: Fix copyright. 2010-01-29 Felix Abecassis * src/tgba/taatgba.cc, src/tgba/taatbga.hh: Fix a memory issue on Darwin. 2010-01-25 Damien Lefortier * wrap/python/cgi/ltl2tgba.in, wrap/python/spot.i: Add a new translation algorithm: Tauriainen/TAA. 2010-01-25 Damien Lefortier * wrap/python/cgi/ltl2tgba.in: Use the uuid Python module instead of the UNIQUE_ID environment variable to avoid being Apache-specific. 2010-01-24 Guillaume Sadegh Fix copyrights. * bench/Makefile.am, bench/gspn-ssp/Makefile.am, bench/gspn-ssp/defs.in, bench/scc-stats/Makefile.am, bench/split-product/Makefile.am, configure.ac, iface/Makefile.am, iface/gspn/Makefile.am, iface/gspn/ssp.hh, iface/nips/Makefile.am, iface/nips/common.cc, iface/nips/common.hh, iface/nips/dottynips.cc, iface/nips/nips.cc, iface/nips/nips.hh, src/Makefile.am, src/eltlparse/Makefile.am, src/eltlparse/eltlparse.yy, src/eltlparse/eltlscan.ll, src/eltlparse/fmterror.cc, src/eltlparse/parsedecl.hh, src/eltltest/Makefile.am, src/eltltest/defs.in, src/eltltest/nfa.cc, src/evtgba/evtgba.hh, src/evtgba/product.cc, src/evtgba/product.hh, src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaparse/Makefile.am, src/evtgbaparse/evtgbaparse.yy, src/evtgbatest/defs.in, src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/ltl2evtgba.test, src/evtgbatest/product.cc, src/evtgbatest/product.test, src/evtgbatest/readsave.cc, src/evtgbatest/readsave.test, 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/formula_tree.cc, src/ltlast/formula_tree.hh, src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh, src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlenv/declenv.cc, src/ltlenv/declenv.hh, src/ltlenv/environment.hh, src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy, 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/randltl.cc, src/ltltest/readltl.cc, src/ltltest/reduccmp.test, src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test, src/ltltest/tostring.cc, src/ltltest/tostring.test, src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test, src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc, src/ltlvisit/clone.hh, src/ltlvisit/contain.cc, src/ltlvisit/destroy.cc, src/ltlvisit/destroy.hh, src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc, src/ltlvisit/randomltl.cc, src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc, src/misc/bddalloc.cc, src/misc/bddop.cc, src/misc/bddop.hh, src/misc/freelist.hh, src/misc/hash.hh, src/misc/minato.cc, src/misc/minato.hh, src/misc/optionmap.cc, src/misc/timer.cc, src/misc/timer.hh, src/saba/Makefile.am, src/saba/explicitstateconjunction.cc, src/saba/explicitstateconjunction.hh, src/saba/saba.cc, src/saba/saba.hh, src/saba/sabacomplementtgba.cc, src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh, src/saba/sabasucciter.hh, src/sabaalgos/Makefile.am, src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh, src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh, src/sabatest/Makefile.am, src/sabatest/defs.in, src/sanity/Makefile.am, src/tgba/Makefile.am, src/tgba/bdddict.cc, src/tgba/bddprint.cc, src/tgba/formula2bdd.cc, src/tgba/state.hh, src/tgba/succiterconcrete.cc, src/tgba/taatgba.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbacomplement.cc, src/tgba/tgbacomplement.hh, src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.cc, src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh, src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh, src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh, src/tgbaalgos/dupexp.cc, src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/emptiness.cc, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh, src/tgbaalgos/powerset.cc, src/tgbaalgos/reachiter.cc, src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh, src/tgbaparse/Makefile.am, src/tgbaparse/tgbaparse.yy, src/tgbatest/Makefile.am, src/tgbatest/bddprod.test, src/tgbatest/complementation.cc, src/tgbatest/complementation.test, src/tgbatest/defs.in, src/tgbatest/dfs.test, src/tgbatest/dupexp.test, src/tgbatest/explicit.cc, src/tgbatest/explicit.test, src/tgbatest/explpro3.test, src/tgbatest/explpro4.test, src/tgbatest/explprod.cc, src/tgbatest/explprod.test, src/tgbatest/ltl2neverclaim.test, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltl2tgba.test, src/tgbatest/ltlprod.cc, src/tgbatest/ltlprod.test, src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test, src/tgbatest/powerset.cc, src/tgbatest/readsave.cc, src/tgbatest/readsave.test, src/tgbatest/reduccmp.test, src/tgbatest/reductgba.cc, src/tgbatest/reductgba.test, src/tgbatest/taatgba.cc, src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test, src/tgbatest/tripprod.cc, src/tgbatest/tripprod.test, wrap/python/cgi/ltl2tgba.in, wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py: Fix copyrights. 2010-01-24 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.cc: More comments. 2010-01-24 Alexandre Duret-Lutz Check that all directories are documented. * src/sanity/readme.test: For each AC_OUTPUT Makefile, check that the directory is documented in README. Also skip non distributed directories in readme.test. * README: Fit on 80 columns. 2010-01-24 Alexandre Duret-Lutz * README: Typo. 2010-01-24 Alexandre Duret-Lutz * src/sanity/Makefile.am (EXTRA_DIST): Distribute readme.test. 2010-01-24 Alexandre Duret-Lutz * README: Add descriptions for subdirectories of bench/, src/sanity, and src/kripke. 2010-01-24 Guillaume Sadegh * src/sanity/readme.test: A script to check whether all the directories referenced in README exist. * src/sanity/Makefile.am: Adjust to call `readme.test' when make check is invoked. 2010-01-24 Guillaume Sadegh Update the README. * README: Reference src/saba/, src/sabaalgos/, src/sabatest/, iface/nips/, iface/nips/nipstest/ and iface/nips/nips_vm/. 2010-01-22 Alexandre Duret-Lutz Turn parse_error_list into an opaque type for Swig. This kills a memory leak warning from swig/python. * src/ltlparse/public.hh (parse_error_list): Declare as an empty struct for Swig. * wrap/python/tests/ltlparse.py: Fix copyright. 2010-01-22 Alexandre Duret-Lutz Fix the computation of the length of multops. * src/ltlvisit/length.cc (visit(multop*)): New function. "a & b & c" has length 5, not 4, even though it is stored as And(a,b,c). This caused reduc.test to fail on some formulae. 2010-01-21 Alexandre Duret-Lutz Please the style checks... * src/tgbaalgos/randomgraph.cc: Fix the copyright and make it fit on 80 columns. 2010-01-21 Alexandre Duret-Lutz * src/ltltest/reduc.cc (main): Fix harmless memory leak introduced today. 2010-01-21 Alexandre Duret-Lutz Fix taa_tgba_formula's destructor. * src/tgba/taatgba.cc (taa_tgba_formula::~taa_tgba_formula): Really destroy all formulae, not only half of them. 2010-01-21 Alexandre Duret-Lutz * src/tgbatest/randtgba.cc: Do not include twice. 2010-01-21 Alexandre Duret-Lutz Speedup reduc.test by not spawning one process per formula. * src/ltltest/reduc.cc: Add an option -f to read a lot of formulae from a file. Running a process for each formula was too slow. Also add an option -h to hide reduced formulae. * src/ltltest/reduc.test: Simplify accordingly. 2010-01-21 Alexandre Duret-Lutz Move the last test from emptchk.test to emptchke.test. * src/tgbatest/emptchk.test: Move the newly added test ... * src/tgbatest/emptchke.test: ... here, with other explicit test. Also test more algorithms. 2010-01-21 Alexandre Duret-Lutz Fix a memory leak in Cou99 statistics. * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::acss_states): Delete the iterator after using it. * src/tgbatest/emptchkr.test: Run 'randtgba -z' with valgrind too. 2010-01-21 Alexandre Duret-Lutz Fix a longstanding bug in our implementation of GV04. * src/tgbaalgos/gv04.cc (push): Fix the tracking of the accepting link. This bug was discovered on a random generated graph with a complex accepting cycle. * src/tgbatest/emptchk.test: Add the troublesome graph as test case. 2010-01-20 Damien Lefortier When iterating a hash_map, be careful not to delete i->first before doing ++i to avoid memory issues. * src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Fix them. 2010-01-20 Damien Lefortier Minor fixes to compile with GCC 3.3 * src/ltlast/automatop.cc, src/ltlast/automatop.hh: Rename nfa as get_nfa to avoid a name clash with the `nfa' class. * src/ltlvisit/clone.cc, src/ltlvisit/nenoform.cc, src/ltlvisit/tostring.cc, src/tgbaalgos/eltl2tgba_lacim.cc: Use get_nfa instead of nfa. * src/tgba/tgbasafracomplement.cc: Don't use a const_reverse_iterator. 2010-01-20 Alexandre Duret-Lutz Remove some non-determinism in random_graph() * src/tgbaalgos/randomgraph.cc (random_graph): Revert the part of the patch from 2007-02-06 which silently replaced the use of state index by state pointers. Storing states pointer in this map cause some non-determinism because of the memory layout. It was almost impossible to reproduce bugs found by tests based on randtgba. 2010-01-19 Damien Lefortier * src/tgbaalgos/ltl2taa.cc: Fix the previous patch. 2010-01-18 Damien Lefortier * src/tgba/taatgba.cc, src/tgba/taatgba.hh: Fix memory issues occuring when labels are pointers. * src/tgbaalgos/ltl2taa.cc: Fix a bug. * src/tgbatest/ltl2tgba.cc: Fix a bug. 2010-01-16 Guillaume Sadegh * src/saba/sabacomplementtgba.cc: Fix a bug. 2010-01-16 Damien Lefortier Use taa_tgba_formula instead of taa_tgba_string in ltl_to_taa to speed up a little the translation. * src/tgbaalgos/ltl2taa.cc: Adjust. Also fix a bug with acceptance conditions in all_n_tuples. * src/tgba/taatgba.cc, src/tgba/taatgba.hh: Adjust. 2010-01-16 Damien Lefortier Introduce taa_tgba_labelled