Limit number of choices in a choose(.) to atmost 10,000

Adds throwing a compile-time or runtime error if the number of choices in a choose(.) is greater than 10000.

Updates GitHub docs to reflect this change.

Docs/docs/manual/expressions.md

@@ -342,3 +342,12 @@ The choose operation can be used to model nondeterministic environment machines
 
 !!! note ""
     Performing a `choose` over an empty collection leads to an error. Also, `choose` from a `map` value returns a random key from the map.
+
+Note that the maximum number of choices allowed in a `choose(expr)` is 10,000. Performing a `choose` with an `int` value greater than 10000 or over a collection with more than 10000 elements leads to an error.
+
+``` java
+choose(10001) // throws a compile-time error
+choose(x)     // throws a runtime error if x is of integer type and has value greater than 10000
+choose(x)     // throws a runtime error if x is of seq/set/map type and has size greater than 10000 elements
+```
+

Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs

@@ -159,6 +159,11 @@ public Exception IllegalChooseSubExprType(PParser.ChooseExprContext context, PLa
             return IssueError(context, $"choose expects a parameter of type int (max value) or a collection type (seq, set, or map) got a parameter of type {subExprType}");
         }
 
+        public Exception IllegalChooseSubExprValue(PParser.ChooseExprContext context, int numChoices)
+        {
+            return IssueError(context, $"choose expects a parameter with at most 10000 choices, got {numChoices} choices instead.");
+        }
+
         public Exception IllegalFunctionUsedInSpecMachine(Function function, Machine callerOwner)
         {
             return IssueError(function.SourceLocation,

Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs

@@ -116,6 +116,7 @@ Exception DuplicateStartState(
         Exception MoreThanOneParameterForHandlers(ParserRuleContext sourceLocation, int count);
 
         Exception IllegalChooseSubExprType(PParser.ChooseExprContext context, PLanguageType subExprType);
+        Exception IllegalChooseSubExprValue(PParser.ChooseExprContext context, int numChoices);
         Exception IllegalFunctionUsedInSpecMachine(Function function, Machine callerOwner);
 
         String SpecObservesSetIncompleteWarning(ParserRuleContext loc, PEvent ev, Machine machine);

Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs

@@ -393,7 +393,11 @@ public override IPExpr VisitChooseExpr(PParser.ChooseExprContext context)
                     return new ChooseExpr(context, subExpr, mapType.KeyType);
 
                 case PrimitiveType primType when primType.IsSameTypeAs(PrimitiveType.Int):
+                {
+                    if (subExpr is IntLiteralExpr subExprAsInt && subExprAsInt.Value > 10000)
+                        throw handler.IllegalChooseSubExprValue(context, subExprAsInt.Value);
                     return new ChooseExpr(context, subExpr, PrimitiveType.Int);
+                }
 
                 default:
                     throw handler.IllegalChooseSubExprType(context, subExprType);

Src/PRuntimes/PCSharpRuntime/PMachine.cs

@@ -136,21 +136,27 @@ public IPrtValue TryRandom(IPrtValue param)
             switch (param)
             {
                 case PrtInt maxValue:
+                {
+                    TryAssert(maxValue <= 10000, $"choose expects a parameter with at most 10000 choices, got {maxValue} choices instead.");
                     return (PrtInt)TryRandomInt(maxValue);
+                }
 
                 case PrtSeq seq:
                 {
                     TryAssert(seq.Any(), "Trying to choose from an empty sequence!");
+                    TryAssert(seq.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {seq.Count} choices instead.");
                     return seq[TryRandomInt(seq.Count)];
                 }
                 case PrtSet set:
                 {
                     TryAssert(set.Any(), "Trying to choose from an empty set!");
+                    TryAssert(set.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {set.Count} choices instead.");
                     return set.ElementAt(TryRandomInt(set.Count));
                 }
                 case PrtMap map:
                 {
                     TryAssert(map.Any(), "Trying to choose from an empty map!");
+                    TryAssert(map.Keys.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {map.Keys.Count} choices instead.");
                     return map.Keys.ElementAt(TryRandomInt(map.Keys.Count));
                 }
                 default: