Adding function to test if two büchi automata are isomorphic.
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.
This commit is contained in:
Thibaud Michaud
Alexandre Duret-Lutz
parent
61edf7f41d
commit
97fdea9d71
6 changed files with 434 additions and 1 deletions
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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 \
|
||||
|
|
|
|||
215
src/tgbaalgos/are_isomorphic.cc
Normal file
215
src/tgbaalgos/are_isomorphic.cc
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include "tgba/tgbagraph.hh"
|
||||
#include "tgbaalgos/are_isomorphic.hh"
|
||||
#include <unordered_map>
|
||||
#include <vector>
|
||||
#include <algorithm>
|
||||
#include "misc/hashfunc.hh"
|
||||
|
||||
namespace
|
||||
{
|
||||
typedef size_t class_t;
|
||||
typedef std::vector<unsigned> states_t;
|
||||
typedef std::unordered_map<class_t, states_t> class2states_t;
|
||||
typedef std::vector<class_t> 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<bool(trans_storage_t ts1, trans_storage_t ts2)>
|
||||
trans_lessthan_mapped(const std::vector<unsigned>& 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<states_t> 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<unsigned>()).first)).second.
|
||||
emplace_back(s);
|
||||
}
|
||||
|
||||
return class2states;
|
||||
}
|
||||
|
||||
bool
|
||||
mapping_from_classes(std::vector<unsigned>& 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<unsigned>& 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<trans_storage_t> trans1;
|
||||
std::vector<trans_storage_t> 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<unsigned> 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;
|
||||
}
|
||||
}
|
||||
41
src/tgbaalgos/are_isomorphic.hh
Normal file
41
src/tgbaalgos/are_isomorphic.hh
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#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
|
||||
|
|
@ -118,6 +118,7 @@ TESTS = \
|
|||
ltl2ta2.test \
|
||||
randaut.test \
|
||||
randtgba.test \
|
||||
isomorph.test \
|
||||
emptchk.test \
|
||||
emptchke.test \
|
||||
dfs.test \
|
||||
|
|
|
|||
136
src/tgbatest/isomorph.test
Executable file
136
src/tgbatest/isomorph.test
Executable file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
. ./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 <<EOF
|
||||
HOA: v1
|
||||
States: 10
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: all
|
||||
Acceptance: 0 t
|
||||
properties: trans-labels explicit-labels state-acc
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&1] 1
|
||||
[0&1] 2
|
||||
State: 1
|
||||
[!0&!1] 2
|
||||
[0&!1] 3
|
||||
[!0&1] 4
|
||||
State: 2
|
||||
[0&1] 5
|
||||
[0&!1] 1
|
||||
State: 3
|
||||
[!0&!1] 5
|
||||
[!0&!1] 1
|
||||
[!0&1] 0
|
||||
[0&!1] 6
|
||||
State: 4
|
||||
[0&1] 5
|
||||
[0&1] 0
|
||||
[!0&1] 7
|
||||
State: 5
|
||||
[0&1] 5
|
||||
[!0&1] 8
|
||||
State: 6
|
||||
[0&1] 9
|
||||
State: 7
|
||||
[0&!1] 9
|
||||
[0&1] 1
|
||||
State: 8
|
||||
[!0&1] 8
|
||||
[0&!1] 5
|
||||
State: 9
|
||||
[!0&!1] 5
|
||||
[!0&1] 8
|
||||
--END--
|
||||
EOF
|
||||
|
||||
cat >>notiso <<EOF
|
||||
HOA: v1
|
||||
States: 10
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: all
|
||||
Acceptance: 0 t
|
||||
properties: trans-labels explicit-labels state-acc
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&1] 1
|
||||
State: 1
|
||||
[!0&1] 2
|
||||
[!0&1] 3
|
||||
[!0&1] 4
|
||||
[!0&1] 5
|
||||
[!0&1] 6
|
||||
State: 2
|
||||
[0&1] 7
|
||||
[!0&1] 0
|
||||
State: 3
|
||||
[!0&!1] 0
|
||||
[!0&1] 6
|
||||
[0&!1] 8
|
||||
State: 4
|
||||
[!0&1] 3
|
||||
[!0&!1] 9
|
||||
[!0&!1] 0
|
||||
State: 5
|
||||
[0&1] 0
|
||||
State: 6
|
||||
[!0&!1] 9
|
||||
State: 7
|
||||
[0&!1] 0
|
||||
[!0&1] 7
|
||||
[!0&!1] 6
|
||||
State: 8
|
||||
[0&1] 6
|
||||
[!0&!1] 1
|
||||
[!0&!1] 0
|
||||
State: 9
|
||||
[0&!1] 7
|
||||
[!0&1] 2
|
||||
[0&1] 1
|
||||
--END--
|
||||
EOF
|
||||
|
||||
run 0 ../../bin/autfilt -F notiso --isomorph filt --hoa >out
|
||||
test `grep HOA out | wc -l` -eq 0 || exit 1
|
||||
Loading…
Add table
Add a link
Reference in a new issue