From 11ca2803c9dbcad387b7db2ef99d8767166d60bf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 27 Apr 2017 11:47:19 +0200 Subject: [PATCH] gen: hide ks_cobuchi(), introduce aut_pattern() * spot/gen/automata.hh, spot/gen/automata.cc: Hide ks_cobuchi() behind introduce aut_pattern(), as we have already done for the formulas. * bin/genaut.cc: Simplify using this interface. * python/spot/gen.i: Introduce aut_patterns(). * tests/python/gen.ipynb, tests/python/gen.py: Adjust. --- bin/genaut.cc | 50 ++++---------- python/spot/gen.i | 28 ++++++++ spot/gen/automata.cc | 147 ++++++++++++++++++++++++++--------------- spot/gen/automata.hh | 55 +++++++++------ tests/python/gen.ipynb | 54 ++++++++++++--- tests/python/gen.py | 4 +- 6 files changed, 216 insertions(+), 122 deletions(-) diff --git a/bin/genaut.cc b/bin/genaut.cc index 598d37ce2..e4208bb9e 100644 --- a/bin/genaut.cc +++ b/bin/genaut.cc @@ -43,28 +43,14 @@ using namespace spot; -const char argp_program_doc[] ="\ -Generate omega automata from predefined patterns."; - -enum { - FIRST_CLASS = 256, - OPT_KS_COBUCHI = FIRST_CLASS, - LAST_CLASS, -}; - -const char* const class_name[LAST_CLASS - FIRST_CLASS] = - { - "ks-cobuchi", - }; - -#define OPT_ALIAS(o) { #o, 0, nullptr, OPTION_ALIAS, nullptr, 0 } +const char argp_program_doc[] ="Generate ω-automata from predefined patterns."; static const argp_option options[] = { /**************************************************/ // Keep this alphabetically sorted (expect for aliases). { nullptr, 0, nullptr, 0, "Pattern selection:", 1}, - { "ks-cobuchi", OPT_KS_COBUCHI, "RANGE", 0, + { "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}, RANGE_DOC, @@ -75,7 +61,7 @@ static const argp_option options[] = struct job { - int pattern; + gen::aut_pattern_id pattern; struct range range; }; @@ -94,7 +80,7 @@ static void enqueue_job(int pattern, const char* range_str) { job j; - j.pattern = pattern; + j.pattern = static_cast(pattern); j.range = parse_range(range_str); jobs.push_back(j); } @@ -102,35 +88,23 @@ enqueue_job(int pattern, const char* range_str) static int parse_opt(int key, char* arg, struct argp_state*) { - // This switch is alphabetically-ordered. - switch (key) + if (key >= gen::AUT_BEGIN && key < gen::AUT_END) { - case OPT_KS_COBUCHI: enqueue_job(key, arg); - break; - default: - return ARGP_ERR_UNKNOWN; + return 0; } - return 0; + return ARGP_ERR_UNKNOWN; } static void -output_pattern(int pattern, int n) +output_pattern(gen::aut_pattern_id pattern, int n) { - twa_graph_ptr aut = nullptr; - switch (pattern) - { - // Keep this alphabetically-ordered! - case OPT_KS_COBUCHI: - aut = spot::gen::ks_cobuchi(n); - break; - default: - error(100, 0, "internal error: pattern not implemented"); - } - process_timer timer; + timer.start(); + twa_graph_ptr aut = spot::gen::aut_pattern(pattern, n); + timer.stop(); automaton_printer printer; - printer.print(aut, timer, nullptr, class_name[pattern - FIRST_CLASS], n); + printer.print(aut, timer, nullptr, aut_pattern_name(pattern), n); } static void diff --git a/python/spot/gen.i b/python/spot/gen.i index 7b91093cd..f64874f76 100644 --- a/python/spot/gen.i +++ b/python/spot/gen.i @@ -85,4 +85,32 @@ def ltl_patterns(*args): raise RuntimeError("invalid pattern specification") for n in range(min, max + 1): yield ltl_pattern(pat, n) + +def aut_patterns(*args): + """ + Generate automata patterns. + + The arguments should be have one of these three forms: + - (id, n) + - (id, min, max) + - id + In the first case, the pattern id=n is generated. In the second + case, all pattern id=n for min<=n<=max are generated. The + third case is a shorthand for (id, 1, 10). + """ + for spec in args: + if type(spec) is int: + pat = spec + min = 1 + max = 10 + else: + ls = len(spec) + if ls == 2: + pat, min, max = spec[0], spec[1], spec[1] + elif ls == 3: + pat, min, max = spec + else: + raise RuntimeError("invalid pattern specification") + for n in range(min, max + 1): + yield aut_pattern(pat, n) %} diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc index 7a00b5aa0..67374bce6 100644 --- a/spot/gen/automata.cc +++ b/spot/gen/automata.cc @@ -17,75 +17,114 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include #include -#include #include namespace spot { namespace gen { - - twa_graph_ptr - ks_cobuchi(unsigned n) + namespace { - if (n == 0) - throw std::runtime_error("ks_cobuchi() 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 - // the exact encoding is not important - // each letter is a permutation of the set {1..2n} - // s = (1 2 .. 2n) the rotation - // p = (1 2) the swap of the first two elements - // i is the identity - // d is the identity on {2..2n} but is undefined on 1 + static twa_graph_ptr + ks_cobuchi(unsigned n) + { + if (n == 0) + throw std::runtime_error("ks_cobuchi 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 + // the exact encoding is not important + // each letter is a permutation of the set {1..2n} + // s = (1 2 .. 2n) the rotation + // p = (1 2) the swap of the first two elements + // i is the identity + // d is the identity on {2..2n} but is undefined on 1 - // the automaton has 2n+1 states, numbered from 0 to 2n - // 0 is the initial state and the only non-deterministic state + // the automaton has 2n+1 states, numbered from 0 to 2n + // 0 is the initial state and the only non-deterministic state - auto dict = make_bdd_dict(); - auto aut = make_twa_graph(dict); + auto dict = make_bdd_dict(); + auto aut = make_twa_graph(dict); - // register aps - aut->register_ap("a"); - aut->register_ap("b"); + // register aps + bdd a = bdd_ithvar(aut->register_ap("a")); + bdd b = bdd_ithvar(aut->register_ap("b")); - // retrieve the four letters, and name them - bdd i = formula_to_bdd(parse_formula("a&&b"), dict, aut); - bdd s = formula_to_bdd(parse_formula("a&&!b"), dict, aut); - bdd p = formula_to_bdd(parse_formula("!a&&b"), dict, aut); - bdd h = formula_to_bdd(parse_formula("!a&&!b"), dict, aut); + // name the four letters + bdd i = a & b; + bdd s = a & (!b); + bdd p = (!a) & b; + bdd h = (!a) & (!b); - // actually build the automaton - aut->new_states(2*n+1); - aut->set_init_state(0); - aut->set_acceptance(1, acc_cond::acc_code::cobuchi()); + // actually build the automaton + aut->new_states(2*n+1); + aut->set_init_state(0); + aut->set_acceptance(1, acc_cond::acc_code::cobuchi()); - // from 0, we can non-deterministically jump to any state (except 0) with - // any letter. - for (unsigned q = 1; q <= 2*n; ++q) - aut->new_edge(0, q, bddtrue, {0}); - // i is the identity - for (unsigned q = 1; q <= 2*n; ++q) - aut->new_edge(q, q, i); - // p swaps 1 and 2, and leaves all other states invariant - aut->new_edge(1, 2, p); - aut->new_edge(2, 1, p); - for (unsigned q = 3; q <= 2*n; ++q) - aut->new_edge(q, q, p); - // s does to next state (mod 2*n, 0 excluded) - aut->new_edge(2*n, 1, s); - for (unsigned q = 1; q < 2*n; ++q) - aut->new_edge(q, q+1, s); - // h is the same as i, except on 1 where it goes back to the initial state - aut->new_edge(1, 0, h); - for (unsigned q = 2; q <= 2*n; ++q) - aut->new_edge(q, q, h); + // from 0, we can non-deterministically jump to any state + // (except 0) with any letter. + for (unsigned q = 1; q <= 2*n; ++q) + aut->new_edge(0, q, bddtrue, {0}); + // i is the identity + for (unsigned q = 1; q <= 2*n; ++q) + aut->new_edge(q, q, i); + // p swaps 1 and 2, and leaves all other states invariant + aut->new_edge(1, 2, p); + aut->new_edge(2, 1, p); + for (unsigned q = 3; q <= 2*n; ++q) + aut->new_edge(q, q, p); + // s does to next state (mod 2*n, 0 excluded) + aut->new_edge(2*n, 1, s); + for (unsigned q = 1; q < 2*n; ++q) + aut->new_edge(q, q+1, s); + // h is the same as i, except on 1 where it goes back to the + // initial state + aut->new_edge(1, 0, h); + for (unsigned q = 2; q <= 2*n; ++q) + aut->new_edge(q, q, h); - aut->merge_edges(); - aut->prop_state_acc(true); - return aut; + aut->merge_edges(); + aut->prop_state_acc(true); + return aut; + } + } + + twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n) + { + if (n < 0) + { + std::ostringstream err; + err << "pattern argument for " << aut_pattern_name(pattern) + << " should be positive"; + throw std::runtime_error(err.str()); + } + + switch (pattern) + { + // Keep this alphabetically-ordered! + case AUT_KS_COBUCHI: + return ks_cobuchi(n); + case AUT_END: + break; + } + throw std::runtime_error("unsupported pattern"); + } + + const char* aut_pattern_name(aut_pattern_id pattern) + { + static const char* const class_name[] = + { + "ks-cobuchi", + }; + // Make sure we do not forget to update the above table every + // time a new pattern is added. + static_assert(sizeof(class_name)/sizeof(*class_name) + == AUT_END - AUT_BEGIN, "size mismatch"); + if (pattern < AUT_BEGIN || pattern >= AUT_END) + throw std::runtime_error("unsupported pattern"); + return class_name[pattern - AUT_BEGIN]; } } } diff --git a/spot/gen/automata.hh b/spot/gen/automata.hh index b4d5a0057..9da6d0a5b 100644 --- a/spot/gen/automata.hh +++ b/spot/gen/automata.hh @@ -19,31 +19,48 @@ #pragma once -#include +#include +#include namespace spot { namespace gen { - /// \brief A family of co-Büchi automata. + enum aut_pattern_id { + 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} + /// } + /// + /// Only defined for n>0 + AUT_KS_COBUCHI = AUT_BEGIN, + AUT_END + }; + + /// \brief generate an automaton from a known pattern /// - /// 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: + /// The pattern is specified using one value from the aut_pattern_id + /// enum. See the man page of the `genaut` binary for a + /// description of those patterns, and bibliographic references. + SPOT_API twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n); + + /// \brief convert an aut_pattern_it value into a name /// - /// @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} - /// } - /// - /// \pre n>0 - SPOT_API twa_graph_ptr - ks_cobuchi(unsigned n); + /// The returned name is suitable to be used as an option + /// key for the genaut binary. + SPOT_API const char* aut_pattern_name(aut_pattern_id pattern); } } diff --git a/tests/python/gen.ipynb b/tests/python/gen.ipynb index 04d69503a..5b540ddd6 100644 --- a/tests/python/gen.ipynb +++ b/tests/python/gen.ipynb @@ -45,7 +45,7 @@ "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 13 + "prompt_number": 1 }, { "cell_type": "markdown", @@ -71,13 +71,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 14, + "prompt_number": 2, "text": [ "GFp1 & GFp2 & GFp3" ] } ], - "prompt_number": 14 + "prompt_number": 2 }, { "cell_type": "code", @@ -94,13 +94,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 15, + "prompt_number": 3, "text": [ "F(p & Xp & XXp & XXXp) & F(q & Xq & XXq & XXXq)" ] } ], - "prompt_number": 15 + "prompt_number": 3 }, { "cell_type": "markdown", @@ -289,7 +289,7 @@ ] } ], - "prompt_number": 20 + "prompt_number": 4 }, { "cell_type": "markdown", @@ -304,7 +304,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "sg.ks_cobuchi(3).show('.a')" + "sg.aut_pattern(sg.AUT_KS_COBUCHI, 3).show('.a')" ], "language": "python", "metadata": {}, @@ -312,7 +312,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 23, + "prompt_number": 5, "svg": [ "\n", "\n", @@ -491,7 +491,43 @@ ] } ], - "prompt_number": 23 + "prompt_number": 5 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Multiple automata can be generated using the `aut_patterns()` function, which works similarly to `ltl_patterns()`." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for aut in sg.aut_patterns(sg.AUT_KS_COBUCHI):\n", + " print(aut.num_states())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "3\n", + "5\n", + "7\n", + "9\n", + "11\n", + "13\n", + "15\n", + "17\n", + "19\n", + "21\n" + ] + } + ], + "prompt_number": 6 }, { "cell_type": "code", diff --git a/tests/python/gen.py b/tests/python/gen.py index 92e1bc9b0..3fc1d7cf4 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.ks_cobuchi(2) +k2 = gen.aut_pattern(gen.AUT_KS_COBUCHI, 2) assert k2.prop_state_acc() assert k2.num_states() == 5 # to_str is defined in the spot package, so this makes sure @@ -32,7 +32,7 @@ assert k2.num_states() == 5 assert 'to_str' in dir(k2) try: - gen.ks_cobuchi(0) + gen.aut_pattern(gen.AUT_KS_COBUCHI, 0) except RuntimeError as e: assert 'positive argument' in str(e) else: