Commit graph

10 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
51094329d8 * src/tgba/state.hh (state_ptr_less_than): Make sure left is
non-null.  Suggested by Denis Poitreneaud.
2003-08-25 19:21:02 +00:00
Alexandre Duret-Lutz
519a67babc * src/tgba/state.hh, src/tgba/statebdd.hh, src/tgba/statebdd.cc:
Remove the translate() method.  Useless since 2003-07-14.
2003-08-14 09:18:13 +00:00
Alexandre Duret-Lutz
a307c0d0ae spacing 2003-07-08 11:54:46 +00:00
Alexandre Duret-Lutz
e562620885 * doc/Doxyfile.in (HAVE_DOT): Set to YES to output
collaboration diagrams.
* doc/mainpage.dox: Typo.

* src/tgba/state.hh (state::as_bdd): Delete.
* src/tgba/tgbaproduct.hh (state_bdd_product): Inherit from state,
not state_bdd.
(state_bdd_product::state_bdd_product): Adjust.
* src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product):
Adjust.

* src/tgba/succiter.hh (tgba_bdd_succ_iterator::done):
Mark as const.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::done): Likewise.
* src/tgba/succiterconcrete.hh
(tgba_succ_iterator_concrete::done): Likewise.
* src/tgba/tgbaexplicit.cc
(tgba_explicit_succ_iterator::done): Likewise.
* src/tgba/tgbaexplicit.hh
(tgba_explicit_succ_iterator::done): Likewise.
* src/tgba/tgbaproduct.cc
(tgba_product_succ_iterator::done): Likewise.
* src/tgba/tgbaproduct.hh
(tgba_product_succ_iterator::done): Likewise.
* src/tgba/tgbatranslateproxy.hh
(tgba_translate_proxy_succ_iterator::done): Likewise.
* src/tgba/tgbatranslateproxy.cc
(tgba_translate_proxy_succ_iterator::done): Likewise.

* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::next): Call bdd_satoneset
on data_.varandnext_set.  The previous implementation
was wrong for GFa.
* src/tgba/tgbabddcoredata.hh: Declare varandnext_set.
* src/tgba/tgbabddcoredata.cc: Handle varandnext_set.
2003-06-30 15:38:41 +00:00
Alexandre Duret-Lutz
692f78d663 Fix errors reported by ICC.
* src/tgba/state.hh (state_ptr_less_than::operator()): Make it const.
* src/tgba/tgbaproduct.cc: Include string.hh.
* src/ltlast/multop.hh (multop::add, multop::add_sorted): Do
not use qualified names in declarations.
* m4/gccwarn.m4 (CF_GXX_WARNINGS): Fix GXX test.
* src/ltlenv/defaultenv.hh, src/ltlenv/defaultenv.cc,
src/ltlenv/environment.hh: Add virtual destructors.
2003-06-28 10:10:25 +00:00
Alexandre Duret-Lutz
4db70160c9 * src/tgba/tgbabddprod.cc, src/tgba/tgbabddprod.hh: Rename as ...
* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: ... these.
(tgba_bdd_product, tgba_bdd_product_succ_iterator): Rename as ...
(tgba_product, tgba_product_succ_iterator): ... these, and adjust
all uses.
* src/tgba/tgbabddtranslateproxy.cc,
src/tgba/tgbabddtranslateproxy.hh: Rename as ...
* src/tgba/tgbatranslateproxy.cc,
src/tgba/tgbatranslateproxy.hh: ... these.
(tgba_bdd_translate_proxy, tgba_bdd_translate_proxy_succ_iterator):
Rename as ...
(tgba_translate_proxy, tgba_translate_proxy_succ_iterator): ... these,
and adjust all uses.
2003-06-16 15:46:08 +00:00
Alexandre Duret-Lutz
ab09c18597 Make sure we can multiply two tgba_explicit.
* tgba/state.hh (state::translate, state::clone, state::as_bdd):
New virtual methods.
* tgba/stataebdd.cc (state::translate, state::clone): New methods.
* tgba/stataebdd.hh (state::translate, state::clone): New methods.
* tgba/tgbabddprod.cc (state_bdd_product::clone,
tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator):
New methods.
(tgba_bdd_product_succ_iterator::first): Reset right_
if any of left_ or right_ is already done (i.e., is empty).
(tgba_bdd_product_succ_iterator::done): Return true
if right_ is NULL.
(tgba_bdd_product_succ_iterator::current_state,
tgba_bdd_product::get_init_state): Work	directory with `state's.
* tgba/tgbabddprod.hh (state_bdd_product::clone,
tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator):
New methods.
* tgba/tgbabddtranslateproxy.cc
(tgba_bdd_translate_proxy_succ_iterator::
tgba_bdd_translate_proxy_succ_iterator): Work on any kind of iteraator.
(tgba_bdd_translate_proxy_succ_iterator::
~tgba_bdd_translate_proxy_succ_iterator): New method.
(tgba_bdd_translate_proxy_succ_iterator::current_state,
tgba_bdd_translate_proxy::get_init_state,
tgba_bdd_translate_proxy::succ_iter): Work on `state's and
`tgba_succ_iterator's directlry.
(tgba_bdd_translate_proxy::format_state): Delegate formating
to the proxied automata.
* tgba/tgbaexplicit.cc (state_explicit::clone): New method.
* src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition,
tgba_explicit::get_promise): Call ltl::destroy on existing formulae.
* tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
(explprod_SOURCES): New variable.
(TESTS): Add explprod.test.
(CLEANFILES): Add input1 and input2.
2003-06-16 15:18:20 +00:00
Alexandre Duret-Lutz
fb5ff901d0 * src/tgba/bddprint.hh (bdd_format_set): New function.
* src/tgba/bddprint.cc (bdd_format_set): Likewise.
* src/tgba/state.hh: Add Doxygen comments.
(state::compare): Take a state*, not a state&.
(state_ptr_less_than): New functor.
* src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a
state&.
* src/tgba/statebdd.cc (state_bdd::compare): Likewise.
* src/tgba/succiter.hh: Add Doxygen comments.
* src/tgba/tgba.hh: Mention promises.
(tgba::formate_state): New pure virtual method.
* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::formate_state):
New method.
* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::formate_state):
Likewise.
* src/tgbaalgos/dotty.cc: Adjust to use state_ptr_less_than
and tgba::formate_state.
2003-05-27 13:05:22 +00:00
Alexandre Duret-Lutz
3f0e95f061 * src/tgba/succiter.hh (tgba_succ_iterator::current_state):
Return a state*, not a state_bdd.
* src/tgba/succiterconcrete.hh
(tgba_succ_iterator_concrete::current_state): Return a state_bdd*,
not a state_bdd.
* src/tgba/state.hh (state::as_bdd): New abstract method.
* src/tgba/statebdd.hh (state_bdd::as_bdd): Move definitions ...
* src/tgba/statebdd.cc (state_bdd::as_bdd): ... here.
* src/tgba/tgba.hh: Add Doxygen comments.
(tgba::succ_iter, tgba::get_init_state): Use state*, not state_bdd.
* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::get_init_state):
Return a state_bdd*, not a state_bdd.
(tgba_bdd_concrete::get_init_bdd): New method.
(tgba_bdd_concrete::succ_uter): Take a state* as argument.
* src/tgba/tgbabddconcrete.cc: Likewise.
* src/tgba/tgbabddtranslatefactory.cc
(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use
tgba_bdd_concrete::get_init_bdd.
* src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty): Adjust
to use state* instead of state_bdd.
* src/tgba/succlist.hh: Delete.  (Leftover from a previous
draft.)
2003-05-27 10:40:16 +00:00
Alexandre Duret-Lutz
c03934140f Initial code for TGBA (Transition Generalized Büchi Automata).
Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba,
a LTL-to-TGBA translator using Couvreur's algorithm.

* src/Makefile.am (SUBDIRS): Add tgba.
(libspot_la_LIBADD): Add tgba/libtgba.la.
* src/tgba/Makefile.am, src/tgba/bddfactory.cc,
src/tgba/bddfactory.hh, src/tgba/dictunion.cc,
src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh,
src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh,
src/tgba/succiter.hh, src/tgba/succiterconcrete.cc,
src/tgba/succiterconcrete.hh, src/tgba/succlist.hh,
src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc,
src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbabddconcreteproduct.cc,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc,
src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.cc,
src/tgba/tgbabdddict.hh, src/tgba/tgbabddfactory.hh,
src/tgba/tgbabddtranslatefactory.cc,
src/tgba/tgbabddtranslatefactory.hh: New files.
2003-05-26 11:17:40 +00:00