Commit 679be1d7 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

speed up equivalence check for LTL formulas

With this patch reduc.test goes from 4:57 down to 4:06 on my laptop.

* spot/tl/contain.cc (equal): Use are_isomorphic() before testing
for containment.
* spot/twaalgos/are_isomorphic.hh, spot/twaalgos/are_isomorphic.cc:
(are_isomorphic): New static method.
parent 2e15ed95
...@@ -24,6 +24,7 @@ ...@@ -24,6 +24,7 @@
#include <spot/tl/simplify.hh> #include <spot/tl/simplify.hh>
#include <spot/tl/formula.hh> #include <spot/tl/formula.hh>
#include <spot/twaalgos/product.hh> #include <spot/twaalgos/product.hh>
#include <spot/twaalgos/are_isomorphic.hh>
namespace spot namespace spot
{ {
...@@ -104,6 +105,12 @@ namespace spot ...@@ -104,6 +105,12 @@ namespace spot
bool bool
language_containment_checker::equal(formula l, formula g) language_containment_checker::equal(formula l, formula g)
{ {
if (l == g)
return true;
record_* rl = register_formula_(l);
record_* rg = register_formula_(g);
if (isomorphism_checker::are_isomorphic(rl->translation, rg->translation))
return true;
return contained(l, g) && contained(g, l); return contained(l, g) && contained(g, l);
} }
......
...@@ -123,29 +123,40 @@ namespace spot ...@@ -123,29 +123,40 @@ namespace spot
} }
bool bool
isomorphism_checker::is_isomorphic(const const_twa_graph_ptr aut) isomorphism_checker::is_isomorphic_(const const_twa_graph_ptr aut)
{ {
if (trivially_different(ref_, aut)) bool autdet = aut->prop_deterministic();
return false;
if (ref_deterministic_) if (ref_deterministic_)
{ {
if (aut->prop_deterministic() || spot::is_deterministic(aut)) if (autdet || spot::is_deterministic(aut))
{ return are_isomorphic_det(ref_, aut);
return are_isomorphic_det(ref_, aut);
}
} }
else else
{ {
if (aut->prop_deterministic() || if (autdet || nondet_states_ != spot::count_nondet_states(aut))
nondet_states_ != spot::count_nondet_states(aut)) return false;
{
return false;
}
} }
auto tmp = make_twa_graph(aut, twa::prop_set::all()); auto tmp = make_twa_graph(aut, twa::prop_set::all());
spot::canonicalize(tmp); spot::canonicalize(tmp);
return *tmp == *ref_; return *tmp == *ref_;
} }
bool
isomorphism_checker::is_isomorphic(const const_twa_graph_ptr aut)
{
if (trivially_different(ref_, aut))
return false;
return is_isomorphic_(aut);
}
bool
isomorphism_checker::are_isomorphic(const const_twa_graph_ptr ref,
const const_twa_graph_ptr aut)
{
if (trivially_different(ref, aut))
return false;
isomorphism_checker c(ref);
return c.is_isomorphic_(aut);
}
} }
...@@ -25,7 +25,7 @@ ...@@ -25,7 +25,7 @@
namespace spot namespace spot
{ {
/// Check if two automata are isomorphic. /// Check if two automata are isomorphic.
class SPOT_API isomorphism_checker class SPOT_API isomorphism_checker final
{ {
public: public:
isomorphism_checker(const const_twa_graph_ptr ref); isomorphism_checker(const const_twa_graph_ptr ref);
...@@ -45,7 +45,14 @@ namespace spot ...@@ -45,7 +45,14 @@ namespace spot
bool bool
is_isomorphic(const const_twa_graph_ptr aut); is_isomorphic(const const_twa_graph_ptr aut);
/// \ingroup twa_misc
/// \brief Check whether two automata are isomorphic.
static bool are_isomorphic(const const_twa_graph_ptr ref,
const const_twa_graph_ptr aut);
private: private:
bool is_isomorphic_(const const_twa_graph_ptr aut);
twa_graph_ptr ref_; twa_graph_ptr ref_;
bool ref_deterministic_ = false; bool ref_deterministic_ = false;
unsigned nondet_states_ = 0; unsigned nondet_states_ = 0;
......
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