From 7b0e15a7fb5eed76fb8cbd3ad766e87800b5b4bf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 18 Sep 2024 12:04:23 +0200 Subject: [PATCH] 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 | 9 ++ bin/autfilt.cc | 35 ++++++- doc/spot.bib | 14 +++ python/spot/impl.i | 2 + spot/twaalgos/Makefile.am | 6 +- spot/twaalgos/mcs.cc | 196 ++++++++++++++++++++++++++++++++++++++ spot/twaalgos/mcs.hh | 63 ++++++++++++ tests/Makefile.am | 1 + tests/core/mcs.test | 180 ++++++++++++++++++++++++++++++++++ 9 files changed, 501 insertions(+), 5 deletions(-) create mode 100644 spot/twaalgos/mcs.cc create mode 100644 spot/twaalgos/mcs.hh create mode 100755 tests/core/mcs.test diff --git a/NEWS b/NEWS index 0da353568..9a5c0a1c7 100644 --- a/NEWS +++ b/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 diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 0252a0562..a6ef46d57 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -65,6 +65,7 @@ #include #include #include +#include #include #include #include @@ -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> 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::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) { diff --git a/doc/spot.bib b/doc/spot.bib index bc2b39a1f..ba25b5070 100644 --- a/doc/spot.bib +++ b/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 diff --git a/python/spot/impl.i b/python/spot/impl.i index 1f9c11fde..2291730ed 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -133,6 +133,7 @@ #include #include #include +#include #include #include #include @@ -742,6 +743,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index b5993aaef..8e5b929d0 100644 --- a/spot/twaalgos/Makefile.am +++ b/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 \ diff --git a/spot/twaalgos/mcs.cc b/spot/twaalgos/mcs.cc new file mode 100644 index 000000000..b73016a15 --- /dev/null +++ b/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 . + +#include "config.h" +#include +#include +#include + +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 vertex; + // set is an array of doubly-linked list built using vertex elements + std::vector 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 + 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> 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 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 order = maximum_cardinality_search(a, tie); + a->defrag_states(order, order.size()); + return a; + } +} diff --git a/spot/twaalgos/mcs.hh b/spot/twaalgos/mcs.hh new file mode 100644 index 000000000..76a67b74a --- /dev/null +++ b/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 . + +#pragma once + +#include +#include +#include + +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 + 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); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index 898bcccd8..6f7abf994 100644 --- a/tests/Makefile.am +++ b/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 \ diff --git a/tests/core/mcs.test b/tests/core/mcs.test new file mode 100755 index 000000000..da654a547 --- /dev/null +++ b/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 . + +. ./defs +set -e + +cat >in.hoa < out1.hoa +autfilt --mcs=scc in.hoa > out2.hoa + +cat >expected1.hoa <expected2.hoa <