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