dtmc

global inchannelOne : [0..4] init 4;//suppose at beginning 4 players are all in channel 1

global inchannelTwo : [0..4];

global inchannelThree : [0..4];

global inchannelFour : [0..4];

global inchannelOneNextRound : [0..4];//temporarily record how many agents choose action 1 in next round

global inchannelTwoNextRound : [0..4];

global inchannelThreeNextRound : [0..4];

global inchannelFourNextRound : [0..4];

global p1end : bool init false;//record if Agent1 module ends or not

global p2end : bool init false;

global p3end : bool init false;

global p4end : bool init false;

global RoundBegin : bool init true;

//p5end : bool init false;

//p6end : bool init false;

formula safe = inchannelOneNextRound < 4 & inchannelTwoNextRound < 4 & inchannelThreeNextRound < 4 & inchannelFourNextRound < 4;

module Agent1

p1 :[0..4] init 1;

//0 idle

//1 in channel 1

//2 in channel 2

//3 in channel 3

//4 in channel 4

//no channel has just one player

[] safe & RoundBegin & inchannelOne!=1 & inchannelTwo!=1 & inchannelThree!=1 & inchannelFour != 1 ->

0.25 : (p1'=1)& (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

0.25 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

0.25 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1) +

0.25 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

//p1 is the only agent in channel 1

[] safe & RoundBegin & p1=1 & inchannelOne=1 -> (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1);

[] safe & RoundBegin & p1=1 & inchannelOne!=1 & inchannelTwo=1 & inchannelThree!=1 & inchannelFour!=1 ->

1/3 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

1/3 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1) +

1/3 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=1 & inchannelOne!=1 & inchannelTwo!=1 & inchannelThree=1 & inchannelFour!=1 ->

1/3 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

1/3 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

1/3 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=1 & inchannelOne!=1 & inchannelTwo!=1 & inchannelThree!=1 & inchannelFour=1 ->

1/3 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

1/3 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

1/3 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1);

[] safe & RoundBegin & p1=1 & inchannelOne!=1 & inchannelTwo=1 & inchannelThree=1 & inchannelFour!=1 ->

0.5 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

0.5 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=1 & inchannelOne!=1 & inchannelTwo=1 & inchannelThree!=1 & inchannelFour=1 ->

0.5 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

0.5 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1);

[] safe & RoundBegin & p1=1 & inchannelOne!=1 & inchannelTwo!=1 & inchannelThree=1 & inchannelFour=1 ->

0.5 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

0.5 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1);

//p1 is the only aget in channel 2

[] safe & RoundBegin & p1=2 & inchannelTwo=1 -> (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1);

[] safe & RoundBegin & p1=2 & inchannelOne=1 & inchannelTwo!=1 & inchannelThree!=1 & inchannelFour!=1 ->

1/3 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

1/3 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1) +

1/3 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=2 & inchannelOne!=1 & inchannelTwo!=1 & inchannelThree=1 & inchannelFour!=1 ->

1/3 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

1/3 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

1/3 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=2 & inchannelOne!=1 & inchannelTwo!=1 & inchannelThree!=1 & inchannelFour=1 ->

1/3 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

1/3 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

1/3 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1);

[] safe & RoundBegin & p1=2 & inchannelOne=1 & inchannelTwo!=1 & inchannelThree=1 & inchannelFour!=1 ->

0.5 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

0.5 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=2 & inchannelOne=1 & inchannelTwo!=1 & inchannelThree!=1 & inchannelFour=1 ->

0.5 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

0.5 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1);

[] safe & RoundBegin & p1=2 & inchannelOne!=1 & inchannelTwo!=1 & inchannelThree=1 & inchannelFour=1 ->

0.5 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

0.5 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1);

//p1 is the only agent in channel 3

[] safe & RoundBegin & p1=3 & inchannelThree=1 -> (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1);

[] safe & RoundBegin & p1=3 & inchannelOne=1 & inchannelTwo!=1 & inchannelThree!=1 & inchannelFour!=1 ->

1/3 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

1/3 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1) +

1/3 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=3 & inchannelOne!=1 & inchannelTwo=1 & inchannelThree!=1 & inchannelFour!=1 ->

1/3 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

1/3 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1) +

1/3 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=3 & inchannelOne!=1 & inchannelTwo!=1 & inchannelThree!=1 & inchannelFour=1 ->

1/3 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

1/3 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

1/3 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1);

[] safe & RoundBegin & p1=3 & inchannelOne=1 & inchannelTwo=1 & inchannelThree!=1 & inchannelFour!=1 ->

0.5 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1) +

0.5 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=3 & inchannelOne=1 & inchannelTwo!=1 & inchannelThree!=1 & inchannelFour=1 ->

0.5 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

0.5 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1);

[] safe & RoundBegin & p1=3 & inchannelOne!=1 & inchannelTwo=1 & inchannelThree!=1 & inchannelFour=1 ->

0.5 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

0.5 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1);

//p1 is the only agent in channel 4

[] safe & RoundBegin & p1=4 & inchannelFour=1 -> (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=4 & inchannelOne=1 & inchannelTwo!=1 & inchannelThree!=1 & inchannelFour!=1 ->

1/3 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

1/3 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1) +

1/3 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=4 & inchannelOne!=1 & inchannelTwo=1 & inchannelThree!=1 & inchannelFour!=1 ->

1/3 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

1/3 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1) +

1/3 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=4 & inchannelOne!=1 & inchannelTwo!=1 & inchannelThree=1 & inchannelFour!=1 ->

1/3 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

1/3 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

1/3 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=4 & inchannelOne=1 & inchannelTwo=1 & inchannelThree!=1 & inchannelFour!=1 ->

0.5 : (p1'=3) & (p1end'=true) & (RoundBegin'=false) & (inchannelThreeNextRound' = inchannelThreeNextRound + 1) +

0.5 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=4 & inchannelOne=1 & inchannelTwo!=1 & inchannelThree=1 & inchannelFour!=1 ->

0.5 : (p1'=2) & (p1end'=true) & (RoundBegin'=false) & (inchannelTwoNextRound' = inchannelTwoNextRound + 1) +

0.5 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

[] safe & RoundBegin & p1=4 & inchannelOne!=1 & inchannelTwo=1 & inchannelThree=1 & inchannelFour!=1 ->

0.5 : (p1'=1) & (p1end'=true) & (RoundBegin'=false) & (inchannelOneNextRound' = inchannelOneNextRound + 1) +

0.5 : (p1'=4) & (p1end'=true) & (RoundBegin'=false) & (inchannelFourNextRound' = inchannelFourNextRound + 1);

endmodule

module Agent2 = Agent1[RoundBegin=p1end, p1end=p2end, p1=p2] endmodule

module Agent3 = Agent1[RoundBegin=p2end, p1end=p3end, p1=p3] endmodule

module Agent4 = Agent1[RoundBegin=p3end, p1end=p4end, p1=p4] endmodule

module Roundfinish

[] p4end -> (inchannelOne'=inchannelOneNextRound) & (inchannelOneNextRound'=0) & (inchannelTwo'=inchannelTwoNextRound) & (inchannelTwoNextRound'=0) &

(inchannelThree'=inchannelThreeNextRound) & (inchannelThreeNextRound'=0) & (inchannelFour'=inchannelFourNextRound) & (inchannelFourNextRound'=0) &

(RoundBegin'=true) & (p4end'=false);

endmodule

label "MDO" = inchannelOne=1&inchannelTwo=1&inchannelThree=1&inchannelFour=1;