diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 2faf91e09..68f4fa424 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -866,29 +866,27 @@ In most tools =%F= and =%L= are the input filename and line number, but as this makes no sense in =randaut=, these two sequences emit numbers related to the generation of automata. -For instance let's generate 100 random automata with 10 states and +For instance let's generate 1000 random automata with 100 states and density 0.2, and just count the number of edges in each automaton. Then use =R= to summarize the distribution of these values: #+BEGIN_SRC sh :results verbatim :exports both -randaut -d0.2 -Q10 -n1000 a --stats %e > size.csv +randaut -d0.2 -Q100 -n1000 a --stats %e > size.csv R --slave -e "summary(read.csv('size.csv', header=FALSE, col.names='edges'))" #+END_SRC #+RESULTS: : edges -: Min. :14.00 -: 1st Qu.:22.00 -: Median :25.00 -: Mean :24.72 -: 3rd Qu.:27.00 -: Max. :36.00 - - -For $Q=10$ states and density $D=0.2$ the expected degree of each -state is $1+(Q-1)D = 1+9\times 0.2 = 2.8$, so the expected number of -edges should be 10 times that. +: Min. :1939 +: 1st Qu.:2056 +: Median :2083 +: Mean :2082 +: 3rd Qu.:2107 +: Max. :2233 +For $Q=100$ states and density $D=0.2$ the expected degree of each +state is $1+(Q-1)D = 1+99\times 0.2 = 20.8$, so the expected number of +edges should be $20.8\times100=2080$. * Naming automata diff --git a/src/misc/random.hh b/src/misc/random.hh index ac820cebe..b7d04a6d4 100644 --- a/src/misc/random.hh +++ b/src/misc/random.hh @@ -23,6 +23,7 @@ #pragma once #include "common.hh" +#include #include #include @@ -72,7 +73,7 @@ namespace spot /// \brief Compute pseudo-random integer value between 0 /// and \a n included, following a binomial distribution - /// for probability \a p. + /// with probability \a p. /// /// \a gen must be a random function computing a pseudo-random /// double value following a standard normal distribution. @@ -93,18 +94,16 @@ namespace spot int rand() const { - int res; - for (;;) { - double x = gen() * s_ + m_; - if (x < 0.0) + int x = round(gen() * s_ + m_); + if (x < 0) continue; - res = static_cast (x); - if (res <= n_) - break; + if (x <= n_) + return x; } - return res; + SPOT_UNREACHABLE(); + return 0; } protected: const int n_; diff --git a/src/tests/randaut.test b/src/tests/randaut.test index 633fea7bb..4d32f4480 100755 --- a/src/tests/randaut.test +++ b/src/tests/randaut.test @@ -59,10 +59,10 @@ test `expr $a + $b` = 100 $randaut -n 5 --name='%F-%L-%s-%c-%e' -H a | grep '^name' >out cat >expected< output cat output cat >expected <beforeafter\n", - "\n", + "
beforeafter
\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\u2776\n", - ") | (Fin(\n", - "\u2777\n", - ") & Fin(\n", - "\u2778\n", - ") & Fin(\n", - "\u24ff\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", + "!p0 & p1\n", "\n", "\n", - "4->0\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", - "\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", - "\u2777\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", - "\u2778\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", - "\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", - "1->3\n", - "\n", - "\n", - "p0 & p1\n", - "\n", - "\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", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "p0 & !p1\n", + "4->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\u2777\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", - "\u2777\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2777\n", - "\u2778\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2777\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "(Fin(\n", - "\u24ff\n", - ") & Fin(\n", - "\u2777\n", - ")) | Inf(\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", - "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", - "\u2776\n", - "\u2777\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "p0 & !p1\n", - "\u2776\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", + "!p0 & p1\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", - "\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", + "4->3\n", + "\n", + "\n", + "!p0 & !p1\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", + "1\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\u2778\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\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", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\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", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "4->3\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", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u24ff\n", + ") & Fin(\n", + "\u2778\n", + ")) | (Fin(\n", + "\u2777\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", + "\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", + "\u2778\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "3->0\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", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u24ff\n", + ") & Fin(\n", + "\u2777\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", + "\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", + "\u2777\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "3->0\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", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u2776\n", + ") & Inf(\n", + "\u2777\n", + ")) | (Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2778\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", + "\u2777\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "3->2\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", + "2->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u2776\n", + ") | (Inf(\n", + "\u24ff\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", + "\u2776\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "3->2\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", + "2->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ") | Fin(\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", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\u2778\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\u2778\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2778\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", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ") | Fin(\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", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\u2778\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\u2778\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2778\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", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u2777\n", + ") | Inf(\n", + "\u2778\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", + "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", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\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", + "4->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "4->1\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", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "2->4\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", + ")\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", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\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", + "4->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "4->1\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", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u2777\n", + ") | Inf(\n", + "\u2776\n", + ")) & (Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2778\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", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u2777\n", + ") | Inf(\n", + "\u2776\n", + ")) & (Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2778\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", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u24ff\n", + ") & (Inf(\n", + "\u2776\n", + ")&Inf(\n", + "\u2777\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", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", "!p0 & !p1\n", - "\u2777\n", - "\u2778\n", + "\u2777\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!p0 & p1\n", - "\u2778\n", + "\n", + "3->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\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", + "p0 & !p1\n", + "\u24ff\n", + "\u2778\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "p0 & !p1\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", + "2->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\u2778\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", - "\n", - "3->4\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "2->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", "\n", - "\n", - "4->2\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "4->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\u2778\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "f\n", + "\n", + "(Fin(\n", + "\u24ff\n", + ") & (Inf(\n", + "\u2776\n", + ")&Inf(\n", + "\u2777\n", + "))) | Fin(\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", + "0->0\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", + "\u2777\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "3->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", + "\u24ff\n", + "\u2778\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\u2778\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u2776\n", + "\u2778\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "((Fin(\n", + "\u2777\n", + ")|Fin(\n", + "\u2778\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", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2778\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2778\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2778\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "(Fin(\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", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "
\n", + "\n", + "G\n", + "\n", + "(Inf(\n", + "\u2776\n", + ") | (Fin(\n", + "\u24ff\n", + ")|Fin(\n", + "\u2777\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", + "\u2776\n", + "\u2778\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\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", + "2\n", + "\n", + "2\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "p0 & p1\n", + "1->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "4->2\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", + "\u2778\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "3\n", - "\n", - "3\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->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", + "3->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2778\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", + "!p0 & !p1\n", + "\u2777\n", "\n", "\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", + "(Inf(\n", + "\u2776\n", + ") | (Fin(\n", + "\u24ff\n", + ")|Fin(\n", + "\u2777\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", "0->0\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\u2778\n", "\n", "\n", "1\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", + "p0 & p1\n", + "\u24ff\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "4\n", + "\n", + "4\n", "\n", - "\n", - "2->4\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "1->4\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", - "\n", - "3->2\n", - "\n", - "\n", - "p0 & p1\n", - "\u24ff\n", - "\u2778\n", + "\n", + "2\n", + "\n", + "2\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2777\n", + "\n", + "1->2\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "4->0\n", - "\n", - "\n", - "!p0 & p1\n", - "\u2777\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\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", + "4->2\n", + "\n", + "\n", + "p0 & p1\n", + "\u2778\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", "\n", - "\n", - "1->3\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "4->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\u2778\n", "\n", - "\n", - "2\n", - "\n", - "2\n", + "\n", + "2->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2778\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "p0 & p1\n", - "\u2776\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "p0 & p1\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2777\n", "\n", "\n", - "\n", - "\n", + "
\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\u24ff\n", - ")|Fin(\n", - "\u2776\n", - ")|Fin(\n", - "\u2777\n", - ")\n", + "\n", + "(Fin(\n", + "\u2777\n", + ")|Fin(\n", + "\u2778\n", + ")) | (Fin(\n", + "\u2776\n", + ") & Inf(\n", + "\u24ff\n", + "))\n", "\n", "\n", "0\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", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!p0 & !p1\n", - "\u2776\n", - "\u2778\n", + "\n", + "\n", + "p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", - "\n", - "0->3\n", - "\n", - "\n", - "p0 & p1\n", - "\u2777\n", - "\u2778\n", + "\n", + "1->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\u2778\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!p0 & p1\n", - "\u2778\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", - "\n", - "3->0\n", - "\n", - "\n", - "p0 & p1\n", - "\u2777\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", "\n", "\n", "4\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", - "\u2776\n", - "\u2777\n", - "\u2778\n", + "\n", + "4->1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "f\n", + "\n", + "(Fin(\n", + "\u2777\n", + ")|Fin(\n", + "\u2778\n", + ")) | (Fin(\n", + "\u2776\n", + ") & Inf(\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", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", - "\n", - "0->3\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "1->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\u2778\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "3->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", + "2->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", "\n", "\n", "4\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", + "4->1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "
" ], "metadata": {}, "output_type": "pyout", - "prompt_number": 3, + "prompt_number": 2, "text": [ - "" + "" ] } ], - "prompt_number": 3 + "prompt_number": 2 }, { "cell_type": "code", @@ -2006,4 +2282,4 @@ "metadata": {} } ] -} +} \ No newline at end of file