#import "PAT.Lib.Prob";

#define num_of_action 2;

#define num_of_agent 4;

var ActionHolder[num_of_action + 1] = [0, 4, 0];

var ActionChooser[num_of_action + 1];

var SequentialNumber[num_of_action + 1];

var terminal = false;

PlayerChooseAction(i, stepBound) =

ifa(SequentialNumber[i] < stepBound && ActionHolder[i] > call(numOfPlayerfloor, num_of_agent, num_of_action)){

pcase{

//method defined in external library is used to assign the transition probability

call(probability_1, ActionHolder, 1, i,num_of_agent,num_of_action) :{ActionChooser[1]++; SequentialNumber[i]++}->PlayerChooseAction(i, stepBound)

call(probability_1, ActionHolder, 2, i,num_of_agent,num_of_action) :{ActionChooser[2]++; SequentialNumber[i]++}->PlayerChooseAction(i, stepBound)

}

}

else ifa(SequentialNumber[i] == stepBound)

{

Skip

}

else

{

{ActionChooser[i]++; SequentialNumber[i]++} -> PlayerChooseAction(i, stepBound)

};

RoundFinish = ifa(MDO){{

ActionHolder[1] = ActionChooser[1];

ActionHolder[2] = ActionChooser[2];

ActionChooser[1] = 0;

ActionChooser[2] = 0;

SequentialNumber[1] = 0;

SequentialNumber[2] = 0;

terminal = true

}->Stop}

else {{

ActionHolder[1] = ActionChooser[1];

ActionHolder[2] = ActionChooser[2];

ActionChooser[1] = 0;

ActionChooser[2] = 0;

SequentialNumber[1] = 0;

SequentialNumber[2] = 0;

}->Skip};

System(a1, a2) = PlayerChooseAction(1, a1);PlayerChooseAction(2, a2)

;RoundFinish;System(ActionHolder[1], ActionHolder[2]);

aSystem = System(ActionHolder[1], ActionHolder[2]);

///////////////////////////////properties to be checked///////////////////

#define MDO call(isMDO, ActionHolder, num_of_action, num_of_agent);

#assert aSystem() |= <>[] MDO with prob;//convergence

#define Goal !MDO && terminal;

#assert aSystem() reaches Goal with prob;//check the probability that exiting from MDO state