[Tutorial] Update hints for PEx

[PEx] minor change

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()));
     }
 }

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 {

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;

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<String, PValue<?>> values = new HashMap<>();
         Random rand = new Random();
@@ -18,5 +18,5 @@ public static PNamedTuple ChooseRandomTransaction(PInt uniqueId) {
 
         return new PNamedTuple(values);
     }
-    */
+*/
 }