alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/ChangeLog
Alexandre Duret-Lutz 7991efa10f * iface/gspn/gspn.cc (tgba_gspn_private_::tgba_gspn_private_): 
Rethrow caught expections.
2003-07-23 15:23:00 +00:00

1322 lines
55 KiB
Text
Raw Blame History

2003-07-23 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* iface/gspn/gspn.cc (tgba_gspn_private_::tgba_gspn_private_):
Rethrow caught expections.
2003-07-22 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* 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.
2003-07-17 Alexandre Duret-Lutz <aduret@src.lip6.fr>
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.
* iface/gspn/gspn.cc (EVENT_TRUE): Override temporarily.
(tgba_gspn::succ_iter): Fix usage of cube.
2003-07-16 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* 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.
2003-07-15 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* m4/lbtt.m4 (AX_CHECK_LBTT): Set LBTT and LBTT_TRANSLATE
when using an already installed lbtt.
Homogenize passing of automata as pointers, not references.
Disallow copy for security.
* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Disallow copy.
* src/tgba/tgbaexplicit.hh (tgba_explicit): Likewise.
* src/tgba/tgbaexplicit.cc (tgba_explicit::operator=,
tgba_explicit::tgba_explicit(tgba_explicit)): Remove.
* src/tgba/tgbabddconcreteproduct.cc
(tgba_bdd_concrete_product_factory::tgba_bdd_concrete_product_factory,
product): Take operand automata as pointers.
* src/tgba/tgbabddconcreteproduct.hh (product): Likewise.
* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh:
(tgba_product): Disallow copy.
(tgba_product::tgba_product): Take operand automata as pointers.
* src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty_reachable):
Take tgba arguments as pointer.
* src/tgbaalgos/dotty.hh (dotty_reachable): Likewise.
* src/tgbaalgos/lbtt.cc (fill_todo, lbtt_reachable): Likewise.
* src/tgbaalgos/lbtt.hh (lbtt_reachable): Likewise.
* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh (ltl_to_tgba):
Likewise.
* src/tgbaalgos/save.cc (save_rec, tgba_save_reachable): Likewise.
* src/tgbaalgos/save.hh (save): Likewise.
* src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
src/tgbatest/mixprod.cc, src/tgbatest/readsave.cc,
src/tgbatest/spotlbtt.cc, src/tgbatest/tgbaread.cc,
src/tgbatest/tripprod.cc: Likewise.
2003-07-14 Alexandre Duret-Lutz <aduret@src.lip6.fr>
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.
* src/Makefile.am (libspot_la_LIBADD): Add misc/libmisc.la.
* src/misc/bddalloc.hh, src/misc/bddalloc.cc: New files. These
partly replace src/tgba/bddfactory.hh and src/tgba/bddfactory.cc.
* src/misc/Makefile.am: Adjust to build bddalloc.hh and bddalloc.cc.
* src/tgba/bddfactory.hh, src/tgba/bddfactory.cc,
src/tgba/dictunion.hh, src/tgba/dictunion.cc,
src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
src/tgba/tgbabddtranslatefactory.hh,
src/tgba/tgbabddtranslatefactory.cc,
src/tgba/tgbatranslateproxy.hh, src/tgba/tgbatranslateproxy.cc:
Delete.
* src/tgba/bdddict.hh, src/tgba/bdddict.cc: New files. These
replaces tgbabdddict.hh and tgbabdddict.cc, and also part of
bddfactory.hh and bddfactory.cc.
* src/tgba/bddprint.cc, src/tgba/bddprint.hh: Adjust to
use bdd_dict* instead of tgba_bdd_dict&.
* src/tgba/succiterconcrete.cc (succ_iter_concrete::next()):
Get next_to_now from the dictionary.
* src/tgba/tgba.hh (tgba::get_dict): Return a bdd_dict*,
not a const tgba_bdd_dict*.
* src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh:
Adjust to use the new dictionary, stored in data_.
* src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddconcretefactory.hh: Likewise. Plus
now_to_next_ is now also stored in the dictionary.
* src/tgba/tgbabddconcreteproduct.cc: Likewise. Now
that both operand share the same product, there is not
point in using tgba_bdd_translate_factory.
* src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh:
Store a bdd_dict (taken as constructor argument).
(tgba_bdd_core_data::~tgba_bdd_core_data): Remove.
(tgba_bdd_core_data::translate): Remove.
(tgba_bdd_core_data::next_to_now): Remove (now in dict).
(tgba_bdd_core_data::dict): New pointer.
* src/tgba/tgbabddfactory.hh: (tgba_bdd_factory::get_dict): Remove.
* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
Adjust to use the new dictionary.
* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Likewise. Do
not use tgba_bdd_dict_union and tgba_bdd_translate_proxy anymore.
* src/tgbaalgos/lbtt.cc, src/tgbaalgos/save.cc: Adjust to
use bdd_dict* instead of tgba_bdd_dict&.
* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.cc: Likewise.
(ltl_to_tgba): Take a dict argument.
* src/tgbaparse/public.hh (tgba_parse): Take a dict argument.
* src/tgbaparse/tgbaparse.yy (tgba_parse): Take a dict argument.
* src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
src/tgbatest/readsave.cc, src/tgbatest/spotlbtt.cc,
src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Instantiate
a dictionary, and pass it to the automata' constructors.
* src/tgbatest/ltl2tgba.cc: Likewise, and remove the -o (defrag)
option.
* iface/gspn/gspn.hh (tgba_gspn::tgba_gspn): Take a bdd_dict argument.
(tgba_gspn::get_dict): Adjust return type.
* iface/gspn/gspn.cc: Do not use bdd_factory, adjust to
use the new dictionary instead.
2003-07-13 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* configure.ac: Bump version to 0.0e.
* configure.ac: Bump version to 0.0d.
* NEWS, README: New files.
2003-07-12 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* m4/lbtt.m4: Run lbtt-translate, not lbtt.
* iface/gspn/gspn.cc: Include cassert.
2003-07-10 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(multop)):
Forward root_ to children of And.
(ltl_trad_visitor::recurse): Take a root argument.
* 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.
* 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.
* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::X)):
Remove FIXME about handling X(a U b) and X(a R b) better, it's
done naturally.
* src/tgbatest/spotlbtt.test: Make 100 rounds.
* 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].
2003-07-09 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* 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.
* src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next):
Fix computation of states sharing the same accepting set.
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.
* src/tgbaalgos/lbtt.cc (lbtt_reachable): Do not end transitions
guards with -1 in output.
2003-07-08 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* 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 "!".
* src/ltlvisit/dump.cc: Strip useless spot::ltl:: prefixes.
2003-07-07 Alexandre Duret-Lutz <aduret@src.lip6.fr>
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.
* 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.
* iface/gspn/gspnlib.h: Fit 80 columns.
[__cplusplus]: Wrap everything under extern "C".
* src/tgba/succiterconcrete.hh
(tgba_succ_iterator_concrete::current_acc_): New attribute.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::next): Set current_acc_.
(tgba_succ_iterator_concrete::current_accepting_conditions):
Simply return it.
* configure.ac: Output iface/Makefile and iface/gspn/Makefile.
* iface/Makefile.am, iface/gspn/Makefile.am: New files.
* Makefile.am (SUBDIRS): Add iface.
* iface/gspn/gspnlib.h: New file, from Yann and Souheib.
* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::tgba_bdd_core_data,
tgba_bdd_core_data::translate): Handle all_accepting_conditions.
* src/tgba/tgbabddconcretefactory.cc
(tgba_bdd_concrete_factory::finish): Fill all_accepting_conditions.
2003-07-04 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit): Declare
accepting conditions w.r.t. to Now variables, not Next.
2003-07-03 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbaproduct.cc (tgba_product_succ_iterator::first):
Simplify, do not call next_non_false_() if either side is done.
* src/tgba/succiter.hh (tgba_succ_iterator::current_condition):
State that this is a boolean function.
* src/tgba/succiterconcrete.hh
(tgba_succ_iterator_concrete::trans_dest_,
tgba_succ_iterator_concrete::trans_set_,
tgba_succ_iterator_concrete::trans_set_left_,
tgba_succ_iterator_concrete::neg_trans_set_): Remove.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::tgba_succ_iterator_concrete,
tgba_succ_iterator_concrete::first): Adjust to removed members.
(tgba_succ_iterator_concrete::next): Simplify, transitions
are no labelled by boolean functions, not only conjunctions.
Suggested by Denis Poitrenaud.
2003-07-02 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New
function.
* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate):
Likewise.
* src/tgba/tgbabddtranslatefactory.cc
(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use
tgba_bdd_core_data::translate.
* src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::nownext_set):
New attribute.
* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc:
Handle nownext_set.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::next): Use nownext_set to simplify.
Rewrite tgba_succ_iterator_concrete::next for the fourth time
(or is it the fifth?).
* src/tgba/succiterconcrete.hh
(tgba_succ_iterator_concrete::trans_dest_,
tgba_succ_iterator_concrete::trans_set_,
tgba_succ_iterator_concrete::trans_set_left_,
tgba_succ_iterator_concrete::neg_trans_set_): New attributes.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::tgba_succ_iterator_concrete): Initialize
new members.
(tgba_succ_iterator_concrete::first): Likewise.
(tgba_succ_iterator_concrete::next): Rewrite.
* tgba/tgbabddcoredata.hh (tgba_bdd_core_data::acc_set): New attribute.
* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc:
Handle acc_set.
2003-07-01 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbabddtranslatefactory.cc
(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Translate
varandnext_set.
2003-06-30 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbaparse/tgbaparse.yy (lines): Expect at last one line.
* 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.
* doc/Doxygen.in: Enable LaTeX output.
* doc/Makefile.am (spotref.pdf): New rule.
(EXTRA_DIST): Add spotref.pdf.
* src/tgba/tgbabddconcretefactory.cc:
(tgba_bdd_concrete_factory::tgba_bdd_concrete_factory): New.
(tgba_bdd_concrete_factory::create_state): Update now_to_next_.
(tgba_bdd_concrete_factory::finish): Constraint Next variables
in the relation.
* src/tgba/tgbabddconcretefactory.hh
(tgba_bdd_concrete_factory::now_to_next_): New variable.
2003-06-28 Alexandre Duret-Lutz <aduret@src.lip6.fr>
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-26 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* Makefile.am (EXTRA_DIST): Add HACKING.
* configure.ac: Bump version to 0.0c.
* configure.ac: Bump version to 0.0b.
* INSTALL: New file.
* src/tgba/ltl2tgba.hh, src/tgba/ltl2tgba.cc: Move ...
* src/tgbaalgos/ltl2tgba.hh, src/tgbaalgos/ltl2tgba.cc: ... here.
* src/tgba/Makefile.am, src/tgbaalgos/Makefile.am: Adjust.
* src/tgba/public.hh: Do not include ltl2tgba.hh.
* src/tgbatests/explprod.cc, src/tgbatests/ltl2tgba.cc,
src/tgbatests/ltlprod.cc, src/tgbatests/mixprod.cc,
src/tgbatests/reach.cc, src/tgbatests/tripprod.cc: Adjust inclusions.
* src/tgba/tgbabddcoredata.hh: Fix some Doxygen comments.
* src/ltlast/formula.hh: More Doxygen comments.
* src/tgba/tgba.hh: Use <tt> in Doxygen comments.
* doc/mainpage.dox: New file.
* doc/Makefile.am (EXTRA_DIST): Add mainpage.dox.
* doc/Doxyfile.in (INPUT): Add @srcdir@/mainpage.dox
* src/tgba/succiter.hh: Adjust comments about promises to
refer to accepting conditions.
* src/tgba/tgbabddconcretefactory.hh: Likewise.
* src/tgba/tgbabddcoredata.hh: Likewise.
* src/tgba/dictunion.cc: Likewise.
* src/tgba/tgba.hh: Likewise.
* doc/Makefile.am (doc): Typo.
* src/ltlvisit/tostring.hh (to_string): Add doxygen comments.
* src/ltlast/multop.hh (multop::paircmp): Add doxygen comments.
* src/tgba/tgbaexplicit.hh (tgba_explicit::transtion,
state_explicit, tgba_explicit_succ_iterator): Add doxygen comments.
* src/ltlvisit/postfix.hh: Typo.
* src/ltlast/Makefile.am (ltlastdir, ltlast_HEADERS): New variables.
(libltlast_la_SOURCES): Move all headers to ltlast_HEADERS.
* src/ltlenv/Makefile.am (ltlenvdir, ltlenv_HEADERS): New variables.
(libltlenv_la_SOURCES): Move all headers to ltlenv_HEADERS.
* src/ltlparse/Makefile.am (ltlparsedir, ltlparse_HEADERS): New
variables.
(libltlparse_la_SOURCES): Move all public headers to ltlparse_HEADERS.
* src/ltlvisit/Makefile.am (ltlvisitdir, ltlvisit_HEADERS): New
variables.
(libltlvisit_la_SOURCES): Move all headers to ltlparse_HEADERS.
* src/misc/Makefile.am (include_HEADERS): Rename as ..
(misc_HEADERS): ... this.
(miscdir): New variable.
* src/tgba/Makefile.am (tgbadir, tgba_HEADERS): New variables.
(libtgba_la_SOURCES): Move all headers to tgba_HEADERS.
* src/tgbaalgos/Makefile.am (tgbaalgosdir, tgbaalgos_HEADERS):
New variables.
(libtgbaalgos_la_SOURCES): Move all headers to tgbaalgos_HEADERS.
* src/tgbaparse/Makefile.am (tgbaparsedir, tgbaparse_HEADERS): New
variables.
(libtgbaparse_la_SOURCES): Move all public headers to
tgbaparse_HEADERS.
* src/tgbaparse/public.hh: Include ltlparse/location.hh, not
location.hh.
* doc/Makefile.am (stamp): Prefix $(srcdir) explicitely.
* m4/buddy.m4 (BUDDY_LDFLAGS): Use $(top_builddir), not $(top_srcdir).
* src/tgbaparse/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS).
* doc/Makefile.am: Rewrite to run Doxygen whenever Doxyfile.in
or configure.ac changes. Distribute the html doc.
* doc/Doxyfile.in (EXCLUDE_PATTERNS): Complete with
useless Bison classes.
(FILE_PATTERNS): Remove *.cc files.
Distribute BuDDy. Compile and link with the included version if
explicitely requested (--with-included-buddy) or if there is now
stuitable version already installed.
* buddy/: New directory. Contains a patched version of BuDDy 2.2.
* m4/buddy.m4: Make sure the installed BuDDy supports bdd_mergepairs.
Honor --with-included-buddy and --without-included-buddy. Define
the BUDDY_LDFLAGS and BUDDY_CPPFLAGS output variables, and the
WITH_INCLUDED_BUDDY Automake conditional
* Makefile.am [WITH_INCLUDED_BUDDY] (MAYBE_SUBDIRS): New variable.
(SUBDIRS): Prepend $(MAYBE_SUBDIRS).
* src/Makefile.am (libspot_LDFLAGS): New variable.
* src/tgba/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS).
* src/tgbaalgos/Makefile.am (AM_CPPFLAGS): Likewise.
* src/tgbatest/Makefile.am (AM_CPPFLAGS): Likewise.
2003-06-25 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next):
Rewrite using bdd_satoneset. This time it's for real. (I hope.)
* src/tgba/succiterconcrete.hh (current_base_,
current_base_left_): Delete.
* tgba/tgbabddcoredata.hh (next_set): New variable.
* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust
to update next_set.
* src/tgba/bddprint.hh, src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbaproduct.hh: Fix Doxygen comments.
* src/tgba/succiterconcrete.hh (next_succ_set_): Rename as ...
(succ_set_left_): ... this.
(current_base_, current_base_left_): New variables.
* src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::first):
Reset current_.
(tgba_succ_iterator_concrete::next): Rewrite.
(tgba_succ_iterator_concrete::current_state): Simplify.
(tgba_succ_iterator_concrete::current_accepting_conditions): Remove
atomic proposition with universal quantification.
* src/tgba/ltl2tgba.cc (ltl_to_tgba): Normalize the formula.
* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::set_init_state):
Complete the initial state.
(tgba_bdd_concrete::succ_iter): Do not remove Now variable
from the BDD passed to the iterator.
* tgba/tgbabddcoredata.hh (notnow_set, var_set): New variables.
* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust
to update notnow_set and var_set.
* src/tgbatest/ltl2tgba.cc: Support -v.
2003-06-24 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbatest/ltl2tgba.cc (syntax): Fix usage message.
* src/tgbatest/tripprod.test, src/tgbatest/explprod.test: Sort
accepting conditions.
* src/ltlvisit/nenoform.cc (negative_normal_form): New const variant.
* src/ltlvisit/nenoform.hh (negative_normal_form): New const variant.
* src/ltlvisit/lunabbrev.cc (unabbreviate_logic): New const variant.
* src/ltlvisit/lunabbrev.hh (unabbreviate_logic): New const variant.
* src/ltlvisit/tunabbrev.cc (unabbreviate_ltl): New const variant.
* src/ltlvisit/tunabbrev.hh (unabbreviate_ltl): New const variant.
2003-06-23 Alexandre Duret-Lutz <aduret@src.lip6.fr>
Switch from "promises" to "accepting sets". Fix the definitions
of these accepting sets so that they are really useful. Provide
an all_accepting_conditions() method for use in the emptyness
check, and a neg_accepting_conditions() for products. Predeclare
TGBA accepting conditions in the i/o.
* src/tgba/bddprint.cc (want_prom): Rename as ...
(want_prom): ... this.
(print_handler): Adjust to display Acc[].
(print_acc_handler, bdd_print_acc): New functions.
* src/tgba/bddprint.hh (print_acc_handler, bdd_print_acc):
New functions.
* src/tgba/succiter.hh (current_promise): Rename as ...
(current_accepting_conditions): ... this.
* src/tgba/succiterconcrete.cc (current_state):
Rename next to now.
(current_promise): Rename as ...
(current_accepting_conditions): ... this, and compute
the accepting conditions.
* src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc,
src/tgba/succiterconcrete.hh,
src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh,
src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
src/tgba/tgbabddtranslatefactory.cc,
src/tgbaalgos/dotty.cc: Adjust to new names.
* src/tgba/tgba.hh (all_accepting_conditions,
neg_accepting_conditions): New functions.
* src/tgba/tgbabddconcretefactory.cc: Adjust to new
names, and record accepting conditions instead of promises.
* src/tgba/tgbabddcoredata.hh (accepting_conditions,
all_accepting_conditions, negacc_set): New variables.
(notnow_set, notprom_set, declare_promise): Rename as ...
(notnext_set, notacc_set, declare_accepting_condition): ... these.
* src/tgba/tgbaexplicit.hh
(tgba_explicit_succ_iterator::current_promise): Rename as ...
(tgba_explicit_succ_iterator::current_accepting_conditions): ... this.
(tgba_explicit::add_promise): Rename as ...
(tgba_explicit::add_accepting_condition): ... this.
(tgba_explicit::declare_accepting_condition,
tgba_explicit::has_accepting_condition): New variables.
(tgba_explicit::get_promise): Rename as ...
(tgba_explicit::get_accepting_condition): ... this.
(tgba_explicit::all_accepting_conditions,
tgba_explicit::neg_accepting_conditions): Implement them.
(all_accepting_conditions, neg_accepting_conditions,
all_accepting_conditions): New variables.
(tgba_explicit_succ_iterator): Embed all_accepting_conditions_.
* src/tgba/tgbaexplicit.cc: Likewise.
* src/tgba/tgbaproduct.hh
(tgba_product_succ_uterator): Embed left_neg_ and right_neg_.
(tgba_product::all_accepting_conditions,
tgba_product::neg_accepting_conditions): Implement them.
* src/tgba/tgbatranslateproxy.hh:
(tgba_translate_proxy::all_accepting_conditions,
tgba_translate_proxy::neg_accepting_conditions): Implement them.
* src/tgba/tgbatranslateproxy.cc: Likewise.
* src/tgbaalgos/save.cc (save_rec): Call bdd_print
(tgba_save_reachable): Output the `acc =' line.
* src/tgbaparse/tgbaparse.yy: Support the for
accepting conditions definitions using an "acc =" line
at the start. Later, use has_accepting_condition while
parsing accepting conditions to ensure they were declared.
Disallow !cond in accepting conditions.
* src/tgbaparse/tgbascan.ll (ACC_DEF): New token.
* src/tgbatest/explicit.cc (main): Declare accepting conditions.
* src/tgbatest/ltl2tgba.cc (main): Add support for the -a, -A,
and -R new options.
* src/tgbatest/tgbaread.cc (main): Really exit on parse error.
* src/tgbatest/explicit.test, src/tgbatest/explprod.test,
src/tgbatest/mixprod.test, src/tgbatest/readsave.test,
src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Reflect
recent changes.
2003-06-22 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbatest/tripprod.test, src/tgbatest/explprod.test:
Sort out some possible inversions in the output.
2003-06-19 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbabddconcretefactory.cc
(tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory): destroy the
formulae used as keys in prom_.
(tgba_bdd_concrete_factory::create_promise): Delete.
(tgba_bdd_concrete_factory::declare_promise,
tgba_bdd_concrete_factory::finish): New functions.
* src/tgba/tgbabddconcretefactory.hh
(tgba_bdd_concrete_factory::create_promise): Delete.
(tgba_bdd_concrete_factory::declare_promise,
tgba_bdd_concrete_factory::finish): New functions.
(tgba_bdd_concrete_factory::prom_): New map.
* src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Adjust
the Fx and aUb cases to register promises with
tgba_bdd_concrete_factory::declare_promise().
(ltl2tgba): Call tgba_bdd_concrete_factory::finish().
* src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter):
Revert the change from 2003-06-12, it needs more work (the
automaton generated on Xa&(b U !a) was bogus, with that
patch).
* src/tgbatest/ltl2tgba.cc: Handle the -o and -r options.
* src/tgbatest/tripprod.test, src/tgbatest/explprod.test,
src/tgbatest/readsave.test: Adjust to reflect yesterday's
bddprint.cc change.
2003-06-18 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/bddprint.cc (print_handler): Quote promises
when !want_prom.
* src/tgbaparse/tgbaparse.yy (prop_list): Accept strings or
identifiers. Discard empty strings.
* src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test: New file.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add mixprod.
(mixprod_SOURCES): New variable.
(TESTS): Add mixprod.test.
2003-06-17 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product):
New constructor.
* src/tgba/tgbaproduct.hh (state_bdd_product::state_bdd_product):
New constructor.
* tgbatest/tripprod.cc, tgbatest/tripprod.test: New files.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
(tripprod_SOURCES): New variable.
(CLEANFILES): Add input3.
(TESTS): Add tripprod.test.
2003-06-16 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* 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.
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/explprod.cc, tgbatest/explprod.test: New files.
* tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
(explprod_SOURCES): New variable.
(TESTS): Add explprod.test.
(CLEANFILES): Add input1 and input2.
2003-06-12 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Make
sure to compute the status of the most Now variables possible.
This helps to identify equivalant states.
(tgba_bdd_concrete): Call set_init_state.
2003-06-10 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Handle F and G.
* src/tgbatest/ltl2tgba.test: Use F and G.
2003-06-06 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbatest/bddprod.test: New file.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add bddprod.
(bddprod_SOURCES, bddprod_CXXFLAGS): New variables.
(TESTS): Add bddprod.test.
* src/tgbatest/ltlprod.c: Handle BDD_CONCRETE_PRODUCT.
* src/tgba/dictunion.cc (tgba_bdd_dict_union): Clone formulae
while building new dictionary.
* src/tgbatest/ltlprod.test, src/tgbatest/ltlprod.cc: New files.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add ltlprod.
(ltlprod_SOURCES): New variable.
(TESTS): Add ltlprod.test.
* src/ltlvisit/clone.cc (clone): New const version.
* src/ltlvisit/clone.hh (clone): Likewise.
* src/ltlvisit/destroy.cc (destroy): New const version.
* src/ltlvisit/destroy.hh (destroy): Likewise.
* src/tgba/tgbabddconcretefactory.cc
(tgba_bdd_concrete_factory::create_state,
tgba_bdd_concrete_factory::create_atomic_prop,
tgba_bdd_concrete_factory::promise): Clone new formulae.
* src/tgba/tgbabdddict.cc (tgba_bdd_dict::tgba_bdd_dict,
tgba_bdd_dict::~tgba_bdd_dict, tgba_bdd_dict::operator=): New methods
that clone and destroy formulae.
* src/tgbatest/ltl2tgba.test, src/tgbatest/ltl2tgba.cc: New files.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add ltl2tgba.
(ltl2tgba_SOURCES): New variable.
(TESTS): Add ltl2tgba.test.
* src/ltltest/equals.cc, src/ltltest/readltl.cc,
src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include <cassert>.
2003-06-05 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/bddprint.cc (dict): Make this variable static.
(want_prom): New global static variable.
(print_handle): Honor want_prom.
(print_sat_handler, bdd_print_sat, bdd_format_sat): New functions.
(bdd_print_set, bdd_print_dot, bdd_print_table): Set want_prom.
* src/tgba/bddprint.hh (bdd_print_sat, bdd_format_sat): New functions.
* src/tgbaalgos/save.cc, src/tgbaalgos/save.hh,
src/tgbatest/readsave.cc, src/tgbatest/readsave.test: New files.
* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add
save.cc and save.hh.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add readsave.
(readsave_SOURCES): New variable.
(TESTS): Add readsave.test.
* configure.ac: Output src/tgbaparse/Makefile.
* src/Makefile.am (SUBDIRS): Add tgbaparse.
(libspot_la_LDADD): Add tgbaparse/libtgbaparse.la.
* src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition,
tgba_explicit::get_promise, tgba_explicit::add_neg_condition,
tgba_explicit::add_neg_promise): New methods.
* src/tgba/tgbaexplicit.hh: Declare them.
* src/tgbaparse/Makefile.am, src/tgbaparse/fmterror.cc,
src/tgbaparse/parsedecl.hh, src/tgbaparse/public.hh,
src/tgbaparse/tgbaparse.yy, src/tgbaparse/tgbascan.ll,
src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test: New files.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add tgbaread.
(TESTS): Add tgbaread.cc.
(CLEANFILES): Add input.
(tgbaread_SOURCES): New variable.
* src/ltlparse/ltlparse.yy: Typo in comment.
* configure.ac: Output src/tgbatest/Makefile and src/tgbatest/defs.
* src/Makefile.am (SUBDIRS): Add tgbatest.
* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc: New file.
* src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgbaexplicit.cc
and tgbaexplicit.hh.
* src/tgbatest/Makefile.am, src/tgbatest/defs.in,
src/tgbatest/explicit.cc, src/tgbatest/explicit.test: New files.
2003-06-04 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/ltlparse/ltlparse.yy (result): Suppress unused definition.
* src/Makefile.am (SUBDIRS): Build `ltltest' after `.'.
* src/ltlparse/ltlscan.ll: Use ltlyy as %prefix.
* src/ltlparse/parsedecl.hh (YY_DECL): Rename yylex to ltlyylex.
* src/ltlparse/ltlparse.yy: Define yylex as ltlyylex.
2003-06-03 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc,
src/tgba/succiterconcrete.cc, src/tgba/tgbabddconcrete.cc,
src/tgba/tgbabddprod.cc, src/tgba/tgbabddtranslatefactory.cc,
src/tgba/tgbabddtranslateproxy.cc: Include <cassert>.
2003-06-02 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbabdddict.cc, src/tgba/tgbabdddict.hh: New files.
* src/tgba/Makefile.am (libtgba_la_SOURCES): Add them.
* src/tgba/tgbabdddict.cc (tgba_bdd_dict::contains): New function.
* src/tgba/tgbabdddict.hh (tgba_bdd_dict::contains): Likewise.
2003-05-28 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/statebdd.hh (state_bdd::as_bdd): Add non-const variant.
* src/tgba/tgbabddtranslateproxy.cc,
src/tgba/tgbabddtranslateproxy.hh: New files.
* src/tgba/Makefile.am (libtgba_la_SOURCES): Add them.
2003-05-27 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/bddprint.cc, src/tgba/bddprint.hh,
src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh,
src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbabddconcreteproduct.cc,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddfactory.hh,
src/tgba/tgbabddtranslatefactory.hh, src/tgbaalgos/dotty.cc:
Add Doxygen comments.
* src/tgba/bddfactory.hh, src/tgba/statebdd.hh,
src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add
Doxygen comments.
* 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.
* 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/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-26 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files.
* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them.
* src/tgba/tgbabddtranslatefactory.cc
(tgba_bdd_translate_factory::compute_pairs): Be quiet.
* src/Makefile.am (SUBDIRS): Add tgbaalgos.
(libspot_la_LIBADD): Add tgba/libtgbaalgos.
* src/tgbaalgos/Makefile.am: New file.
* configure.ac: Output src/tgbaalgos/Makefile.
* src/tgba/bddprint.hh, src/tgba/bddprint.cc: New files.
* src/tgba/Makefile.am (libtgba_la_SOURCES): Add them.
* src/tgba/public.hh: Include bddprint.hh.
* src/tgba/tgba.hh: Rename as ...
* src/tgba/public.hh: .. this.
* src/tgba/tgba.hh: New file.
* src/tgba/Makefile.am (libtgba_la_SOURCES): Add public.hh.
* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Inherit from tgba.
(tgba_bdd_concrete::init_iter): Delete.
(tgba_bdd_concrete::succ_iter): Take a state_bdd as argument,
not a bdd.
* src/tgba/tgbabddconcrete.cc: Likewise.
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.
* configure.ac: Output src/tgba/Makefile.
* 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-23 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* m4/gccwarn.m4: Do not use -Winline, this is inappropriate
with STL.
* src/ltlast/atomic_prop.cc, src/ltlvisit/lunabbrev.cc,
src/ltlvisit/nenoform.cc: Include <cassert>.
2003-05-16 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/ltlvisit/dotty.cc: Rewrite to display formulae as
graphs rather than trees, to show how nodes are shared.
* src/ltlvisit/dump.hh (dump): Return the passed ostream.
* src/ltlvisit/dump.cc (dump): Likewise.
* src/ltlvisit/dotty.hh (dotty): Likewise.
* src/ltlvisit/dotty.cc (dotty): Likewise.
* src/ltlvisit/tostring.hh (to_string): Likewise.
* src/ltlvisit/tostring.cc (to_string): Likewise.
* src/ltlvisit/dump.hh (dump): Take a formula* as argument,
not a formula&. This is more homogeneous.
* src/ltlvisit/dump.cc (dump): Likewise.
* src/ltlvisit/dotty.hh (dotty): Likewise.
* src/ltlvisit/dotty.cc (dotty): Likewise.
* src/ltlvisit/tostring.hh (to_string): Likewise.
* src/ltlvisit/tostring.cc (to_string): Likewise.
* src/ltltest/readltl.cc, src/ltltest/equals.cc,
src/ltltest/tostring.cc: Adjust usage.
Check trivial multop equality at build time. This makes the equal
visitor useless, since two equals formulae will now share the same
address.
* src/ltlast/multop.hh (add_sorted): New function.
(paircmp): New comparison functor.
(map): Use paircmp, we want to compare the vectors' contents,
not their addresses.
* src/ltlast/multop.cc (add_sorted): New function.
(add): Use it.
* src/ltltest/equals.cc, src/ltltest/tostring.cc: Compare
pointers instead of calling equal.
* src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: Delete.
* src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Remove
equals.cc and equals.hh.
* wrap/spot.i: Do not include equals.hh.
2003-05-15 Alexandre Duret-Lutz <aduret@src.lip6.fr>
Implement spot::ltl::destroy() and exercise it.
* src/ltlast/atomic_prop.hh: Declare instance_count().
* src/ltlast/binop.hh, src/ltlast/unop.hh, src/ltlast/multop.hh:
Likewise. Also, really inherit for ref_formula this time.
* src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
src/ltlast/unop.cc, src/ltlast/multop.cc: On destruction, suppress
the instance from the instance map. Implement instance_count().
* src/ltlast/formula.cc, src/ltlast/formula.hh,
src/ltlast/ref_formula.cc, src/ltlast/ref_formula.hh: Add virtual
destructors.
* src/ltlparse/ltlparse.yy: Recover from binary operators with
missing right hand operand (the point is just to destroy the
the left hand operand).
* src/ltltest/equals.cc, src/ltltest/readltl.cc,
src/ltltest/tostring.cc: Destroy used formulae. Make sure
instance_count()s are null are the end.
* src/ltltest/parseerr.test: Adjust expected result, now
that the parser lnows about missing right hand operands.
* src/ltlvisit/destroy.hh, src/ltlvisit/destroy.cc,
src/ltlvisit/postfix.hh, src/ltlvisit/postfix.cc: New files.
* src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Add them.
* src/ltlvisit/lunabbrev.cc (Xor, Equiv): Clone formulae
occurring twice in the rewritten expression.
Massage the AST so that identical sub-formula share the same
reference-counted formula*. One can't call constructors for AST
items anymore, everything need to be acquired through instance()
class methods.
* src/ltlast/formula.cc, src/ltlast/refformula.cc,
src/ltlast/refformula.hh: New files.
* src/ltlast/Makefile.am (libltlast_la_SOURCES): Add them.
* src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/unop.cc, src/ltlast/unop.hh,
src/ltlast/binop.cc, src/ltlast/binop.hh: Make the constructor
and destructor protected. Define a static function `instance()'
to get an instance with specific argument. Use a map called
`instances' to store all known instances. Inherit from
ref_formula.
* src/ltlast/constant.hh, src/ltlast/constant.cc: Protect
the constructor and destructor. Provide the false_instance()
and true_instance() functions instead.
* src/formula.hh (ref, unref, ref_, unref_): New methods.
* src/ltlast/multop.cc, src/ltlast/multop.hh: Protect
the constructor, destructor, as well as the add() method.
Provides the instance(), and add() class methods instead.
Store children_ as a pointer.
* src/ltlenv/defaultenv.cc (require): Adjust to
call atomic_prop::instance.
* src/ltlparse/ltlparse.yy: Adjust to call instance() functions
instead of constructors.
* src/ltltest/Makefile.am (LDADD): Tweak library ordering.
* src/ltlvisit/clone.hh (clone_visitor): Inherit from visitor,
not const_visitor, and adjust all prototypes appropriately.
* src/ltlvisit/clone.cc (clone_visitor): Likewise.
Call ref() or instance() methods instead of copy constructors.
* src/ltlvisit/equals.cc: Simplify atomic_prop and constant
cases.
* src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc,
src/ltlvisit/tunabbrev.hh, src/ltlvisit/tunabbrev.cc,
src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: Use instance()
methods instead of constructor. Make these children of visitor, not
const_visitor.
* src/ltltest/readltl.c (main): Do not delete the formula.
* src/ltlparse/ltlscan.ll (to_parse_size): Declare as size_t to
remove a warning with newer versions of Flex.
* src/ltlparse/ltlparse.yy (error_list, parse_environment, result):
CVS Bison now supports %parse-param for the C++ skeleton; pass these
variables as arguments to the Parser::Parser constructor instead of
using globals.
(parse): Adjust Parser::Parser call.
2003-05-12 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/ltlvisit/tostring.cc: Reindent and strip out superfluous
spot::ltl:: prefixes.
(to_string(formula)): New function.
* src/ltlvisit/tostring.hh (to_string(formula)): Likewise.
* src/ltltest/tostring.cc: Use this new to_string function to
simplify.
2003-05-05 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* m4/buddy.m4: New file.
* Makefile.am (EXTRA_DIST): Add m4/buddy.m4.
* configure.ac: Call AX_CHECK_BUDDY.
2003-04-30 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/ltlvisit/Makefile.am (lib_LTLIBRARIES): Rename as ...
(noinst_LTLIBRARIES): ... this.
* src/ltlenv/Makefile.am, src/ltlast/Makefile.am,
src/ltlparse/Makefile.am: Likewise.
* src/Makefile.am (lib_LTLIBRARIES, libspot_la_SOURCES,
libspot_la_LIBADD): New variable. Build a libspot.la library
from all the sub-libraries.
* m4/pypath.m4: New file.
* Makefile.am (SUBDIRS): Add wrap.
* wrap/Makefile.am: New file.
* wrap/spot.i: New file. Preliminary bindings for Python.
* configure.ac: Call adl_CHECK_PYTHON and output wrap/Makefile.
2003-04-29 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* configure.ac: Call AC_PROG_LIBTOOL.
* src/ltlast/Makefile.am, src/ltlenv/Makefile.am,
src/ltlparse/Makefile.am, src/ltltest/Makefile.am,
src/ltlvisit/Makefile.am: Adust to build libtool libraries.
* src/ltlenv/defaultenv.hh: Do not include atomic_prop.hh here...
* src/ltlenv/defaultenv.cc: ... but here.
* src/ltltest/tostring.test: Simplify with set -e. Move the
description of the test ...
* src/ltltest/tostring.cc: ... here, where it is actually coded.
* src/ltltest/lunabbrev.test, src/ltltest/tunabbrev.test,
src/ltltest/nenoform.test, src/ltltest/tunenoform.test:
Simplify with set -e.
* configure.ac (AM_INIT_AUTOMAKE): Use nostdinc, to make
sure we always use paths relative to src/ in src/'s
subdirectories.
2003-04-28 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/ltlparse/Makefile.am (CXXFLAGS): Turn on GCC warnings
now that CVS Bison is fixed.
* src/ltlparse/ltlscan.ll: Use yyunput to shut up a GCC warning.
2003-04-24 Rachid REBIHA <rebiha@nyx>
* src/ltltest/tostring.test: New file.
* src/ltltest/tostring.cc: New files.
* src/ltlvisit/tostring.hh: From ast to string New files.
* src/ltlvisit/tostring.cc: From ast to string New files.
2003-04-18 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/ltlparse/Makefile.am (EXTRA_DIST): Distribute ltlparse.yy.
* src/ltlast/Makefile.am (libltlast_a_SOURCES): Add visitor.hh.
* src/ltlast/atomic_prop.hh, src/ltlast/binop.hh,
src/ltlast/constant.hh, src/ltlast/formula.hh,
src/ltlast/multop.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh,
src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh,
src/ltlparse/public.hh, src/ltlvisit/clone.hh,
src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh,
src/ltlvisit/equals.hh, src/ltlvisit/lunabbrev.hh,
src/ltlvisit/nenoform.hh, src/ltlvisit/tunabbrev.hh: Add
Doxygen comments.
* src/visitor.hh: Do not use const_sel. This clarifies
the code and helps Doxygen.
* configure.ac: Output doc/Doxyfile and doc/Makefile.
* doc/Makefile.am, doc/Doxyfile.in: New files.
* Makefile.am (SUBDIRS): Add doc.
* src/ltlparse/ltlscan.ll: Recognize && and ||.
* src/ltltest/parse.test, src/ltltest/parseerr.test,
src/ltltest/equals.test: Use these operators..
2003-04-17 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/ltltest/readltl.cc, src/ltltest/equals.cc: Cosmetics.
* src/ltlenv/environment.hh (require): Return a formula, not
an atomic_prop.
* src/ltlast/atomic_prop.hh (atomic_prop): New argument env.
(environment_): New member.
(env): New method.
* src/ltlast/atomic_prop.cc (atomic_prop, env): Likewise.
* src/ltlenv/defaultenv.cc (require): Pass *this as the
environment argument to atomic_prop.
* src/ltlvisit/clone.cc (visit(const atomic_prop*)): Also copy
the environment.
* src/ltlvisit/nenoform.cc (visit(const atomic_prop*)): Likewise.
* configure.ac: Output src/ltlenv/Makefile.
* src/ltlenv/Makefile.am, src/ltlenv/defaultenv.cc,
src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh: New files.
* src/ltlparse/public.hh (parse): Take an environment as third
argument.
* src/ltlparse/ltlparse.yy (ATOMIC_PROP, parse): Require the
atomic proposition via the environment.
* src/ltltest/readltl.cc (main): Adjust the call to parse().
* src/ltltest/Makefile.am (LDADD): Add ../ltlenv/libltlenv.a.
* src/ltlvisit/clone.hh, src/ltlvisit/clone.cc: New files.
* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
* src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Inherit
from clone_visitor and remove all useless methods (now inherited).
* src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: New files.
* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
* src/ltltest/equals.cc (main) [NENOFORM]: Call negative_normal_form.
* src/ltltest/nenoform.test, src/ltltest/tunenoform.test: New files.
* src/ltltest/Makefile.am (check_PROGRAMS): Add nenoform and
tunenoform.
(nenoform_SOURCES, nenoform_CPPFLAGS, tunenoform_SOURCES,
tunenoform_CPPFLAGS): New variables.
(TESTS): Add nenoform.test and tunenoform.test.
* src/ltlvisit/lunabbrev.hh: Fix include guard.
2003-04-16 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh: New files.
* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
* src/ltltest/tunabbrev.test: New file.
* src/ltltest/lunabbrev.test: Fix comment.
* src/ltltest/Makefile.am (TESTS): Add tunabbrev.test.
(check_PROGRAMS): Add tunabbrev.
(tunabbrev_SOURCES, tunabbrev_CPPFLAGS): New variables.
* src/ltltest/equals.cc (main) [TUNABBREV]: Call unabbreviate_ltl.
* src/ltlvisit/lunabbrev.hh (unabbreviate_logic_visitor::recurse):
New virtual function.
* src/ltlvisit/lunabbrev.cc (unabbreviate_logic_visitor::recurse):
Likewise.
(unabbreviate_logic_visitor::visit): Use it instead of calling
unabbreviate_logic directly.
* src/ltlvisit/lunabbrev.hh: Add missing include guard.
* src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: New files.
* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
* src/ltlast/multop.cc (multop::multop(type)): New constructor.
* src/ltlast/multop.hh (multop::multop(type)): New constructor.
* src/ltltest/lunabbrev.test: New file.
* src/ltltest/Makefile.am (TESTS): Add lunabbrev.test.
(check_PROGRAMS): Add lunabbrev.
(lunabbrev_SOURCES, lunabbrev_CPPFLAGS): New variables.
* src/ltltest/equals.cc (main) [LUNABBREV]: Call unabbreviate_logic.
* src/ltltest/equals.test (check0, check1): Remove. Use check 0, and
check 1 instead.
* src/ltlast/formulae.hh: Rename as ...
* src/ltlast/formula.hh: ... this.
* src/ltlast/Makefile.am (libltlast_a_SOURCES): Adjust.
* src/ltlast/formula.hh (formulae): Rename as ...
(formula): ... this.
Adjust all uses.
* src/ltlparse/public.hh (format_parse_errors): New function.
* src/ltlparse/fmterror.cc: New file.
* src/ltlparse/Makefile.am (libltlparse_a_SOURCES): Add fmterror.cc.
* src/ltltests/equals.cc, src/ltltests/readltl.cc: Simplify using
format_parse_errors.
* src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: New files.
* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add equals.hh
and equals.cc.
* src/ltltest/equals.cc, src/ltltest/equals.test: New files.
* src/ltltest/Makefile.am (check_PROGRAMS): Add equals.
(equals_SOURCES): New variable.
(TESTS): Add equals.test.
* src/ltlast/multop.cc (multop::multop): Use multop::add.
(multop::add): If the formulae we add is itself a multop for the
same operator, merge its children with ours.
* src/ltltest/parseerr.test: Add two tests for multop merging.
2003-04-15 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/ltlast/formulae.hh (formulae::equals): Remove.
* src/ltlast/unop.hh (unop::equals): Remove.
* src/ltlast/unop.cc (unop::equals): Remove.
* src/ltlast/binop.hh (binop::equals): Remove.
* src/ltlast/binop.cc (binop::equals): Remove.
* src/ltlast/multop.hh (multop::equals): Remove.
* src/ltlast/multop.cc (multop::equals): Remove.
* src/ltlast/atomic_prop.hh (atomic_prop::equals): Remove.
* src/ltlast/atomic_prop.cc (atomic_prop::equals): Remove.
* src/ltlast/constant.hh (constant::equals): Remove.
* src/ltlast/constant.cc (constant::equals): Remove.
* HACKING, Makefile.am, configure.ac, m4/gccwarn.m4,
src/Makefile.am, src/ltlast/Makefile.am, src/ltlast/allnodes.hh,
src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc,
src/ltlast/constant.hh, src/ltlast/formulae.hh,
src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/predecl.hh,
src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlast/visitor.hh,
src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
src/ltlparse/public.hh, src/ltlvisit/Makefile.am,
src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
src/ltlvisit/rewrite.cc, src/ltlvisit/rewrite.hh,
src/ltltest/Makefile.am, src/ltltest/defs.in, src/ltltest/readltl.cc,
src/ltltest/parse.test, src/ltltest/parseerr.test,
src/misc/Makefile.am, src/misc/const_sel.hh: New files.
Reference in a new issue View git blame Copy permalink