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
25namespace spot
26{
62 class SPOT_API enumerate_cycles
63 {
64 protected:
65 // Extra information required for the algorithm for each state.
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()).
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.4