```// model of aloha protocol with backoff scheme (three players)
// each player tries to send a single message

csg

player usr1 user1 endplayer
player usr2 user2 endplayer
player usr3 user3 endplayer

const int bcmax; // backoff limit
const int M=pow(2,bcmax)-1; // backoff counter (slots to wait)

// time can pass
formula tick = (s1=0 | s1=2 | s1=3) & (s2=0 | s2=2 | s2=3) & (s3=0 | s3=2 | s3=3) & (tr1=0 & tr2=0 & tr3=0);

// probability of successful transmission
const double beta=1;
const double q;
formula n = tr1+tr2+tr3;
formula rn = (n=3)? q/(pow(beta,2)*3) : (n=2)? q/(pow(beta,2)*2) : (n=1)? q : 0;

module user1

s1 : [0..3] init 0; // local state
tr1 : [0..1]; // try to transmit
bc1 : [0..M]; // backoff counter
cd1 : [0..bcmax]; // collision counter
t1 : [0..2]; // can only wait for two time units before trying

// wait or decide to try and transmit
[wait1] tick & (s1=0 | s1=3) & t1<2 -> (t1'=t1+1);
[trans1] tick & s1=0 -> (tr1'=1) & (t1'=0);
// transmit
[try1] tr1=1 -> (rn/n) : (s1'=3) & (tr1'=0)
+ (1-rn/n) : (s1'=1) & (tr1'=0) & (cd1'=min(bcmax,cd1+1));
// set backoff counter
[sbc1] s1=1 & cd1=1 -> 1/2 : (s1'=2) & (bc1'=0)
+ 1/2 : (s1'=2) & (bc1'=1);
[sbc1] s1=1 & cd1=2 -> 1/4 : (s1'=2) & (bc1'=0)
+ 1/4 : (s1'=2) & (bc1'=1)
+ 1/4 : (s1'=2) & (bc1'=2)
+ 1/4 : (s1'=2) & (bc1'=3);
[sbc1] s1=1 & cd1=3 -> 1/8 : (s1'=2) & (bc1'=0)
+ 1/8 : (s1'=2) & (bc1'=1)
+ 1/8 : (s1'=2) & (bc1'=2)
+ 1/8 : (s1'=2) & (bc1'=3)
+ 1/8 : (s1'=2) & (bc1'=4)
+ 1/8 : (s1'=2) & (bc1'=5)
+ 1/8 : (s1'=2) & (bc1'=6)
+ 1/8 : (s1'=2) & (bc1'=7);
[sbc1] s1=1 & cd1=4 -> 1/16 : (s1'=2) & (bc1'=0)
+ 1/16 : (s1'=2) & (bc1'=1)
+ 1/16 : (s1'=2) & (bc1'=2)
+ 1/16 : (s1'=2) & (bc1'=3)
+ 1/16 : (s1'=2) & (bc1'=4)
+ 1/16 : (s1'=2) & (bc1'=5)
+ 1/16 : (s1'=2) & (bc1'=6)
+ 1/16 : (s1'=2) & (bc1'=7)
+ 1/16 : (s1'=2) & (bc1'=8)
+ 1/16 : (s1'=2) & (bc1'=9)
+ 1/16 : (s1'=2) & (bc1'=10)
+ 1/16 : (s1'=2) & (bc1'=11)
+ 1/16 : (s1'=2) & (bc1'=12)
+ 1/16 : (s1'=2) & (bc1'=13)
+ 1/16 : (s1'=2) & (bc1'=14)
+ 1/16 : (s1'=2) & (bc1'=15);
[sbc1] s1=1 & cd1=5 -> 1/32 : (s1'=2) & (bc1'=0)
+ 1/32 : (s1'=2) & (bc1'=1)
+ 1/32 : (s1'=2) & (bc1'=2)
+ 1/32 : (s1'=2) & (bc1'=3)
+ 1/32 : (s1'=2) & (bc1'=4)
+ 1/32 : (s1'=2) & (bc1'=5)
+ 1/32 : (s1'=2) & (bc1'=6)
+ 1/32 : (s1'=2) & (bc1'=7)
+ 1/32 : (s1'=2) & (bc1'=8)
+ 1/32 : (s1'=2) & (bc1'=9)
+ 1/32 : (s1'=2) & (bc1'=10)
+ 1/32 : (s1'=2) & (bc1'=11)
+ 1/32 : (s1'=2) & (bc1'=12)
+ 1/32 : (s1'=2) & (bc1'=13)
+ 1/32 : (s1'=2) & (bc1'=14)
+ 1/32 : (s1'=2) & (bc1'=15)
+ 1/32 : (s1'=2) & (bc1'=16)
+ 1/32 : (s1'=2) & (bc1'=17)
+ 1/32 : (s1'=2) & (bc1'=18)
+ 1/32 : (s1'=2) & (bc1'=19)
+ 1/32 : (s1'=2) & (bc1'=20)
+ 1/32 : (s1'=2) & (bc1'=21)
+ 1/32 : (s1'=2) & (bc1'=22)
+ 1/32 : (s1'=2) & (bc1'=23)
+ 1/32 : (s1'=2) & (bc1'=24)
+ 1/32 : (s1'=2) & (bc1'=25)
+ 1/32 : (s1'=2) & (bc1'=26)
+ 1/32 : (s1'=2) & (bc1'=27)
+ 1/32 : (s1'=2) & (bc1'=28)
+ 1/32 : (s1'=2) & (bc1'=29)
+ 1/32 : (s1'=2) & (bc1'=30)
+ 1/32 : (s1'=2) & (bc1'=31);
[sbc1] s1=1 & cd1=6 -> 1/64 : (s1'=2) & (bc1'=0)
+ 1/64 : (s1'=2) & (bc1'=1)
+ 1/64 : (s1'=2) & (bc1'=2)
+ 1/64 : (s1'=2) & (bc1'=3)
+ 1/64 : (s1'=2) & (bc1'=4)
+ 1/64 : (s1'=2) & (bc1'=5)
+ 1/64 : (s1'=2) & (bc1'=6)
+ 1/64 : (s1'=2) & (bc1'=7)
+ 1/64 : (s1'=2) & (bc1'=8)
+ 1/64 : (s1'=2) & (bc1'=9)
+ 1/64 : (s1'=2) & (bc1'=10)
+ 1/64 : (s1'=2) & (bc1'=11)
+ 1/64 : (s1'=2) & (bc1'=12)
+ 1/64 : (s1'=2) & (bc1'=13)
+ 1/64 : (s1'=2) & (bc1'=14)
+ 1/64 : (s1'=2) & (bc1'=15)
+ 1/64 : (s1'=2) & (bc1'=16)
+ 1/64 : (s1'=2) & (bc1'=17)
+ 1/64 : (s1'=2) & (bc1'=18)
+ 1/64 : (s1'=2) & (bc1'=19)
+ 1/64 : (s1'=2) & (bc1'=20)
+ 1/64 : (s1'=2) & (bc1'=21)
+ 1/64 : (s1'=2) & (bc1'=22)
+ 1/64 : (s1'=2) & (bc1'=23)
+ 1/64 : (s1'=2) & (bc1'=24)
+ 1/64 : (s1'=2) & (bc1'=25)
+ 1/64 : (s1'=2) & (bc1'=26)
+ 1/64 : (s1'=2) & (bc1'=27)
+ 1/64 : (s1'=2) & (bc1'=28)
+ 1/64 : (s1'=2) & (bc1'=29)
+ 1/64 : (s1'=2) & (bc1'=30)
+ 1/64 : (s1'=2) & (bc1'=31)
+ 1/64 : (s1'=2) & (bc1'=32)
+ 1/64 : (s1'=2) & (bc1'=33)
+ 1/64 : (s1'=2) & (bc1'=34)
+ 1/64 : (s1'=2) & (bc1'=35)
+ 1/64 : (s1'=2) & (bc1'=36)
+ 1/64 : (s1'=2) & (bc1'=37)
+ 1/64 : (s1'=2) & (bc1'=38)
+ 1/64 : (s1'=2) & (bc1'=39)
+ 1/64 : (s1'=2) & (bc1'=40)
+ 1/64 : (s1'=2) & (bc1'=41)
+ 1/64 : (s1'=2) & (bc1'=42)
+ 1/64 : (s1'=2) & (bc1'=43)
+ 1/64 : (s1'=2) & (bc1'=44)
+ 1/64 : (s1'=2) & (bc1'=45)
+ 1/64 : (s1'=2) & (bc1'=46)
+ 1/64 : (s1'=2) & (bc1'=47)
+ 1/64 : (s1'=2) & (bc1'=48)
+ 1/64 : (s1'=2) & (bc1'=49)
+ 1/64 : (s1'=2) & (bc1'=50)
+ 1/64 : (s1'=2) & (bc1'=51)
+ 1/64 : (s1'=2) & (bc1'=52)
+ 1/64 : (s1'=2) & (bc1'=53)
+ 1/64 : (s1'=2) & (bc1'=54)
+ 1/64 : (s1'=2) & (bc1'=55)
+ 1/64 : (s1'=2) & (bc1'=56)
+ 1/64 : (s1'=2) & (bc1'=57)
+ 1/64 : (s1'=2) & (bc1'=58)
+ 1/64 : (s1'=2) & (bc1'=59)
+ 1/64 : (s1'=2) & (bc1'=60)
+ 1/64 : (s1'=2) & (bc1'=61)
+ 1/64 : (s1'=2) & (bc1'=62)
+ 1/64 : (s1'=2) & (bc1'=63);
[sbc1] s1=1 & cd1=7 -> 1/128 : (s1'=2) & (bc1'=0)
+ 1/128 : (s1'=2) & (bc1'=1)
+ 1/128 : (s1'=2) & (bc1'=2)
+ 1/128 : (s1'=2) & (bc1'=3)
+ 1/128 : (s1'=2) & (bc1'=4)
+ 1/128 : (s1'=2) & (bc1'=5)
+ 1/128 : (s1'=2) & (bc1'=6)
+ 1/128 : (s1'=2) & (bc1'=7)
+ 1/128 : (s1'=2) & (bc1'=8)
+ 1/128 : (s1'=2) & (bc1'=9)
+ 1/128 : (s1'=2) & (bc1'=10)
+ 1/128 : (s1'=2) & (bc1'=11)
+ 1/128 : (s1'=2) & (bc1'=12)
+ 1/128 : (s1'=2) & (bc1'=13)
+ 1/128 : (s1'=2) & (bc1'=14)
+ 1/128 : (s1'=2) & (bc1'=15)
+ 1/128 : (s1'=2) & (bc1'=16)
+ 1/128 : (s1'=2) & (bc1'=17)
+ 1/128 : (s1'=2) & (bc1'=18)
+ 1/128 : (s1'=2) & (bc1'=19)
+ 1/128 : (s1'=2) & (bc1'=20)
+ 1/128 : (s1'=2) & (bc1'=21)
+ 1/128 : (s1'=2) & (bc1'=22)
+ 1/128 : (s1'=2) & (bc1'=23)
+ 1/128 : (s1'=2) & (bc1'=24)
+ 1/128 : (s1'=2) & (bc1'=25)
+ 1/128 : (s1'=2) & (bc1'=26)
+ 1/128 : (s1'=2) & (bc1'=27)
+ 1/128 : (s1'=2) & (bc1'=28)
+ 1/128 : (s1'=2) & (bc1'=29)
+ 1/128 : (s1'=2) & (bc1'=30)
+ 1/128 : (s1'=2) & (bc1'=31)
+ 1/128 : (s1'=2) & (bc1'=32)
+ 1/128 : (s1'=2) & (bc1'=33)
+ 1/128 : (s1'=2) & (bc1'=34)
+ 1/128 : (s1'=2) & (bc1'=35)
+ 1/128 : (s1'=2) & (bc1'=36)
+ 1/128 : (s1'=2) & (bc1'=37)
+ 1/128 : (s1'=2) & (bc1'=38)
+ 1/128 : (s1'=2) & (bc1'=39)
+ 1/128 : (s1'=2) & (bc1'=40)
+ 1/128 : (s1'=2) & (bc1'=41)
+ 1/128 : (s1'=2) & (bc1'=42)
+ 1/128 : (s1'=2) & (bc1'=43)
+ 1/128 : (s1'=2) & (bc1'=44)
+ 1/128 : (s1'=2) & (bc1'=45)
+ 1/128 : (s1'=2) & (bc1'=46)
+ 1/128 : (s1'=2) & (bc1'=47)
+ 1/128 : (s1'=2) & (bc1'=48)
+ 1/128 : (s1'=2) & (bc1'=49)
+ 1/128 : (s1'=2) & (bc1'=50)
+ 1/128 : (s1'=2) & (bc1'=51)
+ 1/128 : (s1'=2) & (bc1'=52)
+ 1/128 : (s1'=2) & (bc1'=53)
+ 1/128 : (s1'=2) & (bc1'=54)
+ 1/128 : (s1'=2) & (bc1'=55)
+ 1/128 : (s1'=2) & (bc1'=56)
+ 1/128 : (s1'=2) & (bc1'=57)
+ 1/128 : (s1'=2) & (bc1'=58)
+ 1/128 : (s1'=2) & (bc1'=59)
+ 1/128 : (s1'=2) & (bc1'=60)
+ 1/128 : (s1'=2) & (bc1'=61)
+ 1/128 : (s1'=2) & (bc1'=62)
+ 1/128 : (s1'=2) & (bc1'=63)
+ 1/128 : (s1'=2) & (bc1'=64)
+ 1/128 : (s1'=2) & (bc1'=65)
+ 1/128 : (s1'=2) & (bc1'=66)
+ 1/128 : (s1'=2) & (bc1'=67)
+ 1/128 : (s1'=2) & (bc1'=68)
+ 1/128 : (s1'=2) & (bc1'=69)
+ 1/128 : (s1'=2) & (bc1'=70)
+ 1/128 : (s1'=2) & (bc1'=71)
+ 1/128 : (s1'=2) & (bc1'=72)
+ 1/128 : (s1'=2) & (bc1'=73)
+ 1/128 : (s1'=2) & (bc1'=74)
+ 1/128 : (s1'=2) & (bc1'=75)
+ 1/128 : (s1'=2) & (bc1'=76)
+ 1/128 : (s1'=2) & (bc1'=77)
+ 1/128 : (s1'=2) & (bc1'=78)
+ 1/128 : (s1'=2) & (bc1'=79)
+ 1/128 : (s1'=2) & (bc1'=80)
+ 1/128 : (s1'=2) & (bc1'=81)
+ 1/128 : (s1'=2) & (bc1'=82)
+ 1/128 : (s1'=2) & (bc1'=83)
+ 1/128 : (s1'=2) & (bc1'=84)
+ 1/128 : (s1'=2) & (bc1'=85)
+ 1/128 : (s1'=2) & (bc1'=86)
+ 1/128 : (s1'=2) & (bc1'=87)
+ 1/128 : (s1'=2) & (bc1'=88)
+ 1/128 : (s1'=2) & (bc1'=89)
+ 1/128 : (s1'=2) & (bc1'=90)
+ 1/128 : (s1'=2) & (bc1'=91)
+ 1/128 : (s1'=2) & (bc1'=92)
+ 1/128 : (s1'=2) & (bc1'=93)
+ 1/128 : (s1'=2) & (bc1'=94)
+ 1/128 : (s1'=2) & (bc1'=95)
+ 1/128 : (s1'=2) & (bc1'=96)
+ 1/128 : (s1'=2) & (bc1'=97)
+ 1/128 : (s1'=2) & (bc1'=98)
+ 1/128 : (s1'=2) & (bc1'=99)
+ 1/128 : (s1'=2) & (bc1'=100)
+ 1/128 : (s1'=2) & (bc1'=101)
+ 1/128 : (s1'=2) & (bc1'=102)
+ 1/128 : (s1'=2) & (bc1'=103)
+ 1/128 : (s1'=2) & (bc1'=104)
+ 1/128 : (s1'=2) & (bc1'=105)
+ 1/128 : (s1'=2) & (bc1'=106)
+ 1/128 : (s1'=2) & (bc1'=107)
+ 1/128 : (s1'=2) & (bc1'=108)
+ 1/128 : (s1'=2) & (bc1'=109)
+ 1/128 : (s1'=2) & (bc1'=110)
+ 1/128 : (s1'=2) & (bc1'=111)
+ 1/128 : (s1'=2) & (bc1'=112)
+ 1/128 : (s1'=2) & (bc1'=113)
+ 1/128 : (s1'=2) & (bc1'=114)
+ 1/128 : (s1'=2) & (bc1'=115)
+ 1/128 : (s1'=2) & (bc1'=116)
+ 1/128 : (s1'=2) & (bc1'=117)
+ 1/128 : (s1'=2) & (bc1'=118)
+ 1/128 : (s1'=2) & (bc1'=119)
+ 1/128 : (s1'=2) & (bc1'=120)
+ 1/128 : (s1'=2) & (bc1'=121)
+ 1/128 : (s1'=2) & (bc1'=122)
+ 1/128 : (s1'=2) & (bc1'=123)
+ 1/128 : (s1'=2) & (bc1'=124)
+ 1/128 : (s1'=2) & (bc1'=125)
+ 1/128 : (s1'=2) & (bc1'=126)
+ 1/128 : (s1'=2) & (bc1'=127);
[sbc1] s1=1 & cd1=8 -> 1/256 : (s1'=2) & (bc1'=0)
+ 1/256 : (s1'=2) & (bc1'=1)
+ 1/256 : (s1'=2) & (bc1'=2)
+ 1/256 : (s1'=2) & (bc1'=3)
+ 1/256 : (s1'=2) & (bc1'=4)
+ 1/256 : (s1'=2) & (bc1'=5)
+ 1/256 : (s1'=2) & (bc1'=6)
+ 1/256 : (s1'=2) & (bc1'=7)
+ 1/256 : (s1'=2) & (bc1'=8)
+ 1/256 : (s1'=2) & (bc1'=9)
+ 1/256 : (s1'=2) & (bc1'=10)
+ 1/256 : (s1'=2) & (bc1'=11)
+ 1/256 : (s1'=2) & (bc1'=12)
+ 1/256 : (s1'=2) & (bc1'=13)
+ 1/256 : (s1'=2) & (bc1'=14)
+ 1/256 : (s1'=2) & (bc1'=15)
+ 1/256 : (s1'=2) & (bc1'=16)
+ 1/256 : (s1'=2) & (bc1'=17)
+ 1/256 : (s1'=2) & (bc1'=18)
+ 1/256 : (s1'=2) & (bc1'=19)
+ 1/256 : (s1'=2) & (bc1'=20)
+ 1/256 : (s1'=2) & (bc1'=21)
+ 1/256 : (s1'=2) & (bc1'=22)
+ 1/256 : (s1'=2) & (bc1'=23)
+ 1/256 : (s1'=2) & (bc1'=24)
+ 1/256 : (s1'=2) & (bc1'=25)
+ 1/256 : (s1'=2) & (bc1'=26)
+ 1/256 : (s1'=2) & (bc1'=27)
+ 1/256 : (s1'=2) & (bc1'=28)
+ 1/256 : (s1'=2) & (bc1'=29)
+ 1/256 : (s1'=2) & (bc1'=30)
+ 1/256 : (s1'=2) & (bc1'=31)
+ 1/256 : (s1'=2) & (bc1'=32)
+ 1/256 : (s1'=2) & (bc1'=33)
+ 1/256 : (s1'=2) & (bc1'=34)
+ 1/256 : (s1'=2) & (bc1'=35)
+ 1/256 : (s1'=2) & (bc1'=36)
+ 1/256 : (s1'=2) & (bc1'=37)
+ 1/256 : (s1'=2) & (bc1'=38)
+ 1/256 : (s1'=2) & (bc1'=39)
+ 1/256 : (s1'=2) & (bc1'=40)
+ 1/256 : (s1'=2) & (bc1'=41)
+ 1/256 : (s1'=2) & (bc1'=42)
+ 1/256 : (s1'=2) & (bc1'=43)
+ 1/256 : (s1'=2) & (bc1'=44)
+ 1/256 : (s1'=2) & (bc1'=45)
+ 1/256 : (s1'=2) & (bc1'=46)
+ 1/256 : (s1'=2) & (bc1'=47)
+ 1/256 : (s1'=2) & (bc1'=48)
+ 1/256 : (s1'=2) & (bc1'=49)
+ 1/256 : (s1'=2) & (bc1'=50)
+ 1/256 : (s1'=2) & (bc1'=51)
+ 1/256 : (s1'=2) & (bc1'=52)
+ 1/256 : (s1'=2) & (bc1'=53)
+ 1/256 : (s1'=2) & (bc1'=54)
+ 1/256 : (s1'=2) & (bc1'=55)
+ 1/256 : (s1'=2) & (bc1'=56)
+ 1/256 : (s1'=2) & (bc1'=57)
+ 1/256 : (s1'=2) & (bc1'=58)
+ 1/256 : (s1'=2) & (bc1'=59)
+ 1/256 : (s1'=2) & (bc1'=60)
+ 1/256 : (s1'=2) & (bc1'=61)
+ 1/256 : (s1'=2) & (bc1'=62)
+ 1/256 : (s1'=2) & (bc1'=63)
+ 1/256 : (s1'=2) & (bc1'=64)
+ 1/256 : (s1'=2) & (bc1'=65)
+ 1/256 : (s1'=2) & (bc1'=66)
+ 1/256 : (s1'=2) & (bc1'=67)
+ 1/256 : (s1'=2) & (bc1'=68)
+ 1/256 : (s1'=2) & (bc1'=69)
+ 1/256 : (s1'=2) & (bc1'=70)
+ 1/256 : (s1'=2) & (bc1'=71)
+ 1/256 : (s1'=2) & (bc1'=72)
+ 1/256 : (s1'=2) & (bc1'=73)
+ 1/256 : (s1'=2) & (bc1'=74)
+ 1/256 : (s1'=2) & (bc1'=75)
+ 1/256 : (s1'=2) & (bc1'=76)
+ 1/256 : (s1'=2) & (bc1'=77)
+ 1/256 : (s1'=2) & (bc1'=78)
+ 1/256 : (s1'=2) & (bc1'=79)
+ 1/256 : (s1'=2) & (bc1'=80)
+ 1/256 : (s1'=2) & (bc1'=81)
+ 1/256 : (s1'=2) & (bc1'=82)
+ 1/256 : (s1'=2) & (bc1'=83)
+ 1/256 : (s1'=2) & (bc1'=84)
+ 1/256 : (s1'=2) & (bc1'=85)
+ 1/256 : (s1'=2) & (bc1'=86)
+ 1/256 : (s1'=2) & (bc1'=87)
+ 1/256 : (s1'=2) & (bc1'=88)
+ 1/256 : (s1'=2) & (bc1'=89)
+ 1/256 : (s1'=2) & (bc1'=90)
+ 1/256 : (s1'=2) & (bc1'=91)
+ 1/256 : (s1'=2) & (bc1'=92)
+ 1/256 : (s1'=2) & (bc1'=93)
+ 1/256 : (s1'=2) & (bc1'=94)
+ 1/256 : (s1'=2) & (bc1'=95)
+ 1/256 : (s1'=2) & (bc1'=96)
+ 1/256 : (s1'=2) & (bc1'=97)
+ 1/256 : (s1'=2) & (bc1'=98)
+ 1/256 : (s1'=2) & (bc1'=99)
+ 1/256 : (s1'=2) & (bc1'=100)
+ 1/256 : (s1'=2) & (bc1'=101)
+ 1/256 : (s1'=2) & (bc1'=102)
+ 1/256 : (s1'=2) & (bc1'=103)
+ 1/256 : (s1'=2) & (bc1'=104)
+ 1/256 : (s1'=2) & (bc1'=105)
+ 1/256 : (s1'=2) & (bc1'=106)
+ 1/256 : (s1'=2) & (bc1'=107)
+ 1/256 : (s1'=2) & (bc1'=108)
+ 1/256 : (s1'=2) & (bc1'=109)
+ 1/256 : (s1'=2) & (bc1'=110)
+ 1/256 : (s1'=2) & (bc1'=111)
+ 1/256 : (s1'=2) & (bc1'=112)
+ 1/256 : (s1'=2) & (bc1'=113)
+ 1/256 : (s1'=2) & (bc1'=114)
+ 1/256 : (s1'=2) & (bc1'=115)
+ 1/256 : (s1'=2) & (bc1'=116)
+ 1/256 : (s1'=2) & (bc1'=117)
+ 1/256 : (s1'=2) & (bc1'=118)
+ 1/256 : (s1'=2) & (bc1'=119)
+ 1/256 : (s1'=2) & (bc1'=120)
+ 1/256 : (s1'=2) & (bc1'=121)
+ 1/256 : (s1'=2) & (bc1'=122)
+ 1/256 : (s1'=2) & (bc1'=123)
+ 1/256 : (s1'=2) & (bc1'=124)
+ 1/256 : (s1'=2) & (bc1'=125)
+ 1/256 : (s1'=2) & (bc1'=126)
+ 1/256 : (s1'=2) & (bc1'=127)
+ 1/256 : (s1'=2) & (bc1'=128)
+ 1/256 : (s1'=2) & (bc1'=129)
+ 1/256 : (s1'=2) & (bc1'=130)
+ 1/256 : (s1'=2) & (bc1'=131)
+ 1/256 : (s1'=2) & (bc1'=132)
+ 1/256 : (s1'=2) & (bc1'=133)
+ 1/256 : (s1'=2) & (bc1'=134)
+ 1/256 : (s1'=2) & (bc1'=135)
+ 1/256 : (s1'=2) & (bc1'=136)
+ 1/256 : (s1'=2) & (bc1'=137)
+ 1/256 : (s1'=2) & (bc1'=138)
+ 1/256 : (s1'=2) & (bc1'=139)
+ 1/256 : (s1'=2) & (bc1'=140)
+ 1/256 : (s1'=2) & (bc1'=141)
+ 1/256 : (s1'=2) & (bc1'=142)
+ 1/256 : (s1'=2) & (bc1'=143)
+ 1/256 : (s1'=2) & (bc1'=144)
+ 1/256 : (s1'=2) & (bc1'=145)
+ 1/256 : (s1'=2) & (bc1'=146)
+ 1/256 : (s1'=2) & (bc1'=147)
+ 1/256 : (s1'=2) & (bc1'=148)
+ 1/256 : (s1'=2) & (bc1'=149)
+ 1/256 : (s1'=2) & (bc1'=150)
+ 1/256 : (s1'=2) & (bc1'=151)
+ 1/256 : (s1'=2) & (bc1'=152)
+ 1/256 : (s1'=2) & (bc1'=153)
+ 1/256 : (s1'=2) & (bc1'=154)
+ 1/256 : (s1'=2) & (bc1'=155)
+ 1/256 : (s1'=2) & (bc1'=156)
+ 1/256 : (s1'=2) & (bc1'=157)
+ 1/256 : (s1'=2) & (bc1'=158)
+ 1/256 : (s1'=2) & (bc1'=159)
+ 1/256 : (s1'=2) & (bc1'=160)
+ 1/256 : (s1'=2) & (bc1'=161)
+ 1/256 : (s1'=2) & (bc1'=162)
+ 1/256 : (s1'=2) & (bc1'=163)
+ 1/256 : (s1'=2) & (bc1'=164)
+ 1/256 : (s1'=2) & (bc1'=165)
+ 1/256 : (s1'=2) & (bc1'=166)
+ 1/256 : (s1'=2) & (bc1'=167)
+ 1/256 : (s1'=2) & (bc1'=168)
+ 1/256 : (s1'=2) & (bc1'=169)
+ 1/256 : (s1'=2) & (bc1'=170)
+ 1/256 : (s1'=2) & (bc1'=171)
+ 1/256 : (s1'=2) & (bc1'=172)
+ 1/256 : (s1'=2) & (bc1'=173)
+ 1/256 : (s1'=2) & (bc1'=174)
+ 1/256 : (s1'=2) & (bc1'=175)
+ 1/256 : (s1'=2) & (bc1'=176)
+ 1/256 : (s1'=2) & (bc1'=177)
+ 1/256 : (s1'=2) & (bc1'=178)
+ 1/256 : (s1'=2) & (bc1'=179)
+ 1/256 : (s1'=2) & (bc1'=180)
+ 1/256 : (s1'=2) & (bc1'=181)
+ 1/256 : (s1'=2) & (bc1'=182)
+ 1/256 : (s1'=2) & (bc1'=183)
+ 1/256 : (s1'=2) & (bc1'=184)
+ 1/256 : (s1'=2) & (bc1'=185)
+ 1/256 : (s1'=2) & (bc1'=186)
+ 1/256 : (s1'=2) & (bc1'=187)
+ 1/256 : (s1'=2) & (bc1'=188)
+ 1/256 : (s1'=2) & (bc1'=189)
+ 1/256 : (s1'=2) & (bc1'=190)
+ 1/256 : (s1'=2) & (bc1'=191)
+ 1/256 : (s1'=2) & (bc1'=192)
+ 1/256 : (s1'=2) & (bc1'=193)
+ 1/256 : (s1'=2) & (bc1'=194)
+ 1/256 : (s1'=2) & (bc1'=195)
+ 1/256 : (s1'=2) & (bc1'=196)
+ 1/256 : (s1'=2) & (bc1'=197)
+ 1/256 : (s1'=2) & (bc1'=198)
+ 1/256 : (s1'=2) & (bc1'=199)
+ 1/256 : (s1'=2) & (bc1'=200)
+ 1/256 : (s1'=2) & (bc1'=201)
+ 1/256 : (s1'=2) & (bc1'=202)
+ 1/256 : (s1'=2) & (bc1'=203)
+ 1/256 : (s1'=2) & (bc1'=204)
+ 1/256 : (s1'=2) & (bc1'=205)
+ 1/256 : (s1'=2) & (bc1'=206)
+ 1/256 : (s1'=2) & (bc1'=207)
+ 1/256 : (s1'=2) & (bc1'=208)
+ 1/256 : (s1'=2) & (bc1'=209)
+ 1/256 : (s1'=2) & (bc1'=210)
+ 1/256 : (s1'=2) & (bc1'=211)
+ 1/256 : (s1'=2) & (bc1'=212)
+ 1/256 : (s1'=2) & (bc1'=213)
+ 1/256 : (s1'=2) & (bc1'=214)
+ 1/256 : (s1'=2) & (bc1'=215)
+ 1/256 : (s1'=2) & (bc1'=216)
+ 1/256 : (s1'=2) & (bc1'=217)
+ 1/256 : (s1'=2) & (bc1'=218)
+ 1/256 : (s1'=2) & (bc1'=219)
+ 1/256 : (s1'=2) & (bc1'=220)
+ 1/256 : (s1'=2) & (bc1'=221)
+ 1/256 : (s1'=2) & (bc1'=222)
+ 1/256 : (s1'=2) & (bc1'=223)
+ 1/256 : (s1'=2) & (bc1'=224)
+ 1/256 : (s1'=2) & (bc1'=225)
+ 1/256 : (s1'=2) & (bc1'=226)
+ 1/256 : (s1'=2) & (bc1'=227)
+ 1/256 : (s1'=2) & (bc1'=228)
+ 1/256 : (s1'=2) & (bc1'=229)
+ 1/256 : (s1'=2) & (bc1'=230)
+ 1/256 : (s1'=2) & (bc1'=231)
+ 1/256 : (s1'=2) & (bc1'=232)
+ 1/256 : (s1'=2) & (bc1'=233)
+ 1/256 : (s1'=2) & (bc1'=234)
+ 1/256 : (s1'=2) & (bc1'=235)
+ 1/256 : (s1'=2) & (bc1'=236)
+ 1/256 : (s1'=2) & (bc1'=237)
+ 1/256 : (s1'=2) & (bc1'=238)
+ 1/256 : (s1'=2) & (bc1'=239)
+ 1/256 : (s1'=2) & (bc1'=240)
+ 1/256 : (s1'=2) & (bc1'=241)
+ 1/256 : (s1'=2) & (bc1'=242)
+ 1/256 : (s1'=2) & (bc1'=243)
+ 1/256 : (s1'=2) & (bc1'=244)
+ 1/256 : (s1'=2) & (bc1'=245)
+ 1/256 : (s1'=2) & (bc1'=246)
+ 1/256 : (s1'=2) & (bc1'=247)
+ 1/256 : (s1'=2) & (bc1'=248)
+ 1/256 : (s1'=2) & (bc1'=249)
+ 1/256 : (s1'=2) & (bc1'=250)
+ 1/256 : (s1'=2) & (bc1'=251)
+ 1/256 : (s1'=2) & (bc1'=252)
+ 1/256 : (s1'=2) & (bc1'=253)
+ 1/256 : (s1'=2) & (bc1'=254)
+ 1/256 : (s1'=2) & (bc1'=255);
// backs off
[boff1] tick & s1=2 & bc1>0 -> (bc1'=bc1-1); // decrement counter
[boff1] tick & s1=2 & bc1=0 -> (tr1'=1) & (s1'=0); // finish backoff so transmit again

endmodule

// construct further users through renaming
// (need to rename s2, s3, tr2 and tr3 as they appear in formulae)
module user2=user1[s1=s2,s2=s1,tr1=tr2,tr2=tr1,bc1=bc2,cd1=cd2,wait1=wait2,trans1=trans2,try1=try2,boff1=boff2,sbc1=sbc2,t1=t2] endmodule
module user3=user1[s1=s3,s3=s1,tr1=tr3,tr3=tr1,bc1=bc3,cd1=cd3,wait1=wait3,trans1=trans3,try1=try3,boff1=boff3,sbc1=sbc3,t1=t3] endmodule

// module for counting when time passes (slots)
module timer

t : [0..D+1];

[] tick -> (t'=min(D+1,t+1));

endmodule

// reward structure for time passage
rewards "time"
tick : 1;
endrewards
```