From 5c8abf093ba225b277f9f22124d26c834cbe6d9b Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Thu, 5 Sep 2024 21:31:31 +0000 Subject: [PATCH] [Tutorial] Update hints for PEx [PEx] minor change --- .../pex/utils/exceptions/TooManyChoicesException.java | 5 ++--- Tutorial/1_ClientServer/PSrc/Client.p | 9 ++++++--- Tutorial/1_ClientServer/PTst/TestDriver.p | 6 +++--- Tutorial/2_TwoPhaseCommit/PForeign/PExForeignCode.java | 4 ++-- 4 files changed, 13 insertions(+), 11 deletions(-) diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java index a92fbca3a0..e739e67a15 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java @@ -23,9 +23,8 @@ public TooManyChoicesException(String loc, int numChoices) { */ public TooManyChoicesException(String loc, int numChoices, int numCalls) { super(String.format(""" - %s: too many choices generated from this location - total %d choices after %d choose calls. - Reduce the total number of choices generated here to at most %d, by reducing the number times this choose statement is called. - For example, limit the number of transactions/requests etc.""", + %s: too many choices generated from this statement - total %d choices after %d choose calls. + Reduce the total number of choices generated here to at most %d, by reducing the number of times this choose statement is called.""", loc, numChoices, numCalls, PExGlobal.getConfig().getMaxChoicesPerStmtPerSchedule())); } } diff --git a/Tutorial/1_ClientServer/PSrc/Client.p b/Tutorial/1_ClientServer/PSrc/Client.p index a7dbacdd28..81b88b359e 100644 --- a/Tutorial/1_ClientServer/PSrc/Client.p +++ b/Tutorial/1_ClientServer/PSrc/Client.p @@ -70,7 +70,10 @@ machine Client print format ("Withdrawal with rId = {0} failed, account balance = {1}", resp.rId, resp.balance); } + if (currentBalance > 10) +/* Hint 3: Reduce the number of times WithdrawAmount() is called by changing the above line to the following: if (currentBalance > 10 && nextReqId < (accountId*100 + 5)) +*/ { print format ("Still have account balance = {0}, lets try and withdraw more", currentBalance); goto WithdrawMoney; @@ -81,9 +84,9 @@ machine Client // function that returns a random integer between (1 to current balance + 1) fun WithdrawAmount() : int { return choose(currentBalance) + 1; - /* Hint 2: Decrease the amount of data non-determinism by changing the above line to the following: - return ((choose(5) * currentBalance) / 4) + 1; - */ +/* Hint 2: Reduce the number of choices by changing the above line to the following: + return ((choose(5) * currentBalance) / 4) + 1; +*/ } state NoMoneyToWithDraw { diff --git a/Tutorial/1_ClientServer/PTst/TestDriver.p b/Tutorial/1_ClientServer/PTst/TestDriver.p index 4526a6e40a..effb03e008 100644 --- a/Tutorial/1_ClientServer/PTst/TestDriver.p +++ b/Tutorial/1_ClientServer/PTst/TestDriver.p @@ -28,9 +28,9 @@ fun CreateRandomInitialAccounts(numAccounts: int) : map[int, int] var bankBalance: map[int, int]; while(i < numAccounts) { bankBalance[i] = choose(100) + 10; // min 10 in the account - /* Hint 1: Decrease the amount of data non-determinism by changing the above line to the following: - bankBalance[i] = choose(5) + 10; // min 10 in the account - */ +/* Hint 1: Reduce the number of choices by changing the above line to the following: + bankBalance[i] = choose(10) + 10; // min 10 in the account +*/ i = i + 1; } return bankBalance; diff --git a/Tutorial/2_TwoPhaseCommit/PForeign/PExForeignCode.java b/Tutorial/2_TwoPhaseCommit/PForeign/PExForeignCode.java index 33a4af6752..8619e8a97c 100644 --- a/Tutorial/2_TwoPhaseCommit/PForeign/PExForeignCode.java +++ b/Tutorial/2_TwoPhaseCommit/PForeign/PExForeignCode.java @@ -8,7 +8,7 @@ import java.util.Random; public class PExForeignCode { - /* Not recommended to use data non-determinism in PEx foreign code +/* Not allowed to use data non-determinism in PEx foreign code. So we cannot do the following: public static PNamedTuple ChooseRandomTransaction(PInt uniqueId) { Map> values = new HashMap<>(); Random rand = new Random(); @@ -18,5 +18,5 @@ public static PNamedTuple ChooseRandomTransaction(PInt uniqueId) { return new PNamedTuple(values); } - */ +*/ }