alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

safra: Output parity acceptance sets

Browse source 
* src/twaalgos/safra.cc, src/twaalgos/safra.hh:  Note that the created
automaton is not a true parity automaton as they are not handled yet
by Spot.
This commit is contained in:
Alexandre Lewkowicz 2015-05-19 16:32:00 +02:00 • committed by Alexandre Duret-Lutz
parent f2fa92004c
commit ef3143f048
2 changed files with 15 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/twaalgos/safra.cc
View file

@ -53,25 +53,29 @@ namespace spot
for (auto& s: res) for (auto& s: res)
{ {
safra_state& tmp = s.first; safra_state& tmp = s.first;
tmp.finalize_construction(); s.first.color_ = tmp.finalize_construction();
} }
return res; return res;
} }
void safra_state::finalize_construction() unsigned safra_state::finalize_construction()
{ {
unsigned red = -1U;
unsigned green = -1U;
std::vector<unsigned> rem_succ_of; std::vector<unsigned> rem_succ_of;
assert(is_green_.size() == nb_braces_.size()); assert(is_green_.size() == nb_braces_.size());
for (unsigned i = 0; i < is_green_.size(); ++i) for (unsigned i = 0; i < is_green_.size(); ++i)
{ {
if (nb_braces_[i] == 0) if (nb_braces_[i] == 0)
{ {
red = std::min(red, 2 * i + 1);
// TODO We also emit Red = min(red, i) // TODO We also emit Red = min(red, i)
// Step A3: Brackets that do not contain any nodes emit red // Step A3: Brackets that do not contain any nodes emit red
is_green_[i] = false; is_green_[i] = false;
} }
else if (is_green_[i]) else if (is_green_[i])
{ {
green = std::min(green, 2 * i);
// Step A4 Emit green // Step A4 Emit green
rem_succ_of.emplace_back(i); rem_succ_of.emplace_back(i);
} }
@ -109,6 +113,7 @@ namespace spot
// it // it
nn.disable_construction(); nn.disable_construction();
} }
return std::min(red, green);
} }
void safra_state::node::renumber(const std::vector<unsigned>& decr_by) void safra_state::node::renumber(const std::vector<unsigned>& decr_by)
@ -317,11 +322,14 @@ namespace spot
else else
{ {
dst_num = res->new_state(); dst_num = res->new_state();
s.first.print_debug(dst_num); // s.first.print_debug(dst_num);
todo.push_back(s.first); todo.push_back(s.first);
seen.insert(std::make_pair(s.first, dst_num)); seen.insert(std::make_pair(s.first, dst_num));
} }
res->new_transition(src_num, dst_num, s.second); if (s.first.color_ != -1U)
res->new_transition(src_num, dst_num, s.second, {s.first.color_});
else
res->new_transition(src_num, dst_num, s.second);
} }
} }
return res; return res;

4
src/twaalgos/safra.hh
View file

@ -70,7 +70,8 @@ namespace spot
// A new intermediate node is created with src's braces and with dst as id // 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 // 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 update_succ(const node& src, unsigned dst, const acc_cond::mark_t acc);
void finalize_construction(); // Return the emitted color, red or green
unsigned finalize_construction();
// A list of nodes similar to the ones of a // A list of nodes similar to the ones of a
// safra tree. These are constructed in the same way as the powerset // safra tree. These are constructed in the same way as the powerset
// algorithm. // algorithm.
@ -80,6 +81,7 @@ namespace spot
std::vector<size_t> nb_braces_; std::vector<size_t> nb_braces_;
// A bitfield to know if a brace can emit green. // A bitfield to know if a brace can emit green.
std::vector<bool> is_green_; std::vector<bool> is_green_;
unsigned color_;
}; };
SPOT_API twa_graph_ptr SPOT_API twa_graph_ptr