spot  2.3.5
cycles.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
3 // Développement de l'Epita (LRDE).
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 <spot/twaalgos/sccinfo.hh>
23 #include <spot/misc/hash.hh>
24 #include <deque>
25 
26 namespace spot
27 {
32 
45  class SPOT_API enumerate_cycles
77  {
78  protected:
79  // Extra information required for the algorithm for each state.
80  struct state_info
81  {
82  state_info(unsigned num)
83  : seen(false), reach(false), mark(false), del(num)
84  {
85  }
86  bool seen;
87  // Whether the state has already left the stack at least once.
88  bool reach;
89  // set to true when the state current state w is stacked, and
90  // reset either when the state is unstacked after having
91  // contributed to a cycle, or when some state z that (1) w could
92  // reach (even indirectly) without discovering a cycle, and (2)
93  // that a contributed to a contributed to a cycle.
94  bool mark;
95  // Deleted successors (in the paper, states deleted from A(x))
96  std::vector<bool> del;
97  // Predecessors of the current states, that could not yet
98  // contribute to a cycle.
99  std::vector<unsigned> b;
100  };
101 
102  // The automaton we are working on.
103  const_twa_graph_ptr aut_;
104  // Store the state_info for all visited states.
105  std::vector<state_info> info_;
106  // The SCC map built for aut_.
107  const scc_info& sm_;
108 
109  // The DFS stack. Each entry contains a state, an iterator on the
110  // transitions leaving that state, and a Boolean f indicating
111  // whether this state as already contributed to a cycle (f is
112  // updated when backtracking, so it should not be used by
113  // cycle_found()).
114  struct dfs_entry
115  {
116  unsigned s;
117  unsigned succ = 0U;
118  bool f = false;
119  dfs_entry(unsigned s): s(s)
120  {
121  }
122  };
123  typedef std::vector<dfs_entry> dfs_stack;
124  dfs_stack dfs_;
125 
126  public:
127  enumerate_cycles(const scc_info& map);
128  virtual ~enumerate_cycles() {}
129 
135  void run(unsigned scc);
136 
137 
153  virtual bool cycle_found(unsigned start);
154 
155  private:
156  // add a new state to the dfs_ stack
157  void push_state(unsigned s);
158  // block the edge (x,y) because it cannot contribute to a new
159  // cycle currently (sub-procedure from the paper)
160  void nocycle(unsigned x, unsigned y);
161  // unmark the state y (sub-procedure from the paper)
162  void unmark(unsigned y);
163  };
164 }
Definition: graph.hh:33
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:39
Definition: cycles.hh:80
Enumerate elementary cycles in a SCC.
Definition: cycles.hh:76
Definition: cycles.hh:114

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