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 --- .../au/id/zancanaro/javacheck/state/Command.java | 23 ++++++ .../id/zancanaro/javacheck/state/CommandList.java | 91 ++++++++++++++++++++++ .../javacheck/state/CommandListGenerator.java | 50 ++++++++++++ .../zancanaro/javacheck/state/CommandResult.java | 31 ++++++++ .../id/zancanaro/javacheck/state/CommandValue.java | 47 +++++++++++ .../javacheck/state/GeneratedCommand.java | 52 +++++++++++++ .../au/id/zancanaro/javacheck/statem/Command.java | 23 ------ .../id/zancanaro/javacheck/statem/CommandList.java | 85 -------------------- .../javacheck/statem/CommandListGenerator.java | 50 ------------ .../zancanaro/javacheck/statem/CommandResult.java | 31 -------- .../zancanaro/javacheck/statem/CommandValue.java | 60 -------------- .../javacheck/statem/GeneratedCommand.java | 56 ------------- .../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 --------------------- 18 files changed, 503 insertions(+), 393 deletions(-) create mode 100644 src/main/java/au/id/zancanaro/javacheck/state/Command.java create mode 100644 src/main/java/au/id/zancanaro/javacheck/state/CommandList.java create mode 100644 src/main/java/au/id/zancanaro/javacheck/state/CommandListGenerator.java create mode 100644 src/main/java/au/id/zancanaro/javacheck/state/CommandResult.java create mode 100644 src/main/java/au/id/zancanaro/javacheck/state/CommandValue.java create mode 100644 src/main/java/au/id/zancanaro/javacheck/state/GeneratedCommand.java delete mode 100644 src/main/java/au/id/zancanaro/javacheck/statem/Command.java delete mode 100644 src/main/java/au/id/zancanaro/javacheck/statem/CommandList.java delete mode 100644 src/main/java/au/id/zancanaro/javacheck/statem/CommandListGenerator.java delete mode 100644 src/main/java/au/id/zancanaro/javacheck/statem/CommandResult.java delete mode 100644 src/main/java/au/id/zancanaro/javacheck/statem/CommandValue.java delete mode 100644 src/main/java/au/id/zancanaro/javacheck/statem/GeneratedCommand.java 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 diff --git a/src/main/java/au/id/zancanaro/javacheck/state/Command.java b/src/main/java/au/id/zancanaro/javacheck/state/Command.java new file mode 100644 index 0000000..afa3957 --- /dev/null +++ b/src/main/java/au/id/zancanaro/javacheck/state/Command.java @@ -0,0 +1,23 @@ +package au.id.zancanaro.javacheck.state; + +import au.id.zancanaro.javacheck.Generator; + +public abstract class Command { + public Generator argsGenerator(State state) { + return Generator.pure(null); + } + + public boolean preCondition(State state, Args args) { + return true; + } + + public abstract Result runCommand(Args args); + + public State nextState(State state, Args args, CommandValue result) { + return state; + } + + public boolean postCondition(State oldState, State newState, Args args, Result result) { + return true; + } +} diff --git a/src/main/java/au/id/zancanaro/javacheck/state/CommandList.java b/src/main/java/au/id/zancanaro/javacheck/state/CommandList.java new file mode 100644 index 0000000..0426fd3 --- /dev/null +++ b/src/main/java/au/id/zancanaro/javacheck/state/CommandList.java @@ -0,0 +1,91 @@ +package au.id.zancanaro.javacheck.state; + +import java.util.*; + +public class CommandList { + private final List> commands; + + public CommandList(List> commands) { + this.commands = new ArrayList<>(commands); + } + + public CommandResult run(State initialState) { + Map values = new HashMap<>(); + CommandResult result = CommandResult.success(initialState); + for (GeneratedCommand generated : commands) { + result = runRealCommand(generated, result.getState(), values); + if (result.isFailed()) { + break; + } + } + return result; + } + + private static CommandResult runRealCommand( + GeneratedCommand generated, + State state, + Map values) { + int id = generated.getId(); + Command command = generated.getCommand(); + Args args = generated.getArgs(); + try { + if (!command.preCondition(state, args)) { + return CommandResult.fail(state, new Error("Precondition failed")); + } + Result result = CommandValue.withValues(values, () -> + command.runCommand(args)); + values.put(id, 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); + } catch (Throwable ex) { + return CommandResult.fail(state, ex); + } + } + + private static CommandResult runAbstractCommand( + GeneratedCommand generated, + State state) { + int id = generated.getId(); + Command command = generated.getCommand(); + Args args = generated.getArgs(); + try { + if (!command.preCondition(state, args)) { + return CommandResult.fail(state, new Error("Precondition failed")); + } + state = command.nextState(state, args, new CommandValue<>(id)); + return CommandResult.success(state); + } catch (Throwable ex) { + return CommandResult.fail(state, ex); + } + } + + public boolean isValid() { + CommandResult result = CommandResult.success(null); + for (GeneratedCommand generated : commands) { + result = runAbstractCommand(generated, result.getState()); + if (result.isFailed()) { + break; + } + } + return !result.isFailed(); + } + + @Override + public String toString() { + StringBuilder builder = new StringBuilder(); + Iterator> 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/state/CommandListGenerator.java b/src/main/java/au/id/zancanaro/javacheck/state/CommandListGenerator.java new file mode 100644 index 0000000..4c2c47f --- /dev/null +++ b/src/main/java/au/id/zancanaro/javacheck/state/CommandListGenerator.java @@ -0,0 +1,50 @@ +package au.id.zancanaro.javacheck.state; + +import au.id.zancanaro.javacheck.Generator; +import au.id.zancanaro.javacheck.ShrinkTree; + +import java.util.Random; +import java.util.function.Function; + +import static au.id.zancanaro.javacheck.Generator.pure; +import static au.id.zancanaro.javacheck.Generators.noShrink; + +public class CommandListGenerator implements Generator> { + private final Function>> generateCommand; + + public CommandListGenerator(Function>> generateCommand) { + this.generateCommand = generateCommand; + } + + public Generator> commandGenerator(int id, State state) { + return noShrink(generateCommand.apply(state)) + .flatMap(command -> generateSingleCommand(id, command, state)); + } + + public Generator> generateSingleCommand(int id, Command command, State state) { + return command.argsGenerator(state).flatMap(generatedArgs -> + command.preCondition(state, generatedArgs) ? + pure(new GeneratedCommand<>(id, command, generatedArgs)) : + commandGenerator(id, state)); + } + + public State nextState(int id, GeneratedCommand generatedCommand, State state) { + return generatedCommand.getCommand().nextState(state, generatedCommand.getArgs(), new CommandValue<>(id)); + } + + @Override + public ShrinkTree> generate(Random random, int size) { + int count = random.nextInt(size); + @SuppressWarnings("unchecked") + ShrinkTree>[] commandTrees = (ShrinkTree>[]) new ShrinkTree[count]; + State state = null; + for (int i = 0; i < count; ++i) { + commandTrees[i] = commandGenerator(i, state).generate(random, size); + GeneratedCommand generatedCommand = commandTrees[i].getValue(); + state = nextState(i, generatedCommand, state); + } + return ShrinkTree.combine(commandTrees, ShrinkTree::removeAndPromoteChildren) + .map(list -> new CommandList<>(list)) + .filter(CommandList::isValid); + } +} diff --git a/src/main/java/au/id/zancanaro/javacheck/state/CommandResult.java b/src/main/java/au/id/zancanaro/javacheck/state/CommandResult.java new file mode 100644 index 0000000..12f650d --- /dev/null +++ b/src/main/java/au/id/zancanaro/javacheck/state/CommandResult.java @@ -0,0 +1,31 @@ +package au.id.zancanaro.javacheck.state; + +public class CommandResult { + private final State state; + private final Throwable thrown; + + private CommandResult(State state, Throwable thrown) { + this.state = state; + this.thrown = thrown; + } + + public State getState() { + return state; + } + + public boolean isFailed() { + return thrown != null; + } + + public Throwable getThrown() { + return thrown; + } + + public static CommandResult success(State state) { + return new CommandResult<>(state, null); + } + + public static CommandResult fail(State state, Throwable ex) { + return new CommandResult<>(state, ex); + } +} 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 { + private static Map values = null; + + public static T withValues(Map newValues, Supplier action) { + Map 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/state/GeneratedCommand.java b/src/main/java/au/id/zancanaro/javacheck/state/GeneratedCommand.java new file mode 100644 index 0000000..90d9a47 --- /dev/null +++ b/src/main/java/au/id/zancanaro/javacheck/state/GeneratedCommand.java @@ -0,0 +1,52 @@ +package au.id.zancanaro.javacheck.state; + +public class GeneratedCommand { + private final int id; + private final Command command; + private final Args args; + + public GeneratedCommand(int id, Command command, Args args) { + this.id = id; + this.command = command; + this.args = args; + } + + public int getId() { + return id; + } + + public Command getCommand() { + return command; + } + + public Args getArgs() { + return args; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + + GeneratedCommand that = (GeneratedCommand) o; + + if (args != null ? !args.equals(that.args) : that.args != null) + return false; + if (command != null ? !command.equals(that.command) : that.command != null) + return false; + + return true; + } + + @Override + public int hashCode() { + int result = command != null ? command.hashCode() : 0; + result = 31 * result + (args != null ? args.hashCode() : 0); + return result; + } + + @Override + public String toString() { + return "#{" + id + "} = " + command + " <- " + args; + } +} diff --git a/src/main/java/au/id/zancanaro/javacheck/statem/Command.java b/src/main/java/au/id/zancanaro/javacheck/statem/Command.java deleted file mode 100644 index a741f0a..0000000 --- a/src/main/java/au/id/zancanaro/javacheck/statem/Command.java +++ /dev/null @@ -1,23 +0,0 @@ -package au.id.zancanaro.javacheck.statem; - -import au.id.zancanaro.javacheck.Generator; - -public abstract class Command { - public Generator argsGenerator(State state) { - return Generator.pure(null); - } - - public boolean preCondition(State state, Args args) { - return true; - } - - public abstract Result runCommand(Args args); - - public State nextState(State state, Args args, CommandValue result) { - return state; - } - - public boolean postCondition(State oldState, State newState, Args args, Result result) { - return true; - } -} diff --git a/src/main/java/au/id/zancanaro/javacheck/statem/CommandList.java b/src/main/java/au/id/zancanaro/javacheck/statem/CommandList.java deleted file mode 100644 index 9e8948a..0000000 --- a/src/main/java/au/id/zancanaro/javacheck/statem/CommandList.java +++ /dev/null @@ -1,85 +0,0 @@ -package au.id.zancanaro.javacheck.statem; - -import java.util.ArrayList; -import java.util.HashMap; -import java.util.List; -import java.util.Map; - -public class CommandList { - private final List> commands; - - public CommandList(List> commands) { - this.commands = new ArrayList<>(commands); - } - - public CommandResult run(State initialState) { - Map values = new HashMap<>(); - CommandResult result = CommandResult.success(initialState); - for (GeneratedCommand generated : commands) { - result = runRealCommand(generated, result.getState(), values); - if (result.isFailed()) { - break; - } - } - return result; - } - - private static CommandResult runRealCommand( - GeneratedCommand generated, - State state, - Map values) { - int id = generated.getId(); - Command command = generated.getCommand(); - Args args = generated.getArgs(); - try { - if (!command.preCondition(state, args)) { - return CommandResult.fail(state, new Error("Precondition failed")); - } - Result result = 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)) { - return CommandResult.fail(state, new Error("Postcondition failed")); - } - return CommandResult.success(state); - } catch (Throwable ex) { - return CommandResult.fail(state, ex); - } - } - - private static CommandResult runAbstractCommand( - GeneratedCommand generated, - State state) { - int id = generated.getId(); - Command command = generated.getCommand(); - Args args = generated.getArgs(); - try { - if (!command.preCondition(state, args)) { - return CommandResult.fail(state, new Error("Precondition failed")); - } - state = command.nextState(state, args, new CommandValue.AbstractValue<>(id)); - return CommandResult.success(state); - } catch (Throwable ex) { - return CommandResult.fail(state, ex); - } - } - - public boolean isValid() { - CommandResult result = CommandResult.success(null); - for (GeneratedCommand generated : commands) { - result = runAbstractCommand(generated, result.getState()); - if (result.isFailed()) { - break; - } - } - return !result.isFailed(); - } - - @Override - public String toString() { - return "CommandList{" + - "commands=" + commands + - '}'; - } -} diff --git a/src/main/java/au/id/zancanaro/javacheck/statem/CommandListGenerator.java b/src/main/java/au/id/zancanaro/javacheck/statem/CommandListGenerator.java deleted file mode 100644 index a0df66f..0000000 --- a/src/main/java/au/id/zancanaro/javacheck/statem/CommandListGenerator.java +++ /dev/null @@ -1,50 +0,0 @@ -package au.id.zancanaro.javacheck.statem; - -import au.id.zancanaro.javacheck.Generator; -import au.id.zancanaro.javacheck.ShrinkTree; - -import java.util.Random; -import java.util.function.Function; - -import static au.id.zancanaro.javacheck.Generator.pure; -import static au.id.zancanaro.javacheck.Generators.noShrink; - -public class CommandListGenerator implements Generator> { - private final Function>> generateCommand; - - public CommandListGenerator(Function>> generateCommand) { - this.generateCommand = generateCommand; - } - - public Generator> commandGenerator(int id, State state) { - return noShrink(generateCommand.apply(state)) - .flatMap(command -> generateSingleCommand(id, command, state)); - } - - public Generator> generateSingleCommand(int id, Command command, State state) { - return command.argsGenerator(state).flatMap(generatedArgs -> - command.preCondition(state, generatedArgs) ? - pure(new GeneratedCommand<>(id, command, generatedArgs)) : - commandGenerator(id, state)); - } - - public State nextState(int id, GeneratedCommand generatedCommand, State state) { - return generatedCommand.getCommand().nextState(state, generatedCommand.getArgs(), new CommandValue.AbstractValue<>(id)); - } - - @Override - public ShrinkTree> generate(Random random, int size) { - int count = random.nextInt(size); - @SuppressWarnings("unchecked") - ShrinkTree>[] commandTrees = (ShrinkTree>[]) new ShrinkTree[count]; - State state = null; - for (int i = 0; i < count; ++i) { - commandTrees[i] = commandGenerator(i, state).generate(random, size); - GeneratedCommand generatedCommand = commandTrees[i].getValue(); - state = nextState(i, generatedCommand, state); - } - return ShrinkTree.combine(commandTrees, ShrinkTree::removeAndPromoteChildren) - .map(list -> new CommandList<>(list)) - .filter(CommandList::isValid); - } -} diff --git a/src/main/java/au/id/zancanaro/javacheck/statem/CommandResult.java b/src/main/java/au/id/zancanaro/javacheck/statem/CommandResult.java deleted file mode 100644 index dc5b085..0000000 --- a/src/main/java/au/id/zancanaro/javacheck/statem/CommandResult.java +++ /dev/null @@ -1,31 +0,0 @@ -package au.id.zancanaro.javacheck.statem; - -public class CommandResult { - private final State state; - private final Throwable thrown; - - private CommandResult(State state, Throwable thrown) { - this.state = state; - this.thrown = thrown; - } - - public State getState() { - return state; - } - - public boolean isFailed() { - return thrown != null; - } - - public Throwable getThrown() { - return thrown; - } - - public static CommandResult success(State state) { - return new CommandResult<>(state, null); - } - - public static CommandResult fail(State state, Throwable ex) { - return new CommandResult<>(state, ex); - } -} 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 { - 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 extends CommandValue { - 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 extends CommandValue { - private final Map values; - - public ConcreteValue(int id, Map 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/main/java/au/id/zancanaro/javacheck/statem/GeneratedCommand.java b/src/main/java/au/id/zancanaro/javacheck/statem/GeneratedCommand.java deleted file mode 100644 index 5e576b4..0000000 --- a/src/main/java/au/id/zancanaro/javacheck/statem/GeneratedCommand.java +++ /dev/null @@ -1,56 +0,0 @@ -package au.id.zancanaro.javacheck.statem; - -public class GeneratedCommand { - private final int id; - private final Command command; - private final Args args; - - public GeneratedCommand(int id, Command command, Args args) { - this.id = id; - this.command = command; - this.args = args; - } - - public int getId() { - return id; - } - - public Command getCommand() { - return command; - } - - public Args getArgs() { - return args; - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - - GeneratedCommand that = (GeneratedCommand) o; - - if (args != null ? !args.equals(that.args) : that.args != null) - return false; - if (command != null ? !command.equals(that.command) : that.command != null) - return false; - - return true; - } - - @Override - public int hashCode() { - int result = command != null ? command.hashCode() : 0; - result = 31 * result + (args != null ? args.hashCode() : 0); - return result; - } - - @Override - public String toString() { - return "GeneratedCommand{" + - "id=" + id + - ", command=" + command + - ", args=" + args + - '}'; - } -} 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