Skip to content
Snippets Groups Projects
Commit 8521544f authored by miwer106's avatar miwer106
Browse files

refactor some notebooks and open folder for delayed notebooks

parent 83dcdd35
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 42 additions and 227 deletions
Apples_and_Oranges.ipynb
+ 1
− 22
View file @ 8521544f
%% Cell type:markdown id: tags:
# Apples and Oranges
Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.
This puzzle is [apparently an Interview question at Apple](https://bgr.com/2015/11/20/apple-interview-questions/). Quoting from
[1](https://bgr.com/2015/11/20/apple-interview-questions/) we have the
[here](https://bgr.com/2015/11/20/apple-interview-questions/) we have the
following information:
* (1) There are three boxes, one contains only apples, one contains only oranges, and one contains both apples and oranges.
* (2) The boxes have been incorrectly labeled such that no label identifies the actual contents of the box it labels.
* (3) Opening just one box, and without looking in the box, you take out one piece of fruit.
* (4) By looking at the fruit, how can you immediately label all of the boxes correctly?
Here is one encoding of this puzzle in B:
%% Cell type:code id: tags:
``` prob
::load
MACHINE ApplesOranges
SETS
Fruit={apple,orange}; // possible content for the boxes
Label={A,O,Both} // labels for the boxes
CONSTANTS a,o,b, // a,o,b are the three boxes
Take, // which box should we open (the label of that box)
DecisionFunction // given the fruit we pick from Take: what are the contents of the boxes labeled A,O,Both
PROPERTIES
a = {apple} & o={orange} & b={apple,orange} // (1)
&
Take : Label //3
&
DecisionFunction : Fruit --> (Label >->> {a,o,b}) & //4
!label. ( // the decision function has to work for all allowed labelings
( label : {a,o,b} >->> Label &
label(a) /= A & label(o) /= O & label(b) /= Both // (2)
)
=>
!f.(f: label~(Take)
=> DecisionFunction(f)=label~ // the function should tell us what is behind label A,O,Both
)
)
END
```
%% Output
Loaded machine: ApplesOranges
%% Cell type:markdown id: tags:
We have abstracted the box of apples `a` by the set containing `apple`.
Ditto for `o` and `b`, which are abstracted by `{orange}` and
`{apple,orange}` respectively.
NOTE: You need a recent version of ProB 1.5.1-beta3 or newer to load the above model on your own computer with its one-line comments. If you have an older version of ProB, simply use the normal comments `/* ... */`.
`:goto Number` jumps to the state with the given number.
With the `:trace` command, you will get the information of your current trace.
There is an autocompletion tool, which allows you to see the possible commands, simply use TAB after you type in your `:`.
This model gives you just one solution, after setting up the constants with `:constants`.
%% Cell type:code id: tags:
``` prob
:goto -1
```
%% Output
Changed to state with index -1
%% Cell type:code id: tags:
``` prob
:trace
```
%% Output
* -1: Root state **(current)**
-1: Root state (current)
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
Take
```
%% Output
$\mathit{Both}$
Both
%% Cell type:markdown id: tags:
As we can see, the only solution is to open the box labelled with
"Both". We can inspect the decision function by using the jupyter notebook code block, like follows:
%% Cell type:code id: tags:
``` prob
DecisionFunction(apple)
```
%% Output
$\{(\mathit{A}\mapsto\{\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{Both}\mapsto\{\mathit{apple}\})\}$
{(A↦{orange}),(O↦{apple,orange}),(Both↦{apple})}
%% Cell type:code id: tags:
``` prob
DecisionFunction(orange)
```
%% Output
$\{(\mathit{A}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple}\}),(\mathit{Both}\mapsto\{\mathit{orange}\})\}$
{(A↦{apple,orange}),(O↦{apple}),(Both↦{orange})}
%% Cell type:markdown id: tags:
In other words, when we pick an apple out of the box labelled with
"Both", then it contains only apples and the box labelled "O"ranges
contains both apples and oranges. The box labelled "A"pples contains
just oranges. Similarly, if we pick up an orange out of the box labelled
with "Both", then it contains only oranges and the box labelled with
"A"pples contains contains both apples and oranges. The box labelled
"O"ranges contains just apples.
NOTE: You can use `:table Expression` to get values or expressions in a tabular form.
%% Cell type:code id: tags:
``` prob
:table DecisionFunction
```
%% Output
|prj1|prj2|
|---|---|
|$\mathit{apple}$|$\{(\mathit{A}\mapsto\{\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{Both}\mapsto\{\mathit{apple}\})\}$|
|$\mathit{orange}$|$\{(\mathit{A}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple}\}),(\mathit{Both}\mapsto\{\mathit{orange}\})\}$|
prj1 prj2
apple {(A|->{orange}),(O|->{apple,orange}),(Both|->{apple})}
orange {(A|->{apple,orange}),(O|->{apple}),(Both|->{orange})}
%% Cell type:markdown id: tags:
## Argumentation Theory
Below we try to model some concepts of argumentation theory in B. The examples try to show that classical (monotonic) logic with set theory can be used to model some aspects of argumentation theory quite naturally, and that ProB can solve and visualise some problems in argumentation theory. Alternative solutions are encoding arguments as normal logic programs (with non-monotonic negation) and using answer set solvers for problem solving.
The following model was inspired by a talk given by Claudia Schulz.
The model below represents the labelling of the arguments as a total function from arguments to its status, which can either be in (the argument is accepted), out (the argument is rejected), or undec (the argument is undecided). The relation between the arguments is given in the binary attacks relation.
In case you are new to B, you probably need to know the following operators to understand the specification below (we als have a summary page about the B syntax in our handbook):
* `x : S` specifies that x is an element of S
* `a|→b` represents the pair (a,b); note that a relation and function in B is a set of pairs.
*
......
Die_Hard_Jugs.ipynb
+ 2
− 0
View file @ 8521544f
%% Cell type:markdown id: tags:
# Die Hard Jugs Puzzle
Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.
This is the B model of a puzzle from the movie "Die Hard with a Vengeance". [This clip](https://www.youtube.com/watch?v=BVtQNK_ZUJg) shows Bruce Willis and Samuel Jackson having a go at the puzzle. A more detailed explanation can be found [here](https://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm).
At start we have one 3 gallon and one 5 gallon jug, and we need to measure precisely 4 gallons by filling, emptying or transferring water from the jugs.
%% Cell type:code id: tags:
``` prob
::load
MACHINE Jars
DEFINITIONS
GOAL == (4 : ran(level));
SETS Jars = {j3,j5}
CONSTANTS maxf
PROPERTIES maxf : Jars --> NATURAL &
maxf = {j3 |-> 3, j5 |-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */
VARIABLES level
INVARIANT
level: Jars --> NATURAL
INITIALISATION level := Jars * {0} /* all jars start out empty */
OPERATIONS
FillJar(j) = /* we can completely fill a jar j */
PRE j:Jars & level(j)<maxf(j) THEN
level(j) := maxf(j)
END;
EmptyJar(j) = /* we can completely empty a jar j */
PRE j:Jars & level(j)>0 THEN
level(j) := 0
END;
Transfer(j1,amount,j2) = /* we can transfer from jar j1 to j2 until either j2 is full or j1 is empty */
PRE j1:Jars & j2:Jars & j1 /= j2 & amount>0 &
amount = min({level(j1), maxf(j2)-level(j2)}) THEN
level := level <+ { j1|-> level(j1)-amount, j2 |-> level(j2)+amount }
END
END
```
%% Output
Loaded machine: Jars
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:markdown id: tags:
## Trace for solution
In the following, we will see the trace for the solution of the puzzle.
%% Cell type:code id: tags:
``` prob
:exec FillJar j=j5
```
%% Output
Executed operation: FillJar(j5)
%% Cell type:code id: tags:
``` prob
:exec Transfer j1=j5 & amount=3 & j2=j3
```
%% Output
Executed operation: Transfer(j5,3,j3)
%% Cell type:code id: tags:
``` prob
:exec EmptyJar j=j3
```
%% Output
Executed operation: EmptyJar(j3)
%% Cell type:code id: tags:
``` prob
:exec Transfer j1=j5 & amount=2 & j2=j3
```
%% Output
Executed operation: Transfer(j5,2,j3)
%% Cell type:code id: tags:
``` prob
:exec FillJar j=j5
```
%% Output
Executed operation: FillJar(j5)
%% Cell type:code id: tags:
``` prob
:exec Transfer j1=j5 & amount=1 & j2=j3
```
%% Output
Executed operation: Transfer(j5,1,j3)
%% Cell type:code id: tags:
``` prob
:trace
```
%% Output
* -1: Root state
* 0: `SETUP_CONSTANTS()`
* 1: `INITIALISATION()`
* 2: `FillJar(j5)`
* 3: `Transfer(j5,3,j3)`
* 4: `EmptyJar(j3)`
* 5: `Transfer(j5,2,j3)`
* 6: `FillJar(j5)`
* 7: `Transfer(j5,1,j3)` **(current)**
-1: Root state
0: SETUP_CONSTANTS()
1: INITIALISATION()
2: FillJar(j5)
3: Transfer(j5,3,j3)
4: EmptyJar(j3)
5: Transfer(j5,2,j3)
6: FillJar(j5)
7: Transfer(j5,1,j3) (current)
%% Cell type:code id: tags:
``` prob
:table (maxf, level)
```
%% Output
|prj1|prj2|
|---|---|
|$\{(\mathit{j3}\mapsto 3),(\mathit{j5}\mapsto 5)\}$|$\{(\mathit{j3}\mapsto 3),(\mathit{j5}\mapsto 4)\}$|
prj1 prj2
{(j3|->3),(j5|->5)} {(j3|->3),(j5|->4)}
%% Cell type:markdown id: tags:
## Graphical Animation
Like some of the other jupyter notebook examples, this machine can be animated with the `ANIMATION_FUNCTION`. To do that, we have to add the following lines into the `DEFINTION` section of the machine:
```
ANIMATION_IMG1 == "images/Filled.gif";
ANIMATION_IMG2 == "images/Empty.gif";
ANIMATION_IMG3 == "images/Void.gif";
gmax == max(ran(maxf));
ANIMATION_FUNCTION_DEFAULT == {r,c,i | c:Jars & r:1..gmax & i=3};
ri == (gmax+1-r);
ANIMATION_FUNCTION == {r,c,i | c:Jars & ri:1..maxf(c) & (ri<=level(c) => i=1 ) & (ri>level(c) => i=2)}
```
After that, we can just load the machine as usual.
%% Cell type:code id: tags:
``` prob
::load
MACHINE Jars
DEFINITIONS
GOAL == (4 : ran(level));
ANIMATION_IMG1 == "images/Filled.gif";
ANIMATION_IMG2 == "images/Empty.gif";
ANIMATION_IMG3 == "images/Void.gif";
gmax == max(ran(maxf));
ANIMATION_FUNCTION_DEFAULT == {r,c,i | c:Jars & r:1..gmax & i=3};
ri == (gmax+1-r);
ANIMATION_FUNCTION == {r,c,i | c:Jars & ri:1..maxf(c) &
(ri<=level(c) => i=1 ) & (ri>level(c) => i=2)}
SETS Jars = {j3,j5}
CONSTANTS maxf
PROPERTIES maxf : Jars --> NATURAL &
maxf = {j3 |-> 3, j5 |-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */
VARIABLES level
INVARIANT
level: Jars --> NATURAL
INITIALISATION level := Jars * {0} /* all jars start out empty */
OPERATIONS
FillJar(j) = /* we can completely fill a jar j */
PRE j:Jars & level(j)<maxf(j) THEN
level(j) := maxf(j)
END;
EmptyJar(j) = /* we can completely empty a jar j */
PRE j:Jars & level(j)>0 THEN
level(j) := 0
END;
Transfer(j1,amount,j2) = /* we can transfer from jar j1 to j2 until either j2 is full or j1 is empty */
PRE j1:Jars & j2:Jars & j1 /= j2 & amount>0 &
amount = min({level(j1), maxf(j2)-level(j2)}) THEN
level := level <+ { j1|-> level(j1)-amount, j2 |-> level(j2)+amount }
END
END
```
%% Output
Loaded machine: Jars
%% Cell type:markdown id: tags:
Now that we loaded the machine, we have to initiate the machine. To run the animation, you can use the commant `:show`. This will make it easier to understand the trace we have seen before:
! If you run into any difficulties with the setup for the graphical animation, please consider reading our "ProB Jupyter Notebook Overview" notebook for more information.
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec FillJar j=j5
```
%% Output
Executed operation: FillJar(j5)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec Transfer j1=j5 & amount=3 & j2=j3
```
%% Output
Executed operation: Transfer(j5,3,j3)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec EmptyJar j=j3
```
%% Output
Executed operation: EmptyJar(j3)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec Transfer j1=j5 & amount=2 & j2=j3
```
%% Output
Executed operation: Transfer(j5,2,j3)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec FillJar j=j5
```
%% Output
Executed operation: FillJar(j5)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec Transfer j1=j5 & amount=1 & j2=j3
```
%% Output
Executed operation: Transfer(j5,1,j3)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:markdown id: tags:
As you can see, the right jar (that holds 5 gallons) contains exactly 4 gallons of water. With this we precisely measured 4 gallons of water and found a solution for the puzzle.
%% Cell type:code id: tags:
``` prob
```
......
Euler_Problem.ipynb
+ 2
− 0
View file @ 8521544f
%% Cell type:markdown id: tags:
# Euler Problem 67 - Maximum Path Sum II
Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.
In the following we will give a solution for the Euler Problem 67. For convenience, the description of the problem can be found on the official site for the [Euler Problem 67](https://projecteuler.net/problem=67).
By starting at the top of the triangle below and moving to adjacent numbers on the row below, the maximum total from top to bottom is 23.
```
3
7 4
2 4 6
8 5 9 3
```
That is, 3 + 7 + 4 + 9 = 23.
In this notebook we are going to find the maximum total from top to bottom in triangle.txt, a 15K text file containing a triangle with one-hundred rows.
Please note, that this is a much more difficult version of Problem 18. It is not possible to try every route to solve this problem, as there are 299 altogether! If you could check one trillion (1012) routes every second it would take over twenty billion years to check them all. There is an efficient algorithm to solve it.
%% Cell type:code id: tags:
``` prob
::load
MACHINE Euler_Problem_067
DEFINITIONS
"resources/triangle_Euler67.def";
SET_PREF_TIME_OUT == 5000
CONSTANTS n, Sol, OptimalSolution, TriangleC
PROPERTIES TriangleC = Triangle &
n = size (TriangleC) &
Sol : 1..n --> seq(INTEGER) &
Sol(n) = TriangleC(n) /* Initialisation */
&
! i. (i:1..(n-1) =>
(size(Sol(i)) = size(TriangleC(i))
& !j.(j: 1..size(TriangleC(i)) => Sol(i)(j) = TriangleC(i)(j)+max({Sol(i+1)(j),Sol(i+1)(j+1)}))
)
)
& OptimalSolution = Sol(1)(1)
ASSERTIONS
OptimalSolution = 7273;
n = 100
END
```
%% Output
Loaded machine: Euler_Problem_067
%% Cell type:markdown id: tags:
An interesting fact is the that dynamic programming is done automatically by ProB’s constraint solving.
For a better overview we are showing the optimal solution in this notebook with the `:eval` command.
```
ASSERTIONS
OptimalSolution = 7273;
n = 100
```
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags:
``` prob
:check assertions
```
%% Output
|Predicate|Value|
|---|---|
|$\mathit{OptimalSolution} = 7273$|$\mathit{TRUE}$|
|$\mathit{n} = 100$|$\mathit{TRUE}$|
OptimalSolution = 7273 = TRUE
n = 100 = TRUE
......
Fibonacci_Numbers.ipynb
+ 3
− 3
View file @ 8521544f
%% Cell type:markdown id: tags:
# Fibonacci Numbers with Automatic Dynamic Programming
In this jupyter notebook, we show you how to encode the Fibonacci problem in such a way that you get dynamic programming automatically when using ProB to solve the encoding.
Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.
First of all we have to load the machine, if you are struggeling with any operation of our jupyter kernel, try out `:help` or take a look at our `ProB Jupyter Noteboook Overview`.
In this jupyter notebook, we show you how to encode the Fibonacci problem in such a way that you get dynamic programming automatically when using ProB to solve the encoding.
After loading the machine, we are setting up the constants with `:constants` and initialising it with `:init`.
After loading the machine as seen below, we are setting up the constants with `:constants` and initialising it with `:init`.
Now you can ask the machine for the solution of the `n`th fibonacci number by typing in `sol`.
%% Cell type:code id: tags:
``` prob
::load
MACHINE Fibonacci_Dynamic_Programming
/* an encoding of Fibonacci where we get dynamic programming for free from ProB */
DEFINITIONS
DOM == INTEGER; /* INTEGER : For ProB no restriction necessary; for Kodkod yes */
CONSTANTS n, fib, sol
PROPERTIES
fib : 0..n --> DOM &
fib(0) = 1 & fib(1) = 1 &
!x.(x:2..n => fib(x) = fib(x-1) + fib(x-2))
/* You can change n here: */
& n = 5 & sol = fib(n)
END
```
%% Output
Loaded machine: Fibonacci_Dynamic_Programming
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags:
``` prob
n
```
%% Output
$5$
5
%% Cell type:code id: tags:
``` prob
sol
```
%% Output
$8$
8
%% Cell type:markdown id: tags:
Please note, that there is an explanation missing for this machine.
......
Game_of_Life.ipynb
+ 2
− 0
View file @ 8521544f
%% Cell type:markdown id: tags:
# Game of Life
Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.
This is an improved model of Conway’s Game of Life. It was written for animation with ProB. One interesting aspect is that the simulation is unbounded, i.e., not restricted to some pre-determined area of the grid. In this notebook we will examine the following machine and animate it.
To see all the specifications for Conway's Game of Life, click [here](https://en.wikipedia.org/wiki/Conway's_Game_of_Life).
%% Cell type:code id: tags:
``` prob
::load
MACHINE GameOfLife
/* A simple B model of the Game of Life */
/* by Jens Bendisposto and Michael Leuschel */
/* v2: improved version with more elegant neighbour relation */
ABSTRACT_CONSTANTS neigh
PROPERTIES
/* neighbour relation: */
neigh = {x,y,nb | x∈COORD ∧ y∈COORD ∧ (x,y) ≠ nb ∧
prj1(COORD,COORD)(nb) ∈ (x-1)..(x+1) ∧
prj2(COORD,COORD)(nb) ∈ (y-1)..(y+1) }
VARIABLES alive
DEFINITIONS
COORD == INTEGER;
/* some simple GOL patterns: */
blinker == {(2,1),(2,2),(2,3)} ; glider == {(1,2),(2,3),(3,1),(3,2),(3,3)} ;
SET_PREF_CLPFD == TRUE;
/* describing the animation function for the graphical visualization: */
wmin == min(dom(alive)∪{1}); wmax == max(dom(alive)∪{1});
hmin == min(ran(alive)∪{1}); hmax == max(ran(alive)∪{1});
ANIMATION_FUNCTION_DEFAULT == ( (wmin..wmax)*(hmin..hmax)*{0} );
ANIMATION_FUNCTION == ( alive * {1} );
ANIMATION_RIGHT_CLICK(I,J) == BEGIN step END;
ANIMATION_IMG0 == "images/sm_empty_box.gif";
ANIMATION_IMG1 == "images/sm_gray_box.gif"
INVARIANT
alive ⊆ COORD * COORD ∧ alive ≠ ∅
INITIALISATION
alive := glider
OPERATIONS
step = alive := { uv1 | uv1∈alive ∧ card(neigh[{uv1}] ∩ alive) = 2 }
∪
{ uv2 | uv2∈neigh[alive] ∧ /* restrict enumeration to neighbours */
card(neigh[{uv2}] ∩ alive)=3 }
END
```
%% Output
Loaded machine: GameOfLife
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec step
```
%% Output
Executed operation: step()
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec step
```
%% Output
Executed operation: step()
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec step
```
%% Output
Executed operation: step()
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_gray_box.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
```
......
Gilbreath_Card_Trick.ipynb
+ 2
− 0
View file @ 8521544f
%% Cell type:markdown id: tags:
# Gilbreath Card Trick
Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.
A while ago a member of the research group that created ProB and ProB2 stumbled across a short article [Unraveling a Card Trick](https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10) by Tony Hoare and Natarajan Shankar in the Dagstuhl library. In memory of Amir Pnueli they decided to model the problem as described in the article.
The article unravels a card trick by Gilbreath that has several phases:
* first you arrange 16 cards into a sequence of quartets with one card from each suit (Spade, Club, Heart, Diamond) in the same order. The example in the article is as follows: ⟨5♠⟩,⟨3♡⟩,⟨Q♣⟩,⟨8♢⟩, ⟨K♠⟩,⟨2♡⟩,⟨7♣⟩,⟨4♢⟩, ⟨8♠⟩,⟨J♡⟩,⟨9♣⟩,⟨A♢⟩
* you split the cards into two sequences. The example in the article is: ⟨5♠⟩,⟨3♡⟩,⟨Q♣⟩,⟨8♢⟩,⟨K♠⟩ and ⟨2♡⟩,⟨7♣⟩,⟨4♢⟩,⟨8♠⟩,⟨J♡⟩,⟨9♣⟩,⟨A♢⟩ .
* you reverse one of the sequences
* you perform a (not necessarily perfect) riffle shuffle of the two sequences
* the resulting final sequence is guaranteed to consist of a sequence of four quartets with one card from each suite.
In this notebook we are going to use the B machine they have created and visualise it.
%% Cell type:code id: tags:
``` prob
::load
MACHINE CardTrick
/* Translation by Michael Leuschel of Example in
"Unraveling a Card Trick" by Tony Hoare and Natarajan Shankar
in LNCS 6200, pp. 195-201, 2010.
DOI: 10.1007/978-3-642-13754-9_10
https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10
*/
SETS
SUIT={spade,club,heart,diamond}
DEFINITIONS
all == [spade,club,heart,diamond]; /* an arbitrary permutation of the suits */
/* check that in dst we can partition the deck into quartets where every suit occurs once: */
ok(dst) == #(a,b,c,d).(dst = a^b^c^d & size(a)=4 & size(b)=4 & size(c)=4 & size(d)=4 &
a : perm(SUIT) & b:perm(SUIT) & c:perm(SUIT) & d:perm(SUIT));
ANIMATION_FUNCTION_DEFAULT == {(1,0,"x"),(2,0,"y"),(3,0,"dest")};
ANIMATION_FUNCTION == ( {r,c,i| r=1 & c|->i:x} \/ {r,c,i| r=2 & c|->i:y} \/ {r,c,i| r=3 & c|->i:dest} );
ANIMATION_IMG1 == "images/French_suits_Spade.gif";
ANIMATION_IMG2 == "images/French_suits_Club.gif";
ANIMATION_IMG3 == "images/French_suits_Heart.gif";
ANIMATION_IMG4 == "images/French_suits_Diamond.gif";
CONSTANTS
initial
PROPERTIES
initial = all^all^all^all /* we fix the sequence; i.e., we perform symmetry reduction by hand; it should be possible to achieve this by ProB's symmetry reduction itself using a deferred set */
VARIABLES x,y,dest,reversed
INVARIANT
x:seq(SUIT) & y:seq(SUIT) & dest:seq(SUIT) & reversed:BOOL &
((x=<> & y=<>) => ok(dest)) /* the property we are interested in: after the riffle shuffle the sequence consists of four quartets, each containing every suit */
INITIALISATION
x,y : (x^y = initial) /* split the initial sequence into two: x and y */
|| dest := <> || reversed := FALSE
OPERATIONS
/* reverse one of the two decks */
Reverse = PRE reversed=FALSE THEN CHOICE x := rev(x) OR y := rev(y) END || reversed := TRUE END;
/* perform the riffle shuffle: transfer one card from either x or y to dest */
Shuffle1 = PRE x/=<> & reversed=TRUE THEN dest := dest<-last(x) || x:= front(x) END;
Shuffle2 = PRE y/=<> & reversed=TRUE THEN dest := dest<-last(y) || y:= front(y) END
END
```
%% Output
Loaded machine: CardTrick
%% Cell type:markdown id: tags:
First of all, we will make some observations.
In this machine, symmetry reduction is perfomed by hand, by forcing a particular order of the cards initially. You can find a version of this model without the symmetry reduction in our [Modelling Examples](https://www3.hhu.de/stups/handbook/prob2/modelling_examples.html#gilbreath-card-trick). For the purpose of this notebook, we will use this model however, because arguably model checking gives less insight into why the trick works than proof does.
A longer Why3 encoding can be found [here](http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html). A version of the model that can be run in TLC was additionally created and can be found in our [Modelling Examples](https://www3.hhu.de/stups/handbook/prob2/modelling_examples.html#gilbreath-card-trick), as well.
**Note:** To see the graphical visualisation, you will need to have the images for the `ANIMATION_FUNCTION` in your images folder.
Now we will set up the constants and initialize the machine. As you can see below, our machine has a lot of initialization options, you can use `card(x)=NUMBER` to quickly set a number of cards that should be initialized in x.
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: CardTrick
Sets: SUIT
Constants: initial
Variables: x, y, dest, reversed
Operations:
INITIALISATION()
INITIALISATION()
INITIALISATION()
INITIALISATION()
More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)
%% Cell type:code id: tags:
``` prob
:init card(x)=4
```
%% Output
Machine initialised using operation 5: $initialise_machine()
%% Cell type:markdown id: tags:
Here we can take a look at our options with the `:browse` command. You will see, that we can execute the reverse operation by typing in `:exec Reverse` and executing that command.
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: CardTrick
Sets: SUIT
Constants: initial
Variables: x, y, dest, reversed
Operations:
Reverse()
Reverse()
%% Cell type:code id: tags:
``` prob
:exec Reverse
```
%% Output
Executed operation: Reverse()
%% Cell type:markdown id: tags:
If we take another look at out options here, we can see, that we can now execute the Shuffle2 command. From here on you can try out the visualisation for yourself. Chose as many Shuffles as you want and look at the visualisation by using the `:show` command.
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: CardTrick
Sets: SUIT
Constants: initial
Variables: x, y, dest, reversed
Operations:
Shuffle1()
Shuffle2()
%% Cell type:code id: tags:
``` prob
:exec Shuffle2
```
%% Output
Executed operation: Shuffle2()
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">x</td>
<td style="padding:0px"><img alt="4" src="images/French_suits_Diamond.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/French_suits_Heart.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/French_suits_Club.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/French_suits_Spade.gif"/></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">y</td>
<td style="padding:0px"><img alt="1" src="images/French_suits_Spade.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/French_suits_Club.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/French_suits_Heart.gif"/></td>
<td style="padding:0px"><img alt="4" src="images/French_suits_Diamond.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/French_suits_Spade.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/French_suits_Club.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/French_suits_Heart.gif"/></td>
<td style="padding:0px"><img alt="4" src="images/French_suits_Diamond.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/French_suits_Spade.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/French_suits_Club.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/French_suits_Heart.gif"/></td>
</tr>
<tr>
<td style="padding:10px">dest</td>
<td style="padding:0px"><img alt="4" src="images/French_suits_Diamond.gif"/></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: CardTrick
Sets: SUIT
Constants: initial
Variables: x, y, dest, reversed
Operations:
Shuffle1()
Shuffle2()
%% Cell type:code id: tags:
``` prob
:exec Shuffle1
```
%% Output
Executed operation: Shuffle1()
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">x</td>
<td style="padding:0px"><img alt="4" src="images/French_suits_Diamond.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/French_suits_Heart.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/French_suits_Club.gif"/></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">y</td>
<td style="padding:0px"><img alt="1" src="images/French_suits_Spade.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/French_suits_Club.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/French_suits_Heart.gif"/></td>
<td style="padding:0px"><img alt="4" src="images/French_suits_Diamond.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/French_suits_Spade.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/French_suits_Club.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/French_suits_Heart.gif"/></td>
<td style="padding:0px"><img alt="4" src="images/French_suits_Diamond.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/French_suits_Spade.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/French_suits_Club.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/French_suits_Heart.gif"/></td>
</tr>
<tr>
<td style="padding:10px">dest</td>
<td style="padding:0px"><img alt="4" src="images/French_suits_Diamond.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/French_suits_Spade.gif"/></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: CardTrick
Sets: SUIT
Constants: initial
Variables: x, y, dest, reversed
Operations:
Shuffle1()
Shuffle2()
%% Cell type:code id: tags:
``` prob
```
......
N-Bishops.ipynb
+ 1
− 0
View file @ 8521544f
%% Cell type:markdown id: tags:
# N-Bishops Puzzle
Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.
This puzzle is a variation of the N-Queens puzzle. You can find the N-Queens puzzle in our modeling examples as well. In this puzzle we try to place as many bishops as possible on a n by n chess board. In contrast to the N-Queens puzzle, one can place more than one bishop per row. As such, we can now longer represent the positions of the bishops as an total function `1..n >-> 1..n`.
There are two encodings shown below. The first and following represents the bishops as a subset of the Cartesian product `(1..n)*(1..n)`, i.e., a set of positions (aka a binary relation on `1..n`).
First of all we have to load the machine, if you are struggeling with any operation of our jupyter kernel, try out `:help` or take a look at our `ProB Jupyter Noteboook Overview`.
%% Cell type:code id: tags:
``` prob
::load
MACHINE NBishopsSets
CONSTANTS n, nbishops, hasbishop
PROPERTIES
n=8 &
hasbishop <: (1..n)*(1..n) &
!(i,j).(i:1..n & j:1..n
=>
( (i,j): hasbishop
=>
(!k.(k:(i+1)..n =>
(k,j+k-i) /: hasbishop &
(k,j-k+i) /: hasbishop
))
))
& nbishops = card(hasbishop)
& nbishops >13
END
```
%% Output
Loaded machine: NBishopsSets
%% Cell type:markdown id: tags:
One can try and find the maximum number of bishops by gradually
increasing the lower limit for nbishops in the last line of the model
before the final END. The maximum number of bishops that can be placed
is 2*n - 2; see [here](http://mathworld.wolfram.com/BishopsProblem.html).
To show this graphically, we will now include the ANIMATION_FUNCTION for this example. The ANIMATION_FUNCTION has to be declared in the `DEFINITIONS` section as follows:
%% Cell type:code id: tags:
``` prob
::load
MACHINE NBishopsSets
DEFINITIONS
BWOFFSET(x,y) == (x+y) mod 2;
ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..n & c:1..n & i=(r+c) mod 2 } );
ANIMATION_FUNCTION == {r,c,i|(r,c):hasbishop & i= 2+BWOFFSET(r,c)} ;
ANIMATION_IMG0 == "images/ChessPieces/Chess_emptyl45.gif";
ANIMATION_IMG1 == "images/ChessPieces/Chess_emptyd45.gif";
ANIMATION_IMG2 == "images/ChessPieces/Chess_bll45.gif";
ANIMATION_IMG3 == "images/ChessPieces/Chess_bld45.gif";
SET_PREF_TK_CUSTOM_STATE_VIEW_PADDING == 1;
CONSTANTS n, nbishops, hasbishop
PROPERTIES
n=8 &
hasbishop <: (1..n)*(1..n) &
!(i,j).(i:1..n & j:1..n
=>
( (i,j): hasbishop
=>
(!k.(k:(i+1)..n =>
(k,j+k-i) /: hasbishop &
(k,j-k+i) /: hasbishop
))
))
& nbishops = card(hasbishop)
& nbishops >13
END
```
%% Output
Loaded machine: NBishopsSets
%% Cell type:markdown id: tags:
We will now initialise the machine and run the default setting to take a look at the animation.
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:markdown id: tags:
With the `:show` command from the jupyter kernel you can see the results of the N-Queens problem for yourself.
Please note, that the image paths given in the DEFINITIONS have to be relative to the jupyter notebook.
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
<td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
<td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
<td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
<td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
<td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
<td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
<td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
</tr>
<tr>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
</tr>
<tr>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
</tr>
<tr>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
</tr>
<tr>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
</tr>
<tr>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
</tr>
<tr>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
</tr>
<tr>
<td style="padding:1px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
<td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
<td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
<td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
<td style="padding:1px"><img alt="2" src="images/ChessPieces/Chess_bll45.gif"/></td>
<td style="padding:1px"><img alt="3" src="images/ChessPieces/Chess_bld45.gif"/></td>
<td style="padding:1px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:markdown id: tags:
For the chess pieces we have used the images available at [this site](https://commons.wikimedia.org/wiki/Category:SVG_chess_pieces). These images are available under the [Creative Commons](https://en.wikipedia.org/wiki/Creative_Commons)
[Attribution-Share Alike 3.0 Unported license](https://creativecommons.org/licenses/by-sa/3.0/deed.en). The same applies to the screenshots shown here.
%% Cell type:code id: tags:
``` prob
```
......
Peaceable_Armies_of_Queens.ipynb
+ 2
− 109
View file @ 8521544f
%% Cell type:markdown id: tags:
# Peaceable Armies of Queens
Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.
The paper [Models and symmetry breaking for 'peaceable armies of queens'](https://link.springer.com/chapter/10.1007/978-3-540-24664-0_19) by Smith, Petrie and Gent describes a challenging constraint programming problem.
A variation of the problem can be found on page 329 of the [Handbook on Constraint Programming](https://www.elsevier.com/books/handbook-of-constraint-programming/rossi/978-0-444-52726-4).
The challenge is to place two equal-sized armies of white and black queens onto a chessboard. We can distinguish between two problems:
* checking whether two armies of n queens can be placed on a dim*dim chessboard,
* for a given board of size dim*dim find the maximal size n of armies that can be placed onto the board, i.e., solving an optimisation problem.
In this notebook, we take a look at both of the problems and visualize them with the `ANIMATION_FUNCTION`.
%% Cell type:markdown id: tags:
## Checking
First we will take a look at the model for the checking problem. This problem is quite straightforward to encode in B. Most of the lines in the DEFINITIONS section are for our visualization with the `ANIMATION_FUNCTION`.
We will load (`::load`), set up the constants (`:constants`), and initialize the machine (`:init`), before we visualize it (`:show`).
%% Cell type:code id: tags:
``` prob
::load
MACHINE JustQueens
DEFINITIONS
SET_PREF_TIME_OUT == 1000000;
SET_PREF_MAX_INITIALISATIONS == 1;
ANIMATION_IMG0 == "images/ChessPieces/Chess_emptyl45.gif";
ANIMATION_IMG1 == "images/ChessPieces/Chess_emptyd45.gif";
ANIMATION_IMG2 == "images/ChessPieces/Chess_qdl45.gif";
ANIMATION_IMG3 == "images/ChessPieces/Chess_qdd45.gif";
ANIMATION_IMG6 == "images/ChessPieces/Chess_qll45.gif";
ANIMATION_IMG7 == "images/ChessPieces/Chess_qld45.gif";
BWOFFSET(xx,yy) == (xx+yy) mod 2;
ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..dim & c:1..dim & i=(r+c) mod 2 } );
ANIMATION_FUNCTION == ( UNION(k).(k:1..n| {(blackc(k),blackr(k),2+BWOFFSET(blackc(k),blackr(k)))}) \/
UNION(k).(k:1..n| {(whitec(k),whiter(k),6+BWOFFSET(whitec(k),whiter(k)))}) );
ORDERED(c,r) == (!i.(i:1..(n-1) => c(i) <= c(i+1)) &
!i.(i:1..(n-1) => (c(i)=c(i+1) => r(i) < r(i+1))))
CONSTANTS n, dim, blackc, blackr, whitec, whiter
PROPERTIES
n = 8 & dim = 8 &
blackc : 1..n --> 1..dim &
whitec : 1..n --> 1..dim &
blackr : 1..n --> 1..dim &
whiter : 1..n --> 1..dim &
ORDERED(blackc,blackr) & /* ensures proper ordering + that we do not place two queens on same square */
ORDERED(whitec,whiter) &
!(i,j).(i:1..n & j:1..n => blackc(i) /= whitec(j)) &
!(i,j).(i:1..n & j:1..n => blackr(i) /= whiter(j)) &
!(i,j).(i:1..n & j:1..n => blackr(i) /= whiter(j) + (blackc(i)-whitec(j))) &
!(i,j).(i:1..n & j:1..n => blackr(i) /= whiter(j) - (blackc(i)-whitec(j))) &
whitec(1) < blackc(1) /* symmetry breaking */
END
```
%% Output
Loaded machine: JustQueens
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/ChessPieces/Chess_qll45.gif"/></td>
<td style="padding:0px"><img alt="7" src="images/ChessPieces/Chess_qld45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/ChessPieces/Chess_qdl45.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/ChessPieces/Chess_qdl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/ChessPieces/Chess_qdl45.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="7" src="images/ChessPieces/Chess_qld45.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/ChessPieces/Chess_qll45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="7" src="images/ChessPieces/Chess_qld45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/ChessPieces/Chess_qll45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="7" src="images/ChessPieces/Chess_qld45.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/ChessPieces/Chess_qll45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:markdown id: tags:
### Setting up constants
This machine is a great one to understand setting up various constants within jupyter notebook.
If you reload the machine (by pressing `SHIFT`+`ENTER` in the code cell with our machine code) you can change the constants for the queens to change their positions on the board.
Try it out! Reload the machine and run the next cell. Then, initialise and visualise as ususal.
You can change the collums of the queens with the constants `blackc`/`whitec` and the rows with the constants `blackr`/`whiter`.
%% Cell type:code id: tags:
``` prob
:constants blackc(2)=2 & blackr(2)=6
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:constants whitec(2)=4 & whiter(2)=4
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/ChessPieces/Chess_qll45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/ChessPieces/Chess_qdl45.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/ChessPieces/Chess_qll45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/ChessPieces/Chess_qll45.gif"/></td>
<td style="padding:0px"><img alt="7" src="images/ChessPieces/Chess_qld45.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/ChessPieces/Chess_qll45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/ChessPieces/Chess_qll45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/ChessPieces/Chess_qll45.gif"/></td>
<td style="padding:0px"><img alt="7" src="images/ChessPieces/Chess_qld45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:markdown id: tags:
## Optimization
One can obviously use the above model to try and manually find a maximal value of n for a given board size dim. Below, we have encoded this process as B constraints, by setting up the problem twice: once for the army size n and a second time for army size n+1. The second encoding is wrapped into a negated existential quantification.
ProB solves this optimisation problem in about 660 seconds for a board size of 8. This is very competitive with the timings reported in the above mentioned constraint solving paper using new symmetry breaking techniques and much more low-level encoding on state of the art constraint solving libraries such as ILOG.
To find out how long our jupyter notebook kernel needs to run this, we can use the command `:time`:
Times and specs:
```
Acer TravelMate X349-G2-M,
8 GB RAM,
Intel(R) Core(TM) i5-7200U CPU @ 2.50GHz 2.70 GHz Prozessor,
Windows 10 OS
dim=5 --> optimum n=4 0.326799900 secs
dim=6 --> optimum n=5 0.954069900 secs
dim=7 --> optimum n=7 19.829867700 secs
dim=8 --> optimum n=9 658.281314000 secs
```
If you want to check out the optimization for dim=5, dim=6, dim=8, you can do so by changing the constant in the `PROPERTIES` section of the machine code cell.
*EDITOR'S NOTE* : 660 seconds are 11 minutes, and that is why we only recomment to work with dim=5, dim=6 and dim=7 for the purposes of this notebook. However, if you really want to try out dim=8... You know how to.
%% Cell type:code id: tags:
``` prob
::load
MACHINE JustQueens_FindOptimal_CBC
DEFINITIONS
SET_PREF_TIME_OUT == 1000000;
SET_PREF_MAX_INITIALISATIONS == 1;
ANIMATION_IMG0 == "images/ChessPieces/Chess_emptyl45.gif";
ANIMATION_IMG1 == "images/ChessPieces/Chess_emptyd45.gif";
ANIMATION_IMG2 == "images/ChessPieces/Chess_qdl45.gif";
ANIMATION_IMG3 == "images/ChessPieces/Chess_qdd45.gif";
ANIMATION_IMG6 == "images/ChessPieces/Chess_qll45.gif";
ANIMATION_IMG7 == "images/ChessPieces/Chess_qld45.gif";
BWOFFSET(xx,yy) == (xx+yy) mod 2;
ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..dim & c:1..dim & i=(r+c) mod 2 } );
ANIMATION_FUNCTION == ( UNION(k).(k:1..n| {(blackc(k),blackr(k),2+BWOFFSET(blackc(k),blackr(k)))}) \/
UNION(k).(k:1..n| {(whitec(k),whiter(k),6+BWOFFSET(whitec(k),whiter(k)))}) );
ORDERED(c,r,nn) == (!i.(i:1..(nn-1) => c(i) <= c(i+1)) &
!i.(i:1..(nn-1) => (c(i)=c(i+1) => r(i) < r(i+1))));
CHECK_TYPE(bc,br,wc,wr,nn) == (
bc : 1..nn --> 1..dim &
wc : 1..nn --> 1..dim &
br : 1..nn --> 1..dim &
wr : 1..nn --> 1..dim );
CHECK_DIAGONALS(bc,br,wc,wr,nn) == (
!(i,j).(i:1..nn & j:1..nn => bc(i) /= wc(j)) &
!(i,j).(i:1..nn & j:1..nn => br(i) /= wr(j)) &
!(i,j).(i:1..nn & j:1..nn => br(i) /= wr(j) + (bc(i)-wc(j))) &
!(i,j).(i:1..nn & j:1..nn => br(i) /= wr(j) - (bc(i)-wc(j)))
)
CONSTANTS n, dim, blackc, blackr, whitec, whiter
PROPERTIES
n : 1..16 & dim = 7 & // <------------------------------------YOU CAN CHANGE dim HERE
CHECK_TYPE(blackc, blackr, whitec, whiter, n) &
ORDERED(blackc,blackr,n) & /* ensures proper ordering + that we do not place two queens on same square */
ORDERED(whitec,whiter,n) &
CHECK_DIAGONALS(blackc, blackr, whitec, whiter, n) &
whitec(1) < blackc(1) /* symmetry breaking */ &
/* Repeat constraints for n+1 and assert that it cannot be solved */
not( #(n1,blackc1, blackr1, whitec1, whiter1).
(n1=n+1 & /* n1:2..17 & */
CHECK_TYPE(blackc1, blackr1, whitec1, whiter1, n1) &
ORDERED(blackc1,blackr1,n1) & /* ensures proper ordering + that we do not place two queens on same square */
ORDERED(whitec1,whiter1,n1) &
CHECK_DIAGONALS(blackc1, blackr1, whitec1, whiter1, n1) &
whitec1(1) < blackc1(1) /* symmetry breaking */
)
)
END
```
%% Output
Loaded machine: JustQueens_FindOptimal_CBC
%% Cell type:code id: tags:
``` prob
:time :constants
```
%% Output
Execution time: 17.606007400 seconds
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags:
``` prob
n
```
%% Output
$7$
7
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="7" src="images/ChessPieces/Chess_qld45.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/ChessPieces/Chess_qll45.gif"/></td>
<td style="padding:0px"><img alt="7" src="images/ChessPieces/Chess_qld45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/ChessPieces/Chess_qdl45.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="6" src="images/ChessPieces/Chess_qll45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="7" src="images/ChessPieces/Chess_qld45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="7" src="images/ChessPieces/Chess_qld45.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/ChessPieces/Chess_qll45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/ChessPieces/Chess_qdl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/ChessPieces/Chess_qdl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/ChessPieces/Chess_emptyd45.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/ChessPieces/Chess_emptyl45.gif"/></td>
<td style="padding:0px"><img alt="3" src="images/ChessPieces/Chess_qdd45.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/ChessPieces/Chess_qdl45.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:help
```
%% Output
Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use `:load` to load an external machine file.
You can also use any of the following commands. For more help on a particular command, run `:help commandname`.
## Evaluation
* `:eval` - Evaluate a formula and display the result.
* `:solve` - Solve a predicate with the specified solver.
* `:table` - Display an expression as a table.
* `:type` - Display the static type of a formula.
* `:prettyprint` - Pretty-print a predicate.
* `:let` - Evaluate an expression and store it in a local variable.
* `:unlet` - Remove a local variable.
* `:assert` - Ensure that the predicate is true, and show an error otherwise.
## Animation
* `::load` - Load a B machine from the given source code.
* `:load` - Load a machine from a file.
* `:constants` - Set up the current machine's constants.
* `:init` - Initialise the current machine with the specified predicate
* `:exec` - Execute an operation.
* `:browse` - Show information about the current state.
* `:trace` - Display all states and executed operations in the current trace.
* `:goto` - Go to the state with the specified index in the current trace.
* `:find` - Try to find a state for which the given predicate is true (in addition to the machine's invariant).
## Visualisation
* `:show` - Show the machine's animation function visualisation for the current state.
* `:dot` - Execute and show a dot visualisation.
## Verification
* `:check` - Check the machine's properties, invariant, or assertions in the current state.
* `:modelcheck` - Run the ProB model checker on the current model.
## Other
* `::render` - Render some content with the specified MIME type.
* `:bsymb` - Load all bsymb.sty command definitions, so that they can be used in $\LaTeX$ formulas in Markdown cells.
* `:groovy` - Evaluate the given Groovy expression.
* `:help` - Display help for a specific command, or general help about the REPL.
* `:pref` - View or change the value of one or more preferences.
* `:stats` - Show statistics about the state space.
* `:time` - Execute the given command and measure how long it takes to execute.
* `:version` - Display version info about the ProB CLI and ProB 2.
Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use :load to load an external machine file.
You can also use any of the following commands. For more help on a particular command, run :help commandname.
Evaluation:
:eval - Evaluate a formula and display the result.
:solve - Solve a predicate with the specified solver.
:table - Display an expression as a table.
:type - Display the static type of a formula.
:prettyprint - Pretty-print a predicate.
:let - Evaluate an expression and store it in a local variable.
:unlet - Remove a local variable.
:assert - Ensure that the predicate is true, and show an error otherwise.
Animation:
::load - Load a B machine from the given source code.
:load - Load a machine from a file.
:constants - Set up the current machine's constants.
:init - Initialise the current machine with the specified predicate
:exec - Execute an operation.
:browse - Show information about the current state.
:trace - Display all states and executed operations in the current trace.
:goto - Go to the state with the specified index in the current trace.
:find - Try to find a state for which the given predicate is true (in addition to the machine's invariant).
Visualisation:
:show - Show the machine's animation function visualisation for the current state.
:dot - Execute and show a dot visualisation.
Verification:
:check - Check the machine's properties, invariant, or assertions in the current state.
:modelcheck - Run the ProB model checker on the current model.
Other:
::render - Render some content with the specified MIME type.
:bsymb - Load all bsymb.sty command definitions, so that they can be used in $\LaTeX$ formulas in Markdown cells.
:groovy - Evaluate the given Groovy expression.
:help - Display help for a specific command, or general help about the REPL.
:pref - View or change the value of one or more preferences.
:stats - Show statistics about the state space.
:time - Execute the given command and measure how long it takes to execute.
:version - Display version info about the ProB CLI and ProB 2.
%% Cell type:code id: tags:
``` prob
```
......
SEND-MORE-MONEY.ipynb
+ 10
− 1
View file @ 8521544f
%% Cell type:markdown id: tags:
# SEND-MORE-MONEY
In this jupyter notebook, we will study how to solve the famous [verbal arithmetic SEND-MORE-MONEY](https://en.wikipedia.org/wiki/Verbal_arithmetic) puzzle. The task is to find the digits S,E,N,D,M,O,R,Y such that the addition of SEND to MORE leads the decimal number MONEY.
Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.
In this jupyter notebook, we will take a look on how to solve the famous [verbal arithmetic SEND-MORE-MONEY](https://en.wikipedia.org/wiki/Verbal_arithmetic) puzzle. The task is to find the digits S,E,N,D,M,O,R,Y such that the addition of SEND to MORE leads the decimal number MONEY.
The quickest way is to use the ProB Logic Calculator, which is implemented in Jupyter notebook. To solve the puzzle, simply type in:
`{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` and press enter:
%% 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:
## Explanation
Now let us review the individual conjuncts of the B encoding of the puzzle: The following specifies that S,E,N,D,M,O,R,Y are all digits.
Note that `<:` is the subset operator in B:
`{S,E,N,D, M,O,R, Y} <: 0..9`
An alternative, slightly longer, encoding would have been to write:
`S:0..9 & E:0..9 & N:0..9 & D:0..9 & M:0..9 & O:0..9 & R:0..9 & Y:0..9`
The following conjunct specifies that the S and M cannot be 0:
`S>0 & M>0`
The next conjunct specifies that all digits are distinct:
`card({S,E,N,D, M,O,R, Y})=8`
Note that an alternative, but much longer encoding would have been to specify inequalities:
`S /= E & S /= N & S /= D & … & R/=Y`
Finally, the last conjunct expresses the sum constraint:
`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:markdown id: tags:
## Alternative Solutions
We are still not sure if this is the only solution. One way to ensure this is to compute a set comprehension with all solutions:
`{S,E,N,D,M,O,R,Y|{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|{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
$\{(9\mapsto 5\mapsto 6\mapsto 7\mapsto 1\mapsto 0\mapsto 8\mapsto 2)\}$
{(9↦5↦6↦7↦1↦0↦8↦2)}
%% Cell type:markdown id: tags:
## Wrapping predicate into B machine
Another alternative is to wrap the predicate into a full B machine with the following content:
%% Cell type:code id: tags:
``` prob
::load
MACHINE SendMoreMoney
CONSTANTS S,E,N,D, M,O,R, Y
PROPERTIES
{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
END
```
%% Output
Loaded machine: SendMoreMoney
%% Cell type:markdown id: tags:
To run this example, you will need to setup the constants and initialise the machine with the following commands:
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:markdown id: tags:
To see the result, we will create the following table:
%% Cell type:code id: tags:
``` prob
:table (S,E,N,D, M,O,R, Y)
```
%% Output
|S|E|N|D|M|O|R|Y|
|---|---|---|---|---|---|---|---|
|$9$|$5$|$6$|$7$|$1$|$0$|$8$|$2$|
S E N D M O R Y
9 5 6 7 1 0 8 2
%% Cell type:markdown id: tags:
## KISS * KISS = PASSION
A similar puzzle, this times involving multiplication is the KISS * KISS = PASSION puzzle.
Here we again have distinct digits K, I, S, P, A, O, N such that the square of KISS equals the decimal number passion.
The puzzle can be described and solved in a fashion very similar to the problem above:
`{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 id: tags:
To make sure, that we don't use the variables from our machine loaded above, we reset our machine to be empty:
%% Cell type:code id: tags:
``` prob
::load
MACHINE empty
END
```
%% Output
Loaded machine: empty
%% Cell type:code id: tags:
``` 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
$\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
```
......
Untitled.ipynb → waiting_for_features/Jobs_Puzzle.ipynb
+ 17
− 92
View file @ 8521544f
%% Cell type:markdown id: tags:
# The Jobs Puzzle
Based on *Michael Leuschel, David Schneider. Towards B as a High-Level Constraint Modeling Language. In Yamine Ait Amer, Klaus-Dieter Schewe (ed.): Abstract State Machines, Alloy, B, TLA, VDM, and Z, Springer Berlin Heidelberg, 8477: 101-116, 2014.*
This puzzle was originally published in 1984 by [Wos et al., 1984](https://www.mcs.anl.gov/research/projects/AR/book1.html) as part of a collection of puzzles for automatic reasoners. A reference implementation of the puzzle, by one of the authors of the book, using [OTTER, 2003](https://arxiv.org/abs/cs/0310056).
The puzzle consists of eight statements that describe the problem domain and provide some constraints on the elements of the domain. The problem is about a set of people and a set of jobs; the question posed by the puzzle is: who holds which job? The text of the puzzle as presented in "The jobs puzzle: A challenge for logical expressibility and automated reasoning."[S. C. Shapiro, 2011](https://cse.buffalo.edu/~shapiro/Papers/SS11-06-017.pdf) is as follows:
* There are four people: Roberta, Thelma, Steve, and Pete.
* Among them, they hold eight different jobs.
* Each holds exactly two jobs.
* The jobs are: chef, guard, nurse, clerk, police officer (gender not implied), teacher, actor, and boxer.
* The job of nurse is held by a male.
* The husband of the chef is the clerk.
* Roberta is not a boxer.
* Pete has no education past the ninth grade.
* Roberta, the chef, and the police officer went golfing together.
What makes this puzzle interesting for automatic reasoners, is that not all the information required to solve the puzzle is provided explicitly in the text.
The puzzle can only be solved if certain implicit assumptions about the world are taken into account, such as: the names in the puzzle denote gender or that some of the job names imply the gender of the person that holds it.
%% Cell type:markdown id: tags:
## Shapiro's Challenge
Shapiro, following the original authors' remarks, that formalizing the puzzle was at times hard and tendious, identified three challenges posed by the puat times hard and tedious, identified three challenges posed by the puzzle with regard to automatic reasoners. According to Shapiro, the challenges posed by the jobs puzzle are to:
1. formalize it in a non-difficult, non-tedious way
2. formalize it in a way that adheres closely to the English statement of the puzzle
3. have an automated general-purpose commonsense reasoner that can accept that formalization and solve the puzzle quickly.
Any formalization also needs to encode the implicit knowledge used to solve the puzzle for the automatic reasoners while still trying to satisfy the aspects mentioned above. Addressing this challenge makes this puzzle a good case-study for the expressiveness of B to formalize such a problem.
%% Cell type:markdown id: tags:
## A Solution to the Jobs Puzzle using B
The B encoding of the puzzle uses plain predicate logic,
combined with set theory and arithmetic. We will show how this
enables a very concise encoding of the problem, staying very close to the natural language requirements. Moreover, the puzzle can be quickly solved using the constraint solving capabilities of ProB. Following the order of the sentences in the puzzle we will discuss one or more possibilities to formalize them using B.
To express "*There are four people: Roberta, Thelma, Steve, and Pete*" we define a set of people, that holds the list of names:
%% Cell type:code id: tags:
``` prob
:let PEOPLE {"Roberta", "Thelma", "Steve", "Pete"}
```
%% Output
$\{\text{"Pete"},\text{"Roberta"},\text{"Steve"},\text{"Thelma"}\}$
{"Pete","Roberta","Steve","Thelma"}
%% Cell type:markdown id: tags:
We are using strings here to describe the elements of the set. This has the advantage, that the elements of the set are implicitly different.
Alternatively, we could use enumerated or deferred sets defined in the SETS section of a B machine. As stated above we need some additional information that is not included in the puzzle to solve it.
The first bit of information is that the names used in the puzzle imply the gender. In order to express this information we create two sets, MALE and FEMALE which are subsets of PEOPLE and contain the corresponding names.
%% Cell type:code id: tags:
``` prob
:let FEMALE {"Roberta", "Thelma"}
```
%% Output
$\{\text{"Roberta"},\text{"Thelma"}\}$
{"Roberta","Thelma"}
%% Cell type:code id: tags:
``` prob
:let MALE {"Steve", "Pete"}
```
%% Output
$\{\text{"Pete"},\text{"Steve"}\}$
{"Pete","Steve"}
%% Cell type:markdown id: tags:
The next statement of the puzzle is: "*among them, they hold eight different jobs*". This can be formalized in B using a function that maps from a job to the corresponding person that holds this job using a total surjection from JOBS to PEOPLE.
To use that statement, however we have to define JOBS, or the fourth statement.
%% Cell type:code id: tags:
``` prob
:let JOBS {"chef", "guard", "nurse", "clerk", "police", "teacher", "actor", "boxer"}
```
%% Output
$\{\text{"actor"},\text{"boxer"},\text{"chef"},\text{"clerk"},\text{"guard"},\text{"nurse"},\text{"police"},\text{"teacher"}\}$
{"actor","boxer","chef","clerk","guard","nurse","police","teacher"}
%% Cell type:markdown id: tags:
Now we can see what Holds Job will do.
%% Cell type:code id: tags:
``` prob
HoldsJob : JOBS -->> PEOPLE
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{HoldsJob} = \{(\text{"actor"}\mapsto\text{"Steve"}),(\text{"boxer"}\mapsto\text{"Thelma"}),(\text{"chef"}\mapsto\text{"Pete"}),(\text{"clerk"}\mapsto\text{"Pete"}),(\text{"guard"}\mapsto\text{"Pete"}),(\text{"nurse"}\mapsto\text{"Pete"}),(\text{"police"}\mapsto\text{"Pete"}),(\text{"teacher"}\mapsto\text{"Roberta"})\}$
* $\mathit{JOBS} = \{\text{"actor"},\text{"boxer"},\text{"chef"},\text{"clerk"},\text{"guard"},\text{"nurse"},\text{"police"},\text{"teacher"}\}$
* $\mathit{PEOPLE} = \{\text{"Pete"},\text{"Roberta"},\text{"Steve"},\text{"Thelma"}\}$
* $\mathit{MALE} = \{\text{"Pete"},\text{"Steve"}\}$
* $\mathit{FEMALE} = \{\text{"Roberta"},\text{"Thelma"}\}$
TRUE
Solution:
HoldsJob = {("actor"↦"Steve"),("boxer"↦"Thelma"),("chef"↦"Pete"),("clerk"↦"Pete"),("guard"↦"Pete"),("nurse"↦"Pete"),("police"↦"Pete"),("teacher"↦"Roberta")}
JOBS = {"actor","boxer","chef","clerk","guard","nurse","police","teacher"}
PEOPLE = {"Pete","Roberta","Steve","Thelma"}
MALE = {"Pete","Steve"}
FEMALE = {"Roberta","Thelma"}
%% Cell type:markdown id: tags:
Since we have not yet added any additional information, the Jobs are just randomly assigned to each Person.
Although redundant, as we will see below, to express “*Among them, they hold eight different jobs*” we can add the assertion that the cardinality of HoldsJob is 8.
This is possible, because in B functions and relations can be treated as sets of pairs, where each pair consists of an element of the domain and the corresponding element from the range of the relation.
%% Cell type:code id: tags:
``` prob
HoldsJob : JOBS -->> PEOPLE & card(HoldsJob) = 8
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{HoldsJob} = \{(\text{"actor"}\mapsto\text{"Steve"}),(\text{"boxer"}\mapsto\text{"Thelma"}),(\text{"chef"}\mapsto\text{"Pete"}),(\text{"clerk"}\mapsto\text{"Pete"}),(\text{"guard"}\mapsto\text{"Pete"}),(\text{"nurse"}\mapsto\text{"Pete"}),(\text{"police"}\mapsto\text{"Pete"}),(\text{"teacher"}\mapsto\text{"Roberta"})\}$
* $\mathit{JOBS} = \{\text{"actor"},\text{"boxer"},\text{"chef"},\text{"clerk"},\text{"guard"},\text{"nurse"},\text{"police"},\text{"teacher"}\}$
* $\mathit{PEOPLE} = \{\text{"Pete"},\text{"Roberta"},\text{"Steve"},\text{"Thelma"}\}$
* $\mathit{MALE} = \{\text{"Pete"},\text{"Steve"}\}$
* $\mathit{FEMALE} = \{\text{"Roberta"},\text{"Thelma"}\}$
TRUE
Solution:
HoldsJob = {("actor"↦"Steve"),("boxer"↦"Thelma"),("chef"↦"Pete"),("clerk"↦"Pete"),("guard"↦"Pete"),("nurse"↦"Pete"),("police"↦"Pete"),("teacher"↦"Roberta")}
JOBS = {"actor","boxer","chef","clerk","guard","nurse","police","teacher"}
PEOPLE = {"Pete","Roberta","Steve","Thelma"}
MALE = {"Pete","Steve"}
FEMALE = {"Roberta","Thelma"}
%% Cell type:markdown id: tags:
Constraining the jobs each person holds, the puzzle states: “*Each holds exactly two jobs*”. To express this we use the inverse relation of HoldsJob, it maps a PERSON to the JOBS associated to her. The inverse function or relation is expressed in B using the ~ operator.
For readability we assign the inverse of HoldsJob to a variable called JobsOf. JobsOf is in this case is a relation, because, as stated above, each person holds two jobs.
First of all, we have to add HoldsJob to our globals, however.
%% Cell type:code id: tags:
``` prob
:let HoldsJob JOBS -->> PEOPLE
```
%% Output
de.prob.animator.domainobjects.EvaluationException: de.be4.classicalb.core.parser.exceptions.BCompoundException: [2,26] expecting: identifier literal
%% Cell type:markdown id: tags:
Because JobsOf is a relation and not a function, in order to read the values, we need to use B’s relational image operator. This operator maps a subset of the domain to a subset of the range, instead of a single value. To read the jobs Steve holds, the relational image of JobsOf is used as shown below:
%% Cell type:code id: tags:
``` prob
:let card(HoldsJob) 8
```
%% Output
$8$
8
%% Cell type:code id: tags:
``` prob
:let JobsOf HoldsJob~
```
%% Output
%% Cell type:markdown id: tags:
de.prob.animator.domainobjects.EvaluationException: de.be4.classicalb.core.parser.exceptions.BCompoundException: [2,26] expecting: identifier literal
### Needs possibility to save executed expressions
%% Cell type:code id: tags:
``` prob
```
......
Nine_Prisoners.ipynb → waiting_for_features/Nine_Prisoners.ipynb
+ 0
− 0
View file @ 8521544f
File moved
Sudoku_Solved.ipynb → waiting_for_features/Sudoku_Solved.ipynb
+ 0
− 0
View file @ 8521544f
File moved
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment