diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index 0035936a0..6be931569 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -59,29 +59,31 @@ atomic propositions \"a\" and \"b\":\n\ \n\ This builds three random, complete, and deterministic TGBA with 5 to 10\n\ states, 1 to 3 acceptance sets, and three atomic propositions:\n\ - % randaut -n 3 --hoa -S5..10 -A1..3 3\n\ + % randaut -n3 -D -H -S5..10 -A1..3 3\n\ +\n\ +Build 3 random, complete, and deterministic Rabin automata\n\ +with 2 to 3 acceptance pairs, state-based acceptance, 8 states, \n\ +a high density of transitions, and 3 to 4 atomic propositions:\n\ + % randaut -n3 -D -H -S8 -d.8 --state-based -A 'Rabin 2..3' 3..4\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 }, + { 0, 0, 0, 0, "Generation:", 1 }, + { "acceptance", 'A', "ACCEPTANCE", 0, + "specify the acceptance type of the automaton", 0 }, { "acc-probability", 'a', "FLOAT", 0, "probability that a transition belong to one acceptance set (0.2)", 0 }, { "automata", 'n', "INT", 0, "number of automata to output (1)\n"\ "use a negative value for unbounded generation", 0 }, { "ba", 'B', 0, 0, - "build a Buchi automaton (implies --acc-sets=1 --state-acc)", 0 }, + "build a Buchi automaton (implies --acceptance=Buchi --state-acc)", 0 }, { "density", 'd', "FLOAT", 0, "density of the transitions (0.2)", 0 }, { "deterministic", 'D', 0, 0, "build a complete, deterministic automaton ", 0 }, @@ -93,6 +95,25 @@ static const argp_option options[] = { "states", 'S', "RANGE", 0, "number of states to output (10)", 0 }, { "state-acc", OPT_STATE_ACC, 0, 0, "use state-based acceptance", 0 }, RANGE_DOC, + { 0, 0, 0, 0, "ACCEPTANCE may be either a RANGE (in which case " + "generalized Büchi is assumed), or an arbitrary acceptance formula " + "such as 'Fin(0)|Inf(1)&Fin(2)' in the same syntax as in the HOA " + "format, or one of the following patterns:\n" + " none\n" + " all\n" + " Buchi\n" + " co-Buchi\n" + " generalized-Buchi RANGE\n" + " generalized-co-Buchi RANGE\n" + " Rabin RANGE\n" + " Streett RANGE\n" + " generalized-Rabin INT RANGE RANGE ... RANGE\n" + " parity (min|max|rand) (odd|even|rand) RANGE\n" + " random RANGE\n" + " random RANGE PROBABILITY\n" + "The random acceptance condition uses each set only once, " + "unless a probability (to reuse the set again every time it is used) " + "is given.", 2 }, /**************************************************/ { 0, 0, 0, 0, "Miscellaneous options:", -1 }, { 0, 0, 0, 0, 0, 0 } @@ -107,27 +128,11 @@ 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; +static const char* opt_acceptance = nullptr; typedef spot::twa_graph::graph_t::trans_storage_t tr_t; typedef std::set> unique_aut_t; static spot::ltl::atomic_prop_set aprops; -static bool ap_count_given = false; +static range ap_count_given = {-1, -2}; // Must be two different negative val static int opt_seed = 0; static const char* opt_seed_str = "0"; static int opt_automata = 1; @@ -138,6 +143,8 @@ static float opt_acc_prob = 0.2; static bool opt_deterministic = false; static bool opt_state_acc = false; static bool ba_wanted = false; +static bool generic_wanted = false; +static bool gba_wanted = false; static std::unique_ptr opt_uniq = nullptr; static void @@ -147,6 +154,18 @@ ba_options() opt_state_acc = true; } +// Range should have the form 12..34 or 12:34, maybe with spaces. The +// characters between '.' and ':' include all digits plus '/', but the +// parser will later choke on '/' if it is used, so let's not worry +// here. +static bool +looks_like_a_range(const char* str) +{ + while (*str == ' ' || (*str >= '.' && *str <= ':')) + ++str; + return !*str; +} + static int parse_opt(int key, char* arg, struct argp_state* as) { @@ -163,11 +182,20 @@ parse_opt(int key, char* arg, struct argp_state* as) "should be between 0.0 and 1.0"); break; case 'A': - opt_acc_sets = parse_range(arg); - if (opt_acc_sets.min > opt_acc_sets.max) - std::swap(opt_acc_sets.min, opt_acc_sets.max); - if (opt_acc_sets.min < 0) - error(2, 0, "number of acceptance sets should be positive"); + if (looks_like_a_range(arg)) + { + opt_acc_sets = parse_range(arg); + if (opt_acc_sets.min > opt_acc_sets.max) + std::swap(opt_acc_sets.min, opt_acc_sets.max); + if (opt_acc_sets.min < 0) + error(2, 0, "number of acceptance sets should be positive"); + gba_wanted = true; + } + else + { + opt_acceptance = arg; + generic_wanted = true; + } break; case 'B': ba_options(); @@ -193,9 +221,6 @@ 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; @@ -211,16 +236,13 @@ parse_opt(int key, char* arg, struct argp_state* as) // non-options. So if as->argc == as->next we know this is the // last non-option argument, and if aprops.empty() we know this // is the also the first one. - if (aprops.empty() && as->argc == as->next) + if (aprops.empty() && as->argc == as->next && looks_like_a_range(arg)) { - char* endptr; - int res = strtol(arg, &endptr, 10); - if (!*endptr && res >= 0) // arg is a number - { - ap_count_given = true; - aprops = spot::ltl::create_atomic_prop_set(res); - break; - } + ap_count_given = parse_range(arg); + // Create the set once if the count is fixed. + if (ap_count_given.min == ap_count_given.max) + aprops = spot::ltl::create_atomic_prop_set(ap_count_given.min); + break; } aprops.insert(spot::ltl::default_environment::instance().require(arg)); break; @@ -247,22 +269,26 @@ main(int argc, char** argv) // running 'randaut 0' is one way to generate automata using no // atomic propositions so do not complain in that case. - if (aprops.empty() && !ap_count_given) + if (aprops.empty() && ap_count_given.max < 0) error(2, 0, "No atomic proposition supplied? Run '%s --help' for usage.", program_name); + if (generic_wanted && automaton_format == Spin) + error(2, 0, "--spin implies --ba so should not be used with --acceptance"); + if (generic_wanted && ba_wanted) + error(2, 0, "--acceptance and --ba may not be used together"); + if (automaton_format == Spin && opt_acc_sets.max > 1) - error(2, 0, "--spin is incompatible with --acc-sets=%d..%d", + error(2, 0, "--spin is incompatible with --acceptance=%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", + error(2, 0, "--ba is incompatible with --acceptance=%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"); + if (ba_wanted && generic_wanted) + error(2, 0, "--ba is incompatible with --acceptance=%s", opt_acceptance); + + if (automaton_format == Spin) + ba_options(); try { @@ -281,6 +307,14 @@ main(int argc, char** argv) spot::stopwatch sw; sw.start(); + if (ap_count_given.max > 0 + && ap_count_given.min != ap_count_given.max) + { + spot::ltl::destroy_atomic_prop_set(aprops); + int c = spot::rrand(ap_count_given.min, ap_count_given.max); + aprops = spot::ltl::create_atomic_prop_set(c); + } + int size = opt_states.min; if (size != opt_states.max) size = spot::rrand(size, opt_states.max); @@ -289,20 +323,20 @@ main(int argc, char** argv) if (accs != opt_acc_sets.max) accs = spot::rrand(accs, opt_acc_sets.max); + spot::acc_cond::acc_code code; + if (opt_acceptance) + { + code = spot::parse_acc_code(opt_acceptance); + accs = code.used_sets().max_set(); + } + auto aut = spot::random_graph(size, opt_density, &aprops, d, 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_acceptance) + aut->set_acceptance(accs, code); if (opt_uniq) { diff --git a/src/tests/randaut.test b/src/tests/randaut.test index 6a3839572..095a49e64 100755 --- a/src/tests/randaut.test +++ b/src/tests/randaut.test @@ -82,19 +82,54 @@ 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 +( + $randaut -n 2 -S5 -A4 -H 2 + $randaut -A 'random 4' -n 2 -S5 -H 2 + $randaut -A 'parity rand rand 2..4' -n3 -S5 -H 2 + $randaut -A 'generalized-Rabin 3 1..2 2..3 0' -n3 -S5 -H 2 +) | grep -E '(acc-name:|Acceptance:)' > output cat output +a=Acceptance 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 +$randaut --spin -A 'random 2' 2 2>stderr && exit 1 +grep 'randaut: --spin.*--acceptance' stderr +$randaut --ba --acceptance='random 2' 2 2>stderr && exit 1 +grep 'randaut: --acceptance.*--ba' stderr + +$randaut -n 10 2..4 -H | grep AP: > output +cat output +cat >expected <0 are always satisfiable, so it makes sense + // that it should be satisfiable for n_accs=0 as well.) + if (n_accs == 0) + return {}; + + std::vector codes; + codes.reserve(n_accs); + for (unsigned i = 0; i < n_accs; ++i) + { + if (drand() < 0.5) + codes.push_back(inf({i})); + else + codes.push_back(fin({i})); + if (reuse > 0.0 && drand() < reuse) + --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]; + } + namespace { bdd to_bdd_rec(const acc_cond::acc_word* c, const bdd* map) @@ -1284,12 +1326,75 @@ namespace spot if (errno || num != n) { std::ostringstream s; - s << "syntax error at '" << input << "': value too large."; + s << "syntax error at '" << input << "': invalid number."; throw parse_error(s.str()); } input = end; + return n; + } - return num; + static unsigned parse_range(const char*& str) + { + skip_space(str); + int min; + int max; + char* end; + errno = 0; + min = strtol(str, &end, 10); + if (end == str || errno) + { + // No leading number. It's OK as long as the string is not + // empty. + if (!*end || errno) + { + std::ostringstream s; + s << "syntax error at '" << str << "': invalid range."; + throw parse_error(s.str()); + } + min = 1; + } + if (!*end || (*end != ':' && *end != '.')) + { + // Only one number. + max = min; + } + else + { + // Skip : or .. + if (end[0] == ':') + ++end; + else if (end[0] == '.' && end[1] == '.') + end += 2; + + // Parse the next integer. + char* end2; + max = strtol(end, &end2, 10); + if (end == end2 || errno) + { + std::ostringstream s; + s << "syntax error at '" << str + << "': invalid range (missing end?)"; + throw parse_error(s.str()); + } + end = end2; + } + + if (min < 0 || max < 0) + { + std::ostringstream s; + s << "invalid range '" << str + << "': values must be positive"; + throw parse_error(s.str()); + } + + str = end; + + if (min == max) + return min; + + if (min > max) + std::swap(min, max); + return spot::rrand(min, max); } static unsigned parse_par_num(const char*& input) @@ -1302,6 +1407,28 @@ namespace spot return num; } + static double parse_proba(const char*& input) + { + errno = 0; + char* end; + double n = strtod(input, &end); + if (errno) + { + std::ostringstream s; + s << "syntax error at '" << input << "': can't convert to double"; + throw parse_error(s.str()); + } + if (!(n >= 0.0 && n <= 1.0)) + { + std::ostringstream s; + s << "syntax error at '" << input + << "': value should be between 0 and 1."; + throw parse_error(s.str()); + } + input = end; + return n; + } + static acc_cond::acc_code parse_term(const char*& input) { acc_cond::acc_code res; @@ -1366,6 +1493,16 @@ namespace spot input += 3; return false; } + if (!strncmp(input, "rand", 4)) + { + input += 4; + return drand() < 0.5; + } + if (!strncmp(input, "random", 6)) + { + input += 6; + return drand() < 0.5; + } std::ostringstream s; s << "syntax error at '" << input << "': expecting 'min' or 'max'"; @@ -1385,6 +1522,16 @@ namespace spot input += 4; return false; } + if (!strncmp(input, "rand", 4)) + { + input += 4; + return drand() < 0.5; + } + if (!strncmp(input, "random", 6)) + { + input += 6; + return drand() < 0.5; + } std::ostringstream s; s << "syntax error at '" << input << "': expecting 'odd' or 'even'"; @@ -1420,22 +1567,22 @@ namespace spot else if (!strncmp(input, "generalized-Buchi", 17)) { input += 17; - c = acc_cond::acc_code::generalized_buchi(parse_num(input)); + c = acc_cond::acc_code::generalized_buchi(parse_range(input)); } else if (!strncmp(input, "generalized-co-Buchi", 20)) { input += 20; - c = acc_cond::acc_code::generalized_co_buchi(parse_num(input)); + c = acc_cond::acc_code::generalized_co_buchi(parse_range(input)); } else if (!strncmp(input, "Rabin", 5)) { input += 5; - c = acc_cond::acc_code::rabin(parse_num(input)); + c = acc_cond::acc_code::rabin(parse_range(input)); } else if (!strncmp(input, "Streett", 7)) { input += 7; - c = acc_cond::acc_code::streett(parse_num(input)); + c = acc_cond::acc_code::streett(parse_range(input)); } else if (!strncmp(input, "generalized-Rabin", 17)) { @@ -1445,7 +1592,7 @@ namespace spot v.reserve(num); while (num > 0) { - v.push_back(parse_num(input)); + v.push_back(parse_range(input)); --num; } c = acc_cond::acc_code::generalized_rabin(v.begin(), v.end()); @@ -1455,9 +1602,19 @@ namespace spot input += 6; bool max = max_or_min(input); bool odd = odd_or_even(input); - unsigned num = parse_num(input); + unsigned num = parse_range(input); c = acc_cond::acc_code::parity(max, odd, num); } + else if (!strncmp(input, "random", 6)) + { + input += 6; + unsigned n = parse_range(input); + skip_space(input); + double reuse = (*input) ? parse_proba(input) : 0.0; + if (reuse >= 1.0) + throw parse_error("probability for set reuse should be <1."); + c = acc_cond::acc_code::random(n, reuse); + } else { c = parse_acc(input); diff --git a/src/twa/acc.hh b/src/twa/acc.hh index d31b56496..1506d7fb4 100644 --- a/src/twa/acc.hh +++ b/src/twa/acc.hh @@ -521,6 +521,11 @@ namespace spot static acc_code parity(bool max, bool odd, unsigned sets); + // Number of acceptance sets to use, and probability to reuse + // each set another time after it has been used in the + // acceptance formula. + static acc_code random(unsigned n, double reuse = 0.0); + void append_and(acc_code&& r) { if (is_true() || r.is_false()) diff --git a/src/twaalgos/randomgraph.cc b/src/twaalgos/randomgraph.cc index 8538533f0..1979242ff 100644 --- a/src/twaalgos/randomgraph.cc +++ b/src/twaalgos/randomgraph.cc @@ -240,42 +240,4 @@ namespace spot delete[] props; 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/wrap/python/tests/randaut.ipynb b/wrap/python/tests/randaut.ipynb index 0366eafa2..5a1d19bcb 100644 --- a/wrap/python/tests/randaut.ipynb +++ b/wrap/python/tests/randaut.ipynb @@ -1,7 +1,23 @@ { "metadata": { - "name": "", - "signature": "sha256:0282f226c25df3a47177f96c3d474c1f5191fa8f7d87a35445a3d0d978bb8e35" + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.4.3+" + }, + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -19,14 +35,14 @@ "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 1 + "prompt_number": 2 }, { "cell_type": "code", "collapsed": false, "input": [ "txt = \"\"\n", - "for a in spot.automata('randaut --acc-type=random -H -S5 -A4 -n10 2|'):\n", + "for a in spot.automata('randaut -A \"random 4\" -H -S5 -n10 2|'):\n", " txt += \"\".format(a.show('.a').data, spot.cleanup_acceptance(a).show('.a').data)\n", "txt += (\"
beforeafter
{0}{1}
\")\n", "HTML(txt)" @@ -36,2003 +52,1946 @@ "outputs": [ { "html": [ - "
beforeafter
\n", - "\n", + "
beforeafter
\n", + "\n", "G\n", - "\n", - "(Fin(\n", - "\u2777\n", - ") & Inf(\n", - "\u2778\n", - ")) | Inf(\n", - "\u24ff\n", - ") | Fin(\n", - "\u2776\n", - ")\n", + "\n", + "Fin(\n", + "\u2776\n", + ") | (Fin(\n", + "\u2777\n", + ") & Fin(\n", + "\u2778\n", + ") & Fin(\n", + "\u24ff\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", - "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", - "\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", - "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", + "!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", + "4->0\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", - "\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", + "3\n", + "\n", + "3\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", - "3->0\n", - "\n", - "\n", - "p0 & !p1\n", + "3->0\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", - "\u2776\n", + "3->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2778\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "(Fin(\n", - "\u2777\n", - ") & Inf(\n", - "\u2776\n", - ")) | Fin(\n", - "\u24ff\n", - ")\n", + "\n", + "Fin(\n", + "\u24ff\n", + ") | (Fin(\n", + "\u2776\n", + ") & Fin(\n", + "\u2777\n", + "))\n", "\n", "\n", "0\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", "\n", "\n", - "4\n", - "\n", - "4\n", + "4\n", + "\n", + "4\n", "\n", - "\n", - "2->4\n", - "\n", - "\n", - "p0 & p1\n", - "\u2776\n", + "\n", + "0->4\n", + "\n", + "\n", + "!p0 & p1\n", "\n", - "\n", - "4->2\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "4->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2776\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", - "3->0\n", - "\n", - "\n", - "p0 & !p1\n", + "3->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u2777\n", + ") | ((Inf(\n", + "\u24ff\n", + ") | Inf(\n", + "\u2776\n", + ")) & Fin(\n", + "\u2778\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", + "\u2778\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\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", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\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", + "\u2777\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ") | Inf(\n", + "\u2778\n", + ") | (Fin(\n", + "\u2777\n", + ") & Fin(\n", + "\u2776\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", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ") | Inf(\n", + "\u2778\n", + ") | (Fin(\n", + "\u2777\n", + ") & Fin(\n", + "\u2776\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", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u24ff\n", + ") & Fin(\n", + "\u2778\n", + ") & Fin(\n", + "\u2776\n", + ")) | Inf(\n", + "\u2777\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", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2778\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", + "\n", + "\n", + "!p0 & !p1\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", + "4->0\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", + "4->4\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\u2777\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2777\n", + "\u2778\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", + "2->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2777\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "(Inf(\n", - "\u2777\n", - ") | Inf(\n", - "\u24ff\n", - ")) & Fin(\n", - "\u2776\n", - ")\n", + "\n", + "(Fin(\n", + "\u24ff\n", + ") & Fin(\n", + "\u2777\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", - "0->0\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u24ff\n", + "\n", + "3\n", + "\n", + "3\n", "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "p0 & p1\n", - "\u2776\n", - "\u2777\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "3->1\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->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\u2777\n", "\n", - "\n", - "2\n", - "\n", - "2\n", + "\n", + "2->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", "\n", - "\n", - "4->2\n", - "\n", - "\n", - "p0 & p1\n", - "\u2776\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u2776\n", + ") | Inf(\n", + "\u2777\n", + ") | Fin(\n", + "\u2778\n", + ") | Inf(\n", + "\u24ff\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", + "\u24ff\n", + "\u2776\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "\n", + "4->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", + "2->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\u2778\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u2776\n", + ") | Inf(\n", + "\u2777\n", + ") | Fin(\n", + "\u2778\n", + ") | Inf(\n", + "\u24ff\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", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "4->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", + "2->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\u2778\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u2778\n", + ") & Fin(\n", + "\u2777\n", + ") & Fin(\n", + "\u24ff\n", + ") & Inf(\n", + "\u2776\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", + "\u2778\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "1->1\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", + "\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", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "p0 & p1\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", + "1->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1->1\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", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\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", + "\u2776\n", + ") | Fin(\n", + "\u2777\n", + ")) & Fin(\n", + "\u24ff\n", + ") & Fin(\n", + "\u2778\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\u2778\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", + "1\n", + "\n", + "1\n", + "\u2778\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\u24ff\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "(Inf(\n", + "\u2776\n", + ") | Fin(\n", + "\u2777\n", + ")) & Fin(\n", + "\u24ff\n", + ") & Fin(\n", + "\u2778\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\u2778\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", + "1\n", + "\n", + "1\n", + "\u2778\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\u24ff\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u2777\n", + ") & (Inf(\n", + "\u24ff\n", + ") | Fin(\n", + "\u2776\n", + ")) & Inf(\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", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "2->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", + "3->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\u2778\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "p0 & p1\n", - "\u2776\n", + "3->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2777\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", - "2\n", - "\n", - "2\n", + "\n", + "4->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2777\n", "\n", "\n", "4->2\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2777\n", "\n", - "\n", - "1->0\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", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u24ff\n", - "\u2776\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\u24ff\n", - "\n", - "\n", - "2->0\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u24ff\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "4->4\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\u2777\n", - ") & (Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - "))\n", + "\n", + "Fin(\n", + "\u2777\n", + ") & (Inf(\n", + "\u24ff\n", + ") | Fin(\n", + "\u2776\n", + ")) & Inf(\n", + "\u2778\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", - "\n", - "0->4\n", - "\n", - "\n", - "!p0 & p1\n", - "\u24ff\n", - "\u2776\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", - "\n", - "4->1\n", - "\n", - "\n", - "p0 & p1\n", - "\u2777\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", - "\n", - "4->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!p0 & p1\n", - "\u2776\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2777\n", + "\u2778\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u24ff\n", - "\u2776\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\u24ff\n", - "\n", - "\n", - "2->0\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u24ff\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "p0 & !p1\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->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\u2778\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u2778\n", + ") | Inf(\n", + "\u2777\n", + ") | Fin(\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", + "\u2776\n", + "\u2778\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\u2778\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", + "\u2776\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")|Fin(\n", + "\u2776\n", + ")|Fin(\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", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "4->1\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", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u2778\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", + "\u2776\n", + "\u2778\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "3->1\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", + "\u2776\n", + "\u2777\n", + "\u2778\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", + "0->3\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", + "3->0\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "3->1\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", "
" ], "metadata": {}, "output_type": "pyout", - "prompt_number": 2, + "prompt_number": 3, "text": [ - "" + "" ] } ], - "prompt_number": 2 + "prompt_number": 3 }, { "cell_type": "code",