// contract signing protocol [BGMR90]
// dxp/gxn 11/07/02

mdp

// constants
// v=0.100000
// alpha=1.100000
// beta=1.010000

// discretize the coin (uniform choice over [0,1])
// suppose choices are 1/100,2/100,...

// number of messages each party sends
const N=24;

module contract

	pA : [1..N]; // probabilities A sends to B
	pB : [1..N]; // probabilities B sends to A
	turn : [0..1]; // whos turn it is
	c : [0..1]; // status of the coin 0 not flipped 1 flipped
	rho : [0..100]; // value of the coin=x means value is 1/100
	
	// parties continue after the coin has been flipped
	[] turn=0 -> pA'=min(N,pA+1) & turn'=1;
	[] turn=1 -> pB'=min(N,pB+1) & turn'=0;
	
	// flip coin (at any time)
	[] c=0 & (pA>1 | pB>1) ->   1/100 : (c'=1) & (rho'=1) 
	          + 1/100 : (c'=1) & (rho'=2) 
	          + 1/100 : (c'=1) & (rho'=3) 
	          + 1/100 : (c'=1) & (rho'=4) 
	          + 1/100 : (c'=1) & (rho'=5) 
	          + 1/100 : (c'=1) & (rho'=6) 
	          + 1/100 : (c'=1) & (rho'=7) 
	          + 1/100 : (c'=1) & (rho'=8)
	          + 1/100 : (c'=1) & (rho'=9) 
	          + 1/100 : (c'=1) & (rho'=10)
	          + 1/100 : (c'=1) & (rho'=11)
	          + 1/100 : (c'=1) & (rho'=12)
	          + 1/100 : (c'=1) & (rho'=13)
	          + 1/100 : (c'=1) & (rho'=14)
	          + 1/100 : (c'=1) & (rho'=15)
	          + 1/100 : (c'=1) & (rho'=16)
	          + 1/100 : (c'=1) & (rho'=17)
	          + 1/100 : (c'=1) & (rho'=18)
	          + 1/100 : (c'=1) & (rho'=19)
	          + 1/100 : (c'=1) & (rho'=20)
	          + 1/100 : (c'=1) & (rho'=21)
	          + 1/100 : (c'=1) & (rho'=22)
	          + 1/100 : (c'=1) & (rho'=23)
	          + 1/100 : (c'=1) & (rho'=24)
	          + 1/100 : (c'=1) & (rho'=25)
	          + 1/100 : (c'=1) & (rho'=26)
	          + 1/100 : (c'=1) & (rho'=27)
	          + 1/100 : (c'=1) & (rho'=28)
	          + 1/100 : (c'=1) & (rho'=29)
	          + 1/100 : (c'=1) & (rho'=30)
	          + 1/100 : (c'=1) & (rho'=31)
	          + 1/100 : (c'=1) & (rho'=32)
	          + 1/100 : (c'=1) & (rho'=33)
	          + 1/100 : (c'=1) & (rho'=34)
	          + 1/100 : (c'=1) & (rho'=35)
	          + 1/100 : (c'=1) & (rho'=36)
	          + 1/100 : (c'=1) & (rho'=37)
	          + 1/100 : (c'=1) & (rho'=38)
	          + 1/100 : (c'=1) & (rho'=39)
	          + 1/100 : (c'=1) & (rho'=40)
	          + 1/100 : (c'=1) & (rho'=41)
	          + 1/100 : (c'=1) & (rho'=42)
	          + 1/100 : (c'=1) & (rho'=43)
	          + 1/100 : (c'=1) & (rho'=44)
	          + 1/100 : (c'=1) & (rho'=45)
	          + 1/100 : (c'=1) & (rho'=46)
	          + 1/100 : (c'=1) & (rho'=47)
	          + 1/100 : (c'=1) & (rho'=48)
	          + 1/100 : (c'=1) & (rho'=49)
	          + 1/100 : (c'=1) & (rho'=50)
	          + 1/100 : (c'=1) & (rho'=51)
	          + 1/100 : (c'=1) & (rho'=52)
	          + 1/100 : (c'=1) & (rho'=53)
	          + 1/100 : (c'=1) & (rho'=54)
	          + 1/100 : (c'=1) & (rho'=55)
	          + 1/100 : (c'=1) & (rho'=56)
	          + 1/100 : (c'=1) & (rho'=57)
	          + 1/100 : (c'=1) & (rho'=58)
	          + 1/100 : (c'=1) & (rho'=59)
	          + 1/100 : (c'=1) & (rho'=60)
	          + 1/100 : (c'=1) & (rho'=61)
	          + 1/100 : (c'=1) & (rho'=62)
	          + 1/100 : (c'=1) & (rho'=63)
	          + 1/100 : (c'=1) & (rho'=64)
	          + 1/100 : (c'=1) & (rho'=65)
	          + 1/100 : (c'=1) & (rho'=66)
	          + 1/100 : (c'=1) & (rho'=67)
	          + 1/100 : (c'=1) & (rho'=68)
	          + 1/100 : (c'=1) & (rho'=69)
	          + 1/100 : (c'=1) & (rho'=70)
	          + 1/100 : (c'=1) & (rho'=71)
	          + 1/100 : (c'=1) & (rho'=72)
	          + 1/100 : (c'=1) & (rho'=73)
	          + 1/100 : (c'=1) & (rho'=74)
	          + 1/100 : (c'=1) & (rho'=75)
	          + 1/100 : (c'=1) & (rho'=76)
	          + 1/100 : (c'=1) & (rho'=77)
	          + 1/100 : (c'=1) & (rho'=78)
	          + 1/100 : (c'=1) & (rho'=79)
	          + 1/100 : (c'=1) & (rho'=80)
	          + 1/100 : (c'=1) & (rho'=81)
	          + 1/100 : (c'=1) & (rho'=82)
	          + 1/100 : (c'=1) & (rho'=83)
	          + 1/100 : (c'=1) & (rho'=84)
	          + 1/100 : (c'=1) & (rho'=85)
	          + 1/100 : (c'=1) & (rho'=86)
	          + 1/100 : (c'=1) & (rho'=87)
	          + 1/100 : (c'=1) & (rho'=88)
	          + 1/100 : (c'=1) & (rho'=89)
	          + 1/100 : (c'=1) & (rho'=90)
	          + 1/100 : (c'=1) & (rho'=91)
	          + 1/100 : (c'=1) & (rho'=92)
	          + 1/100 : (c'=1) & (rho'=93)
	          + 1/100 : (c'=1) & (rho'=94)
	          + 1/100 : (c'=1) & (rho'=95)
	          + 1/100 : (c'=1) & (rho'=96)
	          + 1/100 : (c'=1) & (rho'=97)
	          + 1/100 : (c'=1) & (rho'=98)
	          + 1/100 : (c'=1) & (rho'=99)
	          + 1/100 : (c'=1) & (rho'=100);

endmodule