diff --git a/notebooks/presentations/LPOP18.ipynb b/notebooks/presentations/LPOP18.ipynb index e150e6f92ad4b7add653520086abac86f18ff47d..6fd4bae5f2f7a8d6cf4c14b6bc88f7b5a0a5d237 100644 --- a/notebooks/presentations/LPOP18.ipynb +++ b/notebooks/presentations/LPOP18.ipynb @@ -2289,69 +2289,32 @@ }, { "cell_type": "code", - "execution_count": 61, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $y1 = TRUE$\n", - "* $x1 = TRUE$\n", - "* $y2 = TRUE$\n", - "* $x2 = FALSE$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\ty1 = TRUE\n", - "\tx1 = TRUE\n", - "\ty2 = TRUE\n", - "\tx2 = FALSE" - ] - }, - "execution_count": 61, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "{x1,x2,y1,y2} <: BOOL &\n", - " x1=TRUE or y1=TRUE & x2=TRUE or y2=TRUE & // x \\/ y = 1..2\n", - " x1=TRUE & // 1:x \n", - " (x1=TRUE => y1=TRUE) & (x2=TRUE => y2=TRUE) & (x1/=y1 or x2/=y2) // x <<: y" - ] - }, - { - "cell_type": "code", - "execution_count": 62, + "execution_count": 55, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "|Nr|x1|x2|y1|y2|\n", - "|---|---|---|---|---|\n", - "|1|TRUE|FALSE|TRUE|TRUE|\n" + "|x1|x2|y1|y2|\n", + "|---|---|---|---|\n", + "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n" ], "text/plain": [ - "Nr\tx1\tx2\ty1\ty2\n", - "1\tTRUE\tFALSE\tTRUE\tTRUE\n" + "x1\tx2\ty1\ty2\n", + "TRUE\tFALSE\tTRUE\tTRUE\n" ] }, - "execution_count": 62, + "execution_count": 55, "metadata": {}, "output_type": "execute_result" } ], "source": [ ":table {x1,x2,y1,y2 | {x1,x2,y1,y2} <: BOOL &\n", - " x1=TRUE or y1=TRUE & x2=TRUE or y2=TRUE & \n", + " (x1=TRUE or y1=TRUE) & (x2=TRUE or y2=TRUE) & // x ∪ y = 1..2\n", " x1=TRUE & // 1:x \n", - " (x1=TRUE => y1=TRUE) & (x2=TRUE => y2=TRUE) & (x1/=y1 or x2/=y2) }" + " (x1=TRUE => y1=TRUE) & (x2=TRUE => y2=TRUE) & (x1/=y1 or x2/=y2) //x ⊂ y\n", + " }" ] }, { @@ -2647,8 +2610,8 @@ } ], "source": [ - "∀ smt_tmp28.(smt_tmp28 ∈ x ⇒ smt_tmp28 ≥ 1 & 2 ≥ smt_tmp28) & \n", - "∀ smt_tmp29.(smt_tmp29 ∈ y ⇒ smt_tmp29 ≥ 1 & 2 ≥ smt_tmp29) &\n", + "∀ smt_tmp28.(smt_tmp28 ∈ x ⇒ smt_tmp28 ≥ 1 & 2 ≥ smt_tmp28) & // x ⊆ 1..2\n", + "∀ smt_tmp29.(smt_tmp29 ∈ y ⇒ smt_tmp29 ≥ 1 & 2 ≥ smt_tmp29) & // y ⊆ 1..2\n", "x ∪ y = {1,2}" ] }, @@ -2702,15 +2665,15 @@ }, { "cell_type": "code", - "execution_count": 70, + "execution_count": 56, "metadata": {}, "outputs": [ { "ename": "CommandExecutionException", - "evalue": ":solve: Computation not completed: time out", + "evalue": ":solve: Computation not completed: no solution found (but one might exist)", "output_type": "error", "traceback": [ - "\u001b[1m\u001b[31m:solve: Computation not completed: time out\u001b[0m" + "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m" ] } ], @@ -2775,7 +2738,7 @@ }, { "cell_type": "code", - "execution_count": 72, + "execution_count": 57, "metadata": { "slideshow": { "slide_type": "subslide" @@ -2791,7 +2754,7 @@ "f = {(1↦3),(2↦6)} ∧ (∃ /* LET */ (st13).( (st13)=r ∧ ∀st15·(st15 ∈ st13 ⇒ ∃st16·(6 ↦ st15 ∈ st16 ∧ (∀(st17,st18)·(st17 ↦ st18 ∈ st16 ⇒ st18 ↦ st17 ∈ f) ∧ ∀(st17,st18)·(st18 ↦ st17 ∈ f ⇒ st17 ↦ st18 ∈ st16)))) ∧ ∀st15·(∃st19·(6 ↦ st15 ∈ st19 ∧ (∀(st20,st21)·(st20 ↦ st21 ∈ st19 ⇒ st21 ↦ st20 ∈ f) ∧ ∀(st20,st21)·(st21 ↦ st20 ∈ f ⇒ st20 ↦ st21 ∈ st19))) ⇒ st15 ∈ st13)))" ] }, - "execution_count": 72, + "execution_count": 57, "metadata": {}, "output_type": "execute_result" } @@ -2808,7 +2771,7 @@ }, { "cell_type": "code", - "execution_count": 73, + "execution_count": 58, "metadata": { "slideshow": { "slide_type": "subslide" @@ -2818,10 +2781,10 @@ { "data": { "text/markdown": [ - "Execution time: 0.058100600 seconds" + "Execution time: 0.140791514 seconds" ], "text/plain": [ - "Execution time: 0.058100600 seconds" + "Execution time: 0.140791514 seconds" ] }, "metadata": {}, @@ -2830,11 +2793,11 @@ { "data": { "text/markdown": [ - "$TRUE$\n", + "$\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $r = \\{2\\}$\n", - "* $f = \\{(1\\mapsto3),(2\\mapsto6)\\}$" + "* $\\mathit{r} = \\{2\\}$\n", + "* $\\mathit{f} = \\{(1\\mapsto 3),(2\\mapsto 6)\\}$" ], "text/plain": [ "TRUE\n", @@ -2844,7 +2807,7 @@ "\tf = {(1↦3),(2↦6)}" ] }, - "execution_count": 73, + "execution_count": 58, "metadata": {}, "output_type": "execute_result" } @@ -2861,7 +2824,7 @@ }, { "cell_type": "code", - "execution_count": 74, + "execution_count": 59, "metadata": {}, "outputs": [ { @@ -2898,19 +2861,19 @@ }, { "cell_type": "code", - "execution_count": 75, + "execution_count": 60, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "$FALSE$" + "$\\mathit{FALSE}$" ], "text/plain": [ "FALSE" ] }, - "execution_count": 75, + "execution_count": 60, "metadata": {}, "output_type": "execute_result" } @@ -2928,19 +2891,19 @@ }, { "cell_type": "code", - "execution_count": 76, + "execution_count": 61, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "$FALSE$" + "$\\mathit{FALSE}$" ], "text/plain": [ "FALSE" ] }, - "execution_count": 76, + "execution_count": 61, "metadata": {}, "output_type": "execute_result" } @@ -2977,7 +2940,7 @@ }, { "cell_type": "code", - "execution_count": 77, + "execution_count": 62, "metadata": { "slideshow": { "slide_type": "fragment" @@ -2993,7 +2956,7 @@ "{0,100,200,300,400,500,600,700,800,900,1000}" ] }, - "execution_count": 77, + "execution_count": 62, "metadata": {}, "output_type": "execute_result" } @@ -3015,18 +2978,18 @@ }, { "cell_type": "code", - "execution_count": 78, + "execution_count": 63, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "$TRUE$\n", + "$\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $mn = 0$\n", - "* $s = \\{0,100,200,300,400,500,600,700,800,900,1000\\}$\n", - "* $mx = 1000$" + "* $\\mathit{mn} = 0$\n", + "* $\\mathit{s} = \\{0,100,200,300,400,500,600,700,800,900,1000\\}$\n", + "* $\\mathit{mx} = 1000$" ], "text/plain": [ "TRUE\n", @@ -3037,7 +3000,7 @@ "\tmx = 1000" ] }, - "execution_count": 78, + "execution_count": 63, "metadata": {}, "output_type": "execute_result" } @@ -3638,21 +3601,21 @@ }, { "cell_type": "code", - "execution_count": 91, + "execution_count": 64, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "$TRUE$\n", + "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $r2 = \\{1,4,9,16,25,36,49,64,81,100\\}$\n", - "* $r3 = [4,9,25,49,121]$\n", - "* $r4 = 256$\n", - "* $sqrt = 10$\n", - "* $f = \\lambdax\\qdot(x \\in INTEGER\\midx * x)$\n", - "* $r1 = 10000000000$" + "* $\\mathit{r2} = \\{1,4,9,16,25,36,49,64,81,100\\}$\n", + "* $\\mathit{r3} = [4,9,25,49,121]$\n", + "* $\\mathit{r4} = 256$\n", + "* $\\mathit{sqrt} = 10$\n", + "* $\\mathit{f} = \\lambda \\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid \\mathit{x} * \\mathit{x})$\n", + "* $\\mathit{r1} = 10000000000$" ], "text/plain": [ "TRUE\n", @@ -3666,7 +3629,7 @@ "\tr1 = 10000000000" ] }, - "execution_count": 91, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -3682,22 +3645,22 @@ }, { "cell_type": "code", - "execution_count": 92, + "execution_count": 65, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "$TRUE$\n", + "$\\newcommand{\\cprod}{\\mathbin\\times}\\newcommand{\\cprod}{\\mathbin\\times}\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $r2 = \\{1,2,3,4\\}$\n", - "* $r3 = [2,2,3,3,4]$\n", - "* $r4 = 2$\n", - "* $r5 = \\{2,4,10,100\\}$\n", - "* $sqr = 9802$\n", - "* $f = \\{x,y\\midx \\in NATURAL \\land y \\cprod 2 \\geq x \\land (y - 1) \\cprod 2 < x\\}$\n", - "* $r1 = 317$" + "* $\\mathit{r2} = \\{1,2,3,4\\}$\n", + "* $\\mathit{r3} = [2,2,3,3,4]$\n", + "* $\\mathit{r4} = 2$\n", + "* $\\mathit{r5} = \\{2,4,10,100\\}$\n", + "* $\\mathit{sqr} = 9802$\n", + "* $\\mathit{f} = \\{\\mathit{x},\\mathit{y}\\mid \\mathit{x} \\in \\mathit{NATURAL} \\land \\mathit{y} \\cprod 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) \\cprod 2 < \\mathit{x}\\}$\n", + "* $\\mathit{r1} = 317$" ], "text/plain": [ "TRUE\n", @@ -3712,7 +3675,7 @@ "\tr1 = 317" ] }, - "execution_count": 92, + "execution_count": 65, "metadata": {}, "output_type": "execute_result" } @@ -3781,366 +3744,6 @@ "" ] }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "slide" - } - }, - "source": [ - "### Relation to SETLOG ###\n", - "\n", - "Setlog (http://people.dmi.unipr.it/gianfranco.rossi/setlog.Home.html) is based on non-deterministic set unification\n", - "Setlog has additional inference rules\n", - "\n", - "The former causes problems with larger sets, in our experience.\n", - "The latter could be added to ProB via CHR, but currently not done.\n", - "\n", - "Let us look at a simpler Setlog example from the article \"{log} as a Test Case Generator\n", - "for the Test Template Framework\" by Cristia, Rossi and Frydman:\n", - "```\n", - "1 in R & 1 nin S & inters(R,S,T) & T = {X}\n", - "```\n", - "This can be encoded in B as follows:" - ] - }, - { - "cell_type": "code", - "execution_count": 94, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $R = \\{1,0\\}$\n", - "* $S = \\{0\\}$\n", - "* $T = \\{0\\}$\n", - "* $X = 0$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tR = {1,0}\n", - "\tS = {0}\n", - "\tT = {0}\n", - "\tX = 0" - ] - }, - "execution_count": 94, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "1:R & 1/:S & R/\\S=T & T={X}" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "Another example from that paper is\n", - "```\n", - "X in int(1,5) & Y in int(4,10) & inters({X},{Y},R) & X >= Y\n", - "```\n", - "which has three solutions\n", - "```\n", - "X=4,Y=4,R={4}; X=5,Y=5,R={5}; X=5,Y=4,R={}.\n", - "```\n", - "Let us check this with ProB:" - ] - }, - { - "cell_type": "code", - "execution_count": 95, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$\\{((4\\mapsto4)\\mapsto\\{4\\}),((5\\mapsto4)\\mapsto\\emptyset),((5\\mapsto5)\\mapsto\\{5\\})\\}$" - ], - "text/plain": [ - "{((4↦4)↦{4}),((5↦4)↦∅),((5↦5)↦{5})}" - ] - }, - "execution_count": 95, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "{X,Y,R|X: 1..5 & Y: 4..10 & {X}/\\{Y}=R & X>=Y}" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "However, in particular with unbounded sets Setlog can solve some constraints that ProB, Z3 and Kodkod cannot:\n", - "```\n", - "un(A,B,D) & disj(A,C) & D=C & ris(X in A,[],true,X) neq {}\n", - "```\n", - "In B this corresponds to:" - ] - }, - { - "cell_type": "code", - "execution_count": 96, - "metadata": {}, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":eval: UNKNOWN (FALSE with enumeration warning)", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:eval: UNKNOWN (FALSE with enumeration warning)\u001b[0m" - ] - } - ], - "source": [ - "A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(STRING)" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "From A\\/B=D we and D=C we could infer A<:C and hence A/\\C=C and hence A={} which is in conflict with A/={}.\n", - "ProB (as well as Kodkod and Z3 backends) can only infer the conflict for finite domains:" - ] - }, - { - "cell_type": "code", - "execution_count": 97, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$FALSE$" - ], - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 97, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(BOOL)" - ] - }, - { - "cell_type": "code", - "execution_count": 98, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$FALSE$" - ], - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 98, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":solve kodkod A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(BOOL)" - ] - }, - { - "cell_type": "code", - "execution_count": 99, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$FALSE$" - ], - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 99, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":solve z3 A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(BOOL)" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "Setlog has problems with larger sets. For example, the following takes 24 seconds using the latest stable release 4.9.1 of Setlog from http://people.dmi.unipr.it/gianfranco.rossi/setlog.Home.html: \n", - "```\n", - "{log}=> diff(int(1,200),{50},R).\n", - "\n", - "R = {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200}\n", - "\n", - "Another solution? (y/n)\n", - "```\n", - "In ProB this is instantenous:" - ] - }, - { - "cell_type": "code", - "execution_count": 100, - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "outputs": [ - { - "data": { - "text/markdown": [ - "Execution time: 0.004239836 seconds" - ], - "text/plain": [ - "Execution time: 0.004239836 seconds" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $R = \\{1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200\\}$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tR = {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200}" - ] - }, - "execution_count": 100, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":time R= (1..200) \\ {50}" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Another example, for minimum of set from SETS'18 paper:" - ] - }, - { - "cell_type": "code", - "execution_count": 101, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "Execution time: 0.014517786 seconds" - ], - "text/plain": [ - "Execution time: 0.014517786 seconds" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $S = \\{2,4,5,6,8,10\\}$\n", - "* $y = 2$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tS = {2,4,5,6,8,10}\n", - "\ty = 2" - ] - }, - "execution_count": 101, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":time :solve prob S = {8,4,6,2,10,5} & y:S & S = {x|x:S & y<=x}" - ] - }, - { - "cell_type": "code", - "execution_count": 102, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $S = \\{2,4,5,6,8,10\\}$\n", - "* $y = 2$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tS = {2,4,5,6,8,10}\n", - "\ty = 2" - ] - }, - "execution_count": 102, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "S= {8,4,6,2,10,5} & y:S & !x.(x:S => y<=x)" - ] - }, { "cell_type": "markdown", "metadata": {