% 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).