spot  2.10.0.dev
zlktree.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2021 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 
29 namespace spot
30 {
40  class SPOT_API zielonka_tree
41  {
42  public:
44  zielonka_tree(const acc_cond& cond);
45 
50  unsigned num_branches() const
51  {
52  return num_branches_;
53  }
54 
58  unsigned first_branch() const
59  {
60  return one_branch_;
61  }
62 
82  std::pair<unsigned, unsigned>
83  step(unsigned branch, acc_cond::mark_t colors) const;
84 
87  bool is_even() const
88  {
89  return is_even_;
90  }
91 
96  bool has_rabin_shape() const
97  {
98  return has_rabin_shape_;
99  }
100 
105  bool has_streett_shape() const
106  {
107  return has_streett_shape_;
108  }
109 
113  bool has_parity_shape() const
114  {
115  return has_streett_shape_ && has_rabin_shape_;
116  }
117 
119  void dot(std::ostream&) const;
120 
121  private:
122  struct zielonka_node
123  {
124  unsigned parent;
125  unsigned next_sibling = 0;
126  unsigned first_child = 0;
127  unsigned level;
128  acc_cond::mark_t colors;
129  };
130  std::vector<zielonka_node> nodes_;
131  unsigned one_branch_ = 0;
132  unsigned num_branches_ = 0;
133  bool is_even_;
134  bool empty_is_even_;
135  bool has_rabin_shape_ = true;
136  bool has_streett_shape_ = true;
137  };
138 
150  SPOT_API
151  twa_graph_ptr zielonka_tree_transform(const const_twa_graph_ptr& aut);
152 
153 
156  enum class acd_options
157  {
159  NONE = 0,
161  CHECK_RABIN = 1,
163  CHECK_STREETT = 2,
169  ABORT_WRONG_SHAPE = 4,
174  ORDER_HEURISTIC = 8,
175  };
176 
177 #ifndef SWIG
178  inline
179  bool operator!(acd_options me)
180  {
181  return me == acd_options::NONE;
182  }
183 
184  inline
185  acd_options operator&(acd_options left, acd_options right)
186  {
187  typedef std::underlying_type_t<acd_options> ut;
188  return static_cast<acd_options>(static_cast<ut>(left)
189  & static_cast<ut>(right));
190  }
191 
192  inline
194  {
195  typedef std::underlying_type_t<acd_options> ut;
196  return static_cast<acd_options>(static_cast<ut>(left)
197  | static_cast<ut>(right));
198  }
199 
200  inline
201  acd_options operator-(acd_options left, acd_options right)
202  {
203  typedef std::underlying_type_t<acd_options> ut;
204  return static_cast<acd_options>(static_cast<ut>(left)
205  & ~static_cast<ut>(right));
206  }
207 
208 #endif
209 
219  class SPOT_API acd
220  {
221  public:
224  acd(const const_twa_graph_ptr& aut, acd_options opt = acd_options::NONE);
225 
226  ~acd();
227 
236  std::pair<unsigned, unsigned>
237  step(unsigned branch, unsigned edge) const;
238 
245  unsigned state_step(unsigned node, unsigned edge) const;
246 
250  std::vector<unsigned> edges_of_node(unsigned n) const;
251 
253  unsigned node_count() const
254  {
255  return nodes_.size();
256  }
257 
261  bool node_acceptance(unsigned n) const;
262 
264  unsigned node_level(unsigned n) const;
265 
267  const acc_cond::mark_t& node_colors(unsigned n) const;
268 
271  bool is_even(unsigned scc) const
272  {
273  if (scc >= scc_count_)
274  report_invalid_scc_number(scc, "is_even");
275  return trees_[scc].is_even;
276  }
277 
284  bool is_even() const
285  {
286  return is_even_;
287  }
288 
290  unsigned first_branch(unsigned state) const;
291 
292  unsigned scc_max_level(unsigned scc) const
293  {
294  if (scc >= scc_count_)
295  report_invalid_scc_number(scc, "scc_max_level");
296  return trees_[scc].max_level;
297  }
298 
304  bool has_rabin_shape() const;
305 
311  bool has_streett_shape() const;
312 
318  bool has_parity_shape() const;
319 
321  const const_twa_graph_ptr get_aut() const
322  {
323  return aut_;
324  }
325 
330  void dot(std::ostream&, const char* id = nullptr) const;
331 
332  private:
333  const scc_info* si_;
334  bool own_si_ = false;
335  acd_options opt_;
336 
337  // This structure is used to represent one node in the ACD forest.
338  // The tree use a left-child / right-sibling representation
339  // (called here first_child, next_sibling). Each node
340  // additionally store a level (depth in the ACD, adjusted at the
341  // end of the construction so that all node on the same level have
342  // the same parity), the SCC (which is also it's tree number), and
343  // some bit vectors representing the edges and states of that
344  // node. Those bit vectors are as large as the original
345  // automaton, and they are shared among nodes from the different
346  // trees of the ACD forest (since each tree correspond to a
347  // different SCC, they cannot share state or edges).
348  struct acd_node
349  {
350  unsigned parent;
351  unsigned next_sibling = 0;
352  unsigned first_child = 0;
353  unsigned level;
354  unsigned scc;
355  acc_cond::mark_t colors;
356  unsigned minstate;
357  bitvect& edges;
358  bitvect& states;
359  acd_node(bitvect& e, bitvect& s) noexcept
360  : edges(e), states(s)
361  {
362  }
363  };
364  // We store the nodes in a deque so that their addresses do not
365  // change.
366  std::deque<acd_node> nodes_;
367  // Likewise for bitvectors: this is the support for all edge vectors
368  // and state vectors used in acd_node.
369  std::deque<std::unique_ptr<bitvect>> bitvectors;
370  // Information about a tree of the ACD. Each treinserte correspond
371  // to an SCC.
372  struct scc_data
373  {
374  bool trivial; // whether the SCC is trivial we do
375  // not store any node for trivial
376  // SCCs.
377  unsigned root = 0; // root node of a non-trivial SCC.
378  bool is_even; // parity of the tree, used at the end
379  // of the construction to adjust
380  // levels.
381  unsigned max_level = 0; // Maximum level for this SCC.
382  unsigned num_nodes = 0; // Number of node in this tree. This
383  // is only used to share bitvectors
384  // between SCC: node with the same
385  // "rank" in each tree share the same
386  // bitvectors.
387  };
388  std::vector<scc_data> trees_;
389  unsigned scc_count_;
390  const_twa_graph_ptr aut_;
391  // Information about the overall ACD.
392  bool is_even_;
393  bool has_rabin_shape_ = true;
394  bool has_streett_shape_ = true;
395 
396  // Build the ACD structure. Called by the constructors.
397  void build_();
398 
399  // leftmost branch of \a node that contains \a state
400  unsigned leftmost_branch_(unsigned node, unsigned state) const;
401 
402 #ifndef SWIG
403  [[noreturn]] static
404  void report_invalid_scc_number(unsigned num, const char* fn);
405  [[noreturn]] static void report_need_opt(const char* opt);
406  [[noreturn]] static void report_empty_acd(const char* fn);
407 #endif
408  };
409 
432  SPOT_API
433  twa_graph_ptr acd_transform(const const_twa_graph_ptr& aut,
434  bool colored = false);
435  SPOT_API
436  twa_graph_ptr acd_transform_sbacc(const const_twa_graph_ptr& aut,
437  bool colored = false,
438  bool order_heuristic = true);
440 }
An acceptance condition.
Definition: acc.hh:61
Alternating Cycle Decomposition implementation.
Definition: zlktree.hh:220
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:321
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:271
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:253
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:284
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:41
bool has_rabin_shape() const
Whether the Zielonka tree has Rabin shape.
Definition: zlktree.hh:96
bool has_parity_shape() const
Whether the Zielonka tree has parity shape.
Definition: zlktree.hh:113
bool has_streett_shape() const
Whether the Zielonka tree has Streett shape.
Definition: zlktree.hh:105
std::pair< unsigned, unsigned > step(unsigned branch, acc_cond::mark_t colors) const
Walk through the Zielonka tree.
bool is_even() const
Whether the tree corresponds to a min even or min odd parity acceptance.
Definition: zlktree.hh:87
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:58
zielonka_tree(const acc_cond &cond)
Build a Zielonka tree from the acceptance condition.
unsigned num_branches() const
The number of branches in the Zielonka tree.
Definition: zlktree.hh:50
acd_options
Options to alter the behavior of acd.
Definition: zlktree.hh:157
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.
@ CHECK_STREETT
Check if the ACD has Streett shape.
@ CHECK_RABIN
Check if the ACD has Rabin shape.
@ CHECK_PARITY
Check if the ACD has Parity 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:89

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.1