Skip to content
Snippets Groups Projects
Commit 6d9b9466 authored by dgelessus's avatar dgelessus
Browse files

Add .gitignore and remove generated files

parent 1cbe29fb
No related branches found
No related tags found
No related merge requests found
Expand all Show whitespace changes
Inline Side-by-side
Showing
with 14 additions and 8349 deletions
.gitignore 0 → 100644
+ 14
− 0
View file @ 6d9b9466
# Jupyter notebook checkpoints
.ipynb_checkpoints/
# nbconvert HTML/slides output
*.html
# nbconvert LaTeX output
*.aux
*.dvi
*.log
*.out
*.pdf
*.svg
*.tex
.ipynb_checkpoints/Apples_and_Oranges-checkpoint.ipynb deleted 100644 → 0
+ 0
− 293
View file @ 1cbe29fb
%% Cell type:markdown id: tags:
# Apples and Oranges
Use `:help` to get an overview for the jupyter notebook commands.
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
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
* 0: `SETUP_CONSTANTS()` **(current)**
-1: Root state
0: SETUP_CONSTANTS() (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:code id: tags:
``` prob
```
.ipynb_checkpoints/Argumentation_Theory-checkpoint.ipynb deleted 100644 → 0
+ 0
− 999
View file @ 1cbe29fb
This diff is collapsed.
.ipynb_checkpoints/Bridges_Puzzle-checkpoint.ipynb deleted 100644 → 0
+ 0
− 484
View file @ 1cbe29fb
%% Cell type:markdown id: tags:
# Bridges Puzzle (Hashiwokakero)
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 [Hashiwokakero](https://en.wikipedia.org/wiki/Hashiwokakero) Puzzle is a logical puzzle where one has to build bridges between islands. The puzzle is also known under the name Ai-Ki-Ai. The puzzles can also be [played online](http://www.puzzle-bridges.com).
The requirements for this puzzle are as follows:
* the goal is to build bridges between islands so as to generate a connected graph
* every island has a number on it, indicating exactly how many bridges should be linked with the island
* there is an upper bound (MAXBRIDGES) on the number of bridges that can be built-between two islands
* bridges cannot cross each other
A B model for this puzzle can be found below. The constants and sets of the model are as follows:
* N are the nodes (islands); we have added a constant ignore where one can stipulate which islands should be ignored in this puzzle
* nl (number of links) stipulates for each island how many bridges it should be linked with
* xc, yc are the x- and y-coordinates for every island
A simple puzzle with four islands would be defined as follows, assuming
the basic set N is defined as `N = {a,b,c,d,e,f,g,h,i,j,k,l,m,n}`:
~~~~
xc(a)=0 & xc(b)=1 & xc(c)=0 & xc(d) = 1 &
yc(a)=0 & yc(b)=0 & yc(c)=1 & yc(d) = 1 &
nl = {a|->2, b|->2, c|->2, d|->2} &
ignore = {e,f,g,h,i,j,k,l,m,n}
~~~~
Below we will use a more complicated puzzle to illustrate the B model.
The model then contains the following derived constants:
* plx,ply: the possible links between islands on the x- and y-axis respectively
* pl: the possible links both on the x- and y-axis combined
* cs: the conflict set of links which overlap, i.e., one cannot build bridges on both links (a,b) when the pair (a,b) is in cs
* connected: the set of links on which at least one bridge was built
The model also sets up the goal constant `sol` which maps every link in `pl` to a number indicating how many bridges are built on it. The model also stipulates that the graph set up by connected generates a fully connected graph.
%% Cell type:code id: tags:
``` prob
::load DOT=/usr/bin/dot
MACHINE Bridges
DEFINITIONS
MAXBRIDGES==2;
LINKS == 1..(MAXBRIDGES*4);
COORD == 0..10;
p1 == prj1(nodes,nodes);
p2 == prj2(nodes,nodes);
p1i == prj1(nodes,INTEGER)
SETS
N = {a,b,c,d,e,f,g,h,i,j,k,l,m,n}
CONSTANTS nodes, ignore, nl, xc,yc, plx,ply,pl, cs, sol, connected
PROPERTIES
nodes = N \ ignore &
// target number of links per node:
nl : nodes --> LINKS & /* number of links */
// coordinates of nodes
xc: nodes --> COORD & yc: nodes --> COORD &
// possible links:
pl : nodes <-> nodes &
plx : nodes <-> nodes &
ply : nodes <-> nodes &
plx = {n1,n2 | xc(n1)=xc(n2) & n1 /= n2 & yc(n2)>yc(n1) &
!n3.(xc(n3)=xc(n1) => yc(n3) /: yc(n1)+1..yc(n2)-1) } &
ply = {n1,n2 | yc(n1)=yc(n2) & n1 /= n2 & xc(n2)>xc(n1) &
!n3.(yc(n3)=yc(n1) => xc(n3) /: xc(n1)+1..xc(n2)-1)} &
pl = plx \/ ply &
// compute conflict set (assumes xc,yc coordinates ordered in plx,ply)
cs = {pl1,pl2 | pl1:plx & pl2:ply &
xc(p1(pl1)): xc(p1(pl2))+1..xc(p2(pl2))-1 &
yc(p1(pl2)): yc(p1(pl1))+1..yc(p2(pl1))-1} &
sol : pl --> 0..MAXBRIDGES &
!nn.(nn:nodes => SIGMA(l).(l:pl &
(p1(l)=nn or p2(l)=nn)|sol(l))=nl(nn)) &
!(pl1,pl2).( (pl1,pl2):cs => sol(pl1)=0 or sol(pl2)=0) & // no conflicts
// check graph connected
connected = {pl|sol(pl)>0} &
closure1(connected \/ connected~)[{a}] = {nn|nn:nodes & nl(nn)>0} &
// encoding of puzzle
// A puzzle from bridges.png
xc(a)=1 & yc(a)=1 & nl(a)=4 &
xc(b)=1 & yc(b)=4 & nl(b)=6 &
xc(c)=1 & yc(c)=6 & nl(c)=3 &
xc(d)=2 & yc(d)=2 & nl(d)=1 &
xc(e)=2 & yc(e)=5 & nl(e)=2 &
xc(f)=3 & yc(f)=2 & nl(f)=4 &
xc(g)=3 & yc(g)=4 & nl(g)=6 &
xc(h)=3 & yc(h)=5 & nl(h)=4 &
xc(i)=4 & yc(i)=3 & nl(i)=3 &
xc(j)=4 & yc(j)=6 & nl(j)=3 &
xc(k)=5 & yc(k)=2 & nl(k)=1 &
xc(l)=6 & yc(l)=1 & nl(l)=4 &
xc(m)=6 & yc(m)=3 & nl(m)=5 &
xc(n)=6 & yc(n)=5 & nl(n)=2 &
ignore = {}
END
```
%% Output
Loaded machine: Bridges
%% 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:
After setting the constants and initialising the machine with the above commands, one can see that the solution for this puzzle, which is saved in `sol`, is the following:
(Simply type in `sol` to get the value for it.)
%% Cell type:code id: tags:
``` prob
sol
```
%% Output
$\{(\mathit{a}\mapsto \mathit{b}\mapsto 2),(\mathit{a}\mapsto \mathit{l}\mapsto 2),(\mathit{b}\mapsto \mathit{c}\mapsto 2),(\mathit{b}\mapsto \mathit{g}\mapsto 2),(\mathit{c}\mapsto \mathit{j}\mapsto 1),(\mathit{d}\mapsto \mathit{e}\mapsto 0),(\mathit{d}\mapsto \mathit{f}\mapsto 1),(\mathit{e}\mapsto \mathit{h}\mapsto 2),(\mathit{f}\mapsto \mathit{g}\mapsto 2),(\mathit{f}\mapsto \mathit{k}\mapsto 1),(\mathit{g}\mapsto \mathit{h}\mapsto 2),(\mathit{h}\mapsto \mathit{n}\mapsto 0),(\mathit{i}\mapsto \mathit{j}\mapsto 2),(\mathit{i}\mapsto \mathit{m}\mapsto 1),(\mathit{l}\mapsto \mathit{m}\mapsto 2),(\mathit{m}\mapsto \mathit{n}\mapsto 2)\}$
{(a↦b↦2),(a↦l↦2),(b↦c↦2),(b↦g↦2),(c↦j↦1),(d↦e↦0),(d↦f↦1),(e↦h↦2),(f↦g↦2),(f↦k↦1),(g↦h↦2),(h↦n↦0),(i↦j↦2),(i↦m↦1),(l↦m↦2),(m↦n↦2)}
%% Cell type:markdown id: tags:
## Adding Graphical Visualisation
To show the solution graphically, we can add the following to the
`DEFINITIONS` clause in the model:
~~~~
CUSTOM_GRAPH_NODES == {n,w,w2|(n|->w):nl & w=w2}; // %n1.(n1:nodes|nl(n1));
CUSTOM_GRAPH_EDGES == {n1,w,n2|n1:nl & n2:nl & (p1i(n1),p1i(n2),w):sol}
~~~~
%% Cell type:code id: tags:
``` prob
::load
MACHINE Bridges
DEFINITIONS
MAXBRIDGES==2;
LINKS == 1..(MAXBRIDGES*4);
COORD == 0..10;
p1 == prj1(nodes,nodes);
p2 == prj2(nodes,nodes);
p1i == prj1(nodes,INTEGER);
CUSTOM_GRAPH_NODES == {n,w,w2|(n|->w):nl & w=w2}; // %n1.(n1:nodes|nl(n1));
CUSTOM_GRAPH_EDGES == {n1,w,n2|n1:nl & n2:nl & (p1i(n1),p1i(n2),w):sol}
SETS
N = {a,b,c,d,e,f,g,h,i,j,k,l,m,n}
CONSTANTS nodes, ignore, nl, xc,yc, plx,ply,pl, cs, sol, connected
PROPERTIES
nodes = N \ ignore &
// target number of links per node:
nl : nodes --> LINKS & /* number of links */
// coordinates of nodes
xc: nodes --> COORD & yc: nodes --> COORD &
// possible links:
pl : nodes <-> nodes &
plx : nodes <-> nodes &
ply : nodes <-> nodes &
plx = {n1,n2 | xc(n1)=xc(n2) & n1 /= n2 & yc(n2)>yc(n1) &
!n3.(xc(n3)=xc(n1) => yc(n3) /: yc(n1)+1..yc(n2)-1) } &
ply = {n1,n2 | yc(n1)=yc(n2) & n1 /= n2 & xc(n2)>xc(n1) &
!n3.(yc(n3)=yc(n1) => xc(n3) /: xc(n1)+1..xc(n2)-1)} &
pl = plx \/ ply &
// compute conflict set (assumes xc,yc coordinates ordered in plx,ply)
cs = {pl1,pl2 | pl1:plx & pl2:ply &
xc(p1(pl1)): xc(p1(pl2))+1..xc(p2(pl2))-1 &
yc(p1(pl2)): yc(p1(pl1))+1..yc(p2(pl1))-1} &
sol : pl --> 0..MAXBRIDGES &
!nn.(nn:nodes => SIGMA(l).(l:pl &
(p1(l)=nn or p2(l)=nn)|sol(l))=nl(nn)) &
!(pl1,pl2).( (pl1,pl2):cs => sol(pl1)=0 or sol(pl2)=0) & // no conflicts
// check graph connected
connected = {pl|sol(pl)>0} &
closure1(connected \/ connected~)[{a}] = {nn|nn:nodes & nl(nn)>0} &
// encoding of puzzle
// A puzzle from bridges.png
xc(a)=1 & yc(a)=1 & nl(a)=4 &
xc(b)=1 & yc(b)=4 & nl(b)=6 &
xc(c)=1 & yc(c)=6 & nl(c)=3 &
xc(d)=2 & yc(d)=2 & nl(d)=1 &
xc(e)=2 & yc(e)=5 & nl(e)=2 &
xc(f)=3 & yc(f)=2 & nl(f)=4 &
xc(g)=3 & yc(g)=4 & nl(g)=6 &
xc(h)=3 & yc(h)=5 & nl(h)=4 &
xc(i)=4 & yc(i)=3 & nl(i)=3 &
xc(j)=4 & yc(j)=6 & nl(j)=3 &
xc(k)=5 & yc(k)=2 & nl(k)=1 &
xc(l)=6 & yc(l)=1 & nl(l)=4 &
xc(m)=6 & yc(m)=3 & nl(m)=5 &
xc(n)=6 & yc(n)=5 & nl(n)=2 &
ignore = {}
END
```
%% Output
Loaded machine: Bridges
%% 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:
One can then initialise the model, as above and the execute the command `:dot custom_graph`. This leads to the following picture:
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
Error from ProB: Prolog said no.
Error: Could not execute command "/usr/bin/dot" due to exception: 'Could not access file:'('/usr/bin/dot')
%% Cell type:code id: tags:
``` prob
:dot
```
%% Output
java.lang.IndexOutOfBoundsException: Index: 0, Size: 0
%% Cell type:code id: tags:
``` prob
:version
```
%% Output
ProB CLI: 1.9.1-nightly (e1c6b13036a30115e0fea4fc880887b737b82ce4)
ProB 2: 3.2.12-SNAPSHOT (e73f14155d2b248b99097801ddddfab206c4cf2b)
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
Error from ProB: Prolog said no.
Error: Could not execute command "/usr/bin/dot" due to exception: 'Could not access file:'('/usr/bin/dot')
%% Cell type:code id: tags:
``` prob
:pref DOT
```
%% Output
DOT = /usr/bin/dot
%% Cell type:code id: tags:
``` prob
```
.ipynb_checkpoints/Cheryls_Birthday-checkpoint.ipynb deleted 100644 → 0
+ 0
− 404
View file @ 1cbe29fb
%% Cell type:markdown id: tags:
# Cheryl's Birthday
This Puzzle is a variation of another Puzzle (Sum and Product) and has
been described
in a New York Times article(http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html).
Here is a first solution in B, where the text of the puzzle has been
integrated as comments. There are almost certainly more elegant
encodings of the problem in B.
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-of-b-syntax,summary page about the B syntax>>):
* `x : S` specifies that x is an element of S
* `dom(r)` is the domain of a function or relation r
* `r~` is the inverse of a function or relation r
* `r[S]` is the relational image of a relation r for a set of domain values S
* `card(S)` is the cardinality of a set S
* `a|->b` represents the pair (a,b); note that a relation and function in B is a set of pairs.
* `!x.(P => Q)` denotes universal quantification over variable x
In case you are new to using the jupyter notebook, simply type in `:help` to get an overview over the full range of options you have with the ProB core.
%% Cell type:code id: tags:
``` prob
::load
MACHINE CherylsBirthday
/* A simplified version of the SumProduct Puzzle taken from
http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html
*/
DEFINITIONS
DontKnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) > 1;
KnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) = 1
CONSTANTS Month, Day, PD, PD2
PROPERTIES
/* Albert and Bernard just met Cheryl. “When’s your birthday?” Albert asked Cheryl.*/
Month:STRING & Day:1..31 &
/* Cheryl thought a second and said, “I’m not going to tell you, but I’ll give you some clues.” She wrote down a list of 10 dates: */
PD = {("aug"|->14),("aug"|->15),("aug"|->17),
("july"|->14),("july"|->16),("june"|->17),("june"|->18),
("may"|->15),("may"|->16),("may"|->19)}
&
/*
Then Cheryl whispered in Albert’s ear the month — and only the month — of her birthday.
To Bernard, she whispered the day, and only the day.
*/
Month : dom(PD) &
Day : ran(PD) &
Month|->Day : PD &
/* Albert: I don’t know when your birthday is, */
card(PD[{Month}]) > 1 &
/* but I know Bernard doesn’t know, either. */
!x.(x:PD[{Month}] => DontKnowFromDay(PD,x) ) &
/* Bernard: I didn’t know originally, */
DontKnowFromDay(PD,Day) &
/* but now I do. */
PD2 = {m,d| (m|->d):PD & !x.(x:PD[{m}] => DontKnowFromDay(PD,x) ) } &
KnowFromDay(PD2,Day) &
/* Albert: Well, now I know, too! */
card({d|Month|->d : PD2 & KnowFromDay(PD2,d)})=1
ASSERTIONS /* single solution found by ProB */
Month = "july";
Day = 16
END
```
%% Output
Loaded machine: CherylsBirthday
%% Cell type:markdown id: tags:
After loading this B machine, you will see that there is only a single solution (solving time 20-30 ms) : `Month = "july"` and `Day = 16`.
With jupyter notebook, you have to type in `:constants` to set up the models constants.
After doing that, you can use `:init` to initialise your machine.
%% 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:
You can check for the solution simply by typing in `Month` and `Day`. You will see, there is only one solution for this problem.
%% Cell type:code id: tags:
``` prob
Month
```
%% Output
$\text{"july"}$
"july"
%% Cell type:code id: tags:
``` prob
Day
```
%% Output
$16$
16
%% Cell type:markdown id: tags:
## Using an enumerated set
It is possible to use an enumerated set for the Months. One simply has to add:
~~~~
SETS MONTHS = {may, june, july, aug, sep}
~~~~
change the definition of the possible dates:
~~~~
PD = {(aug|->14), (aug|->15), (aug|->17),
(july|->14),(july|->16),(june|->17),
(june|->18),
(may|->15),(may|->16),(may|->19)}
~~~~
and change the type of Month to `MONTHS`. This possible solution makes the constraint solving via ProB marginally faster.
%% Cell type:code id: tags:
``` prob
::load
MACHINE CherylsBirthday
/* A simplified version of the SumProduct Puzzle taken from
http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html
*/
DEFINITIONS
DontKnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) > 1;
KnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) = 1
SETS
MONTHS = {may, june, july, aug, sep}
CONSTANTS Month, Day, PD, PD2
PROPERTIES
/* Albert and Bernard just met Cheryl. “When’s your birthday?” Albert asked Cheryl.*/
Month:MONTHS & Day:1..31 &
/* Cheryl thought a second and said, “I’m not going to tell you, but I’ll give you some clues.” She wrote down a list of 10 dates: */
PD = {(aug|->14), (aug|->15), (aug|->17),
(july|->14),(july|->16),(june|->17),
(june|->18),
(may|->15),(may|->16),(may|->19)}
&
/*
Then Cheryl whispered in Albert’s ear the month — and only the month — of her birthday.
To Bernard, she whispered the day, and only the day.
*/
Month : dom(PD) &
Day : ran(PD) &
Month|->Day : PD &
/* Albert: I don’t know when your birthday is, */
card(PD[{Month}]) > 1 &
/* but I know Bernard doesn’t know, either. */
!x.(x:PD[{Month}] => DontKnowFromDay(PD,x) ) &
/* Bernard: I didn’t know originally, */
DontKnowFromDay(PD,Day) &
/* but now I do. */
PD2 = {m,d| (m|->d):PD & !x.(x:PD[{m}] => DontKnowFromDay(PD,x) ) } &
KnowFromDay(PD2,Day) &
/* Albert: Well, now I know, too! */
card({d|Month|->d : PD2 & KnowFromDay(PD2,d)})=1
ASSERTIONS /* single solution found by ProB */
Month = july;
Day = 16
END
```
%% Output
Loaded machine: CherylsBirthday
%% 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:
One will get one possible solution with this code as well. By typing in `Month` and `Day` again, it is possible to check this.
%% Cell type:code id: tags:
``` prob
Month
```
%% Output
$\mathit{july}$
july
%% Cell type:code id: tags:
``` prob
Day
```
%% Output
$16$
16
%% Cell type:code id: tags:
``` prob
```
.ipynb_checkpoints/N_Queens-checkpoint.ipynb deleted 100644 → 0
+ 0
− 1893
View file @ 1cbe29fb
This diff is collapsed.
.ipynb_checkpoints/ProB_Jupyter_Notebook_Overview-checkpoint.ipynb deleted 100644 → 0
+ 0
− 2475
View file @ 1cbe29fb
This diff is collapsed.
notebook.tex deleted 100644 → 0
+ 0
− 1604
View file @ 1cbe29fb
This diff is collapsed.
output_78_0.pdf deleted 100644 → 0
+ 0
− 0
View file @ 1cbe29fb
File deleted
output_78_0.svg deleted 100644 → 0
+ 0
− 98
View file @ 1cbe29fb
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<!-- Generated by graphviz version 2.40.1 (20161225.0304)
-->
<!-- Title: state Pages: 1 -->
<svg width="574pt" height="131pt"
viewBox="0.00 0.00 573.70 131.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 127)">
<title>state</title>
<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-127 569.6967,-127 569.6967,4 -4,4"/>
<!-- FALSE -->
<g id="node1" class="node">
<title>FALSE</title>
<ellipse fill="#a52a2a" stroke="#a52a2a" cx="37.6967" cy="-105" rx="37.8943" ry="18"/>
<text text-anchor="middle" x="37.6967" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">FALSE</text>
</g>
<!-- ROOT&#45;NODE -->
<g id="node2" class="node">
<title>ROOT&#45;NODE</title>
<polygon fill="#add8e6" stroke="#add8e6" points="292.6967,-36 205.5564,-18 292.6967,0 379.8369,-18 292.6967,-36"/>
<text text-anchor="middle" x="292.6967" y="-14.3" font-family="Times,serif" font-size="14.00" fill="#000000">ROOT&#45;NODE</text>
</g>
<!-- FALSE&#45;&gt;ROOT&#45;NODE -->
<g id="edge1" class="edge">
<title>FALSE&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#b22222" d="M45.4313,-87.0482C51.2604,-75.7333 60.3678,-61.829 72.6967,-54 96.4841,-38.8946 164.3902,-29.3258 218.5285,-23.8823"/>
<polygon fill="#b22222" stroke="#b22222" points="219.1954,-27.334 228.8089,-22.8808 218.5167,-20.367 219.1954,-27.334"/>
<text text-anchor="middle" x="101.6967" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">door_open</text>
</g>
<!-- TRUE -->
<g id="node3" class="node">
<title>TRUE</title>
<ellipse fill="#698b22" stroke="#698b22" cx="126.6967" cy="-105" rx="33.5952" ry="18"/>
<text text-anchor="middle" x="126.6967" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">TRUE</text>
</g>
<!-- TRUE&#45;&gt;ROOT&#45;NODE -->
<g id="edge2" class="edge">
<title>TRUE&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#a0522d" d="M128.4128,-86.5614C130.3881,-75.6337 134.6244,-62.3348 143.6967,-54 156.5391,-42.2015 195.2856,-33.048 230.0463,-26.9236"/>
<polygon fill="#a0522d" stroke="#a0522d" points="230.9228,-30.3249 240.195,-25.1989 229.7499,-23.4239 230.9228,-30.3249"/>
<text text-anchor="middle" x="178.1967" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">direction_up</text>
</g>
<!-- &#45;1 -->
<g id="node4" class="node">
<title>&#45;1</title>
<polygon fill="#cdba96" stroke="#cdba96" points="319.6967,-123 265.6967,-123 265.6967,-87 319.6967,-87 319.6967,-123"/>
<text text-anchor="middle" x="292.6967" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">&#45;1</text>
</g>
<!-- &#45;1&#45;&gt;ROOT&#45;NODE -->
<g id="edge3" class="edge">
<title>&#45;1&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#473c8b" d="M265.574,-99.2206C249.2281,-94.1898 229.6958,-85.08 219.6967,-69 209.7592,-53.0192 225.7758,-40.7054 245.3118,-32.1844"/>
<polygon fill="#473c8b" stroke="#473c8b" points="246.7714,-35.3705 254.7693,-28.4218 244.1838,-28.8664 246.7714,-35.3705"/>
<text text-anchor="middle" x="245.1967" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">cur_floor</text>
</g>
<!-- &#45;1&#45;&gt;ROOT&#45;NODE -->
<g id="edge5" class="edge">
<title>&#45;1&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#000000" d="M292.6967,-86.9735C292.6967,-75.1918 292.6967,-59.5607 292.6967,-46.1581"/>
<polygon fill="#000000" stroke="#000000" points="296.1968,-46.0033 292.6967,-36.0034 289.1968,-46.0034 296.1968,-46.0033"/>
<text text-anchor="middle" x="326.1967" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">call_buttons</text>
</g>
<!-- &#45;1&#45;&gt;ROOT&#45;NODE -->
<g id="edge7" class="edge">
<title>&#45;1&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#bdef6b" d="M319.7358,-98.1105C334.6112,-92.7883 351.8084,-83.7625 360.6967,-69 369.8361,-53.8203 355.4433,-41.6607 337.5823,-33.0275"/>
<polygon fill="#bdef6b" stroke="#bdef6b" points="338.5958,-29.6502 328.0322,-28.837 335.7831,-36.0602 338.5958,-29.6502"/>
<text text-anchor="middle" x="384.1967" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">groundf</text>
</g>
<!-- 1 -->
<g id="node5" class="node">
<title>1</title>
<polygon fill="#cdba96" stroke="#cdba96" points="475.6967,-123 421.6967,-123 421.6967,-87 475.6967,-87 475.6967,-123"/>
<text text-anchor="middle" x="448.6967" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">1</text>
</g>
<!-- 1&#45;&gt;ROOT&#45;NODE -->
<g id="edge4" class="edge">
<title>1&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#000000" d="M438.6092,-86.6124C431.7628,-75.7039 421.7712,-62.4073 409.6967,-54 392.4638,-42.0011 371.1042,-33.9017 351.3706,-28.479"/>
<polygon fill="#000000" stroke="#000000" points="352.0918,-25.0507 341.5356,-25.9538 350.351,-31.8308 352.0918,-25.0507"/>
<text text-anchor="middle" x="458.1967" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">call_buttons</text>
</g>
<!-- 2 -->
<g id="node6" class="node">
<title>2</title>
<polygon fill="#cdba96" stroke="#cdba96" points="565.6967,-123 511.6967,-123 511.6967,-87 565.6967,-87 565.6967,-123"/>
<text text-anchor="middle" x="538.6967" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">2</text>
</g>
<!-- 2&#45;&gt;ROOT&#45;NODE -->
<g id="edge6" class="edge">
<title>2&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#efdf84" d="M528.0369,-86.8227C520.4593,-75.5637 509.2422,-61.808 495.6967,-54 473.2129,-41.0397 411.0663,-31.2111 361.4046,-25.1247"/>
<polygon fill="#efdf84" stroke="#efdf84" points="361.6802,-21.6328 351.3353,-23.9202 360.8488,-28.5832 361.6802,-21.6328"/>
<text text-anchor="middle" x="524.6967" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">topf</text>
</g>
</g>
</svg>
\ No newline at end of file
output_79_0.pdf deleted 100644 → 0
+ 0
− 0
View file @ 1cbe29fb
File deleted
output_79_0.svg deleted 100644 → 0
+ 0
− 99
View file @ 1cbe29fb
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<!-- Generated by graphviz version 2.40.1 (20161225.0304)
-->
<!-- Title: state Pages: 1 -->
<svg width="536pt" height="131pt"
viewBox="0.00 0.00 536.49 131.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 127)">
<title>state</title>
<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-127 532.4937,-127 532.4937,4 -4,4"/>
<!-- TRUE -->
<g id="node1" class="node">
<title>TRUE</title>
<ellipse fill="#698b22" stroke="#698b22" cx="33.797" cy="-105" rx="33.5952" ry="18"/>
<text text-anchor="middle" x="33.797" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">TRUE</text>
</g>
<!-- ROOT&#45;NODE -->
<g id="node2" class="node">
<title>ROOT&#45;NODE</title>
<polygon fill="#add8e6" stroke="#add8e6" points="260.797,-36 173.6568,-18 260.797,0 347.9373,-18 260.797,-36"/>
<text text-anchor="middle" x="260.797" y="-14.3" font-family="Times,serif" font-size="14.00" fill="#000000">ROOT&#45;NODE</text>
</g>
<!-- TRUE&#45;&gt;ROOT&#45;NODE -->
<g id="edge1" class="edge">
<title>TRUE&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#b22222" d="M35.2345,-86.8422C37.0949,-75.738 41.3079,-62.1465 50.797,-54 70.531,-37.0582 131.9518,-27.8663 183.3061,-23.0221"/>
<polygon fill="#b22222" stroke="#b22222" points="183.7819,-26.4935 193.4275,-22.1103 183.1537,-19.5218 183.7819,-26.4935"/>
<text text-anchor="middle" x="85.297" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">direction_up</text>
</g>
<!-- ROOT&#45;NODE&#45;&gt;ROOT&#45;NODE -->
<g id="edge5" class="edge">
<title>ROOT&#45;NODE&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#000000" d="M311.7306,-25.4982C340.0441,-26.8978 366.1169,-24.3984 366.1169,-18 366.1169,-12.3764 345.9763,-9.7647 321.8755,-10.1649"/>
<polygon fill="#000000" stroke="#000000" points="321.6089,-6.6717 311.7306,-10.5018 321.8413,-13.6679 321.6089,-6.6717"/>
<text text-anchor="middle" x="405.6169" y="-14.3" font-family="Times,serif" font-size="14.00" fill="#000000">inside_buttons</text>
</g>
<!-- 1 -->
<g id="node3" class="node">
<title>1</title>
<polygon fill="#cdba96" stroke="#cdba96" points="197.797,-123 143.797,-123 143.797,-87 197.797,-87 197.797,-123"/>
<text text-anchor="middle" x="170.797" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">1</text>
</g>
<!-- 1&#45;&gt;ROOT&#45;NODE -->
<g id="edge2" class="edge">
<title>1&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#a0522d" d="M143.5311,-89.5409C129.5789,-79.6256 117.333,-66.3421 126.797,-54 135.9895,-42.0119 168.3405,-33.1292 198.9506,-27.1866"/>
<polygon fill="#a0522d" stroke="#a0522d" points="199.6023,-30.6255 208.7962,-25.3603 198.3255,-23.7429 199.6023,-30.6255"/>
<text text-anchor="middle" x="160.297" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">call_buttons</text>
</g>
<!-- 1&#45;&gt;ROOT&#45;NODE -->
<g id="edge7" class="edge">
<title>1&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#bdef6b" d="M189.4451,-86.9735C203.4754,-73.4109 222.7826,-54.7473 237.7754,-40.2542"/>
<polygon fill="#bdef6b" stroke="#bdef6b" points="240.4143,-42.5713 245.1716,-33.1046 235.5491,-37.5383 240.4143,-42.5713"/>
<text text-anchor="middle" x="232.797" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">topf</text>
</g>
<!-- &#45;1 -->
<g id="node4" class="node">
<title>&#45;1</title>
<polygon fill="#cdba96" stroke="#cdba96" points="377.797,-123 323.797,-123 323.797,-87 377.797,-87 377.797,-123"/>
<text text-anchor="middle" x="350.797" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">&#45;1</text>
</g>
<!-- &#45;1&#45;&gt;ROOT&#45;NODE -->
<g id="edge3" class="edge">
<title>&#45;1&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#a0522d" d="M323.6897,-101.9537C302.9755,-98.0547 275.6924,-89.18 261.797,-69 257.1356,-62.2303 255.7227,-53.6658 255.8156,-45.4976"/>
<polygon fill="#a0522d" stroke="#a0522d" points="259.3045,-45.774 256.6073,-35.5283 252.3265,-45.2198 259.3045,-45.774"/>
<text text-anchor="middle" x="295.297" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">call_buttons</text>
</g>
<!-- &#45;1&#45;&gt;ROOT&#45;NODE -->
<g id="edge6" class="edge">
<title>&#45;1&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#efdf84" d="M346.2352,-86.7909C342.8415,-76.2176 337.3012,-63.2099 328.797,-54 321.3804,-45.9678 311.7557,-39.3919 302.0929,-34.1621"/>
<polygon fill="#efdf84" stroke="#efdf84" points="303.397,-30.901 292.8877,-29.5568 300.2649,-37.1612 303.397,-30.901"/>
<text text-anchor="middle" x="364.297" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">cur_floor</text>
</g>
<!-- &#45;1&#45;&gt;ROOT&#45;NODE -->
<g id="edge8" class="edge">
<title>&#45;1&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#5863ee" d="M377.829,-89.2398C391.3652,-79.32 403.0879,-66.1401 393.797,-54 384.7192,-42.1383 352.8479,-33.2825 322.5817,-27.3226"/>
<polygon fill="#5863ee" stroke="#5863ee" points="322.8887,-23.8191 312.4143,-25.4123 321.596,-30.6987 322.8887,-23.8191"/>
<text text-anchor="middle" x="418.297" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">groundf</text>
</g>
<!-- FALSE -->
<g id="node5" class="node">
<title>FALSE</title>
<ellipse fill="#a52a2a" stroke="#a52a2a" cx="490.797" cy="-105" rx="37.8943" ry="18"/>
<text text-anchor="middle" x="490.797" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">FALSE</text>
</g>
<!-- FALSE&#45;&gt;ROOT&#45;NODE -->
<g id="edge4" class="edge">
<title>FALSE&#45;&gt;ROOT&#45;NODE</title>
<path fill="none" stroke="#473c8b" d="M479.2874,-87.6545C470.8217,-76.3008 458.2969,-62.1147 443.797,-54 423.6778,-42.7404 369.3139,-32.8677 325.0301,-26.3232"/>
<polygon fill="#473c8b" stroke="#473c8b" points="325.2844,-22.8236 314.8862,-24.8553 324.2818,-29.7514 325.2844,-22.8236"/>
<text text-anchor="middle" x="491.797" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">door_open</text>
</g>
</g>
</svg>
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment