quicktheories · jrwest · Feb 12, 2019
diff --git a/core/src/main/java/org/quicktheories/QuickTheory.java b/core/src/main/java/org/quicktheories/QuickTheory.java
@@ -16,14 +16,16 @@
 import org.quicktheories.dsl.TheoryBuilder2;
 import org.quicktheories.dsl.TheoryBuilder3;
 import org.quicktheories.dsl.TheoryBuilder4;
+import org.quicktheories.impl.stateful.StatefulCore;
+import org.quicktheories.impl.stateful.StatefulTheory;
 
 /**
  * Entry point for property based testing.
  */
 @CheckReturnValue
 public class QuickTheory {
 
-  private final Supplier<Strategy> state;
+  protected final Supplier<Strategy> state;
 
   private QuickTheory(Supplier<Strategy> state) {
     this.state = state;
@@ -137,6 +139,26 @@ public QuickTheory withShrinkCycles(int shrinks) {
     return new QuickTheory(() -> state.get().withShrinkCycles(shrinks));
   }
 
+  /**
+   * Sets the minimum of number of steps to be generated when running a stateful model
+   *
+   * @param minStatefulSteps minimum number of steps to generate
+   * @return a QuickTheory using the new minimum number of steps
+   */
+  public QuickTheory withMinStatefulSteps(int minStatefulSteps) {
+    return new QuickTheory(() -> state.get().withMinStatefulSteps(minStatefulSteps));
+  }
+
+  /**
+   * Sets the maximum of number of steps to be generated when running a stateful model
+   *
+   * @param maxStatefulSteps maximum number of steps to generate
+   * @return a QuickTheory using the new maximum number of steps
+   */
+  public QuickTheory withMaxStatefulSteps(int maxStatefulSteps) {
+    return new QuickTheory(() -> state.get().withMaxStatefulSteps(maxStatefulSteps));
+  }
+
   /**
    * Sets the number of generate attempts to use
    * @param generateAttempts number of generate attempts
@@ -259,6 +281,55 @@ public <A, B, C, D> TheoryBuilder4<A, B, C, D> forAll(
       final Gen<D> ds) {
     return new TheoryBuilder4<>(state, as, bs, cs, ds, (a, b, c, d) -> true);
   }
-
+
+  /**
+   * Set the stateful model used to generate examples. The model is only used if
+   * {@link StatefulTheoryBuilder#checkStateful()} is called instead of forAll.
+   *
+   * Stateful models customize QuickTheory properties with the following:
+   * <ul>
+   *   <li>Raises generate attempts to account for cases where there are a small number of steps, which can accidentally
+   *   exhaust the generator
+   *   <li>Turn off shrinking because the current shrinker is not effective at shrinking stateful models for a variety
+   *   of reasons
+   * </ul>
+   * These properties can be overridden just as they would with any QuickTheory property.
+   *
+   * @param theory A supplier of the stateful model used to generate examples
+   * @see #stateful(Supplier)
+   * @see StatefulTheoryBuilder#checkStateful()
+   * @return A {@link StatefulTheoryBuilder} that can continue to be used to configure QuickTheories
+   * or run the model
+   */
+  public StatefulTheoryBuilder withStatefulModel(final Supplier<StatefulTheory<?>> theory) {
+    return new StatefulTheoryBuilder(() -> state.get().withShrinkCycles(0).withGenerateAttempts(100), theory);
+  }
+
+  /**
+   * Set the stateful model used to generate examples. The model is run immediately as if
+   * {@code withStatefulModel(...).checkStateful()} were called. This is useful when no further customization to QuickTheory
+   * properties is needed.
+   *
+   * @param theory A supplier of the stateful model used to generate examples
+   * @see #withStatefulModel(Supplier)
+   * @see StatefulTheoryBuilder#checkStateful()
+   */
+  public void stateful(final Supplier<StatefulTheory<?>> theory) {
+    withStatefulModel(theory).checkStateful();
+  }
+
+  public static class StatefulTheoryBuilder extends QuickTheory {
+
+    private final Supplier<StatefulTheory<?>> statefulTheory;
+    private StatefulTheoryBuilder(Supplier<Strategy> state, Supplier<StatefulTheory<?>> statefulTheory) {
+      super(state);
+      this.statefulTheory = statefulTheory;
+    }
+
+    public void checkStateful() {
+      new TheoryBuilder<>(state, StatefulCore.generator(statefulTheory)).check(sm -> sm.run(state));
+    }
+
+  }
 
 }
diff --git a/core/src/main/java/org/quicktheories/core/Configuration.java b/core/src/main/java/org/quicktheories/core/Configuration.java
@@ -14,6 +14,8 @@ public abstract class Configuration {
   private static final int DEFAULT_NO_ATTEMPTS = 10;
   private static final int DEFAULT_NO_EXAMPLES = 1000;
   private static final int DEFAULT_TESTING_TIME_MILLIS = -1;
+  private static final int DEFAULT_MIN_STATEFUL_STEPS = 1;
+  private static final int DEFAULT_MAX_STATEFUL_STEPS = 100;
 
   public final static String PROFILE = "QT_PROFILE";
   public final static String SEED = "QT_SEED";
@@ -55,8 +57,8 @@ public static Strategy defaultStrategy(Class<?> testClass) {
    * @return a Strategy
    */
   public static Strategy systemStrategy() {
-    return new Strategy(defaultPRNG(pickSeed()), pickExamples(), pickTestingTimeMillis(), pickShrinks(), pickAttempts(),
-        new ExceptionReporter(), pickGuidance());
+    return new Strategy(defaultPRNG(pickSeed()), pickExamples(), pickTestingTimeMillis(), pickShrinks(),
+            DEFAULT_MIN_STATEFUL_STEPS, DEFAULT_MAX_STATEFUL_STEPS, pickAttempts(), new ExceptionReporter(), pickGuidance());
   }
 
   private static int pickAttempts() {

diff --git a/core/src/main/java/org/quicktheories/core/Strategy.java b/core/src/main/java/org/quicktheories/core/Strategy.java
@@ -14,6 +14,8 @@ public class Strategy {
   private final int examples;
   private final long testingTimeMillis;
   private final int shrinkCycles;
+  private final int minStatefulSteps;
+  private final int maxStatefulSteps;
   private final Reporter reporter;
   private final Function<PseudoRandom, Guidance> guidance;
 
@@ -38,11 +40,14 @@ public class Strategy {
    *          Strategy to use to guide search
    */
   public Strategy(final PseudoRandom prng, final int examples, final long testingTimeMillis,
-      final int shrinkCycles, final int generateAttempts, Reporter reporter, Function<PseudoRandom, Guidance> guidance) {
+                  final int shrinkCycles,  final int minStatefulSteps, final int maxStatefulSteps, final int generateAttempts,
+                  Reporter reporter, Function<PseudoRandom, Guidance> guidance) {
     this.prng = prng;
     this.examples = examples;
     this.testingTimeMillis = testingTimeMillis;
     this.shrinkCycles = shrinkCycles;
+    this.minStatefulSteps = minStatefulSteps;
+    this.maxStatefulSteps = maxStatefulSteps;
     this.reporter = reporter;
     this.generateAttempts = generateAttempts;
     this.guidance = guidance;
@@ -78,7 +83,25 @@ public PseudoRandom prng() {
   public int shrinkCycles() {
     return this.shrinkCycles;
   }
-
+
+  /**
+   * Returns the minimum number of steps that will be generated in a run of a stateful model
+   *
+   * @return the minimum number of steps that will be generated in a run of a stateful model
+   */
+  public int minStatefulSteps() {
+    return this.minStatefulSteps;
+  }
+
+  /**
+   * Returns the maximum number of steps that will be generated in a run of a stateful model
+   *
+   * @return the maximum number of steps that will be generated in a run of a stateful model
+   */
+  public int maxStatefulSteps() {
+    return this.maxStatefulSteps;
+  }
+
   /**
    * Returns the maximum number of times to try to retrieve each value before giving up.
    * 
@@ -110,8 +133,8 @@ public Guidance guidance() {
    *         supplied
    */
   public Strategy withFixedSeed(long seed) {
-    return new Strategy(defaultPRNG(seed), examples, testingTimeMillis, shrinkCycles, generateAttempts,
-        reporter, guidance);
+    return new Strategy(defaultPRNG(seed), examples, testingTimeMillis, shrinkCycles, minStatefulSteps, maxStatefulSteps,
+            generateAttempts, reporter, guidance);
   }
 
   /**
@@ -123,7 +146,8 @@ public Strategy withFixedSeed(long seed) {
    * @return a strategy with the maximum number of examples as supplied
    */
   public Strategy withExamples(int examples) {
-    return new Strategy(prng, examples, testingTimeMillis, shrinkCycles, generateAttempts, reporter, guidance);
+    return new Strategy(prng, examples, testingTimeMillis, shrinkCycles, minStatefulSteps, maxStatefulSteps,
+            generateAttempts, reporter, guidance);
   }
 
   /**
@@ -145,7 +169,8 @@ public Strategy withUnlimitedExamples() {
    * @return a strategy with the testing time set to the amount of time given.
    */
   public Strategy withTestingTime(long time, TimeUnit timeUnit) {
-    return new Strategy(prng, examples, timeUnit.toMillis(time), shrinkCycles, generateAttempts, reporter, guidance);
+    return new Strategy(prng, examples, timeUnit.toMillis(time), shrinkCycles, minStatefulSteps, maxStatefulSteps,
+            generateAttempts, reporter, guidance);
   }
 
   /**
@@ -164,7 +189,8 @@ public Strategy withUnlimitedTestingTime() {
    * @return a strategy
    */
   public Strategy withGenerateAttempts(int generateAttempts) {
-    return new Strategy(prng, examples, testingTimeMillis, shrinkCycles, generateAttempts, reporter, guidance);
+    return new Strategy(prng, examples, testingTimeMillis, shrinkCycles, minStatefulSteps, maxStatefulSteps,
+            generateAttempts, reporter, guidance);
   }
 
   /**
@@ -173,7 +199,8 @@ public Strategy withGenerateAttempts(int generateAttempts) {
    * @return a strategy
    */
   public Strategy withGuidance(Function<PseudoRandom, Guidance> guidance) {
-    return new Strategy(prng, examples, testingTimeMillis, shrinkCycles, generateAttempts, reporter, guidance);
+    return new Strategy(prng, examples, testingTimeMillis, shrinkCycles, minStatefulSteps, maxStatefulSteps,
+            generateAttempts, reporter, guidance);
   }
 
   /**
@@ -184,16 +211,30 @@ public Strategy withGuidance(Function<PseudoRandom, Guidance> guidance) {
    * @return a strategy with the maximum number of shrinks as supplied
    */
   public Strategy withShrinkCycles(int shrinks) {
-    return new Strategy(prng, examples, testingTimeMillis, shrinks, generateAttempts, reporter, guidance);
+    return new Strategy(prng, examples, testingTimeMillis, shrinks, minStatefulSteps, maxStatefulSteps,
+            generateAttempts, reporter, guidance);
   }
-
+
+  public Strategy withMinStatefulSteps(int minStatefulSteps)
+  {
+    return new Strategy(prng, examples, testingTimeMillis, shrinkCycles, minStatefulSteps, maxStatefulSteps,
+            generateAttempts, reporter, guidance);
+  }
+
+  public Strategy withMaxStatefulSteps(int maxStatefulSteps)
+  {
+    return new Strategy(prng, examples, testingTimeMillis, shrinkCycles, minStatefulSteps, maxStatefulSteps,
+            generateAttempts, reporter, guidance);
+  }
+
   /**
    * Creates a strategy using the supplied reporter
    * @param reporter Reporter to use
    * @return a strategy with suppled reporter
    */
   public Strategy withReporter(Reporter reporter) {
-    return new Strategy(prng, examples, testingTimeMillis, shrinkCycles, generateAttempts, reporter, guidance);
+    return new Strategy(prng, examples, testingTimeMillis, shrinkCycles, minStatefulSteps, maxStatefulSteps,
+            generateAttempts, reporter, guidance);
   }
 
   /**

diff --git a/core/src/main/java/org/quicktheories/impl/stateful/StatefulCore.java b/core/src/main/java/org/quicktheories/impl/stateful/StatefulCore.java
@@ -0,0 +1,59 @@
+package org.quicktheories.impl.stateful;
+
+import org.quicktheories.core.Gen;
+import org.quicktheories.core.RandomnessSource;
+import org.quicktheories.core.Strategy;
+import org.quicktheories.generators.Generate;
+import org.quicktheories.impl.Constraint;
+
+import java.util.Iterator;
+import java.util.function.Supplier;
+
+/**
+ * Drives a {@link StatefulTheory}
+ */
+public class StatefulCore<T> {
+
+    private final RandomnessSource prng;
+    private final StatefulTheory<T> theory;
+
+    public static Gen<StatefulCore> generator(Supplier<StatefulTheory<?>> theory) {
+        Gen<StatefulCore> gen = prng -> {
+            // swallow a random value so that hashes of each StatefulCore differ
+            // (hashes are based on the prng not the value)
+            prng.next(Constraint.none());
+            return new StatefulCore<>(prng, theory.get());
+        };
+        return gen.describedAs(c -> c.theory.formattedHistory());
+    }
+
+
+    private StatefulCore(RandomnessSource prng, StatefulTheory<T> theory) {
+        this.prng = prng;
+        this.theory = theory;
+    }
+
+    public boolean run(Supplier<Strategy> state) {
+        theory.init();
+        Iterator<Gen<T>> setupSteps = theory.setupSteps();
+        while (setupSteps.hasNext()) {
+            theory.executeStep(setupSteps.next().generate(prng));
+        }
+
+        Strategy strategy = state.get();
+        int numSteps = Generate.longRange(strategy.minStatefulSteps(), strategy.maxStatefulSteps(), strategy.minStatefulSteps())
+                               .map(Long::intValue)
+                               .generate(prng);
+        try {
+            for (int i = 0; i < numSteps; i++) {
+                if (!theory.executeStep(theory.steps().generate(prng))) {
+                    return false;
+                }
+            }
+        } finally {
+            theory.teardown();
+        }
+
+        return true;
+    }
+}