diff --git a/README b/README index 588ab6dcf..9176f68b2 100644 --- a/README +++ b/README @@ -41,7 +41,7 @@ Optional third-party dependencies If the SAT-solver glucose is found on your system, it will be used by our test suite to test our SAT-based minimization algorithm. -Spot used to distribute a modified version of LBTT (an LTL to Büchi +Spot used to distribute a modified version of LBTT (an LTL to Büchi test bench), mostly fixing errors reported by recent compilers. However Spot now distributes its own reimplementation of LBTT, called ltlcross, so the use of LBTT is completely optional. The last @@ -151,12 +151,12 @@ src/ Sources for libspot. ltltest/ Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/. misc/ Miscellaneous support files. priv/ Private algorithms, used internally but not exported. - tgba/ TGBA objects and cousins. - tgbaalgos/ Algorithms on TGBA. - gtec/ Couvreur's Emptiness-Check. ta/ TA objects and cousins (TGTA). taalgos/ Algorithms on TA/TGTA. - tgbatest/ Tests for tgba/, tgbaalgos/, ta/ and taalgos/. + tgbaalgos/ Algorithms on TGBA. + gtec/ Couvreur's Emptiness-Check. + tgbatest/ Tests for twa/, tgbaalgos/, ta/ and taalgos/. + twa/ TωA objects and cousins. sanity/ Sanity tests for the whole project. doc/ Documentation for libspot. org/ Source of userdoc/ as org-mode files. @@ -166,7 +166,7 @@ doc/ Documentation for libspot. bench/ Benchmarks for ... dtgbasat/ ... SAT-based minimization of DTGBA, emptchk/ ... emptiness-check algorithms, - ltl2tgba/ ... LTL-to-Büchi translation algorithms, + ltl2tgba/ ... LTL-to-Büchi translation algorithms, ltlcounter/ ... translation of a class of LTL formulae, ltlclasses/ ... translation of more classes of LTL formulae, spin13/ ... compositional suspension and other improvements, @@ -197,10 +197,11 @@ debian/ Configuration file to build Debian packages. ------------------------------------------------------------------------------- Local Variables: mode: text +coding: utf-8 End: - LocalWords: Python's BuDDy LBTT LTL Büchi lbtt gspn DIR GreatSPN Soheib Yann - LocalWords: Baarir Thierry Mieg CVS Università di Torino devel src libspot ac + LocalWords: Python's BuDDy LBTT LTL Büchi lbtt gspn DIR GreatSPN Soheib Yann + LocalWords: Baarir Thierry Mieg CVS Università di Torino devel src libspot ac LocalWords: ltlast ltlenv ltlparse ltlvisit ltltest misc tgba TGBA tgbaalgos LocalWords: gtec Tarjan tgbatest doc html PDF spotref pdf cgi ELTL LocalWords: CGI ltl iface BDD Couvreur's emptchk kripke Kripke saba vm diff --git a/bench/stutter/stutter_invariance_randomgraph.cc b/bench/stutter/stutter_invariance_randomgraph.cc index bc2303f53..cda96ed29 100644 --- a/bench/stutter/stutter_invariance_randomgraph.cc +++ b/bench/stutter/stutter_invariance_randomgraph.cc @@ -25,8 +25,8 @@ #include "tgbaalgos/product.hh" #include "tgbaalgos/stutter.hh" #include "tgbaalgos/stats.hh" -#include "tgba/tgbagraph.hh" -#include "tgba/bdddict.hh" +#include "twa/tgbagraph.hh" +#include "twa/bdddict.hh" #include "misc/random.hh" #include #include diff --git a/configure.ac b/configure.ac index f74f68274..ca9744e7b 100644 --- a/configure.ac +++ b/configure.ac @@ -219,7 +219,7 @@ AC_CONFIG_FILES([ src/sanity/Makefile src/tgbaalgos/gtec/Makefile src/tgbaalgos/Makefile - src/tgba/Makefile + src/twa/Makefile src/taalgos/Makefile src/ta/Makefile src/tgbatest/defs diff --git a/iface/ltsmin/modelcheck.cc b/iface/ltsmin/modelcheck.cc index ae313ddf7..adc8ffecc 100644 --- a/iface/ltsmin/modelcheck.cc +++ b/iface/ltsmin/modelcheck.cc @@ -26,7 +26,7 @@ #include "tgbaalgos/emptiness.hh" #include "tgbaalgos/reducerun.hh" #include "tgbaalgos/postproc.hh" -#include "tgba/tgbaproduct.hh" +#include "twa/twaproduct.hh" #include "misc/timer.hh" #include "misc/memusage.hh" #include diff --git a/src/Makefile.am b/src/Makefile.am index 30f47e9e7..39ab34165 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -25,7 +25,7 @@ AUTOMAKE_OPTIONS = subdir-objects # List directories in the order they must be built. Keep tests at the # end, after building '.' (since the current directory contains # libspot.la needed by the tests) -SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph tgba \ +SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph twa \ tgbaalgos ta taalgos kripke kripkeparse dstarparse hoaparse \ . bin ltltest graphtest tgbatest kripketest sanity @@ -46,7 +46,7 @@ libspot_la_LIBADD = \ taalgos/libtaalgos.la \ ta/libta.la \ tgbaalgos/libtgbaalgos.la \ - tgba/libtgba.la \ + twa/libtwa.la \ ../lib/libgnu.la # Dummy C++ source to cause C++ linking. diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 3c072f72c..fb51f4486 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -25,7 +25,7 @@ #include "common_cout.hh" #include "common_post.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" diff --git a/src/bin/common_conv.hh b/src/bin/common_conv.hh index 1abf61b36..daf1e6139 100644 --- a/src/bin/common_conv.hh +++ b/src/bin/common_conv.hh @@ -20,7 +20,7 @@ #pragma once #include "common_sys.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" int to_int(const char* s); int to_pos_int(const char* s); diff --git a/src/bin/common_trans.hh b/src/bin/common_trans.hh index cd18f8425..598e7cf09 100644 --- a/src/bin/common_trans.hh +++ b/src/bin/common_trans.hh @@ -25,7 +25,7 @@ #include "misc/formater.hh" #include "misc/tmpfile.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" extern const struct argp trans_argp; diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 230d7e6d3..656f2151c 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -37,7 +37,7 @@ #include "tgbaalgos/hoa.hh" #include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/stats.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "misc/optionmap.hh" #include "misc/timer.hh" #include "dstarparse/public.hh" diff --git a/src/bin/ltl2tgta.cc b/src/bin/ltl2tgta.cc index b422d6a97..f3fc52903 100644 --- a/src/bin/ltl2tgta.cc +++ b/src/bin/ltl2tgta.cc @@ -38,7 +38,7 @@ #include "tgbaalgos/dotty.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/translate.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "taalgos/tgba2ta.hh" #include "taalgos/dotty.hh" diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index ee788da20..a1847c3f7 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -38,7 +38,7 @@ #include "misc/timer.hh" #include "misc/random.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "tgbaalgos/randomgraph.hh" #include "tgbaalgos/canonicalize.hh" diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc index 616c12ef4..56987f237 100644 --- a/src/dstarparse/dra2ba.cc +++ b/src/dstarparse/dra2ba.cc @@ -18,7 +18,7 @@ // along with this program. If not, see . #include "public.hh" -#include "tgba/tgbamask.hh" +#include "twa/twamask.hh" #include "tgbaalgos/scc.hh" #include "tgbaalgos/reachiter.hh" #include "tgbaalgos/gtec/gtec.hh" diff --git a/src/dstarparse/public.hh b/src/dstarparse/public.hh index 4e461f896..69c2c554b 100644 --- a/src/dstarparse/public.hh +++ b/src/dstarparse/public.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include "misc/location.hh" #include "ltlenv/defaultenv.hh" #include diff --git a/src/graphtest/Makefile.am b/src/graphtest/Makefile.am index eb33d9f88..1758a2a19 100644 --- a/src/graphtest/Makefile.am +++ b/src/graphtest/Makefile.am @@ -26,7 +26,7 @@ noinst_PROGRAMS = graph ngraph tgbagraph graph_SOURCES = graph.cc ngraph_SOURCES = ngraph.cc -tgbagraph_SOURCES = tgbagraph.cc +tgbagraph_SOURCES = twagraph.cc TESTS = graph.test ngraph.test tgbagraph.test diff --git a/src/graphtest/ngraph.cc b/src/graphtest/ngraph.cc index d208966fd..e1fd7da32 100644 --- a/src/graphtest/ngraph.cc +++ b/src/graphtest/ngraph.cc @@ -20,7 +20,7 @@ #include #include "graph/ngraph.hh" -#include "tgba/tgba.hh" +#include "twa/twa.hh" template void diff --git a/src/graphtest/tgbagraph.cc b/src/graphtest/twagraph.cc similarity index 98% rename from src/graphtest/tgbagraph.cc rename to src/graphtest/twagraph.cc index a65465491..55cc225e6 100644 --- a/src/graphtest/tgbagraph.cc +++ b/src/graphtest/twagraph.cc @@ -19,7 +19,7 @@ #include -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include "tgbaalgos/dotty.hh" #include "ltlenv/defaultenv.hh" diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index 9ee323967..0ca0d6116 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -35,7 +35,7 @@ #include #include #include "ltlast/constant.hh" -#include "tgba/formula2bdd.hh" +#include "twa/formula2bdd.hh" #include "public.hh" #include "priv/accmap.hh" #include "ltlparse/public.hh" diff --git a/src/hoaparse/public.hh b/src/hoaparse/public.hh index 4029ce516..1c7cbba98 100644 --- a/src/hoaparse/public.hh +++ b/src/hoaparse/public.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include "misc/location.hh" #include "ltlenv/defaultenv.hh" #include diff --git a/src/kripke/fairkripke.hh b/src/kripke/fairkripke.hh index 9ef7587c3..6a648a74b 100644 --- a/src/kripke/fairkripke.hh +++ b/src/kripke/fairkripke.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "fwd.hh" /// \addtogroup kripke Kripke Structures diff --git a/src/kripke/kripkeexplicit.cc b/src/kripke/kripkeexplicit.cc index 9d7a4f86c..6f0f3f72c 100644 --- a/src/kripke/kripkeexplicit.cc +++ b/src/kripke/kripkeexplicit.cc @@ -19,8 +19,8 @@ #include "kripkeexplicit.hh" -#include "tgba/bddprint.hh" -#include "tgba/formula2bdd.hh" +#include "twa/bddprint.hh" +#include "twa/formula2bdd.hh" #include namespace spot diff --git a/src/kripke/kripkeprint.cc b/src/kripke/kripkeprint.cc index 2a50ac130..613ba354d 100644 --- a/src/kripke/kripkeprint.cc +++ b/src/kripke/kripkeprint.cc @@ -20,7 +20,7 @@ #include "kripkeprint.hh" #include "kripkeexplicit.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "misc/escape.hh" #include "tgbaalgos/reachiter.hh" #include diff --git a/src/kripkeparse/kripkeparse.yy b/src/kripkeparse/kripkeparse.yy index 4d9eed10c..a2b8bdd1e 100644 --- a/src/kripkeparse/kripkeparse.yy +++ b/src/kripkeparse/kripkeparse.yy @@ -58,7 +58,7 @@ typedef std::map formula_cache; #include "ltlparse/public.hh" #include -/* tgbaparse.hh and parsedecl.hh include each other recursively. +/* twaparse.hh and parsedecl.hh include each other recursively. We must ensure that YYSTYPE is declared (by the above %union) before parsedecl.hh uses it. */ #include "parsedecl.hh" diff --git a/src/ltlvisit/apcollect.cc b/src/ltlvisit/apcollect.cc index 44567766a..ca6286d6a 100644 --- a/src/ltlvisit/apcollect.cc +++ b/src/ltlvisit/apcollect.cc @@ -22,8 +22,8 @@ #include "apcollect.hh" #include "ltlvisit/postfix.hh" -#include "tgba/tgba.hh" -#include "tgba/bdddict.hh" +#include "twa/twa.hh" +#include "twa/bdddict.hh" namespace spot { diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh index ab5a461cd..ed92714be 100644 --- a/src/ltlvisit/apcollect.hh +++ b/src/ltlvisit/apcollect.hh @@ -25,7 +25,7 @@ #include "ltlast/atomic_prop.hh" #include #include -#include "tgba/fwd.hh" +#include "twa/fwd.hh" namespace spot { diff --git a/src/ltlvisit/exclusive.hh b/src/ltlvisit/exclusive.hh index 3aa94bfd5..31c2bd4bf 100644 --- a/src/ltlvisit/exclusive.hh +++ b/src/ltlvisit/exclusive.hh @@ -22,7 +22,7 @@ #include #include "ltlast/atomic_prop.hh" #include "ltlast/formula.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 16f228c10..e2b0d8e2f 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -32,7 +32,7 @@ #include "ltlvisit/contain.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/snf.hh" -#include "tgba/formula2bdd.hh" +#include "twa/formula2bdd.hh" #include namespace spot diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh index 5fe451f35..a8a7a38aa 100644 --- a/src/ltlvisit/simplify.hh +++ b/src/ltlvisit/simplify.hh @@ -21,7 +21,7 @@ #include "ltlast/formula.hh" #include -#include "tgba/bdddict.hh" +#include "twa/bdddict.hh" #include namespace spot diff --git a/src/priv/accmap.hh b/src/priv/accmap.hh index 4962fef53..d7da5b3fa 100644 --- a/src/priv/accmap.hh +++ b/src/priv/accmap.hh @@ -22,7 +22,7 @@ #include #include "misc/hash.hh" #include "ltlast/formula.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/ta/ta.hh b/src/ta/ta.hh index 30724d356..89aa662ab 100644 --- a/src/ta/ta.hh +++ b/src/ta/ta.hh @@ -23,7 +23,7 @@ #include #include "misc/bddlt.hh" -#include "tgba/tgba.hh" +#include "twa/twa.hh" namespace spot { diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index 271ee0417..ebd168c78 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -29,11 +29,11 @@ #include "ltlast/atomic_prop.hh" #include "ltlast/constant.hh" #include "taexplicit.hh" -#include "tgba/formula2bdd.hh" +#include "twa/formula2bdd.hh" #include #include "ltlvisit/tostring.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" namespace spot { diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh index 7b6da1d47..88aa1704a 100644 --- a/src/ta/taexplicit.hh +++ b/src/ta/taexplicit.hh @@ -21,7 +21,7 @@ #include "misc/hash.hh" #include -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include #include "ltlast/formula.hh" #include diff --git a/src/ta/tgta.hh b/src/ta/tgta.hh index c12e31861..06a6342d6 100644 --- a/src/ta/tgta.hh +++ b/src/ta/tgta.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgba.hh" +#include "twa/twa.hh" namespace spot { diff --git a/src/ta/tgtaexplicit.cc b/src/ta/tgtaexplicit.cc index 26c2f229d..6abb74035 100644 --- a/src/ta/tgtaexplicit.cc +++ b/src/ta/tgtaexplicit.cc @@ -20,10 +20,10 @@ #include "ltlast/atomic_prop.hh" #include "ltlast/constant.hh" #include "tgtaexplicit.hh" -#include "tgba/formula2bdd.hh" +#include "twa/formula2bdd.hh" #include "ltlvisit/tostring.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" namespace spot { diff --git a/src/ta/tgtaexplicit.hh b/src/ta/tgtaexplicit.hh index cfe6e1789..89b90f82a 100644 --- a/src/ta/tgtaexplicit.hh +++ b/src/ta/tgtaexplicit.hh @@ -21,7 +21,7 @@ #include "misc/hash.hh" #include -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include #include "ltlast/formula.hh" #include diff --git a/src/ta/tgtaproduct.hh b/src/ta/tgtaproduct.hh index 177dbc601..ca6ed5a63 100644 --- a/src/ta/tgtaproduct.hh +++ b/src/ta/tgtaproduct.hh @@ -19,8 +19,8 @@ #pragma once -#include "tgba/tgba.hh" -#include "tgba/tgbaproduct.hh" +#include "twa/twa.hh" +#include "twa/twaproduct.hh" #include "misc/fixpool.hh" #include "kripke/kripke.hh" #include "tgta.hh" diff --git a/src/taalgos/dotty.cc b/src/taalgos/dotty.cc index 5b58866c9..f5c5c8ccc 100644 --- a/src/taalgos/dotty.cc +++ b/src/taalgos/dotty.cc @@ -19,7 +19,7 @@ #include #include "dotty.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "reachiter.hh" #include "misc/escape.hh" #include "misc/bareword.hh" diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index 10afe8e98..98fef72ff 100644 --- a/src/taalgos/emptinessta.cc +++ b/src/taalgos/emptinessta.cc @@ -29,7 +29,7 @@ #include "emptinessta.hh" #include "misc/memusage.hh" #include -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" namespace spot { diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index 74a81b5f3..7b42a7d73 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -35,8 +35,8 @@ #include "misc/bddlt.hh" #include "ta/tgtaexplicit.hh" #include "taalgos/statessetbuilder.hh" -#include "tgba/tgbagraph.hh" -#include "tgba/bddprint.hh" +#include "twa/twagraph.hh" +#include "twa/bddprint.hh" namespace spot { diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index e5863df44..870ecb4e8 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -28,11 +28,11 @@ #include "ltlast/atomic_prop.hh" #include "ltlast/constant.hh" -#include "tgba/formula2bdd.hh" +#include "twa/formula2bdd.hh" #include #include "ltlvisit/tostring.hh" #include -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include #include "tgba2ta.hh" #include "taalgos/statessetbuilder.hh" @@ -454,15 +454,15 @@ namespace spot state_ta_explicit* source = todo.top(); todo.pop(); - twa_succ_iterator* tgba_succ_it = + twa_succ_iterator* twa_succ_it = tgba_->succ_iter(source->get_tgba_state()); - for (tgba_succ_it->first(); !tgba_succ_it->done(); - tgba_succ_it->next()) + for (twa_succ_it->first(); !twa_succ_it->done(); + twa_succ_it->next()) { - const state* tgba_state = tgba_succ_it->current_state(); - bdd tgba_condition = tgba_succ_it->current_condition(); + const state* tgba_state = twa_succ_it->current_state(); + bdd tgba_condition = twa_succ_it->current_condition(); acc_cond::mark_t tgba_acceptance_conditions = - tgba_succ_it->current_acceptance_conditions(); + twa_succ_it->current_acceptance_conditions(); bdd satone_tgba_condition; while ((satone_tgba_condition = bdd_satoneset(tgba_condition, @@ -515,7 +515,7 @@ namespace spot } tgba_state->destroy(); } - delete tgba_succ_it; + delete twa_succ_it; } if (no_livelock) diff --git a/src/taalgos/tgba2ta.hh b/src/taalgos/tgba2ta.hh index fc231d987..5e66a0ea7 100644 --- a/src/taalgos/tgba2ta.hh +++ b/src/taalgos/tgba2ta.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "ta/taexplicit.hh" #include "ta/tgtaexplicit.hh" diff --git a/src/tgbaalgos/are_isomorphic.cc b/src/tgbaalgos/are_isomorphic.cc index db391ec1f..2caa3265a 100644 --- a/src/tgbaalgos/are_isomorphic.cc +++ b/src/tgbaalgos/are_isomorphic.cc @@ -20,7 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include "tgbaalgos/are_isomorphic.hh" #include "tgbaalgos/canonicalize.hh" #include "tgbaalgos/isdet.hh" diff --git a/src/tgbaalgos/are_isomorphic.hh b/src/tgbaalgos/are_isomorphic.hh index 0c2845dc2..c71445191 100644 --- a/src/tgbaalgos/are_isomorphic.hh +++ b/src/tgbaalgos/are_isomorphic.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include namespace spot diff --git a/src/tgbaalgos/bfssteps.cc b/src/tgbaalgos/bfssteps.cc index 282457772..1d801dff6 100644 --- a/src/tgbaalgos/bfssteps.cc +++ b/src/tgbaalgos/bfssteps.cc @@ -22,7 +22,7 @@ #include #include -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "bfssteps.hh" namespace spot diff --git a/src/tgbaalgos/canonicalize.cc b/src/tgbaalgos/canonicalize.cc index a535c038c..b61f44196 100644 --- a/src/tgbaalgos/canonicalize.cc +++ b/src/tgbaalgos/canonicalize.cc @@ -18,7 +18,7 @@ // along with this program. If not, see . #include "canonicalize.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include #include diff --git a/src/tgbaalgos/canonicalize.hh b/src/tgbaalgos/canonicalize.hh index fbb80a0d3..e240174e1 100644 --- a/src/tgbaalgos/canonicalize.hh +++ b/src/tgbaalgos/canonicalize.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/cleanacc.hh b/src/tgbaalgos/cleanacc.hh index bf76f7e2c..04178cc63 100644 --- a/src/tgbaalgos/cleanacc.hh +++ b/src/tgbaalgos/cleanacc.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/complete.hh b/src/tgbaalgos/complete.hh index 089ac9ab2..05c6158fa 100644 --- a/src/tgbaalgos/complete.hh +++ b/src/tgbaalgos/complete.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/compsusp.cc b/src/tgbaalgos/compsusp.cc index 4c412bbf9..fb115cb23 100644 --- a/src/tgbaalgos/compsusp.cc +++ b/src/tgbaalgos/compsusp.cc @@ -20,7 +20,7 @@ #include "compsusp.hh" #include "sccfilter.hh" #include "sccinfo.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include "ltl2tgba_fm.hh" #include "minimize.hh" #include "simulation.hh" diff --git a/src/tgbaalgos/compsusp.hh b/src/tgbaalgos/compsusp.hh index eb3fcd42e..c6d21329b 100644 --- a/src/tgbaalgos/compsusp.hh +++ b/src/tgbaalgos/compsusp.hh @@ -20,7 +20,7 @@ #pragma once #include "ltlast/formula.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index ad75f091e..b13eeadec 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -19,7 +19,7 @@ #include "degen.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include "misc/hash.hh" #include "misc/hashfunc.hh" #include @@ -27,7 +27,7 @@ #include #include #include "tgbaalgos/sccinfo.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" //#define DEGEN_DEBUG diff --git a/src/tgbaalgos/degen.hh b/src/tgbaalgos/degen.hh index 58f6f0c68..772b6c386 100644 --- a/src/tgbaalgos/degen.hh +++ b/src/tgbaalgos/degen.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 55622292e..069676540 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -22,13 +22,13 @@ #include #include -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include "dotty.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "reachiter.hh" #include "misc/escape.hh" -#include "tgba/tgbagraph.hh" -#include "tgba/formula2bdd.hh" +#include "twa/twagraph.hh" +#include "twa/formula2bdd.hh" #include "tgbaalgos/sccinfo.hh" #include #include diff --git a/src/tgbaalgos/dotty.hh b/src/tgbaalgos/dotty.hh index b14948a28..c62cdea96 100644 --- a/src/tgbaalgos/dotty.hh +++ b/src/tgbaalgos/dotty.hh @@ -23,7 +23,7 @@ #pragma once #include -#include +#include #include "misc/common.hh" namespace spot diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index 1fec0dc8a..3f15ded67 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -25,7 +25,7 @@ #include #include #include "sccinfo.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "stats.hh" #include "misc/satsolver.hh" #include "misc/timer.hh" diff --git a/src/tgbaalgos/dtbasat.hh b/src/tgbaalgos/dtbasat.hh index b6a09d159..f13309cda 100644 --- a/src/tgbaalgos/dtbasat.hh +++ b/src/tgbaalgos/dtbasat.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/dtgbacomp.hh b/src/tgbaalgos/dtgbacomp.hh index 412075524..ed3f05cda 100644 --- a/src/tgbaalgos/dtgbacomp.hh +++ b/src/tgbaalgos/dtgbacomp.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index 499c12df5..36803a98d 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -25,7 +25,7 @@ #include #include #include "sccinfo.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "ltlast/constant.hh" #include "stats.hh" #include "ltlenv/defaultenv.hh" diff --git a/src/tgbaalgos/dtgbasat.hh b/src/tgbaalgos/dtgbasat.hh index ad4a64283..b0ce7a2d5 100644 --- a/src/tgbaalgos/dtgbasat.hh +++ b/src/tgbaalgos/dtgbasat.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc index 9c5dbf9d9..b4c6867c6 100644 --- a/src/tgbaalgos/dupexp.cc +++ b/src/tgbaalgos/dupexp.cc @@ -21,7 +21,7 @@ // along with this program. If not, see . #include "dupexp.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include #include #include diff --git a/src/tgbaalgos/dupexp.hh b/src/tgbaalgos/dupexp.hh index b12a1977b..ba5f5c5a6 100644 --- a/src/tgbaalgos/dupexp.hh +++ b/src/tgbaalgos/dupexp.hh @@ -23,8 +23,8 @@ #pragma once #include "misc/common.hh" -#include "tgba/fwd.hh" -#include "tgba/tgba.hh" +#include "twa/fwd.hh" +#include "twa/twa.hh" #include namespace spot diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc index f6d7b0bcc..776149b97 100644 --- a/src/tgbaalgos/emptiness.cc +++ b/src/tgbaalgos/emptiness.cc @@ -22,8 +22,8 @@ #include #include "emptiness.hh" -#include "tgba/tgba.hh" -#include "tgba/bddprint.hh" +#include "twa/twa.hh" +#include "twa/bddprint.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/gv04.hh" #include "tgbaalgos/magic.hh" diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index 3254f8342..97d4c27dc 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -27,7 +27,7 @@ #include #include #include "misc/optionmap.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include "emptiness_stats.hh" namespace spot diff --git a/src/tgbaalgos/gtec/sccstack.hh b/src/tgbaalgos/gtec/sccstack.hh index 1683c6a8d..c6c8e03b7 100644 --- a/src/tgbaalgos/gtec/sccstack.hh +++ b/src/tgbaalgos/gtec/sccstack.hh @@ -24,7 +24,7 @@ #include #include -#include "tgba/tgba.hh" +#include "twa/twa.hh" namespace spot { diff --git a/src/tgbaalgos/gtec/status.hh b/src/tgbaalgos/gtec/status.hh index 4e277083c..d7db86a78 100644 --- a/src/tgbaalgos/gtec/status.hh +++ b/src/tgbaalgos/gtec/status.hh @@ -23,7 +23,7 @@ #pragma once #include "sccstack.hh" -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include namespace spot diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index f0a47374d..b16f0d037 100644 --- a/src/tgbaalgos/gv04.cc +++ b/src/tgbaalgos/gv04.cc @@ -32,7 +32,7 @@ #include #include #include -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "misc/hash.hh" #include "emptiness.hh" #include "emptiness_stats.hh" diff --git a/src/tgbaalgos/gv04.hh b/src/tgbaalgos/gv04.hh index 054309f30..73c423070 100644 --- a/src/tgbaalgos/gv04.hh +++ b/src/tgbaalgos/gv04.hh @@ -23,7 +23,7 @@ #pragma once #include "misc/optionmap.hh" -#include "tgba/fwd.hh" +#include "twa/fwd.hh" #include "emptiness.hh" namespace spot diff --git a/src/tgbaalgos/hoa.cc b/src/tgbaalgos/hoa.cc index 09f3ba51e..5da1cd088 100644 --- a/src/tgbaalgos/hoa.cc +++ b/src/tgbaalgos/hoa.cc @@ -24,14 +24,14 @@ #include #include #include -#include "tgba/tgba.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twa.hh" +#include "twa/twagraph.hh" #include "hoa.hh" #include "reachiter.hh" #include "misc/escape.hh" #include "misc/bddlt.hh" #include "misc/minato.hh" -#include "tgba/formula2bdd.hh" +#include "twa/formula2bdd.hh" #include "ltlast/atomic_prop.hh" namespace spot diff --git a/src/tgbaalgos/hoa.hh b/src/tgbaalgos/hoa.hh index a75a2d413..94f7517a0 100644 --- a/src/tgbaalgos/hoa.hh +++ b/src/tgbaalgos/hoa.hh @@ -21,7 +21,7 @@ #include #include "misc/common.hh" -#include "tgba/fwd.hh" +#include "twa/fwd.hh" namespace spot { diff --git a/src/tgbaalgos/isdet.hh b/src/tgbaalgos/isdet.hh index b062d09d9..377ec768d 100644 --- a/src/tgbaalgos/isdet.hh +++ b/src/tgbaalgos/isdet.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 19f68abc1..1cfac8b91 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -24,7 +24,7 @@ #include #include #include -#include "tgba/formula2bdd.hh" +#include "twa/formula2bdd.hh" #include "reachiter.hh" #include "misc/bddlt.hh" #include "priv/accmap.hh" diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh index 4262c5f6f..5a267e3fa 100644 --- a/src/tgbaalgos/lbtt.hh +++ b/src/tgbaalgos/lbtt.hh @@ -22,7 +22,7 @@ #pragma once -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include namespace spot diff --git a/src/tgbaalgos/ltl2taa.hh b/src/tgbaalgos/ltl2taa.hh index 4f1a64f1b..b501bf440 100644 --- a/src/tgbaalgos/ltl2taa.hh +++ b/src/tgbaalgos/ltl2taa.hh @@ -20,7 +20,7 @@ #pragma once #include "ltlast/formula.hh" -#include "tgba/taatgba.hh" +#include "twa/taatgba.hh" namespace spot { diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 7f001ca6d..1c0a2aed7 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -36,7 +36,7 @@ #include #include #include "ltl2tgba_fm.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "tgbaalgos/sccinfo.hh" //#include "tgbaalgos/dotty.hh" diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index ddf0a0019..c0342838a 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -23,7 +23,7 @@ #pragma once #include "ltlast/formula.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include "ltlvisit/apcollect.hh" #include "ltlvisit/simplify.hh" diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index c732ae2e9..5d6555b4a 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -32,7 +32,7 @@ #include #include #include "misc/hash.hh" -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "emptiness.hh" #include "emptiness_stats.hh" #include "magic.hh" diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh index 616e98ec0..1ec3eb86b 100644 --- a/src/tgbaalgos/magic.hh +++ b/src/tgbaalgos/magic.hh @@ -23,7 +23,7 @@ #pragma once #include -#include "tgba/fwd.hh" +#include "twa/fwd.hh" #include "misc/optionmap.hh" #include "emptiness.hh" diff --git a/src/tgbaalgos/mask.hh b/src/tgbaalgos/mask.hh index aff67953f..a4f444f8a 100644 --- a/src/tgbaalgos/mask.hh +++ b/src/tgbaalgos/mask.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/minimize.hh b/src/tgbaalgos/minimize.hh index f3c30bd6e..8eaf6ee86 100644 --- a/src/tgbaalgos/minimize.hh +++ b/src/tgbaalgos/minimize.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include "ltlast/formula.hh" namespace spot diff --git a/src/tgbaalgos/ndfs_result.hxx b/src/tgbaalgos/ndfs_result.hxx index 153dbfaa2..315f398e0 100644 --- a/src/tgbaalgos/ndfs_result.hxx +++ b/src/tgbaalgos/ndfs_result.hxx @@ -34,7 +34,7 @@ #include #include #include "misc/hash.hh" -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "emptiness.hh" #include "emptiness_stats.hh" #include "bfssteps.hh" diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 48fd50825..b3231a63a 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -23,11 +23,11 @@ #include #include #include "neverclaim.hh" -#include "tgba/bddprint.hh" -#include "tgba/tgbagraph.hh" +#include "twa/bddprint.hh" +#include "twa/twagraph.hh" #include "reachiter.hh" #include "ltlvisit/tostring.hh" -#include "tgba/formula2bdd.hh" +#include "twa/formula2bdd.hh" namespace spot { diff --git a/src/tgbaalgos/neverclaim.hh b/src/tgbaalgos/neverclaim.hh index 10c44b7bd..24f5b43c2 100644 --- a/src/tgbaalgos/neverclaim.hh +++ b/src/tgbaalgos/neverclaim.hh @@ -23,7 +23,7 @@ #pragma once #include -#include "tgba/fwd.hh" +#include "twa/fwd.hh" #include "misc/common.hh" namespace spot diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh index 45e483ddf..80d70ccbf 100644 --- a/src/tgbaalgos/postproc.hh +++ b/src/tgbaalgos/postproc.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 97569e856..75a55b247 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -30,7 +30,7 @@ #include "tgbaalgos/cycles.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/product.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/ltl2tgba_fm.hh" diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index fa14cd782..e00fccf16 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -24,7 +24,7 @@ #include #include -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/product.cc b/src/tgbaalgos/product.cc index 51568a42d..d21d91f24 100644 --- a/src/tgbaalgos/product.cc +++ b/src/tgbaalgos/product.cc @@ -18,7 +18,7 @@ // along with this program. If not, see . #include "product.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include #include #include "misc/hash.hh" diff --git a/src/tgbaalgos/product.hh b/src/tgbaalgos/product.hh index fad190baf..f7e98a4fa 100644 --- a/src/tgbaalgos/product.hh +++ b/src/tgbaalgos/product.hh @@ -20,7 +20,7 @@ #pragma once #include "misc/common.hh" -#include "tgba/fwd.hh" +#include "twa/fwd.hh" #include #include diff --git a/src/tgbaalgos/projrun.cc b/src/tgbaalgos/projrun.cc index 7bfa8aedd..16b0d69b6 100644 --- a/src/tgbaalgos/projrun.cc +++ b/src/tgbaalgos/projrun.cc @@ -21,7 +21,7 @@ // along with this program. If not, see . #include "projrun.hh" -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "tgbaalgos/emptiness.hh" namespace spot diff --git a/src/tgbaalgos/projrun.hh b/src/tgbaalgos/projrun.hh index 7cc422f28..5f2258554 100644 --- a/src/tgbaalgos/projrun.hh +++ b/src/tgbaalgos/projrun.hh @@ -24,7 +24,7 @@ #include "misc/common.hh" #include -#include "tgba/fwd.hh" +#include "twa/fwd.hh" #include "tgbaalgos/emptiness.hh" namespace spot diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index 7d0eaa03f..8538533f0 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -21,7 +21,7 @@ // along with this program. If not, see . #include "randomgraph.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" #include "misc/random.hh" #include "misc/bddlt.hh" #include "ltlast/atomic_prop.hh" diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh index 78abd8265..8b2768f8b 100644 --- a/src/tgbaalgos/randomgraph.hh +++ b/src/tgbaalgos/randomgraph.hh @@ -24,8 +24,8 @@ #include "ltlvisit/apcollect.hh" #include "ltlenv/defaultenv.hh" -#include "tgba/bdddict.hh" -#include "tgba/acc.hh" +#include "twa/bdddict.hh" +#include "twa/acc.hh" namespace spot { diff --git a/src/tgbaalgos/randomize.hh b/src/tgbaalgos/randomize.hh index 373ff7dd9..548b218d3 100644 --- a/src/tgbaalgos/randomize.hh +++ b/src/tgbaalgos/randomize.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/reachiter.hh b/src/tgbaalgos/reachiter.hh index 3054ec1cb..f8883c05a 100644 --- a/src/tgbaalgos/reachiter.hh +++ b/src/tgbaalgos/reachiter.hh @@ -23,7 +23,7 @@ #pragma once #include "misc/hash.hh" -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include #include diff --git a/src/tgbaalgos/reducerun.cc b/src/tgbaalgos/reducerun.cc index 9f3f6e6af..13d7e4f41 100644 --- a/src/tgbaalgos/reducerun.cc +++ b/src/tgbaalgos/reducerun.cc @@ -22,7 +22,7 @@ #include "misc/hash.hh" #include "emptiness.hh" -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "bfssteps.hh" #include "reducerun.hh" diff --git a/src/tgbaalgos/reducerun.hh b/src/tgbaalgos/reducerun.hh index c6b862a10..a011f4a96 100644 --- a/src/tgbaalgos/reducerun.hh +++ b/src/tgbaalgos/reducerun.hh @@ -23,7 +23,7 @@ #pragma once #include "misc/common.hh" -#include "tgba/fwd.hh" +#include "twa/fwd.hh" #include "tgbaalgos/emptiness.hh" namespace spot diff --git a/src/tgbaalgos/relabel.hh b/src/tgbaalgos/relabel.hh index 591afa5e2..45c1df9e9 100644 --- a/src/tgbaalgos/relabel.hh +++ b/src/tgbaalgos/relabel.hh @@ -20,7 +20,7 @@ #pragma once #include "ltlvisit/relabel.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/remfin.hh b/src/tgbaalgos/remfin.hh index e478a6706..f219f1375 100644 --- a/src/tgbaalgos/remfin.hh +++ b/src/tgbaalgos/remfin.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/remprop.hh b/src/tgbaalgos/remprop.hh index 8fe078b84..d450801bf 100644 --- a/src/tgbaalgos/remprop.hh +++ b/src/tgbaalgos/remprop.hh @@ -21,7 +21,7 @@ #include #include "ltlast/atomic_prop.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/replayrun.cc b/src/tgbaalgos/replayrun.cc index 53ab96e8e..acd4b43f1 100644 --- a/src/tgbaalgos/replayrun.cc +++ b/src/tgbaalgos/replayrun.cc @@ -22,9 +22,9 @@ #include "misc/hash.hh" #include "replayrun.hh" -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "emptiness.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include namespace spot diff --git a/src/tgbaalgos/replayrun.hh b/src/tgbaalgos/replayrun.hh index 018595276..995e711be 100644 --- a/src/tgbaalgos/replayrun.hh +++ b/src/tgbaalgos/replayrun.hh @@ -24,7 +24,7 @@ #include "misc/common.hh" #include -#include "tgba/fwd.hh" +#include "twa/fwd.hh" #include "tgbaalgos/emptiness.hh" namespace spot diff --git a/src/tgbaalgos/sbacc.hh b/src/tgbaalgos/sbacc.hh index 2290d1222..bb9a0d112 100644 --- a/src/tgbaalgos/sbacc.hh +++ b/src/tgbaalgos/sbacc.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 56b11c2a7..0c72accf2 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -22,7 +22,7 @@ #include #include #include "scc.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "misc/escape.hh" namespace spot diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index 368a33fe3..b09158566 100644 --- a/src/tgbaalgos/scc.hh +++ b/src/tgbaalgos/scc.hh @@ -22,7 +22,7 @@ #include #include #include -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include #include "misc/hash.hh" #include "misc/bddlt.hh" diff --git a/src/tgbaalgos/sccfilter.hh b/src/tgbaalgos/sccfilter.hh index d03894f3a..b47d5d13e 100644 --- a/src/tgbaalgos/sccfilter.hh +++ b/src/tgbaalgos/sccfilter.hh @@ -21,7 +21,7 @@ #include "misc/common.hh" #include -#include "tgba/fwd.hh" +#include "twa/fwd.hh" namespace spot { diff --git a/src/tgbaalgos/sccinfo.cc b/src/tgbaalgos/sccinfo.cc index 1f4dcd6de..fe68e57de 100644 --- a/src/tgbaalgos/sccinfo.cc +++ b/src/tgbaalgos/sccinfo.cc @@ -21,7 +21,7 @@ #include #include #include -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "misc/escape.hh" namespace spot diff --git a/src/tgbaalgos/sccinfo.hh b/src/tgbaalgos/sccinfo.hh index 0222c6ce4..835a75f16 100644 --- a/src/tgbaalgos/sccinfo.hh +++ b/src/tgbaalgos/sccinfo.hh @@ -20,7 +20,7 @@ #pragma once #include -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index 07e90a918..9659c2e60 100644 --- a/src/tgbaalgos/se05.cc +++ b/src/tgbaalgos/se05.cc @@ -32,7 +32,7 @@ #include #include #include "misc/hash.hh" -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "emptiness.hh" #include "emptiness_stats.hh" #include "se05.hh" diff --git a/src/tgbaalgos/se05.hh b/src/tgbaalgos/se05.hh index 90e3e15b9..cd1a45a3b 100644 --- a/src/tgbaalgos/se05.hh +++ b/src/tgbaalgos/se05.hh @@ -24,7 +24,7 @@ #include #include "misc/optionmap.hh" -#include "tgba/fwd.hh" +#include "twa/fwd.hh" #include "emptiness.hh" namespace spot diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 7569fc2c5..c9ffe41af 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -24,7 +24,7 @@ #include #include "simulation.hh" #include "misc/minato.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "tgbaalgos/reachiter.hh" #include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/sccinfo.hh" diff --git a/src/tgbaalgos/simulation.hh b/src/tgbaalgos/simulation.hh index b716e15d9..6480e302f 100644 --- a/src/tgbaalgos/simulation.hh +++ b/src/tgbaalgos/simulation.hh @@ -20,7 +20,7 @@ #pragma once #include "misc/common.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index ea14d3549..48fa71a50 100644 --- a/src/tgbaalgos/stats.cc +++ b/src/tgbaalgos/stats.cc @@ -22,7 +22,7 @@ #include #include -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "stats.hh" #include "reachiter.hh" #include "ltlvisit/tostring.hh" diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh index b7a8079c6..bc7912306 100644 --- a/src/tgbaalgos/stats.hh +++ b/src/tgbaalgos/stats.hh @@ -22,7 +22,7 @@ #pragma once -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include #include "misc/formater.hh" diff --git a/src/tgbaalgos/stripacc.hh b/src/tgbaalgos/stripacc.hh index 17714eef2..c8b2e5b68 100644 --- a/src/tgbaalgos/stripacc.hh +++ b/src/tgbaalgos/stripacc.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/stutter.cc b/src/tgbaalgos/stutter.cc index dcccd3c03..2c9ab6ee3 100644 --- a/src/tgbaalgos/stutter.cc +++ b/src/tgbaalgos/stutter.cc @@ -18,7 +18,7 @@ // along with this program. If not, see . #include "stutter.hh" -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "dupexp.hh" #include "misc/hash.hh" #include "misc/hashfunc.hh" @@ -29,8 +29,8 @@ #include "ltlvisit/remove_x.hh" #include "tgbaalgos/product.hh" #include "tgbaalgos/ltl2tgba_fm.hh" -#include "tgba/tgbaproduct.hh" -#include "tgba/bddprint.hh" +#include "twa/twaproduct.hh" +#include "twa/bddprint.hh" #include #include #include @@ -94,17 +94,17 @@ namespace spot bdd cond_; }; - class tgbasl_succ_iterator : public twa_succ_iterator + class twasl_succ_iterator : public twa_succ_iterator { public: - tgbasl_succ_iterator(twa_succ_iterator* it, const state_tgbasl* state, + twasl_succ_iterator(twa_succ_iterator* it, const state_tgbasl* state, bdd_dict_ptr d, bdd atomic_propositions) : it_(it), state_(state), aps_(atomic_propositions), d_(d) { } virtual - ~tgbasl_succ_iterator() + ~twasl_succ_iterator() { delete it_; } @@ -229,7 +229,7 @@ namespace spot { const state_tgbasl* s = down_cast(state); assert(s); - return new tgbasl_succ_iterator(a_->succ_iter(s->real_state()), s, + return new twasl_succ_iterator(a_->succ_iter(s->real_state()), s, a_->get_dict(), aps_); } diff --git a/src/tgbaalgos/stutter.hh b/src/tgbaalgos/stutter.hh index 7bc5fe27d..6c20dff84 100644 --- a/src/tgbaalgos/stutter.hh +++ b/src/tgbaalgos/stutter.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/tau03.cc b/src/tgbaalgos/tau03.cc index 593720355..d499d2227 100644 --- a/src/tgbaalgos/tau03.cc +++ b/src/tgbaalgos/tau03.cc @@ -35,7 +35,7 @@ #include #include #include "misc/hash.hh" -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "emptiness.hh" #include "emptiness_stats.hh" #include "tau03.hh" diff --git a/src/tgbaalgos/tau03.hh b/src/tgbaalgos/tau03.hh index dcb8f9396..8e2cc443d 100644 --- a/src/tgbaalgos/tau03.hh +++ b/src/tgbaalgos/tau03.hh @@ -23,7 +23,7 @@ #pragma once #include "misc/optionmap.hh" -#include "tgba/fwd.hh" +#include "twa/fwd.hh" #include "emptiness.hh" namespace spot diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc index 58d14cbea..a6187e11e 100644 --- a/src/tgbaalgos/tau03opt.cc +++ b/src/tgbaalgos/tau03opt.cc @@ -45,7 +45,7 @@ #include #include #include "misc/hash.hh" -#include "tgba/tgba.hh" +#include "twa/twa.hh" #include "emptiness.hh" #include "emptiness_stats.hh" #include "tau03opt.hh" diff --git a/src/tgbaalgos/tau03opt.hh b/src/tgbaalgos/tau03opt.hh index 77c3300ed..491c2767e 100644 --- a/src/tgbaalgos/tau03opt.hh +++ b/src/tgbaalgos/tau03opt.hh @@ -23,7 +23,7 @@ #pragma once #include "misc/optionmap.hh" -#include "tgba/fwd.hh" +#include "twa/fwd.hh" #include "emptiness.hh" namespace spot diff --git a/src/tgbaalgos/totgba.cc b/src/tgbaalgos/totgba.cc index 71062928b..8bf320b94 100644 --- a/src/tgbaalgos/totgba.cc +++ b/src/tgbaalgos/totgba.cc @@ -20,7 +20,7 @@ #include "totgba.hh" #include "remfin.hh" #include "cleanacc.hh" -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/totgba.hh b/src/tgbaalgos/totgba.hh index 4d230398e..a40e5fbe1 100644 --- a/src/tgbaalgos/totgba.hh +++ b/src/tgbaalgos/totgba.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba/tgbagraph.hh" +#include "twa/twagraph.hh" namespace spot { diff --git a/src/tgbaalgos/weight.hh b/src/tgbaalgos/weight.hh index 551bf8017..5a5e38bc6 100644 --- a/src/tgbaalgos/weight.hh +++ b/src/tgbaalgos/weight.hh @@ -25,7 +25,7 @@ #include #include #include -#include "tgba/acc.hh" +#include "twa/acc.hh" namespace spot { diff --git a/src/tgbaalgos/word.cc b/src/tgbaalgos/word.cc index 525c01d98..dbfd1e829 100644 --- a/src/tgbaalgos/word.cc +++ b/src/tgbaalgos/word.cc @@ -18,8 +18,8 @@ // along with this program. If not, see . #include "word.hh" -#include "tgba/bddprint.hh" -#include "tgba/bdddict.hh" +#include "twa/bddprint.hh" +#include "twa/bdddict.hh" namespace spot { diff --git a/src/tgbatest/acc.cc b/src/tgbatest/acc.cc index 9344c7dce..e1719867f 100644 --- a/src/tgbatest/acc.cc +++ b/src/tgbatest/acc.cc @@ -22,7 +22,7 @@ #include #include #include -#include "tgba/acc.hh" +#include "twa/acc.hh" void check(spot::acc_cond& ac, spot::acc_cond::mark_t m) { diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index 1705d7bf3..c84539a0a 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -22,7 +22,7 @@ #include "tgbaalgos/dotty.hh" #include "tgbaalgos/hoa.hh" #include "hoaparse/public.hh" -#include "tgba/tgbaproduct.hh" +#include "twa/twaproduct.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "ltlparse/public.hh" @@ -33,7 +33,7 @@ #include "tgbaalgos/emptiness_stats.hh" #include "tgbaalgos/degen.hh" -#include "tgba/tgbasafracomplement.hh" +#include "twa/twasafracomplement.hh" void usage(const char* prog) { diff --git a/src/tgbatest/emptchk.cc b/src/tgbatest/emptchk.cc index fc2ae00d8..d058ac1f9 100644 --- a/src/tgbatest/emptchk.cc +++ b/src/tgbatest/emptchk.cc @@ -28,7 +28,7 @@ #include "tgbaalgos/ltl2taa.hh" #include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/degen.hh" -#include "tgba/tgbaproduct.hh" +#include "twa/twaproduct.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/emptiness.hh" diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 4bf7b7ea4..8d7a0cd2d 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -32,12 +32,12 @@ #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/ltl2taa.hh" -#include "tgba/bddprint.hh" +#include "twa/bddprint.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" #include "tgbaalgos/hoa.hh" #include "tgbaalgos/degen.hh" -#include "tgba/tgbaproduct.hh" +#include "twa/twaproduct.hh" #include "tgbaalgos/reducerun.hh" #include "dstarparse/public.hh" #include "hoaparse/public.hh" diff --git a/src/tgbatest/taatgba.cc b/src/tgbatest/taatgba.cc index 3f28ce82c..944805b02 100644 --- a/src/tgbatest/taatgba.cc +++ b/src/tgbatest/taatgba.cc @@ -23,7 +23,7 @@ #include "ltlenv/defaultenv.hh" #include "ltlast/allnodes.hh" #include "tgbaalgos/dotty.hh" -#include "tgba/taatgba.hh" +#include "twa/taatgba.hh" int main() diff --git a/src/tgba/.cvsignore b/src/twa/.cvsignore similarity index 100% rename from src/tgba/.cvsignore rename to src/twa/.cvsignore diff --git a/src/tgba/.gitignore b/src/twa/.gitignore similarity index 100% rename from src/tgba/.gitignore rename to src/twa/.gitignore diff --git a/src/tgba/Makefile.am b/src/twa/Makefile.am similarity index 79% rename from src/tgba/Makefile.am rename to src/twa/Makefile.am index 1133ca9a7..6ecf7c180 100644 --- a/src/tgba/Makefile.am +++ b/src/twa/Makefile.am @@ -23,32 +23,32 @@ AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) -tgbadir = $(pkgincludedir)/tgba +twadir = $(pkgincludedir)/twa -tgba_HEADERS = \ +twa_HEADERS = \ acc.hh \ bdddict.hh \ bddprint.hh \ formula2bdd.hh \ fwd.hh \ taatgba.hh \ - tgba.hh \ - tgbagraph.hh \ - tgbamask.hh \ - tgbaproxy.hh \ - tgbaproduct.hh \ - tgbasafracomplement.hh + twa.hh \ + twagraph.hh \ + twamask.hh \ + twaproxy.hh \ + twaproduct.hh \ + twasafracomplement.hh -noinst_LTLIBRARIES = libtgba.la -libtgba_la_SOURCES = \ +noinst_LTLIBRARIES = libtwa.la +libtwa_la_SOURCES = \ acc.cc \ bdddict.cc \ bddprint.cc \ formula2bdd.cc \ taatgba.cc \ - tgba.cc \ - tgbagraph.cc \ - tgbaproduct.cc \ - tgbamask.cc \ - tgbaproxy.cc \ - tgbasafracomplement.cc + twa.cc \ + twagraph.cc \ + twaproduct.cc \ + twamask.cc \ + twaproxy.cc \ + twasafracomplement.cc diff --git a/src/tgba/acc.cc b/src/twa/acc.cc similarity index 100% rename from src/tgba/acc.cc rename to src/twa/acc.cc diff --git a/src/tgba/acc.hh b/src/twa/acc.hh similarity index 100% rename from src/tgba/acc.hh rename to src/twa/acc.hh diff --git a/src/tgba/bdddict.cc b/src/twa/bdddict.cc similarity index 100% rename from src/tgba/bdddict.cc rename to src/twa/bdddict.cc diff --git a/src/tgba/bdddict.hh b/src/twa/bdddict.hh similarity index 100% rename from src/tgba/bdddict.hh rename to src/twa/bdddict.hh diff --git a/src/tgba/bddprint.cc b/src/twa/bddprint.cc similarity index 100% rename from src/tgba/bddprint.cc rename to src/twa/bddprint.cc diff --git a/src/tgba/bddprint.hh b/src/twa/bddprint.hh similarity index 100% rename from src/tgba/bddprint.hh rename to src/twa/bddprint.hh diff --git a/src/tgba/formula2bdd.cc b/src/twa/formula2bdd.cc similarity index 100% rename from src/tgba/formula2bdd.cc rename to src/twa/formula2bdd.cc diff --git a/src/tgba/formula2bdd.hh b/src/twa/formula2bdd.hh similarity index 100% rename from src/tgba/formula2bdd.hh rename to src/twa/formula2bdd.hh diff --git a/src/tgba/fwd.hh b/src/twa/fwd.hh similarity index 100% rename from src/tgba/fwd.hh rename to src/twa/fwd.hh diff --git a/src/tgba/taatgba.cc b/src/twa/taatgba.cc similarity index 99% rename from src/tgba/taatgba.cc rename to src/twa/taatgba.cc index 9badf2890..5efc0cf54 100644 --- a/src/tgba/taatgba.cc +++ b/src/twa/taatgba.cc @@ -21,7 +21,7 @@ #include #include #include -#include "tgba/formula2bdd.hh" +#include "twa/formula2bdd.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/clone.hh" #include "taatgba.hh" diff --git a/src/tgba/taatgba.hh b/src/twa/taatgba.hh similarity index 99% rename from src/tgba/taatgba.hh rename to src/twa/taatgba.hh index 21b8fc527..9cfcb019d 100644 --- a/src/tgba/taatgba.hh +++ b/src/twa/taatgba.hh @@ -26,7 +26,7 @@ #include "misc/hash.hh" #include "ltlast/formula.hh" #include "bdddict.hh" -#include "tgba.hh" +#include "twa.hh" #include "ltlvisit/tostring.hh" namespace spot diff --git a/src/tgba/tgba.cc b/src/twa/twa.cc similarity index 98% rename from src/tgba/tgba.cc rename to src/twa/twa.cc index 36a569c84..f680136fc 100644 --- a/src/tgba/tgba.cc +++ b/src/twa/twa.cc @@ -20,8 +20,8 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include "tgba.hh" -#include "tgbagraph.hh" +#include "twa.hh" +#include "twagraph.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/remfin.hh" #include diff --git a/src/tgba/tgba.hh b/src/twa/twa.hh similarity index 100% rename from src/tgba/tgba.hh rename to src/twa/twa.hh diff --git a/src/tgba/tgbagraph.cc b/src/twa/twagraph.cc similarity index 99% rename from src/tgba/tgbagraph.cc rename to src/twa/twagraph.cc index da487a460..0f29d3393 100644 --- a/src/tgba/tgbagraph.cc +++ b/src/twa/twagraph.cc @@ -17,7 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include "tgbagraph.hh" +#include "twagraph.hh" #include "ltlast/constant.hh" namespace spot diff --git a/src/tgba/tgbagraph.hh b/src/twa/twagraph.hh similarity index 99% rename from src/tgba/tgbagraph.hh rename to src/twa/twagraph.hh index 2818fe842..9bbefb260 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/twa/twagraph.hh @@ -22,8 +22,8 @@ #include "fwd.hh" #include "graph/graph.hh" #include "graph/ngraph.hh" -#include "tgba/bdddict.hh" -#include "tgba/tgba.hh" +#include "twa/bdddict.hh" +#include "twa/twa.hh" #include "tgbaalgos/dupexp.hh" #include diff --git a/src/tgba/tgbamask.cc b/src/twa/twamask.cc similarity index 99% rename from src/tgba/tgbamask.cc rename to src/twa/twamask.cc index 575994038..188f61e10 100644 --- a/src/tgba/tgbamask.cc +++ b/src/twa/twamask.cc @@ -17,7 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include "tgbamask.hh" +#include "twamask.hh" #include namespace spot diff --git a/src/tgba/tgbamask.hh b/src/twa/twamask.hh similarity index 98% rename from src/tgba/tgbamask.hh rename to src/twa/twamask.hh index ef58f5159..28fb71727 100644 --- a/src/tgba/tgbamask.hh +++ b/src/twa/twamask.hh @@ -20,7 +20,7 @@ #pragma once #include -#include "tgbaproxy.hh" +#include "twaproxy.hh" namespace spot { diff --git a/src/tgba/tgbaproduct.cc b/src/twa/twaproduct.cc similarity index 99% rename from src/tgba/tgbaproduct.cc rename to src/twa/twaproduct.cc index 30ca26c04..5de3c44ef 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/twa/twaproduct.cc @@ -20,7 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include "tgbaproduct.hh" +#include "twaproduct.hh" #include #include #include "misc/hashfunc.hh" diff --git a/src/tgba/tgbaproduct.hh b/src/twa/twaproduct.hh similarity index 99% rename from src/tgba/tgbaproduct.hh rename to src/twa/twaproduct.hh index 954744907..e94f16da5 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/twa/twaproduct.hh @@ -22,7 +22,7 @@ #pragma once -#include "tgba.hh" +#include "twa.hh" #include "misc/fixpool.hh" namespace spot diff --git a/src/tgba/tgbaproxy.cc b/src/twa/twaproxy.cc similarity index 98% rename from src/tgba/tgbaproxy.cc rename to src/twa/twaproxy.cc index 97d9b9af6..d24001156 100644 --- a/src/tgba/tgbaproxy.cc +++ b/src/twa/twaproxy.cc @@ -17,7 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include "tgbaproxy.hh" +#include "twaproxy.hh" namespace spot { diff --git a/src/tgba/tgbaproxy.hh b/src/twa/twaproxy.hh similarity index 98% rename from src/tgba/tgbaproxy.hh rename to src/twa/twaproxy.hh index f028593b1..c2954bf10 100644 --- a/src/tgba/tgbaproxy.hh +++ b/src/twa/twaproxy.hh @@ -19,7 +19,7 @@ #pragma once -#include "tgba.hh" +#include "twa.hh" namespace spot { diff --git a/src/tgba/tgbasafracomplement.cc b/src/twa/twasafracomplement.cc similarity index 97% rename from src/tgba/tgbasafracomplement.cc rename to src/twa/twasafracomplement.cc index 373c77c6e..d31c0f146 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/twa/twasafracomplement.cc @@ -27,13 +27,13 @@ #include #include "misc/hash.hh" #include "misc/bddlt.hh" -#include "tgba/bdddict.hh" -#include "tgba/tgba.hh" +#include "twa/bdddict.hh" +#include "twa/twa.hh" #include "misc/hashfunc.hh" #include "ltlast/formula.hh" #include "ltlast/constant.hh" #include "tgbaalgos/dotty.hh" -#include "tgba/tgbasafracomplement.hh" +#include "twa/twasafracomplement.hh" #include "tgbaalgos/degen.hh" namespace spot @@ -955,19 +955,19 @@ namespace spot /// Successor iterators used by spot::tgba_safra_complement. /// \ingroup twa_representation - class tgba_safra_complement_succ_iterator: public twa_succ_iterator + class twa_safra_complement_succ_iterator: public twa_succ_iterator { public: typedef std::multimap succ_list_t; - tgba_safra_complement_succ_iterator(const succ_list_t& list, + twa_safra_complement_succ_iterator(const succ_list_t& list, acc_cond::mark_t the_acceptance_cond) : list_(list), the_acceptance_cond_(the_acceptance_cond) { } virtual - ~tgba_safra_complement_succ_iterator() + ~twa_safra_complement_succ_iterator() { for (auto& p: list_) delete p.second; @@ -986,41 +986,41 @@ namespace spot }; bool - tgba_safra_complement_succ_iterator::first() + twa_safra_complement_succ_iterator::first() { it_ = list_.begin(); return it_ != list_.end(); } bool - tgba_safra_complement_succ_iterator::next() + twa_safra_complement_succ_iterator::next() { ++it_; return it_ != list_.end(); } bool - tgba_safra_complement_succ_iterator::done() const + twa_safra_complement_succ_iterator::done() const { return it_ == list_.end(); } state_complement* - tgba_safra_complement_succ_iterator::current_state() const + twa_safra_complement_succ_iterator::current_state() const { assert(!done()); return new state_complement(*(it_->second)); } bdd - tgba_safra_complement_succ_iterator::current_condition() const + twa_safra_complement_succ_iterator::current_condition() const { assert(!done()); return it_->first; } acc_cond::mark_t - tgba_safra_complement_succ_iterator::current_acceptance_conditions() const + twa_safra_complement_succ_iterator::current_acceptance_conditions() const { assert(!done()); return the_acceptance_cond_; @@ -1153,7 +1153,7 @@ namespace spot assert(tr != a->automaton.end()); acc_cond::mark_t condition = 0U; - tgba_safra_complement_succ_iterator::succ_list_t succ_list; + twa_safra_complement_succ_iterator::succ_list_t succ_list; int nb_acceptance_pairs = a->get_nb_acceptance_pairs(); bitvect* e = make_bitvect(nb_acceptance_pairs); @@ -1227,7 +1227,7 @@ namespace spot delete l; } delete e; - return new tgba_safra_complement_succ_iterator(succ_list, condition); + return new twa_safra_complement_succ_iterator(succ_list, condition); } std::string diff --git a/src/tgba/tgbasafracomplement.hh b/src/twa/twasafracomplement.hh similarity index 99% rename from src/tgba/tgbasafracomplement.hh rename to src/twa/twasafracomplement.hh index b325efcfd..857b1e743 100644 --- a/src/tgba/tgbasafracomplement.hh +++ b/src/twa/twasafracomplement.hh @@ -20,7 +20,7 @@ #pragma once #include -#include "tgba.hh" +#include "twa.hh" #ifndef TRANSFORM_TO_TBA # define TRANSFORM_TO_TBA 0 diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 16356eb1e..7b3606cc6 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -55,7 +55,7 @@ %shared_ptr(spot::taa_tgba) %shared_ptr(spot::taa_tgba_string) %shared_ptr(spot::taa_tgba_formula) -%shared_ptr(spot::tgba_safra_complement) +%shared_ptr(spot::twa_safra_complement) %shared_ptr(spot::tgba_run) %shared_ptr(spot::emptiness_check_result) %shared_ptr(spot::emptiness_check) @@ -93,7 +93,7 @@ namespace std { #include "ltlparse/public.hh" -#include "tgba/bdddict.hh" +#include "twa/bdddict.hh" #include "ltlvisit/apcollect.hh" #include "ltlvisit/dotty.hh" @@ -109,12 +109,12 @@ namespace std { #include "ltlvisit/remove_x.hh" #include "ltlvisit/relabel.hh" -#include "tgba/bddprint.hh" -#include "tgba/fwd.hh" -#include "tgba/acc.hh" -#include "tgba/tgba.hh" -#include "tgba/taatgba.hh" -#include "tgba/tgbaproduct.hh" +#include "twa/bddprint.hh" +#include "twa/fwd.hh" +#include "twa/acc.hh" +#include "twa/twa.hh" +#include "twa/taatgba.hh" +#include "twa/twaproduct.hh" #include "tgbaalgos/cleanacc.hh" #include "tgbaalgos/dotty.hh" @@ -228,13 +228,13 @@ using namespace spot; %include "ltlparse/public.hh" /* these must come before apcollect.hh */ -%include "tgba/bdddict.hh" -%include "tgba/bddprint.hh" -%include "tgba/fwd.hh" +%include "twa/bdddict.hh" +%include "twa/bddprint.hh" +%include "twa/fwd.hh" %feature("flatnested") spot::acc_cond::mark_t; %feature("flatnested") spot::acc_cond::acc_code; -%include "tgba/acc.hh" -%include "tgba/tgba.hh" +%include "twa/acc.hh" +%include "twa/twa.hh" %include "ltlvisit/apcollect.hh" %include "ltlvisit/dotty.hh" @@ -252,9 +252,9 @@ using namespace spot; // Help SWIG with namespace lookups. #define ltl spot::ltl -%include "tgba/taatgba.hh" -%include "tgba/tgbaproduct.hh" -%include "tgba/tgbagraph.hh" +%include "twa/taatgba.hh" +%include "twa/twaproduct.hh" +%include "twa/twagraph.hh" // Should come after the definition of twa_graph