split.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 <vector>
 
namespace spot
{
  SPOT_API twa_graph_ptr split_edges(const const_twa_graph_ptr& aut);
 
#ifndef SWIG
  // pseudo container that we use to iterate over
  // the items of LABELS that are compatible with COND.
  template<bool subsumed>
  struct SPOT_API edge_separator_filter
    {
      edge_separator_filter(const std::vector<bdd>& labels, bdd cond)
      : labels_(labels), cond_(cond)
      {
      }
 
      class iterator
      {
        std::vector<bdd>::const_iterator pos_;
        std::vector<bdd> const& labels_;
        bdd cond_;
 
      public:
        iterator(const std::vector<bdd>& labels, bdd cond)
          : labels_(labels), cond_(cond)
        {
          pos_ = labels_.begin();
          next();
        }
 
        iterator& operator++()
        {
          ++pos_;
          next();
          return *this;
        }
 
        void next()
        {
          // If subsumed is true, we want to match the labels
          // that imply the current condition.  Otherwise we
          // want to match the labels that are compatible.
          while (pos_ != labels_.end() &&
                 ((subsumed && !bdd_implies(*pos_, cond_))
                  || (!subsumed && (*pos_ & cond_) == bddfalse)))
            ++pos_;
        }
 
        bdd operator*() const
        {
          if (subsumed)
            return *pos_;
          else
            return *pos_ & cond_;
        }
 
        bool operator==(const iterator& other) const
        {
          return pos_ == other.pos_;
        }
 
        bool operator!=(const iterator& other) const
        {
          return pos_ != other.pos_;
        }
 
        bool operator==(std::vector<bdd>::const_iterator pos) const
        {
          return pos_ == pos;
        }
 
        bool operator!=(std::vector<bdd>::const_iterator pos) const
        {
          return pos_ != pos;
        }
      };
 
      iterator begin() const
      {
        return iterator(labels_, cond_);
      }
 
      std::vector<bdd>::const_iterator end() const
      {
        return labels_.end();
      }
 
    private:
      const std::vector<bdd>& labels_;
      bdd cond_;
    };
#endif
 
 
  class SPOT_API edge_separator
  {
  public:
    void add_to_basis(bdd label);
    void add_to_basis(const const_twa_graph_ptr& aut);
    bool add_to_basis(const const_twa_graph_ptr& aut,
                      unsigned long max_label);
    twa_graph_ptr separate_implying(const const_twa_graph_ptr& aut);
    twa_graph_ptr separate_compat(const const_twa_graph_ptr& aut);
#ifndef SWIG
    edge_separator_filter<true> separate_implying(bdd label)
    {
      return {basis_, label};
    }
    edge_separator_filter<false> separate_compat(bdd label)
    {
      return {basis_, label};
    }
#endif
 
    unsigned basis_size() const
    {
      return basis_.size();
    }
 
    const std::vector<bdd>& basis() const
    {
      return basis_;
    }
 
  private:
    std::vector<bdd> basis_{bddtrue};
    std::set<formula> aps_;
  };
 
  SPOT_API twa_graph_ptr separate_edges(const const_twa_graph_ptr& aut);
}