cycles.hh 6.08 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015, 2018 Laboratoire de Recherche et
3
// Développement de l'Epita (LRDE).
4
5
6
7
8
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// 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
11
12
13
14
15
16
17
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// 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
23
#include <spot/twaalgos/sccinfo.hh>
#include <spot/misc/hash.hh>
24
25
26
27
#include <deque>

namespace spot
{
28
  /// \brief Enumerate elementary cycles in a SCC.
29
  ///
30
31
  /// This class implements a non-recursive version of the algorithm
  /// on page 170 of:
32
33
34
35
36
37
  /** \verbatim
      @Article{loizou.82.is,
        author =  {George Loizou and Peter Thanisch},
        title =   {Enumerating the Cycles of a Digraph: A New
                   Preprocessing Strategy},
        journal = {Information Sciences},
38
        year =           {1982},
39
40
41
42
43
44
        volume =  {27},
        number =  {3},
        pages =   {163--182},
        month =   aug
      }
      \endverbatim */
45
46
47
48
49
50
51
52
53
54
55
56
  /// (the additional preprocessings described later in that paper are
  /// not implemented).
  ///
  /// It should be noted that although the above paper does not
  /// consider multiple arcs and self-loops in its definitions, the
  /// algorithm they present works as expected in these cases.
  ///
  /// For our purpose an elementary cycle is a sequence of transitions
  /// that form a cycle and that visit a state at most once.  We may
  /// have two cycles that visit the same states in the same order if
  /// some pair of states are connected by several transitions.  Also
  /// A cycle may visit only one state if it is a self-loop.
57
  ///
58
59
60
61
62
  /// We represent a cycle by a sequence of succ_iterator objects
  /// positioned on the transition contributing to the cycle.  These
  /// succ_itertor are stored, along with their source state, in the
  /// dfs_ stack.  Only the last portion of this stack may form a
  /// cycle.
63
  ///
64
65
66
67
68
  /// Calling <code>run(n)</code> will enumerate all elementary cycles
  /// in SCC <code>n</code>.  Each time an SCC is found, the method
  /// cycle_found(s) is called with the initial state s of the cycle:
  /// the cycle is constituted from all the states that are on the \c
  /// dfs_ stack after \c s (including \c s).
69
70
71
72
73
74
75
  ///
  /// You should inherit from this class and redefine the
  /// cycle_found() method to perform any work you would like to do on
  /// the enumerated cycles.  If cycle_found() returns false, the
  /// run() method will terminate.  If it returns true, the run()
  /// method will search for the next elementary cycle and call
  /// cycle_found() again if it finds another cycle.
76
  class SPOT_API enumerate_cycles
77
78
  {
  protected:
79
    // Extra information required for the algorithm for each state.
80
81
    struct state_info
    {
82
      state_info(unsigned num)
83
        : seen(false), reach(false), mark(false), del(num)
84
85
      {
      }
86
      bool seen;
87
88
89
90
91
92
93
94
95
      // Whether the state has already left the stack at least once.
      bool reach;
      // set to true when the state current state w is stacked, and
      // reset either when the state is unstacked after having
      // contributed to a cycle, or when some state z that (1) w could
      // reach (even indirectly) without discovering a cycle, and (2)
      // that a contributed to a contributed to a cycle.
      bool mark;
      // Deleted successors (in the paper, states deleted from A(x))
96
      std::vector<bool> del;
97
98
      // Predecessors of the current states, that could not yet
      // 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
105
    // Store the state_info for all visited states.
    std::vector<state_info> info_;
106
    // The SCC map built for aut_.
107
    const scc_info& sm_;
108

109
110
111
112
    // The DFS stack.  Each entry contains a state, an iterator on the
    // transitions leaving that state, and a Boolean f indicating
    // whether this state as already contributed to a cycle (f is
    // updated when backtracking, so it should not be used by
113
    // cycle_found()).
114
115
    struct dfs_entry
    {
116
117
118
      unsigned s;
      unsigned succ = 0U;
      bool f = false;
119
120
      dfs_entry(unsigned s) noexcept
        : s(s)
121
122
      {
      }
123
    };
124
    typedef std::vector<dfs_entry> dfs_stack;
125
126
127
    dfs_stack dfs_;

  public:
128
    enumerate_cycles(const scc_info& map);
129
    virtual ~enumerate_cycles() {}
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150

    /// \brief Run in SCC scc, and call \a cycle_found() for any new
    /// elementary cycle found.
    ///
    /// It is safe to call this method multiple times, for instance to
    /// enumerate the cycle of each SCC.
    void run(unsigned scc);


    /// \brief Called whenever a cycle was found.
    ///
    /// The cycle uses all the states from the dfs stack, starting
    /// from the one labeled \a start.  The iterators in the DFS stack
    /// are all pointing to the transition considered for the cycle.
    ///
    /// This method is not const so you can modify private variables
    /// to your subclass, but it should definitely NOT modify the dfs
    /// stack or the tags map.
    ///
    /// The default implementation, not very useful, will print the
    /// states in the cycle on std::cout.
151
152
153
    ///
    /// This method method should return false iff no more cycles need
    /// should be enumerated by run().
154
    virtual bool cycle_found(unsigned start);
155

156
157
  private:
    // add a new state to the dfs_ stack
158
    void push_state(unsigned s);
159
160
    // block the edge (x,y) because it cannot contribute to a new
    // cycle currently (sub-procedure from the paper)
161
    void nocycle(unsigned x, unsigned y);
162
    // unmark the state y (sub-procedure from the paper)
163
    void unmark(unsigned y);
164
165
  };
}