summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorCarlo Zancanaro <carlo@zancanaro.id.au>2015-06-05 17:30:46 +1000
committerCarlo Zancanaro <carlo@zancanaro.id.au>2015-06-05 17:30:46 +1000
commit05ec409ce96da92d430c4a8e58b08d46f42d667a (patch)
tree2c3d8925fa9dd86cc265dcfbcb1fe5d8ee97cd0b /src
parent20b1226b4eb10e85497862bd73fe9e9a2f05191d (diff)
More work on the stateful checker; still not perfect, but it's getting better
Diffstat (limited to 'src')
-rw-r--r--src/main/java/au/id/zancanaro/javacheck/state/Command.java (renamed from src/main/java/au/id/zancanaro/javacheck/statem/Command.java)2
-rw-r--r--src/main/java/au/id/zancanaro/javacheck/state/CommandList.java (renamed from src/main/java/au/id/zancanaro/javacheck/statem/CommandList.java)32
-rw-r--r--src/main/java/au/id/zancanaro/javacheck/state/CommandListGenerator.java (renamed from src/main/java/au/id/zancanaro/javacheck/statem/CommandListGenerator.java)4
-rw-r--r--src/main/java/au/id/zancanaro/javacheck/state/CommandResult.java (renamed from src/main/java/au/id/zancanaro/javacheck/statem/CommandResult.java)2
-rw-r--r--src/main/java/au/id/zancanaro/javacheck/state/CommandValue.java47
-rw-r--r--src/main/java/au/id/zancanaro/javacheck/state/GeneratedCommand.java (renamed from src/main/java/au/id/zancanaro/javacheck/statem/GeneratedCommand.java)8
-rw-r--r--src/main/java/au/id/zancanaro/javacheck/statem/CommandValue.java60
-rw-r--r--src/test/java/au/id/zancanaro/javacheck/state/queue/NewQueueCommand.java30
-rw-r--r--src/test/java/au/id/zancanaro/javacheck/state/queue/PopQueueCommand.java58
-rw-r--r--src/test/java/au/id/zancanaro/javacheck/state/queue/PushQueueCommand.java60
-rw-r--r--src/test/java/au/id/zancanaro/javacheck/state/queue/QueueState.java24
-rw-r--r--src/test/java/au/id/zancanaro/javacheck/state/queue/QueueTest.java37
-rw-r--r--src/test/java/au/id/zancanaro/javacheck/statem/QueueTest.java88
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";
- }
- }
-}