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 +++++++++ .../id/zancanaro/javacheck/statem/QueueTest.java | 88 ---------------------- 6 files changed, 209 insertions(+), 88 deletions(-) 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 delete mode 100644 src/test/java/au/id/zancanaro/javacheck/statem/QueueTest.java (limited to 'src/test/java') 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(); + } + } +} diff --git a/src/test/java/au/id/zancanaro/javacheck/statem/QueueTest.java b/src/test/java/au/id/zancanaro/javacheck/statem/QueueTest.java deleted file mode 100644 index 4cd6345..0000000 --- a/src/test/java/au/id/zancanaro/javacheck/statem/QueueTest.java +++ /dev/null @@ -1,88 +0,0 @@ -package au.id.zancanaro.javacheck.statem; - -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.junit.Properties; -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; -import static org.junit.Assert.assertTrue; - -@RunWith(Properties.class) -public class QueueTest { - private static final Queue queue = new LinkedList<>(); - - @DataSource - public static Generator>> commandGenerator = - new CommandListGenerator<>(state -> oneOf( - pure(new QueuePushCommand()), - pure(new QueuePopCommand()) - )); - - @Property - public void test(CommandList> commands) { - queue.clear(); - CommandResult> result = commands.run(null); - assertFalse(result.isFailed()); - } - - private static class QueuePushCommand extends Command, Integer, Void> { - @Override - public Generator argsGenerator(List integers) { - return integer(); - } - - @Override - public Void runCommand(Integer integer) { - queue.offer(integer); - return null; - } - - @Override - public List nextState(List integers, Integer integer, CommandValue result) { - List nextState = new ArrayList<>(integers == null ? new ArrayList<>() : integers); - nextState.add(integer); - return nextState; - } - - @Override - public String toString() { - return "push"; - } - } - - private static class QueuePopCommand extends Command, Void, Integer> { - @Override - public boolean preCondition(List integers, Void aVoid) { - return integers != null && !integers.isEmpty(); - } - - @Override - public Integer runCommand(Void aVoid) { - return queue.poll(); - } - - @Override - public boolean postCondition(List oldState, List newState, Void aVoid, Integer integer) { - return Objects.equals(integer, oldState.get(0)); - } - - @Override - public List nextState(List integers, Void aVoid, CommandValue result) { - List nextState = new ArrayList<>(integers == null ? new ArrayList<>() : integers); - nextState.remove(0); - return nextState; - } - - @Override - public String toString() { - return "pop"; - } - } -} -- cgit v1.2.3