#import "PAT.Lib.Prob";

#define targetStep 30; //the step you want to check

#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];

var step = 0;

PlayerChooseAction(i, stepBound) =

[step < targetStep]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)

};

RoundFinish = {

step++;

ActionHolder[1] = ActionChooser[1];

ActionHolder[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;

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 && step <= targetStep;

#assert aSystem reaches MDO with prob;