alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Commit graph

  • e7bc4f2a5a * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run, couvreur99_check_result::complete_cycle, couvreur99_check_result::accepting_path): Record conditions and acceptance conditions in the accepting run. Simplify the todo BFS stack for accepting_run and complete_cycle. * src/tgbatest/ltl2tgba.cc (main): Do use replay_tgba_run now everything works. * src/tgbaalgos/replayrun.cc (replay_tgba_run): Be more verbose when an outgoing transition is not found. Alexandre Duret-Lutz 2004-10-29 00:30:09 +00:00
  • 35a286ba41 * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc (magic_search): Record the acceptance conditions in the accepting run. * src/tgbaalgos/replayrun.cc (replay_tgba_run): Fix logic. Alexandre Duret-Lutz 2004-10-28 22:02:53 +00:00
  • 7819f14db2 * src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh: New files. Cannot test them because the run returned by the emptiness checks are currently incomplete (they lack the acceptance conditions, and sometimes even the labels in the prefix). * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them. * src/tgbatest/ltl2tgba.cc (main): Prepare to use replay_tgba_run when the emptiness checks are fixed. Alexandre Duret-Lutz 2004-10-28 12:10:12 +00:00
  • 6c815004c4 Introduce an emptiness-check interface, and modify the existing algorithms to conform to it, uniformly. This will unfortunately break third-party code that were using these algorithms. * src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: New files. * src/tgbaalgos/Makefile.am: New files. * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh: Adjust to conform to the new emptiness-check interface. * src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh: Likewise. The classes have been renamed are as following emptiness_check -> couvreur99_check emptiness_check_shy -> couvreur99_check_shy counter_example -> couvreur99_check_result * src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh, iface/gspn/ssp.cc: Adjust to renaming and new interface. Alexandre Duret-Lutz 2004-10-27 16:47:54 +00:00
  • 7010a02cd9 * src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaalgos/tgba2evtgba.hh: New files. * src/evtgbaalgos/Makefile.am (evtgbaalgos_HEADERS, libevtgbaalgos_la_SOURCES): Add them. * src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/ltl2evtgba.test: New files. * src/evtgbatest/Makefile.am (check_PROGRAMS, TESTS): Add them. (ltl2evtgba_SOURCES): New variable. Alexandre Duret-Lutz 2004-10-27 11:18:13 +00:00
  • b89f1e252e * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Do not assert that the true state has only one link when unobs is used. Alexandre Duret-Lutz 2004-10-27 11:13:52 +00:00
  • 0864d1ca1e * src/evtgbatest/Makefile.am (CLEANFILES): New variable. Alexandre Duret-Lutz 2004-10-23 07:49:08 +00:00
  • 73ff928b6f Preliminary support for Event-based GBA. * src/evtgba/Makefile.am, src/evtgba/evtgba.cc, src/evtgba/evtgba.hh, src/evtgba/evtgbaiter.hh, src/evtgba/explicit.cc, src/evtgba/explicit.hh, src/evtgba/product.cc, src/evtgba/product.hh, src/evtgba/symbol.cc, src/evtgba/symbol.hh, src/evtgbaalgos/Makefile.am, src/evtgbaalgos/dotty.cc, src/evtgbaalgos/dotty.hh, src/evtgbaalgos/reachiter.cc, src/evtgbaalgos/reachiter.hh, src/evtgbaalgos/save.cc, src/evtgbaalgos/save.hh, src/evtgbaparse/Makefile.am, src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll, src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh, src/evtgbaparse/public.hh, src/evtgbatest/Makefile.am, src/evtgbatest/defs.in, src/evtgbatest/explicit.cc, src/evtgbatest/explicit.test, src/evtgbatest/product.cc, src/evtgbatest/product.test, src/evtgbatest/readsave.cc, src/evtgbatest/readsave.test: New files. * configure.ac: Create the Makefiles in these new subdirectories. * src/Makefile.am: Recurse them. Alexandre Duret-Lutz 2004-10-22 16:22:31 +00:00
  • d9b29a0590 * src/misc/bareword.hh, src/misc/bareword.cc (quote_unless_bare_word): New function. Alexandre Duret-Lutz 2004-10-22 16:06:55 +00:00
  • 38f7cac8dd * src/ltlvisit/tostring.cc (to_spin_string_visitor): Move to anonymous namespace. Alexandre Duret-Lutz 2004-10-22 12:29:13 +00:00
  • 91b9682bd8 * wrap/python/Makefile.am (_spot_la_SOURCES): Add spot_wrap.h. Alexandre Duret-Lutz 2004-10-21 11:01:27 +00:00
  • 55b84b1a48 * src/misc/modgray.hh (loopless_modular_mixed_radix_gray_code::done, loopless_modular_mixed_radix_gray_code::last): Declare as const. Alexandre Duret-Lutz 2004-10-20 16:04:06 +00:00
  • 4defec66b4 * src/misc/bareword.hh, src/misc/bareword.cc: New files. * src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them. Alexandre Duret-Lutz 2004-10-20 15:50:52 +00:00
  • 094ddca665 * src/misc/modgray.hh, src/misc/modgray.cc: New files. * src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them. * wrap/python/spot.i: Activate directors, and interface modgray.hh. * wrap/python/tests/modgray.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add it. Alexandre Duret-Lutz 2004-10-20 15:46:56 +00:00
  • 7d27fd3796 * iface/gspn/gspn.cc, src/ltlvisit/basicreduce.cc, src/ltlvisit/destroy.cc, src/ltlvisit/dotty.cc, src/ltlvisit/dump.cc, src/ltlvisit/length.cc, src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc, src/tgba/tgbabddconcreteproduct.cc, src/tgba/tgbatba.cc, src/tgbaalgos/dotty.cc, src/tgbaalgos/dupexp.cc, src/tgbaalgos/lbtt.cc, src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/save.cc, src/tgbaalgos/stats.cc, src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh: Declare private classes and helper function in anonymous namespaces. * HACKING, src/sanity/style.test: Document and check this. Also check for trailing { after namespace or class. * src/ltlast/predecl.hh, src/ltlast/visitor.hh, src/tgba/tgbareduc.hh: Fix trailing {. Alexandre Duret-Lutz 2004-10-18 13:56:31 +00:00
  • 5176caf4d2 * src/tgbaalgos/gtec/ce.cc: Reinstall change from 2004-09-21. Alexandre Duret-Lutz 2004-10-15 13:33:50 +00:00
  • ed6db92642 Back out all Thomas's changes on emptiness checks since 2004-08-23. Some of these will need to be reintegrated more slowly and cleanly. Alexandre Duret-Lutz 2004-10-15 10:33:55 +00:00
  • 01987350b7 * src/ltltest/reduc.test: Do source ./defs. Revert mistaken change from 2004-09-13. Alexandre Duret-Lutz 2004-10-14 12:57:12 +00:00
  • 2a2c630bfa * src/tgbatest/explicit.test: Typo. Alexandre Duret-Lutz 2004-10-14 12:21:48 +00:00
  • e8e2bec243 The computation of the counter example fails the valgrind tests and is wrong into two ways: the search stack is generally not a path, and does not run until the end of the STL container. Remove it. * src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh (tarjan_on_fly): Do not inherit from the emptiness_search class, because the check method will no longer return a counter example. (tarjan_on_fly::check): Return only a boolean. (tarjan_on_fly::build_counter): Delete. * src/tgbatest/ltl2tgba.cc: Adjust. Alexandre Duret-Lutz 2004-10-13 17:39:27 +00:00
  • ca27267c69 * src/tgba/tgbaexplicit.cc (tgba_explicit_succ_iterator::current_state, tgba_explicit_succ_iterator::current_condition, tgba_explicit_succ_iterator::current_accepting_conditions): Assert the iteration is not finished. Alexandre Duret-Lutz 2004-10-13 14:32:05 +00:00
  • d647e7a0db * wrap/python/tests/run.in: Typo. From Akim Demaille. Alexandre Duret-Lutz 2004-10-12 07:41:19 +00:00
  • 7bcd027712 * configure.ac: Empty CFLAGS and CXXFLAGS. * m4/debug.m4: Update CXXFLAGS too. Alexandre Duret-Lutz 2004-10-11 12:32:49 +00:00
  • 6e40095471 * doc/Doxyfile.in: Upgrade to Doxygen 1.3.9. Alexandre Duret-Lutz 2004-10-08 13:57:49 +00:00
  • 8b3bfaacdb * src/sanity/style.test: Suggest using "x->y", not "(*x).y". * src/tgbaalgos/tarjan_on_fly.cc: Fix. Alexandre Duret-Lutz 2004-09-27 14:57:37 +00:00
  • 2c0a2cd517 typo Alexandre Duret-Lutz 2004-09-27 13:02:53 +00:00
  • 3f2cba6304 * src/sanity/style.test: Suggest ++i over i++ when it does not matter, for consistency. * src/tgbaalgos/tarjan_on_fly.cc, iface/gspn/ssp.cc, src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/minimalce.cc, src/tgba/tgbareduc.cc: Adjust. Alexandre Duret-Lutz 2004-09-23 12:20:10 +00:00
  • 3780650ea0 * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): New unobs argument. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Handle unobs. * src/tgbatest/ltl2tgba.cc (syntax, main): New -U option. Alexandre Duret-Lutz 2004-09-23 11:56:43 +00:00
  • a59b9aa7f4 * src/tgbaalgos/colordfs.hh, src/tgbaalgos/minimalce.cc, src/tgbaalgos/minimalce.hh, src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/tarjan_on_fly.hh, src/tgbatest/ltl2tgba.cc: Rename emptyness_search to emptiness_search. Alexandre Duret-Lutz 2004-09-21 15:19:26 +00:00
  • c30823f7be * src/sanity/style.test: Warn about places where size() is used instead of empty(). * src/misc/bddalloc.cc (bdd_allocator::extend): Use empty() rather than size() when checking emptiness of lists. * src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/minimalce.cc, src/ltlvisit/basicreduce.cc, src/ltlvisit/reduce.cc, src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/misc/minato.cc: Likewise. * src/ltlast/multop.cc (multop::instance): Call ->size() only once. Alexandre Duret-Lutz 2004-09-21 13:01:27 +00:00
  • f0aa58034c Update to SWIG 1.3.22. * wrap/python/libpy.c: Delete. * wrap/python/swigpy.i: New file. * wrap/python/Makefile.am (swigpy_wrap.c): Build this from swigpy.i and use it instead of libpy.c. Alexandre Duret-Lutz 2004-09-20 16:35:46 +00:00
  • b4065d9083 * INSTALL, lbtt/INSTALL: New upstream version. Alexandre Duret-Lutz 2004-09-20 15:05:44 +00:00
  • 314f51ac55 * src/tgbatest/emptchk.test src/tgbaalgos/tarjan_on_fly.hh, src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/minimalce.hh, src/tgbaalgos/minimalce.cc: To correct a bug. martinez 2004-09-14 16:11:14 +00:00
  • ad71da0042 * src/ltltest/reduc.test (FICH): bad file name. martinez 2004-09-14 11:51:56 +00:00
  • 0e5ca8a586 * src/tgbaalgos/nesteddfsgen.hh src/tgbaalgos/nesteddfsgen.cc: New algorithm for emptiness check. martinez 2004-09-13 15:47:33 +00:00
  • 5af687b2c8 * src/tgbatest/spotlbtt.test, src/tgbatest/reductgba.cc, src/tgbatest/ltl2tgba.cc: Add option for reduction of TGBA. martinez 2004-09-13 15:25:13 +00:00
  • 2d1151e018 * src/tgbaalgos/tarjan_on_fly.hh, src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/minimalce.hh, src/tgbaalgos/minimalce.cc, src/tgbaalgos/colordfs.hh, src/tgbaalgos/colordfs.cc: four new algorithms for emptyness check. martinez 2004-08-23 12:48:33 +00:00
  • 3d2135c883 * configure.ac, NEWS: Bump version to 0.0y. Alexandre Duret-Lutz 2004-08-13 13:32:46 +00:00
  • 280ad8d756 * configure.ac, NEWS: Bump version to 0.0x. Alexandre Duret-Lutz 2004-08-13 13:18:10 +00:00
  • 4531700d36 * doc/Doxyfile.in (GENERATE_TAGFILE): Build spot.tag. * doc/Makefile.am (dist_pkgdata_DATA): Add spot.tag. Alexandre Duret-Lutz 2004-08-12 16:48:08 +00:00
  • 8f502a8e32 * src/tgbatest/ltl2tgba.cc (syntax): Typo. Alexandre Duret-Lutz 2004-08-12 14:45:07 +00:00
  • 15785496d8 * doc/Doxyfile.in (STRIP_FROM_PATH): Strip @srcdir@ so its does not appear when listing mainpage.dox. Alexandre Duret-Lutz 2004-08-12 14:25:49 +00:00
  • 59947d11cf * src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh: Typos in Doxygen comments. Alexandre Duret-Lutz 2004-08-11 09:05:27 +00:00
  • 42fc2b772f * src/ltlvisit/apcollect.hh: Fix include guard. Report from Denis. * src/sanity/includes.test: Include files twice to check include guards. Alexandre Duret-Lutz 2004-08-10 18:07:20 +00:00
  • 11762deafc * src/tgbatest/ltl2tgba.cc (main): Fix another gcc warning in case assert() is disabled. Alexandre Duret-Lutz 2004-08-10 16:01:14 +00:00
  • 7818321589 * src/Makefile.am (nodist_EXTRA_libspot_la_SOURCES): New variable, to force C++ linking. Alexandre Duret-Lutz 2004-08-10 15:52:21 +00:00
  • fb8618b708 * iface/gspn/ltlgspn.cc: Fix a gcc warning in case assert() is disabled. Alexandre Duret-Lutz 2004-08-10 10:33:18 +00:00
  • 79ef47dbf1 * src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh: New files, based on code from <Denis.Poitrenaud@lip6.fr>. * src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES, ltlvisit_HEADERS): Add them. Alexandre Duret-Lutz 2004-08-09 16:55:08 +00:00
  • ad96e8fbad * iface/gspn/common.cc, iface/gspn/common.hh, src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh, src/ltlparse/fmterror.cc, src/ltlparse/public.hh, src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh, src/ltlvisit/dump.cc, src/ltlvisit/dump.hh, src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh, src/misc/escape.cc, src/misc/escape.hh, src/tgba/bdddict.cc, src/tgba/bdddict.hh, src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh, src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh, src/tgbaalgos/save.cc, src/tgbaalgos/save.hh, src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh, src/tgbaparse/fmterror.cc, src/tgbaparse/public.hh: Include <iosfwd> in headers, and prefer <ostream> in the body whenever possible. * src/sanity/style.test, HACKING: Check and document this. Alexandre Duret-Lutz 2004-08-09 16:32:25 +00:00
  • 6853977be2 * src/ltlast/allnodes.hh, src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/multop.hh, src/ltlast/predecl.hh, src/ltlast/refformula.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh: Use file to introduce each file. Alexandre Duret-Lutz 2004-08-09 13:43:55 +00:00
  • 04fc0b986f * doc/Doxyfile.in (STRIP_FROM_INC_PATH): Define, so that the `#include' references are correct. Alexandre Duret-Lutz 2004-08-09 13:40:09 +00:00
  • 01566183d8 * README: Update. Alexandre Duret-Lutz 2004-08-09 09:41:00 +00:00
  • e94f297ba3 * m4/gccoptim.m4: Compute optimization flags for CXX too. Alexandre Duret-Lutz 2004-08-09 09:14:15 +00:00
  • 50ed9f8c0b * m4/ndebug.m4: Update CPPFLAGS, not CFLAGS. Alexandre Duret-Lutz 2004-08-09 08:51:39 +00:00
  • 576e00099d * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Document all parameters. * src/tgbaalgos/ltl2tgba_lacim.hh (ltl_to_tgba_lacim): Likewise. Alexandre Duret-Lutz 2004-08-09 08:50:42 +00:00
  • 7b314789ca * configure.ac: Call AC_PROG_CC and AM_PROG_CC_C_O. * wrap/python/Makefile.am (_buddy_la_LDFLAGS): Move libspotswigpy.la ... (_buddy_la_LIBADD): ... here. Alexandre Duret-Lutz 2004-08-07 22:11:45 +00:00
  • f3dc612d64 * lbtt/: Merge lbtt 1.1.2. Alexandre Duret-Lutz 2004-08-02 09:02:19 +00:00
  • e4befcecc7 Import of lbtt 1.1.2 Alexandre Duret-Lutz 2004-08-02 08:59:00 +00:00
  • 70597c3f51 * lbtt/: Merge lbtt 1.1.1. Alexandre Duret-Lutz 2004-07-30 11:50:08 +00:00
  • 894050ed90 Import of lbtt 1.1.1 Alexandre Duret-Lutz 2004-07-30 11:37:46 +00:00
  • 3d6a75ecfa * doc/Doxyfile.in: Update for Doxygen 1.3.8. Alexandre Duret-Lutz 2004-07-26 12:15:49 +00:00
  • 9bdefd34e7 * configure.ac: Call AC_LIBTOOL_WIN32_DLL * src/Makefile.am (libspot_la_LDFLAGS): Add -no-undefined. Alexandre Duret-Lutz 2004-07-23 09:08:45 +00:00
  • 3b693c5ca7 * configure.ac: Call AC_LIBTOOL_WIN32_DLL * src/Makefile.am (libbdd_la_LDFLAGS): Add -no-undefined. Alexandre Duret-Lutz 2004-07-23 09:07:49 +00:00
  • 89db9aa512 * src/Makefile.am (libbdd_la_LDFLAGS): Add -no-undefined. Alexandre Duret-Lutz 2004-07-23 09:06:54 +00:00
  • f6174b7f5e * src/tgbatest/explicit.test: Do not use -i', it's not needed and it is wrong to put it after -e'. Caught by Denis too. Alexandre Duret-Lutz 2004-07-22 14:26:51 +00:00
  • 3ec8a99b24 * src/ltltest/reduc.test: Use test a = b' not test a == b'. Reported by <Denis.Poitrenaud@lip6.fr> (failure on Cygwin). Alexandre Duret-Lutz 2004-07-22 13:53:51 +00:00
  • df75d35a5a * src/tgbatest/defs.in (VALGRIND): Specify --tool=memcheck for compatibility with valgrind 2.1.x. * src/ltltest/defs.in (VALGRIND): Likewise. Alexandre Duret-Lutz 2004-07-20 15:47:30 +00:00
  • f84dd2e72c * configure.ac: Call AC_GNU_SOURCE to make glibc's strsignal definition visible even to non-GNU compilers. Alexandre Duret-Lutz 2004-07-19 08:54:37 +00:00
  • 85d2b7b287 * configure.ac: Call AC_GNU_SOURCE to make glibc's strsignal definition visible even to non-GNU compilers. Alexandre Duret-Lutz 2004-07-16 16:25:38 +00:00
  • b4eda5e84d * m4/gccwarn.m4: Do not check nor use -Wstrict-prototypes. g++-3.4 complains it makes no sense in C++. Alexandre Duret-Lutz 2004-07-16 14:38:44 +00:00
  • bec7402a67 * iface/gspn/ssp.cc: Typos. Alexandre Duret-Lutz 2004-07-16 11:52:19 +00:00
  • 44ebe5a746 * iface/gspn/gspn.cc (tgba_succ_iterator_gspn::tgba_succ_iterator_gspn): Set size_ to 1 when stuttering is needed, so that done() does not return true immediately. Alexandre Duret-Lutz 2004-07-16 11:19:28 +00:00
  • 7abc2604f3 * examples/bddcalc/parser.yxx (actionSeq, varlist): Rewrite as left-recursive rules. Alexandre Duret-Lutz 2004-07-12 14:03:53 +00:00
  • 4cbc1d8856 * src/tgbaalgos/gtec/gtec.hh: Typos in comments. Alexandre Duret-Lutz 2004-07-12 11:16:12 +00:00
  • 844b17a211 * src/tgba/state.hh (state_ptr_equal, state_ptr_hash): Fix Doxygen example. Alexandre Duret-Lutz 2004-07-09 15:17:41 +00:00
  • 1aad1ffbfd * src/tgbaalgos/reductgba_sim.hh (parity_game_graph_delayed, reduc_tgba_sim): Fix warnings about Doxygen comment. * src/ltlvisit/reduce.hh (reduce): Likewise. Alexandre Duret-Lutz 2004-07-09 15:12:35 +00:00
  • c534bac478 * doc/footer.html: New file, link to RefDocComments on the wiki. * doc/Doxyfile.in (HTML_FOOTER): Use footer.html. * doc/Makefile.am (EXTRA_DIST): Add footer.html. Alexandre Duret-Lutz 2004-07-09 14:51:56 +00:00
  • 61a5ec760e typos Alexandre Duret-Lutz 2004-07-09 13:08:42 +00:00
  • 0f304df2ed * THANKS: Fill in. Alexandre Duret-Lutz 2004-07-09 13:06:33 +00:00
  • 019bdef8ff * src/tgbatest/ltl2baw.pl: Do not use -T anymore. Fix comments. Alexandre Duret-Lutz 2004-07-09 12:54:08 +00:00
  • 3b85646638 lbtt 1.1.0 supports TGBAs, use that and remove old workarounds. * src/tgbaalgos/lbtt.cc (state_acc_pair, state_acc_pair_equal, state_acc_pair_hash, acp_seen_map, todo_set, seen_map, fill_todo lbtt_reachable): Remove. (nonacceptant_lbtt_bfs): Rename as ... (lbtt_bfs): ... this, and adjust to output acceptance conditions on transitions. (nonacceptant_lbtt_reachable): Rename as ... (lbtt_reachable): ... this. * src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): Delete. * src/tgbatest/ltl2tgba.cc: Suppress option "-T". Alexandre Duret-Lutz 2004-07-08 16:42:00 +00:00
  • 59df610023 Patch from Heikki Tauriainen <heikki.tauriainen@hut.fi>. * src/tgbaalgos/gtec/ce.cc (counter_example::counter_example): Do not parenthesize the type after the new operator (g++ 3.4 complains). * src/tgbaalgos/dupexp.cc (dupexp_iter::process_state, dupexp_iter::declare_state): Use this->automata_ instead of automata_.   Local member automata_ inherited from template base classes must be prefixed or g++ 3.4 will not look them up (conforming to §14.6.2.3). Alexandre Duret-Lutz 2004-07-08 14:50:46 +00:00
  • e11da2e3af * lbtt/: Merge lbtt 1.1.0. * src/tgbatest/spotlbtt.test: Adjust config file syntax to please lbtt 1.1.0. Alexandre Duret-Lutz 2004-07-07 17:41:42 +00:00
  • d7b3d97422 Import of lbtt 1.1.0 Alexandre Duret-Lutz 2004-07-07 16:40:50 +00:00
  • cfdd81a919 Initial revision Alexandre Duret-Lutz 2004-07-07 16:40:50 +00:00
  • 478844dad8 * src/tgbaalgos/gtec/gtec.hh (emptiness_check_shy::find_state): Add comments. * iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Likewise. Soheib and I had a hard time figuring why we did this... Alexandre Duret-Lutz 2004-07-07 12:00:11 +00:00
  • f1c3af808f Merge BuDDy 2.3. * examples/calculator/, examples/internal/: Were renamed as ... * examples/bddcalc/, examples/bddtest/: ... these. * configure.ac: Adjust version and output Makefiles. * examples/Makefile.am (SUBDIRS): Adjust subdir renaming. * examples/cmilner/milner.c, examples/fdd/statespace.cxx: Were renamed as ... * examples/cmilner/cmilner.c, examples/fdd/fdd.cxx: ... these. * examples/cmilner/Makefile.am, examples/fdd/Makefile.am: Adjust accordingly. * src/Makefile.am (AM_CPPFLAGS): Define VERSION. Alexandre Duret-Lutz 2004-07-06 17:39:37 +00:00
  • 9ce6888872 * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim_del.cc: Remove some comments. martinez 2004-07-05 16:03:26 +00:00
  • 7ff3898139 * configure.ac, NEWS: Bump version to 0.0w. Alexandre Duret-Lutz 2004-06-29 18:24:17 +00:00
  • 31b163dbf8 * configure.ac, NEWS: Bump version to 0.0v. Alexandre Duret-Lutz 2004-06-29 18:22:13 +00:00
  • 8be67c1976 * src/tgbatest/reduccmp.test: Bug. martinez 2004-06-28 15:53:20 +00:00
  • acee9e75a4 * buddy/: Merge buddy-2-3. Alexandre Duret-Lutz 2004-06-28 15:25:13 +00:00
  • aa4a582f1b Merge BuDDy 2.3. * examples/calculator/, examples/internal/: Were renamed as ... * examples/bddcalc/, examples/bddtest/: ... these. * configure.ac: Adjust version and output Makefiles. * examples/Makefile.am (SUBDIRS): Adjust subdir renaming. * examples/cmilner/milner.c, examples/fdd/statespace.cxx: Were renamed as ... * examples/cmilner/cmilner.c, examples/fdd/fdd.cxx: ... these. * examples/cmilner/Makefile.am, examples/fdd/Makefile.am: Adjust accordingly. * src/Makefile.am (AM_CPPFLAGS): Define VERSION. Alexandre Duret-Lutz 2004-06-28 15:22:11 +00:00
  • 805b6fb70b Initial revision Alexandre Duret-Lutz 2004-06-28 14:19:59 +00:00
  • 0f79043b2a * src/tgbatest/ltl2tgba.cc (main): Degeneralize before the simulations. Alexandre Duret-Lutz 2004-06-25 11:33:48 +00:00
  • e9fd27e892 * src/ltlvisit/tostring.cc (is_bare_word): New function. (to_string_visitor::visitor(const atomic_prop*)): Use is_bare_word to better check which atomic proposition need to be quoted. * src/ltlparse/ltlscan.ll: Do not allow identifiers starting with F_ or G_. * src/ltltest/equals.test, src/ltltest/tostring.test: More tests. Alexandre Duret-Lutz 2004-06-23 11:36:03 +00:00
  • 3802528bfd * src/tgba/tgbatba.cc (tgba_tba_proxy::format_state): Use bdd_format_accset to print the acceptance condition part of the state. That produces more readable output. Alexandre Duret-Lutz 2004-06-23 08:51:32 +00:00
  • bd69b16e46 * wrap/python/cgi/ltl2tgba.in: Add "Formula Simplications" options. * wrap/python/spot.i: Wrap src/ltlvisite/reduce.hh. Alexandre Duret-Lutz 2004-06-23 08:28:50 +00:00
  • b42cdc0d8f * src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh: New files, extracted from ... * src/ltlvisit/lunabbrev.cc: ... this one, which now work as documented again. * src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc: Adjust to call simplify_f_g() in addition to unabbreviate_logic(). * src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES): Add simpfg.cc and simpfg.hh. Alexandre Duret-Lutz 2004-06-23 08:09:19 +00:00
  • 839837a69e more files to ignore Alexandre Duret-Lutz 2004-06-22 22:58:09 +00:00