"[2018-06-01 10:06:02,879, T+73563] \"ProB Output Logger for instance 6e28bb87\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: f : 1 .. n --> 1 .. n & !x.(x : 2 .. n => f(x) = f... ints: irange(1,50), intatoms: irange(1,50)\u001b[0m\n",
"[2018-06-01 10:06:02,880, T+73564] \"ProB Output Logger for instance 6e28bb87\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n",
"[2018-06-01 10:06:02,881, T+73565] \"ProB Output Logger for instance 6e28bb87\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1236]\u001b[0m\n",
"[2018-06-01 10:33:15,765, T+1706449] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 53813\n",
"[2018-06-01 10:33:15,766, T+1706450] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 2267\n",
"[2018-06-01 10:33:19,931, T+1710615] \"ProB Output Logger for instance 1cb4e9b8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n",
[2018-05-30 15:21:18,280, T+14092] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 53783
[2018-05-30 15:21:18,281, T+14093] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 63388
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
{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.
%% Cell type:code id: tags:
``` prob
(1..3 \/ 5..10) \ (2..6)
```
%% Output
{1,7,8,9,10}
%% Cell type:code id: tags:
``` prob
ran({(thomas↦1),(gordon↦2)})
```
%% Output
{1,2}
%% Cell type:code id: tags:
``` prob
{(thomas↦1),(gordon↦2)} (thomas)
```
%% Output
1
%% Cell type:code id: tags:
``` prob
{(thomas↦1),(gordon↦2)}~[2..3]
```
%% Output
{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
%% Cell type:code id: tags:
``` prob
3>2
```
%% Output
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
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}
%% 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 following is an unsatisfiable predicate:
%% Cell type:code id: tags:
``` prob
x*x=1000
```
%% Output
FALSE
%% Cell type:markdown id: tags:
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.
#### 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:
Suppose that we have the invariant, ```train_position:TRAINS-->1..10000``` we can check whether the event is **feasible** in at least one valid state by solving:
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}
%% 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.)
#### Knights and Knave Puzzle####
Here is a puzzle from Smullyan involving an island with only knights and knaves.
We know that:
- Knights: always tell the truth
- Knaves: always lie
We are given the following information about three persons A,B,C on the island:
1. A says: “B is a knave or C is a knave”
2. B says “A is a knight”
What are A, B and C?
Note: we model A,B,C as boolean variables which are equal to TRUE if they are a knight and FALSE if they are a knave.
%% Cell type:code id: tags:
``` prob
(A=TRUE <=> (B=FALSE or C=FALSE)) & // Sentence 1
(B=TRUE <=> A=TRUE) // Sentence 2
```
%% Output
TRUE
Solution:
A = TRUE
B = TRUE
C = FALSE
%% 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.
Let us consider a small arithmetic puzzle
```
X Y
+ X Y
-----
Y 0
```
%% Cell type:code id: tags:
``` prob
X:1..9 & Y:0..9 & X*10 + Y + X*10 + Y = Y*10
```
%% Output
TRUE
Solution:
X = 2
Y = 5
%% Cell type:markdown id: tags:
Given that we know the domain of X and Y one can represent the integers by binary numbers and convert the constraint to a SAT problem.
%% Cell type:markdown id: tags:
Let us look at an even simpler constraint X:0..3 & Y:0..3 & X+Y=2. As you can see there are three solutions for this constraint:
%% Cell type:code id: tags:
``` prob
{X,Y|X:0..3 & Y:0..3 & X+Y=2}
```
%% Output
{(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``` one 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:
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
[2018-05-30 15:21:22,569, T+18381] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: x : 0 .. 2 & y : 0 .. 2 & x + y = 2 ints: irange(0,4), intatoms: none[0m
[2018-05-30 15:21:22,570, T+18382] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).[0m
[2018-05-30 15:21:22,570, T+18382] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1,2,0][0m
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
[2018-05-30 15:21:22,674, T+18486] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: {x,y|x : 0 .. 2 & y : 0 .. 2 & x + y = 2} = res ints: irange(0,4), intatoms: irange(0,2)[0m
[2018-05-30 15:21:22,675, T+18487] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1][0m
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 operators in the language.
Here is ProB's SMTLib/Z3 API calls for the constraint:
ProB's default solver makes use of constraint logic programming.
For arithmetic, it builts on top of CLP(FD), the finite domain library of SICStus Prolog.
In CLP(FD):
- every integer variable is associated with a domain of possible values, typically an interval
- when adding a new constraints, the domains of the involved variables are updated, or more precisely narrowed down.
- at some point we need to chose variables for enumeration; typically ProB chooses the value with the smallest domain.
Let us use a slightly adapted constraint ```x:0..9 & y:0..9 & x+y=2``` to illustrate how constraint processing works:
- x:0..9 $\leadsto$ x:0..9, y:$-\infty$..$\infty$
- y:0..9 $\leadsto$ x:0..9, y:0..9
- x+y=2 $\leadsto$ x:0..2, y:0..2
- Enumerate (label) variable x
- x=0 $\leadsto$ x:0..0, y:2..2
- x=1 $\leadsto$ x:1..1, y:1..1
- x=2 $\leadsto$ x:2..2, y:0..0
%% Cell type:code id: tags:
``` prob
:solve prob {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7
```
%% Output
TRUE
Solution:
P = 4
A = 1
S = 3
I = 0
K = 2
N = 9
O = 8
%% Cell type:code id: tags:
``` prob
: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
:solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
: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
[2018-05-30 15:21:26,850, T+22662] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: K : 1 .. 9 & P : 1 .. 9 & I : 0 .. 9 & S : 0 .. 9 ... ints: irange(0,99980001), intatoms: irange(0,9)[0m
[2018-05-30 15:21:26,851, T+22663] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [424][0m
TRUE
Solution:
P = 4
A = 1
S = 3
I = 0
K = 2
N = 9
O = 8
%% 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
%% Cell type:markdown id: tags:
Here is an example where ProB generates an enumeration warning, but finds a solution:
: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
%% 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 enabled, but without the module the result is **UNKNOWN**.
%% Cell type:code id: tags:
``` prob
:solve z3 x>y & y>x
```
%% Output
FALSE
%% Cell type:code id: tags:
``` prob
:solve prob x>y &y>x
```
%% Output
[2018-05-30 15:21:29,975, T+25787] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Timeout when posting constraint:[0m
: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:
### Deferred and Enumerated Sets ###
Given an enumerated set ```Trains = {thomas, gordon}``` we associate a variable ```x:Trains``` with
an integer decision variable in the range 1..2.
Similarly, deferred sets are given a finite cardinality $n$, and a decision variables are in the range 1..n.
%% Cell type:code id: tags:
``` prob
x:Trains & y:Trains & x/=y
```
%% Output
TRUE
Solution:
x = thomas
y = gordon
%% 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}
%% 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
```
%% Output
TRUE
Solution:
y1 = TRUE
x1 = TRUE
y2 = TRUE
x2 = FALSE
%% Cell type:markdown id: tags:
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
[2018-05-30 15:21:30,279, T+26091] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: x <: 1 .. 2 & y <: 1 .. 2 & x \/ y = 1 .. 2 & 1 : ... ints: irange(1,2), intatoms: irange(1,2)[0m
[2018-05-30 15:21:30,280, T+26092] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1][0m
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
%% 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}}
%% 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:
The virtual timeout message can be removed (and performance improved) by adding the symbolic pragma:
%% Cell type:code id: tags:
``` prob
inf = /*@symbolic*/ {x|x>1000 & x mod 25 = 0} & 1025 : inf & not(1000:inf) & res = (900..1100) /\ inf
```
%% Output
TRUE
Solution:
inf = {x∣x > 1000 ∧ x mod 25 = 0}
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:
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 = λ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
[2018-05-30 15:21:43,023, T+38835] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] [0m[31m[1m! Keeping comprehension-set symbolic (you may want to use the /*@symbolic*/ pragma to prevent this message, unless it was due to a WD-Error), identifiers: [x,y][0m
[2018-05-30 15:21:43,024, T+38836] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] [0m[31m[1m! Line: 1 Column: 9 until 44[0m
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
%% Cell type:code id: tags:
``` prob
:solve kodkod A \/ B = D & A /\ C = {} & D=C & A /= {} & A:POW(BOOL)
```
%% Output
[2018-05-30 15:21:43,486, T+39298] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: A \/ B = D & A /\ C = {} & D = C & A /= {} ints: none, intatoms: none[0m
[2018-05-30 15:21:43,487, T+39299] "ProB Output Logger for instance 762b9e9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [][0m
FALSE
%% Cell type:code id: tags:
``` prob
:solve z3 A \/ B = D & A /\ C = {} & D=C & A /= {} & A:POW(BOOL)
```
%% Output
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}
Another solution? (y/n)
```
In ProB this is instantenous:
%% Cell type:code id: tags:
``` prob
:time R= (1..200) \ {50}
```
%% Output
Execution time: 0.006102410 seconds
TRUE
Solution:
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:
## 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
f = {(1↦1),(2↦2),(3↦3),(4↦4),(5↦5),(6↦6),(7↦7),(8↦8),(9↦9),(10↦10),(11↦11),(12↦12),(13↦13),(14↦14),(15↦15),(16↦16),(17↦17),(18↦18),(19↦19),(20↦20),(21↦21),(22↦22),(23↦23),(24↦24),(25↦25),(26↦26),(27↦27),(28↦28),(29↦29),(30↦30),(31↦31),(32↦32),(33↦33),(34↦34),(35↦35),(36↦36),(37↦37),(38↦38),(39↦39),(40↦40),(41↦41),(42↦42),(43↦43),(44↦44),(45↦45),(46↦46),(47↦47),(48↦48),(49↦49),(50↦50)}
[2018-06-01 10:06:02,879, T+73563] "ProB Output Logger for instance 6e28bb87" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: f : 1 .. n --> 1 .. n & !x.(x : 2 .. n => f(x) = f... ints: irange(1,50), intatoms: irange(1,50)[0m
[2018-06-01 10:06:02,880, T+73564] "ProB Output Logger for instance 6e28bb87" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).[0m
[2018-06-01 10:06:02,881, T+73565] "ProB Output Logger for instance 6e28bb87" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1236][0m
Execution time: 5.019394450 seconds
TRUE
Solution:
f = {(3↦3),(5↦5),(6↦6),(7↦7),(9↦9),(10↦10),(11↦11),(12↦12),(13↦13),(14↦14),(15↦15),(17↦17),(18↦18),(19↦19),(20↦20),(21↦21),(22↦22),(23↦23),(24↦24),(25↦25),(26↦26),(27↦27),(28↦28),(29↦29),(30↦30),(31↦31),(33↦33),(34↦34),(35↦35),(36↦36),(37↦37),(38↦38),(39↦39),(40↦40),(41↦41),(42↦42),(43↦43),(44↦44),(45↦45),(46↦46),(47↦47),(48↦48),(49↦49),(50↦50),(1↦1),(2↦2),(4↦4),(8↦8),(16↦16),(32↦32)}
[2018-06-01 10:33:15,765, T+1706449] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 53813
[2018-06-01 10:33:15,766, T+1706450] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 2267
[2018-06-01 10:33:19,931, T+1710615] "ProB Output Logger for instance 1cb4e9b8" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).[0m
Execution time: 1.110113990 seconds
FALSE
%% Cell type:code id: tags:
``` prob
:time :solve z3 edges : NODES5 <-> NODES5 &
edges~=edges &
not(#(n1,n2).(n1:NODES5 & n2:NODES5 & n2/=n1 &
card(edges[{n1}]) = card(edges[{n2}]))) &
dom(edges)=NODES5 & id(NODES5) /\ edges = {}
```
%% Output
:time: :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:markdown id: tags:
So with Kodkod we proved the theorem for 5 nodes in about a second.
