- 26 Aug, 2013 10 commits
-
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/postproc.cc: Use tba_determinize_check() if option "tba-det" is set. * src/tgbaalgos/postproc.hh (tba_determinize_): New attribute. * src/tgbatest/det.test: New file. * src/tgbatest/Makefile.am (TESTS): Add it.
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh (dba_determinize, dba_determinize_check): Add a threshold argument. * src/tgbatest/ltl2tgba.cc (-O, -RQ): Accept a threshold argument.
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh (tba_determinize_check): New function. * src/tgbatest/ltl2tgba.cc (-O): Use it.
-
Alexandre Duret-Lutz authored
Loosely based on "Complementing Deterministic Büchi Automata in Polynomial Time", R. P. Kurshan, 1987, J. Comp. Syst. Sci. 35. * src/tgbaalgos/dbacomp.cc, src/tgbaalgos/dbacomp.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatest/ltl2tgba.cc (-DC): New option to test it.
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/powerset.hh, src/tgbaalgos/powerset.cc (tba_determinize): New function. * src/tgbatest/ltl2tgba.cc (-RQ): New option, for testing.
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/reachiter.hh, src/tgbaalgos/reachiter.cc: Fix the tgba_reachable_iterator_depth_first implementation by not making inheriting from tgba_reachable_iterator. Add a tgba_reachable_iterator_depth_first_stack * src/tgbatest/sim.test, src/tgbatest/dstar.test: Adjust.
-
Alexandre Duret-Lutz authored
For example to interface with Rabinizer, we can now use 'java -jar /pathto/Rabinizer.jar -ltl2dstar %F %D; mv %D.dst %D' because Rabinizer always append a suffix to its last argument, we rename the file... * src/bin/ltlcross.cc (printable_result_filename): Adjust.
-
Alexandre Duret-Lutz authored
* doc/org/dstar2tgba.org: New file. * doc/org/tools.org: Link to it. * doc/Makefile.am: Distribute it. * NEWS: Mention the generated web page.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
Extended former conversion from DRA->DBA to handle the case where some SCC is not DBA-realizable. * src/dstarparse/dra2dba.cc: Rename as... * src/dstarparse/dra2ba.cc: ... this. (dra_to_dba, dra_to_dba_worker): Rename as... (dra_to_ba, dra_to_ba_worker): ... these and extend. * src/dstarparse/Makefile.am, src/dstarparse/public.hh, src/dstarparse/dstar2tgba.cc, src/dstarparse/nra2nba.cc: Adjust. * NEWS: Update the description of dstar2tgba accordingly.
-
- 23 Aug, 2013 10 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/bin/dstar2tgba.cc, src/bin/man/dstar2tgba.x: New files. * src/bin/Makefile.am, src/bin/man/Makefile.am: Add them. * NEWS: Mention it. * src/bin/ltl2tgba.cc, src/tgbaalgos/stats.cc, doc/org/ltl2tgba.org: Rename the %S sequence as %c, for consistency with dstar2tgba. * src/tgbatest/ltl2dstar.test: Add more tests. * src/tgbatest/ltl2dstar2.test: New file. * src/tgbatest/Makefile.am: Add it.
-
Alexandre Duret-Lutz authored
This is an implementation of Krishnan's ISAAC'94 paper to convert deterministic Rabin automata into DBA when possible. * src/dstarparse/dra2dba.cc: New file. * src/dstarparse/dstar2tgba.cc: New file. * src/dstarparse/Makefile.am: Add them. * src/dstarparse/nra2nba.cc (nra_to_nba): Adjust so that dra_to_dba() can call it using a masked automaton. * src/dstarparse/public.hh (dra_to_dba, dstar_to_tgba): Declare. * src/tgbatest/ltl2tgba.cc: Add an -XDD option. * src/tgbatest/dstar.test: More tests.
-
Alexandre Duret-Lutz authored
* src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh: New files. * src/tgba/Makefile.am: Add them. * src/tgbatest/explicit3.cc, src/tgbatest/explicit3.test: New files. * src/tgbatest/Makefile.am: Add them.
-
Alexandre Duret-Lutz authored
* src/tgba/state.hh: Define state_set and shared_state_set. * src/tgba/taatgba.cc, src/tgba/taatgba.hh: Rename the existing state_set (that inherits from spot::state) as set_state. * src/tgba/tgbakvcomplement.cc: Use shared_state_set instead of state_set. * src/tgbaalgos/minimize.cc (state_set): Rename as... (build_state_set): ... this.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/bin/ltlcross.cc: Add support for %D. * src/bin/man/ltlcross.x: Add example. * NEWS: Mention it. * src/tgbatest/ltl2dstar.test: New file. * src/tgbatest/Makefile.am: Add it.
-
Alexandre Duret-Lutz authored
Supports reading Rabin and Streett automata, and converting them to nondeterministic Büchi automata (for Rabin) or TGBA (for Streett). * src/dstarparse/Makefile.am, src/dstarparse/dstarparse.yy, src/dstarparse/dstarscan.ll, src/dstarparse/fmterror.cc, src/dstarparse/parsedecl.hh, src/dstarparse/public.hh, src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc: New files. * configure.ac, src/Makefile.am, README: Adjust. * src/tgbatest/ltl2tgba.cc: Add options -XD, -XDB. * src/tgbatest/dstar.test: New file. * src/tgbatest/Makefile.am (TESTS): Add it.
-
Alexandre Duret-Lutz authored
* src/misc/bitvect.cc, src/misc/bitvect.hh: New files. * src/misc/Makefile.am: Add them. * src/tgbatest/bitvect.cc, src/tgbatest/bitvect.test: New files. * src/tgbatest/Makefile.am: Add them.
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/degen.cc: Choose the initial level according to acceptance condition common to all outgoing transitions. * src/tgbatest/degenid.test: Add test case. * NEWS: Mention it.
-
- 21 Aug, 2013 2 commits
-
-
Alexandre Duret-Lutz authored
* m4/gccoptim.m4: Typo.
-
Alexandre Duret-Lutz authored
* configure.ac (CXXFLAGS): Add -DSPOT_BUILD regardless of whether -fvisibility-inlines-hidden is supported.
-
- 29 Jul, 2013 18 commits
-
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/word.cc, src/tgbaalgos/word.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatest/ltlcrossce.test: New file. * src/tgbatest/Makefile.am: Add it. * src/bin/ltlcross.cc: Compute and display an accepted word for nonempty cross-products. * NEWS, doc/org/ltlcross.org: Document it.
-
Alexandre Duret-Lutz authored
* src/misc/tmpfile.cc: Check these environment variables. * src/bin/man/ltlcross.x, NEWS: Document them.
-
Alexandre Duret-Lutz authored
* tools/test-driver-teamcity: New file. * Makefile.am: Distribute it. * HACKING: Document it. * wrap/python/tests/Makefile.am: Use it also for Python tests.
-
Alexandre Duret-Lutz authored
* src/bin/ltlcross.cc: Use features introduced by misc/tmpfile.hh.
-
Alexandre Duret-Lutz authored
* lib/mkstemps.c, m4/mkstemps.m4: New files. * lib/Makefile.am, m4/gnulib-cache.m4, m4/gnulib-comp.m4: Update.
-
Alexandre Duret-Lutz authored
It cause issues when <ctime> latter undefine the gmtime/localtime macros to access the real function. * lib/Makefile.am, lib/time.in.h, m4/gettimeofday.m4, m4/time_h.m4: These changes are mostly based on the patch posted in http://permalink.gmane.org/gmane.comp.lib.gnulib.bugs/29229 but with the prototype of gmtime() and localtime() fixed.
-
Alexandre Duret-Lutz authored
* lib/.gitignore, lib/c-ctype.h, lib/msvc-inval.c, lib/stdalign.in.h, lib/vasnprintf.c, lib/verify.h, m4/extern-inline.m4, m4/stdalign.m4: Update.
-
Alexandre Duret-Lutz authored
This is needed now that lib/ is in the include path. * src/misc/bareword.cc, src/misc/bddop.cc, src/misc/escape.cc, src/misc/formater.cc, src/misc/intvcmp2.cc, src/misc/intvcomp.cc, src/misc/memusage.cc, src/misc/minato.cc, src/misc/optionmap.cc, src/misc/random.cc, src/misc/timer.cc, src/misc/version.cc: Include config.h.
-
Alexandre Duret-Lutz authored
* src/misc/tmpfile.cc, src/misc/tmpfile.hh: New files. * src/misc/Makefile.am: Add them * src/Makefile.am: Link with gnulib for mkstemp and mkstemps.
-
Alexandre Duret-Lutz authored
* lib/stpcpy.c, m4/stpcpy.m4: New files. * lib/Makefile.am, m4/gnulib-cache.m4, m4/gnulib-comp.m4: Update.
-
Alexandre Duret-Lutz authored
* src/bin/ltlcross.cc: Add a --color option. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
* lib/argmatch.c, lib/argmatch.h, lib/c-ctype.c, lib/c-ctype.h, lib/config.charset, lib/c-strcasecmp.c, lib/c-strcaseeq.h, lib/c-strcase.h, lib/c-strncasecmp.c, lib/exitfail.c, lib/exitfail.h, lib/isatty.c, lib/localcharset.c, lib/localcharset.h, lib/mbrtowc.c, lib/mbsinit.c, lib/quotearg.c, lib/quotearg.h, lib/quote.h, lib/ref-add.sin, lib/ref-del.sin, lib/streq.h, lib/wctype-h.c, lib/wctype.in.h, lib/xalloc-die.c, lib/xalloc.h, lib/xalloc-oversized.h, lib/xmalloc.c, m4/codeset.m4, m4/configmake.m4, m4/glibc21.m4, m4/isatty.m4, m4/localcharset.m4, m4/locale-fr.m4, m4/locale-ja.m4, m4/locale-zh.m4, m4/mbrtowc.m4, m4/mbsinit.m4, m4/mbstate_t.m4, m4/quotearg.m4, m4/quote.m4, m4/wctype_h.m4, m4/xalloc.m4: New files. * lib/Makefile.am, m4/gnulib-cache.m4, m4/gnulib-comp.m4: Update.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/postproc.cc: Move the count_state() function... * src/priv/countstates.cc, src/priv/countstates.hh: ... in these new files. * src/priv/Makefile.am: Add them. * src/saba/sabacomplementtgba.cc, src/tgba/tgbakvcomplement.cc, src/tgbaalgos/minimize.cc: Use count_states() instead of stats_reachable().
-
Alexandre Duret-Lutz authored
* configure.ac: Check for flags and fill CXXFLAGS and CFLAGS. * iface/dve2/dve2.hh: Mark load_dve2 for export. * src/eltlparse/Makefile.am, src/kripke/Makefile.am, src/kripkeparse/Makefile.am, src/ltlast/Makefile.am, src/ltlenv/Makefile.am, src/ltlparse/Makefile.am, src/ltlvisit/Makefile.am, src/misc/Makefile.am, src/neverparse/Makefile.am, src/priv/Makefile.am, src/saba/Makefile.am, src/sabaalgos/Makefile.am, src/ta/Makefile.am, src/taalgos/Makefile.am, src/tgba/Makefile.am, src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/Makefile.am, src/tgbaparse/Makefile.am: Remove $(VISIBILITY_CXXFLAGS) now that it is set globally.
-