sccinfo.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 <vector>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/emptiness.hh>
#include <spot/misc/bitvect.hh>
 
namespace spot
{
  class scc_info;
 
  enum class edge_filter_choice { keep, ignore, cut };
  typedef edge_filter_choice
  (*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst,
                 void* filter_data);
 
  namespace internal
  {
    struct keep_all
    {
      template <typename Iterator>
      bool operator()(Iterator, Iterator) const noexcept
      {
        return true;
      }
    };
 
    // Keep only transitions that have at least one destination in the
    // current SCC.
    struct keep_inner_scc
    {
    private:
      const std::vector<unsigned>& sccof_;
      unsigned desired_scc_;
    public:
      keep_inner_scc(const std::vector<unsigned>& sccof, unsigned desired_scc)
        : sccof_(sccof), desired_scc_(desired_scc)
      {
      }
 
      template <typename Iterator>
      bool operator()(Iterator begin, Iterator end) const noexcept
      {
        bool want = false;
        while (begin != end)
          if (sccof_[*begin++] == desired_scc_)
            {
              want = true;
              break;
            }
        return want;
      }
    };
 
    template <typename Graph, typename Filter>
    class SPOT_API scc_edge_iterator
    {
    public:
      typedef typename std::conditional<std::is_const<Graph>::value,
                                        const typename Graph::edge_storage_t,
                                        typename Graph::edge_storage_t>::type
        value_type;
      typedef value_type& reference;
      typedef value_type* pointer;
      typedef std::ptrdiff_t difference_type;
      typedef std::forward_iterator_tag iterator_category;
 
      typedef std::vector<unsigned>::const_iterator state_iterator;
 
      typedef typename std::conditional<std::is_const<Graph>::value,
                                        const typename Graph::edge_vector_t,
                                        typename Graph::edge_vector_t>::type
        tv_t;
 
      typedef typename std::conditional<std::is_const<Graph>::value,
                                        const typename Graph::state_vector,
                                        typename Graph::state_vector>::type
        sv_t;
      typedef const typename Graph::dests_vector_t dv_t;
    protected:
 
      state_iterator pos_;
      state_iterator end_;
      unsigned t_;
      tv_t* tv_;
      sv_t* sv_;
      dv_t* dv_;
 
      Filter filt_;
      edge_filter efilter_;
      void* efilter_data_;
 
 
      void inc_state_maybe_()
      {
        while (!t_ && (++pos_ != end_))
          t_ = (*sv_)[*pos_].succ;
      }
 
      void inc_()
      {
        t_ = (*tv_)[t_].next_succ;
        inc_state_maybe_();
      }
 
      // Do we ignore the current transition?
      bool ignore_current()
      {
        unsigned dst = (*this)->dst;
        if ((int)dst >= 0)
          {
            // Non-universal branching => a single destination.
            if (!filt_(&(*this)->dst, 1 + &(*this)->dst))
              return true;
            if (efilter_)
              return efilter_((*tv_)[t_], dst, efilter_data_)
                != edge_filter_choice::keep;
            return false;
          }
        else
          {
            // Universal branching => multiple destinations.
            const unsigned* d = dv_->data() + ~dst;
            if (!filt_(d + 1, d + *d + 1))
              return true;
            if (efilter_)
              {
                // Keep the transition if at least one destination
                // is not filtered.
                const unsigned* end = d + *d + 1;
                for (const unsigned* i = d + 1; i != end; ++i)
                  {
                    if (efilter_((*tv_)[t_], *i, efilter_data_)
                        == edge_filter_choice::keep)
                      return false;
                  }
                return true;
              }
            return false;
          }
      }
 
    public:
      scc_edge_iterator(state_iterator begin, state_iterator end,
                        tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
                        edge_filter efilter, void* efilter_data) noexcept
        : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
          efilter_(efilter), efilter_data_(efilter_data)
      {
        if (pos_ == end_)
          return;
 
        t_ = (*sv_)[*pos_].succ;
        inc_state_maybe_();
        while (pos_ != end_ && ignore_current())
          inc_();
      }
 
      scc_edge_iterator& operator++()
      {
        do
          inc_();
        while (pos_ != end_ && ignore_current());
        return *this;
      }
 
      scc_edge_iterator operator++(int)
      {
        scc_edge_iterator old = *this;
        ++*this;
        return old;
      }
 
      bool operator==(scc_edge_iterator o) const
      {
        return pos_ == o.pos_ && t_ == o.t_;
      }
 
      bool operator!=(scc_edge_iterator o) const
      {
        return pos_ != o.pos_ || t_ != o.t_;
      }
 
      reference operator*() const
      {
        return (*tv_)[t_];
      }
 
      pointer operator->() const
      {
        return &**this;
      }
    };
 
 
    template <typename Graph, typename Filter>
    class SPOT_API scc_edges
    {
    public:
      typedef scc_edge_iterator<Graph, Filter> iter_t;
      typedef typename iter_t::tv_t tv_t;
      typedef typename iter_t::sv_t sv_t;
      typedef typename iter_t::dv_t dv_t;
      typedef typename iter_t::state_iterator state_iterator;
    private:
      state_iterator begin_;
      state_iterator end_;
      tv_t* tv_;
      sv_t* sv_;
      dv_t* dv_;
      Filter filt_;
      edge_filter efilter_;
      void* efilter_data_;
    public:
 
      scc_edges(state_iterator begin, state_iterator end,
                tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
                edge_filter efilter, void* efilter_data) noexcept
        : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
          efilter_(efilter), efilter_data_(efilter_data)
      {
      }
 
      iter_t begin() const
      {
        return {begin_, end_, tv_, sv_, dv_, filt_, efilter_, efilter_data_};
      }
 
      iter_t end() const
      {
        return {end_, end_, nullptr, nullptr, nullptr, filt_, nullptr, nullptr};
      }
    };
  }
 
 
  class SPOT_API scc_info_node
  {
  public:
    typedef std::vector<unsigned> scc_succs;
    friend class scc_info;
  protected:
    scc_succs succ_;          
    std::vector<unsigned> states_; 
    unsigned one_state_;      
    acc_cond::mark_t acc_;    
    acc_cond::mark_t common_; 
    bool trivial_:1;          
    bool accepting_:1;        
    bool rejecting_:1;        
    bool useful_:1;           
  public:
    scc_info_node() noexcept:
      acc_({}), trivial_(true), accepting_(false),
      rejecting_(false), useful_(false)
    {
    }
 
    scc_info_node(acc_cond::mark_t acc,
                  acc_cond::mark_t common, bool trivial) noexcept
      : acc_(acc), common_(common),
      trivial_(trivial), accepting_(false),
      rejecting_(false), useful_(false)
    {
    }
 
    bool is_trivial() const
    {
      return trivial_;
    }
 
    bool is_accepting() const
    {
      return accepting_;
    }
 
    bool is_rejecting() const
    {
      return rejecting_;
    }
 
    bool is_useful() const
    {
      return useful_;
    }
 
    acc_cond::mark_t acc_marks() const
    {
      return acc_;
    }
 
    acc_cond::mark_t common_marks() const
    {
      return common_;
    }
 
    const std::vector<unsigned>& states() const
    {
      return states_;
    }
 
    unsigned one_state() const
    {
      return one_state_;
    }
 
    const scc_succs& succ() const
    {
      return succ_;
    }
  };
 
  enum class scc_info_options
  {
    NONE = 0,
    STOP_ON_ACC = 1,
    TRACK_STATES = 2,
    TRACK_SUCCS = 4,
    TRACK_STATES_IF_FIN_USED = 8,
    PROCESS_UNREACHABLE_STATES = 16,
    ALL = TRACK_STATES | TRACK_SUCCS,
  };
 
  inline
  bool operator!(scc_info_options me)
  {
    return me == scc_info_options::NONE;
  }
 
  inline
  scc_info_options operator&(scc_info_options left, scc_info_options right)
  {
    typedef std::underlying_type_t<scc_info_options> ut;
    return static_cast<scc_info_options>(static_cast<ut>(left)
                                         & static_cast<ut>(right));
  }
 
  inline
  scc_info_options operator|(scc_info_options left, scc_info_options right)
  {
    typedef std::underlying_type_t<scc_info_options> ut;
    return static_cast<scc_info_options>(static_cast<ut>(left)
                                         | static_cast<ut>(right));
  }
 
  class SPOT_API scc_and_mark_filter;
 
  class SPOT_API scc_info
  {
  public:
    // scc_node used to be an inner class, but Swig 3.0.10 does not
    // support that yet.
    typedef scc_info_node scc_node; 
    typedef scc_info_node::scc_succs scc_succs; 
 
    // These types used to be defined here in Spot up to 2.9.
    typedef spot::edge_filter_choice edge_filter_choice; 
    typedef spot::edge_filter edge_filter; 
 
  protected:
 
    std::vector<unsigned> sccof_; 
    std::vector<scc_node> node_;  
    const_twa_graph_ptr aut_;     
    unsigned initial_state_;      
    edge_filter filter_;          
    void* filter_data_;           
    int one_acc_scc_ = -1;        
    scc_info_options options_;    
 
    // Update the useful_ bits.  Called automatically.
    void determine_usefulness();
 
    const scc_node& node(unsigned scc) const
    {
      return node_[scc];
    }
 
#ifndef SWIG
  private:
    [[noreturn]] static void report_need_track_states();
    [[noreturn]] static void report_need_track_succs();
    [[noreturn]] static void report_incompatible_stop_on_acc();
#endif
 
  public:
    scc_info(const_twa_graph_ptr aut,
             // Use ~0U instead of -1U to work around a bug in Swig.
             // See https://github.com/swig/swig/issues/993
             unsigned initial_state = ~0U,
             edge_filter filter = nullptr,
             void* filter_data = nullptr,
             scc_info_options options = scc_info_options::ALL);
 
    scc_info(const_twa_graph_ptr aut, scc_info_options options)
      : scc_info(aut, ~0U, nullptr, nullptr, options)
      {
      }
 
    scc_info(const scc_and_mark_filter& filt, scc_info_options options);
    // we separate the two functions so that we can rename
    // scc_info(x,options) into scc_info_with_options(x,options) in Python.
    // Otherwise calling scc_info(aut,options) can be confused with
    // scc_info(aut,initial_state).
    scc_info(const scc_and_mark_filter& filt)
    : scc_info(filt, scc_info_options::ALL)
    {
    }
 
    const_twa_graph_ptr get_aut() const
    {
      return aut_;
    }
 
    scc_info_options get_options() const
    {
      return options_;
    }
 
    edge_filter get_filter() const
    {
      return filter_;
    }
 
    void* get_filter_data() const
    {
      return filter_data_;
    }
 
    unsigned scc_count() const
    {
      return node_.size();
    }
 
    int one_accepting_scc() const
    {
      return one_acc_scc_;
    }
 
    bool reachable_state(unsigned st) const
    {
      return scc_of(st) != -1U;
    }
 
    unsigned scc_of(unsigned st) const
    {
      return sccof_[st];
    }
 
    std::vector<scc_node>::const_iterator begin() const
    {
      return node_.begin();
    }
 
    std::vector<scc_node>::const_iterator end() const
    {
      return node_.end();
    }
 
    std::vector<scc_node>::const_iterator cbegin() const
    {
      return node_.cbegin();
    }
 
    std::vector<scc_node>::const_iterator cend() const
    {
      return node_.cend();
    }
 
    std::vector<scc_node>::const_reverse_iterator rbegin() const
    {
      return node_.rbegin();
    }
 
    std::vector<scc_node>::const_reverse_iterator rend() const
    {
      return node_.rend();
    }
 
    const std::vector<unsigned>& states_of(unsigned scc) const
    {
      if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
        report_need_track_states();
      return node(scc).states();
    }
 
    internal::scc_edges<const twa_graph::graph_t, internal::keep_all>
    edges_of(unsigned scc) const
    {
      auto& states = states_of(scc);
      return {states.begin(), states.end(),
              &aut_->edge_vector(), &aut_->states(),
              &aut_->get_graph().dests_vector(),
              internal::keep_all(), filter_, const_cast<void*>(filter_data_)};
    }
 
    internal::scc_edges<const twa_graph::graph_t, internal::keep_inner_scc>
    inner_edges_of(unsigned scc) const
    {
      auto& states = states_of(scc);
      return {states.begin(), states.end(),
              &aut_->edge_vector(), &aut_->states(),
              &aut_->get_graph().dests_vector(),
              internal::keep_inner_scc(sccof_, scc), filter_,
              const_cast<void*>(filter_data_)};
    }
 
    unsigned one_state_of(unsigned scc) const
    {
      return node(scc).one_state();
    }
 
    unsigned initial() const
    {
      SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
      return scc_of(initial_state_);
    }
 
    const scc_succs& succ(unsigned scc) const
    {
      if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
        report_need_track_succs();
      return node(scc).succ();
    }
 
    bool is_trivial(unsigned scc) const
    {
      return node(scc).is_trivial();
    }
 
    bool is_accepting_scc(unsigned scc) const
    {
      return node(scc).is_accepting();
    }
 
    bool is_rejecting_scc(unsigned scc) const
    {
      return node(scc).is_rejecting();
    }
 
    bool is_maximally_accepting_scc(unsigned scc) const
    {
      return aut_->acc().accepting(acc_sets_of(scc));
    }
 
    void determine_unknown_acceptance();
 
    bool check_scc_emptiness(unsigned n) const;
 
    void get_accepting_run(unsigned scc, twa_run_ptr r) const;
 
    bool is_useful_scc(unsigned scc) const
    {
      if (SPOT_UNLIKELY(!!(options_ & scc_info_options::STOP_ON_ACC)))
        report_incompatible_stop_on_acc();
      if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
        report_need_track_succs();
      return node(scc).is_useful();
    }
 
    bool is_useful_state(unsigned st) const
    {
      return reachable_state(st) && is_useful_scc(scc_of(st));
    }
 
    std::vector<std::set<acc_cond::mark_t>> marks() const;
    std::set<acc_cond::mark_t> marks_of(unsigned scc) const;
 
    acc_cond::mark_t acc_sets_of(unsigned scc) const
    {
      return node(scc).acc_marks();
    }
 
    acc_cond::mark_t common_sets_of(unsigned scc) const
    {
      return node(scc).common_marks();
    }
 
    std::vector<bool> weak_sccs() const;
 
    bdd scc_ap_support(unsigned scc) const;
 
    std::vector<twa_graph_ptr> split_on_sets(unsigned scc,
                                             acc_cond::mark_t sets,
                                             bool preserve_names = false) const;
  protected:
    void
    states_on_acc_cycle_of_rec(unsigned scc,
                               acc_cond::mark_t all_fin,
                               acc_cond::mark_t all_inf,
                               unsigned nb_pairs,
                               std::vector<acc_cond::rs_pair>& pairs,
                               std::vector<unsigned>& res,
                               std::vector<unsigned>& old) const;
  public:
    std::vector<unsigned>
    states_on_acc_cycle_of(unsigned scc) const;
  };
 
 
  class SPOT_API scc_and_mark_filter
  {
  protected:
    const scc_info* lower_si_; 
    unsigned lower_scc_;       
    acc_cond::mark_t cut_sets_; 
    const_twa_graph_ptr aut_;  
    acc_cond old_acc_;         
    bool restore_old_acc_ = false; 
    const bitvect* keep_ = nullptr; 
 
    static scc_info::edge_filter_choice
    filter_scc_and_mark_(const twa_graph::edge_storage_t& e,
                         unsigned dst, void* data);
 
    static scc_info::edge_filter_choice
    filter_mark_(const twa_graph::edge_storage_t& e, unsigned, void* data);
 
    static scc_info::edge_filter_choice
    filter_scc_and_mark_and_edges_(const twa_graph::edge_storage_t& e,
                                   unsigned dst, void* data);
 
  public:
    scc_and_mark_filter(const scc_info& lower_si,
                        unsigned lower_scc,
                        acc_cond::mark_t cut_sets)
      : lower_si_(&lower_si), lower_scc_(lower_scc), cut_sets_(cut_sets),
        aut_(lower_si_->get_aut()), old_acc_(aut_->get_acceptance())
    {
      auto f = lower_si.get_filter();
      if (f == &filter_mark_
          || f == &filter_scc_and_mark_
          || f == &filter_scc_and_mark_and_edges_)
        {
          const void* data = lower_si.get_filter_data();
          auto& d = *reinterpret_cast<const scc_and_mark_filter*>(data);
          cut_sets_ |= d.cut_sets_;
          if (f == &filter_scc_and_mark_and_edges_)
            keep_ = d.keep_;
        }
    }
 
    scc_and_mark_filter(const scc_info& lower_si,
                        unsigned lower_scc,
                        acc_cond::mark_t cut_sets,
                        const bitvect& keep)
    : scc_and_mark_filter(lower_si, lower_scc, cut_sets)
    {
      keep_ = &keep;
    }
 
    scc_and_mark_filter(const const_twa_graph_ptr& aut,
                        acc_cond::mark_t cut_sets)
      : lower_si_(nullptr), cut_sets_(cut_sets), aut_(aut),
        old_acc_(aut_->get_acceptance())
    {
    }
 
    ~scc_and_mark_filter()
    {
      restore_acceptance();
    }
 
    void override_acceptance(const acc_cond& new_acc)
    {
      std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(new_acc);
      restore_old_acc_ = true;
    }
 
    void restore_acceptance()
    {
      if (!restore_old_acc_)
        return;
      std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(old_acc_);
      restore_old_acc_ = false;
    }
 
    const_twa_graph_ptr get_aut() const
    {
      return aut_;
    }
 
    unsigned start_state() const
    {
      if (lower_si_)
        return lower_si_->one_state_of(lower_scc_);
      return aut_->get_init_state_number();
    }
 
    scc_info::edge_filter get_filter() const
    {
      if (keep_)
        return filter_scc_and_mark_and_edges_;
      if (lower_si_)
        return filter_scc_and_mark_;
      if (cut_sets_)
        return filter_mark_;
      return nullptr;
    }
  };
 
  SPOT_API std::ostream&
  dump_scc_info_dot(std::ostream& out,
                    const_twa_graph_ptr aut, scc_info* sccinfo = nullptr);
 
}