spot
2.9.3
spot
twaalgos
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
26
namespace
spot
27
{
63
class
SPOT_API
enumerate_cycles
64
{
65
protected
:
66
// Extra information required for the algorithm for each state.
67
struct
state_info
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()).
101
struct
dfs_entry
102
{
103
unsigned
s;
104
unsigned
succ = 0
U
;
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
}
spot
Definition:
automata.hh:26
spot::scc_info
Compute an SCC map and gather assorted information.
Definition:
sccinfo.hh:441
spot::enumerate_cycles::state_info
Definition:
cycles.hh:67
spot::op::U
until
spot::enumerate_cycles
Enumerate elementary cycles in a SCC.
Definition:
cycles.hh:63
spot::enumerate_cycles::dfs_entry
Definition:
cycles.hh:101
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
1.8.13