#import "PAT.Lib.Prob";//external C# library is imported.
#define num_of_action 4;
var ActionHolder[num_of_action + 1] = [0, 4, 0, 0, 0];
var ActionChooser[num_of_action + 1];
var SequentialNumber[num_of_action + 1];
PlayerChooseAction(i, stepBound) =
ifa(SequentialNumber[i] < stepBound && ActionHolder[i] > 1){
pcase{
//method defined
in external library is used to assign the transition probability
call(probability, ActionHolder, 1, i) :{ActionChooser[1]++; SequentialNumber[i]++}->PlayerChooseAction(i, stepBound)
call(probability, ActionHolder, 2, i) :{ActionChooser[2]++; SequentialNumber[i]++}->PlayerChooseAction(i, stepBound)
call(probability, ActionHolder, 3, i) :{ActionChooser[3]++; SequentialNumber[i]++}->PlayerChooseAction(i, stepBound)
call(probability, ActionHolder, 4, i) :{ActionChooser[4]++; SequentialNumber[i]++}->PlayerChooseAction(i, stepBound)
}
}
else ifa(SequentialNumber[i] == stepBound)
{
Skip
}
else
{
{ActionChooser[i]++; SequentialNumber[i]++} -> PlayerChooseAction(i, stepBound)
};
//When all agents finish their choice
in this round, the following process is activated to update the variables for
next round.
RoundFinish = {
ActionHolder[1] = ActionChooser[1]; AtionHolder[2] = ActionChooser[2]; ActionHolder[3] = ActionChooser[3]; ActionHolder[4] = ActionChooser[4];
ActionChooser[1] = 0; ActionChooser[2] = 0; ActionChooser[3] = 0; ActionChooser[4] = 0;
SequentialNumber[1] = 0; SequentialNumber[2] = 0; SequentialNumber[3] = 0; SequentialNumber[4] = 0;
}->Skip;
//whole system is defined as
follows.
System(a1, a2, a3, a4) = PlayerChooseAction(1, a1);PlayerChooseAction(2, a2);PlayerChooseAction(3, a3);PlayerChooseAction(4, a4)
;RoundFinish;System(ActionHolder[1], ActionHolder[2], ActionHolder[3], ActionHolder[4]);
aSystem = System(4, 0, 0, 0);
///////////////////////////////////////////////////property
to be checked/////////////////////////////////////////
#define MDO ActionHolder[1] == 1 && ActionHolder[2] == 1 && ActionHolder[3] == 1 && ActionHolder[4] == 1;//MDO is defined
#assert aSystem |= <>[]MDO with prob;//The probability
of convergence