diff --git a/NEWS b/NEWS index f0d22175d..79b66274a 100644 --- a/NEWS +++ b/NEWS @@ -92,6 +92,10 @@ New in spot 2.4.0.dev (not yet released) compute respectively the intersection and the union of two automata with parity acceptance condition and keep the parity acceptance condition. + - The new function spot::remove_univ_otf() removes universal + transitions on the fly from an alternating Büchi automaton + using Miyano and Hayashi's breakpoint algorithm. + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/python/spot/impl.i b/python/spot/impl.i index 4589d114b..2df195064 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -63,6 +63,7 @@ %shared_ptr(spot::taa_tgba_formula) %shared_ptr(spot::twa_run) %shared_ptr(spot::twa_word) +%shared_ptr(spot::twa_univ_remover) %shared_ptr(spot::emptiness_check_result) %shared_ptr(spot::emptiness_check) %shared_ptr(spot::emptiness_check_instantiator) diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index 14c5943b0..89d8f26fd 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -487,4 +487,237 @@ namespace spot return ar.run(named_states); } + + // On-the-fly alternating Büchi automaton to nondeterministic Büchi automaton + // using the breakpoint construction. + + univ_remover_state::univ_remover_state(const std::set& states) + : is_reset_(false) + { + is_reset_ = std::all_of(states.begin(), states.end(), + [] (unsigned s) { return int(s) < 0; }); + // When all states are marked (i.e. Q0 is empty), the state is in reset + // mode, meaning that it is an accepting state. + // The states can immediately be unmarked, since the acceptance mark is + // held by the incoming transition. + if (is_reset_) + for (unsigned s : states) + states_.insert(~s); + else + states_ = states; + } + + int univ_remover_state::compare(const state* other) const + { + const auto o = down_cast(other); + assert(o); + if (states_ < o->states()) + return -1; + if (states_ > o->states()) + return 1; + return 0; + } + + size_t univ_remover_state::hash() const + { + size_t hash = 0; + for (unsigned s : states_) + hash ^= wang32_hash(s); + return hash; + } + + state* univ_remover_state::clone() const + { + return new univ_remover_state(*this); + } + + const std::set& univ_remover_state::states() const + { + return states_; + } + + bool univ_remover_state::is_reset() const + { + return is_reset_; + } + + class univ_remover_succ_iterator : public twa_succ_iterator + { + private: + bdd transitions_; + bdd all_states_; + bdd ap_; + bdd all_letters_; + bdd transition_; + minato_isop isop_; + const std::map& var_to_state_; + univ_remover_state* dst_; + + public: + univ_remover_succ_iterator(const_twa_graph_ptr aut, + const univ_remover_state* state, + const std::vector& state_to_var, + const std::map& var_to_state, + bdd all_states) + : transitions_(bddtrue), all_states_(all_states), transition_(bddfalse), + isop_(bddfalse), var_to_state_(var_to_state) + { + // Build the bdd transitions_, from which we extract the successors. + for (unsigned s : state->states()) + { + bdd state_bdd = bddfalse; + bool marked = (int)s < 0; + if (marked) + s = ~s; + for (const auto& e : aut->out(s)) + { + bdd univ_bdd = bddtrue; + for (const auto& d : aut->univ_dests(e.dst)) + univ_bdd &= bdd_ithvar(state_to_var[d] + (marked || e.acc)); + state_bdd |= e.cond & univ_bdd; + } + transitions_ &= state_bdd; + } + ap_ = bdd_exist(bdd_support(transitions_), all_states_); + all_letters_ = bdd_exist(transitions_, all_states_); + } + + std::set bdd_to_state(bdd b) const + { + std::set state; + while (b != bddtrue) + { + assert(bdd_low(b) == bddfalse); + int v = bdd_var(b); + b = bdd_high(b); + auto it = var_to_state_.find(v); + assert(it != var_to_state_.end()); + state.insert(it->second); + } + return state; + } + + void one_transition() + { + transition_ = isop_.next(); + if (transition_ != bddfalse || all_letters_ != bddfalse) + { + // If it was the last transition, try the next letter. + if (transition_ == bddfalse) + { + bdd oneletter = bdd_satoneset(all_letters_, ap_, bddtrue); + all_letters_ -= oneletter; + // Get a sum of possible transitions matching this letter. + isop_ = minato_isop(oneletter & transitions_); + transition_ = isop_.next(); + } + bdd dest_bdd = bdd_exist(transition_, ap_); + std::set dest = bdd_to_state(dest_bdd); + dst_ = new univ_remover_state(dest); + } + } + + virtual bool first() override + { + one_transition(); + return transition_ != bddfalse; + } + + virtual bool next() override + { + one_transition(); + return transition_ != bddfalse; + } + + virtual bool done() const override + { + return transition_ == bddfalse && all_letters_ == bddfalse; + } + + virtual const state* dst() const override + { + return dst_; + } + + virtual bdd cond() const override + { + return bdd_exist(transition_, all_states_); + } + + virtual acc_cond::mark_t acc() const override + { + assert(dst_); + return dst_->is_reset(); + } + }; + + twa_univ_remover::twa_univ_remover(const const_twa_graph_ptr& aut) + : twa(aut->get_dict()), aut_(aut) + { + assert(aut->num_sets() == 1); + allocate_state_vars(); + } + + void twa_univ_remover::allocate_state_vars() + { + auto d = aut_->get_dict(); + unsigned ns = aut_->num_states(); + state_to_var_.reserve(ns); + all_states_ = bddtrue; + bdd all_vars = bddtrue; + for (unsigned s = 0; s < ns; ++s) + { + int v = d->register_anonymous_variables(2, this); + // v and v + 1 respectively correspond to state s and ~s, i.e. s \in Q0 + // or s \in Q1 using the original paper's notation. + all_states_ &= bdd_ithvar(v) & bdd_ithvar(v + 1); + state_to_var_.push_back(v); + var_to_state_[v] = s; + var_to_state_[v + 1] = ~s; + } + } + + const state* twa_univ_remover::get_init_state() const + { + std::set state; + for (unsigned i : aut_->univ_dests(aut_->get_init_state_number())) + state.insert(i); + return new univ_remover_state(state); + } + + twa_succ_iterator* twa_univ_remover::succ_iter(const state* s) const + { + auto as = down_cast(s); + assert(as); + return new univ_remover_succ_iterator(aut_, as, state_to_var_, + var_to_state_, all_states_); + } + + std::string twa_univ_remover::format_state(const state* s) const + { + auto as = down_cast(s); + std::ostringstream fmt; + bool first = true; + for (unsigned s : as->states()) + { + if (!first) + fmt << ','; + else + first = false; + if ((int) s < 0) + fmt << '~' << ~s; + else + fmt << s; + } + return fmt.str(); + } + + twa_univ_remover_ptr remove_univ_otf(const const_twa_graph_ptr& aut) + { + assert(aut->acc().is_buchi()); + auto res = std::make_shared(aut); + res->copy_ap_of(aut); + res->copy_acceptance_of(aut); + return res; + } } diff --git a/spot/twaalgos/alternation.hh b/spot/twaalgos/alternation.hh index 40eb5c6e1..c0adcf6ef 100644 --- a/spot/twaalgos/alternation.hh +++ b/spot/twaalgos/alternation.hh @@ -102,4 +102,60 @@ namespace spot SPOT_API twa_graph_ptr remove_alternation(const const_twa_graph_ptr& aut, bool named_states = false); + + + // Remove universal edges on the fly. + + class SPOT_API univ_remover_state: public state + { + protected: + std::set states_; + bool is_reset_; + + public: + univ_remover_state(const std::set& states); + int compare(const state* other) const override; + size_t hash() const override; + state* clone() const override; + const std::set& states() const; + bool is_reset() const; + }; + + class SPOT_API twa_univ_remover: public twa + { + + private: + const_twa_graph_ptr aut_; + std::vector state_to_var_; + std::map var_to_state_; + bdd all_states_; + + public: + twa_univ_remover(const const_twa_graph_ptr& aut); + void allocate_state_vars(); + const state* get_init_state() const override; + twa_succ_iterator* succ_iter(const state* s) const override; + std::string format_state(const state* s) const override; + }; + + typedef std::shared_ptr twa_univ_remover_ptr; + + /// \brief Remove universal edges on the fly from an automaton. + /// + /// This function uses the Myiano & Hayashi (TCS 1984) breakpoint + /// algorithm to construct a non-deterministic Büchi automaton from an + /// alternating Büchi automaton on the fly. + /// + /// \verbatim + /// @Article{ miyano.84.tcs, + /// title = "Alternating finite automata on ω-words", + /// journal = "Theoretical Computer Science", + /// volume = "32", + /// number = "3", + /// pages = "321 - 330", + /// year = "1984", + /// author = "Satoru Miyano and Takeshi Hayashi", + /// } + SPOT_API + twa_univ_remover_ptr remove_univ_otf(const const_twa_graph_ptr& aut); } diff --git a/tests/python/alternating.py b/tests/python/alternating.py index 1a55835ba..8092917e3 100755 --- a/tests/python/alternating.py +++ b/tests/python/alternating.py @@ -169,3 +169,41 @@ State: 4 State: 5 [0&1] 0&1&2 --END--""" + + +# remove_univ_otf + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 & 1 +Acceptance: 1 Inf(0) +AP: 2 "a" "b" +--BODY-- +State: 0 +[0] 0 {0} +State: 1 +[1] 2 {0} +State: 2 +[1] 2 +--END-- +""") + +out = """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 {0} +[0&1] 1 +State: 1 +[0&1] 2 +State: 2 +[0&1] 2 +--END--""" + +desalt = spot.remove_univ_otf(aut) +assert(desalt.to_str('hoa') == out)