Commit e7df182a authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

gen: rename KS_COBUCHI to KS_NCA for consistency

* spot/gen/automata.cc, spot/gen/automata.hh, bin/genaut.cc: Rename
the enum, function, and command-line option.
* tests/core/genaut.test, tests/python/gen.ipynb, tests/python/gen.py:
Adjust test cases.
* doc/org/genaut.org: Adjust doc.
parent 6cd6802a
...@@ -50,7 +50,7 @@ static const argp_option options[] = ...@@ -50,7 +50,7 @@ static const argp_option options[] =
/**************************************************/ /**************************************************/
// Keep this alphabetically sorted (expect for aliases). // Keep this alphabetically sorted (expect for aliases).
{ nullptr, 0, nullptr, 0, "Pattern selection:", 1}, { nullptr, 0, nullptr, 0, "Pattern selection:", 1},
{ "ks-cobuchi", gen::AUT_KS_COBUCHI, "RANGE", 0, { "ks-nca", gen::AUT_KS_NCA, "RANGE", 0,
"A co-Büchi automaton with 2N+1 states for which any equivalent " "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}, "deterministic co-Büchi automaton has at least 2^N/(2N+1) states.", 0},
{ "l-nba", gen::AUT_L_NBA, "RANGE", 0, { "l-nba", gen::AUT_L_NBA, "RANGE", 0,
......
...@@ -14,9 +14,12 @@ genaut --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d' ...@@ -14,9 +14,12 @@ genaut --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: --ks-cobuchi=RANGE A co-Büchi automaton with 2N+1 states for which : --ks-nca=RANGE A co-Büchi automaton with 2N+1 states for which
: any equivalent deterministic co-Büchi automaton : any equivalent deterministic co-Büchi automaton
: has at least 2^N/(2N+1) states. : has at least 2^N/(2N+1) states.
: --l-dsa=RANGE A deterministic Streett automaton with 4N states
: with no equivalent deterministic Rabin automaton
: of less than n! states.
: --l-nba=RANGE A Büchi automaton with 3N+1 states whose : --l-nba=RANGE A Büchi automaton with 3N+1 states whose
: complementary Streett automaton needs at least n! : complementary Streett automaton needs at least n!
: states. : states.
...@@ -28,7 +31,7 @@ By default, the output format is [[file:hoa.org][HOA]], but this can be controll ...@@ -28,7 +31,7 @@ By default, the output format is [[file:hoa.org][HOA]], but this can be controll
For instance: For instance:
#+NAME: kscobuchi2 #+NAME: kscobuchi2
#+BEGIN_SRC sh :results verbatim :exports code #+BEGIN_SRC sh :results verbatim :exports code
genaut --ks-cobuchi=2 --dot genaut --ks-nca=2 --dot
#+END_SRC #+END_SRC
#+BEGIN_SRC dot :file kscobuchi2.png :cmdline -Tpng :var txt=kscobuchi2 :exports results #+BEGIN_SRC dot :file kscobuchi2.png :cmdline -Tpng :var txt=kscobuchi2 :exports results
...@@ -43,12 +46,12 @@ value), =N..M= (all values between N and M included), or =..M= (all ...@@ -43,12 +46,12 @@ value), =N..M= (all values between N and M included), or =..M= (all
values between 1 and M included). values between 1 and M included).
#+BEGIN_SRC sh :results verbatim :exports code #+BEGIN_SRC sh :results verbatim :exports code
genaut --ks-cobuchi=..5 --stats='%F=%L has %s states' genaut --ks-nca=..5 --stats='%F=%L has %s states'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: ks-cobuchi=1 has 3 states : ks-nca=1 has 3 states
: ks-cobuchi=2 has 5 states : ks-nca=2 has 5 states
: ks-cobuchi=3 has 7 states : ks-nca=3 has 7 states
: ks-cobuchi=4 has 9 states : ks-nca=4 has 9 states
: ks-cobuchi=5 has 11 states : ks-nca=5 has 11 states
...@@ -28,10 +28,10 @@ namespace spot ...@@ -28,10 +28,10 @@ namespace spot
namespace namespace
{ {
static twa_graph_ptr static twa_graph_ptr
ks_cobuchi(unsigned n, bdd_dict_ptr dict) ks_nca(unsigned n, bdd_dict_ptr dict)
{ {
if (n == 0) if (n == 0)
throw std::runtime_error("ks_cobuchi expects a positive argument"); throw std::runtime_error("ks_nca expects a positive argument");
// the alphabet has four letters: // the alphabet has four letters:
// i, s (for sigma), p (for pi), h (for hash) // i, s (for sigma), p (for pi), h (for hash)
// we encode this four letters alphabet thanks to two AP a and b // we encode this four letters alphabet thanks to two AP a and b
...@@ -185,8 +185,8 @@ namespace spot ...@@ -185,8 +185,8 @@ namespace spot
switch (pattern) switch (pattern)
{ {
// Keep this alphabetically-ordered! // Keep this alphabetically-ordered!
case AUT_KS_COBUCHI: case AUT_KS_NCA:
return ks_cobuchi(n, dict); return ks_nca(n, dict);
case AUT_L_NBA: case AUT_L_NBA:
return l_nba(n, dict); return l_nba(n, dict);
case AUT_L_DSA: case AUT_L_DSA:
...@@ -201,7 +201,7 @@ namespace spot ...@@ -201,7 +201,7 @@ namespace spot
{ {
static const char* const class_name[] = static const char* const class_name[] =
{ {
"ks-cobuchi", "ks-nca",
"l-nba", "l-nba",
"l-dsa", "l-dsa",
}; };
......
...@@ -35,7 +35,7 @@ namespace spot ...@@ -35,7 +35,7 @@ namespace spot
/// good-for-games and that has no equivalent deterministic /// good-for-games and that has no equivalent deterministic
/// co-Büchi automaton with less than 2^n / (2n+1) states. /// co-Büchi automaton with less than 2^n / (2n+1) states.
/// ///
/// Only defined for n>0 /// Only defined for n>0.
/// ///
/** \verbatim /** \verbatim
@InProceedings{ kuperberg.15.icalp, @InProceedings{ kuperberg.15.icalp,
...@@ -51,7 +51,7 @@ namespace spot ...@@ -51,7 +51,7 @@ namespace spot
doi = {10.1007/978-3-662-47666-6_24} doi = {10.1007/978-3-662-47666-6_24}
} }
\endverbatim */ \endverbatim */
AUT_KS_COBUCHI = AUT_BEGIN, AUT_KS_NCA = AUT_BEGIN,
/// \brief Hard-to-complement non-deterministic Büchi automata /// \brief Hard-to-complement non-deterministic Büchi automata
/// ///
/// Build a non-deterministic Büchi automaton with 3n+1 states /// Build a non-deterministic Büchi automaton with 3n+1 states
......
...@@ -29,7 +29,7 @@ s/[=[].*/=1/p ...@@ -29,7 +29,7 @@ s/[=[].*/=1/p
res=`genaut $opts --stats="--%F=%L"` res=`genaut $opts --stats="--%F=%L"`
test "$opts" = "$res" test "$opts" = "$res"
genaut --ks-cobuchi=..3 --l-nba=..3 --l-dsa=..3 --stats=%s,%e,%t,%c,%g >out genaut --ks-nca=..3 --l-nba=..3 --l-dsa=..3 --stats=%s,%e,%t,%c,%g >out
cat >expected <<EOF cat >expected <<EOF
3,7,16,1,Fin(0) 3,7,16,1,Fin(0)
5,14,32,1,Fin(0) 5,14,32,1,Fin(0)
...@@ -43,7 +43,7 @@ cat >expected <<EOF ...@@ -43,7 +43,7 @@ cat >expected <<EOF
EOF EOF
diff out expected diff out expected
genaut --ks-cobuchi=0 2>err && exit 1 genaut --ks-nca=0 2>err && exit 1
grep positive err grep positive err
genaut --l-nba=0 2>err && exit 1 genaut --l-nba=0 2>err && exit 1
grep positive err grep positive err
...@@ -304,7 +304,7 @@ ...@@ -304,7 +304,7 @@
"cell_type": "code", "cell_type": "code",
"collapsed": false, "collapsed": false,
"input": [ "input": [
"display(sg.aut_pattern(sg.AUT_KS_COBUCHI, 3).show('.a'),\n", "display(sg.aut_pattern(sg.AUT_KS_NCA, 3).show('.a'),\n",
" sg.aut_pattern(sg.AUT_L_DSA, 3).show('.a'),\n", " sg.aut_pattern(sg.AUT_L_DSA, 3).show('.a'),\n",
" sg.aut_pattern(sg.AUT_L_NBA, 3).show('.a'))" " sg.aut_pattern(sg.AUT_L_NBA, 3).show('.a'))"
], ],
...@@ -887,7 +887,7 @@ ...@@ -887,7 +887,7 @@
"cell_type": "code", "cell_type": "code",
"collapsed": false, "collapsed": false,
"input": [ "input": [
"for aut in sg.aut_patterns(sg.AUT_KS_COBUCHI):\n", "for aut in sg.aut_patterns(sg.AUT_KS_NCA):\n",
" print(aut.num_states())" " print(aut.num_states())"
], ],
"language": "python", "language": "python",
......
...@@ -24,7 +24,7 @@ ...@@ -24,7 +24,7 @@
import spot.gen as gen import spot.gen as gen
from sys import exit from sys import exit
k2 = gen.aut_pattern(gen.AUT_KS_COBUCHI, 2) k2 = gen.aut_pattern(gen.AUT_KS_NCA, 2)
assert k2.prop_state_acc() assert k2.prop_state_acc()
assert k2.num_states() == 5 assert k2.num_states() == 5
assert k2.prop_universal().is_false() assert k2.prop_universal().is_false()
...@@ -35,7 +35,7 @@ assert k2.prop_deterministic().is_false() ...@@ -35,7 +35,7 @@ assert k2.prop_deterministic().is_false()
assert k2.prop_terminal().is_false() assert k2.prop_terminal().is_false()
# to_str is defined in the spot package, so this makes sure # to_str is defined in the spot package, so this makes sure
# the type returned by spot.gen.ks_cobuchi() is the correct one. # the type returned by spot.gen.ks_nca() is the correct one.
assert 'to_str' in dir(k2) assert 'to_str' in dir(k2)
k3 = gen.aut_pattern(gen.AUT_L_NBA, 3) k3 = gen.aut_pattern(gen.AUT_L_NBA, 3)
...@@ -51,7 +51,7 @@ assert k3.prop_terminal().is_false() ...@@ -51,7 +51,7 @@ assert k3.prop_terminal().is_false()
assert k2.get_dict() == k3.get_dict() assert k2.get_dict() == k3.get_dict()
try: try:
gen.aut_pattern(gen.AUT_KS_COBUCHI, 0) gen.aut_pattern(gen.AUT_KS_NCA, 0)
except RuntimeError as e: except RuntimeError as e:
assert 'positive argument' in str(e) assert 'positive argument' in str(e)
else: else:
...@@ -82,4 +82,4 @@ assert 40 == sum(p.size() for p in gen.ltl_patterns((gen.LTL_OR_G, 1, 5), ...@@ -82,4 +82,4 @@ assert 40 == sum(p.size() for p in gen.ltl_patterns((gen.LTL_OR_G, 1, 5),
assert 32 == sum(p.num_states() assert 32 == sum(p.num_states()
for p in gen.aut_patterns((gen.AUT_L_NBA, 1, 3), for p in gen.aut_patterns((gen.AUT_L_NBA, 1, 3),
(gen.AUT_KS_COBUCHI, 5))) (gen.AUT_KS_NCA, 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