Commit 1995602d authored by Thibaud Michaud's avatar Thibaud Michaud
Browse files

Adding function to canonicalize an automaton.

* src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh,
src/bin/autfilt.cc: are_isomorphic now uses canonicalize. It returns a
bool, because the mapping cannot be deduced easily from the
canonicalized automaton.
* src/graph/graph.hh: Add equality operator to trans_storage_t
for easy comparison of transition vectors.
* src/tgba/tgbagraph.hh: Add equality operator to tgba_graph_trans_data
and to tgba_digraph.
* src/tgbaalgos/canonicalize.cc, src/tgbaalgos/canonicalize.hh:
New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/isomorph.test: Test them.
parent b83d6d7f
...@@ -53,6 +53,7 @@ ...@@ -53,6 +53,7 @@
#include "tgbaalgos/reducerun.hh" #include "tgbaalgos/reducerun.hh"
#include "tgbaalgos/word.hh" #include "tgbaalgos/word.hh"
#include "tgbaalgos/are_isomorphic.hh" #include "tgbaalgos/are_isomorphic.hh"
#include "tgbaalgos/canonicalize.hh"
static const char argp_program_doc[] ="\ static const char argp_program_doc[] ="\
...@@ -573,7 +574,10 @@ namespace ...@@ -573,7 +574,10 @@ namespace
if (opt_is_deterministic) if (opt_is_deterministic)
matched &= is_deterministic(aut); matched &= is_deterministic(aut);
if (opt_are_isomorphic) if (opt_are_isomorphic)
matched &= !are_isomorphic(aut, opt_are_isomorphic).empty(); {
spot::tgba_digraph_ptr tmp = make_tgba_digraph(aut);
matched &= (*spot::canonicalize(tmp) == *opt_are_isomorphic);
}
if (opt_is_empty) if (opt_is_empty)
matched &= aut->is_empty(); matched &= aut->is_empty();
...@@ -700,8 +704,13 @@ main(int argc, char** argv) ...@@ -700,8 +704,13 @@ main(int argc, char** argv)
if (jobs.empty()) if (jobs.empty())
jobs.emplace_back("-", true); jobs.emplace_back("-", true);
if (opt_are_isomorphic && opt_merge) if (opt_are_isomorphic)
opt_are_isomorphic->merge_transitions(); {
if (opt_merge)
opt_are_isomorphic->merge_transitions();
spot::canonicalize(opt_are_isomorphic);
}
spot::srand(opt_seed); spot::srand(opt_seed);
......
...@@ -183,10 +183,17 @@ namespace spot ...@@ -183,10 +183,17 @@ namespace spot
// This might be costly if the destination is a vector // This might be costly if the destination is a vector
if (dst < other.dst) if (dst < other.dst)
return true; return true;
if (dst < other.dst) if (dst > other.dst)
return false; return false;
return this->data() < other.data(); return this->data() < other.data();
} }
bool operator==(const trans_storage& other) const
{
return src == other.src &&
dst == other.dst &&
this->data() == other.data();
}
}; };
////////////////////////////////////////////////// //////////////////////////////////////////////////
......
...@@ -96,6 +96,12 @@ namespace spot ...@@ -96,6 +96,12 @@ namespace spot
return false; return false;
return acc < other.acc; return acc < other.acc;
} }
bool operator==(const tgba_graph_trans_data& other) const
{
return cond.id() == other.cond.id() &&
acc == other.acc;
}
}; };
...@@ -458,6 +464,17 @@ namespace spot ...@@ -458,6 +464,17 @@ namespace spot
return state_is_accepting(state_number(s)); return state_is_accepting(state_number(s));
} }
bool operator==(const tgba_digraph& aut) const
{
if (num_states() != aut.num_states() ||
num_transitions() != aut.num_transitions() ||
acc().num_sets() != aut.acc().num_sets())
return false;
auto& trans1 = transition_vector();
auto& trans2 = aut.transition_vector();
return std::equal(trans1.begin() + 1, trans1.end(),
trans2.begin() + 1);
}
}; };
inline tgba_digraph_ptr make_tgba_digraph(const bdd_dict_ptr& dict) inline tgba_digraph_ptr make_tgba_digraph(const bdd_dict_ptr& dict)
......
...@@ -30,6 +30,7 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos ...@@ -30,6 +30,7 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos
tgbaalgos_HEADERS = \ tgbaalgos_HEADERS = \
are_isomorphic.hh \ are_isomorphic.hh \
bfssteps.hh \ bfssteps.hh \
canonicalize.hh \
closure.hh \ closure.hh \
complete.hh \ complete.hh \
compsusp.hh \ compsusp.hh \
...@@ -83,6 +84,7 @@ noinst_LTLIBRARIES = libtgbaalgos.la ...@@ -83,6 +84,7 @@ noinst_LTLIBRARIES = libtgbaalgos.la
libtgbaalgos_la_SOURCES = \ libtgbaalgos_la_SOURCES = \
are_isomorphic.cc \ are_isomorphic.cc \
bfssteps.cc \ bfssteps.cc \
canonicalize.cc \
closure.cc \ closure.cc \
complete.cc \ complete.cc \
compsusp.cc \ compsusp.cc \
......
...@@ -22,182 +22,18 @@ ...@@ -22,182 +22,18 @@
#include "tgba/tgbagraph.hh" #include "tgba/tgbagraph.hh"
#include "tgbaalgos/are_isomorphic.hh" #include "tgbaalgos/are_isomorphic.hh"
#include <unordered_map> #include "tgbaalgos/canonicalize.hh"
#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;
struct transition
{
unsigned src;
unsigned dst;
int cond;
spot::acc_cond::mark_t acc;
transition(unsigned src, unsigned dst, int cond, spot::acc_cond::mark_t acc)
: src(src), dst(dst), cond(cond), acc(acc)
{
}
bool operator==(const transition& o) const
{
return src == o.src && dst == o.dst && cond == o.cond && acc == o.acc;
}
};
static bool
trans_lessthan(const transition& ts1, const transition& 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 < ts2.cond;
}
static 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())
{
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];
// XOR the initial state's hash with a pseudo random value so that it is
// in its own class.
state2class[a->get_init_state_number()] ^= 2654435761U;
return state2class;
}
static 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];
auto& states =
class2states.emplace(c1, std::vector<unsigned>()).first->second;
states.emplace_back(s);
}
return class2states;
}
static 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)
{
auto& c2 = classes2[p.first];
if (p.second.size() != c2.size())
return false;
auto ps = p.second.size();
for (unsigned j = 0; j < ps; ++j)
mapping[p.second[j]] = c2[j];
}
return true;
}
static 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;
}
static 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()
|| a1->acc().num_sets() != a2->acc().num_sets());
}
}
namespace spot namespace spot
{ {
std::vector<unsigned> bool
are_isomorphic(const const_tgba_digraph_ptr a1, are_isomorphic(const const_tgba_digraph_ptr aut1,
const const_tgba_digraph_ptr a2) const const_tgba_digraph_ptr aut2)
{ {
if (are_trivially_different(a1, a2)) auto tmp1 = make_tgba_digraph(aut1);
return {}; auto tmp2 = make_tgba_digraph(aut2);
unsigned n = a1->num_states(); spot::canonicalize(tmp1);
assert(n == a2->num_states()); spot::canonicalize(tmp2);
class2states_t a1_classes = map_class_states(a1); return *tmp1 == *tmp2;
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 {};
unsigned tend = a1->num_transitions();
assert(tend == a2->num_transitions());
// a2 is our reference automaton. Keep a sorted list of its
// transition for easy comparison.
std::vector<transition> trans2;
trans2.reserve(tend);
for (auto& t: a2->transitions())
trans2.emplace_back(t.src, t.dst, t.acc, t.cond.id());
std::sort(trans2.begin(), trans2.end(), trans_lessthan);
std::vector<transition> trans1;
trans1.reserve(tend);
for (;;)
{
// Check if current mapping matches the reference automaton
trans1.clear();
for (auto& t: a1->transitions())
trans1.emplace_back(mapping[t.src], mapping[t.dst],
t.acc, t.cond.id());
std::sort(trans1.begin(), trans1.end(), trans_lessthan);
if (trans1 == trans2)
return mapping;
// Consider next mapping
if (!next_class_permutation(a2_classes))
return {};
mapping_from_classes(mapping, a1_classes, a2_classes);
}
} }
} }
...@@ -26,16 +26,18 @@ ...@@ -26,16 +26,18 @@
namespace spot namespace spot
{ {
/// \ingroup tgba_misc /// \ingroup tgba_misc
/// \brief Check whether two automate are isormorphic. /// \brief Check whether two automata are isomorphic.
/// ///
/// Return an isomorphism between a1 and a2 if such an isomorphism /// Two automata are considered isomorphic if there exists a bijection f
/// exists. Otherwise, return an empty vector. /// between the states of a1 and the states of a2 such that for any pair of
/// /// states (s1, s2) of a1, there is a transition from s1 to s2 with
/// \return a vector indexed by states of \a a1, and containing /// condition c and acceptance set A iff there is a transition with
/// states of \a a2. /// condition c and acceptance set A between f(s1) and f(s2) in a2.
SPOT_API std::vector<unsigned> /// This can be done simply by checking if
are_isomorphic(const const_tgba_digraph_ptr a1, /// canonicalize(aut1) == canonicalize(aut2).
const const_tgba_digraph_ptr a2); SPOT_API bool
are_isomorphic(const const_tgba_digraph_ptr aut1,
const const_tgba_digraph_ptr aut2);
} }
#endif #endif
// -*- coding: utf-8 -*-
// Copyright (C) 2014 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/>.
#include "canonicalize.hh"
#include "tgba/tgbagraph.hh"
#include <set>
#include <vector>
namespace
{
typedef std::pair<spot::tgba_digraph::graph_t::trans_data_t, unsigned>
trans_sig_t;
struct signature_t
{
std::vector<trans_sig_t> ingoing;
std::vector<trans_sig_t> outgoing;
unsigned classnum;
bool
operator<(const signature_t& o) const
{
return ingoing != o.ingoing ? ingoing < o.ingoing :
outgoing != o.outgoing ? outgoing < o.outgoing :
classnum < o.classnum;
}
};
typedef std::map<signature_t, std::vector<unsigned>> sig2states_t;
static sig2states_t
sig_to_states(spot::tgba_digraph_ptr aut, std::vector<unsigned>& state2class)
{
std::vector<signature_t> signature(aut->num_states(), signature_t());
for (auto& t : aut->transitions())
{
signature[t.dst].ingoing.emplace_back(t.data(), state2class[t.src]);
signature[t.src].outgoing.emplace_back(t.data(), state2class[t.dst]);
}
sig2states_t sig2states;
for (unsigned s = 0; s < aut->num_states(); ++s)
{
std::sort(signature[s].ingoing.begin(), signature[s].ingoing.end());
std::sort(signature[s].outgoing.begin(), signature[s].outgoing.end());
signature[s].classnum = state2class[s];
sig2states[signature[s]].push_back(s);
}
return sig2states;
}
}
namespace spot
{
tgba_digraph_ptr
canonicalize(tgba_digraph_ptr aut)
{
std::vector<unsigned> state2class(aut->num_states(), 0);
state2class[aut->get_init_state_number()] = 1;
size_t distinct_classes = 2;
sig2states_t sig2states = sig_to_states(aut, state2class);
while (sig2states.size() != distinct_classes &&
sig2states.size() != aut->num_states())
{
distinct_classes = sig2states.size();
unsigned classnum = 0;
for (auto& s: sig2states)
{
for (auto& state: s.second)
state2class[state] = classnum;
++classnum;
}
sig2states = sig_to_states(aut, state2class);
}
unsigned classnum = 0;
for (auto& s: sig2states)
for (auto& state: s.second)
state2class[state] = classnum++;
auto& g = aut->get_graph();
g.rename_states_(state2class);
aut->set_init_state(state2class[aut->get_init_state_number()]);
g.sort_transitions_();
g.chain_transitions_();
return aut;
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2014 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/>.
#ifndef SPOT_TGBAALGOS_CANONICALIZE_HH
# define SPOT_TGBAALGOS_CANONICALIZE_HH
#include "tgba/tgbagraph.hh"
namespace spot
{
/// \ingroup tgba_misc
/// \brief Reorder the states and transitions of aut in a way that will be the
/// same for every isomorphic automata.
SPOT_API tgba_digraph_ptr canonicalize(tgba_digraph_ptr aut);
}
#endif
...@@ -23,7 +23,7 @@ ...@@ -23,7 +23,7 @@
set -e set -e
for i in 0 1 2 3 4; do for i in 0 1 2 3 4; do
../../bin/randaut a --seed=$i -S4 --hoa >iso$i ../../bin/randaut a b --seed=$i -S10 --hoa >iso$i
../../bin/autfilt iso$i --randomize --hoa >aut$i ../../bin/autfilt iso$i --randomize --hoa >aut$i
done done
...@@ -32,3 +32,73 @@ cat aut0 aut1 aut2 aut3 aut4 > all ...@@ -32,3 +32,73 @@ cat aut0 aut1 aut2 aut3 aut4 > all
run 0 ../../bin/autfilt all --are-isomorphic iso$i --hoa run 0 ../../bin/autfilt all --are-isomorphic iso$i --hoa
done) > output done) > output
diff all output diff all output
# Test if two isomorphic automata with different initial states are detected.
cat >aut1 <<EOF
HOA: v1
name: "1"
States: 4
Start: 1
AP: 0
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0 [t] 1 [t] 1
State: 1 [t] 2 [t] 2
State: 2 [t] 3 [t] 3
State: 3 [t] 0 [t] 0
--END--
EOF
cat >aut2 <<EOF
HOA: v1
name: "1"
States: 4
Start: 0
AP: 0
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0 [t] 1 [t] 1
State: 1 [t] 3 [t] 3
State: 3 [t] 2 [t] 2
State: 2 [t] 0 [t] 0
--END--
EOF
# Check that the number of ingoing and outgoing transitions of a state matters,
# even if they behave similarly.
cat >aut3 <<EOF
HOA: v1
States: 3
Start: 0
AP: 0
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0 [t] 1 [t] 2
State: 1 [t] 1 [t] 1
State: 2 [t] 2
--END--
EOF
cat >aut4 <<EOF
HOA: v1
States: 3
Start: 0
AP: 0
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0 [t] 1 [t] 2
State: 1 [t] 1
State: 2 [t] 2 [t] 2
--END--
EOF
run 0 ../../bin/autfilt aut1 --are-isomorphic aut2
run 0 ../../bin/autfilt aut3 --are-isomorphic aut4
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment