spot 2.11.6.dev
zlktree.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2021, 2022 Laboratoire de Recherche et Developpement de
3// l'Epita (LRDE).
4//
5// This file is part of Spot, a model checking library.
6//
7// Spot is free software; you can redistribute it and/or modify it
8// under the terms of the GNU General Public License as published by
9// the Free Software Foundation; either version 3 of the License, or
10// (at your option) any later version.
11//
12// Spot is distributed in the hope that it will be useful, but WITHOUT
13// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15// License for more details.
16//
17// You should have received a copy of the GNU General Public License
18// along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20#pragma once
21
22#include <iosfwd>
23#include <deque>
24#include <memory>
25#include <spot/misc/bitvect.hh>
26#include <spot/twa/twagraph.hh>
27#include <spot/twaalgos/sccinfo.hh>
28
29namespace spot
30{
34 {
36 NONE = 0,
40 CHECK_RABIN = 1,
44 CHECK_STREETT = 2,
57 };
58
59#ifndef SWIG
60 inline
61 bool operator!(zielonka_tree_options me)
62 {
63 return me == zielonka_tree_options::NONE;
64 }
65
66 inline
69 {
70 typedef std::underlying_type_t<zielonka_tree_options> ut;
71 return static_cast<zielonka_tree_options>(static_cast<ut>(left)
72 & static_cast<ut>(right));
73 }
74
75 inline
78 {
79 typedef std::underlying_type_t<zielonka_tree_options> ut;
80 return static_cast<zielonka_tree_options>(static_cast<ut>(left)
81 | static_cast<ut>(right));
82 }
83
84 inline
87 {
88 typedef std::underlying_type_t<zielonka_tree_options> ut;
89 return static_cast<zielonka_tree_options>(static_cast<ut>(left)
90 & ~static_cast<ut>(right));
91 }
92#endif
102 class SPOT_API zielonka_tree
103 {
104 public:
108
113 unsigned num_branches() const
114 {
115 return num_branches_;
116 }
117
121 unsigned first_branch() const
122 {
123 return one_branch_;
124 }
125
145 std::pair<unsigned, unsigned>
146 step(unsigned branch, acc_cond::mark_t colors) const;
147
150 bool is_even() const
151 {
152 return is_even_;
153 }
154
159 bool has_rabin_shape() const
160 {
161 return has_rabin_shape_;
162 }
163
168 bool has_streett_shape() const
169 {
170 return has_streett_shape_;
171 }
172
176 bool has_parity_shape() const
177 {
178 return has_streett_shape_ && has_rabin_shape_;
179 }
180
182 void dot(std::ostream&) const;
183
185 {
186 unsigned parent;
187 unsigned next_sibling = 0;
188 unsigned first_child = 0;
189 unsigned level;
190 acc_cond::mark_t colors;
191 };
192 std::vector<zielonka_node> nodes_;
193 private:
194 unsigned one_branch_ = 0;
195 unsigned num_branches_ = 0;
196 bool is_even_;
197 bool empty_is_even_;
198 bool has_rabin_shape_ = true;
199 bool has_streett_shape_ = true;
200 };
201
213 SPOT_API
214 twa_graph_ptr zielonka_tree_transform(const const_twa_graph_ptr& aut);
215
216
219 enum class acd_options
220 {
222 NONE = 0,
224 CHECK_RABIN = 1,
226 CHECK_STREETT = 2,
237 ORDER_HEURISTIC = 8,
238 };
239
240#ifndef SWIG
241 inline
242 bool operator!(acd_options me)
243 {
244 return me == acd_options::NONE;
245 }
246
247 inline
248 acd_options operator&(acd_options left, acd_options right)
249 {
250 typedef std::underlying_type_t<acd_options> ut;
251 return static_cast<acd_options>(static_cast<ut>(left)
252 & static_cast<ut>(right));
253 }
254
255 inline
257 {
258 typedef std::underlying_type_t<acd_options> ut;
259 return static_cast<acd_options>(static_cast<ut>(left)
260 | static_cast<ut>(right));
261 }
262
263 inline
264 acd_options operator-(acd_options left, acd_options right)
265 {
266 typedef std::underlying_type_t<acd_options> ut;
267 return static_cast<acd_options>(static_cast<ut>(left)
268 & ~static_cast<ut>(right));
269 }
270
271#endif
272
282 class SPOT_API acd
283 {
284 public:
287 acd(const const_twa_graph_ptr& aut, acd_options opt = acd_options::NONE);
288
289 ~acd();
290
299 std::pair<unsigned, unsigned>
300 step(unsigned branch, unsigned edge) const;
301
308 unsigned state_step(unsigned node, unsigned edge) const;
309
313 std::vector<unsigned> edges_of_node(unsigned n) const;
314
316 unsigned node_count() const
317 {
318 return nodes_.size();
319 }
320
324 bool node_acceptance(unsigned n) const;
325
327 unsigned node_level(unsigned n) const;
328
330 const acc_cond::mark_t& node_colors(unsigned n) const;
331
334 bool is_even(unsigned scc) const
335 {
336 if (scc >= scc_count_)
337 report_invalid_scc_number(scc, "is_even");
338 return trees_[scc].is_even;
339 }
340
347 bool is_even() const
348 {
349 return is_even_;
350 }
351
353 unsigned first_branch(unsigned state) const;
354
355 unsigned scc_max_level(unsigned scc) const
356 {
357 if (scc >= scc_count_)
358 report_invalid_scc_number(scc, "scc_max_level");
359 return trees_[scc].max_level;
360 }
361
367 bool has_rabin_shape() const;
368
374 bool has_streett_shape() const;
375
381 bool has_parity_shape() const;
382
384 const const_twa_graph_ptr get_aut() const
385 {
386 return aut_;
387 }
388
393 void dot(std::ostream&, const char* id = nullptr) const;
394
395 private:
396 const scc_info* si_;
397 bool own_si_ = false;
398 acd_options opt_;
399
400 // This structure is used to represent one node in the ACD forest.
401 // The tree use a left-child / right-sibling representation
402 // (called here first_child, next_sibling). Each node
403 // additionally store a level (depth in the ACD, adjusted at the
404 // end of the construction so that all node on the same level have
405 // the same parity), the SCC (which is also it's tree number), and
406 // some bit vectors representing the edges and states of that
407 // node. Those bit vectors are as large as the original
408 // automaton, and they are shared among nodes from the different
409 // trees of the ACD forest (since each tree correspond to a
410 // different SCC, they cannot share state or edges).
411 struct acd_node
412 {
413 unsigned parent;
414 unsigned next_sibling = 0;
415 unsigned first_child = 0;
416 unsigned level;
417 unsigned scc;
418 acc_cond::mark_t colors;
419 unsigned minstate;
420 bitvect& edges;
421 bitvect& states;
422 acd_node(bitvect& e, bitvect& s) noexcept
423 : edges(e), states(s)
424 {
425 }
426 };
427 // We store the nodes in a deque so that their addresses do not
428 // change.
429 std::deque<acd_node> nodes_;
430 // Likewise for bitvectors: this is the support for all edge vectors
431 // and state vectors used in acd_node.
432 std::deque<std::unique_ptr<bitvect>> bitvectors;
433 // Information about a tree of the ACD. Each treinserte correspond
434 // to an SCC.
435 struct scc_data
436 {
437 bool trivial; // whether the SCC is trivial we do
438 // not store any node for trivial
439 // SCCs.
440 unsigned root = 0; // root node of a non-trivial SCC.
441 bool is_even; // parity of the tree, used at the end
442 // of the construction to adjust
443 // levels.
444 unsigned max_level = 0; // Maximum level for this SCC.
445 unsigned num_nodes = 0; // Number of node in this tree. This
446 // is only used to share bitvectors
447 // between SCC: node with the same
448 // "rank" in each tree share the same
449 // bitvectors.
450 };
451 std::vector<scc_data> trees_;
452 unsigned scc_count_;
453 const_twa_graph_ptr aut_;
454 // Information about the overall ACD.
455 bool is_even_;
456 bool has_rabin_shape_ = true;
457 bool has_streett_shape_ = true;
458
459 // Build the ACD structure. Called by the constructors.
460 void build_();
461
462 // leftmost branch of \a node that contains \a state
463 unsigned leftmost_branch_(unsigned node, unsigned state) const;
464
465#ifndef SWIG
466 [[noreturn]] static
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);
470#endif
471 };
472
495 SPOT_API
496 twa_graph_ptr acd_transform(const const_twa_graph_ptr& aut,
497 bool colored = false);
498 SPOT_API
499 twa_graph_ptr acd_transform_sbacc(const const_twa_graph_ptr& aut,
500 bool colored = false,
501 bool order_heuristic = true);
503}
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 acc_cond::mark_t & node_colors(unsigned n) const
Return the colors of a node.
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
std::pair< unsigned, unsigned > step(unsigned branch, unsigned edge) const
Step through the ACD.
bool has_rabin_shape() const
Whether the ACD has Rabin shape.
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
std::pair< unsigned, unsigned > step(unsigned branch, acc_cond::mark_t colors) const
Walk through the Zielonka tree.
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
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
zielonka_tree_options
Options to alter the behavior of acd.
Definition: zlktree.hh:34
acd_options
Options to alter the behavior of acd.
Definition: zlktree.hh:220
twa_graph_ptr zielonka_tree_transform(const const_twa_graph_ptr &aut)
Paritize an automaton using Zielonka tree.
twa_graph_ptr acd_transform(const const_twa_graph_ptr &aut, bool colored=false)
Paritize an automaton using ACD.
twa_graph_ptr acd_transform_sbacc(const const_twa_graph_ptr &aut, bool colored=false, bool order_heuristic=true)
Paritize an automaton using ACD.
@ NONE
Build the ZlkTree, without checking its shape.
@ NONE
Build the ACD, without checking its shape.
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

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.4