Apply patch #212 to fix RandomSearch where one path is explored even with limit > 1 (#401)

Co-authored-by: varad64 <[email protected]>

Author: varad64

src/main/gov/nasa/jpf/search/RandomSearch.java

@@ -29,7 +29,8 @@
  * going forward() until there is no next state then it restarts the search 
  * until it hits a certain number of paths executed
  *
- * <2do> this needs to be updated & tested
+ * To explore different paths, cg.randomize_choices shouldn't be set to NONE
+ *
  */
 public class RandomSearch extends Search {
   int path_limit = 0;
@@ -55,7 +56,7 @@ public void search () {
 
     notifySearchStarted();
     while (!done) {
-      if ((depth < depthLimit) && forward()) {
+      if (!isEndState() && (depth < depthLimit) && forward()) {
         notifyStateAdvanced();
 
         if (currentError != null){
@@ -65,13 +66,7 @@ public void search () {
             return;
           }
         }
-
-        if (isEndState()){
-          return;
-        }
-
         depth++;
-
       } else { // no next state or reached depth limit
         // <2do> we could check for more things here. If the last insn wasn't
         // the main return, or a System.exit() call, we could flag a JPFException

src/tests/gov/nasa/jpf/test/mc/basic/StatelessTest.java

@@ -47,4 +47,21 @@ public void testNumberOfPaths(){
       assert Verify.getCounter(0) == 6;
     }
   }
+
+
+  @Test public void testStatelessRandomSearch () {
+    if (!isJPFRun()){
+      Verify.resetCounter(0);
+    }
+    if (verifyNoPropertyViolation("+search.class=.search.RandomSearch", "+search.RandomSearch.path_limit = 10", "+cg.randomize_choices = FIXED_SEED")){
+      int d = 0;
+      Verify.incrementCounter(0);
+    }
+    if (!isJPFRun()){
+      if (Verify.getCounter(0) != 11){ // path variable will be incremented to limit + 1
+        fail("wrong number of paths");
+      }
+    }
+  }
+
 }