spot 2.12.2
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
24namespace 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
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
bool add_to_basis(const const_twa_graph_ptr &aut, unsigned long max_label)
add label(s) to a basis
edge_separator_filter< true > separate_implying(bdd label)
Separate a label.
Definition: split.hh:192
twa_graph_ptr separate_implying(const const_twa_graph_ptr &aut)
Separate an automaton.
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.
edge_separator_filter< false > separate_compat(bdd label)
Separate a label.
Definition: split.hh:205
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.4