From 05ec409ce96da92d430c4a8e58b08d46f42d667a Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Fri, 5 Jun 2015 17:30:46 +1000 Subject: More work on the stateful checker; still not perfect, but it's getting better --- .../javacheck/state/queue/NewQueueCommand.java | 30 +++++++++++ .../javacheck/state/queue/PopQueueCommand.java | 58 +++++++++++++++++++++ .../javacheck/state/queue/PushQueueCommand.java | 60 ++++++++++++++++++++++ .../javacheck/state/queue/QueueState.java | 24 +++++++++ .../zancanaro/javacheck/state/queue/QueueTest.java | 37 +++++++++++++ 5 files changed, 209 insertions(+) create mode 100644 src/test/java/au/id/zancanaro/javacheck/state/queue/NewQueueCommand.java create mode 100644 src/test/java/au/id/zancanaro/javacheck/state/queue/PopQueueCommand.java create mode 100644 src/test/java/au/id/zancanaro/javacheck/state/queue/PushQueueCommand.java create mode 100644 src/test/java/au/id/zancanaro/javacheck/state/queue/QueueState.java create mode 100644 src/test/java/au/id/zancanaro/javacheck/state/queue/QueueTest.java (limited to 'src/test/java/au/id/zancanaro/javacheck/state') 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 extends Command, Void, Queue> { + @Override + public boolean preCondition(QueueState state, Void args) { + return state == null; + } + + @Override + public Queue runCommand(Void args) { + return new LinkedList<>(); + } + + @Override + public QueueState nextState(QueueState state, Void args, CommandValue> 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 extends Command, PopQueueCommand.ArgsType, T> { + @Override + public Generator> argsGenerator(QueueState tQueueState) { + return pure(tQueueState.getConcreteQueue()).map(x -> new ArgsType<>(x)); + } + + @Override + public boolean preCondition(QueueState state, ArgsType args) { + return state != null && !state.getAbstractQueue().isEmpty(); + } + + @Override + public T runCommand(ArgsType args) { + return args.queue.get().poll(); + } + + @Override + public QueueState nextState(QueueState state, ArgsType args, CommandValue result) { + List newState = new ArrayList<>(state.getAbstractQueue()); + newState.remove(0); + return new QueueState<>(state.getConcreteQueue(), newState); + } + + @Override + public boolean postCondition(QueueState oldState, QueueState newState, ArgsType args, T result) { + return oldState.getAbstractQueue().get(0) == result; + } + + @Override + public String toString() { + return "pop"; + } + + static class ArgsType { + public final CommandValue> queue; + + public ArgsType(CommandValue> 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 extends Command, PushQueueCommand.ArgsType, Void> { + public final Generator generator; + + public PushQueueCommand(Generator argGen) { + this.generator = argGen; + } + + @Override + public Generator> argsGenerator(QueueState state) { + return generator.map(i -> new ArgsType<>(state.getConcreteQueue(), i)); + } + + @Override + public Void runCommand(ArgsType args) { + args.queue.get().offer(args.pushValue); + return null; + } + + @Override + public QueueState nextState(QueueState state, ArgsType args, CommandValue result) { + List newState = new ArrayList<>(state.getAbstractQueue()); + newState.add(args.pushValue); + return new QueueState<>(state.getConcreteQueue(), newState); + } + + @Override + public boolean preCondition(QueueState state, ArgsType args) { + return state != null; + } + + @Override + public String toString() { + return "push"; + } + + static class ArgsType { + public final CommandValue> queue; + public final T pushValue; + + public ArgsType(CommandValue> 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 { + private final CommandValue> concreteQueue; + private final List abstractQueue; + + public QueueState(CommandValue> concreteQueue, List abstractQueue) { + this.concreteQueue = concreteQueue; + this.abstractQueue = abstractQueue; + } + + public CommandValue> getConcreteQueue() { + return concreteQueue; + } + + public List 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>> commandGenerator = + new CommandListGenerator<>(state -> + state == null ? + pure(new NewQueueCommand<>()) : + oneOf( + pure(new PopQueueCommand<>()), + pure(new PushQueueCommand<>(integer())) + )); + + @Property + public void test(CommandList> commands) throws Throwable { + CommandResult> result = commands.run(null); + if (result.isFailed()) { + throw result.getThrown(); + } + } +} -- cgit v1.2.3