Skip to content
Snippets Groups Projects
Commit 40aa6024 authored by penguinn's avatar penguinn
Browse files

Add Gilbreath Card Trick

parent c06ddbb3
No related branches found
No related tags found
No related merge requests found
%% Cell type:markdown id: tags:
# Gilbreath Card Trick
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
```
images/French_suits_Club.gif

194 B

images/French_suits_Diamond.gif

160 B

images/French_suits_Heart.gif

203 B

images/French_suits_Spade.gif

238 B

0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment