From 2893c6d96c82ac2fb5fa152324ee46ea9c34f710 Mon Sep 17 00:00:00 2001 From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de> Date: Wed, 6 Jun 2018 14:35:28 +0100 Subject: [PATCH] update notebooks --- .../SMT_Translation_Experiments.ipynb | 73 + notebooks/presentations/SETS_RODIN18.ipynb | 2370 ++++------------- notebooks/tutorials/prob_solver_intro.ipynb | 40 + 3 files changed, 678 insertions(+), 1805 deletions(-) diff --git a/notebooks/experiments/SMT_Translation_Experiments.ipynb b/notebooks/experiments/SMT_Translation_Experiments.ipynb index 40c0aa6..b200fa7 100644 --- a/notebooks/experiments/SMT_Translation_Experiments.ipynb +++ b/notebooks/experiments/SMT_Translation_Experiments.ipynb @@ -27,6 +27,24 @@ ":solve z3 f = {1|->3, 2|->6} & r = f~[{6}]" ] }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "outputs": [ + { + "ename": "CommandExecutionException", + "evalue": ":solve: Computation not completed: no solution found (but one might exist)", + "output_type": "error", + "traceback": [ + "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m" + ] + } + ], + "source": [ + ":solve z3 f = {1|->3, 2|->6} & r = f~[{6}] & not(r={2})" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -172,6 +190,61 @@ "```" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "This is not using the set datatype but functions to bool." + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "metadata": {}, + "outputs": [ + { + "ename": "CommandExecutionException", + "evalue": ":solve: Computation not completed: no solution found (but one might exist)", + "output_type": "error", + "traceback": [ + "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m" + ] + } + ], + "source": [ + ":solve z3 f:(INTEGER*INTEGER)-->BOOL & \n", + "f = ((INTEGER*INTEGER)*{FALSE}) <+ {(1,3,TRUE),(2,6,TRUE)} &\n", + "r:INTEGER-->BOOL & !x1.(x1:INTEGER => (x1|->TRUE:r <=> (x|->6)|->TRUE:f))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "What we get in probcli REPL:\n", + "unsupported_type_or_expression(comprehension_set([b(identifier(_smt_tmp30),couple(integer,integer),[]),b(identifier(_smt_tmp31),boolean,[])],b(conjunct(b(member(b(couple(b(identifier(_smt_tmp30),couple(integer,integer),[]),b(identifier(_smt_tmp31),boolean,[])),couple(couple(integer,integer),boolean),[]),b(comprehension_set([b(identifier(_smt_tmp33),couple(integer,integer),[]),b(identifier(_smt_tmp32),boolean,[])],b(conjunct(b(exists([b(identifier(_smt_tmp36)" + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [ + { + "ename": "CommandExecutionException", + "evalue": ":solve: Computation not completed: no solution found (but one might exist)", + "output_type": "error", + "traceback": [ + "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m" + ] + } + ], + "source": [ + ":solve z3 f:(INTEGER*INTEGER)-->BOOL & \n", + "f = ((INTEGER*INTEGER)*{FALSE}) <+ {(1,3,TRUE),(2,6,TRUE)} &\n", + "r:INTEGER-->BOOL & !x1.(x1:INTEGER => (x1|->TRUE:r <=> (x|->6)|->TRUE:f)) & not(2|->TRUE:r)" + ] + }, { "cell_type": "code", "execution_count": null, diff --git a/notebooks/presentations/SETS_RODIN18.ipynb b/notebooks/presentations/SETS_RODIN18.ipynb index dba64d2..f9479ae 100644 --- a/notebooks/presentations/SETS_RODIN18.ipynb +++ b/notebooks/presentations/SETS_RODIN18.ipynb @@ -9,6 +9,8 @@ }, "source": [ "# Solving (Set) Constraints in B and Event-B #\n", + "Michael Leuschel,\n", + "David Geleßus (Jupyter Interface)\n", "\n", "## A quick Introduction to B ##" ] @@ -37,7 +39,7 @@ }, { "cell_type": "code", - "execution_count": 1, + "execution_count": 3, "metadata": { "slideshow": { "slide_type": "subslide" @@ -50,7 +52,7 @@ "{FALSE,TRUE}" ] }, - "execution_count": 1, + "execution_count": 3, "metadata": {}, "output_type": "execute_result" } @@ -61,7 +63,7 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 4, "metadata": { "slideshow": { "slide_type": "fragment" @@ -74,7 +76,7 @@ "\"this is a string\"" ] }, - "execution_count": 2, + "execution_count": 4, "metadata": {}, "output_type": "execute_result" } @@ -85,7 +87,7 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 5, "metadata": { "slideshow": { "slide_type": "fragment" @@ -98,7 +100,7 @@ "1024" ] }, - "execution_count": 3, + "execution_count": 5, "metadata": {}, "output_type": "execute_result" } @@ -121,7 +123,7 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 74, "metadata": { "slideshow": { "slide_type": "-" @@ -132,11 +134,11 @@ "name": "stdout", "output_type": "stream", "text": [ - "[2018-06-04 17:10:21,614, T+7877565] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n", - "[2018-06-04 17:10:22,773, T+7878724] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57165\n", - "[2018-06-04 17:10:22,774, T+7878725] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 52908\n", - "[2018-06-04 17:10:22,782, T+7878733] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-06-04 17:10:22,792, T+7878743] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n" + "[2018-06-05 11:26:25,674, T+11556688] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n", + "[2018-06-05 11:26:26,811, T+11557825] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54552\n", + "[2018-06-05 11:26:26,812, T+11557826] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 61500\n", + "[2018-06-05 11:26:26,814, T+11557828] \"ProB Output Logger for instance 78644ca9\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", + "[2018-06-05 11:26:26,833, T+11557847] \"ProB Output Logger for instance 78644ca9\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n" ] }, { @@ -145,7 +147,7 @@ "Loaded machine: MyBasicSets : []\n" ] }, - "execution_count": 14, + "execution_count": 74, "metadata": {}, "output_type": "execute_result" } @@ -159,7 +161,7 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 7, "metadata": {}, "outputs": [ { @@ -168,7 +170,7 @@ "{thomas,gordon}" ] }, - "execution_count": 5, + "execution_count": 7, "metadata": {}, "output_type": "execute_result" } @@ -190,7 +192,7 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 8, "metadata": { "slideshow": { "slide_type": "-" @@ -203,7 +205,7 @@ "{Points1,Points2}" ] }, - "execution_count": 6, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } @@ -226,7 +228,7 @@ }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 9, "metadata": { "slideshow": { "slide_type": "fragment" @@ -239,7 +241,7 @@ "(thomas↦10)" ] }, - "execution_count": 7, + "execution_count": 9, "metadata": {}, "output_type": "execute_result" } @@ -250,7 +252,7 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 10, "metadata": { "slideshow": { "slide_type": "fragment" @@ -263,7 +265,7 @@ "(thomas↦10)" ] }, - "execution_count": 8, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } @@ -285,7 +287,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 11, "metadata": {}, "outputs": [ { @@ -294,7 +296,7 @@ "((thomas↦gordon)↦20)" ] }, - "execution_count": 9, + "execution_count": 11, "metadata": {}, "output_type": "execute_result" } @@ -312,20 +314,9 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "rec(length∈20,position∈10302,train∈thomas)" - ] - }, - "execution_count": 15, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "rec(train:thomas,length:20,position:10302)" ] @@ -345,7 +336,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 12, "metadata": { "slideshow": { "slide_type": "fragment" @@ -358,7 +349,7 @@ "{1,2,3}" ] }, - "execution_count": 10, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } @@ -380,7 +371,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 13, "metadata": { "slideshow": { "slide_type": "fragment" @@ -393,7 +384,7 @@ "{1,2,3}" ] }, - "execution_count": 11, + "execution_count": 13, "metadata": {}, "output_type": "execute_result" } @@ -411,20 +402,9 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "(((({FALSE,TRUE}↦INTEGER)↦STRING)↦{thomas,gordon})↦{Points1,Points2})" - ] - }, - "execution_count": 12, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "(BOOL,INTEGER,STRING,Trains,Points)" ] @@ -442,7 +422,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 14, "metadata": { "slideshow": { "slide_type": "fragment" @@ -455,7 +435,7 @@ "{1,2,3}" ] }, - "execution_count": 13, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -484,7 +464,7 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 15, "metadata": { "slideshow": { "slide_type": "fragment" @@ -497,7 +477,7 @@ "{{0,1},{1,2,3}}" ] }, - "execution_count": 14, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } @@ -555,20 +535,9 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "{(thomas↦thomas),(thomas↦gordon),(gordon↦thomas),(gordon↦gordon)}" - ] - }, - "execution_count": 17, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "Trains * Trains" ] @@ -586,7 +555,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 17, "metadata": {}, "outputs": [ { @@ -595,7 +564,7 @@ "{(thomas↦1),(gordon↦2)}" ] }, - "execution_count": 18, + "execution_count": 17, "metadata": {}, "output_type": "execute_result" } @@ -630,7 +599,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 18, "metadata": { "slideshow": { "slide_type": "fragment" @@ -643,7 +612,7 @@ "10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376" ] }, - "execution_count": 19, + "execution_count": 18, "metadata": {}, "output_type": "execute_result" } @@ -666,7 +635,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 19, "metadata": {}, "outputs": [ { @@ -675,7 +644,7 @@ "{1,7,8,9,10}" ] }, - "execution_count": 20, + "execution_count": 19, "metadata": {}, "output_type": "execute_result" } @@ -686,7 +655,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 20, "metadata": { "slideshow": { "slide_type": "fragment" @@ -699,7 +668,7 @@ "{1,7,8,9,10}" ] }, - "execution_count": 21, + "execution_count": 20, "metadata": {}, "output_type": "execute_result" } @@ -727,7 +696,7 @@ { "data": { "text/plain": [ - "{1,2}" + "{thomas,gordon}" ] }, "execution_count": 22, @@ -736,7 +705,7 @@ } ], "source": [ - "ran({(thomas↦1),(gordon↦2)})" + "dom({(thomas↦1),(gordon↦2)})" ] }, { @@ -752,15 +721,26 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 77, "metadata": { "slideshow": { "slide_type": "fragment" } }, - "outputs": [], + "outputs": [ + { + "ename": "CommandExecutionException", + "evalue": ":eval: NOT-WELL-DEFINED: \nFunction applied outside of domain (#8): Function argument: thomas, function value: {}\n ### Line: 1, Column: 0 until 21\n\n", + "output_type": "error", + "traceback": [ + "\u001b[1m\u001b[31m:eval: NOT-WELL-DEFINED: \u001b[0m", + "\u001b[1m\u001b[31mFunction applied outside of domain (#8): Function argument: thomas, function value: {}\u001b[0m", + "\u001b[1m\u001b[31m ### Line: 1, Column: 0 until 21\u001b[0m" + ] + } + ], "source": [ - "{(thomas↦1),(gordon↦2)} (thomas)" + "{(gordon↦2)} (thomas)" ] }, { @@ -776,13 +756,24 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 24, "metadata": { "slideshow": { "slide_type": "fragment" } }, - "outputs": [], + "outputs": [ + { + "data": { + "text/plain": [ + "{gordon}" + ] + }, + "execution_count": 24, + "metadata": {}, + "output_type": "execute_result" + } + ], "source": [ "{(thomas↦1),(gordon↦2)}~[2..3]" ] @@ -801,7 +792,7 @@ }, { "cell_type": "code", - "execution_count": 23, + "execution_count": 26, "metadata": { "slideshow": { "slide_type": "fragment" @@ -814,7 +805,7 @@ "FALSE" ] }, - "execution_count": 23, + "execution_count": 26, "metadata": {}, "output_type": "execute_result" } @@ -825,7 +816,7 @@ }, { "cell_type": "code", - "execution_count": 24, + "execution_count": 27, "metadata": { "slideshow": { "slide_type": "fragment" @@ -838,7 +829,7 @@ "TRUE" ] }, - "execution_count": 24, + "execution_count": 27, "metadata": {}, "output_type": "execute_result" } @@ -861,7 +852,7 @@ }, { "cell_type": "code", - "execution_count": 25, + "execution_count": 28, "metadata": { "slideshow": { "slide_type": "fragment" @@ -877,7 +868,7 @@ "\tx = −10" ] }, - "execution_count": 25, + "execution_count": 28, "metadata": {}, "output_type": "execute_result" } @@ -900,7 +891,7 @@ }, { "cell_type": "code", - "execution_count": 26, + "execution_count": 29, "metadata": { "slideshow": { "slide_type": "fragment" @@ -913,7 +904,7 @@ "{−10,10}" ] }, - "execution_count": 26, + "execution_count": 29, "metadata": {}, "output_type": "execute_result" } @@ -954,7 +945,7 @@ }, { "cell_type": "code", - "execution_count": 27, + "execution_count": 32, "metadata": { "slideshow": { "slide_type": "fragment" @@ -963,17 +954,20 @@ "outputs": [ { "data": { + "text/latex": [ + "$\\exists \\mathit{x}\\cdot (\\mathit{x} \\in \\mathbb N \\wedge \\mathit{x} * \\mathit{x} = 1000)$" + ], "text/plain": [ - "FALSE" + "∃x·(x ∈ ℕ ∧ x * x = 1000)" ] }, - "execution_count": 27, + "execution_count": 32, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "x*x=1000" + ":prettyprint #x.(x:NATURAL & x*x=1000)" ] }, { @@ -1018,7 +1012,7 @@ }, { "cell_type": "code", - "execution_count": 28, + "execution_count": 33, "metadata": {}, "outputs": [ { @@ -1033,7 +1027,7 @@ "\tt2 = gordon" ] }, - "execution_count": 28, + "execution_count": 33, "metadata": {}, "output_type": "execute_result" } @@ -1046,20 +1040,9 @@ }, { "cell_type": "code", - "execution_count": 29, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 29, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "train_position = {thomas|->2019, gordon|->2020} &\n", "t1:dom(train_position) & t2:dom(train_position) & train_position(t1) < train_position(t2) &\n", @@ -1080,7 +1063,7 @@ }, { "cell_type": "code", - "execution_count": 30, + "execution_count": 34, "metadata": {}, "outputs": [ { @@ -1095,7 +1078,7 @@ "\tt2 = gordon" ] }, - "execution_count": 30, + "execution_count": 34, "metadata": {}, "output_type": "execute_result" } @@ -1106,6 +1089,36 @@ "x:1..(train_position(t2)-train_position(t1)-1)" ] }, + { + "cell_type": "code", + "execution_count": 35, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "|Nr|x|y|\n", + "|---|---|---|\n", + "|1|TRUE|1|\n", + "|2|TRUE|2|\n", + "|3|TRUE|3|\n" + ], + "text/plain": [ + "Nr\tx\ty\n", + "1\tTRUE\t1\n", + "2\tTRUE\t2\n", + "3\tTRUE\t3\n" + ] + }, + "execution_count": 35, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":table {x,y|x=TRUE & y:1..3}" + ] + }, { "cell_type": "markdown", "metadata": { @@ -1125,7 +1138,7 @@ }, { "cell_type": "code", - "execution_count": 31, + "execution_count": 36, "metadata": {}, "outputs": [ { @@ -1134,13 +1147,15 @@ "FALSE" ] }, - "execution_count": 31, + "execution_count": 36, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "train_position:Trains-->1..10000 & train_position(t1) < train_position(t2) & not( t1 /= t2 )" + "train_position:Trains-->1..10000 &\n", + "train_position(t1) < train_position(t2) & \n", + "not( t1 /= t2 )" ] }, { @@ -1167,7 +1182,7 @@ }, { "cell_type": "code", - "execution_count": 32, + "execution_count": 37, "metadata": { "slideshow": { "slide_type": "skip" @@ -1183,7 +1198,7 @@ "{S,E,N,D,M,O,R,Y} ⊆ 0 ‥ 9 ∧ S > 0 ∧ M > 0 ∧ card({S,E,N,D,M,O,R,Y}) = 8 ∧ S * 1000 + E * 100 + N * 10 + D + M * 1000 + O * 100 + R * 10 + E = M * 10000 + O * 1000 + N * 100 + E * 10 + Y" ] }, - "execution_count": 32, + "execution_count": 37, "metadata": {}, "output_type": "execute_result" } @@ -1195,7 +1210,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 38, "metadata": {}, "outputs": [ { @@ -1214,7 +1229,7 @@ "\tO = 0" ] }, - "execution_count": 16, + "execution_count": 38, "metadata": {}, "output_type": "execute_result" } @@ -1240,7 +1255,7 @@ }, { "cell_type": "code", - "execution_count": 34, + "execution_count": 39, "metadata": {}, "outputs": [ { @@ -1249,7 +1264,7 @@ "{(((((((9↦5)↦6)↦7)↦1)↦0)↦8)↦2)}" ] }, - "execution_count": 34, + "execution_count": 39, "metadata": {}, "output_type": "execute_result" } @@ -1265,7 +1280,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 40, "metadata": {}, "outputs": [ { @@ -1280,7 +1295,7 @@ "1\t9\t5\t6\t7\t1\t0\t8\t2\n" ] }, - "execution_count": 15, + "execution_count": 40, "metadata": {}, "output_type": "execute_result" } @@ -1308,29 +1323,9 @@ }, { "cell_type": "code", - "execution_count": 35, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tP = 4\n", - "\tA = 1\n", - "\tS = 3\n", - "\tI = 0\n", - "\tK = 2\n", - "\tN = 9\n", - "\tO = 8" - ] - }, - "execution_count": 35, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ " {K,P} <: 1..9 &\n", " {I,S,A,O,N} <: 0..9 &\n", @@ -1352,7 +1347,7 @@ }, { "cell_type": "code", - "execution_count": 36, + "execution_count": 41, "metadata": {}, "outputs": [ { @@ -1364,7 +1359,7 @@ "\tx = {2,3,4,5}" ] }, - "execution_count": 36, + "execution_count": 41, "metadata": {}, "output_type": "execute_result" } @@ -1426,7 +1421,7 @@ }, { "cell_type": "code", - "execution_count": 37, + "execution_count": 42, "metadata": { "slideshow": { "slide_type": "fragment" @@ -1444,7 +1439,7 @@ "\tC = FALSE" ] }, - "execution_count": 37, + "execution_count": 42, "metadata": {}, "output_type": "execute_result" } @@ -1483,7 +1478,7 @@ }, { "cell_type": "code", - "execution_count": 39, + "execution_count": 43, "metadata": {}, "outputs": [ { @@ -1492,7 +1487,7 @@ "{(0↦2),(1↦1),(2↦0)}" ] }, - "execution_count": 39, + "execution_count": 43, "metadata": {}, "output_type": "execute_result" } @@ -1533,7 +1528,7 @@ }, { "cell_type": "code", - "execution_count": 40, + "execution_count": 44, "metadata": {}, "outputs": [ { @@ -1551,7 +1546,7 @@ "\tCARRY0 = TRUE" ] }, - "execution_count": 40, + "execution_count": 44, "metadata": {}, "output_type": "execute_result" } @@ -1566,7 +1561,7 @@ }, { "cell_type": "code", - "execution_count": 41, + "execution_count": 46, "metadata": { "slideshow": { "slide_type": "subslide" @@ -1576,20 +1571,20 @@ { "data": { "text/plain": [ - "{((((((FALSE↦FALSE)↦FALSE)↦TRUE)↦FALSE)↦TRUE)↦FALSE),((((((FALSE↦TRUE)↦FALSE)↦FALSE)↦FALSE)↦TRUE)↦FALSE),((((((TRUE↦FALSE)↦TRUE)↦FALSE)↦FALSE)↦TRUE)↦TRUE),((((((TRUE↦TRUE)↦TRUE)↦TRUE)↦FALSE)↦TRUE)↦TRUE)}" + "4" ] }, - "execution_count": 41, + "execution_count": 46, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{X0,X1,Y0,Y1,Z0,Z1,CARRY0 | ((X0=TRUE <=> Y0=TRUE) <=> Z0=FALSE) & \n", + "card({X0,X1,Y0,Y1,Z0,Z1,CARRY0 | ((X0=TRUE <=> Y0=TRUE) <=> Z0=FALSE) & \n", " ((X0=TRUE & Y0=TRUE) <=> CARRY0=TRUE) & \n", " (CARRY0=FALSE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=FALSE)) & \n", " (CARRY0=TRUE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=TRUE)) &\n", - " Z0=FALSE & Z1=TRUE}" + " Z0=FALSE & Z1=TRUE})" ] }, { @@ -1602,7 +1597,7 @@ }, { "cell_type": "code", - "execution_count": 42, + "execution_count": 91, "metadata": { "slideshow": { "slide_type": "fragment" @@ -1611,23 +1606,33 @@ "outputs": [ { "data": { + "text/markdown": [ + "|Nr|X0|X1|Y0|Y1|Z0|Z1|CARRY0|\n", + "|---|---|---|---|---|---|---|---|\n", + "|1|FALSE|FALSE|FALSE|TRUE|FALSE|TRUE|FALSE|\n", + "|2|FALSE|TRUE|FALSE|FALSE|FALSE|TRUE|FALSE|\n", + "|3|TRUE|FALSE|TRUE|FALSE|FALSE|TRUE|TRUE|\n" + ], "text/plain": [ - "{((((((FALSE↦FALSE)↦FALSE)↦TRUE)↦FALSE)↦TRUE)↦FALSE),((((((FALSE↦TRUE)↦FALSE)↦FALSE)↦FALSE)↦TRUE)↦FALSE),((((((TRUE↦FALSE)↦TRUE)↦FALSE)↦FALSE)↦TRUE)↦TRUE)}" + "Nr\tX0\tX1\tY0\tY1\tZ0\tZ1\tCARRY0\n", + "1\tFALSE\tFALSE\tFALSE\tTRUE\tFALSE\tTRUE\tFALSE\n", + "2\tFALSE\tTRUE\tFALSE\tFALSE\tFALSE\tTRUE\tFALSE\n", + "3\tTRUE\tFALSE\tTRUE\tFALSE\tFALSE\tTRUE\tTRUE\n" ] }, - "execution_count": 42, + "execution_count": 91, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{X0,X1,Y0,Y1,Z0,Z1,CARRY0 | ((X0=TRUE <=> Y0=TRUE) <=> Z0=FALSE) & \n", + ":table ({X0,X1,Y0,Y1,Z0,Z1,CARRY0 | ((X0=TRUE <=> Y0=TRUE) <=> Z0=FALSE) & \n", " ((X0=TRUE & Y0=TRUE) <=> CARRY0=TRUE) & \n", " (CARRY0=FALSE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=FALSE)) & \n", " (CARRY0=TRUE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=TRUE)) &\n", " (CARRY0=TRUE => (X1=FALSE & Y1=FALSE)) & // no overflow\n", " (CARRY0=FALSE => (X1=FALSE or Y1=FALSE)) & // no overflow\n", - " Z0=FALSE & Z1=TRUE}" + " Z0=FALSE & Z1=TRUE})" ] }, { @@ -1651,7 +1656,7 @@ }, { "cell_type": "code", - "execution_count": 43, + "execution_count": 49, "metadata": { "slideshow": { "slide_type": "subslide" @@ -1662,9 +1667,9 @@ "name": "stdout", "output_type": "stream", "text": [ - "[2018-06-04 14:01:28,941, T+458790] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: x : 0 .. 2 & y : 0 .. 2 & x + y = 2 ints: irange(0,4), intatoms: none\u001b[0m\n", - "[2018-06-04 14:01:28,941, T+458790] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n", - "[2018-06-04 14:01:28,942, T+458791] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2,5,2]\u001b[0m\n" + "[2018-06-05 10:10:18,465, T+6989479] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0mkodkod ok: x : 0 .. 2 & y : 0 .. 2 & x + y = 2 ints: irange(0,4), intatoms: none\u001b[0m\n", + "[2018-06-05 10:10:18,465, T+6989479] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n", + "[2018-06-05 10:10:18,466, T+6989480] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1,2,0]\u001b[0m\n" ] }, { @@ -1677,7 +1682,7 @@ "\ty = 0" ] }, - "execution_count": 43, + "execution_count": 49, "metadata": {}, "output_type": "execute_result" } @@ -1695,7 +1700,7 @@ }, { "cell_type": "code", - "execution_count": 44, + "execution_count": 50, "metadata": { "slideshow": { "slide_type": "fragment" @@ -1706,8 +1711,8 @@ "name": "stdout", "output_type": "stream", "text": [ - "[2018-06-04 14:01:31,052, T+460901] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: {x,y|x : 0 .. 2 & y : 0 .. 2 & x + y = 2} = res ints: irange(0,4), intatoms: irange(0,2)\u001b[0m\n", - "[2018-06-04 14:01:31,054, T+460903] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1]\u001b[0m\n" + "[2018-06-05 10:10:35,717, T+7006731] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: {x,y|x : 0 .. 2 & y : 0 .. 2 & x + y = 2} = res ints: irange(0,4), intatoms: irange(0,2)\u001b[0m\n", + "[2018-06-05 10:10:35,718, T+7006732] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1]\u001b[0m\n" ] }, { @@ -1719,7 +1724,7 @@ "\tres = {(0↦2),(1↦1),(2↦0)}" ] }, - "execution_count": 44, + "execution_count": 50, "metadata": {}, "output_type": "execute_result" } @@ -1770,7 +1775,7 @@ }, { "cell_type": "code", - "execution_count": 45, + "execution_count": 51, "metadata": {}, "outputs": [ { @@ -1783,7 +1788,7 @@ "\ty = 2" ] }, - "execution_count": 45, + "execution_count": 51, "metadata": {}, "output_type": "execute_result" } @@ -1832,16 +1837,16 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 52, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "Execution time: 0.050491290 seconds" + "Execution time: 0.009508264 seconds" ], "text/plain": [ - "Execution time: 0.050491290 seconds" + "Execution time: 0.009508264 seconds" ] }, "metadata": {}, @@ -1862,18 +1867,20 @@ "\tO = 8" ] }, - "execution_count": 17, + "execution_count": 52, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":time :solve prob {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7" + ":time :solve prob {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & \n", + "(1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = \n", + "1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7" ] }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 53, "metadata": { "slideshow": { "slide_type": "subslide" @@ -1895,25 +1902,24 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 54, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "[2018-06-04 21:43:31,067, T+24267018] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: K : 1 .. 9 & P : 1 .. 9 & I : 0 .. 9 & S : 0 .. 9 ... ints: irange(0,99980001), intatoms: irange(0,9)\u001b[0m\n", - "[2018-06-04 21:43:31,069, T+24267020] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n", - "[2018-06-04 21:43:31,069, T+24267020] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [636]\u001b[0m\n" + "[2018-06-05 10:18:05,165, T+7456179] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: K : 1 .. 9 & P : 1 .. 9 & I : 0 .. 9 & S : 0 .. 9 ... ints: irange(0,99980001), intatoms: irange(0,9)\u001b[0m\n", + "[2018-06-05 10:18:05,165, T+7456179] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [395]\u001b[0m\n" ] }, { "data": { "text/markdown": [ - "Execution time: 2.287290784 seconds" + "Execution time: 0.918848527 seconds" ], "text/plain": [ - "Execution time: 2.287290784 seconds" + "Execution time: 0.918848527 seconds" ] }, "metadata": {}, @@ -1934,7 +1940,7 @@ "\tO = 8" ] }, - "execution_count": 19, + "execution_count": 54, "metadata": {}, "output_type": "execute_result" } @@ -1982,7 +1988,7 @@ }, { "cell_type": "code", - "execution_count": 49, + "execution_count": 55, "metadata": { "slideshow": { "slide_type": "fragment" @@ -1998,7 +2004,7 @@ "\tx = −10" ] }, - "execution_count": 49, + "execution_count": 55, "metadata": {}, "output_type": "execute_result" } @@ -2020,14 +2026,14 @@ }, { "cell_type": "code", - "execution_count": 50, + "execution_count": 56, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "[2018-06-04 14:01:46,410, T+476259] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating x : INTEGER : 6001:sup ---> 6001:6001\u001b[0m\n" + "[2018-06-05 10:19:13,740, T+7524754] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating x : INTEGER : 6001:sup ---> 6001:6001\u001b[0m\n" ] }, { @@ -2039,7 +2045,7 @@ "\tx = 6001" ] }, - "execution_count": 50, + "execution_count": 56, "metadata": {}, "output_type": "execute_result" } @@ -2050,7 +2056,7 @@ }, { "cell_type": "code", - "execution_count": 51, + "execution_count": 57, "metadata": {}, "outputs": [ { @@ -2062,7 +2068,7 @@ "\tx = 6001" ] }, - "execution_count": 51, + "execution_count": 57, "metadata": {}, "output_type": "execute_result" } @@ -2084,14 +2090,14 @@ }, { "cell_type": "code", - "execution_count": 52, + "execution_count": 59, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "[2018-06-04 14:01:48,945, T+478794] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating x : INTEGER : 6001:sup ---> 6001:6001\u001b[0m\n" + "[2018-06-05 10:19:51,805, T+7562819] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating x : INTEGER : 6001:sup ---> 6001:6001\u001b[0m\n" ] }, { @@ -2109,7 +2115,7 @@ }, { "cell_type": "code", - "execution_count": 53, + "execution_count": 58, "metadata": {}, "outputs": [ { @@ -2121,7 +2127,7 @@ "\tx = 6756001" ] }, - "execution_count": 53, + "execution_count": 58, "metadata": {}, "output_type": "execute_result" } @@ -2144,47 +2150,18 @@ }, { "cell_type": "code", - "execution_count": 54, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 54, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":solve z3 x>y & y>x" ] }, { "cell_type": "code", - "execution_count": 55, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:01:54,055, T+483904] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Timeout when posting constraint:\u001b[0m\n", - "[2018-06-04 14:01:54,055, T+483904] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % kernel_objects:(_2222183#>0)\u001b[0m\n", - "[2018-06-04 14:01:54,056, T+483905] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating x : INTEGER : inf:sup ---> -1:3\u001b[0m\n" - ] - }, - { - "ename": "CommandExecutionException", - "evalue": ":solve: Computation not completed: no solution found (but one might exist)", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":solve prob x>y &y>x" ] @@ -2223,24 +2200,9 @@ }, { "cell_type": "code", - "execution_count": 56, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = thomas\n", - "\ty = gordon" - ] - }, - "execution_count": 56, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "x:Trains & y:Trains & x/=y" ] @@ -2265,7 +2227,7 @@ }, { "cell_type": "code", - "execution_count": 57, + "execution_count": 2, "metadata": {}, "outputs": [ { @@ -2278,18 +2240,28 @@ "\ty = {1,2}" ] }, - "execution_count": 57, + "execution_count": 2, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "x <: 1..2 & y <: 1..2 & x \\/ y = 1..2 & 1:x & x <<: y" + "x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 & 1:x & x ⊂ y" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "| Element | x | y | x ∪ y |\n", + "| ------------- |-------------| -----| -----|\n", + "| 1 | x1 | y1 | x1 or y1\n", + "| 2 | x2 | y2 | x2 or y2 |" ] }, { "cell_type": "code", - "execution_count": 58, + "execution_count": 88, "metadata": {}, "outputs": [ { @@ -2304,7 +2276,7 @@ "\tx2 = FALSE" ] }, - "execution_count": 58, + "execution_count": 88, "metadata": {}, "output_type": "execute_result" } @@ -2316,6 +2288,35 @@ " (x1=TRUE => y1=TRUE) & (x2=TRUE => y2=TRUE) & (x1/=y1 or x2/=y2) // x <<: y" ] }, + { + "cell_type": "code", + "execution_count": 90, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "|Nr|x1|x2|y1|y2|\n", + "|---|---|---|---|---|\n", + "|1|TRUE|FALSE|TRUE|TRUE|\n" + ], + "text/plain": [ + "Nr\tx1\tx2\ty1\ty2\n", + "1\tTRUE\tFALSE\tTRUE\tTRUE\n" + ] + }, + "execution_count": 90, + "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 & // 1:x \n", + " (x1=TRUE => y1=TRUE) & (x2=TRUE => y2=TRUE) & (x1/=y1 or x2/=y2) }" + ] + }, { "cell_type": "markdown", "metadata": { @@ -2329,15 +2330,15 @@ }, { "cell_type": "code", - "execution_count": 59, + "execution_count": 61, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "[2018-06-04 14:02:32,427, T+522276] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: x <: 1 .. 2 & y <: 1 .. 2 & x \\/ y = 1 .. 2 & 1 : ... ints: irange(1,2), intatoms: irange(1,2)\u001b[0m\n", - "[2018-06-04 14:02:32,428, T+522277] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1]\u001b[0m\n" + "[2018-06-05 10:22:52,620, T+7743634] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: x <: 1 .. 2 & y <: 1 .. 2 & x \\/ y = 1 .. 2 & 1 : ... ints: irange(1,2), intatoms: irange(1,2)\u001b[0m\n", + "[2018-06-05 10:22:52,620, T+7743634] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1]\u001b[0m\n" ] }, { @@ -2350,7 +2351,7 @@ "\ty = {1,2}" ] }, - "execution_count": 59, + "execution_count": 61, "metadata": {}, "output_type": "execute_result" } @@ -2376,7 +2377,7 @@ }, { "cell_type": "code", - "execution_count": 60, + "execution_count": 62, "metadata": {}, "outputs": [ { @@ -2385,7 +2386,7 @@ "1267650600228229401496703205376" ] }, - "execution_count": 60, + "execution_count": 62, "metadata": {}, "output_type": "execute_result" } @@ -2403,23 +2404,9 @@ }, { "cell_type": "code", - "execution_count": 61, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = {{100},{1}}" - ] - }, - "execution_count": 61, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "x <: POW(1..100) & {100}:x & !y.(y:x => {card(y)}:x)" ] @@ -2437,23 +2424,9 @@ }, { "cell_type": "code", - "execution_count": 62, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = {{100},{50,100},{25,50,100},{12,25,50,100},{6,12,25,50,100},{3,6,12,25,50,100},{1,3,6,12,25,50,100},{0,1,3,6,12,25,50,100}}" - ] - }, - "execution_count": 62, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "{100}:x & !y.(y:x => (!z.(z:y => y \\/ {z / 2}:x)))" ] @@ -2472,24 +2445,24 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 63, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "[2018-06-04 21:54:17,800, T+24913751] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: r : 1 .. 5 <-> 1 .. 5 & (r ; r) = r & r /= {} & do... ints: irange(0,5), intatoms: irange(0,5)\u001b[0m\n", - "[2018-06-04 21:54:17,801, T+24913752] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2,2,1,1,3,2,1,2,1,1,5,1,1,2,1,2,1,2,1,1,1,1]\u001b[0m\n" + "[2018-06-05 10:23:40,430, T+7791444] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: r : 1 .. 5 <-> 1 .. 5 & (r ; r) = r & r /= {} & do... ints: irange(0,5), intatoms: irange(0,5)\u001b[0m\n", + "[2018-06-05 10:23:40,431, T+7791445] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2,2,2,2,4,4,7,2,2,4,6,2,1,4,1,3,2,1,2,3,1,1]\u001b[0m\n" ] }, { "data": { "text/markdown": [ - "Execution time: 0.153314218 seconds" + "Execution time: 0.103495089 seconds" ], "text/plain": [ - "Execution time: 0.153314218 seconds" + "Execution time: 0.103495089 seconds" ] }, "metadata": {}, @@ -2504,7 +2477,7 @@ "\tr = {(3↦5),(3↦4),(5↦5),(5↦4),(1↦4),(2↦4),(4↦4)}" ] }, - "execution_count": 20, + "execution_count": 63, "metadata": {}, "output_type": "execute_result" } @@ -2529,24 +2502,9 @@ }, { "cell_type": "code", - "execution_count": 63, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = ∅\n", - "\ty = {1,2}" - ] - }, - "execution_count": 63, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":solve z3 x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2" ] @@ -2560,28 +2518,13 @@ }, { "cell_type": "code", - "execution_count": 64, + "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = ∅\n", - "\ty = {1,2}" - ] - }, - "execution_count": 64, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "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", @@ -2638,25 +2581,9 @@ }, { "cell_type": "code", - "execution_count": 65, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:02:49,960, T+539809] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] z3exception in query: canceled\u001b[0m\n" - ] - }, - { - "ename": "CommandExecutionException", - "evalue": ":solve: Computation not completed: time out", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:solve: Computation not completed: time out\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":solve z3 x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 & 1∈x & x ⊂ y" ] @@ -2718,27 +2645,13 @@ }, { "cell_type": "code", - "execution_count": 67, + "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, - "outputs": [ - { - "data": { - "text/latex": [ - "$\\mathit{f} = \\{(1\\mapsto 3),(2\\mapsto 6)\\} \\wedge (\\exists /* LET */ (\\mathit{st13}).( (\\mathit{st13})=\\mathit{r} \\wedge \\forall \\mathit{st15}\\cdot (\\mathit{st15} \\in \\mathit{st13} \\mathbin\\Rightarrow \\exists \\mathit{st16}\\cdot (6 \\mapsto \\mathit{st15} \\in \\mathit{st16} \\wedge (\\forall (\\mathit{st17},\\mathit{st18})\\cdot (\\mathit{st17} \\mapsto \\mathit{st18} \\in \\mathit{st16} \\mathbin\\Rightarrow \\mathit{st18} \\mapsto \\mathit{st17} \\in \\mathit{f}) \\wedge \\forall (\\mathit{st17},\\mathit{st18})\\cdot (\\mathit{st18} \\mapsto \\mathit{st17} \\in \\mathit{f} \\mathbin\\Rightarrow \\mathit{st17} \\mapsto \\mathit{st18} \\in \\mathit{st16})))) \\wedge \\forall \\mathit{st15}\\cdot (\\exists \\mathit{st19}\\cdot (6 \\mapsto \\mathit{st15} \\in \\mathit{st19} \\wedge (\\forall (\\mathit{st20},\\mathit{st21})\\cdot (\\mathit{st20} \\mapsto \\mathit{st21} \\in \\mathit{st19} \\mathbin\\Rightarrow \\mathit{st21} \\mapsto \\mathit{st20} \\in \\mathit{f}) \\wedge \\forall (\\mathit{st20},\\mathit{st21})\\cdot (\\mathit{st21} \\mapsto \\mathit{st20} \\in \\mathit{f} \\mathbin\\Rightarrow \\mathit{st20} \\mapsto \\mathit{st21} \\in \\mathit{st19}))) \\mathbin\\Rightarrow \\mathit{st15} \\in \\mathit{st13})))$" - ], - "text/plain": [ - "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": 67, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":prettyprint f = {(1|->3),(2|->6)} &\n", "#st13.(r = st13 & (\n", @@ -2751,35 +2664,13 @@ }, { "cell_type": "code", - "execution_count": 68, + "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.038201131 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tr = {2}\n", - "\tf = {(1↦3),(2↦6)}" - ] - }, - "execution_count": 68, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve prob f = {(1|->3),(2|->6)} &\n", "#st13.(r = st13 & (\n", @@ -2792,18 +2683,9 @@ }, { "cell_type": "code", - "execution_count": 69, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":time: :solve: Computation not completed: no solution found (but one might exist)", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:time: :solve: Computation not completed: no solution found (but one might exist)\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":time :solve cvc4 f = {(1|->3),(2|->6)} &\n", "#st13.(r = st13 & (\n", @@ -2829,20 +2711,9 @@ }, { "cell_type": "code", - "execution_count": 70, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 70, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":solve prob x:s1 & x:s2 & x /: (s1 /\\ s2) & s1 <: INTEGER" ] @@ -2856,20 +2727,9 @@ }, { "cell_type": "code", - "execution_count": 71, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 71, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":solve z3 x:s1 & x/:s2 & x /: (s1 \\/s2) & s1 <: INTEGER" ] @@ -2902,24 +2762,13 @@ }, { "cell_type": "code", - "execution_count": 72, + "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, - "outputs": [ - { - "data": { - "text/plain": [ - "{0,100,200,300,400,500,600,700,800,900,1000}" - ] - }, - "execution_count": 72, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "{x|x∈0..2**10 & x mod 100 = 0}" ] @@ -2937,25 +2786,9 @@ }, { "cell_type": "code", - "execution_count": 73, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tmn = 0\n", - "\ts = {0,100,200,300,400,500,600,700,800,900,1000}\n", - "\tmx = 1000" - ] - }, - "execution_count": 73, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "s = {x|x∈0..2**10 & x mod 100 = 0} &\n", "mx = max(s) &\n", @@ -2977,20 +2810,9 @@ }, { "cell_type": "code", - "execution_count": 74, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "{x∣x > 1000}" - ] - }, - "execution_count": 74, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "{x|x>1000}" ] @@ -3004,24 +2826,9 @@ }, { "cell_type": "code", - "execution_count": 75, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tinf = {x∣x > 1000}\n", - "\tres = (1001 ‥ 1100)" - ] - }, - "execution_count": 75, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "inf = {x|x>1000} & 1024 : inf & not(1000:inf) & res = (900..1100) ∩ inf" ] @@ -3040,31 +2847,9 @@ }, { "cell_type": "code", - "execution_count": 76, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:03:14,350, T+564199] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] VIRTUAL TIME-OUT caused by: ### Warning: enumerating x : (all_solutions) : INTEGER : 1025:sup ---> 1025:1025\u001b[0m\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tinf = {x∣x > 1000 ∧ x mod 25 = 0}\n", - "\tres = ((900 ‥ 1100) ∩ {x∣x > 1000 ∧ x mod 25 = 0})" - ] - }, - "execution_count": 76, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "inf = {x|x>1000 & x mod 25 = 0} & 1025 ∈ inf & not(1000∈inf) & res = (900..1100) ∩ inf" ] @@ -3082,24 +2867,9 @@ }, { "cell_type": "code", - "execution_count": 77, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tinf = {x∣x > 1000 ∧ x mod 25 = 0}\n", - "\tres = ((900 ‥ 1100) ∩ {x∣x > 1000 ∧ x mod 25 = 0})" - ] - }, - "execution_count": 77, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "inf = /*@symbolic*/ {x|x>1000 & x mod 25 = 0} & 1025 ∈ inf & not(1000∈inf) & res = (900..1100) ∩ inf" ] @@ -3132,27 +2902,13 @@ }, { "cell_type": "code", - "execution_count": 78, + "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tvec = {(1↦1),(2↦2),(3↦4),(4↦8),(5↦16),(6↦32),(7↦64),(8↦128),(9↦256),(10↦512)}" - ] - }, - "execution_count": 78, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "vec: 1..10 --> 0..9999 &\n", "vec(1) : {1,10} &\n", @@ -3173,87 +2929,27 @@ }, { "cell_type": "code", - "execution_count": 79, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:03:20,699, T+570548] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0mkodkod ok: vec : 1 .. 8 --> 0 .. 199 & vec(1) : {1,10} & !x.(... ints: irange(0,398), intatoms: irange(0,199)\u001b[0m\n", - "[2018-06-04 14:03:20,699, T+570548] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [204]\u001b[0m\n", - "Execution time: 2.184422799 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tvec = {(3↦4),(5↦16),(6↦32),(7↦64),(1↦1),(2↦2),(4↦8),(8↦128)}" - ] - }, - "execution_count": 79, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve kodkod vec: 1..8 --> 0..199 & vec(1) : {1,10} & !x.(x:2..8 => vec(x) = vec(x-1)*2)" ] }, { "cell_type": "code", - "execution_count": 80, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.014949467 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tvec = {(1↦1),(2↦2),(3↦4),(4↦8),(5↦16),(6↦32),(7↦64),(8↦128)}" - ] - }, - "execution_count": 80, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve prob vec: 1..8 --> 0..199 & vec(1) : {1,10} & !x.(x:2..8 => vec(x) = vec(x-1)*2)" ] }, { "cell_type": "code", - "execution_count": 81, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:03:24,797, T+574646] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] z3exception in query: canceled\u001b[0m\n" - ] - }, - { - "ename": "CommandExecutionException", - "evalue": ":time: :solve: Computation not completed: time out", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:time: :solve: Computation not completed: time out\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":time :solve z3 vec: 1..8 --> 0..199 & vec(1) : {1,10} & !x.(x:2..8 => vec(x) = vec(x-1)*2)" ] @@ -3278,33 +2974,9 @@ }, { "cell_type": "code", - "execution_count": 89, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.305008223 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\ts3 = ∃500∈{20,40,…,9980,10000}\n", - "\tn = 4\n", - "\ts1 = ∃2500∈{4,8,…,9996,10000}\n", - "\ts2 = ∃2000∈{5,10,…,9995,10000}" - ] - }, - "execution_count": 89, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve prob s1 = {x|x:1..10**n & x mod n = 0} & s2 = {y|y:1..10**n & y mod (n+1) = 0} & s3 = s1 /\\ s2 & n=4" ] @@ -3322,90 +2994,31 @@ }, { "cell_type": "code", - "execution_count": 90, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.013053703 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\txy = ∃201∈{1,2,…,299,300}\n", - "\tx = (1 ‥ 100)\n", - "\ty = (200 ‥ 300)\n", - "\tn = 100" - ] - }, - "execution_count": 90, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve prob x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y" ] }, { "cell_type": "code", - "execution_count": 91, + "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":solve: Computation not completed: time out", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:solve: Computation not completed: time out\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":solve z3 x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y" ] }, { "cell_type": "code", - "execution_count": 92, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:05:05,176, T+675025] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: x = 1 .. n & y = 2 * n .. 3 * n & n = 100 & xy = x... ints: irange(1,300), intatoms: irange(1,300)\u001b[0m\n", - "[2018-06-04 14:05:05,176, T+675025] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2]\u001b[0m\n", - "Execution time: 0.336676466 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\txy = {3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,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,200,201,202,203,204,205,206,…}\n", - "\tx = {3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,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,1,2,4,8,16,32,64}\n", - "\ty = {200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,256}\n", - "\tn = 100" - ] - }, - "execution_count": 92, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve kodkod x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y" ] @@ -3476,28 +3089,9 @@ }, { "cell_type": "code", - "execution_count": 93, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tr2 = {1,4,9,16,25,36,49,64,81,100}\n", - "\tr3 = [4,9,25,49,121]\n", - "\tr4 = 256\n", - "\tsqrt = 10\n", - "\tf = λx·(x ∈ INTEGER∣x ∗ x)\n", - "\tr1 = 10000000000" - ] - }, - "execution_count": 93, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "f = %x.(x:INTEGER|x*x) &\n", "r1 = f(100000) &\n", @@ -3509,39 +3103,9 @@ }, { "cell_type": "code", - "execution_count": 94, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:08:39,826, T+889675] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[31m\u001b[1m! source(b_compute_comprehension_set)\u001b[0m\n", - "[2018-06-04 14:08:39,826, T+889675] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Keeping comprehension-set symbolic (you may want to use the /*@symbolic*/ pragma to prevent this message, unless it was due to a WD-Error), identifiers: [x,y]\u001b[0m\n", - "[2018-06-04 14:08:39,827, T+889676] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Line: 1 Column: 9 until 44\u001b[0m\n", - "[2018-06-04 14:08:39,837, T+889686] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0mVIRTUAL TIME-OUT caused by: ### Warning: enumerating NATURAL(1) : NATURAL(1) : 1:sup ---> 1:3\u001b[0m\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tr2 = {1,2,3,4}\n", - "\tr3 = [2,2,3,3,4]\n", - "\tr4 = 2\n", - "\tr5 = {2,4,10,100}\n", - "\tsqr = 9802\n", - "\tf = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}\n", - "\tr1 = 317" - ] - }, - "execution_count": 94, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "f = {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function\n", "r1 = f(100000) &\n", @@ -3570,24 +3134,9 @@ }, { "cell_type": "code", - "execution_count": 95, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = 125\n", - "\tReifVar = TRUE" - ] - }, - "execution_count": 95, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "(x>100 <=> (ReifVar=TRUE)) & (x<125 <=> (ReifVar=FALSE)) & x<200" ] @@ -3625,26 +3174,9 @@ }, { "cell_type": "code", - "execution_count": 96, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tR = {1,0}\n", - "\tS = {0}\n", - "\tT = {0}\n", - "\tX = 0" - ] - }, - "execution_count": 96, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "1:R & 1/:S & R/\\S=T & T={X}" ] @@ -3670,20 +3202,9 @@ }, { "cell_type": "code", - "execution_count": 97, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "{((4↦4)↦{4}),((5↦4)↦∅),((5↦5)↦{5})}" - ] - }, - "execution_count": 97, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "{X,Y,R|X: 1..5 & Y: 4..10 & {X}/\\{Y}=R & X>=Y}" ] @@ -3705,26 +3226,9 @@ }, { "cell_type": "code", - "execution_count": 98, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:08:47,442, T+897291] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating A : STRING : inf ---> \"STRING1\",\"STRING2\",...\u001b[0m\n", - "[2018-06-04 14:08:47,443, T+897292] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating B : STRING : inf ---> \"STRING1\",\"STRING2\",...\u001b[0m\n" - ] - }, - { - "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" - ] - } - ], + "outputs": [], "source": [ "A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(STRING)" ] @@ -3743,68 +3247,27 @@ }, { "cell_type": "code", - "execution_count": 99, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 99, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(BOOL)" ] }, { "cell_type": "code", - "execution_count": 100, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:08:48,854, T+898703] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: A \\/ B = D & A /\\ C = {} & D = C & A /= {} ints: none, intatoms: none\u001b[0m\n", - "[2018-06-04 14:08:48,854, T+898703] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: []\u001b[0m\n" - ] - }, - { - "data": { - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 100, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":solve kodkod A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(BOOL)" ] }, { "cell_type": "code", - "execution_count": 101, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 101, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":solve z3 A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(BOOL)" ] @@ -3830,19 +3293,40 @@ }, { "cell_type": "code", - "execution_count": 102, + "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, + "outputs": [], + "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": 86, + "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.005074849 seconds\n" - ] + "data": { + "text/markdown": [ + "Execution time: 0.005957963 seconds" + ], + "text/plain": [ + "Execution time: 0.005957963 seconds" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -3850,16 +3334,41 @@ "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}" + "\tS = {2,4,5,6,8,10}\n", + "\ty = 2" ] }, - "execution_count": 102, + "execution_count": 86, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":time R= (1..200) \\ {50}" + ":time :solve prob S = {8,4,6,2,10,5} & y:S & S = {x|x:S & y<=x}" + ] + }, + { + "cell_type": "code", + "execution_count": 80, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "TRUE\n", + "\n", + "Solution:\n", + "\tS = {2,4,5,6,8,10}\n", + "\ty = 2" + ] + }, + "execution_count": 80, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "S= {8,4,6,2,10,5} & y:S & !x.(x:S => y<=x)" ] }, { @@ -3936,138 +3445,45 @@ }, { "cell_type": "code", - "execution_count": 103, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":solve: Computation not completed: no solution found (but one might exist)", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":solve z3 x = 1..1000 /\\ (200..300)" ] }, { "cell_type": "code", - "execution_count": 104, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.175097068 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = {6,7,8,9,10,11,12,13,14,15}" - ] - }, - "execution_count": 104, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve z3 x = 1..40 /\\ (6..15)" ] }, { "cell_type": "code", - "execution_count": 105, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.754973438 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = {6,7,8,9,10,11,12,13,14,15}" - ] - }, - "execution_count": 105, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve z3 x = 1..60 /\\ (6..15)" ] }, { "cell_type": "code", - "execution_count": 106, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 2.369086566 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = {6,7,8,9,10,11,12,13,14,15}" - ] - }, - "execution_count": 106, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve z3 x = 1..80 /\\ (6..15)" ] }, { "cell_type": "code", - "execution_count": 107, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.004883079 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = (6 ‥ 15)" - ] - }, - "execution_count": 107, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve prob x = 1..80 /\\ (6..15)" ] @@ -4085,44 +3501,18 @@ }, { "cell_type": "code", - "execution_count": 108, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":solve: Computation not completed: no solution found (but one might exist)", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":solve z3 s1 = {2,3,5,7,11} & s2 = {4,8,16,32} & c = s1*s2 & r=c~[{8}]" ] }, { "cell_type": "code", - "execution_count": 109, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tr = {2,3,5,7,11}\n", - "\tc = ({2,3,5,7,11} ∗ {4,8,16,32})\n", - "\ts1 = {2,3,5,7,11}\n", - "\ts2 = {4,8,16,32}" - ] - }, - "execution_count": 109, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":solve prob s1 = {2,3,5,7,11} & s2 = {4,8,16,32} & c = s1*s2 & r=c~[{8}]" ] @@ -4141,89 +3531,27 @@ }, { "cell_type": "code", - "execution_count": 110, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.012805716 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tf = {(1↦1),(2↦2),(3↦3),(4↦4),(5↦5),(6↦6),(7↦7),(8↦8),(9↦9),(10↦10),(11↦11),(12↦12),(13↦13),(14↦14),(15↦15),(16↦16),(17↦17),(18↦18),(19↦19),(20↦20),(21↦21),(22↦22),(23↦23),(24↦24),(25↦25),(26↦26),(27↦27),(28↦28),(29↦29),(30↦30),(31↦31),(32↦32),(33↦33),(34↦34),(35↦35),(36↦36),(37↦37),(38↦38),(39↦39),(40↦40),(41↦41),(42↦42),(43↦43),(44↦44),(45↦45),(46↦46),(47↦47),(48↦48),(49↦49),(50↦50)}\n", - "\tn = 50" - ] - }, - "execution_count": 110, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve prob f: 1..n --> 1..n & !x.(x:2..n => f(x)=f(x-1)+1) & n=50" ] }, { "cell_type": "code", - "execution_count": 111, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:09:10,559, T+920408] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: f : 1 .. n --> 1 .. n & !x.(x : 2 .. n => f(x) = f... ints: irange(1,50), intatoms: irange(1,50)\u001b[0m\n", - "[2018-06-04 14:09:10,560, T+920409] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1185]\u001b[0m\n", - "Execution time: 3.657044854 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tf = {(3↦3),(5↦5),(6↦6),(7↦7),(9↦9),(10↦10),(11↦11),(12↦12),(13↦13),(14↦14),(15↦15),(17↦17),(18↦18),(19↦19),(20↦20),(21↦21),(22↦22),(23↦23),(24↦24),(25↦25),(26↦26),(27↦27),(28↦28),(29↦29),(30↦30),(31↦31),(33↦33),(34↦34),(35↦35),(36↦36),(37↦37),(38↦38),(39↦39),(40↦40),(41↦41),(42↦42),(43↦43),(44↦44),(45↦45),(46↦46),(47↦47),(48↦48),(49↦49),(50↦50),(1↦1),(2↦2),(4↦4),(8↦8),(16↦16),(32↦32)}\n", - "\tn = 50" - ] - }, - "execution_count": 111, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve kodkod f: 1..n --> 1..n & !x.(x:2..n => f(x)=f(x-1)+1) & n=50" ] }, { "cell_type": "code", - "execution_count": 112, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:09:13,146, T+922995] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] z3exception in query: canceled\u001b[0m\n" - ] - }, - { - "ename": "CommandExecutionException", - "evalue": ":time: :solve: Computation not completed: time out", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:time: :solve: Computation not completed: time out\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":time :solve z3 f: 1..n --> 1..n & !x.(x:2..n => f(x)=f(x-1)+1) & n=50" ] @@ -4243,110 +3571,36 @@ }, { "cell_type": "code", - "execution_count": 113, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 2.087463022 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tr = {(1↦1),(1↦2),(1↦3),(1↦4),(1↦5),(2↦3),(2↦4),(3↦3),(3↦4),(4↦3),(4↦4),(5↦1),(5↦2),(5↦3),(5↦4),(5↦5)}" - ] - }, - "execution_count": 113, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve prob r: 1..5 <-> 1..5 & (r;r) = r & r /= {} & dom(r)=1..5 & r[2..3]=3..4" ] }, { "cell_type": "code", - "execution_count": 114, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:09:15,382, T+925231] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: r : 1 .. 5 <-> 1 .. 5 & (r ; r) = r & r /= {} & do... ints: irange(0,5), intatoms: irange(0,5)\u001b[0m\n", - "[2018-06-04 14:09:15,383, T+925232] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1,1,1,0,1,0,1,0,1,1,0,1,0,1,1,0,1,0,1,0,1,1]\u001b[0m\n", - "Execution time: 0.037624591 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tr = {(3↦3),(3↦4),(5↦4),(1↦4),(2↦4),(4↦4)}" - ] - }, - "execution_count": 114, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve kodkod r: 1..5 <-> 1..5 & (r;r) = r & r /= {} & dom(r)=1..5 & r[2..3]=3..4" ] }, { "cell_type": "code", - "execution_count": 115, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":time: :solve: Computation not completed: no solution found (but one might exist)", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:time: :solve: Computation not completed: no solution found (but one might exist)\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":time :solve z3 r: 1..5 <-> 1..5 & (r;r) = r & r /= {} & dom(r)=1..5 & r[2..3]=3..4" ] }, { "cell_type": "code", - "execution_count": 116, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 1.971222669 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tr = {(1↦1),(1↦2),(1↦3),(1↦4),(1↦5),(2↦3),(2↦4),(3↦3),(3↦4),(4↦3),(4↦4),(5↦1),(5↦2),(5↦3),(5↦4),(5↦5)}" - ] - }, - "execution_count": 116, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve prob r: 1..5 <-> 1..5 & (r;r) = r & r /= {} & dom(r)=1..5 & r[2..3]=3..4" ] @@ -4366,31 +3620,9 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 16:46:59,166, T+6475117] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n", - "[2018-06-04 16:47:00,347, T+6476298] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 55595\n", - "[2018-06-04 16:47:00,348, T+6476299] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 52301\n", - "[2018-06-04 16:47:00,350, T+6476301] \"ProB Output Logger for instance ecdd0f\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-06-04 16:47:00,364, T+6476315] \"ProB Output Logger for instance ecdd0f\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n" - ] - }, - { - "data": { - "text/plain": [ - "Loaded machine: GraphTheorem : []\n" - ] - }, - "execution_count": 10, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "::load\n", "MACHINE GraphTheorem\n", @@ -4401,23 +3633,9 @@ }, { "cell_type": "code", - "execution_count": 118, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/latex": [ - "$\\mathit{edges} \\in \\mathit{NODES5} \\mathbin\\leftrightarrow \\mathit{NODES5} \\wedge \\mathit{edges}^{-1} = \\mathit{edges} \\wedge \\neg (\\exists (\\mathit{n1},\\mathit{n2})\\cdot (\\mathit{n1} \\in \\mathit{NODES5} \\wedge \\mathit{n2} \\in \\mathit{NODES5} \\wedge \\mathit{n2} \\neq \\mathit{n1} \\wedge \\mathit{card}(\\mathit{edges}[\\{\\mathit{n1}\\}]) = \\mathit{card}(\\mathit{edges}[\\{\\mathit{n2}\\}]))) \\wedge \\mathit{dom}(\\mathit{edges}) = \\mathit{NODES5} \\wedge id(\\mathit{NODES5}) \\cap \\mathit{edges} = \\emptyset $" - ], - "text/plain": [ - "edges ∈ NODES5 ↔ NODES5 ∧ edges⁻¹ = edges ∧ ¬(∃(n1,n2)·(n1 ∈ NODES5 ∧ n2 ∈ NODES5 ∧ n2 ≠ n1 ∧ card(edges[{n1}]) = card(edges[{n2}]))) ∧ dom(edges) = NODES5 ∧ id(NODES5) ∩ edges = ∅" - ] - }, - "execution_count": 118, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":prettyprint edges : NODES5 <-> NODES5 & \n", " edges~=edges &\n", @@ -4428,18 +3646,9 @@ }, { "cell_type": "code", - "execution_count": 119, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":time: :solve: Computation not completed: time out", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:time: :solve: Computation not completed: time out\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":time :solve prob edges : NODES5 <-> NODES5 & \n", " edges~=edges &\n", @@ -4450,34 +3659,13 @@ }, { "cell_type": "code", - "execution_count": 120, + "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:09:25,781, T+935630] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: edges~ = edges & not(#(n1,n2).(n2 /= n1 & card(edg... ints: irange(0,5), intatoms: none\u001b[0m\n", - "[2018-06-04 14:09:25,781, T+935630] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n", - "[2018-06-04 14:09:25,782, T+935631] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: []\u001b[0m\n", - "Execution time: 0.837816834 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 120, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve kodkod edges : NODES5 <-> NODES5 & \n", " edges~=edges &\n", @@ -4488,18 +3676,9 @@ }, { "cell_type": "code", - "execution_count": 121, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":time: :solve: Computation not completed: no solution found (but one might exist)", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:time: :solve: Computation not completed: no solution found (but one might exist)\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":time :solve z3 edges : NODES5 <-> NODES5 & \n", " edges~=edges &\n", @@ -4522,32 +3701,9 @@ }, { "cell_type": "code", - "execution_count": 122, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:09:26,058, T+935907] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: edges~ = edges & not(#(n1,n2).(n2 /= n1 & card(edg... ints: irange(0,5), intatoms: none\u001b[0m\n", - "[2018-06-04 14:09:26,059, T+935908] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [5,4,3,1,2,2,2,2,2,1,7,1,2,2,2,1,3,2,2,2,1,2]\u001b[0m\n", - "Execution time: 0.107056638 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tedges = {(NODES51↦NODES54),(NODES52↦NODES52),(NODES52↦NODES53),(NODES52↦NODES54),(NODES53↦NODES52),(NODES53↦NODES53),(NODES53↦NODES54),(NODES53↦NODES55),(NODES54↦NODES51),(NODES54↦NODES52),(NODES54↦NODES53),(NODES54↦NODES54),(NODES54↦NODES55),(NODES55↦NODES53),(NODES55↦NODES54)}" - ] - }, - "execution_count": 122, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve kodkod edges : NODES5 <-> NODES5 & \n", " edges~=edges &\n", @@ -4558,28 +3714,9 @@ }, { "cell_type": "code", - "execution_count": 123, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:09:26,173, T+936022] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: edges~ = edges & not(#(n1,n2).(n1 : dom(edges) & n... ints: irange(0,5), intatoms: none\u001b[0m\n", - "Execution time: 0.056822248 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 123, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve kodkod edges : NODES5 <-> NODES5 & \n", " edges~=edges &\n", @@ -4603,31 +3740,9 @@ }, { "cell_type": "code", - "execution_count": 124, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.053214873 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tqueens = {(1↦4),(2↦2),(3↦7),(4↦3),(5↦6),(6↦8),(7↦5),(8↦1)}\n", - "\tn = 8" - ] - }, - "execution_count": 124, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve prob n=8 &\n", " queens : 1..n >-> 1..n &\n", @@ -4636,31 +3751,9 @@ }, { "cell_type": "code", - "execution_count": 125, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.370806337 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tqueens = {(1↦4),(2↦7),(3↦5),(4↦2),(5↦6),(6↦1),(7↦3),(8↦8)}\n", - "\tn = 8" - ] - }, - "execution_count": 125, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve z3 n=8 &\n", " queens : 1..n >-> 1..n &\n", @@ -4669,33 +3762,9 @@ }, { "cell_type": "code", - "execution_count": 126, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:09:27,167, T+937016] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: n = 8 & queens : 1 .. n >-> 1 .. n & !(q1,q2).(q1 ... ints: irange(-7,15), intatoms: irange(1,8)\u001b[0m\n", - "[2018-06-04 14:09:27,168, T+937017] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [27,19,44,9,6,6,11,5,5,10,4,9,22,2,6,8,4,3,3,14,3,3]\u001b[0m\n", - "Execution time: 0.405027874 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tqueens = {(3↦2),(5↦5),(6↦1),(7↦8),(1↦3),(2↦6),(4↦7),(8↦4)}\n", - "\tn = 8" - ] - }, - "execution_count": 126, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve kodkod n=8 &\n", " queens : 1..n >-> 1..n &\n", @@ -4715,31 +3784,9 @@ }, { "cell_type": "code", - "execution_count": 127, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.054922769 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tbshp = {(1↦1),(1↦2),(1↦3)}\n", - "\tn = 3" - ] - }, - "execution_count": 127, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve prob n=3 & bshp <: (1..n)*(1..n) & \n", " !(i,j).({i,j}<:1..n => ( (i,j): bshp => (!k.(k:(i+1)..n => (k,j+k-i) /: bshp & (k,j-k+i) /: bshp )) )) &\n", @@ -4748,25 +3795,9 @@ }, { "cell_type": "code", - "execution_count": 128, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:09:29,856, T+939705] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] z3exception in query: canceled\u001b[0m\n" - ] - }, - { - "ename": "CommandExecutionException", - "evalue": ":time: :solve: Computation not completed: time out", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:time: :solve: Computation not completed: time out\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":time :solve z3 n=3 & bshp <: (1..n)*(1..n) & \n", " !(i,j).({i,j}<:1..n => ( (i,j): bshp => (!k.(k:(i+1)..n => (k,j+k-i) /: bshp & (k,j-k+i) /: bshp )) )) &\n", @@ -4782,23 +3813,9 @@ }, { "cell_type": "code", - "execution_count": 129, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/latex": [ - "$\\mathit{n} = 3 \\wedge \\mathit{bshp} \\subseteq (1 .. \\mathit{n}) \\times (1 .. \\mathit{n}) \\wedge \\forall (\\mathit{i},\\mathit{j})\\cdot (\\{\\mathit{i},\\mathit{j}\\} \\subseteq 1 .. \\mathit{n} \\mathbin\\Rightarrow (\\mathit{i} \\mapsto \\mathit{j} \\in \\mathit{bshp} \\mathbin\\Rightarrow \\forall \\mathit{k}\\cdot (\\mathit{k} \\in \\mathit{i} + 1 .. \\mathit{n} \\mathbin\\Rightarrow (\\mathit{k} \\mapsto (\\mathit{j} + \\mathit{k}) - \\mathit{i}) \\not\\in \\mathit{bshp} \\wedge (\\mathit{k} \\mapsto (\\mathit{j} - \\mathit{k}) + \\mathit{i}) \\not\\in \\mathit{bshp}))) \\wedge \\mathit{card}(\\mathit{bshp}) = 3$" - ], - "text/plain": [ - "n = 3 ∧ bshp ⊆ (1 ‥ n) × (1 ‥ n) ∧ ∀(i,j)·({i,j} ⊆ 1 ‥ n ⇒ (i ↦ j ∈ bshp ⇒ ∀k·(k ∈ i + 1 ‥ n ⇒ (k ↦ (j + k) - i) ∉ bshp ∧ (k ↦ (j - k) + i) ∉ bshp))) ∧ card(bshp) = 3" - ] - }, - "execution_count": 129, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":prettyprint n=3 & bshp <: (1..n)*(1..n) & \n", " !(i,j).({i,j}<:1..n => ( (i,j): bshp => (!k.(k:(i+1)..n => (k,j+k-i) /: bshp & (k,j-k+i) /: bshp )) )) &\n", @@ -4818,46 +3835,18 @@ }, { "cell_type": "code", - "execution_count": 130, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tr = {(1↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦3)}" - ] - }, - "execution_count": 130, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "!x.(x:1..2 => !y.(y:1..3 => (x,y):r)) " ] }, { "cell_type": "code", - "execution_count": 131, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tr = {z_∣z_ ∈ INTEGER ∗ INTEGER}" - ] - }, - "execution_count": 131, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":solve z3 !x.(x:1..2 => !y.(y:1..3 => (x,y):r)) " ] @@ -4871,80 +3860,27 @@ }, { "cell_type": "code", - "execution_count": 132, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":solve: Computation not completed: no solution found (but one might exist)", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":solve z3 !x.(x:1..2 => !y.(y:1..3 => (x,y):r)) & r<: (1..10)*(1..10)" ] - }, - { - "cell_type": "code", - "execution_count": 133, - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:09:32,837, T+942686] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: !x.(x : 1 .. 2 => !y.(y : 1 .. 3 => x |-> y : r)) ... ints: irange(1,10), intatoms: irange(1,10)\u001b[0m\n", - "[2018-06-04 14:09:32,839, T+942688] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2,2,0,2,3,6,0,4,2,0,1,1,2,1,2,0,1,2,4,2,0,1]\u001b[0m\n", - "Execution time: 0.112904757 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tr = {(1↦3),(1↦1),(1↦2),(2↦3),(2↦1),(2↦2)}" - ] - }, - "execution_count": 133, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":time :solve kodkod !x.(x:1..2 => !y.(y:1..3 => (x,y):r)) & r<: (1..10)*(1..10)" - ] - }, - { - "cell_type": "code", - "execution_count": 134, - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.019540215 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tr = {(1↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦3)}" - ] - }, - "execution_count": 134, - "metadata": {}, - "output_type": "execute_result" - } - ], + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + ":time :solve kodkod !x.(x:1..2 => !y.(y:1..3 => (x,y):r)) & r<: (1..10)*(1..10)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], "source": [ ":time :solve prob !x.(x:1..2 => !y.(y:1..3 => (x,y):r)) & r<: (1..10)*(1..10)" ] @@ -4962,31 +3898,9 @@ }, { "cell_type": "code", - "execution_count": 135, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:09:33,012, T+942861] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n", - "[2018-06-04 14:09:34,585, T+944434] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63565\n", - "[2018-06-04 14:09:34,585, T+944434] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47984\n", - "[2018-06-04 14:09:34,589, T+944438] \"ProB Output Logger for instance 79d26131\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-06-04 14:09:34,613, T+944462] \"ProB Output Logger for instance 79d26131\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n" - ] - }, - { - "data": { - "text/plain": [ - "Loaded machine: signals : []\n" - ] - }, - "execution_count": 135, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "::load\n", "MACHINE\n", @@ -5021,31 +3935,9 @@ }, { "cell_type": "code", - "execution_count": 136, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.201494972 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tres = {PL01,PL12}\n", - "\tnxt = {(PL01↦PL02),(PL02↦PL03),(PL03↦PL04),(PL04↦PL05),(PL05↦PL06),(PL06↦PL07),(PL07↦PL08),(PL08↦PL09),(PL09↦PL10),(PL10↦PL11),(PL11↦PL11),(PL12↦PL13),(PL13↦PL14),(PL14↦PL15),(PL15↦PL16),(PL16↦PL17),(PL17↦PL18),(PL18↦PL19),(PL19↦PL20),(PL20↦PL20)}" - ] - }, - "execution_count": 136, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve prob nxt = \n", " {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n", @@ -5058,18 +3950,9 @@ }, { "cell_type": "code", - "execution_count": 137, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":time: :solve: Computation not completed: no solution found (but one might exist)", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:time: :solve: Computation not completed: no solution found (but one might exist)\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":time :solve z3 nxt = \n", " {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n", @@ -5082,34 +3965,9 @@ }, { "cell_type": "code", - "execution_count": 138, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:09:38,479, T+948328] \"ProB Output Logger for instance 79d26131\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: nxt = {PL01 |-> PL02,PL02 |-> PL03,PL03 |-> PL04,P... ints: none, intatoms: none\u001b[0m\n", - "[2018-06-04 14:09:38,480, T+948329] \"ProB Output Logger for instance 79d26131\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n", - "[2018-06-04 14:09:38,480, T+948329] \"ProB Output Logger for instance 79d26131\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2]\u001b[0m\n", - "Execution time: 0.686312764 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tres = {PL01,PL12}\n", - "\tnxt = {(PL01↦PL02),(PL02↦PL03),(PL03↦PL04),(PL04↦PL05),(PL05↦PL06),(PL06↦PL07),(PL07↦PL08),(PL08↦PL09),(PL09↦PL10),(PL10↦PL11),(PL11↦PL11),(PL12↦PL13),(PL13↦PL14),(PL14↦PL15),(PL15↦PL16),(PL16↦PL17),(PL17↦PL18),(PL18↦PL19),(PL19↦PL20),(PL20↦PL20)}" - ] - }, - "execution_count": 138, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve kodkod nxt = \n", " {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n", @@ -5122,31 +3980,9 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 15:03:05,856, T+241807] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n", - "[2018-06-04 15:03:07,015, T+242966] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 51091\n", - "[2018-06-04 15:03:07,018, T+242969] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 50312\n", - "[2018-06-04 15:03:07,021, T+242972] \"ProB Output Logger for instance 5f836b9a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-06-04 15:03:07,034, T+242985] \"ProB Output Logger for instance 5f836b9a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n" - ] - }, - { - "data": { - "text/plain": [ - "Loaded machine: signals : []\n" - ] - }, - "execution_count": 4, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "::load\n", "MACHINE\n", @@ -5201,35 +4037,9 @@ }, { "cell_type": "code", - "execution_count": 140, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:09:40,326, T+950175] \"ProB Output Logger for instance 1361b11\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] empty_kodkod_union_constraint\u001b[0m\n", - "[2018-06-04 14:09:40,326, T+950175] \"ProB Output Logger for instance 1361b11\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod fail: nxt = {PL01 |-> PL02,PL02 |-> PL03,PL03 |-> PL04,P... , reason: integer without upper and lower bound in: {max(ran(nrs))} while extracting used types\u001b[0m\n", - "Execution time: 0.318373176 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tcl1 = ∃197∈{(PL01↦PL02),(PL01↦PL03),…,(PL33↦PL35),(PL34↦PL35)}\n", - "\tmx = {PL01}\n", - "\tnxt = {(PL01↦PL02),(PL02↦PL03),(PL03↦PL04),(PL04↦PL05),(PL05↦PL06),(PL06↦PL07),(PL07↦PL08),(PL08↦PL09),(PL09↦PL10),(PL10↦PL11),(PL11↦PL12),(PL12↦PL13),(PL13↦PL14),(PL14↦PL15),(PL15↦PL16),(PL16↦PL17),(PL17↦PL18),(PL18↦PL19),(PL19↦PL20),(PL20↦PL20),(PL30↦PL31),(PL31↦PL32),(PL33↦PL34),(PL34↦PL35)}\n", - "\tnrs = {(PL01↦19),(PL02↦18),(PL03↦17),(PL04↦16),(PL05↦15),(PL06↦14),(PL07↦13),(PL08↦12),(PL09↦11),(PL10↦10),(PL11↦9),(PL12↦8),(PL13↦7),(PL14↦6),(PL15↦5),(PL16↦4),(PL17↦3),(PL18↦2),(PL19↦1),(PL20↦1),(PL21↦0),(PL22↦0),(PL23↦0),(PL24↦0),(PL25↦0),(PL26↦0),(PL27↦0),(PL28↦0),(PL29↦0),(PL30↦2),(PL31↦1),(PL32↦0),(PL33↦2),(PL34↦1),(PL35↦0),(PL36↦0),(PL37↦0),(PL38↦0),(PL39↦0),(PL40↦0)}" - ] - }, - "execution_count": 140, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve kodkod nxt = \n", " {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n", @@ -5245,33 +4055,9 @@ }, { "cell_type": "code", - "execution_count": 141, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.046631537 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tcl1 = ∃197∈{(PL01↦PL02),(PL01↦PL03),…,(PL33↦PL35),(PL34↦PL35)}\n", - "\tmx = {PL01}\n", - "\tnxt = {(PL01↦PL02),(PL02↦PL03),(PL03↦PL04),(PL04↦PL05),(PL05↦PL06),(PL06↦PL07),(PL07↦PL08),(PL08↦PL09),(PL09↦PL10),(PL10↦PL11),(PL11↦PL12),(PL12↦PL13),(PL13↦PL14),(PL14↦PL15),(PL15↦PL16),(PL16↦PL17),(PL17↦PL18),(PL18↦PL19),(PL19↦PL20),(PL20↦PL20),(PL30↦PL31),(PL31↦PL32),(PL33↦PL34),(PL34↦PL35)}\n", - "\tnrs = {(PL01↦19),(PL02↦18),(PL03↦17),(PL04↦16),(PL05↦15),(PL06↦14),(PL07↦13),(PL08↦12),(PL09↦11),(PL10↦10),(PL11↦9),(PL12↦8),(PL13↦7),(PL14↦6),(PL15↦5),(PL16↦4),(PL17↦3),(PL18↦2),(PL19↦1),(PL20↦1),(PL21↦0),(PL22↦0),(PL23↦0),(PL24↦0),(PL25↦0),(PL26↦0),(PL27↦0),(PL28↦0),(PL29↦0),(PL30↦2),(PL31↦1),(PL32↦0),(PL33↦2),(PL34↦1),(PL35↦0),(PL36↦0),(PL37↦0),(PL38↦0),(PL39↦0),(PL40↦0)}" - ] - }, - "execution_count": 141, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve prob nxt = \n", " {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n", @@ -5287,72 +4073,9 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "|Nr|prj1|prj2|\n", - "|---|---|---|\n", - "|1|PL01|PL02|\n", - "|2|PL02|PL03|\n", - "|3|PL03|PL04|\n", - "|4|PL04|PL05|\n", - "|5|PL05|PL06|\n", - "|6|PL06|PL07|\n", - "|7|PL07|PL08|\n", - "|8|PL08|PL09|\n", - "|9|PL09|PL10|\n", - "|10|PL10|PL11|\n", - "|11|PL11|PL12|\n", - "|12|PL12|PL13|\n", - "|13|PL13|PL14|\n", - "|14|PL14|PL15|\n", - "|15|PL15|PL16|\n", - "|16|PL16|PL17|\n", - "|17|PL17|PL18|\n", - "|18|PL18|PL19|\n", - "|19|PL19|PL20|\n", - "|20|PL20|PL20|\n", - "|21|PL30|PL31|\n", - "|22|PL31|PL32|\n", - "|23|PL33|PL34|\n", - "|24|PL34|PL35|\n" - ], - "text/plain": [ - "Nr\tprj1\tprj2\n", - "1\tPL01\tPL02\n", - "2\tPL02\tPL03\n", - "3\tPL03\tPL04\n", - "4\tPL04\tPL05\n", - "5\tPL05\tPL06\n", - "6\tPL06\tPL07\n", - "7\tPL07\tPL08\n", - "8\tPL08\tPL09\n", - "9\tPL09\tPL10\n", - "10\tPL10\tPL11\n", - "11\tPL11\tPL12\n", - "12\tPL12\tPL13\n", - "13\tPL13\tPL14\n", - "14\tPL14\tPL15\n", - "15\tPL15\tPL16\n", - "16\tPL16\tPL17\n", - "17\tPL17\tPL18\n", - "18\tPL18\tPL19\n", - "19\tPL19\tPL20\n", - "20\tPL20\tPL20\n", - "21\tPL30\tPL31\n", - "22\tPL31\tPL32\n", - "23\tPL33\tPL34\n", - "24\tPL34\tPL35\n" - ] - }, - "execution_count": 5, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":table {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n", " PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09,\n", @@ -5364,35 +4087,13 @@ }, { "cell_type": "code", - "execution_count": 142, + "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:09:40,536, T+950385] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n", - "[2018-06-04 14:09:41,873, T+951722] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63578\n", - "[2018-06-04 14:09:41,874, T+951723] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47994\n", - "[2018-06-04 14:09:41,875, T+951724] \"ProB Output Logger for instance 1145e2a2\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-06-04 14:09:41,890, T+951739] \"ProB Output Logger for instance 1145e2a2\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n" - ] - }, - { - "data": { - "text/plain": [ - "Loaded machine: SlotSolver_KodkodTest : []\n" - ] - }, - "execution_count": 142, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "::load\n", "MACHINE SlotSolver_KodkodTest\n", @@ -5406,31 +4107,9 @@ }, { "cell_type": "code", - "execution_count": 143, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Execution time: 0.353512947 seconds\n" - ] - }, - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tcs = {kom,lin,pol,rom}\n", - "\tmapping = ∃235∈{(((ang↦1)↦T_KF)↦1),(((ang↦1)↦T_KF)↦5),…,(((soz↦2)↦T_EF)↦156),(((soz↦2)↦T_EF)↦158)}" - ] - }, - "execution_count": 143, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ ":time :solve prob mapping = {\n", " (lin, 1, T_EF, 102),\n", @@ -5672,6 +4351,87 @@ " cs = {c|#(sem,typ,nr).( (c,sem,typ,nr):mapping & nr:100..150)}" ] }, + { + "cell_type": "code", + "execution_count": 100, + "metadata": {}, + "outputs": [ + { + "ename": "CliError", + "evalue": "Error during communication with Prolog core.", + "output_type": "error", + "traceback": [ + "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[1m\u001b[31mde.prob.exception.CliError: Error during communication with Prolog core.\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob.cli.ProBInstance.send(ProBInstance.java:78)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob.animator.CommandProcessor.sendCommand(CommandProcessor.java:48)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:68)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.execute(StateSpace.java:549)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.SolveCommand.run(SolveCommand.java:76)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:109)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:124)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.TimeCommand.run(TimeCommand.java:32)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:109)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:124)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$0(ShellChannel.java:50)\u001b[0m", + "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:39)\u001b[0m", + "\u001b[1m\u001b[31mCaused by: java.io.IOException: ProB binary returned nothing - it might have crashed\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob.cli.ProBConnection.getAnswer(ProBConnection.java:75)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob.cli.ProBConnection.send(ProBConnection.java:62)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob.cli.ProBInstance.send(ProBInstance.java:76)\u001b[0m", + "\u001b[1m\u001b[31m\t... 13 more\u001b[0m" + ] + } + ], + "source": [ + ":time :solve kodkod f = %x.(x:1..1000 & x mod 2 = 1|x+1) & f[800..802] = res" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "For 2000: this takes 55 seconds already and generates Java out of heap error." + ] + }, + { + "cell_type": "code", + "execution_count": 99, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "Execution time: 0.053545046 seconds" + ], + "text/plain": [ + "Execution time: 0.053545046 seconds" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/plain": [ + "TRUE\n", + "\n", + "Solution:\n", + "\tres = {802}\n", + "\tf = ∃1000∈{(1↦2),(3↦4),…,(1997↦1998),(1999↦2000)}" + ] + }, + "execution_count": 99, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":time :solve prob f = %x.(x:1..2000 & x mod 2 = 1|x+1) & f[800..802] = res" + ] + }, { "cell_type": "code", "execution_count": null, diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb index 7752c94..b8acdd1 100644 --- a/notebooks/tutorials/prob_solver_intro.ipynb +++ b/notebooks/tutorials/prob_solver_intro.ipynb @@ -338,6 +338,46 @@ " => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))" ] }, + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "|Nr|prj1|prj2|\n", + "|---|---|---|\n", + "|1|1|1|\n", + "|2|2|5|\n", + "|3|3|8|\n", + "|4|4|6|\n", + "|5|5|3|\n", + "|6|6|7|\n", + "|7|7|2|\n", + "|8|8|4|\n" + ], + "text/plain": [ + "Nr\tprj1\tprj2\n", + "1\t1\t1\n", + "2\t2\t5\n", + "3\t3\t8\n", + "4\t4\t6\n", + "5\t5\t3\n", + "6\t6\t7\n", + "7\t7\t2\n", + "8\t8\t4\n" + ] + }, + "execution_count": 1, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":table {(1↦1),(2↦5),(3↦8),(4↦6),(5↦3),(6↦7),(7↦2),(8↦4)}" + ] + }, { "cell_type": "code", "execution_count": 11, -- GitLab