added coin flipping game example

recursion/bitml.maude

@@ -39,9 +39,6 @@ op 0 : -> Configuration [ctor] .
 op lock : -> Configuration [ctor] .  
 op unlock : -> Configuration [ctor] .                                                                                                                     
 op _|_ : Configuration Configuration -> Configuration [comm assoc ctor id: 0 frozen] .    
-op coso : -> Configuration [ctor] .  
-op coso2 : -> Configuration [ctor] .  
-
 
 op 0 : -> Declarations [ctor] .
 op _:=_ : ContractName Contract -> Declaration [ctor] .

recursion/coin-flipping-game.maude

@@ -0,0 +1,32 @@
+mod TEST is
+	protecting BITML .
+
+ops A B : -> Participant .
+ops Xa Xb : -> ContractName .
+ops CFG SplitA SplitB : -> Contract .
+ops Cconf : -> Configuration .
+
+
+eq dec = (Xa := *: (*: (wd A) + *: (rngt Xb + SplitB) + (wd B)) + (wd A)), 
+		 (Xb := *: (*: (rngt Xa + SplitA) + *: (wd B) + (wd B)) + (wd A)) .   
+
+eq SplitA = split((wd A) (wd B)) .
+eq SplitB = split((wd A) (wd B)) .
+
+eq CFG = *: (*: (rngt Xa + SplitA) + *: (rngt Xb + SplitB) + (wd B)) + (wd A) .
+
+eq Cconf = < CFG > | unlock | Xa | Xb .
+
+
+endm
+
+
+***search Contr3  =>* G:Configuration .
+
+
+smod LIQUIDITY-CHECK is
+    protecting BITML_CHECK .
+    including TEST .
+endsm
+
+reduce in LIQUIDITY-CHECK : modelCheck(Cconf , <> contract-free) .           *** true