diff options
author | Carlo Zancanaro <carlo@zancanaro.id.au> | 2015-06-05 17:30:46 +1000 |
---|---|---|
committer | Carlo Zancanaro <carlo@zancanaro.id.au> | 2015-06-05 17:30:46 +1000 |
commit | 05ec409ce96da92d430c4a8e58b08d46f42d667a (patch) | |
tree | 2c3d8925fa9dd86cc265dcfbcb1fe5d8ee97cd0b | |
parent | 20b1226b4eb10e85497862bd73fe9e9a2f05191d (diff) |
More work on the stateful checker; still not perfect, but it's getting better
13 files changed, 281 insertions, 171 deletions
diff --git a/src/main/java/au/id/zancanaro/javacheck/statem/Command.java b/src/main/java/au/id/zancanaro/javacheck/state/Command.java index a741f0a..afa3957 100644 --- a/src/main/java/au/id/zancanaro/javacheck/statem/Command.java +++ b/src/main/java/au/id/zancanaro/javacheck/state/Command.java @@ -1,4 +1,4 @@ -package au.id.zancanaro.javacheck.statem; +package au.id.zancanaro.javacheck.state; import au.id.zancanaro.javacheck.Generator; diff --git a/src/main/java/au/id/zancanaro/javacheck/statem/CommandList.java b/src/main/java/au/id/zancanaro/javacheck/state/CommandList.java index 9e8948a..0426fd3 100644 --- a/src/main/java/au/id/zancanaro/javacheck/statem/CommandList.java +++ b/src/main/java/au/id/zancanaro/javacheck/state/CommandList.java @@ -1,9 +1,6 @@ -package au.id.zancanaro.javacheck.statem; +package au.id.zancanaro.javacheck.state; -import java.util.ArrayList; -import java.util.HashMap; -import java.util.List; -import java.util.Map; +import java.util.*; public class CommandList<State> { private final List<GeneratedCommand<State, ?, ?>> commands; @@ -35,11 +32,14 @@ public class CommandList<State> { if (!command.preCondition(state, args)) { return CommandResult.fail(state, new Error("Precondition failed")); } - Result result = command.runCommand(args); + Result result = CommandValue.withValues(values, () -> + command.runCommand(args)); values.put(id, result); - State oldState = state; - state = command.nextState(state, args, new CommandValue.ConcreteValue<>(id, values)); - if (!command.postCondition(oldState, state, args, result)) { + final State oldState = state; + final State newState = CommandValue.withValues(values, () -> + command.nextState(oldState, args, new CommandValue<>(id))); + state = newState; + if (!CommandValue.withValues(values, () -> command.postCondition(oldState, newState, args, result))) { return CommandResult.fail(state, new Error("Postcondition failed")); } return CommandResult.success(state); @@ -58,7 +58,7 @@ public class CommandList<State> { if (!command.preCondition(state, args)) { return CommandResult.fail(state, new Error("Precondition failed")); } - state = command.nextState(state, args, new CommandValue.AbstractValue<>(id)); + state = command.nextState(state, args, new CommandValue<>(id)); return CommandResult.success(state); } catch (Throwable ex) { return CommandResult.fail(state, ex); @@ -78,8 +78,14 @@ public class CommandList<State> { @Override public String toString() { - return "CommandList{" + - "commands=" + commands + - '}'; + StringBuilder builder = new StringBuilder(); + Iterator<GeneratedCommand<State, ?, ?>> iterator = commands.iterator(); + while (iterator.hasNext()) { + builder.append(iterator.next()); + if (iterator.hasNext()) { + builder.append(", "); + } + } + return builder.toString(); } } diff --git a/src/main/java/au/id/zancanaro/javacheck/statem/CommandListGenerator.java b/src/main/java/au/id/zancanaro/javacheck/state/CommandListGenerator.java index a0df66f..4c2c47f 100644 --- a/src/main/java/au/id/zancanaro/javacheck/statem/CommandListGenerator.java +++ b/src/main/java/au/id/zancanaro/javacheck/state/CommandListGenerator.java @@ -1,4 +1,4 @@ -package au.id.zancanaro.javacheck.statem; +package au.id.zancanaro.javacheck.state; import au.id.zancanaro.javacheck.Generator; import au.id.zancanaro.javacheck.ShrinkTree; @@ -29,7 +29,7 @@ public class CommandListGenerator<State> implements Generator<CommandList<State> } public <Args, Result> State nextState(int id, GeneratedCommand<State, Args, Result> generatedCommand, State state) { - return generatedCommand.getCommand().nextState(state, generatedCommand.getArgs(), new CommandValue.AbstractValue<>(id)); + return generatedCommand.getCommand().nextState(state, generatedCommand.getArgs(), new CommandValue<>(id)); } @Override diff --git a/src/main/java/au/id/zancanaro/javacheck/statem/CommandResult.java b/src/main/java/au/id/zancanaro/javacheck/state/CommandResult.java index dc5b085..12f650d 100644 --- a/src/main/java/au/id/zancanaro/javacheck/statem/CommandResult.java +++ b/src/main/java/au/id/zancanaro/javacheck/state/CommandResult.java @@ -1,4 +1,4 @@ -package au.id.zancanaro.javacheck.statem; +package au.id.zancanaro.javacheck.state; public class CommandResult<State> { private final State state; diff --git a/src/main/java/au/id/zancanaro/javacheck/state/CommandValue.java b/src/main/java/au/id/zancanaro/javacheck/state/CommandValue.java new file mode 100644 index 0000000..8d3f272 --- /dev/null +++ b/src/main/java/au/id/zancanaro/javacheck/state/CommandValue.java @@ -0,0 +1,47 @@ +package au.id.zancanaro.javacheck.state; + +import java.util.Map; +import java.util.NoSuchElementException; +import java.util.function.Supplier; + +public class CommandValue<T> { + private static Map<Integer, Object> values = null; + + public static <T> T withValues(Map<Integer, Object> newValues, Supplier<T> action) { + Map<Integer,Object> oldValues = values; + try { + values = newValues; + return action.get(); + } finally { + values = oldValues; + } + } + + private final int id; + + public CommandValue(int id) { + this.id = id; + } + + public boolean isAbstract() { + return values == null; + } + + @SuppressWarnings("unchecked") + public T get() { + if (values.containsKey(getId())) { + return (T) values.get(getId()); + } else { + throw new NoSuchElementException("Concrete values cannot be supplied prior to being calculated"); + } + } + + public int getId() { + return id; + } + + @Override + public String toString() { + return "#{" + id + "}"; + } +} diff --git a/src/main/java/au/id/zancanaro/javacheck/statem/GeneratedCommand.java b/src/main/java/au/id/zancanaro/javacheck/state/GeneratedCommand.java index 5e576b4..90d9a47 100644 --- a/src/main/java/au/id/zancanaro/javacheck/statem/GeneratedCommand.java +++ b/src/main/java/au/id/zancanaro/javacheck/state/GeneratedCommand.java @@ -1,4 +1,4 @@ -package au.id.zancanaro.javacheck.statem; +package au.id.zancanaro.javacheck.state; public class GeneratedCommand<State, Args, Result> { private final int id; @@ -47,10 +47,6 @@ public class GeneratedCommand<State, Args, Result> { @Override public String toString() { - return "GeneratedCommand{" + - "id=" + id + - ", command=" + command + - ", args=" + args + - '}'; + return "#{" + id + "} = " + command + " <- " + args; } } diff --git a/src/main/java/au/id/zancanaro/javacheck/statem/CommandValue.java b/src/main/java/au/id/zancanaro/javacheck/statem/CommandValue.java deleted file mode 100644 index 0a1fb61..0000000 --- a/src/main/java/au/id/zancanaro/javacheck/statem/CommandValue.java +++ /dev/null @@ -1,60 +0,0 @@ -package au.id.zancanaro.javacheck.statem; - -import java.util.Map; -import java.util.NoSuchElementException; - -public abstract class CommandValue<T> { - private final int id; - - public CommandValue(int id) { - this.id = id; - } - - public abstract boolean isAbstract(); - - public abstract T get(); - - public int getId() { - return id; - } - - static class AbstractValue<T> extends CommandValue<T> { - public AbstractValue(int id) { - super(id); - } - - @Override - public boolean isAbstract() { - return true; - } - - @Override - public T get() { - throw new NoSuchElementException("Abstract values cannot be supplied"); - } - } - - static class ConcreteValue<T> extends CommandValue<T> { - private final Map<Integer, Object> values; - - public ConcreteValue(int id, Map<Integer, Object> values) { - super(id); - this.values = values; - } - - @Override - public boolean isAbstract() { - return true; - } - - @Override - @SuppressWarnings("unchecked") - public T get() { - if (values.containsKey(getId())) { - return (T) values.get(getId()); - } else { - throw new NoSuchElementException("Concrete values cannot be supplied prior to being calculated"); - } - } - } -} 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(); + } + } +} 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<Integer> queue = new LinkedList<>(); - - @DataSource - public static Generator<CommandList<List<Integer>>> commandGenerator = - new CommandListGenerator<>(state -> oneOf( - pure(new QueuePushCommand()), - pure(new QueuePopCommand()) - )); - - @Property - public void test(CommandList<List<Integer>> commands) { - queue.clear(); - CommandResult<List<Integer>> result = commands.run(null); - assertFalse(result.isFailed()); - } - - private static class QueuePushCommand extends Command<List<Integer>, Integer, Void> { - @Override - public Generator<Integer> argsGenerator(List<Integer> integers) { - return integer(); - } - - @Override - public Void runCommand(Integer integer) { - queue.offer(integer); - return null; - } - - @Override - public List<Integer> nextState(List<Integer> integers, Integer integer, CommandValue<Void> result) { - List<Integer> 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<List<Integer>, Void, Integer> { - @Override - public boolean preCondition(List<Integer> integers, Void aVoid) { - return integers != null && !integers.isEmpty(); - } - - @Override - public Integer runCommand(Void aVoid) { - return queue.poll(); - } - - @Override - public boolean postCondition(List<Integer> oldState, List<Integer> newState, Void aVoid, Integer integer) { - return Objects.equals(integer, oldState.get(0)); - } - - @Override - public List<Integer> nextState(List<Integer> integers, Void aVoid, CommandValue<Integer> result) { - List<Integer> nextState = new ArrayList<>(integers == null ? new ArrayList<>() : integers); - nextState.remove(0); - return nextState; - } - - @Override - public String toString() { - return "pop"; - } - } -} |