spot
2.1.2
Main Page
Related Pages
Modules
Classes
Files
File List
All
Classes
Files
Functions
Variables
Typedefs
Enumerations
Enumerator
Friends
Modules
Pages
spot
twaalgos
cycles.hh
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015 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 = 0
U
;
118
bool
f =
false
;
119
dfs_entry
(
unsigned
s): s(s)
120
{
121
}
122
};
123
typedef
std::vector<dfs_entry> dfs_stack;
124
dfs_stack dfs_;
125
126
public
:
127
enumerate_cycles
(
const
scc_info
& map);
128
virtual
~
enumerate_cycles
() {}
129
135
void
run(
unsigned
scc);
136
137
153
virtual
bool
cycle_found(
unsigned
start);
154
155
private
:
156
// add a new state to the dfs_ stack
157
void
push_state(
unsigned
s);
158
// block the edge (x,y) because it cannot contribute to a new
159
// cycle currently (sub-procedure from the paper)
160
void
nocycle(
unsigned
x,
unsigned
y);
161
// unmark the state y (sub-procedure from the paper)
162
void
unmark(
unsigned
y);
163
};
164
}
spot
Definition:
graph.hh:32
spot::scc_info
Definition:
sccinfo.hh:27
spot::enumerate_cycles::state_info
Definition:
cycles.hh:80
spot::op::U
until
spot::enumerate_cycles
Enumerate elementary cycles in a SCC.
Definition:
cycles.hh:76
spot::enumerate_cycles::dfs_entry
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 Oct 14 2016 15:38:13 for spot by
1.8.8