lasso.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/twa/twagraph.hh>
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/word.hh>
#include <climits>
#include <vector>
 
namespace spot
{
  class SPOT_API lasso_enumerator final
  {
  public:
    lasso_enumerator(const const_twa_graph_ptr& aut,
                     unsigned min_stem, unsigned max_stem,
                     unsigned min_cycle, unsigned max_cycle);
 
    ~lasso_enumerator() = default;
    lasso_enumerator(const lasso_enumerator&) = delete;
    lasso_enumerator& operator=(const lasso_enumerator&) = delete;
 
    twa_run_ptr next_run();
 
    twa_word_ptr next_word();
 
  private:
    const_twa_graph_ptr aut_;
    scc_info si_;             
    unsigned min_stem_, max_stem_;
    unsigned min_cycle_, max_cycle_;
    unsigned init_state_; 
    bool done_;           
 
    // Current (stem_len, cycle_len) pair being enumerated.
    unsigned cur_stem_;   
    unsigned cur_cycle_;  
    unsigned cur_total_;  
 
    // DFS stacks: each element is an edge number in the automaton graph.
    std::vector<unsigned> stem_;   
    std::vector<unsigned> cycle_;  
 
    unsigned stem_end_;        
    bool stem_ready_;          
    bool cycle_ready_;         
    bool cycle_exhausted_;     
 
    // Graph access helpers.
    unsigned first_edge_(unsigned state) const;
    unsigned next_edge_(unsigned edge) const;
    unsigned edge_dst_(unsigned edge) const;
    bdd edge_cond_(unsigned edge) const;
    acc_cond::mark_t edge_acc_(unsigned edge) const;
 
    // DFS helpers.
    bool backtrack_(std::vector<unsigned>& path) const;
    bool extend_(std::vector<unsigned>& path,
                 unsigned from_state, unsigned target_len);
    bool is_valid_cycle_() const;
 
    // Advancement functions.
    bool advance_pair_();
    bool advance_stem_();
    bool advance_cycle_();
 
    // Build a twa_run from the current stem_ and cycle_.
    twa_run_ptr build_run_() const;
  };
}