Skip to content

Commit 5c8abf0

Browse files
committed
[Tutorial] Update hints for PEx
[PEx] minor change
1 parent 199ffec commit 5c8abf0

File tree

4 files changed

+13
-11
lines changed

4 files changed

+13
-11
lines changed

Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,8 @@ public TooManyChoicesException(String loc, int numChoices) {
2323
*/
2424
public TooManyChoicesException(String loc, int numChoices, int numCalls) {
2525
super(String.format("""
26-
%s: too many choices generated from this location - total %d choices after %d choose calls.
27-
Reduce the total number of choices generated here to at most %d, by reducing the number times this choose statement is called.
28-
For example, limit the number of transactions/requests etc.""",
26+
%s: too many choices generated from this statement - total %d choices after %d choose calls.
27+
Reduce the total number of choices generated here to at most %d, by reducing the number of times this choose statement is called.""",
2928
loc, numChoices, numCalls, PExGlobal.getConfig().getMaxChoicesPerStmtPerSchedule()));
3029
}
3130
}

Tutorial/1_ClientServer/PSrc/Client.p

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,10 @@ machine Client
7070
print format ("Withdrawal with rId = {0} failed, account balance = {1}", resp.rId, resp.balance);
7171
}
7272

73+
if (currentBalance > 10)
74+
/* Hint 3: Reduce the number of times WithdrawAmount() is called by changing the above line to the following:
7375
if (currentBalance > 10 && nextReqId < (accountId*100 + 5))
76+
*/
7477
{
7578
print format ("Still have account balance = {0}, lets try and withdraw more", currentBalance);
7679
goto WithdrawMoney;
@@ -81,9 +84,9 @@ machine Client
8184
// function that returns a random integer between (1 to current balance + 1)
8285
fun WithdrawAmount() : int {
8386
return choose(currentBalance) + 1;
84-
/* Hint 2: Decrease the amount of data non-determinism by changing the above line to the following:
85-
return ((choose(5) * currentBalance) / 4) + 1;
86-
*/
87+
/* Hint 2: Reduce the number of choices by changing the above line to the following:
88+
return ((choose(5) * currentBalance) / 4) + 1;
89+
*/
8790
}
8891

8992
state NoMoneyToWithDraw {

Tutorial/1_ClientServer/PTst/TestDriver.p

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -28,9 +28,9 @@ fun CreateRandomInitialAccounts(numAccounts: int) : map[int, int]
2828
var bankBalance: map[int, int];
2929
while(i < numAccounts) {
3030
bankBalance[i] = choose(100) + 10; // min 10 in the account
31-
/* Hint 1: Decrease the amount of data non-determinism by changing the above line to the following:
32-
bankBalance[i] = choose(5) + 10; // min 10 in the account
33-
*/
31+
/* Hint 1: Reduce the number of choices by changing the above line to the following:
32+
bankBalance[i] = choose(10) + 10; // min 10 in the account
33+
*/
3434
i = i + 1;
3535
}
3636
return bankBalance;

Tutorial/2_TwoPhaseCommit/PForeign/PExForeignCode.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
import java.util.Random;
99

1010
public class PExForeignCode {
11-
/* Not recommended to use data non-determinism in PEx foreign code
11+
/* Not allowed to use data non-determinism in PEx foreign code. So we cannot do the following:
1212
public static PNamedTuple ChooseRandomTransaction(PInt uniqueId) {
1313
Map<String, PValue<?>> values = new HashMap<>();
1414
Random rand = new Random();
@@ -18,5 +18,5 @@ public static PNamedTuple ChooseRandomTransaction(PInt uniqueId) {
1818
1919
return new PNamedTuple(values);
2020
}
21-
*/
21+
*/
2222
}

0 commit comments

Comments
 (0)