implement maximum cardinality search

* spot/twaalgos/mcs.cc, spot/twaalgos/mcs.hh: New files.
* spot/twaalgos/Makefile.am: Add them.
* python/spot/impl.i: Include mcs.hh.
* bin/autfilt.cc: Add --mcs option.
* NEWS: Mention it.
* doc/spot.bib: Add reference.
* tests/core/mcs.test: New file.
* tests/Makefile.am: Add it.

NEWS

@@ -51,6 +51,10 @@ New in spot 2.12.0.dev (not yet released)
   - autfilt learned --track-formula=F to label states with formulas
     derived from F.  (This is more precise on deterministic automata.)
 
+  - autfilt learned --mcs[=any|scc] to reorder states according to a
+    maximum cardinality search.  The argument specifies how to break
+    ties.
+
   - ltlfilt learned --pi1, --sigma1, --delta1, --pi2, --sigma2, and
     --delta2 to filter according to classes Π₁,Σ₁,Δ₁,Π₂,Σ₂, and Δ₂.
 
@@ -96,6 +100,11 @@ New in spot 2.12.0.dev (not yet released)
   - twa_graph::defrag_states(num) no longer require num[i]≤i; num
     can now describe a permutation of the state numbers.
 
+  - spot::maximum_cardinality_search() and
+    spot::maximum_cardinality_search_reorder_here() are new function
+    to compute (and apply) an ordering of state based on a maximum
+    cardinality search.
+
   Bug fixes:
 
   - Generating random formulas without any unary opertor would very

bin/autfilt.cc

@@ -65,6 +65,7 @@
 #include <spot/twaalgos/langmap.hh>
 #include <spot/twaalgos/mask.hh>
 #include <spot/twaalgos/matchstates.hh>
+#include <spot/twaalgos/mcs.hh>
 #include <spot/twaalgos/product.hh>
 #include <spot/twaalgos/randomize.hh>
 #include <spot/twaalgos/remfin.hh>
@@ -137,6 +138,7 @@ enum {
   OPT_KEEP_STATES,
   OPT_KILL_STATES,
   OPT_MASK_ACC,
+  OPT_MCS,
   OPT_MERGE,
   OPT_NONDET_STATES,
   OPT_PARTIAL_DEGEN,
@@ -296,6 +298,9 @@ static const argp_option options[] =
     WORD_DOC,
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Transformations:", 7 },
+    { "mcs-order", OPT_MCS, "any|scc", OPTION_ARG_OPTIONAL,
+      "reorder states using a maximum cardinality search; use option to"
+      " specify how to break ties", 0 },
     { "merge-transitions", OPT_MERGE, nullptr, 0,
       "merge transitions with same destination and acceptance", 0 },
     { "product", OPT_PRODUCT_AND, "FILENAME", 0,
@@ -522,6 +527,21 @@ static bool const aliases_types[] =
 };
 ARGMATCH_VERIFY(aliases_args, aliases_types);
 
+spot::mcs_tie_break opt_mcs_tie = spot::MCS_TIE_ANY;
+static char const* const mcs_args[] =
+{
+  "any",
+  "scc",
+  nullptr,
+};
+static spot::mcs_tie_break const mcs_types[] =
+{
+  spot::MCS_TIE_ANY,
+  spot::MCS_TIE_SCC,
+};
+ARGMATCH_VERIFY(mcs_args, mcs_types);
+
+
 enum acc_type {
   ACC_Any = 0,
   ACC_Given,
@@ -653,6 +673,7 @@ static struct opt_t
   std::vector<std::pair<spot::twa_graph_ptr, unsigned>> hl_words;
 }* opt;
 
+static bool opt_mcs = false;
 static bool opt_merge = false;
 static bool opt_has_univ_branching = false;
 static bool opt_has_exist_branching = false;
@@ -1107,9 +1128,6 @@ parse_opt(int key, char* arg, struct argp_state*)
         opt_rem_dead = true;
         break;
       }
-    case OPT_MERGE:
-      opt_merge = true;
-      break;
     case OPT_MASK_ACC:
       {
         for (auto res : to_longs(arg))
@@ -1125,6 +1143,14 @@ parse_opt(int key, char* arg, struct argp_state*)
           }
         break;
       }
+    case OPT_MCS:
+      opt_mcs = true;
+      if (arg)
+        opt_mcs_tie = XARGMATCH("--mcs", arg, mcs_args, mcs_types);
+      break;
+    case OPT_MERGE:
+      opt_merge = true;
+      break;
     case OPT_NONDET_STATES:
       opt_nondet_states = parse_range(arg, 0, std::numeric_limits<int>::max());
       opt_nondet_states_set = true;
@@ -1744,6 +1770,9 @@ namespace
           if (auto run = spot::product(aut, word_aut)->accepting_run())
             run->project(aut)->highlight(color);
 
+      if (opt_mcs)
+        spot::maximum_cardinality_search_reorder_here(aut, opt_mcs_tie);
+
       timer.stop();
       if (opt->uniq)
         {

doc/spot.bib

@@ -1085,6 +1085,20 @@
   doi		= {10.1007/978-3-642-16612-9_33}
 }
 
+@Article{	  tarjan.84.sicomp,
+  author	= {Robert E. Tarjan and Mihalis Yannakakis},
+  title		= {Simple linear-time algorithms to test chordality of
+		  graphs, test acyclicity of hypergraphs, and selectively
+		  reduce acyclic hypergraphs},
+  journal	= {SIAM Journal on Computing},
+  year		= {1984},
+  volume	= {13},
+  number	= {3},
+  pages		= {566--579},
+  month		= aug,
+  doi		= {10.1137/0213035}
+}
+
 @TechReport{	  tauriainen.00.tr,
   author	= {Heikki Tauriainen},
   title		= {Automated Testing of {B\"u}chi Automata Translators for

python/spot/impl.i

@@ -133,6 +133,7 @@
 #include <spot/twaalgos/determinize.hh>
 #include <spot/twaalgos/magic.hh>
 #include <spot/twaalgos/matchstates.hh>
+#include <spot/twaalgos/mcs.hh>
 #include <spot/twaalgos/minimize.hh>
 #include <spot/twaalgos/mealy_machine.hh>
 #include <spot/twaalgos/neverclaim.hh>
@@ -742,6 +743,7 @@ def state_is_accepting(self, src) -> "bool":
 %include <spot/twaalgos/langmap.hh>
 %include <spot/twaalgos/magic.hh>
 %include <spot/twaalgos/matchstates.hh>
+%include <spot/twaalgos/mcs.hh>
 %include <spot/twaalgos/minimize.hh>
 %include <spot/twaalgos/mealy_machine.hh>
 %include <spot/twaalgos/neverclaim.hh>

spot/twaalgos/Makefile.am

@@ -37,6 +37,7 @@ twaalgos_HEADERS = \
   compsusp.hh \
   contains.hh \
   copy.hh \
+  couvreurnew.hh \
   cycles.hh \
   dbranch.hh \
   deadends.hh \
@@ -65,9 +66,9 @@ twaalgos_HEADERS = \
   magic.hh \
   mask.hh \
   matchstates.hh \
+  mcs.hh \
   minimize.hh \
   mealy_machine.hh \
-  couvreurnew.hh \
   neverclaim.hh \
   parity.hh \
   postproc.hh \
@@ -114,6 +115,7 @@ libtwaalgos_la_SOURCES = \
   complement.cc \
   compsusp.cc \
   contains.cc \
+  couvreurnew.cc \
   cycles.cc \
   dbranch.cc \
   deadends.cc \
@@ -141,9 +143,9 @@ libtwaalgos_la_SOURCES = \
   magic.cc \
   mask.cc \
   matchstates.cc \
+  mcs.cc \
   minimize.cc \
   mealy_machine.cc \
-  couvreurnew.cc \
   ndfs_result.hxx \
   neverclaim.cc \
   parity.cc \

spot/twaalgos/mcs.cc

@@ -0,0 +1,196 @@
+// -*- 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/>.
+
+#include "config.h"
+#include <spot/twa/twagraph.hh>
+#include <spot/twaalgos/mcs.hh>
+#include <spot/twaalgos/sccinfo.hh>
+
+namespace spot
+{
+  namespace
+  {
+    struct mcs_vertex
+    {
+      // Each vertex is part of a circular doubly-linked list.
+      mcs_vertex* prev = nullptr;
+      mcs_vertex* next = nullptr;
+      // The weight of a vertex, initially 0, is the number of
+      // neighbors that already have an MCS-number.  The weight is -1
+      // if the vertex itself has an MCS-number.
+      int weight = 0;
+    };
+
+    struct mcs_data
+    {
+      std::vector<mcs_vertex> vertex;
+      // set is an array of doubly-linked list built using vertex elements
+      std::vector<mcs_vertex*> set;
+
+      // Initialy, all n vertices are in set[0]
+      mcs_data(unsigned n)
+        : vertex(n), set(n, nullptr)
+      {
+        // make a circular list of everything in vertex
+        vertex[0].prev = &vertex[n - 1];
+        for (unsigned i = 0; i < n - 1; i++)
+          {
+            vertex[i].next = &vertex[i + 1];
+            vertex[i + 1].prev = &vertex[i];
+          }
+        vertex[n - 1].next = &vertex[0];
+        set[0] = &vertex[0];
+      }
+
+      void remove_vertex(unsigned vertex_i, unsigned from_set)
+      {
+        mcs_vertex* v = &vertex[vertex_i];
+        mcs_vertex* prev = v->prev;
+        mcs_vertex* next = v->next;
+        prev->next = next;
+        next->prev = prev;
+        if (v == set[from_set])
+          set[from_set] = (v == next) ? nullptr : next;
+      }
+
+      void insert_vertex(unsigned vertex_i, unsigned to_set)
+      {
+        mcs_vertex* v = &vertex[vertex_i];
+        mcs_vertex* next = set[to_set];
+        if (next == nullptr)
+          {
+            v->prev = v;
+            v->next = v;
+            set[to_set] = v;
+          }
+        else
+          {
+            mcs_vertex* prev = next->prev;
+            v->prev = prev;
+            v->next = next;
+            prev->next = v;
+            next->prev = v;
+          }
+      }
+
+      void increase_vertex_weight(unsigned vertex_i)
+      {
+        mcs_vertex* v = &vertex[vertex_i];
+        if (v->weight >= 0)
+          {
+            remove_vertex(vertex_i, v->weight);
+            ++v->weight;
+            insert_vertex(vertex_i, v->weight);
+          }
+      }
+
+      unsigned select_any_vertex(unsigned from_set)
+      {
+        mcs_vertex* start = set[from_set];
+        assert(start);
+        return start - &vertex[0];
+      }
+
+      scc_info* si;
+      unsigned select_best_vertex_scc(unsigned from_set)
+      {
+        mcs_vertex* start = set[from_set];
+        assert(start);
+        assert(si);
+        unsigned best = start - &vertex[0];
+        unsigned best_scc = si->scc_of(best);
+        mcs_vertex* v = start->next;
+        while (v != start)
+          {
+            unsigned i = v - &vertex[0];
+            if (si->scc_of(i) > best_scc)
+              {
+                best = i;
+                best_scc = si->scc_of(i);
+              }
+            v = v->next;
+          }
+        return best;
+      }
+    };
+  }
+
+  /// \brief Return an ordering of the vertices computed by
+  /// a maximum cardinality search.
+  ///
+  /// Unlike Tarjan's paper \cite tarjan.84.sicomp , where states are
+  /// numbered from N to 1, this number the states from 0 to N-1,
+  /// starting from the initial state.  The next number is assigned to
+  /// a state that maximizes the number of already-numbered neighbors.
+  std::vector<unsigned>
+  maximum_cardinality_search(const const_twa_graph_ptr& a, mcs_tie_break tie)
+  {
+    unsigned n = a->num_states();
+    mcs_data data(n);
+
+    // We need to compute the neighbors of each state independently of
+    // the orientation of the edges.
+    std::vector<std::set<unsigned>> neighbors(n);
+    for (auto& e: a->edges())
+      {
+        neighbors[e.src].insert(e.dst);
+        neighbors[e.dst].insert(e.src);
+      }
+
+    // How to break ties when selecting the next vertex?
+    unsigned (mcs_data::* pick_state)(unsigned) = &mcs_data::select_any_vertex;
+    if (tie == MCS_TIE_SCC)
+      {
+        data.si = new scc_info(a, scc_info_options::NONE);
+        pick_state = &mcs_data::select_best_vertex_scc;
+      }
+
+    std::vector<unsigned> order(n, 0U); // order is α in Tarjan's paper
+    unsigned index = 0;              // index is n-i in Tarjan's paper
+    int max_weight = 0;         // max_weight is j in Tarjan's paper
+    auto number_state = [&](unsigned i)
+    {
+      order[i] = index++;
+      int& w = data.vertex[i].weight;
+      data.remove_vertex(i, w);
+      w = -1;
+      for (unsigned j: neighbors[i])
+        data.increase_vertex_weight(j);
+      ++max_weight;
+    };
+
+    unsigned init = a->get_init_state_number();
+    number_state(init);
+
+    while (index < n)
+      {
+        while (max_weight > 0 && data.set[max_weight] == nullptr)
+          --max_weight;
+        number_state((data.*pick_state)(max_weight));
+      }
+    return order;
+  }
+
+  twa_graph_ptr
+  maximum_cardinality_search_reorder_here(twa_graph_ptr a, mcs_tie_break tie)
+  {
+    std::vector<unsigned> order = maximum_cardinality_search(a, tie);
+    a->defrag_states(order, order.size());
+    return a;
+  }
+}

spot/twaalgos/mcs.hh

@@ -0,0 +1,63 @@
+// -*- 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/misc/common.hh>
+#include <spot/twa/fwd.hh>
+#include <vector>
+
+namespace spot
+{
+  enum mcs_tie_break
+    {
+      ///\brief Break ties by picking the first possible state.
+      MCS_TIE_ANY = 0,
+      /// \brief Break ties by picking states from the "highest" SCCs
+      ///
+      /// This is based on the topological ordering of SCCs computed
+      /// by scc_info.  The initial state is always in the highest
+      /// SCC, and the smallest SCC has no exit.
+      MCS_TIE_SCC,
+    };
+
+
+  /// \brief Return an ordering of the vertices computed by
+  /// a maximum cardinality search.
+  ///
+  /// Unlike Tarjan's paper \cite tarjan.84.sicomp , where states are
+  /// numbered from N to 1, this numbers the states from 0 to N-1,
+  /// starting from the initial state.  The next number is assigned to
+  /// a state that maximizes the number of already-numbered neighbors.
+  ///
+  /// This version returns a vector such that RESULTS[I] is the rank
+  /// of state I in the computed order.
+  ///
+  /// \param tie specify how to break ties.
+  SPOT_API std::vector<unsigned>
+  maximum_cardinality_search(const const_twa_graph_ptr& a,
+                             mcs_tie_break tie = MCS_TIE_ANY);
+
+  /// \brief Reorder the state of \a a according to the order
+  /// computed by maximum_cardinality_search().
+  ///
+  /// This works in place and return the same automaton.
+  SPOT_API twa_graph_ptr
+  maximum_cardinality_search_reorder_here(twa_graph_ptr a,
+                                          mcs_tie_break tie = MCS_TIE_ANY);
+}

tests/Makefile.am

@@ -280,6 +280,7 @@ TESTS_twa = \
   core/randomize.test \
   core/lbttparse.test \
   core/ltlf.test \
+  core/mcs.test \
   core/scc.test \
   core/sccdot.test \
   core/sccif.test \

tests/core/mcs.test

@@ -0,0 +1,180 @@
+#!/bin/sh
+# -*- 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/>.
+
+. ./defs
+set -e
+
+cat >in.hoa <<EOF
+HOA: v1
+name: "G(FGb & F((c & Xd) | (!c & X!d))) | X(Ga & Fd)"
+States: 6
+Start: 3
+AP: 4 "b" "c" "a" "d"
+acc-name: Rabin 1
+Acceptance: 2 Fin(0) & Inf(1)
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[!0&1&2&!3] 0 {0}
+[1&!2] 1
+[0&1&2&!3] 0
+[!1&!2] 2
+[2&3] 5
+[0&!1&2&!3] 4
+[!0&!1&2&!3] 4 {0}
+State: 1
+[!0&1] 1 {0}
+[0&1&3] 1 {1}
+[0&1&!3] 1
+[0&!1&!3] 2
+[0&!1&3] 2 {1}
+[!0&!1] 2 {0}
+State: 2
+[!0&1] 1 {0}
+[0&!1&3] 2
+[0&!1&!3] 2 {1}
+[0&1&!3] 1 {1}
+[0&1&3] 1
+[!0&!1] 2 {0}
+State: 3
+[1] 0
+[!1] 4
+State: 4
+[1&!2] 1
+[!1&!2] 2
+[!0&!1&2&!3] 4 {0}
+[!0&1&2&!3] 0 {0}
+[0&!1&2&!3] 4 {1}
+[0&1&2&!3] 0 {1}
+[2&3] 5
+State: 5
+[1&!2] 1
+[!1&!2] 2
+[2] 5 {1}
+--END--
+EOF
+
+autfilt --mcs in.hoa > out1.hoa
+autfilt --mcs=scc in.hoa > out2.hoa
+
+cat >expected1.hoa <<EOF
+HOA: v1
+name: "G(FGb & F((c & Xd) | (!c & X!d))) | X(Ga & Fd)"
+States: 6
+Start: 0
+AP: 4 "b" "c" "a" "d"
+acc-name: Rabin 1
+Acceptance: 2 Fin(0) & Inf(1)
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[1] 1
+[!1] 2
+State: 1
+[!0&1&2&!3] 1 {0}
+[1&!2] 3
+[0&1&2&!3] 1
+[!1&!2] 4
+[2&3] 5
+[0&!1&2&!3] 2
+[!0&!1&2&!3] 2 {0}
+State: 2
+[1&!2] 3
+[!1&!2] 4
+[!0&!1&2&!3] 2 {0}
+[!0&1&2&!3] 1 {0}
+[0&!1&2&!3] 2 {1}
+[0&1&2&!3] 1 {1}
+[2&3] 5
+State: 3
+[!0&1] 3 {0}
+[0&1&3] 3 {1}
+[0&1&!3] 3
+[0&!1&!3] 4
+[0&!1&3] 4 {1}
+[!0&!1] 4 {0}
+State: 4
+[!0&1] 3 {0}
+[0&!1&3] 4
+[0&!1&!3] 4 {1}
+[0&1&!3] 3 {1}
+[0&1&3] 3
+[!0&!1] 4 {0}
+State: 5
+[1&!2] 3
+[!1&!2] 4
+[2] 5 {1}
+--END--
+EOF
+
+cat >expected2.hoa <<EOF
+HOA: v1
+name: "G(FGb & F((c & Xd) | (!c & X!d))) | X(Ga & Fd)"
+States: 6
+Start: 0
+AP: 4 "b" "c" "a" "d"
+acc-name: Rabin 1
+Acceptance: 2 Fin(0) & Inf(1)
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[1] 1
+[!1] 2
+State: 1
+[!0&1&2&!3] 1 {0}
+[1&!2] 4
+[0&1&2&!3] 1
+[!1&!2] 5
+[2&3] 3
+[0&!1&2&!3] 2
+[!0&!1&2&!3] 2 {0}
+State: 2
+[1&!2] 4
+[!1&!2] 5
+[!0&!1&2&!3] 2 {0}
+[!0&1&2&!3] 1 {0}
+[0&!1&2&!3] 2 {1}
+[0&1&2&!3] 1 {1}
+[2&3] 3
+State: 3
+[1&!2] 4
+[!1&!2] 5
+[2] 3 {1}
+State: 4
+[!0&1] 4 {0}
+[0&1&3] 4 {1}
+[0&1&!3] 4
+[0&!1&!3] 5
+[0&!1&3] 5 {1}
+[!0&!1] 5 {0}
+State: 5
+[!0&1] 4 {0}
+[0&!1&3] 5
+[0&!1&!3] 5 {1}
+[0&1&!3] 4 {1}
+[0&1&3] 4
+[!0&!1] 5 {0}
+--END--
+EOF
+
+diff expected1.hoa out1.hoa
+diff expected2.hoa out2.hoa