spot  2.12
split.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 <spot/twa/twagraph.hh>
22 #include <vector>
23 
24 namespace spot
25 {
40  SPOT_API twa_graph_ptr split_edges(const const_twa_graph_ptr& aut);
41 
42 #ifndef SWIG
43  // pseudo container that we use to iterate over
44  // the items of LABELS that are compatible with COND.
45  template<bool subsumed>
46  struct SPOT_API edge_separator_filter
47  {
48  edge_separator_filter(const std::vector<bdd>& labels, bdd cond)
49  : labels_(labels), cond_(cond)
50  {
51  }
52 
53  class iterator
54  {
55  std::vector<bdd>::const_iterator pos_;
56  std::vector<bdd> const& labels_;
57  bdd cond_;
58 
59  public:
60  iterator(const std::vector<bdd>& labels, bdd cond)
61  : labels_(labels), cond_(cond)
62  {
63  pos_ = labels_.begin();
64  next();
65  }
66 
67  iterator& operator++()
68  {
69  ++pos_;
70  next();
71  return *this;
72  }
73 
74  void next()
75  {
76  // If subsumed is true, we want to match the labels
77  // that imply the current condition. Otherwise we
78  // want to match the labels that are compatible.
79  while (pos_ != labels_.end() &&
80  ((subsumed && !bdd_implies(*pos_, cond_))
81  || (!subsumed && (*pos_ & cond_) == bddfalse)))
82  ++pos_;
83  }
84 
85  bdd operator*() const
86  {
87  if (subsumed)
88  return *pos_;
89  else
90  return *pos_ & cond_;
91  }
92 
93  bool operator==(const iterator& other) const
94  {
95  return pos_ == other.pos_;
96  }
97 
98  bool operator!=(const iterator& other) const
99  {
100  return pos_ != other.pos_;
101  }
102 
103  bool operator==(std::vector<bdd>::const_iterator pos) const
104  {
105  return pos_ == pos;
106  }
107 
108  bool operator!=(std::vector<bdd>::const_iterator pos) const
109  {
110  return pos_ != pos;
111  }
112  };
113 
114  iterator begin() const
115  {
116  return iterator(labels_, cond_);
117  }
118 
119  std::vector<bdd>::const_iterator end() const
120  {
121  return labels_.end();
122  }
123 
124  private:
125  const std::vector<bdd>& labels_;
126  bdd cond_;
127  };
128 #endif
129 
130 
145  class SPOT_API edge_separator
146  {
147  public:
164  void add_to_basis(bdd label);
165  void add_to_basis(const const_twa_graph_ptr& aut);
166  bool add_to_basis(const const_twa_graph_ptr& aut,
167  unsigned long max_label);
175  twa_graph_ptr separate_implying(const const_twa_graph_ptr& aut);
182  twa_graph_ptr separate_compat(const const_twa_graph_ptr& aut);
183 #ifndef SWIG
193  {
194  return {basis_, label};
195  }
206  {
207  return {basis_, label};
208  }
209 #endif
210 
211  unsigned basis_size() const
212  {
213  return basis_.size();
214  }
215 
216  const std::vector<bdd>& basis() const
217  {
218  return basis_;
219  }
220 
221  private:
222  std::vector<bdd> basis_{bddtrue};
223  std::set<formula> aps_;
224  };
225 
238  SPOT_API twa_graph_ptr separate_edges(const const_twa_graph_ptr& aut);
239 }
separate edges so that their labels are disjoint
Definition: split.hh:146
edge_separator_filter< true > separate_implying(bdd label)
Separate a label.
Definition: split.hh:192
bool add_to_basis(const const_twa_graph_ptr &aut, unsigned long max_label)
add label(s) to a basis
twa_graph_ptr separate_implying(const const_twa_graph_ptr &aut)
Separate an automaton.
edge_separator_filter< false > separate_compat(bdd label)
Separate a label.
Definition: split.hh:205
void add_to_basis(bdd label)
add label(s) to a basis
void add_to_basis(const const_twa_graph_ptr &aut)
add label(s) to a basis
twa_graph_ptr separate_compat(const const_twa_graph_ptr &aut)
Separate an automaton.
twa_graph_ptr split_edges(const const_twa_graph_ptr &aut)
transform edges into transitions
twa_graph_ptr separate_edges(const const_twa_graph_ptr &aut)
Make edge labels disjoints.
Definition: automata.hh:26
Definition: split.hh:47

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