From 2f42c1c9bf4a502c733e573e2eec6976b2cd10df Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 31 Mar 2015 13:46:25 +0200 Subject: [PATCH] randaut: add option --acc-type=random Fixes #71. * src/bin/randaut.cc: Implement option --acc-type. * src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh (random_acceptance): New function. * src/tgbatest/randaut.test, wrap/python/tests/randaut.ipynb: Test it. --- src/bin/randaut.cc | 41 + src/tgbaalgos/randomgraph.cc | 39 +- src/tgbaalgos/randomgraph.hh | 6 +- src/tgbatest/randaut.test | 17 + wrap/python/tests/randaut.ipynb | 3744 ++++++++++++++++--------------- 5 files changed, 2017 insertions(+), 1830 deletions(-) diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index 1e74ddbd3..a7dbbd66d 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -26,6 +26,7 @@ #include #include #include "error.h" +#include "argmatch.h" #include "common_setup.hh" #include "common_range.hh" @@ -64,12 +65,16 @@ states, 1 to 3 acceptance sets, and three atomic propositions:\n\ enum { OPT_SEED = 1, OPT_STATE_ACC, + OPT_ACC_TYPE, }; static const argp_option options[] = { /**************************************************/ { 0, 0, 0, 0, "Generation:", 2 }, + { "acc-type", OPT_ACC_TYPE, "buchi|random", 0, + "use a generalized buchi acceptance condition (default), or a " + "random acceptance condition", 0 }, { "acc-sets", 'A', "RANGE", 0, "number of acceptance sets (0)", 0 }, { "acc-probability", 'a', "FLOAT", 0, "probability that a transition belong to one acceptance set (0.2)", 0 }, @@ -102,6 +107,23 @@ static const struct argp_child children[] = { 0, 0, 0, 0 } }; +enum acc_type { acc_buchi, acc_random }; + +static char const *const acc_args[] = +{ + "buchi", "ba", "gba", + "random", + 0 +}; +static acc_type const acc_types[] = +{ + acc_buchi, acc_buchi, acc_buchi, + acc_random, +}; +ARGMATCH_VERIFY(acc_args, acc_types); + + +static acc_type opt_acc = acc_buchi; typedef spot::tgba_digraph::graph_t::trans_storage_t tr_t; typedef std::set> unique_aut_t; static spot::ltl::atomic_prop_set aprops; @@ -171,6 +193,9 @@ parse_opt(int key, char* arg, struct argp_state* as) opt_uniq = std::unique_ptr(new std::set>()); break; + case OPT_ACC_TYPE: + opt_acc = XARGMATCH("--acc-type", arg, acc_args, acc_types); + break; case OPT_SEED: opt_seed = to_int(arg); opt_seed_str = arg; @@ -229,9 +254,15 @@ main(int argc, char** argv) if (automaton_format == Spin && opt_acc_sets.max > 1) error(2, 0, "--spin is incompatible with --acc-sets=%d..%d", opt_acc_sets.min, opt_acc_sets.max); + if (automaton_format == Spin && opt_acc != acc_buchi) + error(2, 0, + "--spin implies --acc-type=buchi but a different --acc-type is used"); if (ba_wanted && opt_acc_sets.min != 1 && opt_acc_sets.max != 1) error(2, 0, "--ba is incompatible with --acc-sets=%d..%d", opt_acc_sets.min, opt_acc_sets.max); + if (ba_wanted && opt_acc != acc_buchi) + error(2, 0, + "--ba implies --acc-type=buchi but a different --acc-type is used"); try { @@ -263,6 +294,16 @@ main(int argc, char** argv) accs, opt_acc_prob, 0.5, opt_deterministic, opt_state_acc); + switch (opt_acc) + { + case acc_buchi: + // Random_graph builds a GBA by default + break; + case acc_random: + aut->set_acceptance(accs, spot::random_acceptance(accs)); + break; + } + if (opt_uniq) { auto tmp = spot::canonicalize diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index 009cec846..0d921ccb2 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2012, 2013, 2014 Laboratoire de +// Copyright (C) 2008, 2009, 2010, 2012, 2013, 2014, 2015 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -241,4 +241,41 @@ namespace spot return res; } + acc_cond::acc_code random_acceptance(unsigned n_accs) + { + // With 0 acceptance sets, we always generate the true acceptance. + // (Working with false is somehow pointless, and the formulas we + // generate for n_accs>0 are always satisfiable, so it makes sense + // that it should be satisfiable for n_accs=0 as well.) + if (n_accs == 0) + return {}; + + acc_cond acc(n_accs); + std::vector codes; + codes.reserve(n_accs); + for (unsigned i = 0; i < n_accs; ++i) + if (drand() < 0.5) + codes.push_back(acc.inf(acc.mark(i))); + else + codes.push_back(acc.fin(acc.mark(i))); + + int s = codes.size(); + while (s > 1) + { + // Pick a random code and put it at the end + int p1 = mrand(s--); + std::swap(codes[p1], codes[s]); + // and another one + int p2 = mrand(s); + + if (drand() < 0.5) + codes[p2].append_or(std::move(codes.back())); + else + codes[p2].append_and(std::move(codes.back())); + + codes.pop_back(); + } + return codes[0]; + } + } diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh index 9e78fbcb2..dd58b977c 100644 --- a/src/tgbaalgos/randomgraph.hh +++ b/src/tgbaalgos/randomgraph.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -25,6 +25,7 @@ #include "ltlvisit/apcollect.hh" #include "ltlenv/defaultenv.hh" #include "tgba/bdddict.hh" +#include "tgba/acc.hh" namespace spot { @@ -81,4 +82,7 @@ namespace spot const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict, unsigned n_accs = 0, float a = 0.1, float t = 0.5, bool deterministic = false, bool state_acc = false); + + /// Build a random acceptance where each acceptance sets is used once. + SPOT_API acc_cond::acc_code random_acceptance(unsigned n_accs); } diff --git a/src/tgbatest/randaut.test b/src/tgbatest/randaut.test index 7247bf12d..6a3839572 100755 --- a/src/tgbatest/randaut.test +++ b/src/tgbatest/randaut.test @@ -81,3 +81,20 @@ test 6 = `$autfilt -c out-det1.hoa` $autfilt -H out.hoa -o foo -c 2>stderr && exit 1 grep 'autfilt: options --output and --count are incompatible' stderr + +$randaut -n 2 -S5 -A4 -H 2 | grep Acceptance: > output +$randaut --acc-type=random -n 2 -S5 -A4 -H 2 | grep Acceptance: >> output +cat output + +cat >expected <stderr && exit 1 +grep 'randaut: --spin.*--acc-type' stderr +$randaut --ba --acc-type=random 2 2>stderr && exit 1 +grep 'randaut: --ba.*--acc-type' stderr diff --git a/wrap/python/tests/randaut.ipynb b/wrap/python/tests/randaut.ipynb index 724c79d81..fbe2c84dd 100644 --- a/wrap/python/tests/randaut.ipynb +++ b/wrap/python/tests/randaut.ipynb @@ -1,7 +1,7 @@ { "metadata": { "name": "", - "signature": "sha256:f26e5cfdf72ab87cc41a6613deb2e29a0cca8a92678f062cd01b7513940e0424" + "signature": "sha256:f4c7efdcb7b97c3b11c230a6b18c8e46c1708289918a5dd8df73fe6baae3c8f6" }, "nbformat": 3, "nbformat_minor": 0, @@ -18,7 +18,7 @@ "# the environment variables the first time it reads them, so\n", "# if you change those variables, the new values will be ignored\n", "# until you restart the kernel.\n", - "os.environ['SPOT_DOTEXTRA'] = 'size=\"5,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]'\n", + "os.environ['SPOT_DOTEXTRA'] = 'size=\"5.4,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]'\n", "os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n", "import spot" ], @@ -32,7 +32,7 @@ "collapsed": false, "input": [ "txt = \"\"\n", - "for a in spot.automata('randaut -H -S5 -A 3 -n10 2|'):\n", + "for a in spot.automata('randaut --acc-type=random -H -S5 -A4 -n10 2|'):\n", " txt += \"\".format(a.show('.a').data, spot.cleanup_acceptance(a).show('.a').data)\n", "txt += (\"
beforeafter
{0}{1}
\")\n", "HTML(txt)" @@ -42,1903 +42,1990 @@ "outputs": [ { "html": [ - "
beforeafter
\n", - "\n", + "
beforeafter
\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", + "\n", + "(Fin(\n", + "\u2777\n", + ") & Inf(\n", + "\u2778\n", + ")) | Inf(\n", + "\u24ff\n", + ") | Fin(\n", + "\u2776\n", + ")\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2777\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "!p0 & p1\n", - "\u2776\n", - "\n", - "\n", - "4->1\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2776\n", - "\n", - "\n", - "2->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "f\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "4->1\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "2->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "
\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "p0 & p1\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "p0 & p1\n", - "\u2777\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "!p0 & p1\n", - "\u2777\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u24ff\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "p0 & p1\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "f\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "p0 & p1\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "p0 & p1\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "p0 & p1\n", - "\n", - "\n", - "
\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "p0 & p1\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "p0 & !p1\n", - "\u24ff\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\n", - "\u2777\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2777\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "!p0 & p1\n", - "\u2777\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "p0 & p1\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "p0 & !p1\n", - "\u24ff\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\n", - "\u2777\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2777\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "!p0 & p1\n", - "\u2777\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "
\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!p0 & p1\n", - "\u2777\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\u2777\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ") | Fin(\n", + "\u2776\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "((Inf(\n", + "\u24ff\n", + ") | Inf(\n", + "\u2776\n", + ")) & Fin(\n", + "\u2778\n", + ")) | Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ") | Inf(\n", + "\u2776\n", + ") | Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "(Inf(\n", + "\u2777\n", + ") | Fin(\n", + "\u2778\n", + ") | Inf(\n", + "\u2776\n", + ")) & Fin(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "p0 & p1\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u2776\n", + ") | Fin(\n", + "\u2777\n", + ") | Inf(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u2777\n", + ") & (Inf(\n", + "\u2776\n", + ") | (Fin(\n", + "\u24ff\n", + ") & Fin(\n", + "\u2778\n", + ")))\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2778\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\u2777\n", "\n", "\n", "4->2\n", - "\n", - "\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u2776\n", + ") & Fin(\n", + "\u24ff\n", + ") & Fin(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "(Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2778\n", + ")) | Inf(\n", + "\u2776\n", + ") | Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\u2778\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "(Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2778\n", + ")) | Inf(\n", + "\u2776\n", + ") | Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\u2778\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "((Inf(\n", + "\u24ff\n", + ") | Fin(\n", + "\u2777\n", + ")) & Inf(\n", + "\u2778\n", + ")) | Fin(\n", + "\u2776\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "t\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u2778\n", + ") & Inf(\n", + "\u2777\n", + ")) | Fin(\n", + "\u2776\n", + ") | Inf(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\u2778\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u2777\n", + ") & Inf(\n", + "\u2776\n", + ")) | Fin(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\u2777\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "(Inf(\n", + "\u24ff\n", + ") | (Inf(\n", + "\u2776\n", + ")&Inf(\n", + "\u2778\n", + "))) & Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "(Inf(\n", + "\u24ff\n", + ") | (Inf(\n", + "\u2776\n", + ")&Inf(\n", + "\u2778\n", + "))) & Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "((Fin(\n", + "\u2777\n", + ") & Inf(\n", + "\u2778\n", + ")) | Inf(\n", + "\u24ff\n", + ")) & Fin(\n", + "\u2776\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\u2778\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "(Inf(\n", + "\u2777\n", + ") | Inf(\n", + "\u24ff\n", + ")) & Fin(\n", + "\u2776\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u2778\n", + ") & Fin(\n", + "\u2777\n", + ") & (Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + "))\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", "p0 & p1\n", "\u2777\n", "\n", - "\n", - "1\n", - "\n", - "1\n", + "\n", + "2\n", + "\n", + "2\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "4->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2776\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!p0 & !p1\n", + "1->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", "\n", - "\n", - "3->4\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "!p0 & !p1\n", + "3->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "!p0 & p1\n", + "2->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "f\n", + "\n", + "Fin(\n", + "\u2777\n", + ") & (Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + "))\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\u2776\n", "\n", - "\n", - "2\n", - "\n", - "2\n", + "\n", + "1\n", + "\n", + "1\n", "\n", - "\n", - "4->2\n", - "\n", - "\n", + "\n", + "4->1\n", + "\n", + "\n", "p0 & p1\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "2->0\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "p0 & p1\n", - "\n", - "\n", - "
\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "!p0 & !p1\n", + "\u2777\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "4->2\n", - "\n", - "\n", - "!p0 & p1\n", + "4->2\n", + "\n", + "\n", + "!p0 & p1\n", "\n", - "\n", - "1\n", - "\n", - "1\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2776\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!p0 & p1\n", - "\u24ff\n", - "\u2777\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "f\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "
\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2777\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2777\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "p0 & !p1\n", - "\u24ff\n", - "\u2776\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", - "\u2776\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2777\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2777\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "p0 & !p1\n", - "\u24ff\n", - "\u2776\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", - "\u2776\n", - "\n", - "\n", - "
\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "p0 & p1\n", - "\u2776\n", - "\n", - "\n", - "2->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "p0 & p1\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!p0 & p1\n", - "\u2776\n", - "\u2777\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\u24ff\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2776\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2777\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "p0 & p1\n", - "\u2776\n", - "\n", - "\n", - "2->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "p0 & p1\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!p0 & p1\n", - "\u2776\n", - "\u2777\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\u24ff\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2776\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2777\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "
\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2777\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "p0 & !p1\n", - "\u24ff\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", - "\u2776\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\n", + "3->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2777\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "p0 & !p1\n", - "\u24ff\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", - "\u2776\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\n", - "\n", - "\n", - "2->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\n", - "\n", - "\n", - "
\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "p0 & p1\n", - "\u2777\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "p0 & p1\n", - "\u2777\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u24ff\n", - "\u2777\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "p0 & p1\n", - "\u2777\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "p0 & p1\n", - "\u2777\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u24ff\n", - "\u2777\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", - "\n", - "\n", - "
\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "p0 & p1\n", - "\u2777\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "!p0 & p1\n", - "\u2776\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!p0 & p1\n", - "\u24ff\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u24ff\n", - "\u2776\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "p0 & p1\n", - "\u2776\n", - "\u2777\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")&Inf(\n", - "\u2777\n", - ")\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "p0 & p1\n", - "\u2777\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "!p0 & p1\n", - "\u2776\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!p0 & p1\n", - "\u24ff\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u24ff\n", - "\u2776\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "p0 & p1\n", - "\u2776\n", - "\u2777\n", + "2->2\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "
" @@ -1947,7 +2034,7 @@ "output_type": "pyout", "prompt_number": 2, "text": [ - "" + "" ] } ], @@ -1959,7 +2046,8 @@ "input": [], "language": "python", "metadata": {}, - "outputs": [] + "outputs": [], + "prompt_number": 3 } ], "metadata": {}