diff --git a/src/ta/tgtaexplicit.cc b/src/ta/tgtaexplicit.cc index 102b7aaac..1cf68c211 100644 --- a/src/ta/tgtaexplicit.cc +++ b/src/ta/tgtaexplicit.cc @@ -33,66 +33,67 @@ namespace spot tgta_explicit::tgta_explicit(const tgba* tgba, bdd all_acceptance_conditions, state_ta_explicit* artificial_initial_state, bool own_tgba) : - ta_explicit(tgba, all_acceptance_conditions, artificial_initial_state, own_tgba) + ta_(tgba, all_acceptance_conditions, artificial_initial_state, own_tgba) { } state* tgta_explicit::get_init_state() const { - return ta_explicit::get_artificial_initial_state(); + return ta_.get_artificial_initial_state(); } tgba_succ_iterator* tgta_explicit::succ_iter(const spot::state* state, const spot::state*, - const tgba*) const + const tgba*) const { - return ta_explicit::succ_iter(state); + return ta_.succ_iter(state); } bdd tgta_explicit::compute_support_conditions(const spot::state* in) const { - return get_tgba()->support_conditions( - ((const state_ta_explicit*) in)->get_tgba_state()); + const state_ta_explicit* s = down_cast(in); + assert(s); + return ta_.get_tgba()->support_conditions(s->get_tgba_state()); } bdd tgta_explicit::compute_support_variables(const spot::state* in) const { - return get_tgba()->support_variables( - ((const state_ta_explicit*) in)->get_tgba_state()); + const state_ta_explicit* s = down_cast(in); + assert(s); + return ta_.get_tgba()->support_variables(s->get_tgba_state()); } bdd_dict* tgta_explicit::get_dict() const { - return ta_explicit::get_dict(); + return ta_.get_dict(); } bdd tgta_explicit::all_acceptance_conditions() const { - - return ta_explicit::all_acceptance_conditions(); + return ta_.all_acceptance_conditions(); } bdd tgta_explicit::neg_acceptance_conditions() const { - return get_tgba()->neg_acceptance_conditions(); + return ta_.get_tgba()->neg_acceptance_conditions(); } std::string tgta_explicit::format_state(const spot::state* s) const { - return ta_explicit::format_state(s); + return ta_.format_state(s); } spot::tgba_succ_iterator* tgta_explicit::succ_iter_by_changeset(const spot::state* s, bdd chngset) const { - return ta_explicit::succ_iter(s, chngset); + return ta_.succ_iter(s, chngset); } } diff --git a/src/ta/tgtaexplicit.hh b/src/ta/tgtaexplicit.hh index 86a9a5f6b..39ed46230 100644 --- a/src/ta/tgtaexplicit.hh +++ b/src/ta/tgtaexplicit.hh @@ -36,7 +36,7 @@ namespace spot /// Explicit representation of a spot::tgta. /// \ingroup ta_representation - class tgta_explicit : public tgta, public ta_explicit + class tgta_explicit : public tgta { public: tgta_explicit(const tgba* tgba, bdd all_acceptance_conditions, @@ -44,30 +44,30 @@ namespace spot bool own_tgba = false); // tgba interface - virtual spot::state* - get_init_state() const; + virtual spot::state* get_init_state() const; + virtual tgba_succ_iterator* succ_iter(const spot::state* local_state, const spot::state* global_state = 0, const tgba* global_automaton = 0) const; + virtual bdd_dict* get_dict() const; - virtual bdd - all_acceptance_conditions() const; - virtual bdd - neg_acceptance_conditions() const; + const ta_explicit* get_ta() const { return &ta_; } + ta_explicit* get_ta() { return &ta_; } - virtual std::string - format_state(const spot::state* s) const; + virtual bdd all_acceptance_conditions() const; + virtual bdd neg_acceptance_conditions() const; + + virtual std::string format_state(const spot::state* s) const; virtual tgba_succ_iterator* succ_iter_by_changeset(const spot::state* s, bdd change_set) const; protected: - virtual bdd - compute_support_conditions(const spot::state* state) const; - virtual bdd - compute_support_variables(const spot::state* state) const; + virtual bdd compute_support_conditions(const spot::state* state) const; + virtual bdd compute_support_variables(const spot::state* state) const; + ta_explicit ta_; }; } diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index 7de54cf76..83eaba3f8 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -514,13 +514,12 @@ namespace spot std::list::iterator itdone; for (itdone = partition.begin(); itdone != partition.end(); ++itdone) delete *itdone; - //delete ta_; return res; } - tgta* - minimize_tgta(const tgta* tgta_) + tgta_explicit* + minimize_tgta(const tgta_explicit* tgta_) { tgba_explicit_number* tgba = new tgba_explicit_number(tgta_->get_dict()); @@ -528,19 +527,17 @@ namespace spot tgta_explicit* res = new tgta_explicit(tgba, tgta_->all_acceptance_conditions(), 0, /* own_tgba = */ true); - //TODO copier le tgta_ dans un tgta_explicit au lieu de faire un cast... - const ta_explicit* tgta = dynamic_cast (tgta_); + const ta_explicit* ta = tgta_->get_ta(); - partition_t partition = build_partition(tgta); + partition_t partition = build_partition(ta); // Build the minimal tgta automaton. - build_result(tgta, partition, tgba, res); + build_result(ta, partition, tgba, res->get_ta()); // Free all the allocated memory. std::list::iterator itdone; for (itdone = partition.begin(); itdone != partition.end(); ++itdone) delete *itdone; - //delete ta_; return res; } diff --git a/src/taalgos/minimize.hh b/src/taalgos/minimize.hh index 793db96cd..a4c68a912 100644 --- a/src/taalgos/minimize.hh +++ b/src/taalgos/minimize.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// DĂ©veloppement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -23,7 +24,7 @@ # include "ta/ta.hh" # include "ta/tgta.hh" -# include "ta/taexplicit.hh" +# include "ta/tgtaexplicit.hh" namespace spot { @@ -71,8 +72,8 @@ namespace spot /// the acceptance conditions of the outgoing transitions. /// /// \param tgta_ the TGTA automaton to convert into a simplified TGTA - tgta* - minimize_tgta(const tgta* tgta_); + tgta_explicit* + minimize_tgta(const tgta_explicit* tgta_); /// @} } diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index 847b0c2b3..4a8ff3d1e 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -621,28 +621,30 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata, // build a Generalized TA automaton involving a single_pass_emptiness_check // (without an artificial livelock state): - build_ta(tgta, atomic_propositions_set_, false, true, false); + ta_explicit* ta = tgta->get_ta(); + build_ta(ta, atomic_propositions_set_, false, true, false); - trace - << "***tgba_to_tgbta: POST build_ta***" << std::endl; + trace << "***tgba_to_tgbta: POST build_ta***" << std::endl; // adapt a ta automata to build tgta automata : - ta::states_set_t states_set = tgta->get_states_set(); + ta::states_set_t states_set = ta->get_states_set(); ta::states_set_t::iterator it; - tgba_succ_iterator* initial_states_iter = tgta->succ_iter( - tgta->get_artificial_initial_state()); + tgba_succ_iterator* initial_states_iter = + ta->succ_iter(ta->get_artificial_initial_state()); initial_states_iter->first(); if (initial_states_iter->done()) - return tgta; - bdd first_state_condition = (initial_states_iter)->current_condition(); + { + delete initial_states_iter; + return tgta; + } + bdd first_state_condition = initial_states_iter->current_condition(); delete initial_states_iter; bdd bdd_stutering_transition = bdd_setxor(first_state_condition, - first_state_condition); + first_state_condition); for (it = states_set.begin(); it != states_set.end(); it++) { - state_ta_explicit* state = static_cast (*it); state_ta_explicit::transitions* trans = state->get_transitions(); @@ -652,21 +654,18 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata, bool trans_empty = (trans == 0 || trans->empty()); if (trans_empty || state->is_accepting_state()) { - tgta->create_transition(state, bdd_stutering_transition, - tgta->all_acceptance_conditions(), state); + ta->create_transition(state, bdd_stutering_transition, + ta->all_acceptance_conditions(), state); } } - if (state->compare(tgta->get_artificial_initial_state())) - tgta->create_transition(state, bdd_stutering_transition, bddfalse, - state); + if (state->compare(ta->get_artificial_initial_state())) + ta->create_transition(state, bdd_stutering_transition, bddfalse, state); state->set_livelock_accepting_state(false); state->set_accepting_state(false); - trace - << "***tgba_to_tgbta: POST create_transition ***" << std::endl; - + trace << "***tgba_to_tgbta: POST create_transition ***" << std::endl; } return tgta; diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 5ac0de8dc..4858fe514 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1153,7 +1153,7 @@ main(int argc, char** argv) } if (tgta_opt) { - spot::tgta* tgta = tgba_to_tgta(a, atomic_props_set_bdd); + spot::tgta_explicit* tgta = tgba_to_tgta(a, atomic_props_set_bdd); if (opt_bisim_ta) { tm.start("TA bisimulation"); diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index fd0b7b872..6588f2aa1 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -289,8 +289,8 @@ def render_automaton(automaton, dont_run_dot, issba, deco = None): dotsrc = spot.ostringstream() if isinstance(automaton, spot.ta): # TA/GTA spot.dotty_reachable(dotsrc, automaton) - elif hasattr(automaton, 'as_ta'): # TGTA - spot.dotty_reachable(dotsrc, automaton.as_ta()) + elif hasattr(automaton, 'get_ta'): # TGTA + spot.dotty_reachable(dotsrc, automaton.get_ta()) else: # TGBA spot.dotty_reachable(dotsrc, automaton, issba, deco) render_dot_maybe(dotsrc.str(), dont_run_dot) diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 961f63132..83a9b6cc4 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -317,14 +317,6 @@ using namespace spot; } -%extend spot::tgta_explicit { - const spot::ta* - as_ta(const spot::tgta_explicit* t) - { - return dynamic_cast(t); - } -} - %nodefaultctor std::ostream; namespace std { class ostream {};