1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
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";
}
}
}
|
