Commit 324b5a8a authored by Akim Demaille's avatar Akim Demaille
Browse files

are-equivalent: use realtime

* vcsn/algos/are-equivalent.hh: Here.
* doc/notebooks/automaton.is_equivalent.ipynb: Update.
* tests/bin/test.py (CHECK_EQUIV): No longer call normalize.
(normalize): Use realtime instead of proper().
* tests/python/efsm.py (check): Use normalize: we have a case
where we compare lan x lan against lal x lal, and since we
don't have synchronize yet, it fails.
parent d98b5361
......@@ -6,6 +6,9 @@ Vcsn, in reverse chronological order. On occasions, significant changes in
the internal API may also be documented.
## 2015-03-21
### are-equivalent: now uses realtime
One may, finally, compare LAL, LAN, and LAW automata.
### join: improvements
The "join" of tuplesets now works properly, so one may, for instance,
add automata on A? x B and A x B? to get an automata on A? x B?.
......@@ -16,8 +19,10 @@ infix `or` operator.
In [2]: c1 = vcsn.context('lat<lal_char(a), lan_char(x)>, z'); c1
Out[2]: {a} × ({x})? → ℤ
In [3]: c2 = vcsn.context('lat<lan_char(b), lal_char(y)>, q'); c2
Out[3]: ({b})? × {y} → ℚ
In [4]: c1 | c2
Out[4]: ({a,b})? × ({x,y})? → ℚ
......
......@@ -112,6 +112,11 @@ check whether is_proper first. However are-equivalent actually uses
a.realtime() = a.letterize().proper(), and a.realtime() checks first if the
automaton is not already realtime.
Update: now we do call realtime (which includes proper). We should also use
synchronize: currently we can't compare a lan x lan with a lal x lal, even
if the former does not have (\e, \e) transitions. Once we do, remove the
calls to "normalize" in tests/python/efsm.py:check.
** are-equivalent
We cannot compare Z-automaton.is_equivalent(B-automaton), because the
B-automaton does not support -1 * aut. However we must perform these
......
This diff is collapsed.
......@@ -151,22 +151,18 @@ def CHECK_EQ(expected, effective, loc = None):
def normalize(a):
'''Turn automaton `a` into something we can check equivalence with.'''
a = a.strip()
if 'nullableset' in str(a.context()):
a = a.proper()
# Eliminate nullablesets if there are that remain.
to = re.sub(r'nullableset<(lal_char\(.*?\)|letterset<char_letters\(.*?\)>)>', r'\1', a.context().format('text'))
a = a.strip().realtime()
# Eliminate nullablesets if there are that remain. If there are
# \e that remains, the following conversion _will_ reject it.
to = re.sub(r'nullableset<(lal_char\(.*?\)|letterset<char_letters\(.*?\)>)>',
r'\1',
a.context().format('text'))
return a.automaton(vcsn.context(to))
def CHECK_EQUIV(a1, a2):
'''Check that `a1` and `a2` are equivalent. Also works for
expressions.'''
if isinstance(a1, vcsn.automaton):
a1 = normalize(a1)
if isinstance(a2, vcsn.automaton):
a2 = normalize(a2)
# Cannot compute equivalence on Zmin, approximate with shortest.
if str(a1.context()).endswith('zmin') or str(a2.context()).endswith('zmin'):
num = 10
......
......@@ -36,7 +36,7 @@ def check(aut, fefsm):
CHECK_EQ(aut, aut2)
CHECK_EQ(efsm, aut2.format('efsm'))
else:
CHECK_EQUIV(aut, aut2)
CHECK_EQUIV(aut, normalize(aut2))
# Check that OpenFST accepts and reproduces our EFSM files.
if have_ofst:
......@@ -44,7 +44,7 @@ def check(aut, fefsm):
if aut.is_standard():
CHECK_EQ(aut, aut3)
else:
CHECK_EQUIV(aut, aut3)
CHECK_EQUIV(aut, normalize(aut3))
else:
SKIP('OpenFST is missing')
......
......@@ -6,6 +6,7 @@
#include <vcsn/algos/determinize.hh>
#include <vcsn/algos/derived-term.hh>
#include <vcsn/algos/left-mult.hh>
#include <vcsn/algos/letterize.hh> // rea
#include <vcsn/algos/product.hh>
#include <vcsn/algos/reduce.hh>
#include <vcsn/algos/strip.hh>
......@@ -24,14 +25,14 @@ namespace vcsn
template <typename Aut1, typename Aut2>
auto
are_equivalent(const Aut1& a1, const Aut2& a2)
-> vcsn::enable_if_t<(labelset_t_of<Aut1>::is_free()
&& std::is_same<weightset_t_of<Aut1>, b>::value
&& labelset_t_of<Aut2>::is_free()
-> vcsn::enable_if_t<(std::is_same<weightset_t_of<Aut1>, b>::value
&& std::is_same<weightset_t_of<Aut2>, b>::value),
bool>
{
return (is_useless(difference(a1, a2))
&& is_useless(difference(a2, a1)));
const auto& l = realtime(a1);
const auto& r = realtime(a2);
return (is_useless(difference(l, r))
&& is_useless(difference(r, l)));
}
......@@ -45,10 +46,12 @@ namespace vcsn
true))
{
const auto& ws2 = *a2->weightset();
// d = a1 U -a2.
auto d = union_a(a1,
const auto& l = realtime(a1);
const auto& r = realtime(a2);
// d = l + -r.
auto d = union_a(l,
left_mult(ws2.sub(ws2.zero(), ws2.one()),
a2));
r));
return is_empty(reduce(d));
}
......
Supports Markdown
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