Gilbreath Card Trick

In the Dagstuhl library I stumbled upon a nice short article by Tony Hoare and Natarajan Shankar in memory of Amir Pnueli. It unravels a card trick by Gilbreath. The card trick 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
• you split the cards into two sequences
• you reverse one of the sequences
• you perform a (not necessarily perfect) riffle shuffle of the two sequences
• the resulting sequence will itself consist of a sequence of four quartets with one card from each suite.

I attempted to model this problem in B and wanted to use model checking to validate the property. As I wanted to measure the time spent modeling I used a stopwatch. It took 13 minutes (starting from an empty B specification) to produce a first model that could be model checked by ProB. Full validation was finished after 19 minutes from the start. The model checking itself generated 150,183 states and 179,158 transitions and took 2 minutes and 17 seconds on a Mac Book Air (1.8 GHz i7).

Here is the specification

MACHINE CardTrick
/* Translation 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
  http://www.springerlink.com/content/gn18673357154448/
  */
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))
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

A (longer) Why3 encoding can be found here

  http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html.