Commit graph

alarsyo/spot

Fork 0

1f0060b716 * configure.ac, NEWS: Bump version to 0.0h. * wrap/python/cgi/Makefile.am (CLEANFILES): Clean ltl2tgba.py. Alexandre Duret-Lutz 2003-08-18 15:24:21 +00:00
f4e9c1defa * wrap/python/tests/ltl2tgba.test: Run $srcdir/ltl2tgba.py, not ltl2tgba.py. Alexandre Duret-Lutz 2003-08-18 13:55:55 +00:00
2b9f17202c This implements Couvreur's FM'99 ltl2tgba translation. * src/tgba/bdddict.cc (bdd_dict::is_registered): Split as ... (bdd_dict::is_registered_proposition, bdd_dict::is_registered_state, bdd_dict::is_registered_accepting_variable): ... these. * src/tgba/bdddict.hh: Likewise. * src/tgba/tgbaexplicit.cc (tgba_explicit::set_init_state): New method. (tgba_explicit::declare_accepting_condition): Arrange so that this function can be called during the construction of the automaton. (tgba_explicit::complement_all_accepting_conditions): New method. (tgba_explicit::has_accepting_condition): Adjust to call bdd_dict::is_registered_accepting_variable. * src/tgba/tgbaexplicit.hh (tgba_explicit::set_init_state, tgba_explicit::complement_all_accepting_conditions): New methods. * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them. * src/tgbaalgos/ltl2tgba.hh: Add bibtex entry in comment. * src/tgbatest/Makefile.am (check_PROGRAMS): Remove spotlbtt and tbalbtt. (tbalbtt_SOURCES, tbalbtt_CXXFLAGS, spotlbtt_SOURCES): Remove. * src/tgbatest/spotlbtt.cc: Delete, superseded by "ltl2tgba -F -t". * src/tgbatest/ltl2tgba.cc: Implement the -f and -F options. * src/tgbatest/spotlbtt.test: Use "ltl2tgba -F -t" instead of "spotlbtt", "ltl2tgba -F -t -D" instead of "tbalbtt", and add also check the ltl2tgba_fm translator. * wrap/python/spot.i: Wrap ltl2tgba_fm. * wrap/python/cgi/ltl2tgba.in: Add radio buttons to select between ltl2tgba and ltl2tgba_fm. * wrap/python/tests/ltl2tgba.py: Add support for the -f option. * wrap/python/tests/ltl2tgba.test: Try the -f option. Alexandre Duret-Lutz 2003-08-15 01:33:09 +00:00
256d800580 varnum can be augmented by other allocator. Keep track of a local varnum (lvarnum) in each allocator. * src/misc/bddalloc.cc (bdd_allocator::bdd_allocator): Initialize lvarnum. (bdd_allocator::extvarnum): New method. (bdd_allocator::allocate_variables): Use lvarnum and extvarnum. * src/misc/bddalloc.hh (bdd_allocator::extvarnum): New mathod. (bdd_allocator::lvarnum): New variable. Alexandre Duret-Lutz 2003-08-15 01:20:57 +00:00
519a67babc * src/tgba/state.hh, src/tgba/statebdd.hh, src/tgba/statebdd.cc: Remove the translate() method. Useless since 2003-07-14. Alexandre Duret-Lutz 2003-08-14 09:18:13 +00:00
a76344eef1 * wrap/python/Makefile.am (SUBDIRS): Build `.' first. * wrap/python/cgi/Makefile.am (ltl2tgba.py): Depend on Makefile. Alexandre Duret-Lutz 2003-08-11 11:12:53 +00:00
de6314ed74 Revamp the multop interface to allow some basic optimizations like not constructing a single-child multop. * src/ltlast/multop.hh (multop::instance(type)): Remove. (multop::instance(type, formula*, formula*)): Return a formula*. (multop::instance(type, vec*)): Make it public and return a formula*. (multop::add_sorted, multop::add): * src/ltlast/multop.cc (multop::instance(type, vec*)): Rewrite. (multop::instance(type)): Delete. (multop::instance(type, formula*, formula*)): Adjust. (multop::add_sorted, multop::add): Remove. * src/ltlvisit/clone.cc (clone_visitor::visit(multop*)) Adjust. * src/ltlvisit/nenoform.cc (negative_normal_form_visitor::::visit(multop*)) Adjust. * src/ltltest/equals.test: Make sure a & a' and a' are equals. * wrap/python/tests/ltlsimple.py: Adjust. Alexandre Duret-Lutz 2003-08-10 16:29:49 +00:00
317fed597b * src/tgba/succiterconcrete.cc, src/tgba/tgbaexplicit.cc, src/tgba/tgbatba.cc, src/tgbaalgos/lbtt.cc: Use -' instead of & !' between two BDDs. That's one less call to BuDDy. Alexandre Duret-Lutz 2003-08-10 13:09:50 +00:00
63c62e1767 * src/tgbatest/tgbaread.test, src/tgbatest/explicit.test: Adjust expected output after 2003-08-07's change. Alexandre Duret-Lutz 2003-08-10 12:48:50 +00:00
07fc5d35bd * src/tgba/bdddict.hh: Typo in comments. Alexandre Duret-Lutz 2003-08-10 10:42:28 +00:00
f1275635cc * src/ltlenv/environment.hh: Typo in comments. Alexandre Duret-Lutz 2003-08-10 10:27:29 +00:00
fb014cc35a * src/ltlparse/ltlparse.yy: Handle and diagnose mismatched parentheses. * src/ltltest/parseerr.test: Add some examples. Alexandre Duret-Lutz 2003-08-08 13:16:39 +00:00
1276abd290 * wrap/python/cgi/ltl2tgba.in: Convert GIFs to PNGs. Restrict the size of dot's output to 1024x1024. * src/tgbaalgos/dotty.cc (dotty_bfs::start): Do not preset the size of the graph. Set height=0 for the invisible state. Alexandre Duret-Lutz 2003-08-07 12:14:01 +00:00
e88b41d8c9 * doc/Makefile.am (EXTRA_DIST): Replace buddy.ps by buddy.pdf (the latter has been rebuilt and on J�rn's request it explicitly mentions the differences with the 2.2 manual). Alexandre Duret-Lutz 2003-08-06 15:15:56 +00:00
3a2ecb791c . Alexandre Duret-Lutz 2003-08-06 14:19:29 +00:00
13cc53ce99 typo Alexandre Duret-Lutz 2003-08-06 14:16:49 +00:00
2cea6446b1 * src/bddop.c (bdd_forallcomp, bdd_uniquecomp): Fix documentation. Alexandre Duret-Lutz 2003-08-06 14:14:16 +00:00
0d32884d20 * src/ltlparse/ltlparse.yy: Fix precedence OP_OR < OP_XOR < OP_AND. * src/ltlast/binop.cc (binop::instance): Order operands for associative operators, so that e.g. "a xor b" and "b xor a" are mapped to the same formula. * src/ltltest/equals.test: Check this. Alexandre Duret-Lutz 2003-08-06 10:47:42 +00:00
65b6a4d8da * src/ltlvisit/dotty.cc (draw_node_): s/shabe/shape/. (visit): Draw rectangular node for atomic propositions and constant. This is an attempt to mimic BuDDy's output. Alexandre Duret-Lutz 2003-08-06 10:08:53 +00:00
c7a269dddc * wrap/python/cgi/ltl2tgba.in: Handle show_formula_dot and show_formula_gif. Alexandre Duret-Lutz 2003-08-06 09:52:04 +00:00
fe2f726863 * src/ltlvisit/dotty.hh (dotty): Move the ostream argument first. * src/ltlvisit/dump.hh (dump): Likewise. * src/ltltest/equals.cc, src/ltltest/readltl.cc, src/ltlvisit/dotty.cc, src/ltlvisit/dump.cc: Adjust. Alexandre Duret-Lutz 2003-08-06 09:43:37 +00:00
a5e04a10e6 * src/misc/version.hh, src/misc/version.cc: New files. * src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them. * wrap/python/spot.i: Include misc/version.hh. * wrap/python/cgi/ltl2tgba.in: Print spot.version(). Alexandre Duret-Lutz 2003-08-05 14:37:50 +00:00
b90e0d611f * README: Update layout. Alexandre Duret-Lutz 2003-08-05 14:23:35 +00:00
bdfbf9c519 * wrap/python/cgi/Makefile.am, wrap/python/cgi/ltl2tgba.in, wrap/python/cgi/README: New files. * wrap/python/Makefile.am (SUBDIRS): Add cgi. * configure.ac: Output wrap/python/cgi/Makefile. Alexandre Duret-Lutz 2003-08-05 14:17:47 +00:00
4d819969d0 * wrap/python/spot.i: Add an ostringstream emulation. Alexandre Duret-Lutz 2003-08-04 22:32:11 +00:00
1bad681a4b * wrap/python/spot.i: Add an ofstream emulation. Alexandre Duret-Lutz 2003-08-04 20:52:02 +00:00
01cc802c2d * wrap/python/spot.i: Declare spot::tgba::get_init_state, spot::tgba::succ_iter, and spot::tgba_succ_iterator::current_state as constructors. Alexandre Duret-Lutz 2003-08-04 15:42:21 +00:00
31f4f7b79a * wrap/python/Makefile.am (lib_LTLIBRARIES) (libspotswigpy_la_SOURCES, libspotswigpy_la_CFLAGS) (libspotswigpy_la_LDFLAGS): New variables. (_spot_la_LIBADD, _buddy_la_LDFLAGS): Link with libspotswigpy.la ($(srcdir)/spot_wrap.cxx, $(srcdir)/buddy_wrap.cxx): Run swig with -c. * wrap/python/tests/libpy.c: New file. * wrap/python/tests/run.in: Run python if no arguments are given. * wrap/python/tests/interdep.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add interdep.py. Alexandre Duret-Lutz 2003-08-04 15:35:55 +00:00
ea9a96237b * wrap/python/spot.i: Declare spot::ltl_to_tgba as a constructor. * wrap/python/tests/ltl2tgba.py: Do not force `thisown=1' on tgba objects. Alexandre Duret-Lutz 2003-08-04 14:36:04 +00:00
1095dd7533 * wrap/python/spot.i: Include headers from tgba/ and tgbaalgos/. * wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test: New files. * wrap/python/tests/Makefile.am (TESTS): Add ltl2tgba.test. (EXTRA_DIST): Add ltl2tgba.py. * wrap/python/tests/run.in: Distinguish *.py and *.test. Alexandre Duret-Lutz 2003-08-04 13:50:59 +00:00
c160eba524 * wrap/python/tests/ltlparse.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add it. Alexandre Duret-Lutz 2003-08-04 09:18:54 +00:00
d21c64d1a2 spacing Alexandre Duret-Lutz 2003-08-01 16:45:11 +00:00
992a9686ca * wrap/python/buddy.i: New file. * wrap/python/Makefile.am (EXTRA_DIST): Add it. (python_PYTHON, MAINTAINERCLEANFILES): Add buddy.py. (pyexec_LTLIBRARIES): Add _buddy.la. (_buddy_la_SOURCES, _buddy_la_LDFLAGS, $(srcdir)/buddy_wrap.cxx) ($(srcdir)/buddy.py): New. * wrap/python/tests/bddnqueen.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add it. Alexandre Duret-Lutz 2003-08-01 16:17:35 +00:00
f1f81fbfef * src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: Merge the two unabbreviate_logic definitions (const and non-const) into a function that takes a const formula* and return a non-const formula*. Since formula* is convertible to const formula*, and the const version of the function just called the non-onst one, it makes no sense to keep both. Also, it confused Swig. * src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh: Likewise for negative_normal_form. * src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh: Likewise for unabbreviate_ltl. * src/ltlvisit/clone.cc, src/ltlvisit/clone.hh: Likewise for clone. * src/ltlvisit/destroy.cc, src/ltlvisit/destroy.hh: Likewise for destroy. Alexandre Duret-Lutz 2003-08-01 13:04:25 +00:00
d33ad6d6bf * configure.ac: Bump version to 0.0g. Alexandre Duret-Lutz 2003-08-01 10:29:46 +00:00
5b245d7dd1 * configure.ac, NEWS: Bump version to 0.0f. * iface/gspn/simple.test, iface/gspn/dcswave.test, iface/gspn/dcswaveltl.test: Make sure the example directory is writable. * m4/lbtt.m4, m4/buddy.m4: Always configure buddy/ and lbtt/, regardless of the --with-included-buddy and --with-included-lbtt settings. Alexandre Duret-Lutz 2003-08-01 10:25:56 +00:00
286405da95 * wrap/python/Makefile.am (python_PYTHON, _spot_la_SOURCES): Explicitely refer to spot_wrap.cxx and spot.py as $(srcdir)/spot_wrap.cxx and $(srcdir)/spot.py. (spot_wrap.cxx, spot.py): Alexandre Duret-Lutz 2003-08-01 08:57:33 +00:00
a066bd459c * wrap/python/Makefile.am (spot_wrap.cxx, spot.py): Lookup spot.i in $(srcdir). Alexandre Duret-Lutz 2003-08-01 08:45:54 +00:00
0c50e20ffd * configure.ac: Output wrap/python/tests/Makefile and wrap/python/tests/run. * wrap/python/Makefile.am (SUBDIRS): New variable. * wrap/python/spot.i: Include all formulae headers from ltlast/, as well as ltlvisit/destroy.hh. (spot::ltl::formula::__cmp__, spot::ltl::formula::__str__): New functions. * wrap/python/tests/Makefile.am, wrap/python/tests/ltlsimple.py, wrap/python/tests/run.in: New files. Alexandre Duret-Lutz 2003-07-31 20:04:29 +00:00
99018935bb typos Alexandre Duret-Lutz 2003-07-31 18:40:51 +00:00
a6bb5eaa5b * wrap/python/ltihooks.py: New file. * wrap/python/Makefile.am (EXTRA_DIST): Add ltihooks.py. Alexandre Duret-Lutz 2003-07-31 16:54:37 +00:00
525cc01696 * wrap/Makefile.am, wrap/spot.i: Move ... * wrap/python/Makefile.am, wrap/python/spot.i: ... here. * wrap/Makefile.am: New file. * configure.ac: Output wrap/python/Makefile. Alexandre Duret-Lutz 2003-07-31 12:20:49 +00:00
bdd2be3366 * src/misc/const_sel.hh: Delete. * src/misc/Makefile.am (misc_HEADERS): Remove const_sel.hh. Alexandre Duret-Lutz 2003-07-31 11:49:53 +00:00
baa7a6f258 * src/tgbaalgos/magic.cc, src/tgbaalgos/reachiter.cc: Include cassert. * iface/Makefile.am (SUBDIRS): Recurse in gspn only if condition WITH_GSPN. Alexandre Duret-Lutz 2003-07-31 11:47:21 +00:00
e78ffdc462 * iface/gspn/gspn.cc (tgba_gspn::format_state): Call gspn's print_state. Alexandre Duret-Lutz 2003-07-30 14:02:57 +00:00
4c40d5920a more files to ignore Alexandre Duret-Lutz 2003-07-30 13:41:47 +00:00
e73bea344a * iface/gspn/dcswaveltl.test: Check for a false formula too. Alexandre Duret-Lutz 2003-07-30 12:54:33 +00:00
7ffd3e6ecc * iface/gspn/dcswaveltl.test, iface/gspn/ltlgspn.cc: New files. * iface/gspn/Makefile.am (TESTS): Add dcswaveltl.test. (ltlgspn_rg_LDADD, ltlgspn_srg_LDADD, ltlgspn_rg_SOURCES) (ltlgspn_srg_SOURCES): New variables. (check_PROGRAMS): Add ltlgspn-rg and ltlgspn-srg. Alexandre Duret-Lutz 2003-07-30 12:45:25 +00:00
372d490712 * iface/gspn/Makefile.am (TESTS): Add dcswaveltl.test. (ltlgspn_rg_LDADD, ltlgspn_srg_LDADD, ltlgspn_rg_SOURCES) (ltlgspn_srg_SOURCES): New variables. (check_PROGRAMS): Add ltlgspn-rg and ltlgspn-srg. Alexandre Duret-Lutz 2003-07-30 12:44:50 +00:00
24099078d6 * src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::project_state): New method. * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc (tgba_product::project_state): New method. * src/tgba/tgbabta.hh, src/tgba/tgbabta.cc (tgba_bta_proxy::project_state): New method. * src/tgbaalgos/magic.cc (magic_search::print_result): Take a restrict argument. Alexandre Duret-Lutz 2003-07-30 12:41:48 +00:00
a66ad58b5d * src/ltlparse/ltlscan.ll: Allow /, /, and xor, used in LBTT. * src/ltltest/parse.test: Test them. Alexandre Duret-Lutz 2003-07-29 16:28:38 +00:00
60ef421dd5 * src/tgbaalgos/lbtt.cc: Typos. Alexandre Duret-Lutz 2003-07-29 16:15:19 +00:00
48c03b89b8 * src/TestOperations.cc (generateBuchiAutomaton): Forward SIGINT and SIGQUIT. * src/ExternalTranslator.cc (ExternalTranslator::translate): Likewise. * src/main.cc (main): Do not intercept SIGINT in non-interactive runs. Alexandre Duret-Lutz 2003-07-29 13:06:53 +00:00
ea90d2f8be merge changes with lbtt 1.0.2 Alexandre Duret-Lutz 2003-07-29 12:21:22 +00:00
06226f3227 lbtt 1.0.2 Alexandre Duret-Lutz 2003-07-29 12:12:15 +00:00
01f58f5fbf * src/tgbatest/Makefile.am (check_PROGRAMS): Add tbalbtt. (tbalbtt_SOURCES, tbalbtt_CXXFLAGS): New variables. * src/tgbatest/spotlbtt.cc [TBA]: Build tba proxies conditionally. * src/tgbatest/spotlbtt.test: Include tbalbtt in the tests. Alexandre Duret-Lutz 2003-07-29 11:21:18 +00:00
860d085b1a * src/tgba/tgbatba.hh, src/tgba/tgbatba.cc (tgba_tba_proxy::state_is_accepting): New method. * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc: New files. * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES, tgbaalgos_HEADERS): Add them. * src/tgbatest/ltlmagic.cc, src/tgbatest/ltlmagic.test: New files. * src/tgbatest/Makefile.am (TESTS, ltlmagic_SOURCES, check_PROGRAMS): Add them. Alexandre Duret-Lutz 2003-07-28 15:49:16 +00:00
af928d28ac * src/tgba/tgba.hh (tgba::~tgba): Make it public. * src/tgba/tgbatba.cc, src/tgba/tgbatba.hh: New files. * src/tgba/Makefile.am (tgba_HEADERS): Add tgbatba.hh. (libtgba_la_SOURCES): Add tgbatba.cc. * src/tgbatest/ltl2tgba.cc: Add option -D. Alexandre Duret-Lutz 2003-07-25 17:27:52 +00:00
5bc2d77e60 * src/tgbaalgos/lbtt.cc (bdd_less_than): Move ... * src/misc/bddlt.hh: ... in this new file. * src/misc/Makefile.am (misc_HEADERS): Add bddlt.hh. Alexandre Duret-Lutz 2003-07-25 14:32:50 +00:00
d0a7a3ab54 * iface/gspn/dcswave.test: Comment state space sizes. Alexandre Duret-Lutz 2003-07-25 14:12:01 +00:00
e24d3be8a7 * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add reachiters.hh. (libtgbaalgos_la_SOURCES): Add reachiters.cc. * src/tgbaalgos/dotty.cc, src/tgbaalgos/save.cc: Rewrite using spot::tgba_reachable_iterator_breadth_first. * src/tgbatest/explicit.test, src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Adjust expected output. Alexandre Duret-Lutz 2003-07-25 13:12:01 +00:00
664e49e07e * configure.ac: Output iface/gspn/defs. * iface/gspn/Makefile.am (EXTRA_DIST): Add $(TESTS). (TESTS, check_SCRIPTS, distclean-local): New. * iface/gspn/dcswave.test, iface/gspn/simple.test, iface/gspn/defs.in: New files. * iface/gspn/dottygspn.cc (main): Take the list of properties of interest in argument. Alexandre Duret-Lutz 2003-07-24 13:04:10 +00:00
5e8cbcde7f * iface/gspn/examples/DCSwave/DCSWave.def, iface/gspn/examples/DCSwave/DCSWave.net iface/gspn/examples/DCSwave/DCSWave.tobs, iface/gspn/examples/simple/simple.def, iface/gspn/examples/simple/simple.net, iface/gspn/examples/simple/simple.tobs: New files, from Yann Thierry-Mieg. * iface/gspn/Makefile.am (EXTRA_DIST): New variables. Alexandre Duret-Lutz 2003-07-23 16:13:45 +00:00
7991efa10f * iface/gspn/gspn.cc (tgba_gspn_private_::tgba_gspn_private_): Rethrow caught expections. Alexandre Duret-Lutz 2003-07-23 15:23:00 +00:00
94a9543f38 * m4/gspnlib.m4: Check for libgspnRG.a and libgspnSRG.a. Define LIBGSPNRG_LDFLAGS and LIBGSPNSRG_LDFLAGS, not LIBGSPN_LDFLAGS. * iface/gspn/Makefile.am: Adjust, build dottygspn-rg and dottygspn-srg instead of dottygspn. * iface/gspn/gspn.cc (EVENT_TRUE): Undefine. (tgba_gspn_private_::~tgba_gspn_private_): Free all_indexes. * iface/gspn/dottygspn.cc (main): Destroy the automaton before its dictionnary. Alexandre Duret-Lutz 2003-07-22 13:11:32 +00:00
44993317ea Rename gspnlin.m4 to gspnlib.m4 Alexandre Duret-Lutz 2003-07-17 16:07:55 +00:00
1d9c3d6409 Now succ_iter() can fetch extra information from the root of a product to reduce its number of successors. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgba.cc. * src/tgba/tgba.hh (tgba::succ_iter): Add the global_state and global_automaton arguments. (tgba::support_conditions, tgba::support_variables, tgba::compute_support_conditions, tgba::compute_support_variables): New functions. (tgba::last_support_conditions_input_, tgba::last_support_conditions_output_, tgba::last_support_variables_input_, tgba::last_support_variables_output_): New attributes. * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::succ_iter): Handle the two new arguments. (tgba_bdd_concrete::compute_support_conditions, tgba_bdd_concrete::compute_support_variables): Implement them. * src/tgba/tgbabddconcrete.hh: Adjust. * src/tgba/tgbaexplicit.cc (tgba_explicit::succ_iter): Ignore the two new arguments. (tgba_explicit::compute_support_conditions, tgba_explicit::compute_support_variables): Implement them. * src/tgba/tgbaexplicit.hh: Adjust. * src/tgba/tgbaproduct.cc (tgba_product::succ_iter): Handle the two new arguments. (tgba_product::compute_support_conditions, tgba_product::compute_support_variables): Implement them. * src/tgba/tgbaproduct.hh: Adjust. * iface/gspn/gspn.cc (tgba_gspn_private_::last_state_cond_input, tgba_gspn_private_::last_state_cond_output, (tgba_gspn_private_::tgba_gspn_private_): Set last_state_cond_input. (tgba_gspn_private_::~tgba_gspn_private_): Delete last_state_cond_input. (tgba_gspn_private_::state_conds): New function, eved out from tgba_gspn::succ_iter. (tgba_gspn::succ_iter): Use it. Use the two new arguments. (tgba_gspn::compute_support_conditions, tgba_gspn::compute_support_variables): New functions. * iface/gspn/gspn.hh: Adjust. Alexandre Duret-Lutz 2003-07-17 15:11:49 +00:00
4bf6c52bea * rsc/bdd.h (bdd_existcomp, bdd_forallcomp, bdd_uniquecomp, bdd_appexcomp, bdd_appallcomp, bdd_appunicomp): Declare for C and C++. * src/bddop.c (CACHEID_EXISTC, CACHEID_FORALLC, CACHEID_UNIQUEC, CACHEID_APPEXC, CACHEID_APPALC, CACHEID_APPUNCC): New macros. (quatvarsetcomp): New variables. (varset2vartable): Take a second argument to indicate negation, set quatvarsetcomp. (INVARSET): Honor quatvarsetcomp. (quantify): New function, extracted from bdd_exist, bdd_forall, and bdd_appunicomp. (bdd_exist, bdd_forall, bdd_appunicomp): Use quantify. (bdd_existcomp, bdd_forallcomp, bdd_appunicompcomp): New functions. (appquantify): New function, extracted from bdd_appex, bdd_appall, and bdd_appuni. (bdd_appex, bdd_appall, bdd_appuni): Use appquantify. (bdd_appexcomp, bdd_appallcomp, bdd_appunicomp): New functions. Alexandre Duret-Lutz 2003-07-17 14:09:03 +00:00
f63c67b507 * iface/gspn/gspn.cc (EVENT_TRUE): Override temporarily.. (tgba_gspn::succ_iter): Fix usage of cube. Alexandre Duret-Lutz 2003-07-17 07:54:16 +00:00
4ac192ac1e * m4/gspnlib.m4: New file. * configure.ac: Call AX_CHECK_GSPNLIB. * Makefile.am (EXTRA_DIST): Add m4/gspnlib.m4. * iface/gspn/Makefile.am (AM_CPPFLAGS): Add $(LIBGSPN_CPPFLAGS). (libspotgspn_la_LIBADD, check_PROGRAMS, dottygspn_SOURCES, dottygspn_LDADD): New variables. * iface/gspn/gspn.hh (gspn_interface): New class. (gspn_exeption): Take a string argument and adjust all callers. (operator<<): Define for gspn_exeption. * iface/gspn/gspn.cc (gspn_interface::gspn_interface, gspn_interface::~gspn_interface): New. * iface/gspn/gspnlib.h: Delete, it belongs to GSPN. * iface/gspn/dottygspn.cc: New file. Alexandre Duret-Lutz 2003-07-16 12:56:38 +00:00
49fd9579da * m4/lbtt.m4 (AX_CHECK_LBTT): Set LBTT and LBTT_TRANSLATE when using an already installed lbtt. Alexandre Duret-Lutz 2003-07-15 12:26:03 +00:00
9791182f64 more files to ignore Alexandre Duret-Lutz 2003-07-15 11:51:32 +00:00
66b1630c31 Homogenize passing of automata as pointers, not references. Disallow copy for security. Alexandre Duret-Lutz 2003-07-14 22:20:35 +00:00
cab3be9795 Before this change, all automata would construct their own dictionaries (map of BDD variables to LTL formulae). This was cumbersome, because to multiply two automata we had to build a common dictionary (the union of the two LTL formula spaces), and install wrappers to translate each automaton's BDD answers into the common dictionary. This translation, that had to be repeated when several products were nested, was time consuming and was a hindrance for some optimizations. In the new scheme, all automata involved in a product must share the same dictionary. An empty dictionary should be constructed by the user and passed to the automaton' constructors as necessary. This huge change removes most code than it adds. Alexandre Duret-Lutz 2003-07-14 21:42:59 +00:00
3013ba8da6 * configure.ac: Bump version to 0.0e. Alexandre Duret-Lutz 2003-07-13 14:57:23 +00:00
53bf08014e * configure.ac: Bump version to 0.0d. * NEWS, README: New files. Alexandre Duret-Lutz 2003-07-13 14:52:38 +00:00
7836595873 * doc/lbtt.texi: Never use @-commands in @node names, recent Texinfo versions are stricter on this. Alexandre Duret-Lutz 2003-07-13 14:45:03 +00:00
600b21acfe * m4/lbtt.m4: Run lbtt-translate, not lbtt. Alexandre Duret-Lutz 2003-07-12 17:59:47 +00:00
c8f6eee9d3 * iface/gspn/gspn.cc: Include cassert. Alexandre Duret-Lutz 2003-07-12 17:54:16 +00:00
9a4da5ffd4 * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(multop)): Forward root_ to children of And. (ltl_trad_visitor::recurse): Take a root argument. Alexandre Duret-Lutz 2003-07-10 14:27:19 +00:00
b963af66f1 * src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory::add_relation): Rename as ... (tgba_bdd_concrete_factory::constrain_relation): ... this. * src/tgba/tgbabddconcretefactory.cc, src/tgbaalgos/ltl2tgba.cc: Adjust. Alexandre Duret-Lutz 2003-07-10 14:13:56 +00:00
f661b0adc4 * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::G)): Do not create Now/Next variable when G is the root of the formula. (ltl_trad_visitor::ltl_trad_visitor): Take a root argument. (ltl_trad_visitor::recurse): Create a new visitor, do not copy the current one. (ltl_to_tgba): Build ltl_trad_visitor with root = true. Alexandre Duret-Lutz 2003-07-10 13:55:20 +00:00
871f421b5e spacing Alexandre Duret-Lutz 2003-07-10 12:46:39 +00:00
006bd6b930 * src/tgbatest/spotlbtt.test: Make 100 rounds. Alexandre Duret-Lutz 2003-07-10 12:01:41 +00:00
977d389724 * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Fix so that !p.!Acc[g].Acc[f] + p.!Acc[g].Acc[f] + p.Acc[g].!Acc[f] is factored as !p.!Acc[g].Acc[f] + p.(!Acc[g].Acc[f] + Acc[g].!Acc[f]), not !Acc[g].Acc[f] + p.Acc[g].!Acc[f]. Alexandre Duret-Lutz 2003-07-10 11:56:03 +00:00
bbba8ca966 Spot wants ^', not xor'. * src/SpotWrapper.hh (SpotWrapper::SPOT_XOR): Declare. * src/SpotWrapper.cc (SpotWrapper::SPOT_XOR): Define. (SpotWrapper::translateFormula): Use SPOT_XOR. Alexandre Duret-Lutz 2003-07-10 08:26:23 +00:00
79bed65843 * lbtt/: New directory. Contains a patched version of lbtt 1.0.1. * Makefile.am (MAYBE_LBTT): New variables. (SUBDIRS): Add $(MAYBE_LBTT). (EXTRA_DIST): Add m4/lbtt.m4. * configure.ac: Call AX_CHECK_LBTT. * m4/lbtt.m4: New file. * src/tgbatest/Makefile.am (check_PROGRAMS): Add spotlbtt. (spotlbtt_SOURCES): New variables. (TESTS): Add spotlbtt.test. (CLEANFILE): Add config. * src/tgbatest/defs.in (top_builddir, LBTT, LBTT_TRANSLATE): New substitutions. * src/tgbatest/spotlbtt.cc, src/tgbatest/spotlbtt.test: New files. Alexandre Duret-Lutz 2003-07-09 15:40:24 +00:00
71b7da1437 I want $? = 1 whenever some test fails. * src/main.cc (testLoop): Return 1 iff an error occured. (main): Use testLoop's output as exit status. Alexandre Duret-Lutz 2003-07-09 15:34:53 +00:00
9df8be4503 typo Alexandre Duret-Lutz 2003-07-09 15:05:00 +00:00
8af9996863 * src/ExternalTranslator.h (class ExternalTranslator): Declare class SpotWrapper as a friend. * src/SpotWrapper.h, src/SpotWrapper.cc: New files. * src/Makefile.am (lbtt_translate_SOURCES): Add SpotWrapper.cc and SpotWrapper.h. * src/translate.cc (main): Add the --spot option, and build a SpotWrapper of required. Alexandre Duret-Lutz 2003-07-09 14:11:25 +00:00
5cc9c66dc0 * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Fix computation of states sharing the same accepting set. Alexandre Duret-Lutz 2003-07-09 14:06:03 +00:00
d14eee25bf * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Fix computation of states sharing the same accepting state. Alexandre Duret-Lutz 2003-07-09 14:05:49 +00:00
2a8b1b7471 Make sure we only output one initial state in LBTT's output. * src/tgbaalgos/lbtt.cc (fill_todo): Add the 'first' argument to designate initial states. (lbtt_reachable): Adjust calls to fill_todo. Handle the fake initial state accepting conditions specially. * src/tgbaalgos/lbtt.hh: Update comments. Alexandre Duret-Lutz 2003-07-09 14:03:43 +00:00
ea04df6971 * src/tgbaalgos/lbtt.cc (lbtt_reachable): Do not end transitions guards with -1 in output. Alexandre Duret-Lutz 2003-07-09 11:43:04 +00:00
f9c8eb1cb7 * src/tgbatest/ltl2tgba.cc: Add option -t to output the LBTT automata. * src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add lbtt.hh. (libtgbaalgos_la_SOURCES): Add lbtt.cc. * src/tgba/bddprint.cc (print_sat_handler): Put a space after "!". * src/tgbatest/readsave.test: Adjust spaces after "!". Alexandre Duret-Lutz 2003-07-08 15:45:11 +00:00
a307c0d0ae spacing Alexandre Duret-Lutz 2003-07-08 11:54:46 +00:00
63e23c7a68 * src/ltlvisit/dump.cc: Strip useless spot::ltl:: prefixes. Alexandre Duret-Lutz 2003-07-08 08:08:12 +00:00
7690e9ad9c First sketch of the GSPN wrapper objects. * iface/gspn/gspn.cc, iface/gspn/gspn.hh: New files. * iface/gspn/Makefile.am (libspotgspn_la_SOURCES): Add them. Alexandre Duret-Lutz 2003-07-07 16:41:10 +00:00
c96af6251a * src/tgba/succiter.hh (current_state, current_conditions current_accepting_conditions): Mark as const. * src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh, src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh, src/tgba/tgbatranslateproxy.cc, src/tgba/tgbatranslateproxy.hh: Likewise. Alexandre Duret-Lutz 2003-07-07 13:43:53 +00:00