spot  2.2.2
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
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 {
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  return node_[scc];
112  }
113 
114  public:
115  scc_info(const_twa_graph_ptr aut);
116 
117  const_twa_graph_ptr get_aut() const
118  {
119  return aut_;
120  }
121 
122  unsigned scc_count() const
123  {
124  return node_.size();
125  }
126 
127  bool reachable_state(unsigned st) const
128  {
129  return scc_of(st) != -1U;
130  }
131 
132  unsigned scc_of(unsigned st) const
133  {
134  return sccof_[st];
135  }
136 
137  auto begin() const
138  SPOT_RETURN(node_.begin());
139  auto end() const
140  SPOT_RETURN(node_.end());
141  auto cbegin() const
142  SPOT_RETURN(node_.cbegin());
143  auto cend() const
144  SPOT_RETURN(node_.cend());
145  auto rbegin() const
146  SPOT_RETURN(node_.rbegin());
147  auto rend() const
148  SPOT_RETURN(node_.rend());
149 
150  const std::vector<unsigned>& states_of(unsigned scc) const
151  {
152  return node(scc).states();
153  }
154 
155  unsigned one_state_of(unsigned scc) const
156  {
157  return states_of(scc).front();
158  }
159 
161  unsigned initial() const
162  {
163  SPOT_ASSERT(scc_count() - 1 == scc_of(aut_->get_init_state_number()));
164  return scc_count() - 1;
165  }
166 
167  const scc_succs& succ(unsigned scc) const
168  {
169  return node(scc).succ();
170  }
171 
172  bool is_trivial(unsigned scc) const
173  {
174  return node(scc).is_trivial();
175  }
176 
177  acc_cond::mark_t acc(unsigned scc) const
178  {
179  return node(scc).acc_marks();
180  }
181 
182  bool is_accepting_scc(unsigned scc) const
183  {
184  return node(scc).is_accepting();
185  }
186 
187  bool is_rejecting_scc(unsigned scc) const
188  {
189  return node(scc).is_rejecting();
190  }
191 
192  // Study the SCC that are currently reported neither as accepting
193  // nor rejecting because of the presence of Fin sets
194  void determine_unknown_acceptance();
195 
196  bool is_useful_scc(unsigned scc) const
197  {
198  return node(scc).is_useful();
199  }
200 
201  bool is_useful_state(unsigned st) const
202  {
203  return reachable_state(st) && node(scc_of(st)).is_useful();
204  }
205 
208  std::vector<std::set<acc_cond::mark_t>> used_acc() const;
209 
210  std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const;
211 
212  acc_cond::mark_t acc_sets_of(unsigned scc) const;
213 
214  std::vector<bool> weak_sccs() const;
215 
216  bdd scc_ap_support(unsigned scc) const;
217  };
218 
219 
223  SPOT_API std::ostream&
224  dump_scc_info_dot(std::ostream& out,
225  const_twa_graph_ptr aut, scc_info* sccinfo = nullptr);
226 
227 }
Definition: sccinfo.hh:32
bool is_rejecting() const
Definition: sccinfo.hh:74
Definition: graph.hh:32
Definition: sccinfo.hh:27
Definition: formula.hh:1671
unsigned initial() const
Get number of the SCC containing the initial state.
Definition: sccinfo.hh:161
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 Fri Dec 16 2016 06:04:08 for spot by doxygen 1.8.8