% prob_card.pi (in Picat, by Neng-Fa Zhou, June 2014)
% A sample ProB model is available at http://www.stups.uni-duesseldorf.de/ProB/index.php5/User_Manual
% The following comment is from the original ProB model.
/*
My belief is that B is a very expressive language, which can be very
convenient for modelling many problems. Hence, when in the Dagstuhl
library I stumbled upon a nice short article by Tony Hoare and
Natarajan Shankar in memory of Amir Pnueli, I decided to model the
problem and time how long it would take me to solve the problem using
ProB. The article 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. 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.
I attempted to model this problem in B and wanted to use model
checking to validate the property on the final sequence. 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). (Further below on this
page I also describe ways to reduce the model checking time.) I am
very interested in seeing how much combined modelling and verification
time is required to solve this task in other formalisms and with other
model checking tools (e.g., Promela with Spin, CSP with FDR, TLA+ with
TLC).
*/
import planner.
main =>
go(16).
go(N) ?=>
initialize_table,
initialize_cards(Cards,N),
plan_unbounded($init(Cards),Plan),
writeln(Plan).
go(_N) =>
writeln(verified).
initialize_cards(Cards,N),N<4 => Cards=[].
initialize_cards(Cards,N) =>
Cards = [1,2,3,4|CardsR], % 1 for spade, 2 for heart, 3 for club, and 4 for diamond
initialize_cards(CardsR,N-4).
final(shuffled(Cards)) =>
test_quartet(Cards,[1,2,3,4]).
test_quartet([C1,C2,C3,C4|_Cards],Suits),
sort([C1,C2,C3,C4]) !== Suits
=>
true.
test_quartet([_,_,_,_|Cards],Suits) =>
test_quartet(Cards,Suits).
action(init(Cards),NewS,Action,ActionCost) =>
NewS = $splitted(Deck1,RDeck2),
Action = split,
ActionCost = 1,
append(Deck1,Deck2,Cards),
Deck1 !== [],
Deck2 !== [],
RDeck2 = Deck2.reverse().
action(splitted(Deck1,Deck2),NewS,Action,ActionCost) =>
NewS = $shuffled(Cards),
Action = shuffle,
ActionCost = 1,
shuffle(Deck1,Deck2,Cards).
shuffle([],Deck2,Cards) => Cards = Deck2.
shuffle(Deck1,[],Cards) => Cards = Deck1.
shuffle([C|Deck1],Deck2,Cards) ?=>
Cards = [C|CardsR],
shuffle(Deck1,Deck2,CardsR).
shuffle(Deck1,[C|Deck2],Cards) =>
Cards = [C|CardsR],
shuffle(Deck1,Deck2,CardsR).