Adds regression tests for choose exceeding 10000 choices

p-org · May 2, 2024 · 895d1f1 · 895d1f1
1 parent 9b7d2aa
commit 895d1f1
Show file tree

Hide file tree

Showing 5 changed files with 96 additions and 0 deletions.
diff --git a/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesInt/tooManyChoicesInt.p b/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesInt/tooManyChoicesInt.p
@@ -0,0 +1,16 @@
+machine Main {
+	start state S {
+		entry {
+		    var x: int;
+		    var y: int;
+
+		    x = 10000;
+		    y = choose(x); // OK
+		    print format("y is {0}", y);
+
+		    x = 10001;
+		    y = choose(x); // error
+		    print format("y is {0}", y);
+		}
+	}
+}
diff --git a/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesMap/tooManyChoicesMap.p b/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesMap/tooManyChoicesMap.p
@@ -0,0 +1,22 @@
+machine Main {
+	start state S {
+		entry {
+		    var x: map[int, int];
+		    var y: int;
+		    var i: int;
+
+            i = 0;
+            while (i < 10000) {
+                x[i] = i;
+                i = i + 1;
+            }
+
+		    y = choose(x); // OK
+		    print format("y is {0}", y);
+
+            x[i] = i;
+		    y = choose(x); // error
+		    print format("y is {0}", y);
+		}
+	}
+}
diff --git a/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSeq/tooManyChoicesSeq.p b/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSeq/tooManyChoicesSeq.p
@@ -0,0 +1,22 @@
+machine Main {
+	start state S {
+		entry {
+		    var x: seq[int];
+		    var y: int;
+		    var i: int;
+
+            i = 0;
+            while (i < 10000) {
+                x += (i, i);
+                i = i + 1;
+            }
+
+		    y = choose(x); // OK
+		    print format("y is {0}", y);
+
+            x += (i, i);
+		    y = choose(x); // error
+		    print format("y is {0}", y);
+		}
+	}
+}
diff --git a/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSet/tooManyChoicesSet.p b/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSet/tooManyChoicesSet.p
@@ -0,0 +1,22 @@
+machine Main {
+	start state S {
+		entry {
+		    var x: set[int];
+		    var y: int;
+		    var i: int;
+
+            i = 0;
+            while (i < 10000) {
+                x += (i);
+                i = i + 1;
+            }
+            
+		    y = choose(x); // OK
+		    print format("y is {0}", y);
+		    
+            x += (i);
+		    y = choose(x); // error
+		    print format("y is {0}", y);
+		}
+	}
+}
diff --git a/Tst/RegressionTests/Feature3Exprs/StaticError/tooManyChoices/tooManyChoices.p b/Tst/RegressionTests/Feature3Exprs/StaticError/tooManyChoices/tooManyChoices.p
@@ -0,0 +1,14 @@
+machine Main {
+	start state S {
+		entry {
+		    var x: int;
+		    var y: int;
+
+		    x = choose(10000); // OK
+		    print format("x is {0}", x);
+
+		    y = choose(10001); // error
+		    print format("y is {0}", y);
+		}
+	}
+}