Commit 17687855 authored by Thibaud Michaud's avatar Thibaud Michaud
Browse files

Wrap are_isomorphic inside a class and optimize when deterministic

* src/bin/autfilt.cc: Use isomorphism_checker.
* src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh: Wrap
are_isomorphic inside a class to keep the canonic version of the first
automaton between two calls, and use a more efficient algorithm in case
both automata are deterministic.
* src/tgbatest/isomorph.test: Add tests for deterministic automata.
parent 1995602d
......@@ -210,6 +210,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 std::unique_ptr<spot::isomorphism_checker> isomorphism_checker = nullptr;
static spot::tgba_digraph_ptr opt_are_isomorphic = nullptr;
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
......@@ -574,10 +575,7 @@ namespace
if (opt_is_deterministic)
matched &= is_deterministic(aut);
if (opt_are_isomorphic)
{
spot::tgba_digraph_ptr tmp = make_tgba_digraph(aut);
matched &= (*spot::canonicalize(tmp) == *opt_are_isomorphic);
}
matched &= isomorphism_checker->is_isomorphic(aut);
if (opt_is_empty)
matched &= aut->is_empty();
......@@ -708,7 +706,8 @@ main(int argc, char** argv)
{
if (opt_merge)
opt_are_isomorphic->merge_transitions();
spot::canonicalize(opt_are_isomorphic);
isomorphism_checker = std::unique_ptr<spot::isomorphism_checker>(
new spot::isomorphism_checker(opt_are_isomorphic));
}
......
......@@ -23,17 +23,127 @@
#include "tgba/tgbagraph.hh"
#include "tgbaalgos/are_isomorphic.hh"
#include "tgbaalgos/canonicalize.hh"
#include "tgbaalgos/isdet.hh"
#include <vector>
#include <queue>
namespace
{
typedef spot::tgba_digraph::graph_t::trans_storage_t tr_t;
bool
tr_t_less_than(const tr_t& t1, const tr_t& t2)
{
return t1.cond.id() < t2.cond.id();
}
bool
operator!=(const tr_t& t1, const tr_t& t2)
{
return t1.cond.id() != t2.cond.id();
}
bool
are_isomorphic_det(const spot::const_tgba_digraph_ptr aut1,
const spot::const_tgba_digraph_ptr aut2)
{
typedef std::pair<unsigned, unsigned> state_pair_t;
std::queue<state_pair_t> workqueue;
workqueue.emplace(aut1->get_init_state_number(),
aut2->get_init_state_number());
std::vector<unsigned> map(aut1->num_states(), -1U);
map[aut1->get_init_state_number()] = aut2->get_init_state_number();
std::vector<tr_t> trans1;
std::vector<tr_t> trans2;
state_pair_t current_state;
while (!workqueue.empty())
{
current_state = workqueue.front();
workqueue.pop();
for (auto& t : aut1->out(current_state.first))
trans1.emplace_back(t);
for (auto& t : aut2->out(current_state.second))
trans2.emplace_back(t);
if (trans1.size() != trans2.size())
return false;
std::sort(trans1.begin(), trans1.end(), tr_t_less_than);
std::sort(trans2.begin(), trans2.end(), tr_t_less_than);
for (auto t1 = trans1.begin(), t2 = trans2.begin();
t1 != trans1.end() && t2 != trans2.end();
++t1, ++t2)
{
if (*t1 != *t2)
{
return false;
}
if (map[t1->dst] == -1U)
{
map[t1->dst] = t2->dst;
workqueue.emplace(t1->dst, t2->dst);
}
else if (map[t1->dst] != t2->dst)
{
return false;
}
}
trans1.clear();
trans2.clear();
}
return true;
}
bool
trivially_different(const spot::const_tgba_digraph_ptr aut1,
const spot::const_tgba_digraph_ptr aut2)
{
return aut1->num_states() != aut2->num_states() ||
aut1->num_transitions() != aut2->num_transitions() ||
aut1->acc().num_sets() != aut2->acc().num_sets();
}
}
namespace spot
{
isomorphism_checker::isomorphism_checker(const const_tgba_digraph_ptr ref)
{
ref_ = make_tgba_digraph(ref);
ref_deterministic_ = ref_->is_deterministic();
if (!ref_deterministic_)
{
nondet_states_ = spot::count_nondet_states(ref_);
ref_deterministic_ = (nondet_states_ == 0);
}
canonicalize(ref_);
}
bool
are_isomorphic(const const_tgba_digraph_ptr aut1,
const const_tgba_digraph_ptr aut2)
isomorphism_checker::is_isomorphic(const const_tgba_digraph_ptr aut)
{
auto tmp1 = make_tgba_digraph(aut1);
auto tmp2 = make_tgba_digraph(aut2);
spot::canonicalize(tmp1);
spot::canonicalize(tmp2);
return *tmp1 == *tmp2;
if (trivially_different(ref_, aut))
return false;
if (ref_deterministic_)
{
if (aut->is_deterministic() || spot::is_deterministic(aut))
{
return are_isomorphic_det(ref_, aut);
}
}
else
{
if (aut->is_deterministic() ||
nondet_states_ != spot::count_nondet_states(aut))
{
return false;
}
}
auto tmp = make_tgba_digraph(aut);
spot::canonicalize(tmp);
return *tmp == *ref_;
}
}
......@@ -25,19 +25,33 @@
namespace spot
{
/// \ingroup tgba_misc
/// \brief Check whether two automata are isomorphic.
///
/// Two automata are considered isomorphic if there exists a bijection f
/// 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
/// condition c and acceptance set A iff there is a transition with
/// condition c and acceptance set A between f(s1) and f(s2) in a2.
/// This can be done simply by checking if
/// canonicalize(aut1) == canonicalize(aut2).
SPOT_API bool
are_isomorphic(const const_tgba_digraph_ptr aut1,
const const_tgba_digraph_ptr aut2);
/// Check if two automata are isomorphic.
class SPOT_API isomorphism_checker
{
public:
isomorphism_checker(const const_tgba_digraph_ptr ref);
/// \ingroup tgba_misc
/// \brief Check whether an automaton is isomorphic to the one passed to
/// the constructor.
///
/// Two automata are considered isomorphic if there exists a bijection f
/// 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
/// condition c and acceptance set A iff there is a transition with
/// condition c and acceptance set A between f(s1) and f(s2) in a2.
/// This can be done simply by checking if
/// canonicalize(aut1) == canonicalize(aut2), but is_isomorphic can do some
/// optimizations in some cases.
bool
is_isomorphic(const const_tgba_digraph_ptr aut);
private:
tgba_digraph_ptr ref_;
bool ref_deterministic_ = false;
unsigned nondet_states_ = 0;
std::vector<tgba_digraph::graph_t::trans_storage_t> reftrans_;
};
}
#endif
......@@ -22,13 +22,17 @@
set -e
for i in 0 1 2 3 4; do
for i in 0 1 2; do
../../bin/randaut a b --seed=$i -S10 --hoa >iso$i
../../bin/autfilt iso$i --randomize --hoa >aut$i
done
for i in 3 4 5; do
../../bin/randaut a b --seed=$i -S10 -D --hoa >iso$i
../../bin/autfilt iso$i --randomize --hoa >aut$i
done
cat aut0 aut1 aut2 aut3 aut4 > all
(for i in 0 1 2 3 4; do
cat aut0 aut1 aut2 aut3 aut4 aut5 > all
(for i in 0 1 2 3 4 5; do
run 0 ../../bin/autfilt all --are-isomorphic iso$i --hoa
done) > output
diff all output
......
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