cycles.hh

// -*- coding: utf-8 -*-
// Copyright (C) by the Spot authors, see the AUTHORS file for details.
//
// 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
// the Free Software Foundation; either version 3 of the License, or
// (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
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
#pragma once
 
#include <spot/twaalgos/sccinfo.hh>
#include <spot/misc/hash.hh>
#include <deque>
 
namespace spot
{
  class SPOT_API enumerate_cycles
  {
  protected:
    // Extra information required for the algorithm for each state.
    struct state_info
    {
      state_info(unsigned num)
        : seen(false), reach(false), mark(false), del(num)
      {
      }
      bool seen;
      // 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))
      std::vector<bool> del;
      // Predecessors of the current states, that could not yet
      // contribute to a cycle.
      std::vector<unsigned> b;
    };
 
    // The automaton we are working on.
    const_twa_graph_ptr aut_;
    // Store the state_info for all visited states.
    std::vector<state_info> info_;
    // The SCC map built for aut_.
    const scc_info& sm_;
 
    // 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
    // cycle_found()).
    struct dfs_entry
    {
      unsigned s;
      unsigned succ = 0U;
      bool f = false;
      dfs_entry(unsigned s) noexcept
        : s(s)
      {
      }
    };
    typedef std::vector<dfs_entry> dfs_stack;
    dfs_stack dfs_;
 
  public:
    enumerate_cycles(const scc_info& map);
    virtual ~enumerate_cycles() {}
 
    void run(unsigned scc);
 
 
    virtual bool cycle_found(unsigned start);
 
  private:
    // add a new state to the dfs_ stack
    void push_state(unsigned s);
    // block the edge (x,y) because it cannot contribute to a new
    // cycle currently (sub-procedure from the paper)
    void nocycle(unsigned x, unsigned y);
    // unmark the state y (sub-procedure from the paper)
    void unmark(unsigned y);
  };
}