Wrote nice comments in the code to explain the pirates demo

Author: maxvonhippel

Makefile

@@ -211,8 +211,8 @@ pirates:
 		--model=demo/pirates/alice.pml  \
 		--phi=demo/pirates/phi.pml 		\
 		--Q=demo/pirates/bob.pml        \
-		--IO=demo/pirates/IO.txt            \
-		--max_attacks=10                \
+		--IO=demo/pirates/IO.txt        \
+		--max_attacks=1                 \
 		--with_recovery=True            \
 		--name=pirates                	\
 		--characterize=True

demo/pirates/alice.pml

@@ -8,12 +8,29 @@ bool aliceRetired = false
 active proctype alice() {
 SCOPING:
     if
+    /* When Alice is scoping for Bob, as soon as she
+     * notices him, she immediately attacks, _regardless_
+     * of what flags he waves.
+     */
     :: bob2alice ? _ -> goto PIRATESTUFF;
     fi
 PIRATESTUFF:
+    /* When Alice attacks, she first hoists the pirate 
+     * flag, to make it clear that she is, in fact, a big
+     * scary pirate.
+     */
     alice2bob ! pirate;
     if
+    /* If Bob shows the white flag of surrender then Alice
+     * takes his loot and then returns to the high sea to 
+     * scope for another ship to plunder.
+     */
     :: bob2alice ? white -> goto SCOPING;
+    /* On the other hand, if Bob hoists the official colors of
+     * Her Majesty's Royal Navy, then Alice will surrender,
+     * because she knows that she is no match for the Royal
+     * Navy in battle!
+     */
     :: bob2alice ? royal -> goto end;
     fi
 end:

demo/pirates/bob.pml

@@ -1,7 +1,11 @@
 active proctype bob() {
 FISHING:
     do
+    /* When Bob sees Alice, he offers to trade. */
     :: bob2alice ! trading;
+    /* If Alice says she is a pirate then Bob 
+     * surrenders immediately.  He has a peaceful soul.
+     */
     :: alice2bob ? pirate -> bob2alice ! white; 
     od
 end: