More work on the stateful checker; still not perfect, but it's getting better

5 files changed, 209 insertions, 0 deletions

diff --git a/src/test/java/au/id/zancanaro/javacheck/state/queue/NewQueueCommand.java b/src/test/java/au/id/zancanaro/javacheck/state/queue/NewQueueCommand.java
new file mode 100644
index 0000000..d2815dc
--- /dev/null
+++ b/src/test/java/au/id/zancanaro/javacheck/state/queue/NewQueueCommand.java
@@ -0,0 +1,30 @@
+package au.id.zancanaro.javacheck.state.queue;
+
+import au.id.zancanaro.javacheck.state.Command;
+import au.id.zancanaro.javacheck.state.CommandValue;
+
+import java.util.ArrayList;
+import java.util.LinkedList;
+import java.util.Queue;
+
+public class NewQueueCommand<T> extends Command<QueueState<T>, Void, Queue<T>> {
+    @Override
+    public boolean preCondition(QueueState<T> state, Void args) {
+        return state == null;
+    }
+
+    @Override
+    public Queue<T> runCommand(Void args) {
+        return new LinkedList<>();
+    }
+
+    @Override
+    public QueueState<T> nextState(QueueState<T> state, Void args, CommandValue<Queue<T>> result) {
+        return new QueueState<>(result, new ArrayList<>());
+    }
+
+    @Override
+    public String toString() {
+        return "new";
+    }
+}
diff --git a/src/test/java/au/id/zancanaro/javacheck/state/queue/PopQueueCommand.java b/src/test/java/au/id/zancanaro/javacheck/state/queue/PopQueueCommand.java
new file mode 100644
index 0000000..f8a018c
--- /dev/null
+++ b/src/test/java/au/id/zancanaro/javacheck/state/queue/PopQueueCommand.java
@@ -0,0 +1,58 @@
+package au.id.zancanaro.javacheck.state.queue;
+
+import au.id.zancanaro.javacheck.Generator;
+import au.id.zancanaro.javacheck.state.Command;
+import au.id.zancanaro.javacheck.state.CommandValue;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Queue;
+
+import static au.id.zancanaro.javacheck.Generator.pure;
+
+public class PopQueueCommand<T> extends Command<QueueState<T>, PopQueueCommand.ArgsType<T>, T> {
+    @Override
+    public Generator<ArgsType<T>> argsGenerator(QueueState<T> tQueueState) {
+        return pure(tQueueState.getConcreteQueue()).map(x -> new ArgsType<>(x));
+    }
+
+    @Override
+    public boolean preCondition(QueueState<T> state, ArgsType<T> args) {
+        return state != null && !state.getAbstractQueue().isEmpty();
+    }
+
+    @Override
+    public T runCommand(ArgsType<T> args) {
+        return args.queue.get().poll();
+    }
+
+    @Override
+    public QueueState<T> nextState(QueueState<T> state, ArgsType<T> args, CommandValue<T> result) {
+        List<T> newState = new ArrayList<>(state.getAbstractQueue());
+        newState.remove(0);
+        return new QueueState<>(state.getConcreteQueue(), newState);
+    }
+
+    @Override
+    public boolean postCondition(QueueState<T> oldState, QueueState<T> newState, ArgsType<T> args, T result) {
+        return oldState.getAbstractQueue().get(0) == result;
+    }
+
+    @Override
+    public String toString() {
+        return "pop";
+    }
+
+    static class ArgsType<T> {
+        public final CommandValue<Queue<T>> queue;
+
+        public ArgsType(CommandValue<Queue<T>> queue) {
+            this.queue = queue;
+        }
+
+        @Override
+        public String toString() {
+            return "[" + queue + "]";
+        }
+    }
+}
diff --git a/src/test/java/au/id/zancanaro/javacheck/state/queue/PushQueueCommand.java b/src/test/java/au/id/zancanaro/javacheck/state/queue/PushQueueCommand.java
new file mode 100644
index 0000000..b198eb5
--- /dev/null
+++ b/src/test/java/au/id/zancanaro/javacheck/state/queue/PushQueueCommand.java
@@ -0,0 +1,60 @@
+package au.id.zancanaro.javacheck.state.queue;
+
+import au.id.zancanaro.javacheck.Generator;
+import au.id.zancanaro.javacheck.state.Command;
+import au.id.zancanaro.javacheck.state.CommandValue;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Queue;
+
+public class PushQueueCommand<T> extends Command<QueueState<T>, PushQueueCommand.ArgsType<T>, Void> {
+    public final Generator<T> generator;
+
+    public PushQueueCommand(Generator<T> argGen) {
+        this.generator = argGen;
+    }
+
+    @Override
+    public Generator<ArgsType<T>> argsGenerator(QueueState<T> state) {
+        return generator.map(i -> new ArgsType<>(state.getConcreteQueue(), i));
+    }
+
+    @Override
+    public Void runCommand(ArgsType<T> args) {
+        args.queue.get().offer(args.pushValue);
+        return null;
+    }
+
+    @Override
+    public QueueState<T> nextState(QueueState<T> state, ArgsType<T> args, CommandValue<Void> result) {
+        List<T> newState = new ArrayList<>(state.getAbstractQueue());
+        newState.add(args.pushValue);
+        return new QueueState<>(state.getConcreteQueue(), newState);
+    }
+
+    @Override
+    public boolean preCondition(QueueState<T> state, ArgsType<T> args) {
+        return state != null;
+    }
+
+    @Override
+    public String toString() {
+        return "push";
+    }
+
+    static class ArgsType<T> {
+        public final CommandValue<Queue<T>> queue;
+        public final T pushValue;
+
+        public ArgsType(CommandValue<Queue<T>> queue, T pushValue) {
+            this.queue = queue;
+            this.pushValue = pushValue;
+        }
+
+        @Override
+        public String toString() {
+            return "[" + queue + ", " + pushValue + "]";
+        }
+    }
+}
diff --git a/src/test/java/au/id/zancanaro/javacheck/state/queue/QueueState.java b/src/test/java/au/id/zancanaro/javacheck/state/queue/QueueState.java
new file mode 100644
index 0000000..e4f65f8
--- /dev/null
+++ b/src/test/java/au/id/zancanaro/javacheck/state/queue/QueueState.java
@@ -0,0 +1,24 @@
+package au.id.zancanaro.javacheck.state.queue;
+
+import au.id.zancanaro.javacheck.state.CommandValue;
+
+import java.util.List;
+import java.util.Queue;
+
+public class QueueState<T> {
+    private final CommandValue<Queue<T>> concreteQueue;
+    private final List<T> abstractQueue;
+
+    public QueueState(CommandValue<Queue<T>> concreteQueue, List<T> abstractQueue) {
+        this.concreteQueue = concreteQueue;
+        this.abstractQueue = abstractQueue;
+    }
+
+    public CommandValue<Queue<T>> getConcreteQueue() {
+        return concreteQueue;
+    }
+
+    public List<T> getAbstractQueue() {
+        return abstractQueue;
+    }
+}
diff --git a/src/test/java/au/id/zancanaro/javacheck/state/queue/QueueTest.java b/src/test/java/au/id/zancanaro/javacheck/state/queue/QueueTest.java
new file mode 100644
index 0000000..083a8ad
--- /dev/null
+++ b/src/test/java/au/id/zancanaro/javacheck/state/queue/QueueTest.java
@@ -0,0 +1,37 @@
+package au.id.zancanaro.javacheck.state.queue;
+
+import au.id.zancanaro.javacheck.Generator;
+import au.id.zancanaro.javacheck.annotations.DataSource;
+import au.id.zancanaro.javacheck.annotations.Property;
+import au.id.zancanaro.javacheck.annotations.Seed;
+import au.id.zancanaro.javacheck.junit.Properties;
+import au.id.zancanaro.javacheck.state.*;
+import org.junit.runner.RunWith;
+
+import java.util.*;
+
+import static au.id.zancanaro.javacheck.Generator.pure;
+import static au.id.zancanaro.javacheck.Generators.integer;
+import static au.id.zancanaro.javacheck.Generators.oneOf;
+import static org.junit.Assert.assertFalse;
+
+@RunWith(Properties.class)
+public class QueueTest {
+    @DataSource
+    public static Generator<CommandList<QueueState<Integer>>> commandGenerator =
+            new CommandListGenerator<>(state ->
+                    state == null ?
+                            pure(new NewQueueCommand<>()) :
+                            oneOf(
+                                    pure(new PopQueueCommand<>()),
+                                    pure(new PushQueueCommand<>(integer()))
+                            ));
+
+    @Property
+    public void test(CommandList<QueueState<Integer>> commands) throws Throwable {
+        CommandResult<QueueState<Integer>> result = commands.run(null);
+        if (result.isFailed()) {
+            throw result.getThrown();
+        }
+    }
+}