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:
    struct state_info
    {
      state_info(unsigned num)
        : seen(false), reach(false), mark(false), del(num)
      {
      }
      bool seen;   
      bool reach;  
      bool mark;   
      std::vector<bool> del;      
      std::vector<unsigned> b;    
    };
 
    const_twa_graph_ptr aut_;   
    std::vector<state_info> info_;  
    const scc_info& sm_;        
 
    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);
  };
}