Commit graph

11 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
83565fb659 * src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh: Rename as ...
* src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/ltl2tgba_lacim.hh:
... this, and rename ltl_to_tgba() as ltl_to_tgba_lacim as well.
* iface/gspn/ltlgspn.cc, src/tgbatest/explprod.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlmagic.cc,
src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
src/tgbatest/tripprod.cc, wrap/python/spot.i,
wrap/python/cgi/ltl2tgba.in, wrap/python/tests/interdep.py,
wrap/python/tests/ltl2tgba.py: Adjust.
2003-09-22 15:54:34 +00:00
Alexandre Duret-Lutz
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.
2003-08-15 01:33:09 +00:00
Alexandre Duret-Lutz
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().
2003-08-05 14:37:50 +00:00
Alexandre Duret-Lutz
4d819969d0 * wrap/python/spot.i: Add an ostringstream emulation. 2003-08-04 22:32:11 +00:00
Alexandre Duret-Lutz
1bad681a4b * wrap/python/spot.i: Add an ofstream emulation. 2003-08-04 20:52:02 +00:00
Alexandre Duret-Lutz
01cc802c2d * wrap/python/spot.i: Declare spot::tgba::get_init_state,
spot::tgba::succ_iter, and spot::tgba_succ_iterator::current_state
as constructors.
2003-08-04 15:42:21 +00:00
Alexandre Duret-Lutz
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.
2003-08-04 15:35:55 +00:00
Alexandre Duret-Lutz
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.
2003-08-04 14:36:04 +00:00
Alexandre Duret-Lutz
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.
2003-08-04 13:50:59 +00:00
Alexandre Duret-Lutz
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.
2003-07-31 20:04:29 +00:00
Alexandre Duret-Lutz
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.
2003-07-31 12:20:49 +00:00
Renamed from wrap/spot.i (Browse further)