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

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