spot  2.3.5
sccinfo.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
3 // Développement de l'Epita.
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 <vector>
23 #include <spot/twa/twagraph.hh>
24 
25 namespace spot
26 {
39  class SPOT_API scc_info
40  {
41  public:
42  typedef std::vector<unsigned> scc_succs;
43 
44  class scc_node
45  {
46  friend class scc_info;
47  protected:
48  scc_succs succ_;
49  acc_cond::mark_t acc_;
50  std::vector<unsigned> states_; // States of the component
51  bool trivial_:1;
52  bool accepting_:1; // Necessarily accepting
53  bool rejecting_:1; // Necessarily rejecting
54  bool useful_:1;
55  public:
56  scc_node():
57  acc_(0U), trivial_(true), accepting_(false),
58  rejecting_(false), useful_(false)
59  {
60  }
61 
62  scc_node(acc_cond::mark_t acc, bool trivial):
63  acc_(acc), trivial_(trivial), accepting_(false),
64  rejecting_(false), useful_(false)
65  {
66  }
67 
68  bool is_trivial() const
69  {
70  return trivial_;
71  }
72 
77  bool is_accepting() const
78  {
79  return accepting_;
80  }
81 
82  // True if we are sure that the SCC is rejecting
86  bool is_rejecting() const
87  {
88  return rejecting_;
89  }
90 
91  bool is_useful() const
92  {
93  return useful_;
94  }
95 
96  acc_cond::mark_t acc_marks() const
97  {
98  return acc_;
99  }
100 
101  const std::vector<unsigned>& states() const
102  {
103  return states_;
104  }
105 
106  const scc_succs& succ() const
107  {
108  return succ_;
109  }
110  };
111 
112  protected:
113 
114  std::vector<unsigned> sccof_;
115  std::vector<scc_node> node_;
116  const_twa_graph_ptr aut_;
117 
118  // Update the useful_ bits. Called automatically.
119  void determine_usefulness();
120 
121  const scc_node& node(unsigned scc) const
122  {
123  return node_[scc];
124  }
125 
126  public:
127  scc_info(const_twa_graph_ptr aut);
128 
129  const_twa_graph_ptr get_aut() const
130  {
131  return aut_;
132  }
133 
134  unsigned scc_count() const
135  {
136  return node_.size();
137  }
138 
139  bool reachable_state(unsigned st) const
140  {
141  return scc_of(st) != -1U;
142  }
143 
144  unsigned scc_of(unsigned st) const
145  {
146  return sccof_[st];
147  }
148 
149  auto begin() const
150  SPOT_RETURN(node_.begin());
151  auto end() const
152  SPOT_RETURN(node_.end());
153  auto cbegin() const
154  SPOT_RETURN(node_.cbegin());
155  auto cend() const
156  SPOT_RETURN(node_.cend());
157  auto rbegin() const
158  SPOT_RETURN(node_.rbegin());
159  auto rend() const
160  SPOT_RETURN(node_.rend());
161 
162  const std::vector<unsigned>& states_of(unsigned scc) const
163  {
164  return node(scc).states();
165  }
166 
167  unsigned one_state_of(unsigned scc) const
168  {
169  return states_of(scc).front();
170  }
171 
173  unsigned initial() const
174  {
175  SPOT_ASSERT(scc_count() - 1 == scc_of(aut_->get_init_state_number()));
176  return scc_count() - 1;
177  }
178 
179  const scc_succs& succ(unsigned scc) const
180  {
181  return node(scc).succ();
182  }
183 
184  bool is_trivial(unsigned scc) const
185  {
186  return node(scc).is_trivial();
187  }
188 
189  acc_cond::mark_t acc(unsigned scc) const
190  {
191  return node(scc).acc_marks();
192  }
193 
194  bool is_accepting_scc(unsigned scc) const
195  {
196  return node(scc).is_accepting();
197  }
198 
199  bool is_rejecting_scc(unsigned scc) const
200  {
201  return node(scc).is_rejecting();
202  }
203 
204  // Study the SCC that are currently reported neither as accepting
205  // nor rejecting because of the presence of Fin sets
206  void determine_unknown_acceptance();
207 
208  bool is_useful_scc(unsigned scc) const
209  {
210  return node(scc).is_useful();
211  }
212 
213  bool is_useful_state(unsigned st) const
214  {
215  return reachable_state(st) && node(scc_of(st)).is_useful();
216  }
217 
220  std::vector<std::set<acc_cond::mark_t>> used_acc() const;
221 
222  std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const;
223 
224  acc_cond::mark_t acc_sets_of(unsigned scc) const;
225 
226  std::vector<bool> weak_sccs() const;
227 
228  bdd scc_ap_support(unsigned scc) const;
229  };
230 
231 
235  SPOT_API std::ostream&
236  dump_scc_info_dot(std::ostream& out,
237  const_twa_graph_ptr aut, scc_info* sccinfo = nullptr);
238 
239 }
Definition: sccinfo.hh:44
Definition: graph.hh:33
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:39
bool is_rejecting() const
Definition: sccinfo.hh:86
unsigned initial() const
Get number of the SCC containing the initial state.
Definition: sccinfo.hh:173
Definition: acc.hh:34
bool is_accepting() const
True if we are sure that the SCC is accepting.
Definition: sccinfo.hh:77

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Thu Jun 22 2017 07:46:14 for spot by doxygen 1.8.13