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

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Jul 11 2016 09:54:34 for spot by doxygen 1.8.8