spot  2.7.5
cycles.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2012, 2013, 2014, 2015, 2018 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) noexcept
120  : s(s)
121  {
122  }
123  };
124  typedef std::vector<dfs_entry> dfs_stack;
125  dfs_stack dfs_;
126 
127  public:
128  enumerate_cycles(const scc_info& map);
129  virtual ~enumerate_cycles() {}
130 
136  void run(unsigned scc);
137 
138 
154  virtual bool cycle_found(unsigned start);
155 
156  private:
157  // add a new state to the dfs_ stack
158  void push_state(unsigned s);
159  // block the edge (x,y) because it cannot contribute to a new
160  // cycle currently (sub-procedure from the paper)
161  void nocycle(unsigned x, unsigned y);
162  // unmark the state y (sub-procedure from the paper)
163  void unmark(unsigned y);
164  };
165 }
Definition: automata.hh:26
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:370
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 Fri Feb 27 2015 10:00:07 for spot by doxygen 1.8.13