From 97fdea9d717fe22ef939183b6ef596ee3c68871c Mon Sep 17 00:00:00 2001 From: Thibaud Michaud Date: Wed, 3 Dec 2014 17:54:22 +0100 Subject: [PATCH] =?UTF-8?q?Adding=20function=20to=20test=20if=20two=20b?= =?UTF-8?q?=C3=BCchi=20automata=20are=20isomorphic.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit And add the corresponding --isomorphic=FILENAME option to autfilt. * src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh: New. * src/tgbaalgos/Makefile.am: Add it. * src/bin/autfilt.cc: Add --isomorphic option. * src/tgbatest/isomorph.test: Test it. * src/tgbatest/Makefile.am: Add it. --- src/bin/autfilt.cc | 40 +++++- src/tgbaalgos/Makefile.am | 2 + src/tgbaalgos/are_isomorphic.cc | 215 ++++++++++++++++++++++++++++++++ src/tgbaalgos/are_isomorphic.hh | 41 ++++++ src/tgbatest/Makefile.am | 1 + src/tgbatest/isomorph.test | 136 ++++++++++++++++++++ 6 files changed, 434 insertions(+), 1 deletion(-) create mode 100644 src/tgbaalgos/are_isomorphic.cc create mode 100644 src/tgbaalgos/are_isomorphic.hh create mode 100755 src/tgbatest/isomorph.test diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index b5db0bfcb..db9cda1ae 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -44,6 +44,7 @@ #include "hoaparse/public.hh" #include "tgbaalgos/sccinfo.hh" #include "tgbaalgos/randomize.hh" +#include "tgbaalgos/are_isomorphic.hh" static const char argp_program_doc[] ="\ @@ -60,6 +61,7 @@ Convert, transform, and filter Büchi automata.\n\ #define OPT_SEED 7 #define OPT_PRODUCT 8 #define OPT_MERGE 9 +#define OPT_ISOMORPH 10 static const argp_option options[] = { @@ -127,6 +129,11 @@ static const argp_option options[] = "randomize states and transitions (specify 's' or 't' to" "randomize only states or transitions)", 0 }, /**************************************************/ + { 0, 0, 0, 0, "Filter:", -1 }, + { "isomorph", 'I', "FILENAME", 0, + "print only the automata that are isomorph to the automaton "\ + "described in FILENAME", 0 }, + /**************************************************/ { 0, 0, 0, 0, "Miscellaneous options:", -1 }, { "extra-options", 'x', "OPTS", 0, "fine-tuning options (see spot-x (7))", 0 }, @@ -153,6 +160,7 @@ static int opt_seed = 0; static auto dict = spot::make_bdd_dict(); static spot::tgba_digraph_ptr opt_product = nullptr; static bool opt_merge = false; +static spot::tgba_digraph_ptr opt_isomorph = nullptr; static int to_int(const char* s) @@ -164,6 +172,24 @@ to_int(const char* s) return res; } +// spot::tgba_digraph_ptr +// hoa_parse(const char* filename) +// { +// spot::hoa_parse_error_list pel; +// auto b = spot::make_bdd_dict(); +// auto hp = spot::hoa_stream_parser(filename); +// +// pel.clear(); +// auto haut = hp.parse(pel, b); +// if (!haut && pel.empty()) +// error(2, 0, "no automaton to parse from %s", filename); +// if (spot::format_hoa_parse_errors(std::cerr, filename, pel)) +// error(2, 0, "failed to parse automaton from %s", filename);; +// if (!haut) +// error(2, 0, "failed to read automaton from %s", filename); +// return haut->aut; +// } + static int parse_opt(int key, char* arg, struct argp_state*) { @@ -183,6 +209,15 @@ parse_opt(int key, char* arg, struct argp_state*) format = Hoa; hoa_opt = arg; break; + case 'I': + { + spot::hoa_parse_error_list pel; + auto p = hoa_parse(arg, pel, dict); + if (spot::format_hoa_parse_errors(std::cerr, arg, pel) + || !p || p->aborted) + error(2, 0, "failed to read automaton from %s", arg); + opt_isomorph = std::move(p->aut); + } case 'M': type = spot::postprocessor::Monitor; break; @@ -385,6 +420,9 @@ namespace if (opt_product) aut = spot::product(std::move(aut), opt_product); + if (opt_isomorph && !are_isomorphic(aut, opt_isomorph)) + return 0; + aut = post.run(aut, nullptr); if (randomize_st || randomize_tr) @@ -450,7 +488,7 @@ namespace else if (haut->aborted) err = std::max(err, aborted(haut, filename)); else - process_automaton(haut, filename); + process_automaton(haut, filename); } return err; diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 803f271a2..301efda74 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -28,6 +28,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) tgbaalgosdir = $(pkgincludedir)/tgbaalgos tgbaalgos_HEADERS = \ + are_isomorphic.hh \ bfssteps.hh \ closure.hh \ complete.hh \ @@ -80,6 +81,7 @@ tgbaalgos_HEADERS = \ noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ + are_isomorphic.cc \ bfssteps.cc \ closure.cc \ complete.cc \ diff --git a/src/tgbaalgos/are_isomorphic.cc b/src/tgbaalgos/are_isomorphic.cc new file mode 100644 index 000000000..0f3a7c026 --- /dev/null +++ b/src/tgbaalgos/are_isomorphic.cc @@ -0,0 +1,215 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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 "tgba/tgbagraph.hh" +#include "tgbaalgos/are_isomorphic.hh" +#include +#include +#include +#include "misc/hashfunc.hh" + +namespace +{ + typedef size_t class_t; + typedef std::vector states_t; + typedef std::unordered_map class2states_t; + typedef std::vector state2class_t; + typedef spot::tgba_digraph::graph_t::trans_storage_t trans_storage_t; + + bool + trans_lessthan(trans_storage_t ts1, trans_storage_t ts2) + { + return + ts1.src != ts2.src ? + ts1.src < ts2.src : + ts1.dst != ts2.dst ? + ts1.dst < ts2.dst : + ts1.acc != ts2.acc ? + ts1.acc < ts2.acc : + ts1.cond.id() < ts2.cond.id(); + } + + std::function + trans_lessthan_mapped(const std::vector& mapping) + { + return [mapping](trans_storage_t ts1, + trans_storage_t ts2) + { + return + mapping[ts1.src] != mapping[ts2.src] ? + mapping[ts1.src] < mapping[ts2.src] : + mapping[ts1.dst] != mapping[ts2.dst] ? + mapping[ts1.dst] < mapping[ts2.dst] : + ts1.acc != ts2.acc ? + ts1.acc < ts2.acc : + ts1.cond.id() < ts2.cond.id(); + }; + } + + state2class_t + map_state_class(const spot::const_tgba_digraph_ptr a) + { + state2class_t hashin(a->num_states(), 0); + state2class_t hashout(a->num_states(), 0); + state2class_t state2class(a->num_states()); + + for (auto& t: a->transitions()) + { + if (!a->is_dead_transition(t)) + { + hashout[t.src] ^= spot::wang32_hash(t.cond.id()); + hashout[t.src] ^= spot::wang32_hash(t.acc); + hashin[t.dst] ^= spot::wang32_hash(t.cond.id()); + hashin[t.dst] ^= spot::wang32_hash(t.acc); + } + } + + for (unsigned i = 0; i < a->num_states(); ++i) + // Rehash the ingoing transitions so that the total hash differs for + // different (in, out) pairs of ingoing and outgoing transitions, even if + // the union of in and out is the same. + state2class[i] = spot::wang32_hash(hashin[i]) ^ hashout[i]; + + return state2class; + } + + class2states_t + map_class_states(const spot::const_tgba_digraph_ptr a) + { + unsigned n = a->num_states(); + std::vector res; + class2states_t class2states; + auto state2class = map_state_class(a); + + for (unsigned s = 0; s < n; ++s) + { + class_t c1 = state2class[s]; + (*(class2states.emplace(c1, std::vector()).first)).second. + emplace_back(s); + } + + return class2states; + } + + bool + mapping_from_classes(std::vector& mapping, + class2states_t classes1, + class2states_t classes2) + { + if (classes1.size() != classes2.size()) + return false; + for (auto& p : classes1) + { + if (p.second.size() != classes2[p.first].size()) + return false; + for (unsigned j = 0; j < p.second.size(); ++j) + mapping[p.second[j]] = classes2[p.first][j]; + } + return true; + } + + bool + next_class_permutation(class2states_t& classes) + { + for (auto& p : classes) + if (std::next_permutation(p.second.begin(), p.second.end())) + return true; + return false; + } + + bool + is_isomorphism(const std::vector& mapping, + const spot::const_tgba_digraph_ptr a1, + const spot::const_tgba_digraph_ptr a2) + { + unsigned n = a1->num_states(); + assert(n == a2->num_states()); + std::vector trans1; + std::vector trans2; + + for (auto& t: a1->transitions()) + if (!(a1->is_dead_transition(t))) + trans1.push_back(t); + + for (auto& t: a2->transitions()) + if (!(a2->is_dead_transition(t))) + trans2.push_back(t); + + // Sort the vectors of transitions so that they can be compared. + // To use the same metric, the transitions of a1 have to be mapped to + // a2. + std::sort(trans1.begin(), trans1.end(), trans_lessthan_mapped(mapping)); + std::sort(trans2.begin(), trans2.end(), trans_lessthan); + + for (unsigned i = 0; i < trans1.size(); ++i) + { + auto ts1 = trans1[i]; + auto ts2 = trans2[i]; + if (!(ts2.src == mapping[ts1.src] && + ts2.dst == mapping[ts1.dst] && + ts1.acc == ts2.acc && + ts1.cond.id() == ts2.cond.id())) + { + return false; + } + } + + return true; + } + + bool + are_trivially_different(const spot::const_tgba_digraph_ptr a1, + const spot::const_tgba_digraph_ptr a2) + { + return (a1->num_states() != a2->num_states() || + a1->num_transitions() != a2->num_transitions()); + } +} + +namespace spot +{ + bool + are_isomorphic(const const_tgba_digraph_ptr a1, + const const_tgba_digraph_ptr a2) + { + if (are_trivially_different(a1, a2)) + return false; + unsigned n = a1->num_states(); + assert(n == a2->num_states()); + class2states_t a1_classes = map_class_states(a1); + class2states_t a2_classes = map_class_states(a2); + std::vector mapping(n); + + // Get the first possible mapping between a1 and a2, or return false if + // the number of class or the size of the classes do not match. + if (!(mapping_from_classes(mapping, a1_classes, a2_classes))) + return false; + + while (!is_isomorphism(mapping, a1, a2)) + { + if (!next_class_permutation(a2_classes)) + return false; + mapping_from_classes(mapping, a1_classes, a2_classes); + } + return true; + } +} diff --git a/src/tgbaalgos/are_isomorphic.hh b/src/tgbaalgos/are_isomorphic.hh new file mode 100644 index 000000000..e4b3b38ff --- /dev/null +++ b/src/tgbaalgos/are_isomorphic.hh @@ -0,0 +1,41 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et +// Développement 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 . + +#ifndef SPOT_TGBAALGOS_ARE_ISOMORPHIC_HH +# define SPOT_TGBAALGOS_ARE_ISOMORPHIC_HH + +#include "tgba/tgbagraph.hh" + +namespace spot +{ + /// \ingroup tgba_misc + /// \brief Check whether two automata are isomorphic. + /// Two automata a1 and a2 are said to be isomorphic if there is a bijection + /// f between the states of a1 and a2 such that for every pair of state (s1, + /// s2) of a1: + /// - there is a transition from s1 to s2 iff there is a transition from f(s1) + /// to f(s2) + /// - if there is such a transition, then the acceptance set and acceptance + /// condition are the same on the transition from s1 to s2 and from f(s1) to + /// f(s2) + SPOT_API bool are_isomorphic(const const_tgba_digraph_ptr a1, + const const_tgba_digraph_ptr a2); +} + +#endif diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index aa357cf84..34d0598ed 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -118,6 +118,7 @@ TESTS = \ ltl2ta2.test \ randaut.test \ randtgba.test \ + isomorph.test \ emptchk.test \ emptchke.test \ dfs.test \ diff --git a/src/tgbatest/isomorph.test b/src/tgbatest/isomorph.test new file mode 100755 index 000000000..22bbcada2 --- /dev/null +++ b/src/tgbatest/isomorph.test @@ -0,0 +1,136 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2014 Laboratoire de Recherche et Développement 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 . + + +. ./defs + +set -e + +../../bin/randaut a b -S10 --hoa >filt + +randomize() +{ + for i in `seq 1 5` + do + ../../bin/autfilt --seed=$i --randomize=$1 -F filt --hoa >> autiso + done +} + +randomize s +randomize t +randomize + +run 0 ../../bin/autfilt -F autiso --isomorph filt --hoa >out +test `grep HOA out | wc -l` -eq 15 + +cat >notiso <>notiso <out +test `grep HOA out | wc -l` -eq 0 || exit 1 -- GitLab