diff --git a/ChangeLog b/ChangeLog index eb6744984..fbcefcf2c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2003-09-22 Alexandre Duret-Lutz + + * 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-11 Alexandre Duret-Lutz * src/tgba/state.hh: Include cassert. diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index 638223fe9..32394987e 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -3,7 +3,7 @@ #include "ltlvisit/destroy.hh" #include "tgba/tgbatba.hh" #include "tgba/tgbaproduct.hh" -#include "tgbaalgos/ltl2tgba.hh" +#include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/magic.hh" @@ -38,7 +38,7 @@ main(int argc, char **argv) #if FM spot::tgba* a_f = spot::ltl_to_tgba_fm(f, dict); #else - spot::tgba* a_f = spot::ltl_to_tgba(f, dict); + spot::tgba* a_f = spot::ltl_to_tgba_lacim(f, dict); #endif spot::ltl::destroy(f); diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index ba679469e..b3a87b68e 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -7,8 +7,8 @@ tgbaalgos_HEADERS = \ reachiter.hh \ dotty.hh \ lbtt.hh \ - ltl2tgba.hh \ ltl2tgba_fm.hh \ + ltl2tgba_lacim.hh \ magic.hh \ save.hh @@ -17,7 +17,7 @@ libtgbaalgos_la_SOURCES = \ reachiter.cc \ dotty.cc \ lbtt.cc \ - ltl2tgba.cc \ ltl2tgba_fm.cc \ + ltl2tgba_lacim.cc \ magic.cc \ save.cc diff --git a/src/tgbaalgos/ltl2tgba.cc b/src/tgbaalgos/ltl2tgba_lacim.cc similarity index 98% rename from src/tgbaalgos/ltl2tgba.cc rename to src/tgbaalgos/ltl2tgba_lacim.cc index 8934f5e62..505da9546 100644 --- a/src/tgbaalgos/ltl2tgba.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -6,7 +6,7 @@ #include "tgba/tgbabddconcretefactory.hh" #include -#include "ltl2tgba.hh" +#include "ltl2tgba_lacim.hh" namespace spot { @@ -231,7 +231,7 @@ namespace spot }; tgba_bdd_concrete* - ltl_to_tgba(const ltl::formula* f, bdd_dict* dict) + ltl_to_tgba_lacim(const ltl::formula* f, bdd_dict* dict) { // Normalize the formula. We want all the negations on // the atomic propositions. We also suppress logic diff --git a/src/tgbaalgos/ltl2tgba.hh b/src/tgbaalgos/ltl2tgba_lacim.hh similarity index 91% rename from src/tgbaalgos/ltl2tgba.hh rename to src/tgbaalgos/ltl2tgba_lacim.hh index 0e6999e69..78fc0d788 100644 --- a/src/tgbaalgos/ltl2tgba.hh +++ b/src/tgbaalgos/ltl2tgba_lacim.hh @@ -24,7 +24,7 @@ namespace spot /// editor = {Pierre Leroux} /// } /// \endverbatim - tgba_bdd_concrete* ltl_to_tgba(const ltl::formula* f, bdd_dict* dict); + tgba_bdd_concrete* ltl_to_tgba_lacim(const ltl::formula* f, bdd_dict* dict); } #endif // SPOT_TGBA_LTL2TGBA_HH diff --git a/src/tgbatest/explprod.cc b/src/tgbatest/explprod.cc index 1d7c32229..1015113a5 100644 --- a/src/tgbatest/explprod.cc +++ b/src/tgbatest/explprod.cc @@ -1,6 +1,5 @@ #include #include -#include "tgbaalgos/ltl2tgba.hh" #include "tgba/tgbaexplicit.hh" #include "tgba/tgbaproduct.hh" #include "tgbaparse/public.hh" diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 3167499b5..d3121447a 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -5,7 +5,7 @@ #include "ltlvisit/destroy.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" -#include "tgbaalgos/ltl2tgba.hh" +#include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgba/bddprint.hh" #include "tgbaalgos/dotty.hh" @@ -139,7 +139,7 @@ main(int argc, char** argv) if (fm_opt) to_free = a = spot::ltl_to_tgba_fm(f, dict); else - to_free = a = concrete = spot::ltl_to_tgba(f, dict); + to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); spot::ltl::destroy(f); diff --git a/src/tgbatest/ltlmagic.cc b/src/tgbatest/ltlmagic.cc index 660748dbe..e99e3b93b 100644 --- a/src/tgbatest/ltlmagic.cc +++ b/src/tgbatest/ltlmagic.cc @@ -3,7 +3,7 @@ #include "ltlvisit/destroy.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" -#include "tgbaalgos/ltl2tgba.hh" +#include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/magic.hh" void @@ -47,7 +47,7 @@ main(int argc, char** argv) spot::bdd_dict* dict = new spot::bdd_dict(); { - spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba(f1, dict); + spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba_lacim(f1, dict); spot::tgba_tba_proxy* a2 = new spot::tgba_tba_proxy(a1); spot::ltl::destroy(f1); diff --git a/src/tgbatest/ltlprod.cc b/src/tgbatest/ltlprod.cc index 572830dbb..ece422dfd 100644 --- a/src/tgbatest/ltlprod.cc +++ b/src/tgbatest/ltlprod.cc @@ -3,7 +3,7 @@ #include "ltlvisit/destroy.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" -#include "tgbaalgos/ltl2tgba.hh" +#include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgba/tgbaproduct.hh" #include "tgba/tgbabddconcreteproduct.hh" #include "tgbaalgos/dotty.hh" @@ -39,8 +39,8 @@ main(int argc, char** argv) spot::bdd_dict* dict = new spot::bdd_dict(); { - spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba(f1, dict); - spot::tgba_bdd_concrete* a2 = spot::ltl_to_tgba(f2, dict); + spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba_lacim(f1, dict); + spot::tgba_bdd_concrete* a2 = spot::ltl_to_tgba_lacim(f2, dict); spot::ltl::destroy(f1); spot::ltl::destroy(f2); diff --git a/src/tgbatest/mixprod.cc b/src/tgbatest/mixprod.cc index 396254621..c1cc3431d 100644 --- a/src/tgbatest/mixprod.cc +++ b/src/tgbatest/mixprod.cc @@ -3,7 +3,7 @@ #include "ltlvisit/destroy.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" -#include "tgbaalgos/ltl2tgba.hh" +#include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgba/tgbaproduct.hh" #include "tgba/tgbabddconcreteproduct.hh" #include "tgbaparse/public.hh" @@ -39,7 +39,7 @@ main(int argc, char** argv) return 2; { - spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba(f1, dict); + spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba_lacim(f1, dict); spot::ltl::destroy(f1); spot::tgba_product p(a1, a2); spot::tgba_save_reachable(std::cout, &p); diff --git a/src/tgbatest/tripprod.cc b/src/tgbatest/tripprod.cc index 2004ab2b1..2c2614698 100644 --- a/src/tgbatest/tripprod.cc +++ b/src/tgbatest/tripprod.cc @@ -1,6 +1,5 @@ #include #include -#include "tgbaalgos/ltl2tgba.hh" #include "tgba/tgbaexplicit.hh" #include "tgba/tgbaproduct.hh" #include "tgbaparse/public.hh" diff --git a/wrap/python/cgi/ltl2tgba.in b/wrap/python/cgi/ltl2tgba.in index 48879b60f..8d30313eb 100644 --- a/wrap/python/cgi/ltl2tgba.in +++ b/wrap/python/cgi/ltl2tgba.in @@ -161,7 +161,7 @@ print '

Building automaton...', sys.stdout.flush() if trans_lacim: - automaton = spot.ltl_to_tgba(f, dict) + automaton = spot.ltl_to_tgba_lacim(f, dict) elif trans_fm: automaton = spot.ltl_to_tgba_fm(f, dict) diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 0f4a8405e..4d1808856 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -48,7 +48,7 @@ #include "tgba/tgbaproduct.hh" #include "tgba/tgbatba.hh" -#include "tgbaalgos/ltl2tgba.hh" +#include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" @@ -84,7 +84,7 @@ using namespace spot; %include "ltlvisit/tostring.hh" %include "ltlvisit/tunabbrev.hh" -%feature("new") spot::ltl_to_tgba; +%feature("new") spot::ltl_to_tgba_lacim; %feature("new") spot::ltl_to_tgba_fm; %feature("new") spot::tgba::get_init_state; %feature("new") spot::tgba::succ_iter; @@ -105,7 +105,7 @@ using namespace spot; %include "tgba/tgbaproduct.hh" %include "tgba/tgbatba.hh" -%include "tgbaalgos/ltl2tgba.hh" +%include "tgbaalgos/ltl2tgba_lacim.hh" %include "tgbaalgos/ltl2tgba_fm.hh" %include "tgbaalgos/dotty.hh" %include "tgbaalgos/lbtt.hh" diff --git a/wrap/python/tests/interdep.py b/wrap/python/tests/interdep.py index 05015922d..8fa948413 100755 --- a/wrap/python/tests/interdep.py +++ b/wrap/python/tests/interdep.py @@ -7,7 +7,7 @@ e = spot.default_environment.instance() p = spot.empty_parse_error_list() f = spot.parse('GFa', p, e) dict = spot.bdd_dict() -a = spot.ltl_to_tgba(f, dict) +a = spot.ltl_to_tgba_lacim(f, dict) s0 = a.get_init_state() b = s0.as_bdd() print b diff --git a/wrap/python/tests/ltl2tgba.py b/wrap/python/tests/ltl2tgba.py index 12c77a166..f5c1f0728 100755 --- a/wrap/python/tests/ltl2tgba.py +++ b/wrap/python/tests/ltl2tgba.py @@ -77,7 +77,7 @@ if f: a = spot.ltl_to_tgba_fm(f, dict) concrete = 0 else: - a = concrete = spot.ltl_to_tgba(f, dict) + a = concrete = spot.ltl_to_tgba_lacim(f, dict) spot.destroy(f) del f