diff --git a/notebooks/presentations/LPOP18.ipynb b/notebooks/presentations/LPOP18.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..e150e6f92ad4b7add653520086abac86f18ff47d
--- /dev/null
+++ b/notebooks/presentations/LPOP18.ipynb
@@ -0,0 +1,4844 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "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 ##"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "### Basic Datavalues in B ###"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "-"
+ }
+ },
+ "source": [
+ "B provides the booleans, strings and integers as built-in datatypes. (Strings are not available in Event-B.)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{FALSE},\\mathit{TRUE}\\}$"
+ ],
+ "text/plain": [
+ "{FALSE,TRUE}"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "BOOL"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"this is a string\"}$"
+ ],
+ "text/plain": [
+ "\"this is a string\""
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "\"this is a string\""
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1024$"
+ ],
+ "text/plain": [
+ "1024"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1024"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Users can define their own datatype in a B machine.\n",
+ "One distinguishes between explicitly specified enumerated sets and deferred sets."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "-"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: MyBasicSets"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE MyBasicSets\n",
+ "SETS Trains = {thomas, gordon}; Points\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "For animation and constraint solving purposes, ProB will instantiate deferred sets to some finite set (the size of which can be controlled and is partially inferred)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "-"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{Points1},\\mathit{Points2}\\}$"
+ ],
+ "text/plain": [
+ "{Points1,Points2}"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "Points"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "### Pairs ###\n",
+ "B also has pairs of values, which can be written in two ways:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$(thomas\\mapsto10)$"
+ ],
+ "text/plain": [
+ "(thomas↦10)"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(thomas,10)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$(thomas\\mapsto10)$"
+ ],
+ "text/plain": [
+ "(thomas↦10)"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "thomas |-> 10"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "source": [
+ "Tuples simply correspond to nested pairs:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$((\\mathit{thomas}\\mapsto \\mathit{gordon})\\mapsto 20)$"
+ ],
+ "text/plain": [
+ "((thomas↦gordon)↦20)"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(thomas |-> gordon |-> 20)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Classical B also provides records:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\mathit{r} = \\mathit{rec}(length:20,position:10302,train:\\mathit{thomas})$"
+ ],
+ "text/plain": [
+ "r = rec(length:20,position:10302,train:thomas)"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint r=rec(train:thomas,length:20,position:10302)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "### Sets ###\n",
+ "Sets in B can be specified in multiple ways.\n",
+ "For example, using explicit enumeration:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{1,2,3\\}$"
+ ],
+ "text/plain": [
+ "{1,2,3}"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{1,3,2,3}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "source": [
+ "or via a predicate by using a set comprehension:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{1,2,3\\}$"
+ ],
+ "text/plain": [
+ "{1,2,3}"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x|x>0 & x<4}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "For integers there are a variety of other sets, such as intervals:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{1,2,3\\}$"
+ ],
+ "text/plain": [
+ "{1,2,3}"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1..3"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "or the set of implementable integers INT = MININT..MAXINT or the set of implementable natural numbers NAT = 0..MAXINT."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Sets can be higher-order and contain other sets:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\{0,1\\},\\{1,2,3\\}\\}$"
+ ],
+ "text/plain": [
+ "{{0,1},{1,2,3}}"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{ 1..3, {1,2,3,2}, 0..1, {x|x>0 & x<4} }"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "source": [
+ "Relations are modelled as sets of pairs:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(\\mathit{thomas}\\mapsto \\mathit{thomas}),(\\mathit{thomas}\\mapsto \\mathit{gordon}),(\\mathit{gordon}\\mapsto \\mathit{gordon})\\}$"
+ ],
+ "text/plain": [
+ "{(thomas↦thomas),(thomas↦gordon),(gordon↦gordon)}"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{ thomas|->gordon, gordon|->gordon, thomas|->thomas}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+ "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+ "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"128pt\" height=\"188pt\"\n",
+ " viewBox=\"0.00 0.00 128.00 188.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 184)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-184 125,-184 125,5 -4,5\"/>\n",
+ "<g id=\"graph2\" class=\"cluster\"><title>cluster_Trains</title>\n",
+ "<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-172 112,-172 112,-8 8,-8\"/>\n",
+ "<text text-anchor=\"middle\" x=\"60\" y=\"-157.2\" font-family=\"Times,serif\" font-size=\"12.00\">Trains</text>\n",
+ "</g>\n",
+ "<!-- gordon -->\n",
+ "<g id=\"node1\" class=\"node\"><title>gordon</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"71.249,-52 16.751,-52 16.751,-16 71.249,-16 71.249,-52\"/>\n",
+ "<text text-anchor=\"middle\" x=\"44\" y=\"-29.8\" font-family=\"Times,serif\" font-size=\"14.00\">gordon</text>\n",
+ "</g>\n",
+ "<!-- gordon->gordon -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>gordon->gordon</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M71.6842,-42.248C81.2638,-42.3353 89,-39.5859 89,-34 89,-30.5961 86.1273,-28.2455 81.7152,-26.9482\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"82.0283,-23.4609 71.6842,-25.752 81.1994,-30.4116 82.0283,-23.4609\"/>\n",
+ "<text text-anchor=\"middle\" x=\"96.3829\" y=\"-29.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
+ "</g>\n",
+ "<!-- thomas -->\n",
+ "<g id=\"node3\" class=\"node\"><title>thomas</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"72.3312,-142 15.6688,-142 15.6688,-106 72.3312,-106 72.3312,-142\"/>\n",
+ "<text text-anchor=\"middle\" x=\"44\" y=\"-119.8\" font-family=\"Times,serif\" font-size=\"14.00\">thomas</text>\n",
+ "</g>\n",
+ "<!-- thomas->gordon -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>thomas->gordon</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M44,-105.614C44,-93.2403 44,-76.3686 44,-62.2198\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"47.5001,-62.0504 44,-52.0504 40.5001,-62.0504 47.5001,-62.0504\"/>\n",
+ "<text text-anchor=\"middle\" x=\"51.3829\" y=\"-74.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
+ "</g>\n",
+ "<!-- thomas->thomas -->\n",
+ "<g id=\"edge6\" class=\"edge\"><title>thomas->thomas</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M72.2994,-132.248C82.0919,-132.335 90,-129.586 90,-124 90,-120.596 87.0634,-118.245 82.5533,-116.948\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"82.6376,-113.434 72.2994,-115.752 81.8265,-120.387 82.6376,-113.434\"/>\n",
+ "<text text-anchor=\"middle\" x=\"97.3829\" y=\"-119.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [(\"rel\",{(thomas,gordon),(gordon,gordon),(thomas,thomas)})]>"
+ ]
+ },
+ "execution_count": 28,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph (\"rel\",{ thomas|->gordon, gordon|->gordon, thomas|->thomas})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "source": [
+ "Note: a pair is an element of a Cartesian product, and a relation is just a subset of a Cartesian product.\n",
+ "The above relation is a subset of ```Trains * Trains```."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Functions are relations which map every domain element to at most one value:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(thomas\\mapsto1),(gordon\\mapsto2)\\}$"
+ ],
+ "text/plain": [
+ "{(thomas↦1),(gordon↦2)}"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{ thomas|->1, gordon|->2}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "## Expressions vs Predicates vs Substitutions ##"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "source": [
+ "\n",
+ "### Expressions ###\n",
+ "Expressions in B have a value. With ProB and with ProB's Jupyter backend, you can evaluate expresssions such as:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376$"
+ ],
+ "text/plain": [
+ "10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "2**1000"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "B provides many operators which return values, such as the usual arithmetic operators but also many operators for sets, relations and functions.\n",
+ "For example set union and set difference:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{1,7,8,9,10\\}$"
+ ],
+ "text/plain": [
+ "{1,7,8,9,10}"
+ ]
+ },
+ "execution_count": 19,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(1..3 \\/ 5..10) \\ (2..6)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{1,7,8,9,10\\}$"
+ ],
+ "text/plain": [
+ "{1,7,8,9,10}"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(1..3 ∪ 5..10) \\ (2..6)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The range of a relation or function:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{thomas,gordon\\}$"
+ ],
+ "text/plain": [
+ "{thomas,gordon}"
+ ]
+ },
+ "execution_count": 22,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "dom({(thomas↦1),(gordon↦2)})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Function application:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 21,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1$"
+ ],
+ "text/plain": [
+ "1"
+ ]
+ },
+ "execution_count": 21,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{(thomas↦1),(gordon↦2)} (thomas)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "source": [
+ "Relational inverse (.~) and relational image .[.] :"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{gordon}\\}$"
+ ],
+ "text/plain": [
+ "{gordon}"
+ ]
+ },
+ "execution_count": 22,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{(thomas↦1),(gordon↦2)}~[2..3]"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "## Predicates\n",
+ "ProB can also be used to evaluate predicates (B distinguishes between expressions which have a value and predicates which are either true or false)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$FALSE$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "2>3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 26,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "3>2"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Within predicates you can use **open** variables, which are implicitly existentially quantified.\n",
+ "ProB will display the solution for the open variables, if possible."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = -10$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = −10"
+ ]
+ },
+ "execution_count": 23,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x*x=100"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "source": [
+ "We can find all solutions to a predicate by using the set comprehension notation.\n",
+ "Note that by this we turn a predicate into an expression."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 24,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{-10,10\\}$"
+ ],
+ "text/plain": [
+ "{−10,10}"
+ ]
+ },
+ "execution_count": 24,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x|x*x=100}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "### Substitutions ###\n",
+ "B also has a rich syntax for substitutions, aka statements.\n",
+ "For example ```x := x+1``` increments the value of x by 1.\n",
+ "We will not talk about substitutions in the rest of this presentation.\n",
+ "The major differences between classical B and Event-B lie in the area of substitutions, machine composition and refinement."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "## Definition of Constraint Solving ##\n",
+ "\n",
+ "Constraint solving is determine whether a predicate with open/existentially quantified variables is satisfiable and providing values for the open variables in case it is.\n",
+ "We have already solved the predicate ```x*x=100``` above, yielding the solution ```x=-10```.\n",
+ "The following is an unsatisfiable predicate:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\exists \\mathit{x}\\cdot (\\mathit{x} \\in \\mathbb N \\wedge \\mathit{x} * \\mathit{x} = 1000)$"
+ ],
+ "text/plain": [
+ "∃x·(x ∈ ℕ ∧ x * x = 1000)"
+ ]
+ },
+ "execution_count": 29,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint #x.(x:NATURAL & x*x=1000)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The difference to **proof** is that in constraint solving one has to produce a solution (aka a model). The difference to **execution** is that not all variables are known."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "## Constraint Solving Applications ##\n",
+ "Constraint solving has many applications in formal methods in general and B in particular.\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",
+ "```\n",
+ "train_catches_up = any t1,t2,x where t1:dom(train_position) & t2:dom(train_position) &\n",
+ " train_position(t1) < train_position(t2) &\n",
+ " x:1..(train_position(t2)-train_position(t1)-1) then\n",
+ " train_position(t1) := train_position(t1)+x end\n",
+ "```\n",
+ "To determine whether the event is enabled, and to obtain values for the parameters of the event in a given state of the model, we have to solve the following constraint:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = 1$\n",
+ "* $train_position = \\{(thomas\\mapsto100),(gordon\\mapsto2020)\\}$\n",
+ "* $t1 = thomas$\n",
+ "* $t2 = gordon$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 1\n",
+ "\ttrain_position = {(thomas↦100),(gordon↦2020)}\n",
+ "\tt1 = thomas\n",
+ "\tt2 = gordon"
+ ]
+ },
+ "execution_count": 30,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "train_position = {thomas|->100, gordon|->2020} &\n",
+ "t1:dom(train_position) & t2:dom(train_position) & train_position(t1) < train_position(t2) &\n",
+ "x:1..(train_position(t2)-train_position(t1)-1)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$FALSE$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 31,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "train_position = {thomas|->2019, gordon|->2020} &\n",
+ "t1:dom(train_position) & t2:dom(train_position) & train_position(t1) < train_position(t2) &\n",
+ "x:1..(train_position(t2)-train_position(t1)-1)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Many other applications exist: generating **testcases**, finding counter examples using **bounded model checking** or other algorithms like IC3.\n",
+ "Other applications are analysing **proof obligations**.\n",
+ "Take the proof obligation for an event theorem t1 $/=$ t2:\n",
+ "```\n",
+ "train_position:Trains-->1..10000 & train_position(t1) < train_position(t2) |- t1 /= t2\n",
+ "```\n",
+ "We can find counter examples to it by negating the proof goal:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 34,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$FALSE$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 34,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "train_position:Trains-->1..10000 &\n",
+ "train_position(t1) < train_position(t2) & \n",
+ "not( t1 /= t2 )"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "As no counter example has been found, we can in this case establish the goal to be proven."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "### Modelling and Solving Problems in B ###\n",
+ "\n",
+ "Obviously, we can also use constraint solving to solve puzzles or real-life problems.\n",
+ "#### Send More Money Puzzle ####\n",
+ "We now try and solve the SEND+MORE=MONEY arithmetic puzzle in B, involving 8 distinct digits:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "skip"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\{\\mathit{S},\\mathit{E},\\mathit{N},\\mathit{D},\\mathit{M},\\mathit{O},\\mathit{R},\\mathit{Y}\\} \\subseteq 0 .. 9 \\wedge \\mathit{S} > 0 \\wedge \\mathit{M} > 0 \\wedge \\mathit{card}(\\{\\mathit{S},\\mathit{E},\\mathit{N},\\mathit{D},\\mathit{M},\\mathit{O},\\mathit{R},\\mathit{Y}\\}) = 8 \\wedge \\mathit{S} * 1000 + \\mathit{E} * 100 + \\mathit{N} * 10 + \\mathit{D} + \\mathit{M} * 1000 + \\mathit{O} * 100 + \\mathit{R} * 10 + \\mathit{E} = \\mathit{M} * 10000 + \\mathit{O} * 1000 + \\mathit{N} * 100 + \\mathit{E} * 10 + \\mathit{Y}$"
+ ],
+ "text/plain": [
+ "{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": 30,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & card({S,E,N,D, M,O,R, Y}) = 8 & \n",
+ " S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = M*10000 + O*1000 + N*100 + E*10 + Y"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{R} = 8$\n",
+ "* $\\mathit{S} = 9$\n",
+ "* $\\mathit{D} = 7$\n",
+ "* $\\mathit{E} = 5$\n",
+ "* $\\mathit{Y} = 2$\n",
+ "* $\\mathit{M} = 1$\n",
+ "* $\\mathit{N} = 6$\n",
+ "* $\\mathit{O} = 0$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tR = 8\n",
+ "\tS = 9\n",
+ "\tD = 7\n",
+ "\tE = 5\n",
+ "\tY = 2\n",
+ "\tM = 1\n",
+ "\tN = 6\n",
+ "\tO = 0"
+ ]
+ },
+ "execution_count": 31,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{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": {
+ "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 solution:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 32,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(((((((9\\mapsto 5)\\mapsto 6)\\mapsto 7)\\mapsto 1)\\mapsto 0)\\mapsto 8)\\mapsto 2)\\}$"
+ ],
+ "text/plain": [
+ "{(((((((9↦5)↦6)↦7)↦1)↦0)↦8)↦2)}"
+ ]
+ },
+ "execution_count": 32,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ " {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": "code",
+ "execution_count": 33,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|S|E|N|D|M|O|R|Y|\n",
+ "|---|---|---|---|---|---|---|---|\n",
+ "|$9$|$5$|$6$|$7$|$1$|$0$|$8$|$2$|\n"
+ ],
+ "text/plain": [
+ "S\tE\tN\tD\tM\tO\tR\tY\n",
+ "9\t5\t6\t7\t1\t0\t8\t2\n"
+ ]
+ },
+ "execution_count": 33,
+ "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": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "#### KISS PASSION Puzzle####\n",
+ "A slightly more complicated puzzle (involving multiplication) is the KISS * KISS = PASSION problem."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 39,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $P = 4$\n",
+ "* $A = 1$\n",
+ "* $S = 3$\n",
+ "* $I = 0$\n",
+ "* $K = 2$\n",
+ "* $N = 9$\n",
+ "* $O = 8$"
+ ],
+ "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": 39,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ " {K,P} <: 1..9 &\n",
+ " {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 &\n",
+ " card({K, I, S, P, A, O, N}) = 7"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Finally, a simple puzzle involving sets is to find a subset of numbers from 1..5 whose sum is 14:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 40,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = \\{2,3,4,5\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = {2,3,4,5}"
+ ]
+ },
+ "execution_count": 40,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x <: 1..5 & SIGMA(y).(y:x|y)=14"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "## How to solve (set) constraints in B ##\n",
+ "\n",
+ "We will now examine how one can perform constraint solving for B."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "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"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "### Integers ###\n",
+ "\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."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "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"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 42,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(0\\mapsto2),(1\\mapsto1),(2\\mapsto0)\\}$"
+ ],
+ "text/plain": [
+ "{(0↦2),(1↦1),(2↦0)}"
+ ]
+ },
+ "execution_count": 42,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{X,Y|X:0..3 & Y:0..3 & X+Y=2}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "We will now study how such constraints can be solved."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "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```, 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",
+ "-----|-----\n",
+ " X1 | X0\n",
+ " + Y1 | Y0\n",
+ " |\n",
+ " Z1 | Z0\n",
+ " \n",
+ "Let us find one solution to this constraint, by encoding addition using an additional carry bit ```CARRY0```:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 44,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$4$"
+ ],
+ "text/plain": [
+ "4"
+ ]
+ },
+ "execution_count": 44,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "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})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "As you can see, we have found four solutions and not three! One solution is 3+3=2.\n",
+ "This is a typical issue when translating arithmetic to binary numbers: we have to prevent overflows, which we do below:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 45,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "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": [
+ "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": 45,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":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})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "In ProB, we can use **Kodkod** backend to achieve such a translation to SAT.\n",
+ "- Kodkod (https://github.com/emina/kodkod) is the API to the **Alloy** (http://alloytools.org) constraint analyzer and takes relational logic predicates and translates them to SAT.\n",
+ "- The SAT problem can be solved by any SAT solver (Sat4J, minisat, glucose,...).\n",
+ "- ProB translates parts of B to the Kodkod API and translates the results back to B values.\n",
+ "- Prior to the translation, ProB performs an interval analysis to determine possible ranges for the integer decision variables.\n",
+ "\n",
+ "The details were presented at FM'2012 (Plagge, L.).\n",
+ "\n",
+ ""
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 46,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = 2$\n",
+ "* $y = 0$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 2\n",
+ "\ty = 0"
+ ]
+ },
+ "execution_count": 46,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve kodkod x:0..2 & y:0..2 & x+y=2"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "We can find all solutions and check that we find exactly the three expected solutions:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 47,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $res = \\{(0\\mapsto2),(1\\mapsto1),(2\\mapsto0)\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tres = {(0↦2),(1↦1),(2↦0)}"
+ ]
+ },
+ "execution_count": 47,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve kodkod {x,y|x:0..2 & y:0..2 & x+y=2}=res"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "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 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",
+ "- mk_op(greater_equal,2,4) $\\rightarrow$ 5\n",
+ "- mk_int_const(2) $\\rightarrow$ 6\n",
+ "- mk_op(greater_equal,6,2) $\\rightarrow$ 7\n",
+ "- mk_int_const(0) $\\rightarrow$ 8\n",
+ "- mk_op(greater_equal,3,8) $\\rightarrow$ 9\n",
+ "- mk_int_const(2) $\\rightarrow$ 10\n",
+ "- mk_op(greater_equal,10,3) $\\rightarrow$ 11\n",
+ "- mk_op(add,2,3) $\\rightarrow$ 12\n",
+ "- mk_int_const(2) $\\rightarrow$ 13\n",
+ "- mk_op(equal,12,13) $\\rightarrow$ 14\n",
+ "- mk_op_arglist(conjunct,[5,7,9,11,14]) $\\rightarrow$ 15"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 48,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = 0$\n",
+ "* $y = 2$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 0\n",
+ "\ty = 2"
+ ]
+ },
+ "execution_count": 48,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve z3 x:0..2 & y:0..2 & x+y=2"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "#### ProB's CLP(FD) Solver ####\n",
+ "ProB's default solver makes use of constraint logic programming.\n",
+ "For arithmetic, it builts on top of CLP(FD), the finite domain library of SICStus Prolog.\n",
+ "In CLP(FD):\n",
+ "- every integer variable is associated with a domain of possible values, typically an interval\n",
+ "- when adding a new constraints, the domains of the involved variables are updated, or more precisely narrowed down.\n",
+ "- at some point we need to chose variables for enumeration; typically ProB chooses the value with the smallest domain.\n",
+ "\n",
+ "Let us use a slightly adapted constraint ```x:0..9 & y:0..9 & x+y=2``` to illustrate how constraint processing works:\n",
+ "\n",
+ "- x:0..9 $\\leadsto$ x:0..9, y:$-\\infty$..$\\infty$\n",
+ "- y:0..9 $\\leadsto$ x:0..9, y:0..9\n",
+ "- x+y=2 $\\leadsto$ x:0..2, y:0..2\n",
+ "- Enumerate (label) variable x\n",
+ " - x=0 $\\leadsto$ x:0..0, y:2..2\n",
+ " - x=1 $\\leadsto$ x:1..1, y:1..1\n",
+ " - 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": 34,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.213287097 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.213287097 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{P} = 4$\n",
+ "* $\\mathit{A} = 1$\n",
+ "* $\\mathit{S} = 3$\n",
+ "* $\\mathit{I} = 0$\n",
+ "* $\\mathit{K} = 2$\n",
+ "* $\\mathit{N} = 9$\n",
+ "* $\\mathit{O} = 8$"
+ ],
+ "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": 34,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":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": 35,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "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"
+ ]
+ }
+ ],
+ "source": [
+ ":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": 36,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "ProBError",
+ "evalue": "ProB reported Errors\nProB returned error messages:\nWarning: Kodkod SAT Solver Timeout for Problem Id: 0",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m",
+ "\u001b[1m\u001b[31mWarning: Kodkod SAT Solver Timeout for Problem Id: 0\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ ":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": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Result for KISS*KISS=PASSION puzzle:\n",
+ "\n",
+ "Solver | Runtime\n",
+ "-------|-------\n",
+ "ProB Default | 0.01 sec\n",
+ "Kodkod Backend | 1 sec\n",
+ "Z3 Backend | ? > 100 sec"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "### Unbounded integers ###\n",
+ "The SAT translation via Kodkod/Alloy requires to determine the bid width.\n",
+ "It cannot be applied to unbounded integers.\n",
+ "Even for bounded integers it is quite tricky to get the bid widths correct: one needs also to take care of intermediate results. Alloy can detect incorrect models where an overflow occured, but to our understanding not where an overflow prevented a model (e.g., use inside negation or equivalence, see ```#(V.SS->V.SS)=0 iff no V.SS``` in paper at ABZ conference).\n",
+ "\n",
+ "SMTLib is more tailored towards proof than towards model finding; as such it has typically no/less issues with unbounded values.\n",
+ "The ProB default solver can also deal with unbounded integers: it tries to narrow down domains to finite ones. If this fails, an unbounded variable is enumerated (partially) and an **enumeration warning** is generated. In case a solution is found, this warning is ignored, otherwise the result of ProB's analysis is **UNKNOWN**.\n",
+ "Some inconsistencies cannot be detected by interval/domain propagation; here it helps to activate ProB's CHR module which performs some additional inferences.\n",
+ "\n",
+ "Let us perform some experiments. Both ProB and Z3 can solve the following:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 52,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = -10$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = −10"
+ ]
+ },
+ "execution_count": 52,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve z3 x*x=100"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Here is an example where ProB generates an enumeration warning, but finds a solution:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 53,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = 6001$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 6001"
+ ]
+ },
+ "execution_count": 53,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x>100 & x mod 2000 = 1 & x mod 3000 = 1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 54,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = 6001$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 6001"
+ ]
+ },
+ "execution_count": 54,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve z3 x>100 & x mod 2000 = 1 & x mod 3000 = 1"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Here ProB generates an enumeration warning and does not find a solution, hence the result is **UNKNOWN**. Here Z3 finds a solution."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 55,
+ "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 prob x>100 & x mod 2000 = 1 & x mod 3000 = 1 & (x+x) mod 4501 = 0"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 56,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = 6756001$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 6756001"
+ ]
+ },
+ "execution_count": 56,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve z3 x>100 & x mod 2000 = 1 & x mod 3000 = 1 & (x+x) mod 4501 = 0"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "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**."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 57,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$FALSE$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 57,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve z3 x>y & y>x"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 58,
+ "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 prob x>y &y>x"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "### Summary for Integer Arithmetic ###\n",
+ "\n",
+ "Solver | Unbounded | Model Finding | Inconsistency Detection (Unbounded)\n",
+ "------|------------|---------------|---\n",
+ "ProB CLP(FD) | yes | very good | limited with CHR\n",
+ "ProB Z3 | yes | reasonable | very good\n",
+ "ProB Kodkod | no | good | -\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "## Set Constraints ##\n",
+ "\n",
+ "After booleans, integers and enumerated set elements, let us now move to constraint solving involving set variables.\n",
+ "\n",
+ "### Translation to SAT ###\n",
+ "The Kodkod/Alloy backend translates sets bit vectors. The size of the vector is the number of possible elements.\n",
+ "\n",
+ "Take for example the following constraint:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 60,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = \\{1\\}$\n",
+ "* $y = \\{1,2\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = {1}\n",
+ "\ty = {1,2}"
+ ]
+ },
+ "execution_count": 60,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "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": 61,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $y1 = TRUE$\n",
+ "* $x1 = TRUE$\n",
+ "* $y2 = TRUE$\n",
+ "* $x2 = FALSE$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\ty1 = TRUE\n",
+ "\tx1 = TRUE\n",
+ "\ty2 = TRUE\n",
+ "\tx2 = FALSE"
+ ]
+ },
+ "execution_count": 61,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x1,x2,y1,y2} <: BOOL &\n",
+ " x1=TRUE or y1=TRUE & x2=TRUE or y2=TRUE & // x \\/ y = 1..2\n",
+ " x1=TRUE & // 1:x \n",
+ " (x1=TRUE => y1=TRUE) & (x2=TRUE => y2=TRUE) & (x1/=y1 or x2/=y2) // x <<: y"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 62,
+ "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": 62,
+ "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": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "This translation to SAT is exactly what the Kodkod backend does:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 63,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = \\{1\\}$\n",
+ "* $y = \\{1,2\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = {1}\n",
+ "\ty = {1,2}"
+ ]
+ },
+ "execution_count": 63,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve kodkod x <: 1..2 & y<: 1..2 & x \\/ y = 1..2 & 1:x & x <<: y"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Limitations of translating set constraints to SAT:\n",
+ "- this cannot deal with **unbounded** sets: we need to know a finite type for each set, so that we can generate a finite bit vector\n",
+ "- this approach cannot usually deal with **higher order** sets (sets of sets), as the size of the bit vector would be prohibitively large\n",
+ "\n",
+ "Given that:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 64,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1267650600228229401496703205376$"
+ ],
+ "text/plain": [
+ "1267650600228229401496703205376"
+ ]
+ },
+ "execution_count": 64,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "card(POW(1..100))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "translating the following constraint to SAT would require a bit vector of length 1267650600228229401496703205376."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 65,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = \\{\\{100\\},\\{1\\}\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = {{100},{1}}"
+ ]
+ },
+ "execution_count": 65,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x <: POW(1..100) & {100}:x & !y.(y:x => {card(y)}:x)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "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)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 66,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = \\{\\{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\\}\\}$"
+ ],
+ "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": 66,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{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": 67,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.097977646 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.097977646 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $r = \\{(3\\mapsto5),(3\\mapsto4),(5\\mapsto5),(5\\mapsto4),(1\\mapsto4),(2\\mapsto4),(4\\mapsto4)\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tr = {(3↦5),(3↦4),(5↦5),(5↦4),(1↦4),(2↦4),(4↦4)}"
+ ]
+ },
+ "execution_count": 67,
+ "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": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "### Translation to SMTLib ###\n",
+ "\n",
+ "This can in principle deal with higher-order sets and unbounded sets, but makes heavy use of quantifiers.\n",
+ "The practical usefulness is currently very limited."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 68,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = \\emptyset$\n",
+ "* $y = \\{1,2\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = ∅\n",
+ "\ty = {1,2}"
+ ]
+ },
+ "execution_count": 68,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve z3 x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Internally, the constraint is rewritten to support operators which do not exist in SMTLib:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 69,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = \\emptyset$\n",
+ "* $y = \\{1,2\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = ∅\n",
+ "\ty = {1,2}"
+ ]
+ },
+ "execution_count": 69,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "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",
+ "x ∪ y = {1,2}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "This in turn gets translated to SMTLib (calls to the Z3 API):\n",
+ "- mk_var(set(integer),x) $\\rightarrow$ 2\n",
+ "- mk_var(set(integer),y) $\\rightarrow$ 3\n",
+ "- mk_bounded_var(integer,_smt_tmp28) $\\rightarrow$ 4\n",
+ "- mk_op(member,4,2) $\\rightarrow$ 5\n",
+ "- mk_int_const(1) $\\rightarrow$ 6\n",
+ "- mk_op(greater_equal,4,6) $\\rightarrow$ 7\n",
+ "- mk_int_const(2) $\\rightarrow$ 8\n",
+ "- mk_op(greater_equal,8,4) $\\rightarrow$ 9\n",
+ "- mk_op_arglist(conjunct,[7,9]) $\\rightarrow$ 10\n",
+ "- mk_op(implication,5,10) $\\rightarrow$ 11\n",
+ "- mk_quantifier(forall,[4],11) $\\rightarrow$ 12\n",
+ "- mk_bounded_var(integer,_smt_tmp29) $\\rightarrow$ 13\n",
+ "- mk_op(member,13,3) $\\rightarrow$ 14\n",
+ "- mk_int_const(1) $\\rightarrow$ 15\n",
+ "- mk_op(greater_equal) $\\rightarrow$ 13,15,16\n",
+ "- mk_int_const(2) $\\rightarrow$ 17\n",
+ "- mk_op(greater_equal,17,13) $\\rightarrow$ 18\n",
+ "- mk_op_arglist(conjunct,[16,18]) $\\rightarrow$ 19\n",
+ "- mk_op(implication,14,19) $\\rightarrow$ 20\n",
+ "- mk_quantifier(forall,[13],20) $\\rightarrow$ 21\n",
+ "- mk_op(union,2,3) $\\rightarrow$ 22\n",
+ "- mk_int_const(1) $\\rightarrow$ 23\n",
+ "- mk_int_const(2) $\\rightarrow$ 24\n",
+ "- mk_set([23,24]) $\\rightarrow$ 25\n",
+ "- mk_op(equal,22,25) $\\rightarrow$ 26\n",
+ "- mk_op_arglist(conjunct,[12,21,26]) $\\rightarrow$ 27"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "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:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 70,
+ "metadata": {},
+ "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"
+ ]
+ }
+ ],
+ "source": [
+ ":solve z3 x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 & 1∈x & x ⊂ y"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Let us look at another relatively simple example which poses problems:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 71,
+ "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}]"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "To understand why this simple constraint cannot be solved, we have to know how the translation works:\n",
+ "The relational inverse gets translated into two universal quantifications for SMTLib:\n",
+ "```\n",
+ " x = y~\n",
+ "<=>\n",
+ " !(st11,st12).(st11 |-> st12 : x => st12 |-> st11 : y) & \n",
+ " !(st11,st12).(st12 |-> st11 : y => st11 |-> st12 : x))\n",
+ "```\n",
+ "Similarly, r = f[s] is translated as follows:\n",
+ "```\n",
+ " r = f[s]\n",
+ "<=>\n",
+ " !st27.(st27 : r => #st26.(st26 |-> st27 : f & st26 : s) & \n",
+ " !st27.(#st26.(st26 |-> st27 : f & st26 : s) => st27 : r)\n",
+ "```\n",
+ "The resulting predicate (without the inverse and image operators) is the following, which Z3 cannot solve (but ProB can)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 72,
+ "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": 72,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint f = {(1|->3),(2|->6)} &\n",
+ "#st13.(r = st13 & (\n",
+ " !st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 & \n",
+ " (!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) & \n",
+ " !(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) & \n",
+ " !st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) &\n",
+ " !(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 73,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.058100600 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.058100600 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $r = \\{2\\}$\n",
+ "* $f = \\{(1\\mapsto3),(2\\mapsto6)\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tr = {2}\n",
+ "\tf = {(1↦3),(2↦6)}"
+ ]
+ },
+ "execution_count": 73,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":time :solve prob f = {(1|->3),(2|->6)} &\n",
+ "#st13.(r = st13 & (\n",
+ " !st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 & \n",
+ " (!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) & \n",
+ " !(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) & \n",
+ " !st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) &\n",
+ " !(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 74,
+ "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"
+ ]
+ }
+ ],
+ "source": [
+ ":time :solve cvc4 f = {(1|->3),(2|->6)} &\n",
+ "#st13.(r = st13 & (\n",
+ " !st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 & \n",
+ " (!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) & \n",
+ " !(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) & \n",
+ " !st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) &\n",
+ " !(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "The SMTLib translation is still of limited value for finding models.\n",
+ "However, for finding inconsistencies it is much better and can detect certain inconsistencies which ProB's solver cannot.\n",
+ "While both ProB and Z3 can solve the following:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 75,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$FALSE$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 75,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve prob x:s1 & x:s2 & x /: (s1 /\\ s2) & s1 <: INTEGER"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "only the Z3 backend can solve this one:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 76,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$FALSE$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 76,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve z3 x:s1 & x/:s2 & x /: (s1 \\/s2) & s1 <: INTEGER"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "### ProB's Set Solver ###\n",
+ "ProB has actually three set representations:\n",
+ "- Prolog lists of elements\n",
+ "- AVL trees for fully known sets\n",
+ "- symbolic closures for large or infinite sets\n",
+ "\n",
+ "For finite sets, the AVL tree representation is the most efficient and allows for efficient lookups.\n",
+ "It, however, requires all elements to be fully known.\n",
+ "\n",
+ "The symbolic closure can be used for large or infinite sets.\n",
+ "ProB will automatically use it for sets it knows to be infinite, or when an enumeration warning occurs during an attempt at expanding a set.\n",
+ "\n",
+ "The list representation is used for sets where some of the members are known or partially known.\n",
+ "\n",
+ "#### AVL tree representation ####\n",
+ "The following generates the AVL tree representation:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 77,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{0,100,200,300,400,500,600,700,800,900,1000\\}$"
+ ],
+ "text/plain": [
+ "{0,100,200,300,400,500,600,700,800,900,1000}"
+ ]
+ },
+ "execution_count": 77,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x|x∈0..2**10 & x mod 100 = 0}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "A lot of operators and predicates have optimised versions for the AVL tree represenation, e.g.,"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 78,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $mn = 0$\n",
+ "* $s = \\{0,100,200,300,400,500,600,700,800,900,1000\\}$\n",
+ "* $mx = 1000$"
+ ],
+ "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": 78,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "s = {x|x∈0..2**10 & x mod 100 = 0} &\n",
+ "mx = max(s) &\n",
+ "mn = min(s)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "#### Symbolic closure representation ####\n",
+ "\n",
+ "In the following case, ProB knows that the set is infinite and is kept symbolic:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 37,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{x}\\mid \\mathit{x} > 1000\\}$"
+ ],
+ "text/plain": [
+ "{x∣x > 1000}"
+ ]
+ },
+ "execution_count": 37,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x|x>1000}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Symbolic sets can be used in various ways:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 38,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{inf} = \\{\\mathit{x}\\mid \\mathit{x} > 1000\\}$\n",
+ "* $\\mathit{res} = (1001 \\ldots 1100)$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tinf = {x∣x > 1000}\n",
+ "\tres = (1001 ‥ 1100)"
+ ]
+ },
+ "execution_count": 38,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "inf = {x|x>1000} & 1024 : inf & not(1000:inf) & res = (900..1100) ∩ inf"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "For the following set, ProB tries to expand it and then an enumeration warning occurs (also called a **virtual timeout**, ProB realises that no matter what time budget it would be given a timeout would occur).\n",
+ "The set is then kept symbolic and can again be used in various ways."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 39,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\newcommand{\\binter}{\\mathbin{\\mkern1mu\\cap\\mkern1mu}}\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{inf} = \\{\\mathit{x}\\mid \\mathit{x} > 1000 \\land \\mathit{x} \\mathit{mod} 25 = 0\\}$\n",
+ "* $\\mathit{res} = ((900 \\ldots 1100) \\binter \\{\\mathit{x}\\mid \\mathit{x} > 1000 \\land \\mathit{x} \\mathit{mod} 25 = 0\\})$"
+ ],
+ "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": 39,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "inf = {x|x>1000 & x mod 25 = 0} & 1025 ∈ inf & not(1000∈inf) & res = (900..1100) ∩ inf"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "The virtual timeout message can be removed (and performance improved) by adding the symbolic pragma:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 40,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\newcommand{\\binter}{\\mathbin{\\mkern1mu\\cap\\mkern1mu}}\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{inf} = \\{\\mathit{x}\\mid \\mathit{x} > 1000 \\land \\mathit{x} \\mathit{mod} 25 = 0\\}$\n",
+ "* $\\mathit{res} = ((900 \\ldots 1100) \\binter \\{\\mathit{x}\\mid \\mathit{x} > 1000 \\land \\mathit{x} \\mathit{mod} 25 = 0\\})$"
+ ],
+ "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": 40,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "inf = /*@symbolic*/ {x|x>1000 & x mod 25 = 0} & 1025 ∈ inf & not(1000∈inf) & res = (900..1100) ∩ inf"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Internally, a symbolic representation is a **closure** in functional programming terms: all dependent variables are *compiled* into the closure: the closure can be passed as a value and evaluated without needing access to an environment. In Prolog this is represented as a tuple:\n",
+ "- closure(Parameters,Types,CompiledPredicate)\n",
+ "For example, a set {x|x>v} where v has the value 17 is compiled to:\n",
+ "- closure([x],[integer],```x>17```)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "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"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 83,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $vec = \\{(1\\mapsto1),(2\\mapsto2),(3\\mapsto4),(4\\mapsto8),(5\\mapsto16),(6\\mapsto32),(7\\mapsto64),(8\\mapsto128),(9\\mapsto256),(10\\mapsto512)\\}$"
+ ],
+ "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": 83,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "vec: 1..10 --> 0..9999 &\n",
+ "vec(1) : {1,10} &\n",
+ "!x.(x:2..10 => vec(x) = vec(x-1)*2)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Note that Kodkod translation and SMT translation not very effective for the above.\n",
+ "The Kodkod translation can deal with a simpler version of the above:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 84,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 2.542529935 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 2.542529935 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $vec = \\{(3\\mapsto4),(5\\mapsto16),(6\\mapsto32),(7\\mapsto64),(1\\mapsto1),(2\\mapsto2),(4\\mapsto8),(8\\mapsto128)\\}$"
+ ],
+ "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": 84,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "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": 85,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.016755497 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.016755497 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $vec = \\{(1\\mapsto1),(2\\mapsto2),(3\\mapsto4),(4\\mapsto8),(5\\mapsto16),(6\\mapsto32),(7\\mapsto64),(8\\mapsto128)\\}$"
+ ],
+ "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": 85,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "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": 86,
+ "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"
+ ]
+ }
+ ],
+ "source": [
+ ":time :solve z3 vec: 1..8 --> 0..199 & vec(1) : {1,10} & !x.(x:2..8 => vec(x) = vec(x-1)*2)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "### ProB's Solving Algorithm ###\n",
+ "\n",
+ "ProB tries to accomplish several conflicting goals:\n",
+ "- being able to deal with concrete data, i.e., sets and relations containing thousands or hundreds of thousands of elementas\n",
+ "- being able to deal with symbolic, infinite sets, relations and functions.\n",
+ "- being able to perform efficient computation over large data as well as constraint solving\n",
+ "\n",
+ "For example, efficient computation over large concrete data is the following:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 42,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.266020568 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.266020568 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{s3} = \\exists 500\\in\\{20,40,\\0xpto,9980,10000\\}$\n",
+ "* $\\mathit{n} = 4$\n",
+ "* $\\mathit{s1} = \\exists 2500\\in\\{4,8,\\0xpto,9996,10000\\}$\n",
+ "* $\\mathit{s2} = \\exists 2000\\in\\{5,10,\\0xpto,9995,10000\\}$"
+ ],
+ "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": 42,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "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"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Here is a simple verison of the above"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 88,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.014582494 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.014582494 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $xy = \\exists201\\in\\{1,2,\\0xpto,299,300\\}$\n",
+ "* $x = (1 \\ldots 100)$\n",
+ "* $y = (200 \\ldots 300)$\n",
+ "* $n = 100$"
+ ],
+ "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": 88,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":time :solve prob x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 89,
+ "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"
+ ]
+ }
+ ],
+ "source": [
+ ":solve z3 x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 90,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.546787958 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.546787958 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $xy = \\{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,\\0xpto\\}$\n",
+ "* $x = \\{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",
+ "* $y = \\{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",
+ "* $n = 100$"
+ ],
+ "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": 90,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":time :solve kodkod x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "In the appendix there are more examples which analyse the performance for such examples."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "ProB employs the *Andorra* principle: deterministic computations are done first.\n",
+ "As there are multiple set representations, there are actually two kinds of deterministic computations:\n",
+ "- deterministic computations that generate an efficient representation, e.g., an AVL set representation\n",
+ "- and other deterministic computations\n",
+ "\n",
+ "The ProB solver has a **WAITFLAG store** where choice points and enumerations are registered with a given priority.\n",
+ "- Priority 0 means that an efficient representation can be generated\n",
+ "- Priority 1 is a deterministic computation not guaranteed to produce an efficient representation\n",
+ "- Priority k is a choice point/enumeration which may generate k possible values\n",
+ "\n",
+ "At each solving step one waitflag is activated, the one with the lowest priority.\n",
+ "CLP(FD) variables are also registered in the WAITFLAG store and are enumerated before a waitflag of the same priority is activated. For tie breaking one typically uses the **most attached constraints first** (ffc) heuristic.\n",
+ "\n",
+ "#### Example ####\n",
+ "Let us examine how ```x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y``` is solved.\n",
+ "- all constraints are registered\n",
+ "- in phase 0 ```n=100``` is run\n",
+ "- this means that ```1..n``` can be efficiently computed\n",
+ "- this means that ```x = 1..n``` triggers in phase 0\n",
+ "- then ```2*n``` and ```3*n``` can be computed, followed by ```2*n..3*n```\n",
+ "- this means that ```y = 2*n..3*n``` triggers in phase 0\n",
+ "- again, this means that ```x \\/ y``` can be efficiently computed\n",
+ "- finally ```xy = x \\/ y``` can be executed in phase 0\n",
+ "\n",
+ "No enumeration was required. In this case ProB's constraint solver works similar to a topological sorting algorithm.\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "#### Dealing with unbounded enumeration ####\n",
+ "\n",
+ "Note: if an unbounded enumeration is encountered, the solver registers an **enumeration warning** in the current scope (every quantification / comprehension set results in a new inner scope). Depending on the kind of scope (existential/universal) and on whether a solution is found, the warning gets translated into an **UNKNOWN** result."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "### Functional Programming ###\n",
+ "\n",
+ "Some functions are automatically detected as infinite by ProB, are kept symbolic but can be applied in several ways:\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 91,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $r2 = \\{1,4,9,16,25,36,49,64,81,100\\}$\n",
+ "* $r3 = [4,9,25,49,121]$\n",
+ "* $r4 = 256$\n",
+ "* $sqrt = 10$\n",
+ "* $f = \\lambdax\\qdot(x \\in INTEGER\\midx * x)$\n",
+ "* $r1 = 10000000000$"
+ ],
+ "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": 91,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "f = %x.(x:INTEGER|x*x) &\n",
+ "r1 = f(100000) &\n",
+ "r2 = f[1..10] &\n",
+ "r3 = ([2,3,5,7,11] ; f) &\n",
+ "r4 = iterate(f,3)(2) &\n",
+ "f(sqrt) = 100"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 92,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $r2 = \\{1,2,3,4\\}$\n",
+ "* $r3 = [2,2,3,3,4]$\n",
+ "* $r4 = 2$\n",
+ "* $r5 = \\{2,4,10,100\\}$\n",
+ "* $sqr = 9802$\n",
+ "* $f = \\{x,y\\midx \\in NATURAL \\land y \\cprod 2 \\geq x \\land (y - 1) \\cprod 2 < x\\}$\n",
+ "* $r1 = 317$"
+ ],
+ "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": 92,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "f = {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function\n",
+ "r1 = f(100000) &\n",
+ "r2 = f[1..10] &\n",
+ "r3 = ([2,3,5,7,11] ; f) &\n",
+ "r4 = iterate(f,3)(2) &\n",
+ "f(sqr) = 100 &\n",
+ "r5 = closure1(f)[{10000}]"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "### Reification ###\n",
+ "\n",
+ "Reification is linking the truth value of a constraint with a boolean variable.\n",
+ "ProB's kernel provides support for reifying a considerable number of constraints (but not yet all!).\n",
+ "Reification is important for efficiency, to avoid choice points and is important to link various solvers of ProB (set, arithmetic, boolean,...).\n",
+ ""
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 93,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = 125$\n",
+ "* $ReifVar = TRUE$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 125\n",
+ "\tReifVar = TRUE"
+ ]
+ },
+ "execution_count": 93,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(x>100 <=> (ReifVar=TRUE)) & (x<125 <=> (ReifVar=FALSE)) & x<200"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ ""
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "### Relation to SETLOG ###\n",
+ "\n",
+ "Setlog (http://people.dmi.unipr.it/gianfranco.rossi/setlog.Home.html) is based on non-deterministic set unification\n",
+ "Setlog has additional inference rules\n",
+ "\n",
+ "The former causes problems with larger sets, in our experience.\n",
+ "The latter could be added to ProB via CHR, but currently not done.\n",
+ "\n",
+ "Let us look at a simpler Setlog example from the article \"{log} as a Test Case Generator\n",
+ "for the Test Template Framework\" by Cristia, Rossi and Frydman:\n",
+ "```\n",
+ "1 in R & 1 nin S & inters(R,S,T) & T = {X}\n",
+ "```\n",
+ "This can be encoded in B as follows:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 94,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $R = \\{1,0\\}$\n",
+ "* $S = \\{0\\}$\n",
+ "* $T = \\{0\\}$\n",
+ "* $X = 0$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tR = {1,0}\n",
+ "\tS = {0}\n",
+ "\tT = {0}\n",
+ "\tX = 0"
+ ]
+ },
+ "execution_count": 94,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1:R & 1/:S & R/\\S=T & T={X}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Another example from that paper is\n",
+ "```\n",
+ "X in int(1,5) & Y in int(4,10) & inters({X},{Y},R) & X >= Y\n",
+ "```\n",
+ "which has three solutions\n",
+ "```\n",
+ "X=4,Y=4,R={4}; X=5,Y=5,R={5}; X=5,Y=4,R={}.\n",
+ "```\n",
+ "Let us check this with ProB:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 95,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{((4\\mapsto4)\\mapsto\\{4\\}),((5\\mapsto4)\\mapsto\\emptyset),((5\\mapsto5)\\mapsto\\{5\\})\\}$"
+ ],
+ "text/plain": [
+ "{((4↦4)↦{4}),((5↦4)↦∅),((5↦5)↦{5})}"
+ ]
+ },
+ "execution_count": 95,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{X,Y,R|X: 1..5 & Y: 4..10 & {X}/\\{Y}=R & X>=Y}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "However, in particular with unbounded sets Setlog can solve some constraints that ProB, Z3 and Kodkod cannot:\n",
+ "```\n",
+ "un(A,B,D) & disj(A,C) & D=C & ris(X in A,[],true,X) neq {}\n",
+ "```\n",
+ "In B this corresponds to:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 96,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":eval: UNKNOWN (FALSE with enumeration warning)",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:eval: UNKNOWN (FALSE with enumeration warning)\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ "A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(STRING)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "From A\\/B=D we and D=C we could infer A<:C and hence A/\\C=C and hence A={} which is in conflict with A/={}.\n",
+ "ProB (as well as Kodkod and Z3 backends) can only infer the conflict for finite domains:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 97,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$FALSE$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 97,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(BOOL)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 98,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$FALSE$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 98,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve kodkod A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(BOOL)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 99,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$FALSE$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 99,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve z3 A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(BOOL)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Setlog has problems with larger sets. For example, the following takes 24 seconds using the latest stable release 4.9.1 of Setlog from http://people.dmi.unipr.it/gianfranco.rossi/setlog.Home.html: \n",
+ "```\n",
+ "{log}=> diff(int(1,200),{50},R).\n",
+ "\n",
+ "R = {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200}\n",
+ "\n",
+ "Another solution? (y/n)\n",
+ "```\n",
+ "In ProB this is instantenous:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 100,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.004239836 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.004239836 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $R = \\{1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tR = {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200}"
+ ]
+ },
+ "execution_count": 100,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":time R= (1..200) \\ {50}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Another example, for minimum of set from SETS'18 paper:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 101,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.014517786 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.014517786 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $S = \\{2,4,5,6,8,10\\}$\n",
+ "* $y = 2$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tS = {2,4,5,6,8,10}\n",
+ "\ty = 2"
+ ]
+ },
+ "execution_count": 101,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":time :solve prob S = {8,4,6,2,10,5} & y:S & S = {x|x:S & y<=x}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 102,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $S = \\{2,4,5,6,8,10\\}$\n",
+ "* $y = 2$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tS = {2,4,5,6,8,10}\n",
+ "\ty = 2"
+ ]
+ },
+ "execution_count": 102,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "S= {8,4,6,2,10,5} & y:S & !x.(x:S => y<=x)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "## Summary of Set Constraint Solving Approaches ##\n",
+ "\n",
+ "- SAT Translation (Kodkod backend): \n",
+ " - needs finite and small base type, no unbounded or higher-order sets\n",
+ " - can be very effective for complex constraints involving image, transitive closure,...\n",
+ " - limited performance for large sets\n",
+ "- SMTLib Translation (Z3/CVC4 backend):\n",
+ " - can deal with unbounded and large sets\n",
+ " - due to heavy use of quantifiers, some finite constraints get translated into infinite ones: limited model finding capabilities\n",
+ "- 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 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": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "## Appendix ##"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "### Explicit Computations ####\n",
+ "\n",
+ "What about explicit computations? How well does the SMTLib translation fare here?"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 103,
+ "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 x = 1..1000 /\\ (200..300)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 104,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.224425596 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.224425596 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = \\{6,7,8,9,10,11,12,13,14,15\\}$"
+ ],
+ "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"
+ }
+ ],
+ "source": [
+ ":time :solve z3 x = 1..40 /\\ (6..15)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 105,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 1.149180308 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 1.149180308 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = \\{6,7,8,9,10,11,12,13,14,15\\}$"
+ ],
+ "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"
+ }
+ ],
+ "source": [
+ ":time :solve z3 x = 1..60 /\\ (6..15)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 106,
+ "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"
+ ]
+ }
+ ],
+ "source": [
+ ":time :solve z3 x = 1..80 /\\ (6..15)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 107,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.005873811 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.005873811 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = (6 \\ldots 15)$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = (6 ‥ 15)"
+ ]
+ },
+ "execution_count": 107,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":time :solve prob x = 1..80 /\\ (6..15)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "In the following the inverse operator seems to pose problems to Z3:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 108,
+ "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 s1 = {2,3,5,7,11} & s2 = {4,8,16,32} & c = s1*s2 & r=c~[{8}]"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 109,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $r = \\{2,3,5,7,11\\}$\n",
+ "* $c = (\\{2,3,5,7,11\\} * \\{4,8,16,32\\})$\n",
+ "* $s1 = \\{2,3,5,7,11\\}$\n",
+ "* $s2 = \\{4,8,16,32\\}$"
+ ],
+ "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"
+ }
+ ],
+ "source": [
+ ":solve prob s1 = {2,3,5,7,11} & s2 = {4,8,16,32} & c = s1*s2 & r=c~[{8}]"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "### Benchmark Puzzles ####\n",
+ "\n",
+ "#### N-Queens ####\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 124,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.060237608 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.060237608 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $queens = \\{(1\\mapsto4),(2\\mapsto2),(3\\mapsto7),(4\\mapsto3),(5\\mapsto6),(6\\mapsto8),(7\\mapsto5),(8\\mapsto1)\\}$\n",
+ "* $n = 8$"
+ ],
+ "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"
+ }
+ ],
+ "source": [
+ ":time :solve prob n=8 &\n",
+ " queens : 1..n >-> 1..n &\n",
+ " !(q1,q2).(q1:1..n & q2:2..n & q2>q1 => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 125,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.393750784 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.393750784 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $queens = \\{(1\\mapsto4),(2\\mapsto7),(3\\mapsto5),(4\\mapsto2),(5\\mapsto6),(6\\mapsto1),(7\\mapsto3),(8\\mapsto8)\\}$\n",
+ "* $n = 8$"
+ ],
+ "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"
+ }
+ ],
+ "source": [
+ ":time :solve z3 n=8 &\n",
+ " queens : 1..n >-> 1..n &\n",
+ " !(q1,q2).(q1:1..n & q2:2..n & q2>q1 => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 126,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.467670114 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.467670114 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $queens = \\{(3\\mapsto2),(5\\mapsto5),(6\\mapsto1),(7\\mapsto8),(1\\mapsto3),(2\\mapsto6),(4\\mapsto7),(8\\mapsto4)\\}$\n",
+ "* $n = 8$"
+ ],
+ "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"
+ }
+ ],
+ "source": [
+ ":time :solve kodkod n=8 &\n",
+ " queens : 1..n >-> 1..n &\n",
+ " !(q1,q2).(q1:1..n & q2:2..n & q2>q1 => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 128,
+ "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"
+ ]
+ }
+ ],
+ "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",
+ " card(bshp) = 3"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Solving takes about 150 seconds; Kodkod translation currently does not work due to card and preventing overflows."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 129,
+ "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"
+ }
+ ],
+ "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",
+ " card(bshp) = 3"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "#### Datavalidation example ####\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 44,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: signals"
+ ]
+ },
+ "execution_count": 44,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE\n",
+ " signals\n",
+ "\n",
+ "SETS\n",
+ "/* Ensemble des signaux */\n",
+ " \tSIGNAL =\n",
+ " \t{ PL01\n",
+ " \t, PL02\n",
+ " \t, PL03\n",
+ " \t, PL04\n",
+ " \t, PL05\n",
+ " \t, PL06\n",
+ " \t, PL07\n",
+ " \t, PL08\n",
+ " \t, PL09\n",
+ " \t, PL10\n",
+ " \t, PL11\n",
+ " \t, PL12\n",
+ "\t,\t PL13\n",
+ " \t, PL14\n",
+ " \t, PL15\n",
+ " \t, PL16\n",
+ " \t, PL17\n",
+ " \t, PL18\n",
+ " \t, PL19\n",
+ " \t, PL20\n",
+ " \t}\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 45,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.199987519 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.199987519 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{res} = \\{\\mathit{PL01},\\mathit{PL12}\\}$\n",
+ "* $\\mathit{nxt} = \\{(\\mathit{PL01}\\mapsto \\mathit{PL02}),(\\mathit{PL02}\\mapsto \\mathit{PL03}),(\\mathit{PL03}\\mapsto \\mathit{PL04}),(\\mathit{PL04}\\mapsto \\mathit{PL05}),(\\mathit{PL05}\\mapsto \\mathit{PL06}),(\\mathit{PL06}\\mapsto \\mathit{PL07}),(\\mathit{PL07}\\mapsto \\mathit{PL08}),(\\mathit{PL08}\\mapsto \\mathit{PL09}),(\\mathit{PL09}\\mapsto \\mathit{PL10}),(\\mathit{PL10}\\mapsto \\mathit{PL11}),(\\mathit{PL11}\\mapsto \\mathit{PL11}),(\\mathit{PL12}\\mapsto \\mathit{PL13}),(\\mathit{PL13}\\mapsto \\mathit{PL14}),(\\mathit{PL14}\\mapsto \\mathit{PL15}),(\\mathit{PL15}\\mapsto \\mathit{PL16}),(\\mathit{PL16}\\mapsto \\mathit{PL17}),(\\mathit{PL17}\\mapsto \\mathit{PL18}),(\\mathit{PL18}\\mapsto \\mathit{PL19}),(\\mathit{PL19}\\mapsto \\mathit{PL20}),(\\mathit{PL20}\\mapsto \\mathit{PL20})\\}$"
+ ],
+ "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": 45,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":time :solve prob nxt = \n",
+ " {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n",
+ " PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09,\n",
+ " PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL11, PL12 |-> PL13,\n",
+ " PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17,\n",
+ " PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20} &\n",
+ " res = SIGNAL \\ nxt[SIGNAL]"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 46,
+ "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"
+ ]
+ }
+ ],
+ "source": [
+ ":time :solve z3 nxt = \n",
+ " {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n",
+ " PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09,\n",
+ " PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL11, PL12 |-> PL13,\n",
+ " PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17,\n",
+ " PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20} &\n",
+ " res = SIGNAL \\ nxt[SIGNAL]"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 47,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.789322780 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.789322780 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{res} = \\{\\mathit{PL01},\\mathit{PL12}\\}$\n",
+ "* $\\mathit{nxt} = \\{(\\mathit{PL01}\\mapsto \\mathit{PL02}),(\\mathit{PL02}\\mapsto \\mathit{PL03}),(\\mathit{PL03}\\mapsto \\mathit{PL04}),(\\mathit{PL04}\\mapsto \\mathit{PL05}),(\\mathit{PL05}\\mapsto \\mathit{PL06}),(\\mathit{PL06}\\mapsto \\mathit{PL07}),(\\mathit{PL07}\\mapsto \\mathit{PL08}),(\\mathit{PL08}\\mapsto \\mathit{PL09}),(\\mathit{PL09}\\mapsto \\mathit{PL10}),(\\mathit{PL10}\\mapsto \\mathit{PL11}),(\\mathit{PL11}\\mapsto \\mathit{PL11}),(\\mathit{PL12}\\mapsto \\mathit{PL13}),(\\mathit{PL13}\\mapsto \\mathit{PL14}),(\\mathit{PL14}\\mapsto \\mathit{PL15}),(\\mathit{PL15}\\mapsto \\mathit{PL16}),(\\mathit{PL16}\\mapsto \\mathit{PL17}),(\\mathit{PL17}\\mapsto \\mathit{PL18}),(\\mathit{PL18}\\mapsto \\mathit{PL19}),(\\mathit{PL19}\\mapsto \\mathit{PL20}),(\\mathit{PL20}\\mapsto \\mathit{PL20})\\}$"
+ ],
+ "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": 47,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":time :solve kodkod nxt = \n",
+ " {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n",
+ " PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09,\n",
+ " PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL11, PL12 |-> PL13,\n",
+ " PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17,\n",
+ " PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20} &\n",
+ " res = SIGNAL \\ nxt[SIGNAL]"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "celltoolbar": "Raw Cell Format",
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}