"# 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:"
"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 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",
"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:"
"{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",
"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```:"
" (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",
"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"
"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)."
"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."
"\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",
":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"
"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",
" - 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"
B provides the booleans, strings and integers as built-in datatypes. (Strings are not available in Event-B.)
%% Cell type:code id: tags:
``` prob
BOOL
```
%% Output
$\{\mathit{FALSE},\mathit{TRUE}\}$
{FALSE,TRUE}
%% Cell type:code id: tags:
``` prob
"this is a string"
```
%% Output
$\text{"this is a string"}$
"this is a string"
%% Cell type:code id: tags:
``` prob
1024
```
%% Output
$1024$
1024
%% Cell type:markdown id: tags:
Users can define their own datatype in a B machine.
One distinguishes between explicitly specified enumerated sets and deferred sets.
%% Cell type:code id: tags:
``` prob
::load
MACHINE MyBasicSets
SETS Trains = {thomas, gordon}; Points
END
```
%% Output
Loaded machine: MyBasicSets
%% Cell type:markdown id: tags:
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 id: tags:
``` prob
Points
```
%% Output
$\{\mathit{Points1},\mathit{Points2}\}$
{Points1,Points2}
%% Cell type:markdown id: tags:
### Pairs ###
B also has pairs of values, which can be written in two ways:
B provides many operators which return values, such as the usual arithmetic operators but also many operators for sets, relations and functions.
For example set union and set difference:
%% Cell type:code id: tags:
``` prob
(1..3 \/ 5..10) \ (2..6)
```
%% Output
$\{1,7,8,9,10\}$
{1,7,8,9,10}
%% Cell type:code id: tags:
``` prob
(1..3 ∪ 5..10) \ (2..6)
```
%% Output
$\{1,7,8,9,10\}$
{1,7,8,9,10}
%% Cell type:markdown id: tags:
The range of a relation or function:
%% Cell type:code id: tags:
``` prob
dom({(thomas↦1),(gordon↦2)})
```
%% Output
$\{thomas,gordon\}$
{thomas,gordon}
%% Cell type:markdown id: tags:
Function application:
%% Cell type:code id: tags:
``` prob
{(thomas↦1),(gordon↦2)} (thomas)
```
%% Output
$1$
1
%% Cell type:markdown id: tags:
Relational inverse (.~) and relational image .[.] :
%% Cell type:code id: tags:
``` prob
{(thomas↦1),(gordon↦2)}~[2..3]
```
%% Output
$\{\mathit{gordon}\}$
{gordon}
%% Cell type:markdown id: tags:
## Predicates
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 id: tags:
``` prob
2>3
```
%% Output
$FALSE$
FALSE
%% Cell type:code id: tags:
``` prob
3>2
```
%% Output
$TRUE$
TRUE
%% Cell type:markdown id: tags:
Within predicates you can use **open** variables, which are implicitly existentially quantified.
ProB will display the solution for the open variables, if possible.
%% Cell type:code id: tags:
``` prob
x*x=100
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = -10$
TRUE
Solution:
x = −10
%% Cell type:markdown id: tags:
We can find all solutions to a predicate by using the set comprehension notation.
Note that by this we turn a predicate into an expression.
%% Cell type:code id: tags:
``` prob
{x|x*x=100}
```
%% Output
$\{-10,10\}$
{−10,10}
%% Cell type:markdown id: tags:
### Substitutions ###
B also has a rich syntax for substitutions, aka statements.
For example ```x := x+1``` increments the value of x by 1.
We will not talk about substitutions in the rest of this presentation.
The major differences between classical B and Event-B lie in the area of substitutions, machine composition and refinement.
%% Cell type:markdown id: tags:
## Definition of Constraint Solving ##
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.
We have already solved the predicate ```x*x=100``` above, yielding the solution ```x=-10```.
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 id: tags:
## Constraint Solving Applications ##
Constraint solving has many applications in formal methods in general and B in particular.
%% Cell type:markdown id: tags:
#### Animation ####
It is required to animate implicit specifications.
Take for example an event
```
train_catches_up = any t1,t2,x where t1:dom(train_position) & t2:dom(train_position) &
train_position(t1) < train_position(t2) &
x:1..(train_position(t2)-train_position(t1)-1) then
train_position(t1) := train_position(t1)+x end
```
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:
{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
%% Cell type:code id: tags:
``` prob
{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
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{R} = 8$
* $\mathit{S} = 9$
* $\mathit{D} = 7$
* $\mathit{E} = 5$
* $\mathit{Y} = 2$
* $\mathit{M} = 1$
* $\mathit{N} = 6$
* $\mathit{O} = 0$
TRUE
Solution:
R = 8
S = 9
D = 7
E = 5
Y = 2
M = 1
N = 6
O = 0
%% Cell type:markdown id: tags:
We can find all solutions (to the unmodified puzzle) using a set comprehension and make sure that there is just a single solution:
Finally, a simple puzzle involving sets is to find a subset of numbers from 1..5 whose sum is 14:
%% Cell type:code id: tags:
``` prob
x <: 1..5 & SIGMA(y).(y:x|y)=14
```
%% Output
$TRUE$
**Solution:**
* $x = \{2,3,4,5\}$
TRUE
Solution:
x = {2,3,4,5}
%% Cell type:markdown id: tags:
## How to solve (set) constraints in B ##
We will now examine how one can perform constraint solving for B.
%% Cell type:markdown id: tags:
### Booleans ###
If we have only booleans, constraint solving is equivalent to SAT solving.
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.
(We do not translate to CNF also because of well-definedness issues.)
%% Cell type:markdown id: tags:
### Integers ###
Let us take the integer constraint ```x*x=100``` which we saw earlier.
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.
So, let us first look at some simpler constraints, where the domains of the variables are all bounded.
%% Cell type:markdown id: tags:
Let us look at the simple constraint ```X:0..3 & Y:0..3 & X+Y=2```.
As you can see there are three solutions for this constraint:
%% Cell type:code id: tags:
``` prob
{X,Y|X:0..3 & Y:0..3 & X+Y=2}
```
%% Output
$\{(0\mapsto2),(1\mapsto1),(2\mapsto0)\}$
{(0↦2),(1↦1),(2↦0)}
%% Cell type:markdown id: tags:
We will now study how such constraints can be solved.
%% Cell type:markdown id: tags:
#### Solving constraints by translating to SAT ####
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.
The number 2 is ```10``` in binary and we can represent X and Y each by two bits X0,X1 and Y0,Y1.
We can translate the addition to a propositional logic formula:
Bit1 | Bit0
-----|-----
X1 | X0
+ Y1 | Y0
|
Z1 | Z0
Let us find one solution to this constraint, by encoding addition using an additional carry bit ```CARRY0```:
(CARRY0=TRUE => (X1=FALSE & Y1=FALSE)) & // no overflow
(CARRY0=FALSE => (X1=FALSE or Y1=FALSE)) & // no overflow
Z0=FALSE & Z1=TRUE})
```
%% Output
|Nr|X0|X1|Y0|Y1|Z0|Z1|CARRY0|
|---|---|---|---|---|---|---|---|
|1|FALSE|FALSE|FALSE|TRUE|FALSE|TRUE|FALSE|
|2|FALSE|TRUE|FALSE|FALSE|FALSE|TRUE|FALSE|
|3|TRUE|FALSE|TRUE|FALSE|FALSE|TRUE|TRUE|
Nr X0 X1 Y0 Y1 Z0 Z1 CARRY0
1 FALSE FALSE FALSE TRUE FALSE TRUE FALSE
2 FALSE TRUE FALSE FALSE FALSE TRUE FALSE
3 TRUE FALSE TRUE FALSE FALSE TRUE TRUE
%% Cell type:markdown id: tags:
In ProB, we can use **Kodkod** backend to achieve such a translation to SAT.
- 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.
- The SAT problem can be solved by any SAT solver (Sat4J, minisat, glucose,...).
- ProB translates parts of B to the Kodkod API and translates the results back to B values.
- Prior to the translation, ProB performs an interval analysis to determine possible ranges for the integer decision variables.
The details were presented at FM'2012 (Plagge, L.).
%% Cell type:code id: tags:
``` prob
:solve kodkod x:0..2 & y:0..2 & x+y=2
```
%% Output
$TRUE$
**Solution:**
* $x = 2$
* $y = 0$
TRUE
Solution:
x = 2
y = 0
%% Cell type:markdown id: tags:
We can find all solutions and check that we find exactly the three expected solutions:
%% Cell type:code id: tags:
``` prob
:solve kodkod {x,y|x:0..2 & y:0..2 & x+y=2}=res
```
%% Output
$TRUE$
**Solution:**
* $res = \{(0\mapsto2),(1\mapsto1),(2\mapsto0)\}$
TRUE
Solution:
res = {(0↦2),(1↦1),(2↦0)}
%% Cell type:markdown id: tags:
#### Translation to SMTLib ####
At iFM'2016 we (Krings, L.) presented a translation to SMTLib format to use either the **Z3** or **CVC4** SMT solver.
Compared to the Kodkod backend, no translation to SAT is performed, SMTLib supports **integer** predicates and integer operators in the language.
%% Cell type:markdown id: tags:
Here is ProB's SMTLib/Z3 API calls for the constraint ``` X:0..3 & Y:0..3 & X+Y=2```:
1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7
```
%% Output
Execution time: 0.213287097 seconds
$\mathit{TRUE}$
**Solution:**
* $\mathit{P} = 4$
* $\mathit{A} = 1$
* $\mathit{S} = 3$
* $\mathit{I} = 0$
* $\mathit{K} = 2$
* $\mathit{N} = 9$
* $\mathit{O} = 8$
TRUE
Solution:
P = 4
A = 1
S = 3
I = 0
K = 2
N = 9
O = 8
%% Cell type:code id: tags:
``` prob
: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
```
%% Output
:time: :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
: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
```
%% Output
Error from ProB: ProB reported Errors
Warning: Kodkod SAT Solver Timeout for Problem Id: 0
%% Cell type:markdown id: tags:
Result for KISS*KISS=PASSION puzzle:
Solver | Runtime
-------|-------
ProB Default | 0.01 sec
Kodkod Backend | 1 sec
Z3 Backend | ? > 100 sec
%% Cell type:markdown id: tags:
### Unbounded integers ###
The SAT translation via Kodkod/Alloy requires to determine the bid width.
It cannot be applied to unbounded integers.
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).
SMTLib is more tailored towards proof than towards model finding; as such it has typically no/less issues with unbounded values.
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**.
Some inconsistencies cannot be detected by interval/domain propagation; here it helps to activate ProB's CHR module which performs some additional inferences.
Let us perform some experiments. Both ProB and Z3 can solve the following:
%% Cell type:code id: tags:
``` prob
:solve z3 x*x=100
```
%% Output
$TRUE$
**Solution:**
* $x = -10$
TRUE
Solution:
x = −10
%% Cell type:markdown id: tags:
Here is an example where ProB generates an enumeration warning, but finds a solution:
%% Cell type:code id: tags:
``` prob
x>100 & x mod 2000 = 1 & x mod 3000 = 1
```
%% Output
$TRUE$
**Solution:**
* $x = 6001$
TRUE
Solution:
x = 6001
%% Cell type:code id: tags:
``` prob
:solve z3 x>100 & x mod 2000 = 1 & x mod 3000 = 1
```
%% Output
$TRUE$
**Solution:**
* $x = 6001$
TRUE
Solution:
x = 6001
%% Cell type:markdown id: tags:
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 id: tags:
``` prob
:solve prob x>100 & x mod 2000 = 1 & x mod 3000 = 1 & (x+x) mod 4501 = 0
```
%% Output
:solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
:solve z3 x>100 & x mod 2000 = 1 & x mod 3000 = 1 & (x+x) mod 4501 = 0
```
%% Output
$TRUE$
**Solution:**
* $x = 6756001$
TRUE
Solution:
x = 6756001
%% Cell type:markdown id: tags:
Here is an inconsistency which cannot be detected by CLP(FD)'s interval propagation.
ProB can detect it with CHR (Constraint Handling Rules) enabled, but without the module the result is **UNKNOWN**.
%% Cell type:code id: tags:
``` prob
:solve z3 x>y & y>x
```
%% Output
$FALSE$
FALSE
%% Cell type:code id: tags:
``` prob
:solve prob x>y &y>x
```
%% Output
:solve: Computation not completed: no solution found (but one might exist)
%% Cell type:markdown id: tags:
### Summary for Integer Arithmetic ###
Solver | Unbounded | Model Finding | Inconsistency Detection (Unbounded)
------|------------|---------------|---
ProB CLP(FD) | yes | very good | limited with CHR
ProB Z3 | yes | reasonable | very good
ProB Kodkod | no | good | -
%% Cell type:markdown id: tags:
## Set Constraints ##
After booleans, integers and enumerated set elements, let us now move to constraint solving involving set variables.
### Translation to SAT ###
The Kodkod/Alloy backend translates sets bit vectors. The size of the vector is the number of possible elements.
Take for example the following constraint:
%% Cell type:code id: tags:
``` prob
x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 & 1:x & x ⊂ y
```
%% Output
$TRUE$
**Solution:**
* $x = \{1\}$
* $y = \{1,2\}$
TRUE
Solution:
x = {1}
y = {1,2}
%% Cell type:markdown id: tags:
| Element | x | y | x ∪ y |
| ------------- |-------------| -----| -----|
| 1 | x1 | y1 | x1 or y1
| 2 | x2 | y2 | x2 or y2 |
%% Cell type:code id: tags:
``` prob
{x1,x2,y1,y2} <: BOOL &
x1=TRUE or y1=TRUE & x2=TRUE or y2=TRUE & // x \/ y = 1..2
x1=TRUE & // 1:x
(x1=TRUE => y1=TRUE) & (x2=TRUE => y2=TRUE) & (x1/=y1 or x2/=y2) // x <<: y
This translation to SAT is exactly what the Kodkod backend does:
%% Cell type:code id: tags:
``` prob
:solve kodkod x <: 1..2 & y<: 1..2 & x \/ y = 1..2 & 1:x & x <<: y
```
%% Output
$TRUE$
**Solution:**
* $x = \{1\}$
* $y = \{1,2\}$
TRUE
Solution:
x = {1}
y = {1,2}
%% Cell type:markdown id: tags:
Limitations of translating set constraints to SAT:
- 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
- this approach cannot usually deal with **higher order** sets (sets of sets), as the size of the bit vector would be prohibitively large
Given that:
%% Cell type:code id: tags:
``` prob
card(POW(1..100))
```
%% Output
$1267650600228229401496703205376$
1267650600228229401496703205376
%% Cell type:markdown id: tags:
translating the following constraint to SAT would require a bit vector of length 1267650600228229401496703205376.
%% Cell type:code id: tags:
``` prob
x <: POW(1..100) & {100}:x & !y.(y:x => {card(y)}:x)
```
%% Output
$TRUE$
**Solution:**
* $x = \{\{100\},\{1\}\}$
TRUE
Solution:
x = {{100},{1}}
%% Cell type:markdown id: tags:
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).
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).
The set is then kept symbolic and can again be used in various ways.
%% Cell type:code id: tags:
``` prob
inf = {x|x>1000 & x mod 25 = 0} & 1025 ∈ inf & not(1000∈inf) & res = (900..1100) ∩ inf
res = ((900 ‥ 1100) ∩ {x∣x > 1000 ∧ x mod 25 = 0})
%% Cell type:markdown id: tags:
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:
- closure(Parameters,Types,CompiledPredicate)
For example, a set {x|x>v} where v has the value 17 is compiled to:
- closure([x],[integer],```x>17```)
%% Cell type:markdown id: tags:
#### List representation ####
The list representation is used when a finite set is partially known and constraint solving has to determine the set.
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}
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 = 100
%% Cell type:markdown id: tags:
In the appendix there are more examples which analyse the performance for such examples.
%% Cell type:markdown id: tags:
ProB employs the *Andorra* principle: deterministic computations are done first.
As there are multiple set representations, there are actually two kinds of deterministic computations:
- deterministic computations that generate an efficient representation, e.g., an AVL set representation
- and other deterministic computations
The ProB solver has a **WAITFLAG store** where choice points and enumerations are registered with a given priority.
- Priority 0 means that an efficient representation can be generated
- Priority 1 is a deterministic computation not guaranteed to produce an efficient representation
- Priority k is a choice point/enumeration which may generate k possible values
At each solving step one waitflag is activated, the one with the lowest priority.
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.
#### Example ####
Let us examine how ```x = 1..n & y = 2*n..3*n & n = 100 & xy = x \/ y``` is solved.
- all constraints are registered
- in phase 0 ```n=100``` is run
- this means that ```1..n``` can be efficiently computed
- this means that ```x = 1..n``` triggers in phase 0
- then ```2*n``` and ```3*n``` can be computed, followed by ```2*n..3*n```
- this means that ```y = 2*n..3*n``` triggers in phase 0
- again, this means that ```x \/ y``` can be efficiently computed
- finally ```xy = x \/ y``` can be executed in phase 0
No enumeration was required. In this case ProB's constraint solver works similar to a topological sorting algorithm.
%% Cell type:markdown id: tags:
#### Dealing with unbounded enumeration ####
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 id: tags:
### Functional Programming ###
Some functions are automatically detected as infinite by ProB, are kept symbolic but can be applied in several ways:
%% Cell type:code id: tags:
``` prob
f = %x.(x:INTEGER|x*x) &
r1 = f(100000) &
r2 = f[1..10] &
r3 = ([2,3,5,7,11] ; f) &
r4 = iterate(f,3)(2) &
f(sqrt) = 100
```
%% Output
$TRUE$
**Solution:**
* $r2 = \{1,4,9,16,25,36,49,64,81,100\}$
* $r3 = [4,9,25,49,121]$
* $r4 = 256$
* $sqrt = 10$
* $f = \lambdax\qdot(x \in INTEGER\midx * x)$
* $r1 = 10000000000$
TRUE
Solution:
r2 = {1,4,9,16,25,36,49,64,81,100}
r3 = [4,9,25,49,121]
r4 = 256
sqrt = 10
f = λx·(x ∈ INTEGER∣x ∗ x)
r1 = 10000000000
%% Cell type:code id: tags:
``` prob
f = {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function
r1 = f(100000) &
r2 = f[1..10] &
r3 = ([2,3,5,7,11] ; f) &
r4 = iterate(f,3)(2) &
f(sqr) = 100 &
r5 = closure1(f)[{10000}]
```
%% Output
$TRUE$
**Solution:**
* $r2 = \{1,2,3,4\}$
* $r3 = [2,2,3,3,4]$
* $r4 = 2$
* $r5 = \{2,4,10,100\}$
* $sqr = 9802$
* $f = \{x,y\midx \in NATURAL \land y \cprod 2 \geq x \land (y - 1) \cprod 2 < x\}$
* $r1 = 317$
TRUE
Solution:
r2 = {1,2,3,4}
r3 = [2,2,3,3,4]
r4 = 2
r5 = {2,4,10,100}
sqr = 9802
f = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}
r1 = 317
%% Cell type:markdown id: tags:
### Reification ###
Reification is linking the truth value of a constraint with a boolean variable.
ProB's kernel provides support for reifying a considerable number of constraints (but not yet all!).
Reification is important for efficiency, to avoid choice points and is important to link various solvers of ProB (set, arithmetic, boolean,...).
A \/ B = D & A /\ C = {} & D=C & A /= {} & A:POW(STRING)
```
%% Output
:eval: UNKNOWN (FALSE with enumeration warning)
%% Cell type:markdown id: tags:
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/={}.
ProB (as well as Kodkod and Z3 backends) can only infer the conflict for finite domains:
%% Cell type:code id: tags:
``` prob
A \/ B = D & A /\ C = {} & D=C & A /= {} & A:POW(BOOL)
```
%% Output
$FALSE$
FALSE
%% Cell type:code id: tags:
``` prob
:solve kodkod A \/ B = D & A /\ C = {} & D=C & A /= {} & A:POW(BOOL)
```
%% Output
$FALSE$
FALSE
%% Cell type:code id: tags:
``` prob
:solve z3 A \/ B = D & A /\ C = {} & D=C & A /= {} & A:POW(BOOL)
```
%% Output
$FALSE$
FALSE
%% Cell type:markdown id: tags:
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:
```
{log}=> diff(int(1,200),{50},R).
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}
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}
%% Cell type:markdown id: tags:
Another example, for minimum of set from SETS'18 paper:
%% Cell type:code id: tags:
``` prob
:time :solve prob S = {8,4,6,2,10,5} & y:S & S = {x|x:S & y<=x}
```
%% Output
Execution time: 0.014517786 seconds
$TRUE$
**Solution:**
* $S = \{2,4,5,6,8,10\}$
* $y = 2$
TRUE
Solution:
S = {2,4,5,6,8,10}
y = 2
%% Cell type:code id: tags:
``` prob
S= {8,4,6,2,10,5} & y:S & !x.(x:S => y<=x)
```
%% Output
$TRUE$
**Solution:**
* $S = \{2,4,5,6,8,10\}$
* $y = 2$
TRUE
Solution:
S = {2,4,5,6,8,10}
y = 2
%% Cell type:markdown id: tags:
## Summary of Set Constraint Solving Approaches ##
- SAT Translation (Kodkod backend):
- needs finite and small base type, no unbounded or higher-order sets
- can be very effective for complex constraints involving image, transitive closure,...
- limited performance for large sets
- SMTLib Translation (Z3/CVC4 backend):
- can deal with unbounded and large sets
- due to heavy use of quantifiers, some finite constraints get translated into infinite ones: limited model finding capabilities
- works well for large sets and semi-deterministic computation
- works well for animation, data validation, disproving
- limitations appear for symbolic model checking (IC3,...)
- Future work: improve combination with Z3/Kodkod, improve list representation (maybe use a bit-vector like representation, and CLP(FD) cardinality variable)
%% Cell type:markdown id: tags:
### Integrations of Approaches ###
ProB provides the joint application of the CLP(FD) and SMT backend (preference ```SMT_SUPPORTED_INTERPRETER```.
Constraints are posted both to ProB and Z3/CVC4, with the hope that Z3/CVC4 prune infeasible branches.
The main motivation was new symbolic validation techniques such as IC3.
The Kodkod integration also passes higher-order/unbounded constraints to ProB, after solving the first order finite constraints with Kodkod/Alloy.
However, this kind of integration is rarely useful (most of the generated solutions get rejected by ProB).
A more promising, fine-grained integration has been presented at PADL'18.
%% Cell type:markdown id: tags:
## Appendix ##
%% Cell type:markdown id: tags:
### Explicit Computations ####
What about explicit computations? How well does the SMTLib translation fare here?
%% Cell type:code id: tags:
``` prob
:solve z3 x = 1..1000 /\ (200..300)
```
%% Output
:solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
:time :solve z3 x = 1..40 /\ (6..15)
```
%% Output
Execution time: 0.224425596 seconds
$TRUE$
**Solution:**
* $x = \{6,7,8,9,10,11,12,13,14,15\}$
TRUE
Solution:
x = {6,7,8,9,10,11,12,13,14,15}
%% Cell type:code id: tags:
``` prob
:time :solve z3 x = 1..60 /\ (6..15)
```
%% Output
Execution time: 1.149180308 seconds
$TRUE$
**Solution:**
* $x = \{6,7,8,9,10,11,12,13,14,15\}$
TRUE
Solution:
x = {6,7,8,9,10,11,12,13,14,15}
%% Cell type:code id: tags:
``` prob
:time :solve z3 x = 1..80 /\ (6..15)
```
%% Output
:time: :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
:time :solve prob x = 1..80 /\ (6..15)
```
%% Output
Execution time: 0.005873811 seconds
$TRUE$
**Solution:**
* $x = (6 \ldots 15)$
TRUE
Solution:
x = (6 ‥ 15)
%% Cell type:markdown id: tags:
In the following the inverse operator seems to pose problems to Z3:
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.28.0 (20110509.1545)--><!-- Title: state Pages: 1 --><svg width="128pt" height="188pt"viewBox="0.00 0.00 128.00 188.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph1" class="graph" transform="scale(1 1) rotate(0) translate(4 184)"><title>state</title><polygon fill="white" stroke="white" points="-4,5 -4,-184 125,-184 125,5 -4,5"/><g id="graph2" class="cluster"><title>cluster_Trains</title><polygon fill="lightgrey" stroke="lightgrey" points="8,-8 8,-172 112,-172 112,-8 8,-8"/><text text-anchor="middle" x="60" y="-157.2" font-family="Times,serif" font-size="12.00">Trains</text></g><!-- gordon --><g id="node1" class="node"><title>gordon</title><polygon fill="#efdf84" stroke="#efdf84" points="71.249,-52 16.751,-52 16.751,-16 71.249,-16 71.249,-52"/><text text-anchor="middle" x="44" y="-29.8" font-family="Times,serif" font-size="14.00">gordon</text></g><!-- gordon->gordon --><g id="edge2" class="edge"><title>gordon->gordon</title><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"/><polygon fill="firebrick" stroke="firebrick" points="82.0283,-23.4609 71.6842,-25.752 81.1994,-30.4116 82.0283,-23.4609"/><text text-anchor="middle" x="96.3829" y="-29.8" font-family="Times,serif" font-size="14.00">rel</text></g><!-- thomas --><g id="node3" class="node"><title>thomas</title><polygon fill="#efdf84" stroke="#efdf84" points="72.3312,-142 15.6688,-142 15.6688,-106 72.3312,-106 72.3312,-142"/><text text-anchor="middle" x="44" y="-119.8" font-family="Times,serif" font-size="14.00">thomas</text></g><!-- thomas->gordon --><g id="edge4" class="edge"><title>thomas->gordon</title><path fill="none" stroke="firebrick" d="M44,-105.614C44,-93.2403 44,-76.3686 44,-62.2198"/><polygon fill="firebrick" stroke="firebrick" points="47.5001,-62.0504 44,-52.0504 40.5001,-62.0504 47.5001,-62.0504"/><text text-anchor="middle" x="51.3829" y="-74.8" font-family="Times,serif" font-size="14.00">rel</text></g><!-- thomas->thomas --><g id="edge6" class="edge"><title>thomas->thomas</title><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"/><polygon fill="firebrick" stroke="firebrick" points="82.6376,-113.434 72.2994,-115.752 81.8265,-120.387 82.6376,-113.434"/><text text-anchor="middle" x="97.3829" y="-119.8" font-family="Times,serif" font-size="14.00">rel</text></g></g></svg>)