diff --git a/notebooks/presentations/SETS_RODIN18.ipynb b/notebooks/presentations/SETS_RODIN18.ipynb index 7004a21ca6d982932cb0bc966d4aa83c71f73594..dba64d2a14c959093ccb6128c719098cae601456 100644 --- a/notebooks/presentations/SETS_RODIN18.ipynb +++ b/notebooks/presentations/SETS_RODIN18.ipynb @@ -121,7 +121,7 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 14, "metadata": { "slideshow": { "slide_type": "-" @@ -132,11 +132,11 @@ "name": "stdout", "output_type": "stream", "text": [ - "[2018-06-04 13:54:14,028, T+23877] \"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 13:54:15,603, T+25452] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 62613\n", - "[2018-06-04 13:54:15,605, T+25454] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47762\n", - "[2018-06-04 13:54:15,609, T+25458] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-06-04 13:54:15,624, T+25473] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n" + "[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" ] }, { @@ -145,7 +145,7 @@ "Loaded machine: MyBasicSets : []\n" ] }, - "execution_count": 4, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -741,7 +741,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "Function application:" ] @@ -761,7 +765,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "fragment" + } + }, "source": [ "Relational inverse (.~) and relational image .[.] :" ] @@ -985,7 +993,17 @@ "source": [ "## Constraint Solving Applications ##\n", "Constraint solving has many applications in formal methods in general and B in particular.\n", - "\n", + "\n" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ "#### Animation ####\n", "It is required to animate implicit specifications.\n", "Take for example an event\n", @@ -1150,7 +1168,11 @@ { "cell_type": "code", "execution_count": 32, - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "skip" + } + }, "outputs": [ { "data": { @@ -1173,7 +1195,7 @@ }, { "cell_type": "code", - "execution_count": 33, + "execution_count": 16, "metadata": {}, "outputs": [ { @@ -1192,13 +1214,13 @@ "\tO = 0" ] }, - "execution_count": 33, + "execution_count": 16, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & \n", + "{S,E,N,D, M,O,R, Y} ⊆ 0..9 & S >0 & M >0 & \n", " card({S,E,N,D, M,O,R, Y}) = 8 & \n", " S*1000 + E*100 + N*10 + D +\n", " M*1000 + O*100 + R*10 + E =\n", @@ -1207,7 +1229,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "We can find all solutions (to the unmodified puzzle) using a set comprehension and make sure that there is just a single soltuion:" ] @@ -1237,6 +1263,37 @@ " M*10000 + O*1000 + N*100 + E*10 + Y }" ] }, + { + "cell_type": "code", + "execution_count": 15, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "|Nr|S|E|N|D|M|O|R|Y|\n", + "|---|---|---|---|---|---|---|---|---|\n", + "|1|9|5|6|7|1|0|8|2|\n" + ], + "text/plain": [ + "Nr\tS\tE\tN\tD\tM\tO\tR\tY\n", + "1\t9\t5\t6\t7\t1\t0\t8\t2\n" + ] + }, + "execution_count": 15, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":table {S,E,N,D, M,O,R, Y |\n", + " {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & \n", + " card({S,E,N,D, M,O,R, Y}) = 8 & \n", + " S*1000 + E*100 + N*10 + D +\n", + " M*1000 + O*100 + R*10 + E =\n", + " M*10000 + O*1000 + N*100 + E*10 + Y }" + ] + }, { "cell_type": "markdown", "metadata": { @@ -1331,13 +1388,27 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "### Booleans ###\n", "\n", "If we have only booleans, constraint solving is equivalent to SAT solving.\n", "Internally, ProB has an interpreter which does **not** translate to CNF (conjunctive normal form), but is otherwise similar to DPLL: deterministic propagations are carried out first (unit propagation) and there are heuristics to choose the next boolean variable to enumerate.\n", - "(We do not translate to CNF also because of well-definedness issues.)\n", + "(We do not translate to CNF also because of well-definedness issues.)\n" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ "\n", "#### Knights and Knave Puzzle####\n", "Here is a puzzle from Smullyan involving an island with only knights and knaves.\n", @@ -1356,7 +1427,11 @@ { "cell_type": "code", "execution_count": 37, - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "fragment" + } + }, "outputs": [ { "data": { @@ -1391,45 +1466,7 @@ "\n", "Let us take the integer constraint ```x*x=100``` which we saw earlier.\n", "This constraint is actually more complicated than might appear at first sight: the constraint is not linear and the domain of x is not bounded. Indeed, B supports mathematical integers without any bit size restriction.\n", - "So, let us first look at some simpler constraints, where the domains of the variables are all bounded.\n", - "Let us consider a small arithmetic puzzle \n", - "```\n", - " X Y\n", - "+ X Y\n", - "-----\n", - " Y 0\n", - "```" - ] - }, - { - "cell_type": "code", - "execution_count": 38, - "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tX = 2\n", - "\tY = 5" - ] - }, - "execution_count": 38, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "X:1..9 & Y:0..9 & X*10 + Y + X*10 + Y = Y*10" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Given that we know the domain of X and Y one can represent the integers by binary numbers and convert the constraint to a SAT problem." + "So, let us first look at some simpler constraints, where the domains of the variables are all bounded." ] }, { @@ -1440,7 +1477,8 @@ } }, "source": [ - "Let us look at an even simpler constraint X:0..3 & Y:0..3 & X+Y=2. As you can see there are three solutions for this constraint:\n" + "Let us look at the simple constraint ```X:0..3 & Y:0..3 & X+Y=2```.\n", + "As you can see there are three solutions for this constraint:\n" ] }, { @@ -1472,11 +1510,15 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "slide" + } + }, "source": [ "#### Solving constraints by translating to SAT ####\n", - "Given that we know the domain of X and Y in the constraint ``` X:0..3 & Y:0..3 & X+Y=2``` one can represent the integers by binary numbers and convert the constraint to a SAT problem.\n", - "The number 2 is 10 in binary and we can represent X and Y each by two bits X0,X1 and Y0,Y1.\n", + "Given that we know the *domain* of X and Y in the constraint ``` X:0..3 & Y:0..3 & X+Y=2```, we can represent the integers by binary numbers and convert the constraint to a **SAT** problem.\n", + "The number 2 is ```10``` in binary and we can represent X and Y each by two bits X0,X1 and Y0,Y1.\n", "We can translate the addition to a propositional logic formula:\n", "\n", "Bit1 | Bit0\n", @@ -1486,7 +1528,7 @@ " |\n", " Z1 | Z0\n", " \n", - "Let us find one solution to this constraint, by encoding addition using an additional carry bit:" + "Let us find one solution to this constraint, by encoding addition using an additional carry bit ```CARRY0```:" ] }, { @@ -1525,7 +1567,11 @@ { "cell_type": "code", "execution_count": 41, - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "outputs": [ { "data": { @@ -1557,7 +1603,11 @@ { "cell_type": "code", "execution_count": 42, - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "fragment" + } + }, "outputs": [ { "data": { @@ -1602,7 +1652,11 @@ { "cell_type": "code", "execution_count": 43, - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "outputs": [ { "name": "stdout", @@ -1676,12 +1730,28 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "slide" + } + }, "source": [ "#### Translation to SMTLib ####\n", - "At iFM'2016 we (Krings, L.) presented a translation to SMTLib format to use either the Z3 or CVC4 SMT solver.\n", - "Compared to the Kodkod backend, no translation to SAT is performed, SMTLib supports integer predicates and operators in the language.\n", - "Here is ProB's SMTLib/Z3 API calls for the constraint:\n", + "At iFM'2016 we (Krings, L.) presented a translation to SMTLib format to use either the **Z3** or **CVC4** SMT solver.\n", + "Compared to the Kodkod backend, no translation to SAT is performed, SMTLib supports **integer** predicates and integer operators in the language.\n", + "\n", + "\n" + ] + }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "Here is ProB's SMTLib/Z3 API calls for the constraint ``` X:0..3 & Y:0..3 & X+Y=2```:\n", "- mk_var(integer,x) $\\rightarrow$ 2\n", "- mk_var(integer,y) $\\rightarrow$ 3\n", "- mk_int_const(0) $\\rightarrow$ 4\n", @@ -1726,7 +1796,7 @@ "cell_type": "markdown", "metadata": { "slideshow": { - "slide_type": "subslide" + "slide_type": "slide" } }, "source": [ @@ -1749,11 +1819,34 @@ " - x=2 $\\leadsto$ x:2..2, y:0..0" ] }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "Let us now examine the three approaches for the KISS-PASSION puzzle:" + ] + }, { "cell_type": "code", - "execution_count": 46, + "execution_count": 17, "metadata": {}, "outputs": [ + { + "data": { + "text/markdown": [ + "Execution time: 0.050491290 seconds" + ], + "text/plain": [ + "Execution time: 0.050491290 seconds" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, { "data": { "text/plain": [ @@ -1769,46 +1862,63 @@ "\tO = 8" ] }, - "execution_count": 46, + "execution_count": 17, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":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 & (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" ] }, { "cell_type": "code", - "execution_count": 47, - "metadata": {}, + "execution_count": 18, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "outputs": [ { "ename": "CommandExecutionException", - "evalue": ":solve: Computation not completed: no solution found (but one might exist)", + "evalue": ":time: :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" + "\u001b[1m\u001b[31m:time: :solve: Computation not completed: no solution found (but one might exist)\u001b[0m" ] } ], "source": [ - ":solve z3 {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 z3 {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" ] }, { "cell_type": "code", - "execution_count": 48, + "execution_count": 19, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "[2018-06-04 14:01:42,085, T+471934] \"ProB Output Logger for instance 1ede3ed1\" 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 14:01:42,086, T+471935] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [373]\u001b[0m\n" + "[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" ] }, + { + "data": { + "text/markdown": [ + "Execution time: 2.287290784 seconds" + ], + "text/plain": [ + "Execution time: 2.287290784 seconds" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, { "data": { "text/plain": [ @@ -1824,18 +1934,22 @@ "\tO = 8" ] }, - "execution_count": 48, + "execution_count": 19, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":solve kodkod {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 kodkod {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" ] }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "Result for KISS*KISS=PASSION puzzle:\n", "\n", @@ -1848,7 +1962,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "slide" + } + }, "source": [ "### Unbounded integers ###\n", "The SAT translation via Kodkod/Alloy requires to determine the bid width.\n", @@ -2020,7 +2138,8 @@ } }, "source": [ - "Here is an inconsistency which cannot be detected by CLP(FD)'s interval propagation. ProB can detect it with CHR enabled, but without the module the result is **UNKNOWN**." + "Here is an inconsistency which cannot be detected by CLP(FD)'s interval propagation.\n", + "ProB can detect it with CHR (Constraint Handling Rules) enabled, but without the module the result is **UNKNOWN**." ] }, { @@ -2072,7 +2191,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "### Summary for Integer Arithmetic ###\n", "\n", @@ -2195,7 +2318,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "This translation to SAT is exactly what the Kodkod backend does:" ] @@ -2299,7 +2426,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "Also, in the following constraint, the set x is unbounded and no translation to SAT is feasible (without a very clever analysis of the universal implications)." ] @@ -2327,6 +2458,61 @@ "{100}:x & !y.(y:x => (!z.(z:y => y \\/ {z / 2}:x)))" ] }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "However, when it is applicable the propositional encoding of sets can be very effective for SAT solvers.\n", + "The following example, involving various relational operators can currently only be solved by our Kodkod backend:" + ] + }, + { + "cell_type": "code", + "execution_count": 20, + "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" + ] + }, + { + "data": { + "text/markdown": [ + "Execution time: 0.153314218 seconds" + ], + "text/plain": [ + "Execution time: 0.153314218 seconds" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/plain": [ + "TRUE\n", + "\n", + "Solution:\n", + "\tr = {(3↦5),(3↦4),(5↦5),(5↦4),(1↦4),(2↦4),(4↦4)}" + ] + }, + "execution_count": 20, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":time :solve kodkod r: 1..5 <-> 1..5 & (r;r) = r & r /= {} & dom(r)=1..5 & r[2..3]=4..5" + ] + }, { "cell_type": "markdown", "metadata": { @@ -2375,7 +2561,11 @@ { "cell_type": "code", "execution_count": 64, - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "fragment" + } + }, "outputs": [ { "data": { @@ -2437,7 +2627,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "This can be solved by Z3 but not by CVC4. Already the slightly more complicated example from above (or the other examples) cannot be solved:" ] @@ -2525,7 +2719,11 @@ { "cell_type": "code", "execution_count": 67, - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "outputs": [ { "data": { @@ -2554,7 +2752,11 @@ { "cell_type": "code", "execution_count": 68, - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "outputs": [ { "name": "stdout", @@ -2681,7 +2883,6 @@ }, "source": [ "### ProB's Set Solver ###\n", - "\n", "ProB has actually three set representations:\n", "- Prolog lists of elements\n", "- AVL trees for fully known sets\n", @@ -2696,7 +2897,6 @@ "The list representation is used for sets where some of the members are known or partially known.\n", "\n", "#### AVL tree representation ####\n", - "\n", "The following generates the AVL tree representation:" ] }, @@ -2871,7 +3071,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "The virtual timeout message can be removed (and performance improved) by adding the symbolic pragma:" ] @@ -2916,7 +3120,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "#### List representation ####\n", "The list representation is used when a finite set is partially known and constraint solving has to determine the set.\n" @@ -2927,7 +3135,7 @@ "execution_count": 78, "metadata": { "slideshow": { - "slide_type": "subslide" + "slide_type": "fragment" } }, "outputs": [ @@ -3148,7 +3356,11 @@ { "cell_type": "code", "execution_count": 91, - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "outputs": [ { "ename": "CommandExecutionException", @@ -3389,7 +3601,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "slide" + } + }, "source": [ "### Relation to SETLOG ###\n", "\n", @@ -3435,7 +3651,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "Another example from that paper is\n", "```\n", @@ -3611,7 +3831,11 @@ { "cell_type": "code", "execution_count": 102, - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "outputs": [ { "name": "stdout", @@ -3658,13 +3882,34 @@ "- ProB's default backend:\n", " - can deal with unbounded and large sets\n", " - limited constraint solving for complex constraints involving image, transitive closure,...\n", + " - no learning, backjumping\n", " - works well for large sets and semi-deterministic computation\n", " - works well for animation, data validation, disproving\n", - " - limitations trigger for symbolic model checking (IC3,...)\n", - " - Future work: improve combination with Z3, improve list representation (maybe use a bit-vector like representation) \n", + " - limitations appear for symbolic model checking (IC3,...)\n", + " - Future work: improve combination with Z3/Kodkod, improve list representation (maybe use a bit-vector like representation, and CLP(FD) cardinality variable) \n", " " ] }, + { + "cell_type": "markdown", + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, + "source": [ + "### Integrations of Approaches ###\n", + "\n", + "ProB provides the joint application of the CLP(FD) and SMT backend (preference ```SMT_SUPPORTED_INTERPRETER```.\n", + "Constraints are posted both to ProB and Z3/CVC4, with the hope that Z3/CVC4 prune infeasible branches.\n", + "The main motivation was new symbolic validation techniques such as IC3.\n", + "\n", + "The Kodkod integration also passes higher-order/unbounded constraints to ProB, after solving the first order finite constraints with Kodkod/Alloy.\n", + "However, this kind of integration is rarely useful (most of the generated solutions get rejected by ProB).\n", + "\n", + "A more promising, fine-grained integration has been presented at PADL'18." + ] + }, { "cell_type": "markdown", "metadata": { @@ -3829,7 +4074,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "In the following the inverse operator seems to pose problems to Z3:" ] @@ -3880,7 +4129,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "slide" + } + }, "source": [ "### Comparison ###\n", "Some further examples for comparison of the backends" @@ -4100,7 +4353,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "slide" + } + }, "source": [ "#### Graph theorem ####\n", "\n", @@ -4109,18 +4366,18 @@ }, { "cell_type": "code", - "execution_count": 117, + "execution_count": 10, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "[2018-06-04 14:09:20,430, T+930279] \"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:21,622, T+931471] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63550\n", - "[2018-06-04 14:09:21,622, T+931471] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47978\n", - "[2018-06-04 14:09:21,624, T+931473] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-06-04 14:09:21,638, T+931487] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n" + "[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" ] }, { @@ -4129,7 +4386,7 @@ "Loaded machine: GraphTheorem : []\n" ] }, - "execution_count": 117, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } @@ -4194,7 +4451,11 @@ { "cell_type": "code", "execution_count": 120, - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "outputs": [ { "name": "stdout", @@ -4249,7 +4510,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "So with Kodkod we proved the theorem for 5 nodes in about a second.\n", "What if we remove the self-loops restriction:" @@ -4325,7 +4590,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "slide" + } + }, "source": [ "### Benchmark Puzzles ####\n", "\n", @@ -4435,7 +4704,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "#### N-Bishops ####\n" ] @@ -4678,7 +4951,11 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "source": [ "#### Datavalidation example ####\n" ] @@ -4845,18 +5122,18 @@ }, { "cell_type": "code", - "execution_count": 139, + "execution_count": 4, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "[2018-06-04 14:09:38,543, T+948392] \"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:39,778, T+949627] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63572\n", - "[2018-06-04 14:09:39,779, T+949628] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47990\n", - "[2018-06-04 14:09:39,781, T+949630] \"ProB Output Logger for instance 1361b11\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-06-04 14:09:39,798, T+949647] \"ProB Output Logger for instance 1361b11\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n" + "[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" ] }, { @@ -4865,7 +5142,7 @@ "Loaded machine: signals : []\n" ] }, - "execution_count": 139, + "execution_count": 4, "metadata": {}, "output_type": "execute_result" } @@ -5010,8 +5287,89 @@ }, { "cell_type": "code", - "execution_count": 142, + "execution_count": 5, "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" + } + ], + "source": [ + ":table {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n", + " PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09,\n", + " PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL12, PL12 |-> PL13,\n", + " PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17,\n", + " PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20,\n", + " PL30 |-> PL31, PL31 |-> PL32, PL33 |-> PL34, PL34 |-> PL35}" + ] + }, + { + "cell_type": "code", + "execution_count": 142, + "metadata": { + "slideshow": { + "slide_type": "subslide" + } + }, "outputs": [ { "name": "stdout", diff --git a/notebooks/presentations/img/inputoutputflow.pdf b/notebooks/presentations/img/inputoutputflow.pdf new file mode 100644 index 0000000000000000000000000000000000000000..6d46a5603ef25a94a12cc7ece12b6de556c5a66b Binary files /dev/null and b/notebooks/presentations/img/inputoutputflow.pdf differ