From 8520c4c33092f9172a41530007fff68c26cbd674 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 21 Apr 2015 19:38:09 +0200 Subject: [PATCH] rename tgba_ptr into twa_ptr Automatic mass renaming. * iface/ltsmin/modelcheck.cc, src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc, src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh, src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh, src/tgba/fwd.hh, src/tgba/tgba.cc, src/tgba/tgba.hh, src/tgba/tgbagraph.hh, src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh, src/tgbaalgos/bfssteps.cc, src/tgbaalgos/bfssteps.hh, src/tgbaalgos/complete.cc, src/tgbaalgos/complete.hh, src/tgbaalgos/compsusp.cc, src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh, src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh, src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh, src/tgbaalgos/hoa.cc, src/tgbaalgos/hoa.hh, src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh, src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, src/tgbaalgos/minimize.cc, src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh, src/tgbaalgos/projrun.cc, src/tgbaalgos/projrun.hh, src/tgbaalgos/reachiter.cc, src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh, src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh, src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh, src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh, src/tgbaalgos/stutter.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh, src/tgbatest/checkta.cc, src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc, wrap/python/spot_impl.i: Rename tgba_ptr as twa_ptr. --- iface/ltsmin/modelcheck.cc | 4 ++-- src/dstarparse/dra2ba.cc | 8 ++++---- src/dstarparse/nra2nba.cc | 4 ++-- src/ltlvisit/apcollect.cc | 2 +- src/ltlvisit/apcollect.hh | 2 +- src/ta/taexplicit.cc | 4 ++-- src/ta/taexplicit.hh | 8 ++++---- src/ta/tgtaexplicit.cc | 2 +- src/ta/tgtaexplicit.hh | 4 ++-- src/ta/tgtaproduct.hh | 2 +- src/taalgos/tgba2ta.cc | 6 +++--- src/taalgos/tgba2ta.hh | 4 ++-- src/tgba/fwd.hh | 4 ++-- src/tgba/tgba.cc | 2 +- src/tgba/tgba.hh | 8 ++++---- src/tgba/tgbagraph.hh | 2 +- src/tgba/tgbamask.cc | 20 ++++++++++---------- src/tgba/tgbamask.hh | 12 ++++++------ src/tgba/tgbaproduct.cc | 14 +++++++------- src/tgba/tgbaproduct.hh | 18 +++++++++--------- src/tgba/tgbaproxy.cc | 4 ++-- src/tgba/tgbaproxy.hh | 6 +++--- src/tgbaalgos/bfssteps.cc | 2 +- src/tgbaalgos/bfssteps.hh | 4 ++-- src/tgbaalgos/complete.cc | 2 +- src/tgbaalgos/complete.hh | 2 +- src/tgbaalgos/compsusp.cc | 2 +- src/tgbaalgos/dotty.cc | 2 +- src/tgbaalgos/dotty.hh | 2 +- src/tgbaalgos/dtgbasat.cc | 4 ++-- src/tgbaalgos/dupexp.cc | 6 +++--- src/tgbaalgos/dupexp.hh | 4 ++-- src/tgbaalgos/emptiness.cc | 8 ++++---- src/tgbaalgos/emptiness.hh | 18 +++++++++--------- src/tgbaalgos/gtec/gtec.cc | 6 +++--- src/tgbaalgos/gtec/gtec.hh | 6 +++--- src/tgbaalgos/gtec/status.cc | 2 +- src/tgbaalgos/gtec/status.hh | 4 ++-- src/tgbaalgos/gv04.cc | 4 ++-- src/tgbaalgos/gv04.hh | 2 +- src/tgbaalgos/hoa.cc | 2 +- src/tgbaalgos/hoa.hh | 2 +- src/tgbaalgos/lbtt.cc | 4 ++-- src/tgbaalgos/lbtt.hh | 2 +- src/tgbaalgos/magic.cc | 8 ++++---- src/tgbaalgos/magic.hh | 6 +++--- src/tgbaalgos/minimize.cc | 10 +++++----- src/tgbaalgos/ndfs_result.hxx | 6 +++--- src/tgbaalgos/neverclaim.cc | 2 +- src/tgbaalgos/neverclaim.hh | 2 +- src/tgbaalgos/projrun.cc | 4 ++-- src/tgbaalgos/projrun.hh | 4 ++-- src/tgbaalgos/reachiter.cc | 8 ++++---- src/tgbaalgos/reachiter.hh | 12 ++++++------ src/tgbaalgos/reducerun.cc | 4 ++-- src/tgbaalgos/reducerun.hh | 2 +- src/tgbaalgos/replayrun.cc | 4 ++-- src/tgbaalgos/replayrun.hh | 2 +- src/tgbaalgos/scc.cc | 6 +++--- src/tgbaalgos/scc.hh | 8 ++++---- src/tgbaalgos/se05.cc | 8 ++++---- src/tgbaalgos/se05.hh | 6 +++--- src/tgbaalgos/stats.cc | 8 ++++---- src/tgbaalgos/stats.hh | 4 ++-- src/tgbaalgos/stutter.cc | 6 +++--- src/tgbaalgos/tau03.cc | 4 ++-- src/tgbaalgos/tau03.hh | 2 +- src/tgbaalgos/tau03opt.cc | 4 ++-- src/tgbaalgos/tau03opt.hh | 2 +- src/tgbatest/checkta.cc | 2 +- src/tgbatest/complementation.cc | 4 ++-- src/tgbatest/emptchk.cc | 2 +- src/tgbatest/ltl2tgba.cc | 6 +++--- wrap/python/spot_impl.i | 2 +- 74 files changed, 189 insertions(+), 189 deletions(-) diff --git a/iface/ltsmin/modelcheck.cc b/iface/ltsmin/modelcheck.cc index f6391174d..ae313ddf7 100644 --- a/iface/ltsmin/modelcheck.cc +++ b/iface/ltsmin/modelcheck.cc @@ -158,8 +158,8 @@ checked_main(int argc, char **argv) spot::ltl::atomic_prop_set ap; auto dict = spot::make_bdd_dict(); spot::const_kripke_ptr model = nullptr; - spot::const_tgba_ptr prop = nullptr; - spot::const_tgba_ptr product = nullptr; + spot::const_twa_ptr prop = nullptr; + spot::const_twa_ptr product = nullptr; spot::emptiness_check_instantiator_ptr echeck_inst = nullptr; int exit_code = 0; spot::postprocessor post; diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc index f6ffdc082..ca380967e 100644 --- a/src/dstarparse/dra2ba.cc +++ b/src/dstarparse/dra2ba.cc @@ -50,7 +50,7 @@ namespace spot // This function is defined in nra2nba.cc, and used only here. SPOT_LOCAL twa_graph_ptr nra_to_nba(const const_dstar_aut_ptr& nra, - const const_tgba_ptr& aut); + const const_twa_ptr& aut); namespace { @@ -65,14 +65,14 @@ namespace spot // retrive acceptances. static bool - filter_states(const const_tgba_ptr& aut, + filter_states(const const_twa_ptr& aut, const const_dstar_aut_ptr& dra, const state_list& sl, state_list& final, state_list& nonfinal); static bool - filter_scc(const const_tgba_ptr& aut, + filter_scc(const const_twa_ptr& aut, const const_dstar_aut_ptr& dra, state_list& final, state_list& nonfinal) @@ -99,7 +99,7 @@ namespace spot } static bool - filter_states(const const_tgba_ptr& aut, + filter_states(const const_twa_ptr& aut, const const_dstar_aut_ptr& dra, const state_list& sl, state_list& final, diff --git a/src/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc index 9fb87864d..628a89e69 100644 --- a/src/dstarparse/nra2nba.cc +++ b/src/dstarparse/nra2nba.cc @@ -38,7 +38,7 @@ namespace spot // AUT is the automaton we iterate on, while A is the automaton // we read the acceptance conditions from. Separating the two // makes its possible to mask AUT, as needed in dra_to_ba(). - nra_to_nba_worker(const const_dstar_aut_ptr& a, const_tgba_ptr aut): + nra_to_nba_worker(const const_dstar_aut_ptr& a, const_twa_ptr aut): tgba_reachable_iterator_depth_first(aut), out_(make_twa_graph(aut->get_dict())), d_(a), @@ -116,7 +116,7 @@ namespace spot // that is a masked version of nra->aut. SPOT_LOCAL twa_graph_ptr nra_to_nba(const const_dstar_aut_ptr& nra, - const const_tgba_ptr& aut) + const const_twa_ptr& aut) { assert(nra->type == Rabin); nra_to_nba_worker w(nra, aut); diff --git a/src/ltlvisit/apcollect.cc b/src/ltlvisit/apcollect.cc index 82bd67dea..44567766a 100644 --- a/src/ltlvisit/apcollect.cc +++ b/src/ltlvisit/apcollect.cc @@ -85,7 +85,7 @@ namespace spot } bdd - atomic_prop_collect_as_bdd(const formula* f, const const_tgba_ptr& a) + atomic_prop_collect_as_bdd(const formula* f, const const_twa_ptr& a) { spot::ltl::atomic_prop_set aps; atomic_prop_collect(f, &aps); diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh index c80f05530..ab5a461cd 100644 --- a/src/ltlvisit/apcollect.hh +++ b/src/ltlvisit/apcollect.hh @@ -68,7 +68,7 @@ namespace spot /// \return A conjunction the atomic propositions. SPOT_API bdd atomic_prop_collect_as_bdd(const formula* f, - const const_tgba_ptr& a); + const const_twa_ptr& a); /// @} } diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index eaed7c432..271ee0417 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -350,7 +350,7 @@ namespace spot // ta_explicit - ta_explicit::ta_explicit(const const_tgba_ptr& tgba, + ta_explicit::ta_explicit(const const_twa_ptr& tgba, unsigned n_acc, state_ta_explicit* artificial_initial_state): ta(tgba->get_dict()), @@ -495,7 +495,7 @@ namespace spot return tgba_->get_dict(); } - const_tgba_ptr + const_twa_ptr ta_explicit::get_tgba() const { return tgba_; diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh index c4524696b..7b6da1d47 100644 --- a/src/ta/taexplicit.hh +++ b/src/ta/taexplicit.hh @@ -40,11 +40,11 @@ namespace spot class SPOT_API ta_explicit : public ta { public: - ta_explicit(const const_tgba_ptr& tgba, + ta_explicit(const const_twa_ptr& tgba, unsigned n_acc, state_ta_explicit* artificial_initial_state = 0); - const_tgba_ptr + const_twa_ptr get_tgba() const; state_ta_explicit* @@ -121,7 +121,7 @@ namespace spot ta_explicit(const ta_explicit& other) SPOT_DELETED; ta_explicit& operator=(const ta_explicit& other) SPOT_DELETED; - const_tgba_ptr tgba_; + const_twa_ptr tgba_; state_ta_explicit* artificial_initial_state_; ta::states_set_t states_set_; ta::states_set_t initial_states_set_; @@ -252,7 +252,7 @@ namespace spot typedef std::shared_ptr ta_explicit_ptr; typedef std::shared_ptr const_ta_explicit_ptr; - inline ta_explicit_ptr make_ta_explicit(const const_tgba_ptr& tgba, + inline ta_explicit_ptr make_ta_explicit(const const_twa_ptr& tgba, unsigned n_acc, state_ta_explicit* artificial_initial_state = 0) diff --git a/src/ta/tgtaexplicit.cc b/src/ta/tgtaexplicit.cc index d940ba43e..26c2f229d 100644 --- a/src/ta/tgtaexplicit.cc +++ b/src/ta/tgtaexplicit.cc @@ -28,7 +28,7 @@ namespace spot { - tgta_explicit::tgta_explicit(const const_tgba_ptr& tgba, + tgta_explicit::tgta_explicit(const const_twa_ptr& tgba, unsigned n_acc, state_ta_explicit* artificial_initial_state) : tgta(tgba->get_dict()), diff --git a/src/ta/tgtaexplicit.hh b/src/ta/tgtaexplicit.hh index 84fbf0c22..cfe6e1789 100644 --- a/src/ta/tgtaexplicit.hh +++ b/src/ta/tgtaexplicit.hh @@ -37,7 +37,7 @@ namespace spot class SPOT_API tgta_explicit : public tgta { public: - tgta_explicit(const const_tgba_ptr& tgba, + tgta_explicit(const const_twa_ptr& tgba, unsigned n_acc, state_ta_explicit* artificial_initial_state); @@ -66,7 +66,7 @@ namespace spot typedef std::shared_ptr tgta_explicit_ptr; typedef std::shared_ptr const_tgta_explicit_ptr; - inline tgta_explicit_ptr make_tgta_explicit(const const_tgba_ptr& tgba, + inline tgta_explicit_ptr make_tgta_explicit(const const_twa_ptr& tgba, unsigned n_acc, state_ta_explicit* artificial_initial_state = 0) diff --git a/src/ta/tgtaproduct.hh b/src/ta/tgtaproduct.hh index f58186903..177dbc601 100644 --- a/src/ta/tgtaproduct.hh +++ b/src/ta/tgtaproduct.hh @@ -42,7 +42,7 @@ namespace spot succ_iter(const state* local_state) const; }; - inline tgba_ptr product(const const_kripke_ptr& left, + inline twa_ptr product(const const_kripke_ptr& left, const const_tgta_ptr& right) { return std::make_shared(left, right); diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index eb0c054e9..e5863df44 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -415,7 +415,7 @@ namespace spot { std::stack todo; - const_tgba_ptr tgba_ = ta->get_tgba(); + const_twa_ptr tgba_ = ta->get_tgba(); // build Initial states set: state* tgba_init_state = tgba_->get_init_state(); @@ -544,7 +544,7 @@ namespace spot } ta_explicit_ptr - tgba_to_ta(const const_tgba_ptr& tgba_, bdd atomic_propositions_set_, + tgba_to_ta(const const_twa_ptr& tgba_, bdd atomic_propositions_set_, bool degeneralized, bool artificial_initial_state_mode, bool single_pass_emptiness_check, bool artificial_livelock_state_mode, @@ -601,7 +601,7 @@ namespace spot } tgta_explicit_ptr - tgba_to_tgta(const const_tgba_ptr& tgba_, bdd atomic_propositions_set_) + tgba_to_tgta(const const_twa_ptr& tgba_, bdd atomic_propositions_set_) { state* tgba_init_state = tgba_->get_init_state(); auto artificial_init_state = new state_ta_explicit(tgba_init_state->clone(), diff --git a/src/taalgos/tgba2ta.hh b/src/taalgos/tgba2ta.hh index 8ad671c3f..fc231d987 100644 --- a/src/taalgos/tgba2ta.hh +++ b/src/taalgos/tgba2ta.hh @@ -82,7 +82,7 @@ namespace spot /// \return A spot::ta_explicit that recognizes the same language as the /// TGBA \a tgba_to_convert. SPOT_API ta_explicit_ptr - tgba_to_ta(const const_tgba_ptr& tgba_to_convert, bdd atomic_propositions_set, + tgba_to_ta(const const_twa_ptr& tgba_to_convert, bdd atomic_propositions_set, bool degeneralized = true, bool artificial_initial_state_mode = true, bool single_pass_emptiness_check = false, @@ -99,6 +99,6 @@ namespace spot /// \return A spot::tgta_explicit (spot::tgta) that recognizes the same /// language as the TGBA \a tgba_to_convert. SPOT_API tgta_explicit_ptr - tgba_to_tgta(const const_tgba_ptr& tgba_to_convert, + tgba_to_tgta(const const_twa_ptr& tgba_to_convert, bdd atomic_propositions_set); } diff --git a/src/tgba/fwd.hh b/src/tgba/fwd.hh index 40ce575d3..5318e940f 100644 --- a/src/tgba/fwd.hh +++ b/src/tgba/fwd.hh @@ -24,8 +24,8 @@ namespace spot { class twa; - typedef std::shared_ptr tgba_ptr; - typedef std::shared_ptr const_tgba_ptr; + typedef std::shared_ptr twa_ptr; + typedef std::shared_ptr const_twa_ptr; class twa_graph; typedef std::shared_ptr const_twa_graph_ptr; diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index aa9d6b43b..36a569c84 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -60,7 +60,7 @@ namespace spot state* twa::project_state(const state* s, - const const_tgba_ptr& t) const + const const_twa_ptr& t) const { if (t.get() == this) return s->clone(); diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 0221d5419..d5869706f 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -629,7 +629,7 @@ namespace spot /// or a new \c state* (the projected state) that must be /// destroyed by the caller. virtual state* project_state(const state* s, - const const_tgba_ptr& t) const; + const const_twa_ptr& t) const; const acc_cond& acc() const @@ -672,7 +672,7 @@ namespace spot } /// \brief Copy the acceptance condition of another tgba. - void copy_acceptance_of(const const_tgba_ptr& a) + void copy_acceptance_of(const const_twa_ptr& a) { acc_ = a->acc(); unsigned num = acc_.num_sets(); @@ -680,7 +680,7 @@ namespace spot prop_state_based_acc(); } - void copy_ap_of(const const_tgba_ptr& a) + void copy_ap_of(const const_twa_ptr& a) { get_dict()->register_all_propositions_of(a, this); } @@ -821,7 +821,7 @@ namespace spot // There is no default value here on purpose. This way any time we // add a new property we have to update every call to prop_copy(). - void prop_copy(const const_tgba_ptr& other, prop_set p) + void prop_copy(const const_twa_ptr& other, prop_set p) { if (p.state_based) prop_state_based_acc(other->has_state_based_acc()); diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 9db68d81f..87b6c4153 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -470,7 +470,7 @@ namespace spot return std::make_shared(aut, p); } - inline twa_graph_ptr make_twa_graph(const const_tgba_ptr& aut, + inline twa_graph_ptr make_twa_graph(const const_twa_ptr& aut, twa::prop_set p) { auto a = std::dynamic_pointer_cast(aut); diff --git a/src/tgba/tgbamask.cc b/src/tgba/tgbamask.cc index c445ed1da..93c86b010 100644 --- a/src/tgba/tgbamask.cc +++ b/src/tgba/tgbamask.cc @@ -91,7 +91,7 @@ namespace spot /// \param masked The automaton to mask /// \param init Any state to use as initial state. This state will be /// destroyed by the destructor. - tgba_mask(const const_tgba_ptr& masked, const state* init = 0): + tgba_mask(const const_twa_ptr& masked, const state* init = 0): tgba_proxy(masked), init_(init) { @@ -150,7 +150,7 @@ namespace spot { const state_set& mask_; public: - tgba_mask_keep(const const_tgba_ptr& masked, + tgba_mask_keep(const const_twa_ptr& masked, const state_set& mask, const state* init) : tgba_mask(masked, init), @@ -169,7 +169,7 @@ namespace spot { const state_set& mask_; public: - tgba_mask_ignore(const const_tgba_ptr& masked, + tgba_mask_ignore(const const_twa_ptr& masked, const state_set& mask, const state* init) : tgba_mask(masked, init), @@ -188,7 +188,7 @@ namespace spot { unsigned mask_; public: - tgba_mask_acc_ignore(const const_tgba_ptr& masked, + tgba_mask_acc_ignore(const const_twa_ptr& masked, unsigned mask, const state* init) : tgba_mask(masked, init), @@ -204,24 +204,24 @@ namespace spot } - const_tgba_ptr - build_tgba_mask_keep(const const_tgba_ptr& to_mask, + const_twa_ptr + build_tgba_mask_keep(const const_twa_ptr& to_mask, const state_set& to_keep, const state* init) { return std::make_shared(to_mask, to_keep, init); } - const_tgba_ptr - build_tgba_mask_ignore(const const_tgba_ptr& to_mask, + const_twa_ptr + build_tgba_mask_ignore(const const_twa_ptr& to_mask, const state_set& to_ignore, const state* init) { return std::make_shared(to_mask, to_ignore, init); } - const_tgba_ptr - build_tgba_mask_acc_ignore(const const_tgba_ptr& to_mask, + const_twa_ptr + build_tgba_mask_acc_ignore(const const_twa_ptr& to_mask, unsigned to_ignore, const state* init) { diff --git a/src/tgba/tgbamask.hh b/src/tgba/tgbamask.hh index 6d33ac01a..49261c705 100644 --- a/src/tgba/tgbamask.hh +++ b/src/tgba/tgbamask.hh @@ -31,8 +31,8 @@ namespace spot /// Mask the TGBA \a to_mask, keeping only the /// states from \a to_keep. The initial state /// can optionally be reset to \a init. - SPOT_API const_tgba_ptr - build_tgba_mask_keep(const const_tgba_ptr& to_mask, + SPOT_API const_twa_ptr + build_tgba_mask_keep(const const_twa_ptr& to_mask, const state_set& to_keep, const state* init = 0); @@ -42,8 +42,8 @@ namespace spot /// Mask the TGBA \a to_mask, keeping only the states that are not /// in \a to_ignore. The initial state can optionally be reset to /// \a init. - SPOT_API const_tgba_ptr - build_tgba_mask_ignore(const const_tgba_ptr& to_mask, + SPOT_API const_twa_ptr + build_tgba_mask_ignore(const const_twa_ptr& to_mask, const state_set& to_ignore, const state* init = 0); @@ -59,8 +59,8 @@ namespace spot /// set of all acceptance set) is not changed, because so far this /// function is only needed in graph algorithms that do not call /// all_acceptance_conditions(). - SPOT_API const_tgba_ptr - build_tgba_mask_acc_ignore(const const_tgba_ptr& to_mask, + SPOT_API const_twa_ptr + build_tgba_mask_acc_ignore(const const_twa_ptr& to_mask, unsigned to_ignore, const state* init = 0); } diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 0aa2be032..30ca26c04 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -90,8 +90,8 @@ namespace spot { } - void recycle(const const_tgba_ptr& l, twa_succ_iterator* left, - const_tgba_ptr r, twa_succ_iterator* right) + void recycle(const const_twa_ptr& l, twa_succ_iterator* left, + const_twa_ptr r, twa_succ_iterator* right) { l->release_iter(left_); left_ = left; @@ -282,8 +282,8 @@ namespace spot //////////////////////////////////////////////////////////// // twa_product - twa_product::twa_product(const const_tgba_ptr& left, - const const_tgba_ptr& right) + twa_product::twa_product(const const_twa_ptr& left, + const const_twa_ptr& right) : twa(left->get_dict()), left_(left), right_(right), pool_(sizeof(state_product)) { @@ -393,7 +393,7 @@ namespace spot } state* - twa_product::project_state(const state* s, const const_tgba_ptr& t) const + twa_product::project_state(const state* s, const const_twa_ptr& t) const { const state_product* s2 = down_cast(s); assert(s2); @@ -423,8 +423,8 @@ namespace spot ////////////////////////////////////////////////////////////////////// // twa_product_init - twa_product_init::twa_product_init(const const_tgba_ptr& left, - const const_tgba_ptr& right, + twa_product_init::twa_product_init(const const_twa_ptr& left, + const const_twa_ptr& right, const state* left_init, const state* right_init) : twa_product(left, right), diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index 15181b1e2..a2537242f 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -84,7 +84,7 @@ namespace spot /// \param left The left automata in the product. /// \param right The right automata in the product. /// Do not be fooled by these arguments: a product is commutative. - twa_product(const const_tgba_ptr& left, const const_tgba_ptr& right); + twa_product(const const_twa_ptr& left, const const_twa_ptr& right); virtual ~twa_product(); @@ -98,7 +98,7 @@ namespace spot virtual std::string transition_annotation(const twa_succ_iterator* t) const; - virtual state* project_state(const state* s, const const_tgba_ptr& t) const; + virtual state* project_state(const state* s, const const_twa_ptr& t) const; const acc_cond& left_acc() const; const acc_cond& right_acc() const; @@ -107,8 +107,8 @@ namespace spot virtual bdd compute_support_conditions(const state* state) const; protected: - const_tgba_ptr left_; - const_tgba_ptr right_; + const_twa_ptr left_; + const_twa_ptr right_; bool left_kripke_; fixed_size_pool pool_; @@ -122,7 +122,7 @@ namespace spot class SPOT_API twa_product_init final: public twa_product { public: - twa_product_init(const const_tgba_ptr& left, const const_tgba_ptr& right, + twa_product_init(const const_twa_ptr& left, const const_twa_ptr& right, const state* left_init, const state* right_init); virtual state* get_init_state() const; protected: @@ -131,15 +131,15 @@ namespace spot }; /// \brief on-the-fly TGBA product - inline twa_product_ptr otf_product(const const_tgba_ptr& left, - const const_tgba_ptr& right) + inline twa_product_ptr otf_product(const const_twa_ptr& left, + const const_twa_ptr& right) { return std::make_shared(left, right); } /// \brief on-the-fly TGBA product with forced initial states - inline twa_product_ptr otf_product_at(const const_tgba_ptr& left, - const const_tgba_ptr& right, + inline twa_product_ptr otf_product_at(const const_twa_ptr& left, + const const_twa_ptr& right, const state* left_init, const state* right_init) { diff --git a/src/tgba/tgbaproxy.cc b/src/tgba/tgbaproxy.cc index 73b2c822d..ada6ad90a 100644 --- a/src/tgba/tgbaproxy.cc +++ b/src/tgba/tgbaproxy.cc @@ -21,7 +21,7 @@ namespace spot { - tgba_proxy::tgba_proxy(const const_tgba_ptr& original) + tgba_proxy::tgba_proxy(const const_twa_ptr& original) : twa(original->get_dict()), original_(original) { get_dict()->register_all_variables_of(original, this); @@ -62,7 +62,7 @@ namespace spot } state* - tgba_proxy::project_state(const state* s, const const_tgba_ptr& t) const + tgba_proxy::project_state(const state* s, const const_twa_ptr& t) const { return original_->project_state(s, t); } diff --git a/src/tgba/tgbaproxy.hh b/src/tgba/tgbaproxy.hh index 6bcbf98ff..290cd6ade 100644 --- a/src/tgba/tgbaproxy.hh +++ b/src/tgba/tgbaproxy.hh @@ -35,7 +35,7 @@ namespace spot class SPOT_API tgba_proxy: public twa { protected: - tgba_proxy(const const_tgba_ptr& original); + tgba_proxy(const const_twa_ptr& original); public: virtual ~tgba_proxy(); @@ -50,10 +50,10 @@ namespace spot virtual std::string transition_annotation(const twa_succ_iterator* t) const; - virtual state* project_state(const state* s, const const_tgba_ptr& t) const; + virtual state* project_state(const state* s, const const_twa_ptr& t) const; protected: virtual bdd compute_support_conditions(const state* state) const; - const_tgba_ptr original_; + const_twa_ptr original_; }; } diff --git a/src/tgbaalgos/bfssteps.cc b/src/tgbaalgos/bfssteps.cc index 0bd40fc7b..282457772 100644 --- a/src/tgbaalgos/bfssteps.cc +++ b/src/tgbaalgos/bfssteps.cc @@ -28,7 +28,7 @@ namespace spot { - bfs_steps::bfs_steps(const const_tgba_ptr& a) + bfs_steps::bfs_steps(const const_twa_ptr& a) : a_(a) { } diff --git a/src/tgbaalgos/bfssteps.hh b/src/tgbaalgos/bfssteps.hh index 49f70a1ce..eef653ac7 100644 --- a/src/tgbaalgos/bfssteps.hh +++ b/src/tgbaalgos/bfssteps.hh @@ -40,7 +40,7 @@ namespace spot class SPOT_API bfs_steps { public: - bfs_steps(const const_tgba_ptr& a); + bfs_steps(const const_twa_ptr& a); virtual ~bfs_steps(); /// \brief Start the search from \a start, and append the @@ -97,6 +97,6 @@ namespace spot tgba_run::steps& l); protected: - const_tgba_ptr a_; ///< The spot::tgba we are searching into. + const_twa_ptr a_; ///< The spot::tgba we are searching into. }; } diff --git a/src/tgbaalgos/complete.cc b/src/tgbaalgos/complete.cc index b10be5d7c..b65e140be 100644 --- a/src/tgbaalgos/complete.cc +++ b/src/tgbaalgos/complete.cc @@ -117,7 +117,7 @@ namespace spot return sink; } - twa_graph_ptr tgba_complete(const const_tgba_ptr& aut) + twa_graph_ptr tgba_complete(const const_twa_ptr& aut) { auto res = make_twa_graph(aut, { true, // state based diff --git a/src/tgbaalgos/complete.hh b/src/tgbaalgos/complete.hh index 7d18804e2..089ac9ab2 100644 --- a/src/tgbaalgos/complete.hh +++ b/src/tgbaalgos/complete.hh @@ -35,5 +35,5 @@ namespace spot /// \brief Clone a tgba and complete it. /// /// If the tgba has no acceptance set, one will be added. - SPOT_API twa_graph_ptr tgba_complete(const const_tgba_ptr& aut); + SPOT_API twa_graph_ptr tgba_complete(const const_twa_ptr& aut); } diff --git a/src/tgbaalgos/compsusp.cc b/src/tgbaalgos/compsusp.cc index e91e6a2e0..4c412bbf9 100644 --- a/src/tgbaalgos/compsusp.cc +++ b/src/tgbaalgos/compsusp.cc @@ -212,7 +212,7 @@ namespace spot static twa_graph_ptr - susp_prod(const const_tgba_ptr& left, const ltl::formula* f, bdd v) + susp_prod(const const_twa_ptr& left, const ltl::formula* f, bdd v) { bdd_dict_ptr dict = left->get_dict(); auto right = diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 2f0d85451..55622292e 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -488,7 +488,7 @@ namespace spot } // anonymous namespace std::ostream& - dotty_reachable(std::ostream& os, const const_tgba_ptr& g, + dotty_reachable(std::ostream& os, const const_twa_ptr& g, const char* options) { dotty_output d(os, options); diff --git a/src/tgbaalgos/dotty.hh b/src/tgbaalgos/dotty.hh index 7eaf680ad..e5c502cf3 100644 --- a/src/tgbaalgos/dotty.hh +++ b/src/tgbaalgos/dotty.hh @@ -42,6 +42,6 @@ namespace spot /// 'a' shows the acceptance. SPOT_API std::ostream& dotty_reachable(std::ostream& os, - const const_tgba_ptr& g, + const const_twa_ptr& g, const char* options = nullptr); } diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index 47c5b4b0b..499c12df5 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -245,12 +245,12 @@ namespace spot struct dict { - dict(const const_tgba_ptr& a) + dict(const const_twa_ptr& a) : aut(a) { } - const_tgba_ptr aut; + const_twa_ptr aut; typedef std::map trans_map; typedef std::map trans_acc_map; trans_map transid; diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc index 14e0fb506..9c5dbf9d9 100644 --- a/src/tgbaalgos/dupexp.cc +++ b/src/tgbaalgos/dupexp.cc @@ -36,7 +36,7 @@ namespace spot class dupexp_iter: public T { public: - dupexp_iter(const const_tgba_ptr& a, twa::prop_set p) + dupexp_iter(const const_twa_ptr& a, twa::prop_set p) : T(a), out_(make_twa_graph(a->get_dict())) { out_->copy_acceptance_of(a); @@ -76,7 +76,7 @@ namespace spot } // anonymous twa_graph_ptr - tgba_dupexp_bfs(const const_tgba_ptr& aut, twa::prop_set p) + tgba_dupexp_bfs(const const_twa_ptr& aut, twa::prop_set p) { dupexp_iter di(aut, p); di.run(); @@ -84,7 +84,7 @@ namespace spot } twa_graph_ptr - tgba_dupexp_dfs(const const_tgba_ptr& aut, twa::prop_set p) + tgba_dupexp_dfs(const const_twa_ptr& aut, twa::prop_set p) { dupexp_iter di(aut, p); di.run(); diff --git a/src/tgbaalgos/dupexp.hh b/src/tgbaalgos/dupexp.hh index 3a7fa1c0c..cea32cba0 100644 --- a/src/tgbaalgos/dupexp.hh +++ b/src/tgbaalgos/dupexp.hh @@ -33,10 +33,10 @@ namespace spot /// \brief Build an explicit automaton from all states of \a aut, /// numbering states in bread first order as they are processed. SPOT_API twa_graph_ptr - tgba_dupexp_bfs(const const_tgba_ptr& aut, twa::prop_set p); + tgba_dupexp_bfs(const const_twa_ptr& aut, twa::prop_set p); /// \ingroup tgba_misc /// \brief Build an explicit automaton from all states of \a aut, /// numbering states in depth first order as they are processed. SPOT_API twa_graph_ptr - tgba_dupexp_dfs(const const_tgba_ptr& aut, twa::prop_set p); + tgba_dupexp_dfs(const const_twa_ptr& aut, twa::prop_set p); } diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc index 8a863bf32..f6d7b0bcc 100644 --- a/src/tgbaalgos/emptiness.cc +++ b/src/tgbaalgos/emptiness.cc @@ -77,7 +77,7 @@ namespace spot std::ostream& print_tgba_run(std::ostream& os, - const const_tgba_ptr& a, + const const_twa_ptr& a, const const_tgba_run_ptr& run) { bdd_dict_ptr d = a->get_dict(); @@ -189,7 +189,7 @@ namespace spot struct ec_algo { const char* name; - emptiness_check_ptr(*construct)(const const_tgba_ptr&, + emptiness_check_ptr(*construct)(const const_twa_ptr&, spot::option_map); unsigned int min_acc; unsigned int max_acc; @@ -225,7 +225,7 @@ namespace spot } emptiness_check_ptr - emptiness_check_instantiator::instantiate(const const_tgba_ptr& a) const + emptiness_check_instantiator::instantiate(const const_twa_ptr& a) const { return static_cast(info_)->construct(a, o_); } @@ -291,7 +291,7 @@ namespace spot ////////////////////////////////////////////////////////////////////// twa_graph_ptr - tgba_run_to_tgba(const const_tgba_ptr& a, const const_tgba_run_ptr& run) + tgba_run_to_tgba(const const_twa_ptr& a, const const_tgba_run_ptr& run) { auto d = a->get_dict(); auto res = make_twa_graph(d); diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index 912245343..104592cca 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -77,7 +77,7 @@ namespace spot class SPOT_API emptiness_check_result { public: - emptiness_check_result(const const_tgba_ptr& a, + emptiness_check_result(const const_twa_ptr& a, option_map o = option_map()) : a_(a), o_(o) { @@ -103,7 +103,7 @@ namespace spot virtual tgba_run_ptr accepting_run(); /// The automaton on which an accepting_run() was found. - const const_tgba_ptr& + const const_twa_ptr& automaton() const { return a_; @@ -126,7 +126,7 @@ namespace spot /// Notify option updates. virtual void options_updated(const option_map& old); - const_tgba_ptr a_; ///< The automaton. + const_twa_ptr a_; ///< The automaton. option_map o_; ///< The options. }; @@ -137,14 +137,14 @@ namespace spot public std::enable_shared_from_this { public: - emptiness_check(const const_tgba_ptr& a, option_map o = option_map()) + emptiness_check(const const_twa_ptr& a, option_map o = option_map()) : a_(a), o_(o) { } virtual ~emptiness_check(); /// The automaton that this emptiness-check inspects. - const const_tgba_ptr& + const const_twa_ptr& automaton() const { return a_; @@ -192,7 +192,7 @@ namespace spot virtual void options_updated(const option_map& old); protected: - const_tgba_ptr a_; ///< The automaton. + const_twa_ptr a_; ///< The automaton. option_map o_; ///< The options }; @@ -207,7 +207,7 @@ namespace spot { public: /// Actually instantiate the emptiness check, for \a a. - emptiness_check_ptr instantiate(const const_tgba_ptr& a) const; + emptiness_check_ptr instantiate(const const_twa_ptr& a) const; /// Accessor to the options. /// @{ @@ -308,7 +308,7 @@ namespace spot /// transition annotation). SPOT_API std::ostream& print_tgba_run(std::ostream& os, - const const_tgba_ptr& a, + const const_twa_ptr& a, const const_tgba_run_ptr& run); /// \brief Return an explicit_tgba corresponding to \a run (i.e. comparable @@ -316,7 +316,7 @@ namespace spot /// /// \pre \a run must correspond to an actual run of the automaton \a a. SPOT_API twa_graph_ptr - tgba_run_to_tgba(const const_tgba_ptr& a, const const_tgba_run_ptr& run); + tgba_run_to_tgba(const const_twa_ptr& a, const const_tgba_run_ptr& run); /// @} diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index bd49c2a67..04a53bd07 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -40,7 +40,7 @@ namespace spot typedef std::pair pair_state_iter; } - couvreur99_check::couvreur99_check(const const_tgba_ptr& a, option_map o) + couvreur99_check::couvreur99_check(const const_twa_ptr& a, option_map o) : emptiness_check(a, o), removed_components(0) { @@ -326,7 +326,7 @@ namespace spot } } - couvreur99_check_shy::couvreur99_check_shy(const const_tgba_ptr& a, + couvreur99_check_shy::couvreur99_check_shy(const const_twa_ptr& a, option_map o) : couvreur99_check(a, o), num(1) { @@ -607,7 +607,7 @@ namespace spot } emptiness_check_ptr - couvreur99(const const_tgba_ptr& a, option_map o) + couvreur99(const const_twa_ptr& a, option_map o) { if (o.get("shy")) return std::make_shared(a, o); diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index 4e1a3d2b0..aac415a90 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -136,7 +136,7 @@ namespace spot /// choosing a successor. Otherwise, only the successor of the /// topmost state on the DFS stack are considered. SPOT_API emptiness_check_ptr - couvreur99(const const_tgba_ptr& a, option_map options = option_map()); + couvreur99(const const_twa_ptr& a, option_map options = option_map()); #ifndef SWIG /// \brief An implementation of the Couvreur99 emptiness-check algorithm. @@ -145,7 +145,7 @@ namespace spot class SPOT_API couvreur99_check: public emptiness_check, public ec_statistics { public: - couvreur99_check(const const_tgba_ptr& a, option_map o = option_map()); + couvreur99_check(const const_twa_ptr& a, option_map o = option_map()); virtual ~couvreur99_check(); /// Check whether the automaton's language is empty. @@ -187,7 +187,7 @@ namespace spot class SPOT_API couvreur99_check_shy final: public couvreur99_check { public: - couvreur99_check_shy(const const_tgba_ptr& a, option_map o = option_map()); + couvreur99_check_shy(const const_twa_ptr& a, option_map o = option_map()); virtual ~couvreur99_check_shy(); virtual emptiness_check_result_ptr check(); diff --git a/src/tgbaalgos/gtec/status.cc b/src/tgbaalgos/gtec/status.cc index f9a8044d2..380222bc7 100644 --- a/src/tgbaalgos/gtec/status.cc +++ b/src/tgbaalgos/gtec/status.cc @@ -25,7 +25,7 @@ namespace spot { - couvreur99_check_status::couvreur99_check_status(const const_tgba_ptr& aut) + couvreur99_check_status::couvreur99_check_status(const const_twa_ptr& aut) : aut(aut) { } diff --git a/src/tgbaalgos/gtec/status.hh b/src/tgbaalgos/gtec/status.hh index 3b32b9bc6..4e277083c 100644 --- a/src/tgbaalgos/gtec/status.hh +++ b/src/tgbaalgos/gtec/status.hh @@ -36,11 +36,11 @@ namespace spot class SPOT_API couvreur99_check_status { public: - couvreur99_check_status(const const_tgba_ptr& aut); + couvreur99_check_status(const const_twa_ptr& aut); ~couvreur99_check_status(); - const_tgba_ptr aut; + const_twa_ptr aut; scc_stack root; typedef std::unordered_mapacc().num_sets() <= 1); @@ -407,7 +407,7 @@ namespace spot } // anonymous emptiness_check_ptr - explicit_gv04_check(const const_tgba_ptr& a, option_map o) + explicit_gv04_check(const const_twa_ptr& a, option_map o) { return std::make_shared(a, o); } diff --git a/src/tgbaalgos/gv04.hh b/src/tgbaalgos/gv04.hh index 6a2f8d1a1..054309f30 100644 --- a/src/tgbaalgos/gv04.hh +++ b/src/tgbaalgos/gv04.hh @@ -53,5 +53,5 @@ namespace spot } \endverbatim */ SPOT_API emptiness_check_ptr - explicit_gv04_check(const const_tgba_ptr& a, option_map o = option_map()); + explicit_gv04_check(const const_twa_ptr& a, option_map o = option_map()); } diff --git a/src/tgbaalgos/hoa.cc b/src/tgbaalgos/hoa.cc index 1854522c6..09f3ba51e 100644 --- a/src/tgbaalgos/hoa.cc +++ b/src/tgbaalgos/hoa.cc @@ -432,7 +432,7 @@ namespace spot std::ostream& hoa_reachable(std::ostream& os, - const const_tgba_ptr& aut, + const const_twa_ptr& aut, const char* opt) { diff --git a/src/tgbaalgos/hoa.hh b/src/tgbaalgos/hoa.hh index 2f7a64d92..6b82cd637 100644 --- a/src/tgbaalgos/hoa.hh +++ b/src/tgbaalgos/hoa.hh @@ -37,6 +37,6 @@ namespace spot /// single-line output. SPOT_API std::ostream& hoa_reachable(std::ostream& os, - const const_tgba_ptr& g, + const const_twa_ptr& g, const char* opt); } diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 2ea28f760..19f68abc1 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -38,7 +38,7 @@ namespace spot class lbtt_bfs : public tgba_reachable_iterator_breadth_first { public: - lbtt_bfs(const const_tgba_ptr& a, std::ostream& os, bool sba_format) + lbtt_bfs(const const_twa_ptr& a, std::ostream& os, bool sba_format) : tgba_reachable_iterator_breadth_first(a), os_(os), sba_format_(sba_format), @@ -133,7 +133,7 @@ namespace spot } std::ostream& - lbtt_reachable(std::ostream& os, const const_tgba_ptr& g, bool sba) + lbtt_reachable(std::ostream& os, const const_twa_ptr& g, bool sba) { if (!g->acc().is_generalized_buchi()) throw std::runtime_error diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh index a7bbc6724..b4c3edffe 100644 --- a/src/tgbaalgos/lbtt.hh +++ b/src/tgbaalgos/lbtt.hh @@ -35,5 +35,5 @@ namespace spot /// \param sba Assume \a g is an SBA and use LBTT's state-based /// acceptance format (similar to LBT's format). SPOT_API std::ostream& - lbtt_reachable(std::ostream& os, const const_tgba_ptr& g, bool sba = false); + lbtt_reachable(std::ostream& os, const const_twa_ptr& g, bool sba = false); } diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index 973d9d319..c732ae2e9 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -54,7 +54,7 @@ namespace spot /// /// \pre The automaton \a a must have at most one acceptance /// condition (i.e. it is a TBA). - magic_search_(const const_tgba_ptr& a, size_t size, + magic_search_(const const_twa_ptr& a, size_t size, option_map o = option_map()) : emptiness_check(a, o), h(size) @@ -584,20 +584,20 @@ namespace spot } // anonymous emptiness_check_ptr - explicit_magic_search(const const_tgba_ptr& a, option_map o) + explicit_magic_search(const const_twa_ptr& a, option_map o) { return std::make_shared>(a, 0, o); } emptiness_check_ptr - bit_state_hashing_magic_search(const const_tgba_ptr& a, + bit_state_hashing_magic_search(const const_twa_ptr& a, size_t size, option_map o) { return std::make_shared>(a, size, o); } emptiness_check_ptr - magic_search(const const_tgba_ptr& a, option_map o) + magic_search(const const_twa_ptr& a, option_map o) { size_t size = o.get("bsh"); if (size) diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh index 63bf43e48..616e98ec0 100644 --- a/src/tgbaalgos/magic.hh +++ b/src/tgbaalgos/magic.hh @@ -96,7 +96,7 @@ namespace spot /// \bug The name is misleading. Magic-search is the algorithm /// from \c godefroid.93.pstv, not \c courcoubetis.92.fmsd. SPOT_API emptiness_check_ptr - explicit_magic_search(const const_tgba_ptr& a, + explicit_magic_search(const const_twa_ptr& a, option_map o = option_map()); /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. @@ -127,7 +127,7 @@ namespace spot /// \sa spot::explicit_magic_search /// SPOT_API emptiness_check_ptr - bit_state_hashing_magic_search(const const_tgba_ptr& a, size_t size, + bit_state_hashing_magic_search(const const_twa_ptr& a, size_t size, option_map o = option_map()); /// \brief Wrapper for the two magic_search implementations. @@ -137,7 +137,7 @@ namespace spot /// in the \c option_map. If \c "bsh" is set and non null, its value /// is used as the size of the hash map. SPOT_API emptiness_check_ptr - magic_search(const const_tgba_ptr& a, option_map o = option_map()); + magic_search(const const_twa_ptr& a, option_map o = option_map()); /// @} } diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 4e17b76f8..87316583b 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -60,7 +60,7 @@ namespace spot { static std::ostream& dump_hash_set(const hash_set* hs, - const const_tgba_ptr& aut, + const const_twa_ptr& aut, std::ostream& out) { out << '{'; @@ -75,7 +75,7 @@ namespace spot } static std::string - format_hash_set(const hash_set* hs, const_tgba_ptr aut) + format_hash_set(const hash_set* hs, const_twa_ptr aut) { std::ostringstream s; dump_hash_set(hs, aut, s); @@ -84,7 +84,7 @@ namespace spot } // Find all states of an automaton. - void build_state_set(const const_tgba_ptr& a, hash_set* seen) + void build_state_set(const const_twa_ptr& a, hash_set* seen) { std::queue tovisit; // Perform breadth-first traversal. @@ -114,7 +114,7 @@ namespace spot // From the base automaton and the list of sets, build the minimal // resulting automaton - twa_graph_ptr build_result(const const_tgba_ptr& a, + twa_graph_ptr build_result(const const_twa_ptr& a, std::list& sets, hash_set* final) { @@ -182,7 +182,7 @@ namespace spot struct wdba_search_acc_loop : public bfs_steps { - wdba_search_acc_loop(const const_tgba_ptr& det_a, + wdba_search_acc_loop(const const_twa_ptr& det_a, unsigned scc_n, scc_info& sm, power_map& pm, const state* dest) : bfs_steps(det_a), scc_n(scc_n), sm(sm), pm(pm), dest(dest) diff --git a/src/tgbaalgos/ndfs_result.hxx b/src/tgbaalgos/ndfs_result.hxx index 856de2459..153dbfaa2 100644 --- a/src/tgbaalgos/ndfs_result.hxx +++ b/src/tgbaalgos/ndfs_result.hxx @@ -229,7 +229,7 @@ namespace spot typedef std::unordered_set state_set; - void clean(const const_tgba_ptr& a, stack_type& st1, + void clean(const const_twa_ptr& a, stack_type& st1, state_set& seen, state_set& dead) { while (!st1.empty()) @@ -372,7 +372,7 @@ namespace spot { public: test_path(ars_statistics* ars, - const const_tgba_ptr& a, const state* t, + const const_twa_ptr& a, const state* t, const state_set& d, const heap& h) : bfs_steps(a), ars(ars), target(t), dead(d), h(h) { @@ -467,7 +467,7 @@ namespace spot { public: min_path(ars_statistics* ars, - const const_tgba_ptr& a, + const const_twa_ptr& a, const m_source_trans& target, const heap& h) : bfs_steps(a), ars(ars), target(target), h(h) { diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 017c7e80d..48fd50825 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -201,7 +201,7 @@ namespace spot } // anonymous namespace std::ostream& - never_claim_reachable(std::ostream& os, const const_tgba_ptr& g, + never_claim_reachable(std::ostream& os, const const_twa_ptr& g, const char* options) { if (!(g->acc().is_buchi() || g->acc().is_true())) diff --git a/src/tgbaalgos/neverclaim.hh b/src/tgbaalgos/neverclaim.hh index 98a6b9918..7cbc8e71b 100644 --- a/src/tgbaalgos/neverclaim.hh +++ b/src/tgbaalgos/neverclaim.hh @@ -40,6 +40,6 @@ namespace spot /// \param opt a string of option: 'c' to comment each state SPOT_API std::ostream& never_claim_reachable(std::ostream& os, - const const_tgba_ptr& g, + const const_twa_ptr& g, const char* opt = nullptr); } diff --git a/src/tgbaalgos/projrun.cc b/src/tgbaalgos/projrun.cc index 79bf35f4b..7bfa8aedd 100644 --- a/src/tgbaalgos/projrun.cc +++ b/src/tgbaalgos/projrun.cc @@ -28,8 +28,8 @@ namespace spot { tgba_run_ptr - project_tgba_run(const const_tgba_ptr& a_run, - const const_tgba_ptr& a_proj, + project_tgba_run(const const_twa_ptr& a_run, + const const_twa_ptr& a_proj, const const_tgba_run_ptr& run) { auto res = std::make_shared(); diff --git a/src/tgbaalgos/projrun.hh b/src/tgbaalgos/projrun.hh index 087c07f27..6afa2ddf2 100644 --- a/src/tgbaalgos/projrun.hh +++ b/src/tgbaalgos/projrun.hh @@ -42,7 +42,7 @@ namespace spot /// \param a_proj the automata on which to project the run /// \return true iff the run could be completed SPOT_API tgba_run_ptr - project_tgba_run(const const_tgba_ptr& a_run, - const const_tgba_ptr& a_proj, + project_tgba_run(const const_twa_ptr& a_run, + const const_twa_ptr& a_proj, const const_tgba_run_ptr& run); } diff --git a/src/tgbaalgos/reachiter.cc b/src/tgbaalgos/reachiter.cc index 2c625b584..2c05ce603 100644 --- a/src/tgbaalgos/reachiter.cc +++ b/src/tgbaalgos/reachiter.cc @@ -28,7 +28,7 @@ namespace spot // tgba_reachable_iterator ////////////////////////////////////////////////////////////////////// - tgba_reachable_iterator::tgba_reachable_iterator(const const_tgba_ptr& a) + tgba_reachable_iterator::tgba_reachable_iterator(const const_twa_ptr& a) : aut_(a) { } @@ -122,7 +122,7 @@ namespace spot ////////////////////////////////////////////////////////////////////// tgba_reachable_iterator_breadth_first:: - tgba_reachable_iterator_breadth_first(const const_tgba_ptr& a) + tgba_reachable_iterator_breadth_first(const const_twa_ptr& a) : tgba_reachable_iterator(a) { } @@ -147,7 +147,7 @@ namespace spot ////////////////////////////////////////////////////////////////////// tgba_reachable_iterator_depth_first:: - tgba_reachable_iterator_depth_first(const const_tgba_ptr& a) + tgba_reachable_iterator_depth_first(const const_twa_ptr& a) : aut_(a) { } @@ -273,7 +273,7 @@ namespace spot tgba_reachable_iterator_depth_first_stack:: - tgba_reachable_iterator_depth_first_stack(const const_tgba_ptr& a) + tgba_reachable_iterator_depth_first_stack(const const_twa_ptr& a) : tgba_reachable_iterator_depth_first(a) { } diff --git a/src/tgbaalgos/reachiter.hh b/src/tgbaalgos/reachiter.hh index 10cfe7841..7bde6d9e9 100644 --- a/src/tgbaalgos/reachiter.hh +++ b/src/tgbaalgos/reachiter.hh @@ -34,7 +34,7 @@ namespace spot class SPOT_API tgba_reachable_iterator { public: - tgba_reachable_iterator(const const_tgba_ptr& a); + tgba_reachable_iterator(const const_twa_ptr& a); virtual ~tgba_reachable_iterator(); /// \brief Iterate over all reachable states of a spot::tgba. @@ -88,7 +88,7 @@ namespace spot const twa_succ_iterator* si); protected: - const_tgba_ptr aut_; ///< The spot::tgba to explore. + const_twa_ptr aut_; ///< The spot::tgba to explore. typedef std::unordered_map seen_map; @@ -102,7 +102,7 @@ namespace spot public tgba_reachable_iterator { public: - tgba_reachable_iterator_breadth_first(const const_tgba_ptr& a); + tgba_reachable_iterator_breadth_first(const const_twa_ptr& a); virtual void add_state(const state* s); virtual const state* next_state(); @@ -116,7 +116,7 @@ namespace spot class SPOT_API tgba_reachable_iterator_depth_first { public: - tgba_reachable_iterator_depth_first(const const_tgba_ptr& a); + tgba_reachable_iterator_depth_first(const const_twa_ptr& a); virtual ~tgba_reachable_iterator_depth_first(); /// \brief Iterate over all reachable states of a spot::tgba. @@ -158,7 +158,7 @@ namespace spot const twa_succ_iterator* si); protected: - const_tgba_ptr aut_; ///< The spot::tgba to explore. + const_twa_ptr aut_; ///< The spot::tgba to explore. typedef std::unordered_map seen_map; @@ -186,7 +186,7 @@ namespace spot : public tgba_reachable_iterator_depth_first { public: - tgba_reachable_iterator_depth_first_stack(const const_tgba_ptr& a); + tgba_reachable_iterator_depth_first_stack(const const_twa_ptr& a); /// \brief Whether state sn is on the DFS stack. /// /// Note the destination state of a transition is only pushed to diff --git a/src/tgbaalgos/reducerun.cc b/src/tgbaalgos/reducerun.cc index 46b6ac297..9f3f6e6af 100644 --- a/src/tgbaalgos/reducerun.cc +++ b/src/tgbaalgos/reducerun.cc @@ -33,7 +33,7 @@ namespace spot class shortest_path: public bfs_steps { public: - shortest_path(const const_tgba_ptr& a) + shortest_path(const const_twa_ptr& a) : bfs_steps(a), target(0) { } @@ -88,7 +88,7 @@ namespace spot } tgba_run_ptr - reduce_run(const const_tgba_ptr& a, const const_tgba_run_ptr& org) + reduce_run(const const_twa_ptr& a, const const_tgba_run_ptr& org) { auto res = std::make_shared(); state_set ss; diff --git a/src/tgbaalgos/reducerun.hh b/src/tgbaalgos/reducerun.hh index aaafe3df7..62dacfa45 100644 --- a/src/tgbaalgos/reducerun.hh +++ b/src/tgbaalgos/reducerun.hh @@ -34,5 +34,5 @@ namespace spot /// Return a run which is accepting for \a a and that is no longer /// than \a org. SPOT_API tgba_run_ptr - reduce_run(const const_tgba_ptr& a, const const_tgba_run_ptr& org); + reduce_run(const const_twa_ptr& a, const const_tgba_run_ptr& org); } diff --git a/src/tgbaalgos/replayrun.cc b/src/tgbaalgos/replayrun.cc index 592f017a1..53ab96e8e 100644 --- a/src/tgbaalgos/replayrun.cc +++ b/src/tgbaalgos/replayrun.cc @@ -33,7 +33,7 @@ namespace spot { void print_annotation(std::ostream& os, - const const_tgba_ptr& a, + const const_twa_ptr& a, const twa_succ_iterator* i) { std::string s = a->transition_annotation(i); @@ -44,7 +44,7 @@ namespace spot } bool - replay_tgba_run(std::ostream& os, const const_tgba_ptr& a, + replay_tgba_run(std::ostream& os, const const_twa_ptr& a, const const_tgba_run_ptr& run, bool debug) { const state* s = a->get_init_state(); diff --git a/src/tgbaalgos/replayrun.hh b/src/tgbaalgos/replayrun.hh index 1b4e65b8c..44feee936 100644 --- a/src/tgbaalgos/replayrun.hh +++ b/src/tgbaalgos/replayrun.hh @@ -48,7 +48,7 @@ namespace spot /// \return true iff the run could be completed SPOT_API bool replay_tgba_run(std::ostream& os, - const const_tgba_ptr& a, + const const_twa_ptr& a, const const_tgba_run_ptr& run, bool debug = false); } diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index a10aa4f65..56b11c2a7 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -27,7 +27,7 @@ namespace spot { - scc_map::scc_map(const const_tgba_ptr& aut) + scc_map::scc_map(const const_twa_ptr& aut) : aut_(aut) { } @@ -76,7 +76,7 @@ namespace spot return aut_->acc().accepting(acc_set_of(n)); } - const_tgba_ptr + const_twa_ptr scc_map::get_aut() const { return aut_; @@ -443,7 +443,7 @@ namespace spot } std::ostream& - dump_scc_dot(const const_tgba_ptr& a, std::ostream& out, bool verbose) + dump_scc_dot(const const_twa_ptr& a, std::ostream& out, bool verbose) { scc_map m(a); m.build_map(); diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index 040db759b..368a33fe3 100644 --- a/src/tgbaalgos/scc.hh +++ b/src/tgbaalgos/scc.hh @@ -41,7 +41,7 @@ namespace spot /// /// This will note compute the map initially. You should call /// build_map() to do so. - scc_map(const const_tgba_ptr& aut); + scc_map(const const_twa_ptr& aut); ~scc_map(); @@ -49,7 +49,7 @@ namespace spot void build_map(); /// Get the automaton for which the map has been constructed. - const_tgba_ptr get_aut() const; + const_twa_ptr get_aut() const; /// \brief Get the number of SCC in the automaton. /// @@ -171,7 +171,7 @@ namespace spot std::set useful_acc; }; - const_tgba_ptr aut_; // Automata to decompose. + const_twa_ptr aut_; // Automata to decompose. typedef std::list stack_type; stack_type root_; // Stack of SCC roots. std::stack arc_acc_; // A stack of acceptance conditions @@ -203,7 +203,7 @@ namespace spot }; SPOT_API std::ostream& - dump_scc_dot(const const_tgba_ptr& a, + dump_scc_dot(const const_twa_ptr& a, std::ostream& out, bool verbose = false); SPOT_API std::ostream& dump_scc_dot(const scc_map& m, std::ostream& out, bool verbose = false); diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index 107a8239f..07e90a918 100644 --- a/src/tgbaalgos/se05.cc +++ b/src/tgbaalgos/se05.cc @@ -54,7 +54,7 @@ namespace spot /// /// \pre The automaton \a a must have at most one acceptance /// condition (i.e. it is a TBA). - se05_search(const const_tgba_ptr a, size_t size, + se05_search(const const_twa_ptr a, size_t size, option_map o = option_map()) : emptiness_check(a, o), h(size) @@ -676,20 +676,20 @@ namespace spot } // anonymous emptiness_check_ptr - explicit_se05_search(const const_tgba_ptr& a, option_map o) + explicit_se05_search(const const_twa_ptr& a, option_map o) { return std::make_shared>(a, 0, o); } emptiness_check_ptr - bit_state_hashing_se05_search(const const_tgba_ptr& a, + bit_state_hashing_se05_search(const const_twa_ptr& a, size_t size, option_map o) { return std::make_shared>(a, size, o); } emptiness_check_ptr - se05(const const_tgba_ptr& a, option_map o) + se05(const const_twa_ptr& a, option_map o) { size_t size = o.get("bsh"); if (size) diff --git a/src/tgbaalgos/se05.hh b/src/tgbaalgos/se05.hh index ad8c2b9ce..90e3e15b9 100644 --- a/src/tgbaalgos/se05.hh +++ b/src/tgbaalgos/se05.hh @@ -101,7 +101,7 @@ namespace spot /// \sa spot::explicit_magic_search /// SPOT_API emptiness_check_ptr - explicit_se05_search(const const_tgba_ptr& a, option_map o = option_map()); + explicit_se05_search(const const_twa_ptr& a, option_map o = option_map()); /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. /// @@ -131,7 +131,7 @@ namespace spot /// \sa spot::explicit_se05_search /// SPOT_API emptiness_check_ptr - bit_state_hashing_se05_search(const const_tgba_ptr& a, size_t size, + bit_state_hashing_se05_search(const const_twa_ptr& a, size_t size, option_map o = option_map()); @@ -142,7 +142,7 @@ namespace spot /// in the \c option_map. If \c "bsh" is set and non null, its value /// is used as the size of the hash map. SPOT_API emptiness_check_ptr - se05(const const_tgba_ptr& a, option_map o); + se05(const const_twa_ptr& a, option_map o); /// @} } diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index 2ea5ed343..ea14d3549 100644 --- a/src/tgbaalgos/stats.cc +++ b/src/tgbaalgos/stats.cc @@ -36,7 +36,7 @@ namespace spot class stats_bfs: public tgba_reachable_iterator_breadth_first { public: - stats_bfs(const const_tgba_ptr& a, tgba_statistics& s) + stats_bfs(const const_twa_ptr& a, tgba_statistics& s) : tgba_reachable_iterator_breadth_first(a), s_(s) { } @@ -61,7 +61,7 @@ namespace spot class sub_stats_bfs: public stats_bfs { public: - sub_stats_bfs(const const_tgba_ptr& a, tgba_sub_statistics& s) + sub_stats_bfs(const const_twa_ptr& a, tgba_sub_statistics& s) : stats_bfs(a, s), s_(s), seen_(bddtrue) { } @@ -118,7 +118,7 @@ namespace spot } tgba_statistics - stats_reachable(const const_tgba_ptr& g) + stats_reachable(const const_twa_ptr& g) { tgba_statistics s; stats_bfs d(g, s); @@ -127,7 +127,7 @@ namespace spot } tgba_sub_statistics - sub_stats_reachable(const const_tgba_ptr& g) + sub_stats_reachable(const const_twa_ptr& g) { tgba_sub_statistics s; sub_stats_bfs d(g, s); diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh index 1eece70d5..dbee7f097 100644 --- a/src/tgbaalgos/stats.hh +++ b/src/tgbaalgos/stats.hh @@ -50,9 +50,9 @@ namespace spot }; /// \brief Compute statistics for an automaton. - SPOT_API tgba_statistics stats_reachable(const const_tgba_ptr& g); + SPOT_API tgba_statistics stats_reachable(const const_twa_ptr& g); /// \brief Compute subended statistics for an automaton. - SPOT_API tgba_sub_statistics sub_stats_reachable(const const_tgba_ptr& g); + SPOT_API tgba_sub_statistics sub_stats_reachable(const const_twa_ptr& g); class SPOT_API printable_formula: public printable_value diff --git a/src/tgbaalgos/stutter.cc b/src/tgbaalgos/stutter.cc index 439c4d196..dcccd3c03 100644 --- a/src/tgbaalgos/stutter.cc +++ b/src/tgbaalgos/stutter.cc @@ -206,7 +206,7 @@ namespace spot class tgbasl final : public twa { public: - tgbasl(const const_tgba_ptr& a, bdd atomic_propositions) + tgbasl(const const_twa_ptr& a, bdd atomic_propositions) : twa(a->get_dict()), a_(a), aps_(atomic_propositions) { get_dict()->register_all_propositions_of(&a_, this); @@ -249,13 +249,13 @@ namespace spot } private: - const_tgba_ptr a_; + const_twa_ptr a_; bdd aps_; }; typedef std::shared_ptr tgbasl_ptr; - inline tgbasl_ptr make_tgbasl(const const_tgba_ptr& aut, bdd ap) + inline tgbasl_ptr make_tgbasl(const const_twa_ptr& aut, bdd ap) { return std::make_shared(aut, ap); } diff --git a/src/tgbaalgos/tau03.cc b/src/tgbaalgos/tau03.cc index 4d3bc601d..593720355 100644 --- a/src/tgbaalgos/tau03.cc +++ b/src/tgbaalgos/tau03.cc @@ -54,7 +54,7 @@ namespace spot { public: /// \brief Initialize the search algorithm on the automaton \a a - tau03_search(const const_tgba_ptr a, size_t size, option_map o) + tau03_search(const const_twa_ptr a, size_t size, option_map o) : emptiness_check(a, o), h(size) { @@ -376,7 +376,7 @@ namespace spot } // anonymous emptiness_check_ptr - explicit_tau03_search(const const_tgba_ptr& a, option_map o) + explicit_tau03_search(const const_twa_ptr& a, option_map o) { return std::make_shared>(a, 0, o); } diff --git a/src/tgbaalgos/tau03.hh b/src/tgbaalgos/tau03.hh index 951edb189..dcb8f9396 100644 --- a/src/tgbaalgos/tau03.hh +++ b/src/tgbaalgos/tau03.hh @@ -95,7 +95,7 @@ namespace spot \endverbatim */ /// SPOT_API emptiness_check_ptr - explicit_tau03_search(const const_tgba_ptr& a, option_map o = option_map()); + explicit_tau03_search(const const_twa_ptr& a, option_map o = option_map()); /// @} } diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc index 4f98a5367..58d14cbea 100644 --- a/src/tgbaalgos/tau03opt.cc +++ b/src/tgbaalgos/tau03opt.cc @@ -65,7 +65,7 @@ namespace spot { public: /// \brief Initialize the search algorithm on the automaton \a a - tau03_opt_search(const const_tgba_ptr& a, size_t size, option_map o) + tau03_opt_search(const const_twa_ptr& a, size_t size, option_map o) : emptiness_check(a, o), current_weight(a->acc()), h(size), @@ -562,7 +562,7 @@ namespace spot } // anonymous emptiness_check_ptr - explicit_tau03_opt_search(const const_tgba_ptr& a, option_map o) + explicit_tau03_opt_search(const const_twa_ptr& a, option_map o) { return std::make_shared>(a, diff --git a/src/tgbaalgos/tau03opt.hh b/src/tgbaalgos/tau03opt.hh index 7d7028e01..77c3300ed 100644 --- a/src/tgbaalgos/tau03opt.hh +++ b/src/tgbaalgos/tau03opt.hh @@ -97,7 +97,7 @@ namespace spot /// state of this stack. /// SPOT_API emptiness_check_ptr - explicit_tau03_opt_search(const const_tgba_ptr& a, + explicit_tau03_opt_search(const const_twa_ptr& a, option_map o = option_map()); /// @} diff --git a/src/tgbatest/checkta.cc b/src/tgbatest/checkta.cc index e76a05979..4cc2ebc35 100644 --- a/src/tgbatest/checkta.cc +++ b/src/tgbatest/checkta.cc @@ -51,7 +51,7 @@ void stats(std::string title, const spot::ta_ptr& ta) << std::setw(6) << s.acceptance_states << '\n'; } -void stats(std::string title, const spot::tgba_ptr& tg) +void stats(std::string title, const spot::twa_ptr& tg) { auto s = stats_reachable(tg); diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index 4c43ca3fd..1705d7bf3 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -127,7 +127,7 @@ int main(int argc, char* argv[]) return 2; spot::twa_graph_ptr a = h->aut; - spot::tgba_ptr complement = 0; + spot::twa_ptr complement = 0; complement = spot::make_safra_complement(a); @@ -155,7 +155,7 @@ int main(int argc, char* argv[]) return 2; auto a = spot::ltl_to_tgba_fm(f1, dict); - spot::tgba_ptr complement = 0; + spot::twa_ptr complement = 0; complement = spot::make_safra_complement(a); spot::dotty_reachable(std::cout, complement); diff --git a/src/tgbatest/emptchk.cc b/src/tgbatest/emptchk.cc index 8b53f261d..fc2ae00d8 100644 --- a/src/tgbatest/emptchk.cc +++ b/src/tgbatest/emptchk.cc @@ -98,7 +98,7 @@ main(int argc, char** argv) auto d = spot::make_bdd_dict(); // Build many different automata from this formula. - spot::const_tgba_ptr aut[4]; + spot::const_twa_ptr aut[4]; { auto a = spot::ltl_to_taa(f, d); aut[0] = a; diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 5b4c5b9f4..4bf7b7ea4 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -309,7 +309,7 @@ to_int(const char* s) return res; } -spot::twa_graph_ptr ensure_digraph(const spot::tgba_ptr& a) +spot::twa_graph_ptr ensure_digraph(const spot::twa_ptr& a) { auto aa = std::dynamic_pointer_cast(a); if (aa) @@ -371,7 +371,7 @@ checked_main(int argc, char** argv) const char* hoa_opt = nullptr; auto& env = spot::ltl::default_environment::instance(); spot::ltl::atomic_prop_set* unobservables = 0; - spot::tgba_ptr system_aut = 0; + spot::twa_ptr system_aut = 0; auto dict = spot::make_bdd_dict(); spot::timer_map tm; bool use_timer = false; @@ -960,7 +960,7 @@ checked_main(int argc, char** argv) if (f || from_file) { - spot::tgba_ptr a = 0; + spot::twa_ptr a = 0; bool assume_sba = false; if (from_file) diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 8da2a67fe..16356eb1e 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -376,7 +376,7 @@ empty_hoa_parse_error_list() } spot::twa_graph_ptr -ensure_digraph(const spot::tgba_ptr& a) +ensure_digraph(const spot::twa_ptr& a) { auto aa = std::dynamic_pointer_cast(a); if (aa) -- GitLab