25 #include <spot/misc/bitvect.hh>
26 #include <spot/twa/twagraph.hh>
27 #include <spot/twaalgos/sccinfo.hh>
70 typedef std::underlying_type_t<zielonka_tree_options> ut;
72 &
static_cast<ut
>(right));
79 typedef std::underlying_type_t<zielonka_tree_options> ut;
81 |
static_cast<ut
>(right));
88 typedef std::underlying_type_t<zielonka_tree_options> ut;
90 & ~
static_cast<ut
>(right));
115 return num_branches_;
145 std::pair<unsigned, unsigned>
161 return has_rabin_shape_;
170 return has_streett_shape_;
178 return has_streett_shape_ && has_rabin_shape_;
182 void dot(std::ostream&)
const;
187 unsigned next_sibling = 0;
188 unsigned first_child = 0;
192 std::vector<zielonka_node> nodes_;
194 unsigned one_branch_ = 0;
195 unsigned num_branches_ = 0;
198 bool has_rabin_shape_ =
true;
199 bool has_streett_shape_ =
true;
250 typedef std::underlying_type_t<acd_options> ut;
251 return static_cast<acd_options>(
static_cast<ut
>(left)
252 &
static_cast<ut
>(right));
258 typedef std::underlying_type_t<acd_options> ut;
259 return static_cast<acd_options>(
static_cast<ut
>(left)
260 |
static_cast<ut
>(right));
266 typedef std::underlying_type_t<acd_options> ut;
267 return static_cast<acd_options>(
static_cast<ut
>(left)
268 & ~
static_cast<ut
>(right));
299 std::pair<unsigned, unsigned>
300 step(
unsigned branch,
unsigned edge)
const;
318 return nodes_.size();
336 if (scc >= scc_count_)
337 report_invalid_scc_number(scc,
"is_even");
338 return trees_[scc].is_even;
355 unsigned scc_max_level(
unsigned scc)
const
357 if (scc >= scc_count_)
358 report_invalid_scc_number(scc,
"scc_max_level");
359 return trees_[scc].max_level;
393 void dot(std::ostream&,
const char*
id =
nullptr)
const;
397 bool own_si_ =
false;
414 unsigned next_sibling = 0;
415 unsigned first_child = 0;
423 : edges(e), states(s)
429 std::deque<acd_node> nodes_;
432 std::deque<std::unique_ptr<bitvect>> bitvectors;
444 unsigned max_level = 0;
445 unsigned num_nodes = 0;
451 std::vector<scc_data> trees_;
453 const_twa_graph_ptr aut_;
456 bool has_rabin_shape_ =
true;
457 bool has_streett_shape_ =
true;
463 unsigned leftmost_branch_(
unsigned node,
unsigned state)
const;
467 void report_invalid_scc_number(
unsigned num,
const char* fn);
468 [[noreturn]]
static void report_need_opt(
const char* opt);
469 [[noreturn]]
static void report_empty_acd(
const char* fn);
497 bool colored =
false);
500 bool colored =
false,
501 bool order_heuristic =
true);
An acceptance condition.
Definition: acc.hh:62
Alternating Cycle Decomposition implementation.
Definition: zlktree.hh:283
bool has_parity_shape() const
Whether the ACD has Streett shape.
unsigned first_branch(unsigned state) const
Return the first branch for state.
bool node_acceptance(unsigned n) const
const const_twa_graph_ptr get_aut() const
Return the automaton on which the ACD is defined.
Definition: zlktree.hh:384
bool is_even(unsigned scc) const
Whether the ACD corresponds to a min even or min odd parity acceptance in SCC scc.
Definition: zlktree.hh:334
bool has_rabin_shape() const
Whether the ACD has Rabin shape.
const acc_cond::mark_t & node_colors(unsigned n) const
Return the colors of a node.
std::pair< unsigned, unsigned > step(unsigned branch, unsigned edge) const
Step through the ACD.
unsigned node_level(unsigned n) const
Return the level of a node.
std::vector< unsigned > edges_of_node(unsigned n) const
Return the list of edges covered by node n of the ACD.
unsigned node_count() const
Return the number of nodes in the the ACD forest.
Definition: zlktree.hh:316
void dot(std::ostream &, const char *id=nullptr) const
Render the ACD as in GraphViz format.
bool is_even() const
Whether the ACD globally corresponds to a min even or min odd parity acceptance.
Definition: zlktree.hh:347
unsigned state_step(unsigned node, unsigned edge) const
Step through the ACD, with rules for state-based output.
acd(const scc_info &si, acd_options opt=acd_options::NONE)
Build a Alternating Cycle Decomposition an SCC decomposition.
bool has_streett_shape() const
Whether the ACD has Streett shape.
A bit vector.
Definition: bitvect.hh:52
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:443
Abstract class for states.
Definition: twa.hh:51
Zielonka Tree implementation.
Definition: zlktree.hh:103
bool has_rabin_shape() const
Whether the Zielonka tree has Rabin shape.
Definition: zlktree.hh:159
bool has_parity_shape() const
Whether the Zielonka tree has parity shape.
Definition: zlktree.hh:176
bool has_streett_shape() const
Whether the Zielonka tree has Streett shape.
Definition: zlktree.hh:168
std::pair< unsigned, unsigned > step(unsigned branch, acc_cond::mark_t colors) const
Walk through the Zielonka tree.
zielonka_tree(const acc_cond &cond, zielonka_tree_options opt=zielonka_tree_options::NONE)
Build a Zielonka tree from the acceptance condition.
bool is_even() const
Whether the tree corresponds to a min even or min odd parity acceptance.
Definition: zlktree.hh:150
void dot(std::ostream &) const
Render the tree as in GraphViz format.
unsigned first_branch() const
The number of one branch in the tree.
Definition: zlktree.hh:121
unsigned num_branches() const
The number of branches in the Zielonka tree.
Definition: zlktree.hh:113
Definition: automata.hh:27
const mc_rvalue operator|(const mc_rvalue &lhs, const mc_rvalue &rhs)
This function helps to find the output value from a set of threads that may have different values.
Definition: mc.hh:131
An acceptance mark.
Definition: acc.hh:85
Definition: zlktree.hh:185