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

gen: introduce a new automaton family

* spot/gen/automata.cc, spot/gen/automata.hh: Define AUT_L_NBA.
* bin/genaut.cc (--l-nba): New option.
* bin/man/genaut.x, doc/org/genaut.org, NEWS: Document it.
* tests/python/gen.py, tests/core/genaut.test: Test it.
parent 649793df
......@@ -13,7 +13,7 @@ New in spot 2.3.3.dev (not yet released)
- genaut is a binary to produce families of automata defined in the
literature (in the same way as we have genltl for LTL formulas).
It currently features only one class of automata.
It currently features only two classes of automata.
Library:
......
......@@ -53,6 +53,9 @@ static const argp_option options[] =
{ "ks-cobuchi", gen::AUT_KS_COBUCHI, "RANGE", 0,
"A co-Büchi automaton with 2N+1 states for which any equivalent "
"deterministic co-Büchi automaton has at least 2^N/(2N+1) states.", 0},
{ "l-nba", gen::AUT_L_NBA, "RANGE", 0,
"A Büchi automaton with 3N+1 states whose complementary Streett "
"automaton needs at least n! states.", 0},
RANGE_DOC,
/**************************************************/
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
......
......@@ -7,7 +7,11 @@ Prefixes used in pattern names refer to the following papers:
.TP
ks
D. Kuperberg, M. Skrzypczak: On Determinisation of Good-for-Games
Automata. Proceddings of ICALP'15.
Automata. Proceedings of ICALP'15.
.TP
l
C. Löding: Optimal Bounds for Transformations of ω-Automata.
Proceedings of FSTTCS'99.
[SEE ALSO]
.BR autfilt (1),
......
......@@ -17,6 +17,9 @@ genaut --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d'
: --ks-cobuchi=RANGE A co-Büchi automaton with 2N+1 states for which
: any equivalent deterministic co-Büchi automaton
: has at least 2^N/(2N+1) states.
: --l-nba=RANGE A Büchi automaton with 3N+1 states whose
: complementary Streett automaton needs at least n!
: states.
By default, the output format is [[file:hoa.org][HOA]], but this can be controlled using
......
......@@ -88,6 +88,39 @@ namespace spot
aut->prop_state_acc(true);
return aut;
}
static twa_graph_ptr
l_nba(unsigned n, bdd_dict_ptr dict)
{
if (n == 0)
throw std::runtime_error("l_nba expects a positive argument");
auto aut = make_twa_graph(dict);
bdd p1 = bdd_ithvar(aut->register_ap("a"));
bdd p2 = bdd_ithvar(aut->register_ap("b"));
bdd a = p1 - p2;
bdd b = p2 - p1;
bdd s = p1 & p2;
bdd all = p1 | p2;
aut->new_states(3 * n + 1);
aut->set_init_state(1);
aut->set_buchi();
aut->prop_state_acc(true);
aut->new_acc_edge(0, n + 1, a);
aut->new_edge(2 * n + 1, 0, b);
for (unsigned s = 1; s <= n; ++s)
{
aut->new_edge(s + n, std::min(s + n + 1, 2 * n), a);
aut->new_edge(s + n, s, b);
aut->new_edge(s, s, all);
aut->new_edge(s, s + 2 * n, a);
aut->new_edge(std::min(s + 2 * n + 1, 3 * n), s + 2 * n, a);
}
return aut;
}
}
twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n, bdd_dict_ptr dict)
......@@ -105,6 +138,8 @@ namespace spot
// Keep this alphabetically-ordered!
case AUT_KS_COBUCHI:
return ks_cobuchi(n, dict);
case AUT_L_NBA:
return l_nba(n, dict);
case AUT_END:
break;
}
......@@ -116,6 +151,7 @@ namespace spot
static const char* const class_name[] =
{
"ks-cobuchi",
"l-nba",
};
// Make sure we do not forget to update the above table every
// time a new pattern is added.
......
......@@ -31,23 +31,56 @@ namespace spot
AUT_BEGIN = 256,
/// \brief A family of co-Büchi automata.
///
/// ks_cobuchi(n) is a co-Büchi automaton of size 2n+1 that is
/// good-for-games and that has no equivalent deterministic co-Büchi
/// automaton with less than 2^n / (2n+1) states.
/// For details and other classes, see:
///
/// @InProceedings{kuperberg2015determinisation,
/// author={Kuperberg, Denis and Skrzypczak, Micha{\l}},
/// title={On Determinisation of Good-for-Games Automata},
/// booktitle={International Colloquium on Automata, Languages, and
/// Programming},
/// pages={299--310},
/// year={2015},
/// organization={Springer}
/// }
/// Builds a co-Büchi automaton of size 2n+1 that is
/// good-for-games and that has no equivalent deterministic
/// co-Büchi automaton with less than 2^n / (2n+1) states.
///
/// Only defined for n>0
///
/** \verbatim
@InProceedings{ kuperberg.15.icalp,
author = {Denis Kuperberg and Micha{\l} Skrzypczak },
title = {On Determinisation of Good-for-Games Automata},
booktitle = {Proceedings of the 42nd International Colloquium on
Automata, Languages, and Programming (ICALP'15)},
pages = {299--310},
year = {2015},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 9135,
doi = {10.1007/978-3-662-47666-6_24}
}
\endverbatim */
AUT_KS_COBUCHI = AUT_BEGIN,
/// \brief Hard-to-complement non-deterministic Büchi automata
///
/// Build a non-deterministic Büchi automaton with 3n+1 states
/// and whose complementary language requires an automaton with
/// at least n! states if Streett acceptance is used.
///
/// Only defined for n>0. The automaton constructed corresponds
/// to the right part of Fig.1 in the following paper, except
/// that only state q_1 is initial. (The fact that states q_2,
/// q_3, ..., and q_n are not initial as in the paper does not
/// change the recognized language.)
///
/** \verbatim
@InProceedings{loding.99.fstts,
author = {Christof L{\"o}ding},
title = {Optimal Bounds for Transformations of
$\omega$-Automata},
booktitle = {Proceedings of the 19th Conference on Foundations of
Software Technology and Theoretical Computer Science
(FSTTCS'99)},
year = 1999,
publisher = {Springer},
pages = {97--109},
series = {Lecture Notes in Computer Science},
volume = 1738,
doi = {10.1007/3-540-46691-6_8}
}
\endverbatim */
AUT_L_NBA,
AUT_END
};
......
......@@ -29,13 +29,18 @@ s/[=[].*/=1/p
res=`genaut $opts --stats="--%F=%L"`
test "$opts" = "$res"
genaut --ks-cobuchi=..3 --stats=%s,%e,%t,%c,%g >out
genaut --ks-cobuchi=..3 --l-nba=..3 --stats=%s,%e,%t,%c,%g >out
cat >expected <<EOF
3,7,16,1,Fin(0)
5,14,32,1,Fin(0)
7,20,48,1,Fin(0)
4,7,9,1,Inf(0)
7,12,16,1,Inf(0)
10,17,23,1,Inf(0)
EOF
diff out expected
genaut --ks-cobuchi=0 2>err && exit 1
grep positive err
genaut --l-nba=0 2>err && exit 1
grep positive err
......@@ -31,7 +31,7 @@ assert k2.num_states() == 5
# the type returned by spot.gen.ks_cobuchi() is the correct one.
assert 'to_str' in dir(k2)
k3 = gen.aut_pattern(gen.AUT_KS_COBUCHI, 3)
k3 = gen.aut_pattern(gen.AUT_L_NBA, 3)
assert k2.get_dict() == k3.get_dict()
try:
......@@ -63,3 +63,7 @@ else:
assert 40 == sum(p.size() for p in gen.ltl_patterns((gen.LTL_OR_G, 1, 5),
(gen.LTL_GH_Q, 3),
gen.LTL_EH_PATTERNS))
assert 32 == sum(p.num_states()
for p in gen.aut_patterns((gen.AUT_L_NBA, 1, 3),
(gen.AUT_KS_COBUCHI, 5)))
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