"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": {},
"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"
"[2018-05-30 11:12:16,405, T+83006756] \"ProB Output Logger for instance 712ca57b\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Keeping comprehension-set symbolic (you may want to use the /*@symbolic*/ pragma to prevent this message, unless it was due to a WD-Error), identifiers: [x,y]\u001b[0m\n",
"[2018-05-30 11:12:16,406, T+83006757] \"ProB Output Logger for instance 712ca57b\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Line: 1 Column: 9 until 44\u001b[0m\n",
":solve z3 A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(BOOL)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"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",
[2018-05-28 14:44:27,573, T+14878906] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 51303
[2018-05-28 14:44:27,573, T+14878906] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 24121
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.
%% Cell type:markdown id: tags:
## 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:
# Constraint solving has many applications in formal methods in general and B in particular.
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 ##
%% 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.
#### 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:
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-28 13:16:28,635, T+9599968] "ProB Output Logger for instance 712ca57b" 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-28 13:16:28,636, T+9599969] "ProB Output Logger for instance 712ca57b" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [679][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).
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.
%% 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-28 13:31:04,544, T+10475877] "ProB Output Logger for instance 712ca57b" 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)
[2018-05-28 13:31:04,546, T+10475879] "ProB Output Logger for instance 712ca57b" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Timeout when posting constraint:[0m
%% Cell type:markdown id: tags:
### Summary for Integer Arithmetic ###
Solver | Unbounded | Model Finding | Inconsistency Detection
------|------------|---------------|---
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 ##
### 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:code id: tags:
``` prob
:solve kodkod x <: 1..2 & y<: 1..2 & x \/ y = 1..2 & 1:x & x <<: y
```
%% Output
[2018-05-28 14:51:49,560, T+15320893] "ProB Output Logger for instance 2dd01afa" 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-28 14:51:49,561, T+15320894] "ProB Output Logger for instance 2dd01afa" 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:
- 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 11:12:16,405, T+83006756] "ProB Output Logger for instance 712ca57b" 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 11:12:16,406, T+83006757] "ProB Output Logger for instance 712ca57b" 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 10:18:29,022, T+79779373] "ProB Output Logger for instance 712ca57b" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: A \/ B = D & A /\ C = {} & D = C & A /= {} ints: none, intatoms: none[0m
FALSE
[2018-05-30 10:18:29,023, T+79779374] "ProB Output Logger for instance 712ca57b" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [][0m
%% 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.041415678 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}