From e7df182a308d7da2d6d3e114150b1dcc4c16bc0f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 3 Sep 2017 15:36:08 +0200 Subject: [PATCH] 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. --- bin/genaut.cc | 2 +- doc/org/genaut.org | 19 +++++++++++-------- spot/gen/automata.cc | 10 +++++----- spot/gen/automata.hh | 4 ++-- tests/core/genaut.test | 4 ++-- tests/python/gen.ipynb | 4 ++-- tests/python/gen.py | 8 ++++---- 7 files changed, 27 insertions(+), 24 deletions(-) diff --git a/bin/genaut.cc b/bin/genaut.cc index d19b26abe..1576a7c14 100644 --- a/bin/genaut.cc +++ b/bin/genaut.cc @@ -50,7 +50,7 @@ static const argp_option options[] = /**************************************************/ // Keep this alphabetically sorted (expect for aliases). { 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 " "deterministic co-Büchi automaton has at least 2^N/(2N+1) states.", 0}, { "l-nba", gen::AUT_L_NBA, "RANGE", 0, diff --git a/doc/org/genaut.org b/doc/org/genaut.org index 9a8430a19..1aaf5ff1b 100644 --- a/doc/org/genaut.org +++ b/doc/org/genaut.org @@ -14,9 +14,12 @@ genaut --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d' #+END_SRC #+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 : 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 : complementary Streett automaton needs at least n! : states. @@ -28,7 +31,7 @@ By default, the output format is [[file:hoa.org][HOA]], but this can be controll For instance: #+NAME: kscobuchi2 #+BEGIN_SRC sh :results verbatim :exports code -genaut --ks-cobuchi=2 --dot +genaut --ks-nca=2 --dot #+END_SRC #+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 values between 1 and M included). #+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 #+RESULTS: -: ks-cobuchi=1 has 3 states -: ks-cobuchi=2 has 5 states -: ks-cobuchi=3 has 7 states -: ks-cobuchi=4 has 9 states -: ks-cobuchi=5 has 11 states +: ks-nca=1 has 3 states +: ks-nca=2 has 5 states +: ks-nca=3 has 7 states +: ks-nca=4 has 9 states +: ks-nca=5 has 11 states diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc index 8818090e0..f543d4682 100644 --- a/spot/gen/automata.cc +++ b/spot/gen/automata.cc @@ -28,10 +28,10 @@ namespace spot namespace { static twa_graph_ptr - ks_cobuchi(unsigned n, bdd_dict_ptr dict) + ks_nca(unsigned n, bdd_dict_ptr dict) { 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: // i, s (for sigma), p (for pi), h (for hash) // we encode this four letters alphabet thanks to two AP a and b @@ -185,8 +185,8 @@ namespace spot switch (pattern) { // Keep this alphabetically-ordered! - case AUT_KS_COBUCHI: - return ks_cobuchi(n, dict); + case AUT_KS_NCA: + return ks_nca(n, dict); case AUT_L_NBA: return l_nba(n, dict); case AUT_L_DSA: @@ -201,7 +201,7 @@ namespace spot { static const char* const class_name[] = { - "ks-cobuchi", + "ks-nca", "l-nba", "l-dsa", }; diff --git a/spot/gen/automata.hh b/spot/gen/automata.hh index fc7018f85..25a8e6918 100644 --- a/spot/gen/automata.hh +++ b/spot/gen/automata.hh @@ -35,7 +35,7 @@ namespace spot /// 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 + /// Only defined for n>0. /// /** \verbatim @InProceedings{ kuperberg.15.icalp, @@ -51,7 +51,7 @@ namespace spot doi = {10.1007/978-3-662-47666-6_24} } \endverbatim */ - AUT_KS_COBUCHI = AUT_BEGIN, + AUT_KS_NCA = AUT_BEGIN, /// \brief Hard-to-complement non-deterministic Büchi automata /// /// Build a non-deterministic Büchi automaton with 3n+1 states diff --git a/tests/core/genaut.test b/tests/core/genaut.test index 35027d85a..ec93c0b42 100644 --- a/tests/core/genaut.test +++ b/tests/core/genaut.test @@ -29,7 +29,7 @@ s/[=[].*/=1/p res=`genaut $opts --stats="--%F=%L"` 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 <expected <err && exit 1 +genaut --ks-nca=0 2>err && exit 1 grep positive err genaut --l-nba=0 2>err && exit 1 grep positive err diff --git a/tests/python/gen.ipynb b/tests/python/gen.ipynb index 06d90b169..78af79137 100644 --- a/tests/python/gen.ipynb +++ b/tests/python/gen.ipynb @@ -304,7 +304,7 @@ "cell_type": "code", "collapsed": false, "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_NBA, 3).show('.a'))" ], @@ -887,7 +887,7 @@ "cell_type": "code", "collapsed": false, "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())" ], "language": "python", diff --git a/tests/python/gen.py b/tests/python/gen.py index 5fac2a54e..85596d978 100644 --- a/tests/python/gen.py +++ b/tests/python/gen.py @@ -24,7 +24,7 @@ import spot.gen as gen 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.num_states() == 5 assert k2.prop_universal().is_false() @@ -35,7 +35,7 @@ assert k2.prop_deterministic().is_false() assert k2.prop_terminal().is_false() # 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) k3 = gen.aut_pattern(gen.AUT_L_NBA, 3) @@ -51,7 +51,7 @@ assert k3.prop_terminal().is_false() assert k2.get_dict() == k3.get_dict() try: - gen.aut_pattern(gen.AUT_KS_COBUCHI, 0) + gen.aut_pattern(gen.AUT_KS_NCA, 0) except RuntimeError as e: assert 'positive argument' in str(e) else: @@ -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() for p in gen.aut_patterns((gen.AUT_L_NBA, 1, 3), - (gen.AUT_KS_COBUCHI, 5))) + (gen.AUT_KS_NCA, 5)))