From 7ee2d9995f8adc618416aa5f7a9d13201d6bbfb9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 24 Mar 2024 20:59:52 +0100 Subject: [PATCH] genaut: add two families of cyclic automata These are meant to test the optimization implemented in issue #568. * spot/gen/automata.hh, spot/gen/automata.cc, bin/genaut.cc: Add support for --cycle-log-nba and --cycle-onehot-nba. * tests/core/genaut.test: Add some tests. * tests/python/gen.ipynb: Illustrate them. * NEWS: Mention them. --- NEWS | 5 + bin/genaut.cc | 6 + spot/gen/automata.cc | 81 +- spot/gen/automata.hh | 21 + tests/core/genaut.test | 7 + tests/python/gen.ipynb | 2165 +++++++++++++++++++++++++++++++++++++++- 6 files changed, 2259 insertions(+), 26 deletions(-) diff --git a/NEWS b/NEWS index 1af53cda2..f2d65c401 100644 --- a/NEWS +++ b/NEWS @@ -55,6 +55,11 @@ New in spot 2.11.6.dev (not yet released) patching the game a posteriori is cumbersome if the equivalence concerns different players). + - genaut learned two new familes of automata, --cycle-log-nba and + --cycle-onehot-nba. They both create a cycle of n^2 states that + can be reduced to a cycle of n states using reduction based on + direct simulation. + Library: - The following new trivial simplifications have been implemented for SEREs: diff --git a/bin/genaut.cc b/bin/genaut.cc index 7c3bbf70b..4f6745f3f 100644 --- a/bin/genaut.cc +++ b/bin/genaut.cc @@ -67,6 +67,12 @@ static const argp_option options[] = { "cyclist-proof-dba", gen::AUT_CYCLIST_PROOF_DBA, "RANGE", 0, "A DBA with N+2 states that should be included " "in cyclist-trace-nba=B.", 0}, + { "cycle-log-nba", gen::AUT_CYCLE_LOG_NBA, "RANGE", 0, + "A cyclic NBA with N*N states and log(N) atomic propositions, that " + "should be simplifiable to a cyclic NBA with N states.", 0 }, + { "cycle-onehot-nba", gen::AUT_CYCLE_ONEHOT_NBA, "RANGE", 0, + "A cyclic NBA with N*N states and N atomic propositions, that " + "should be simplifiable to a cyclic NBA with N states.", 0 }, RANGE_DOC, /**************************************************/ { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc index a7f858a64..5d1edfdbd 100644 --- a/spot/gen/automata.cc +++ b/spot/gen/automata.cc @@ -172,9 +172,10 @@ namespace spot } } + // Return the smallest integer k such that 2^k ≥ n > 1. static unsigned ulog2(unsigned n) { - assert(n>0); + assert(n>1); // clz() is undefined for n==0 --n; return CHAR_BIT*sizeof(unsigned) - clz(n); } @@ -229,7 +230,7 @@ namespace spot m = {}; aut->prop_state_acc(true); - // How many AP to we need to represent n letters + // How many AP to we need to represent n+1 letters unsigned nap = ulog2(n + 1); std::vector apvars(nap); for (unsigned a = 0; a < nap; ++a) @@ -252,6 +253,76 @@ namespace spot return aut; } + static twa_graph_ptr + cycle_nba(unsigned n, bool onehot, bdd_dict_ptr dict) + { + if (n == 0) + throw std::runtime_error + (onehot + ? "cycle-onehot-nba expects a positive argument" + : "cycle-log-nba expects a positive argument"); + + auto aut = make_twa_graph(dict); + acc_cond::mark_t isacc = aut->set_buchi(); + aut->new_states(n * n); + aut->set_init_state(0); + aut->prop_state_acc(true); + aut->prop_weak(n == 1); + aut->prop_universal(n == 1); + aut->prop_complete(false); + + std::vector letters; + letters.reserve(n); + + if (!onehot) + { + // How many AP to we need to represent n letters + unsigned nap = n == 1 ? 1 : ulog2(n); + std::vector apvars(nap); + for (unsigned a = 0; a < nap; ++a) + apvars[a] = aut->register_ap("p" + std::to_string(a)); + + for (unsigned letter = 0; letter < n; ++letter) + { + bdd cond = bdd_ibuildcube(letter, nap, apvars.data()); + letters.push_back(cond); + } + } + else + { + std::vector apvars(n); + bdd allneg = bddtrue; + for (unsigned a = 0; a < n; ++a) + { + int v = aut->register_ap("p" + std::to_string(a)); + apvars[a] = bdd_ithvar(v); + allneg &= bdd_nithvar(v); + } + for (unsigned a = 0; a < n; ++a) + letters.push_back(bdd_exist(allneg, apvars[a]) & apvars[a]); + } + + unsigned n2 = n * n; + for (unsigned s = 0; s < n; ++s) + { + bdd label = letters[s]; + for (unsigned copy = 0; copy < n; ++copy) + { + unsigned q = s + copy * n; + if (s != 0) + { + aut->new_edge(q, q, bddtrue); + aut->new_edge(q, (q + 1) % n2, label); + } + else + { + aut->new_edge(q, (q + 1) % n2, label, isacc); + } + } + } + return aut; + } + twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n, bdd_dict_ptr dict) { @@ -278,6 +349,10 @@ namespace spot return cyclist_trace_or_proof(n, true, dict); case AUT_CYCLIST_PROOF_DBA: return cyclist_trace_or_proof(n, false, dict); + case AUT_CYCLE_LOG_NBA: + return cycle_nba(n, false, dict); + case AUT_CYCLE_ONEHOT_NBA: + return cycle_nba(n, true, dict); case AUT_END: break; } @@ -294,6 +369,8 @@ namespace spot "m-nba", "cyclist-trace-nba", "cyclist-proof-dba", + "cycle-log-nba", + "cycle-onehot-nba", }; // Make sure we do not forget to update the above table every // time a new pattern is added. diff --git a/spot/gen/automata.hh b/spot/gen/automata.hh index fdaa0a6d5..7b60b5269 100644 --- a/spot/gen/automata.hh +++ b/spot/gen/automata.hh @@ -96,6 +96,27 @@ namespace spot /// for a given n contain the automaton generated with /// AUT_CYCLIST_PROOF_DBA for the same n. AUT_CYCLIST_PROOF_DBA, + /// \brief cycles of n letters repeated n times + /// + /// This is a Büchi automaton with n^2 states, in which each + /// state i has a true self-loop and a successor labeled by the + /// (i%n)th letter. Only the states that are multiple of n have + /// no self-loop and are accepting. + /// + /// This version uses log(n) atomic propositions to + /// encore the n letters as minterms. + AUT_CYCLE_LOG_NBA, + /// \brief cycles of n letters repeated n times + /// + /// This is a Büchi automaton with n^2 states, in which each + /// state i has a true self-loop and a successor labeled by the + /// (i%n)th letter. Only the states that are multiple of n have + /// no self-loop and are accepting. + /// + /// This version uses one-hot encoding of letters, i.e, n atomic + /// propositions are used, but only one is positive (except on + /// true self-loops). + AUT_CYCLE_ONEHOT_NBA, AUT_END }; diff --git a/tests/core/genaut.test b/tests/core/genaut.test index c69b87f2a..d74700b68 100644 --- a/tests/core/genaut.test +++ b/tests/core/genaut.test @@ -29,6 +29,7 @@ res=`genaut $opts --stats="--%F=%L"` test "$opts" = "$res" genaut --ks-nca=..3 --l-nba=..3 --l-dsa=..3 --m-nba=..3 \ + --cycle-log-nba=..3 --cycle-onehot-nba=..3 \ --stats=%s,%e,%t,%c,%g >out cat >expected <expected <\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "ks-nca=3\n", + "\n", + "ks-nca=3\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "(!a & b) | (a & !b)\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "(!a & !b) | (a & b)\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "\n" + ], "text/html": [ "\n", "\n", "\n", - "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "ks-nca=3\n", + "\n", + "ks-nca=3\n", "[co-Büchi]\n", "\n", "\n", @@ -730,7 +941,7 @@ "\n" ], "text/plain": [ - "" + " *' at 0x7fb3eb3521f0> >" ] }, "metadata": {}, @@ -738,17 +949,260 @@ }, { "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "l-dsa=3\n", + "\n", + "l-dsa=3\n", + "(Fin(\n", + "⓿\n", + ") | Inf(\n", + "❶\n", + ")) & (Fin(\n", + "❷\n", + ") | Inf(\n", + "❸\n", + ")) & (Fin(\n", + "❹\n", + ") | Inf(\n", + "❺\n", + "))\n", + "[Streett 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "❶\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "1->5\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "❷\n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "5->9\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "❸\n", + "\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "6->10\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "9->9\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "❹\n", + "\n", + "\n", + "\n", + "9->8\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "7->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "10->10\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "11\n", + "❺\n", + "\n", + "\n", + "\n", + "10->11\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "8->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "11->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n" + ], "text/html": [ "\n", "\n", "\n", - "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "l-dsa=3\n", + "\n", + "l-dsa=3\n", "(Fin(\n", "⓿\n", ") | Inf(\n", @@ -978,7 +1432,7 @@ "\n" ], "text/plain": [ - "" + " *' at 0x7fb3eb3519e0> >" ] }, "metadata": {}, @@ -986,17 +1440,223 @@ }, { "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "l-nba=3\n", + "\n", + "l-nba=3\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a | b\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "1->7\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "7->0\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a | b\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "2->8\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "8->7\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a | b\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "3->9\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "9->8\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "9->9\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n" + ], "text/html": [ "\n", "\n", "\n", - "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "l-nba=3\n", + "\n", + "l-nba=3\n", "[Büchi]\n", "\n", "\n", @@ -1189,7 +1849,1458 @@ "\n" ], "text/plain": [ - "" + " *' at 0x7fb3eb351440> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "m-nba=3\n", + "\n", + "m-nba=3\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "m-nba=3\n", + "\n", + "m-nba=3\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fb3eb3513e0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "cyclist-proof-dba=3\n", + "\n", + "cyclist-proof-dba=3\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "cyclist-proof-dba=3\n", + "\n", + "cyclist-proof-dba=3\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fb3eb3503f0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "cyclist-trace-nba=3\n", + "\n", + "cyclist-trace-nba=3\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "cyclist-trace-nba=3\n", + "\n", + "cyclist-trace-nba=3\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fb3eb350510> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "cycle-log-nba=3\n", + "\n", + "cycle-log-nba=3\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "7->8\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "8->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "8->8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "cycle-log-nba=3\n", + "\n", + "cycle-log-nba=3\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "7->8\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "8->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "8->8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fb3eb351080> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "cycle-onehot-nba=3\n", + "\n", + "cycle-onehot-nba=3\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "p0 & !p1 & !p2\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1 & !p2\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!p0 & !p1 & p2\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "p0 & !p1 & !p2\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!p0 & p1 & !p2\n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "!p0 & !p1 & p2\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "p0 & !p1 & !p2\n", + "\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "7->8\n", + "\n", + "\n", + "!p0 & p1 & !p2\n", + "\n", + "\n", + "\n", + "8->0\n", + "\n", + "\n", + "!p0 & !p1 & p2\n", + "\n", + "\n", + "\n", + "8->8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "cycle-onehot-nba=3\n", + "\n", + "cycle-onehot-nba=3\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "p0 & !p1 & !p2\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1 & !p2\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!p0 & !p1 & p2\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "p0 & !p1 & !p2\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!p0 & p1 & !p2\n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "!p0 & !p1 & p2\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "p0 & !p1 & !p2\n", + "\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "7->8\n", + "\n", + "\n", + "!p0 & p1 & !p2\n", + "\n", + "\n", + "\n", + "8->0\n", + "\n", + "\n", + "!p0 & !p1 & p2\n", + "\n", + "\n", + "\n", + "8->8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fb3eb351680> >" ] }, "metadata": {}, @@ -1197,9 +3308,15 @@ } ], "source": [ - "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'))" + "examples = []\n", + "for p in (sg.AUT_KS_NCA, sg.AUT_L_DSA, sg.AUT_L_NBA, sg.AUT_M_NBA,\n", + " sg.AUT_CYCLIST_PROOF_DBA, sg.AUT_CYCLIST_TRACE_NBA,\n", + " sg.AUT_CYCLE_LOG_NBA, sg.AUT_CYCLE_ONEHOT_NBA):\n", + " aut = sg.aut_pattern(p, 3)\n", + " aut.set_name(sg.aut_pattern_name(p) + \"=3\")\n", + " examples.append(aut)\n", + "\n", + "display(*examples)" ] }, { @@ -1253,7 +3370,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.7" + "version": "3.11.8" } }, "nbformat": 4,