Commit 469d8067 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

gen: another automaton family

* spot/gen/automata.hh, spot/gen/automata.cc,
bin/genaut.cc: Introduce L_DSA.
* tests/core/genaut.test: Add quick test.
parent ae78e1d2
......@@ -13,7 +13,6 @@ 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 two classes of automata.
Library:
......
......@@ -56,6 +56,9 @@ static const argp_option options[] =
{ "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},
{ "l-dsa", gen::AUT_L_DSA, "RANGE", 0,
"A deterministic Streett automaton with 4N states with no "
"equivalent deterministic Rabin automaton of less than n! states.", 0},
RANGE_DOC,
/**************************************************/
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
......
......@@ -132,6 +132,44 @@ namespace spot
aut->prop_semi_deterministic(false);
return aut;
}
static twa_graph_ptr
l_dsa(unsigned n, bdd_dict_ptr dict)
{
if (n < 1 || n > 16)
throw std::runtime_error("l_dsa expects 1 <= n <= 16");
auto aut = make_twa_graph(dict);
bdd a = bdd_ithvar(aut->register_ap("a"));
bdd b = !a;
aut->set_acceptance(2 * n, acc_cond::acc_code::streett(n));
aut->new_states(4 * n);
aut->set_init_state(0);
for (unsigned s = 0; s < n; ++s)
{
unsigned col1 = 4 * s;
unsigned col2 = 4 * s + 1;
unsigned col3 = 4 * s + 2;
unsigned col4 = 4 * s + 3;
aut->new_edge(col1, 2, a, {2 * s});
aut->new_edge(col2, col1, b);
aut->new_edge(col2, std::min(col2 + 4, 4 * n - 3), a);
aut->new_edge(col3, col4, b);
aut->new_edge(col3, std::min(col3 + 4, 4 * n - 2), a);
aut->new_edge(col4, 1, a, {2 * s + 1});
}
aut->prop_state_acc(true);
aut->prop_universal(true);
aut->prop_complete(false);
aut->prop_inherently_weak(false);
aut->prop_stutter_invariant(false);
aut->prop_semi_deterministic(true);
return aut;
}
}
twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n, bdd_dict_ptr dict)
......@@ -151,6 +189,8 @@ namespace spot
return ks_cobuchi(n, dict);
case AUT_L_NBA:
return l_nba(n, dict);
case AUT_L_DSA:
return l_dsa(n, dict);
case AUT_END:
break;
}
......@@ -163,6 +203,7 @@ namespace spot
{
"ks-cobuchi",
"l-nba",
"l-dsa",
};
// Make sure we do not forget to update the above table every
// time a new pattern is added.
......
......@@ -81,6 +81,34 @@ namespace spot
}
\endverbatim */
AUT_L_NBA,
/// \brief DSA hard to convert to DRA.
///
/// Build a deterministic Streett automaton 4n states, and n
/// acceptance pairs, such that an equivalent deterministic Rabin
/// automaton would require at least n! states.
///
/// Only defined for 1<n<=16 because Spot does not support more
/// than 32 acceptance pairs.
///
/// This automaton corresponds to the right part of Fig.2 in the
/// following paper.
/** \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_DSA,
AUT_END
};
......
......@@ -29,7 +29,7 @@ s/[=[].*/=1/p
res=`genaut $opts --stats="--%F=%L"`
test "$opts" = "$res"
genaut --ks-cobuchi=..3 --l-nba=..3 --stats=%s,%e,%t,%c,%g >out
genaut --ks-cobuchi=..3 --l-nba=..3 --l-dsa=..3 --stats=%s,%e,%t,%c,%g >out
cat >expected <<EOF
3,7,16,1,Fin(0)
5,14,32,1,Fin(0)
......@@ -37,6 +37,9 @@ cat >expected <<EOF
4,7,9,1,Inf(0)
7,12,16,1,Inf(0)
10,17,23,1,Inf(0)
4,6,6,1,Fin(0) | Inf(1)
8,12,12,1,(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))
12,18,18,1,(Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5))
EOF
diff out expected
......
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