diff --git a/src/twaalgos/safra.cc b/src/twaalgos/safra.cc index 7a3d63a18..2f09eef37 100644 --- a/src/twaalgos/safra.cc +++ b/src/twaalgos/safra.cc @@ -43,10 +43,11 @@ namespace spot safra_state empty_state = safra_state(nb_braces_.size()); idx = res.size(); res.push_back(std::make_pair(empty_state, t.cond)); - std::cerr << "Created inner node: " << idx << std::endl; } safra_state& ss = res[idx].first; + assert(ss.nb_braces_.size() == ss.is_green_.size()); ss.update_succ(node, t.dst, t.acc); + assert(ss.nb_braces_.size() == ss.is_green_.size()); } } for (auto& s: res) @@ -59,53 +60,158 @@ namespace spot void safra_state::finalize_construction() { - // TODO this is a dirty hack to have two comparision functions depending on - // wether or not we are still construction the safra_stata - // Ideally I'd like to have this done statically but not sure how to do it - for (unsigned i = 0; i < nb_braces_.size(); ++i) + std::vector rem_succ_of; + assert(is_green_.size() == nb_braces_.size()); + for (unsigned i = 0; i < is_green_.size(); ++i) { if (nb_braces_[i] == 0) { // TODO We also emit Red = min(red, i) + // Step A3: Brackets that do not contain any nodes emit red is_green_[i] = false; } + else if (is_green_[i]) + { + // Step A4 Emit green + rem_succ_of.emplace_back(i); + } } for (auto& n: nodes_) { node& nn = const_cast(n); + // Step A4 Remove all brackets inside each green pair + nn.truncate_braces(rem_succ_of, nb_braces_); + } + + // Step A5 define the rem variable + std::vector decr_by(nb_braces_.size()); + unsigned decr = 0; + for (unsigned i = 0; i < nb_braces_.size(); ++i) + { + // Step A5 renumber braces + nb_braces_[i - decr] = nb_braces_[i]; + if (nb_braces_[i] == 0) + { + ++decr; + } + // Step A5, renumber braces + decr_by[i] = decr; + } + nb_braces_.resize(nb_braces_.size() - decr); + for (auto& n: nodes_) + { + node& nn = const_cast(n); + nn.renumber(decr_by); + + // TODO this is a dirty hack to have two comparision functions depending + // on wether or not we are still construction the safra_stata + // Ideally I'd like to have this done statically but not sure how to do + // it nn.disable_construction(); } } + void safra_state::node::renumber(const std::vector& decr_by) + { + for (unsigned idx = 0; idx < braces_.size(); ++idx) + { + braces_[idx] -= decr_by[braces_[idx]]; + } + } + + // TODO FINISH TRUNCATE + void + safra_state::node::truncate_braces(const std::vector& rem_succ_of, + std::vector& nb_braces) + { + assert(in_construction_ && "Only allowed to do this during construction"); + for (unsigned idx = 0; idx < braces_.size(); ++idx) + { + bool found = false; + // find first brace that matches rem_succ_of + for (auto s: rem_succ_of) + { + found |= braces_[idx] == s; + } + if (found) + { + assert(idx < braces_.size() - 1); + // For each deleted brace, decrement elements of nb_braces + // This corresponds to A4 step + for (unsigned i = idx + 1; i < braces_.size(); ++i) + { + --nb_braces[braces_[i]]; + } + braces_.resize(idx + 1); + break; + } + } + } + void safra_state::update_succ(const node& src, unsigned dst, const acc_cond::mark_t acc) { - (void) acc; // TODO + unsigned last_brace = src.braces_.back(); + // Check if there already is a node named dst in current macro_state auto i = nodes_.find(node(dst)); if (i != nodes_.end()) { - // Todo need to handle acc and create new braces - if (src.braces_ > i->braces_) + // Step A2: Remove all occurrences whos nesting pattern (i-e braces_) + // is smaller + if (src.braces_ > i->braces_ || + (acc.count() && src.braces_ == i->braces_)) { - std::cerr << "Replacing braces of: " << dst << std::endl; - node& dst = const_cast(*i); - for (auto b: dst.braces_) - nb_braces_[b]--; - dst.braces_ = src.braces_; + auto copy = src.braces_; + // TODO handle multiple accepting transition + if (acc.count()) + { + // Accepting transition generate new braces: step A1 + last_brace = nb_braces_.size(); + copy.emplace_back(nb_braces_.size()); + nb_braces_.emplace_back(1); + // Newly created braces cannot emit green as they won't have + // any braces inside them (by construction) + is_green_.emplace_back(false); + } + { + // Remove brace count of removed node + node& dst = const_cast(*i); + for (auto b: dst.braces_) + --nb_braces_[b]; + } + { + // Affect new value of braces + node& dst = const_cast(*i); + for (auto b: copy) + ++nb_braces_[b]; + dst.braces_ = std::move(copy); + } } - // Node already exists and has bigger values else + // Node already exists and has bigger nesting pattern value return; } else { - // Todo need to handle acc and create new braces - nodes_.emplace(dst, src.braces_); + // TODO need to handle multiple acc sets + auto copy = src.braces_; + if (acc.count()) + { + last_brace = nb_braces_.size(); + copy.emplace_back(nb_braces_.size()); + // Step A4 Newly created braces cannot emit green as they won't have + // any braces inside them (by construction) + is_green_.emplace_back(false); + nb_braces_.emplace_back(0); + } + for (auto b: copy) + ++nb_braces_[b]; + nodes_.emplace(dst, std::move(copy)); } - for (auto b: src.braces_) - nb_braces_[b]++; - // If brace has no right-hand-side brace than it cannot emit any green color - is_green_[src.braces_[src.braces_.size() - 1]] = false; + // Step A4: For a brace to emit green it must surround other braces. + // Therefore, the last brace cannot emit green as it is the most inside + // brace. + is_green_[last_brace] = false; } // Comparison is needed when for a set of safra_state @@ -131,7 +237,7 @@ namespace spot { unsigned nb_braces = val; // One brace set - is_green_.assign(true, nb_braces); + is_green_.assign(nb_braces, true); // First brace has init_state hence one state inside the first braces. nb_braces_.assign(nb_braces, 0); } @@ -156,6 +262,21 @@ namespace spot return false; } + void safra_state::print_debug(unsigned state_id) + { + std::cerr << "State: " << state_id << "{ "; + for (auto& n: nodes_) + { + std::cerr << n.id_ << " ["; + for (auto& b: n.braces_) + { + std::cerr << b << ' '; + } + std::cerr << "], "; + } + std::cerr << "}\n"; + } + twa_graph_ptr tgba_determinisation(const const_twa_graph_ptr& aut) { @@ -196,12 +317,10 @@ namespace spot else { dst_num = res->new_state(); - std::cerr << "New state " << dst_num << std::endl; + s.first.print_debug(dst_num); todo.push_back(s.first); seen.insert(std::make_pair(s.first, dst_num)); } - std::cerr << "Tr: " << src_num << " -> " << dst_num << "[" - << s.second << "]" << std::endl; res->new_transition(src_num, dst_num, s.second); } } diff --git a/src/twaalgos/safra.hh b/src/twaalgos/safra.hh index 5de34bed8..ec28c7779 100644 --- a/src/twaalgos/safra.hh +++ b/src/twaalgos/safra.hh @@ -36,6 +36,9 @@ namespace spot bool operator==(const node& other) const; bool operator<(const node& other) const; void disable_construction() { in_construction_ = false; } + void truncate_braces(const std::vector& rem_succ_of, + std::vector& nb_braces); + void renumber(const std::vector& decr_by); node(unsigned id) : id_(id), in_construction_(true) {} node(unsigned id, brace_t b_id, bool in_construction = true) @@ -57,12 +60,16 @@ namespace spot public: typedef std::vector> succs_t; bool operator<(const safra_state& other) const; + // Print each sub-state with their associated braces of a safra state + void print_debug(unsigned state_id); safra_state(unsigned state_number, bool init_state = false); // Given a certain transition_label, compute all the successors of that // label, and return that new node. succs_t compute_succs(const const_twa_graph_ptr& aut) const; // Used when creating the list of successors - void update_succ(const node& src, unsigned dst, const acc_cond::mark_t); + // A new intermediate node is created with src's braces and with dst as id + // A merge is done if dst already existed in *this + void update_succ(const node& src, unsigned dst, const acc_cond::mark_t acc); void finalize_construction(); // A list of nodes similar to the ones of a // safra tree. These are constructed in the same way as the powerset