zlktree.hh

// -*- coding: utf-8 -*-
// Copyright (C) 2021, 2022 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
//
// 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 <iosfwd>
#include <deque>
#include <memory>
#include <spot/misc/bitvect.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/sccinfo.hh>
 
namespace spot
{
  enum class zielonka_tree_options
  {
    NONE = 0,
    CHECK_RABIN = 1,
    CHECK_STREETT = 2,
    CHECK_PARITY = CHECK_RABIN | CHECK_STREETT,
    ABORT_WRONG_SHAPE = 4,
    MERGE_SUBTREES = 8,
  };
 
#ifndef SWIG
  inline
  bool operator!(zielonka_tree_options me)
  {
    return me == zielonka_tree_options::NONE;
  }
 
  inline
  zielonka_tree_options operator&(zielonka_tree_options left,
                                  zielonka_tree_options right)
  {
    typedef std::underlying_type_t<zielonka_tree_options> ut;
    return static_cast<zielonka_tree_options>(static_cast<ut>(left)
                                              & static_cast<ut>(right));
  }
 
  inline
  zielonka_tree_options operator|(zielonka_tree_options left,
                                  zielonka_tree_options right)
  {
    typedef std::underlying_type_t<zielonka_tree_options> ut;
    return static_cast<zielonka_tree_options>(static_cast<ut>(left)
                                              | static_cast<ut>(right));
  }
 
  inline
  zielonka_tree_options operator-(zielonka_tree_options left,
                                  zielonka_tree_options right)
  {
    typedef std::underlying_type_t<zielonka_tree_options> ut;
    return static_cast<zielonka_tree_options>(static_cast<ut>(left)
                                              & ~static_cast<ut>(right));
  }
#endif
  class SPOT_API zielonka_tree
  {
  public:
    zielonka_tree(const acc_cond& cond,
                  zielonka_tree_options opt = zielonka_tree_options::NONE);
 
    unsigned num_branches() const
    {
      return num_branches_;
    }
 
    unsigned first_branch() const
    {
      return one_branch_;
    }
 
    std::pair<unsigned, unsigned>
    step(unsigned branch, acc_cond::mark_t colors) const;
 
    bool is_even() const
    {
      return is_even_;
    }
 
    bool has_rabin_shape() const
    {
      return has_rabin_shape_;
    }
 
    bool has_streett_shape() const
    {
      return has_streett_shape_;
    }
 
    bool has_parity_shape() const
    {
      return has_streett_shape_ && has_rabin_shape_;
    }
 
    void dot(std::ostream&) const;
 
    struct zielonka_node
    {
      unsigned parent;
      unsigned next_sibling = 0;
      unsigned first_child = 0;
      unsigned level;
      acc_cond::mark_t colors;
    };
    std::vector<zielonka_node> nodes_;
  private:
    unsigned one_branch_ = 0;
    unsigned num_branches_ = 0;
    bool is_even_;
    bool empty_is_even_;
    bool has_rabin_shape_ = true;
    bool has_streett_shape_ = true;
  };
 
  SPOT_API
  twa_graph_ptr zielonka_tree_transform(const const_twa_graph_ptr& aut);
 
 
  enum class acd_options
  {
    NONE = 0,
    CHECK_RABIN = 1,
    CHECK_STREETT = 2,
    CHECK_PARITY = CHECK_RABIN | CHECK_STREETT,
    ABORT_WRONG_SHAPE = 4,
    ORDER_HEURISTIC = 8,
  };
 
#ifndef SWIG
  inline
  bool operator!(acd_options me)
  {
    return me == acd_options::NONE;
  }
 
  inline
  acd_options operator&(acd_options left, acd_options right)
  {
    typedef std::underlying_type_t<acd_options> ut;
    return static_cast<acd_options>(static_cast<ut>(left)
                                    & static_cast<ut>(right));
  }
 
  inline
  acd_options operator|(acd_options left, acd_options right)
  {
    typedef std::underlying_type_t<acd_options> ut;
    return static_cast<acd_options>(static_cast<ut>(left)
                                    | static_cast<ut>(right));
  }
 
  inline
  acd_options operator-(acd_options left, acd_options right)
  {
    typedef std::underlying_type_t<acd_options> ut;
    return static_cast<acd_options>(static_cast<ut>(left)
                                    & ~static_cast<ut>(right));
  }
 
#endif
 
  class SPOT_API acd
  {
  public:
    acd(const scc_info& si, acd_options opt = acd_options::NONE);
    acd(const const_twa_graph_ptr& aut, acd_options opt = acd_options::NONE);
 
    ~acd();
 
    std::pair<unsigned, unsigned>
    step(unsigned branch, unsigned edge) const;
 
    unsigned state_step(unsigned node, unsigned edge) const;
 
    std::vector<unsigned> edges_of_node(unsigned n) const;
 
    unsigned node_count() const
    {
      return nodes_.size();
    }
 
    bool node_acceptance(unsigned n) const;
 
    unsigned node_level(unsigned n) const;
 
    const acc_cond::mark_t& node_colors(unsigned n) const;
 
    bool is_even(unsigned scc) const
    {
      if (scc >= scc_count_)
        report_invalid_scc_number(scc, "is_even");
      return trees_[scc].is_even;
    }
 
    bool is_even() const
    {
      return is_even_;
    }
 
    unsigned first_branch(unsigned state) const;
 
    unsigned scc_max_level(unsigned scc) const
    {
      if (scc >= scc_count_)
        report_invalid_scc_number(scc, "scc_max_level");
      return trees_[scc].max_level;
    }
 
    bool has_rabin_shape() const;
 
    bool has_streett_shape() const;
 
    bool has_parity_shape() const;
 
    const const_twa_graph_ptr get_aut() const
    {
      return aut_;
    }
 
    void dot(std::ostream&, const char* id = nullptr) const;
 
  private:
    const scc_info* si_;
    bool own_si_ = false;
    acd_options opt_;
 
    // This structure is used to represent one node in the ACD forest.
    // The tree use a left-child / right-sibling representation
    // (called here first_child, next_sibling).  Each node
    // additionally store a level (depth in the ACD, adjusted at the
    // end of the construction so that all node on the same level have
    // the same parity), the SCC (which is also it's tree number), and
    // some bit vectors representing the edges and states of that
    // node.  Those bit vectors are as large as the original
    // automaton, and they are shared among nodes from the different
    // trees of the ACD forest (since each tree correspond to a
    // different SCC, they cannot share state or edges).
    struct acd_node
    {
      unsigned parent;
      unsigned next_sibling = 0;
      unsigned first_child = 0;
      unsigned level;
      unsigned scc;
      acc_cond::mark_t colors;
      unsigned minstate;
      bitvect& edges;
      bitvect& states;
      acd_node(bitvect& e, bitvect& s) noexcept
        : edges(e), states(s)
      {
      }
    };
    // We store the nodes in a deque so that their addresses do not
    // change.
    std::deque<acd_node> nodes_;
    // Likewise for bitvectors: this is the support for all edge vectors
    // and state vectors used in acd_node.
    std::deque<std::unique_ptr<bitvect>> bitvectors;
    // Information about a tree of the ACD.  Each treinserte correspond
    // to an SCC.
    struct scc_data
    {
      bool trivial;             // whether the SCC is trivial we do
                                // not store any node for trivial
                                // SCCs.
      unsigned root = 0;        // root node of a non-trivial SCC.
      bool is_even;             // parity of the tree, used at the end
                                // of the construction to adjust
                                // levels.
      unsigned max_level = 0;   // Maximum level for this SCC.
      unsigned num_nodes = 0;   // Number of node in this tree.  This
                                // is only used to share bitvectors
                                // between SCC: node with the same
                                // "rank" in each tree share the same
                                // bitvectors.
    };
    std::vector<scc_data> trees_;
    unsigned scc_count_;
    const_twa_graph_ptr aut_;
    // Information about the overall ACD.
    bool is_even_;
    bool has_rabin_shape_ = true;
    bool has_streett_shape_ = true;
 
    // Build the ACD structure.  Called by the constructors.
    void build_();
 
    // leftmost branch of \a node that contains \a state
    unsigned leftmost_branch_(unsigned node, unsigned state) const;
 
#ifndef SWIG
    [[noreturn]] static
    void report_invalid_scc_number(unsigned num, const char* fn);
    [[noreturn]] static void report_need_opt(const char* opt);
    [[noreturn]] static void report_empty_acd(const char* fn);
#endif
  };
 
  SPOT_API
  twa_graph_ptr acd_transform(const const_twa_graph_ptr& aut,
                              bool colored = false);
  SPOT_API
  twa_graph_ptr acd_transform_sbacc(const const_twa_graph_ptr& aut,
                                    bool colored = false,
                                    bool order_heuristic = true);
}