spot 2.11.1.dev
cycles.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2012-2015, 2018-2019 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
26namespace spot
27{
63 class SPOT_API enumerate_cycles
64 {
65 protected:
66 // Extra information required for the algorithm for each state.
68 {
69 state_info(unsigned num)
70 : seen(false), reach(false), mark(false), del(num)
71 {
72 }
73 bool seen;
74 // Whether the state has already left the stack at least once.
75 bool reach;
76 // set to true when the state current state w is stacked, and
77 // reset either when the state is unstacked after having
78 // contributed to a cycle, or when some state z that (1) w could
79 // reach (even indirectly) without discovering a cycle, and (2)
80 // that a contributed to a contributed to a cycle.
81 bool mark;
82 // Deleted successors (in the paper, states deleted from A(x))
83 std::vector<bool> del;
84 // Predecessors of the current states, that could not yet
85 // contribute to a cycle.
86 std::vector<unsigned> b;
87 };
88
89 // The automaton we are working on.
90 const_twa_graph_ptr aut_;
91 // Store the state_info for all visited states.
92 std::vector<state_info> info_;
93 // The SCC map built for aut_.
94 const scc_info& sm_;
95
96 // The DFS stack. Each entry contains a state, an iterator on the
97 // transitions leaving that state, and a Boolean f indicating
98 // whether this state as already contributed to a cycle (f is
99 // updated when backtracking, so it should not be used by
100 // cycle_found()).
102 {
103 unsigned s;
104 unsigned succ = 0U;
105 bool f = false;
106 dfs_entry(unsigned s) noexcept
107 : s(s)
108 {
109 }
110 };
111 typedef std::vector<dfs_entry> dfs_stack;
112 dfs_stack dfs_;
113
114 public:
115 enumerate_cycles(const scc_info& map);
116 virtual ~enumerate_cycles() {}
117
123 void run(unsigned scc);
124
125
141 virtual bool cycle_found(unsigned start);
142
143 private:
144 // add a new state to the dfs_ stack
145 void push_state(unsigned s);
146 // block the edge (x,y) because it cannot contribute to a new
147 // cycle currently (sub-procedure from the paper)
148 void nocycle(unsigned x, unsigned y);
149 // unmark the state y (sub-procedure from the paper)
150 void unmark(unsigned y);
151 };
152}
Enumerate elementary cycles in a SCC.
Definition: cycles.hh:64
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:443
@ U
until
Definition: automata.hh:27
Definition: cycles.hh:102
Definition: cycles.hh:68

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