spot  2.12.2
cycles.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <spot/twaalgos/sccinfo.hh>
22 #include <spot/misc/hash.hh>
23 #include <deque>
24 
25 namespace spot
26 {
62  class SPOT_API enumerate_cycles
63  {
64  protected:
65  // Extra information required for the algorithm for each state.
66  struct state_info
67  {
68  state_info(unsigned num)
69  : seen(false), reach(false), mark(false), del(num)
70  {
71  }
72  bool seen;
73  // Whether the state has already left the stack at least once.
74  bool reach;
75  // set to true when the state current state w is stacked, and
76  // reset either when the state is unstacked after having
77  // contributed to a cycle, or when some state z that (1) w could
78  // reach (even indirectly) without discovering a cycle, and (2)
79  // that a contributed to a contributed to a cycle.
80  bool mark;
81  // Deleted successors (in the paper, states deleted from A(x))
82  std::vector<bool> del;
83  // Predecessors of the current states, that could not yet
84  // contribute to a cycle.
85  std::vector<unsigned> b;
86  };
87 
88  // The automaton we are working on.
89  const_twa_graph_ptr aut_;
90  // Store the state_info for all visited states.
91  std::vector<state_info> info_;
92  // The SCC map built for aut_.
93  const scc_info& sm_;
94 
95  // The DFS stack. Each entry contains a state, an iterator on the
96  // transitions leaving that state, and a Boolean f indicating
97  // whether this state as already contributed to a cycle (f is
98  // updated when backtracking, so it should not be used by
99  // cycle_found()).
100  struct dfs_entry
101  {
102  unsigned s;
103  unsigned succ = 0U;
104  bool f = false;
105  dfs_entry(unsigned s) noexcept
106  : s(s)
107  {
108  }
109  };
110  typedef std::vector<dfs_entry> dfs_stack;
111  dfs_stack dfs_;
112 
113  public:
114  enumerate_cycles(const scc_info& map);
115  virtual ~enumerate_cycles() {}
116 
122  void run(unsigned scc);
123 
124 
140  virtual bool cycle_found(unsigned start);
141 
142  private:
143  // add a new state to the dfs_ stack
144  void push_state(unsigned s);
145  // block the edge (x,y) because it cannot contribute to a new
146  // cycle currently (sub-procedure from the paper)
147  void nocycle(unsigned x, unsigned y);
148  // unmark the state y (sub-procedure from the paper)
149  void unmark(unsigned y);
150  };
151 }
Enumerate elementary cycles in a SCC.
Definition: cycles.hh:63
virtual bool cycle_found(unsigned start)
Called whenever a cycle was found.
void run(unsigned scc)
Run in SCC scc, and call cycle_found() for any new elementary cycle found.
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:449
@ U
until
Definition: automata.hh:26
Definition: cycles.hh:101
Definition: cycles.hh:67

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.9.1