diff options
Diffstat (limited to 'subprojects/store-dse/src')
4 files changed, 110 insertions, 41 deletions
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreBitVectorEntry.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreBitVectorEntry.java index ba243d7d..24145d03 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreBitVectorEntry.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreBitVectorEntry.java | |||
@@ -14,7 +14,7 @@ public class ActivationStoreBitVectorEntry extends ActivationStoreEntry { | |||
14 | } | 14 | } |
15 | 15 | ||
16 | @Override | 16 | @Override |
17 | public int getNumberOfUnvisitedActivations() { | 17 | public int getNumberOfVisitedActivations() { |
18 | int visited = 0; | 18 | int visited = 0; |
19 | for (int i : selected) { | 19 | for (int i : selected) { |
20 | visited += Integer.bitCount(i); | 20 | visited += Integer.bitCount(i); |
@@ -29,12 +29,13 @@ public class ActivationStoreBitVectorEntry extends ActivationStoreEntry { | |||
29 | int position = index; | 29 | int position = index; |
30 | do { | 30 | do { |
31 | final int selectedElement = position >> ELEMENT_POSITION; | 31 | final int selectedElement = position >> ELEMENT_POSITION; |
32 | final int selectedBit = position & ELEMENT_BITMASK; | 32 | final int selectedBit = 1<<(position & ELEMENT_BITMASK); |
33 | |||
33 | if((selected[selectedElement] & selectedBit) == 0) { | 34 | if((selected[selectedElement] & selectedBit) == 0) { |
34 | selected[selectedElement] |= selectedBit; | 35 | selected[selectedElement] |= selectedBit; |
35 | return position; | 36 | return position; |
36 | } else { | 37 | } else { |
37 | if(position < this.numberOfActivations) { | 38 | if(position < this.numberOfActivations-1) { |
38 | position++; | 39 | position++; |
39 | } else { | 40 | } else { |
40 | position = 0; | 41 | position = 0; |
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreEntry.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreEntry.java index f69b234c..d7339805 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreEntry.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreEntry.java | |||
@@ -12,11 +12,11 @@ public abstract class ActivationStoreEntry { | |||
12 | this.numberOfActivations = numberOfActivations; | 12 | this.numberOfActivations = numberOfActivations; |
13 | } | 13 | } |
14 | 14 | ||
15 | public int getNumberOfVisitedActivations() { | 15 | public abstract int getNumberOfVisitedActivations(); |
16 | return numberOfActivations; | ||
17 | } | ||
18 | 16 | ||
19 | public abstract int getNumberOfUnvisitedActivations(); | 17 | public int getNumberOfUnvisitedActivations() { |
18 | return numberOfActivations - getNumberOfVisitedActivations(); | ||
19 | } | ||
20 | public abstract int getAndAddActivationAfter(int index); | 20 | public abstract int getAndAddActivationAfter(int index); |
21 | 21 | ||
22 | // public abstract boolean contains(int activation) | 22 | // public abstract boolean contains(int activation) |
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreListEntry.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreListEntry.java index 9e25301f..3d4cbfdc 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreListEntry.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreListEntry.java | |||
@@ -16,8 +16,8 @@ public class ActivationStoreListEntry extends ActivationStoreEntry { | |||
16 | } | 16 | } |
17 | 17 | ||
18 | @Override | 18 | @Override |
19 | public int getNumberOfUnvisitedActivations() { | 19 | public int getNumberOfVisitedActivations() { |
20 | return this.numberOfActivations - visitedActivations.size(); | 20 | return visitedActivations.size(); |
21 | } | 21 | } |
22 | 22 | ||
23 | @Override | 23 | @Override |
@@ -27,43 +27,52 @@ public class ActivationStoreListEntry extends ActivationStoreEntry { | |||
27 | this.visitedActivations.add(index); | 27 | this.visitedActivations.add(index); |
28 | return index; | 28 | return index; |
29 | } | 29 | } |
30 | final int positionInSearch = getPosition(index); | ||
31 | int position = positionInSearch; | ||
30 | 32 | ||
31 | int position = getPosition(index); | 33 | // if the position is after the last, we can insert it at the end of the list |
34 | if(position == this.visitedActivations.size()) { | ||
35 | this.visitedActivations.add(index); | ||
36 | return index; | ||
37 | } else if(this.visitedActivations.get(position) != index) { | ||
38 | // If the index is not in the position, one can insert it | ||
32 | 39 | ||
33 | // If the index is not in the position, one can insert it | ||
34 | if(this.visitedActivations.get(position) != index) { | ||
35 | this.visitedActivations.addAtIndex(position,index); | 40 | this.visitedActivations.addAtIndex(position,index); |
36 | return index; | 41 | return index; |
37 | } | 42 | } |
38 | 43 | ||
39 | // Otherwise, get the next empty space between two elements | 44 | // Otherwise, get the next empty space between two elements |
40 | while(position + 2 < this.visitedActivations.size()) { | 45 | while(position + 1 < this.visitedActivations.size()) { |
41 | position++; | ||
42 | if(this.visitedActivations.get(position+1)-this.visitedActivations.get(position) > 1) { | 46 | if(this.visitedActivations.get(position+1)-this.visitedActivations.get(position) > 1) { |
43 | this.visitedActivations.addAtIndex(position+1, this.visitedActivations.get(position+1)+1); | 47 | int newElement = this.visitedActivations.get(position)+1; |
48 | this.visitedActivations.addAtIndex(position+1, newElement); | ||
49 | return newElement; | ||
44 | } | 50 | } |
51 | position++; | ||
45 | } | 52 | } |
46 | 53 | ||
47 | // Otherwise, try to add to the last space | 54 | // Otherwise, try to add to the last space |
48 | int last = this.visitedActivations.get(this.visitedActivations.size()-1); | 55 | int last = this.visitedActivations.get(this.visitedActivations.size()-1); |
49 | if(last<this.numberOfActivations) { | 56 | if(last<this.numberOfActivations-1) { |
50 | this.visitedActivations.add(last+1); | 57 | this.visitedActivations.add(last+1); |
51 | return last+1; | 58 | return last+1; |
52 | } | 59 | } |
53 | 60 | ||
54 | // Otherwise, try to put to the beginning | 61 | // Otherwise, try to put to the beginning |
55 | if(this.visitedActivations.get(0) > 0) { | 62 | if(this.visitedActivations.get(0) > 0) { |
56 | this.visitedActivations.add(0); | 63 | this.visitedActivations.addAtIndex(0,0); |
57 | return 0; | 64 | return 0; |
58 | } | 65 | } |
59 | 66 | ||
60 | // Otherwise, get the next empty space between two elements | 67 | // Otherwise, get the next empty space between two elements |
61 | position = 0; | 68 | position = 0; |
62 | while(position + 2 < this.visitedActivations.size()) { | 69 | while(position < positionInSearch) { |
63 | position++; | ||
64 | if(this.visitedActivations.get(position+1)-this.visitedActivations.get(position) > 1) { | 70 | if(this.visitedActivations.get(position+1)-this.visitedActivations.get(position) > 1) { |
65 | this.visitedActivations.addAtIndex(position+1, this.visitedActivations.get(position+1)+1); | 71 | int newElement = this.visitedActivations.get(position)+1; |
72 | this.visitedActivations.addAtIndex(position+1, newElement); | ||
73 | return newElement; | ||
66 | } | 74 | } |
75 | position++; | ||
67 | } | 76 | } |
68 | 77 | ||
69 | throw new IllegalArgumentException("There is are no unvisited activations!"); | 78 | throw new IllegalArgumentException("There is are no unvisited activations!"); |
diff --git a/subprojects/store-dse/src/test/java/tools/refinery/store/dse/transition/statespace/internal/ActivationUnitTest.java b/subprojects/store-dse/src/test/java/tools/refinery/store/dse/transition/statespace/internal/ActivationUnitTest.java index e7960a06..3a672b18 100644 --- a/subprojects/store-dse/src/test/java/tools/refinery/store/dse/transition/statespace/internal/ActivationUnitTest.java +++ b/subprojects/store-dse/src/test/java/tools/refinery/store/dse/transition/statespace/internal/ActivationUnitTest.java | |||
@@ -9,6 +9,11 @@ import org.junit.jupiter.api.Assertions; | |||
9 | import org.junit.jupiter.params.ParameterizedTest; | 9 | import org.junit.jupiter.params.ParameterizedTest; |
10 | import org.junit.jupiter.params.provider.MethodSource; | 10 | import org.junit.jupiter.params.provider.MethodSource; |
11 | 11 | ||
12 | import java.util.ArrayList; | ||
13 | import java.util.Collections; | ||
14 | import java.util.List; | ||
15 | import java.util.Random; | ||
16 | import java.util.function.Supplier; | ||
12 | import java.util.stream.Stream; | 17 | import java.util.stream.Stream; |
13 | 18 | ||
14 | class ActivationUnitTest { | 19 | class ActivationUnitTest { |
@@ -17,56 +22,110 @@ class ActivationUnitTest { | |||
17 | private static Stream<ActivationStoreEntry> entries() { | 22 | private static Stream<ActivationStoreEntry> entries() { |
18 | return Stream.of( | 23 | return Stream.of( |
19 | new ActivationStoreBitVectorEntry(SMALL_SIZE), | 24 | new ActivationStoreBitVectorEntry(SMALL_SIZE), |
20 | new ActivationStoreListEntry(SMALL_SIZE)); | 25 | new ActivationStoreListEntry(SMALL_SIZE) |
26 | ); | ||
21 | } | 27 | } |
22 | 28 | ||
23 | void addTest(ActivationStoreEntry entry, int elementsAdded) { | 29 | void addTest(ActivationStoreEntry entry, int elementsAdded) { |
24 | Assertions.assertEquals(elementsAdded,entry.getNumberOfVisitedActivations()); | 30 | Assertions.assertEquals(elementsAdded, entry.getNumberOfVisitedActivations()); |
25 | Assertions.assertEquals(SMALL_SIZE-elementsAdded,entry.getNumberOfUnvisitedActivations()); | 31 | Assertions.assertEquals(SMALL_SIZE - elementsAdded, entry.getNumberOfUnvisitedActivations()); |
26 | } | 32 | } |
27 | 33 | ||
28 | @ParameterizedTest | 34 | @ParameterizedTest |
29 | @MethodSource("entries") | 35 | @MethodSource("entries") |
30 | void testDifferent(ActivationStoreEntry entry) { | 36 | void testDifferent(ActivationStoreEntry entry) { |
31 | int elementsAdded = 0; | 37 | int elementsAdded = 0; |
32 | addTest(entry,elementsAdded); | 38 | addTest(entry, elementsAdded); |
33 | Assertions.assertEquals(2, entry.getAndAddActivationAfter(2)); | 39 | Assertions.assertEquals(2, entry.getAndAddActivationAfter(2)); |
34 | addTest(entry,++elementsAdded); | 40 | addTest(entry, ++elementsAdded); |
35 | Assertions.assertEquals(3,entry.getAndAddActivationAfter(3)); | 41 | Assertions.assertEquals(3, entry.getAndAddActivationAfter(3)); |
36 | addTest(entry,++elementsAdded); | 42 | addTest(entry, ++elementsAdded); |
37 | Assertions.assertEquals(1,entry.getAndAddActivationAfter(1)); | 43 | Assertions.assertEquals(1, entry.getAndAddActivationAfter(1)); |
38 | addTest(entry,++elementsAdded); | 44 | addTest(entry, ++elementsAdded); |
39 | Assertions.assertEquals(4,entry.getAndAddActivationAfter(4)); | 45 | Assertions.assertEquals(4, entry.getAndAddActivationAfter(4)); |
40 | addTest(entry,++elementsAdded); | 46 | addTest(entry, ++elementsAdded); |
41 | Assertions.assertEquals(0,entry.getAndAddActivationAfter(0)); | 47 | Assertions.assertEquals(0, entry.getAndAddActivationAfter(0)); |
42 | addTest(entry,++elementsAdded); | 48 | addTest(entry, ++elementsAdded); |
43 | } | 49 | } |
44 | 50 | ||
51 | |||
45 | @ParameterizedTest | 52 | @ParameterizedTest |
46 | @MethodSource("entries") | 53 | @MethodSource("entries") |
47 | void testSame(ActivationStoreEntry entry) { | 54 | void testSame(ActivationStoreEntry entry) { |
48 | int elementsAdded = 0; | 55 | int elementsAdded = 0; |
49 | addTest(entry,elementsAdded); | 56 | addTest(entry, 0); |
50 | entry.getAndAddActivationAfter(2); | 57 | entry.getAndAddActivationAfter(2); |
51 | addTest(entry,++elementsAdded); | 58 | addTest(entry, ++elementsAdded); |
52 | entry.getAndAddActivationAfter(2); | 59 | entry.getAndAddActivationAfter(2); |
53 | addTest(entry,++elementsAdded); | 60 | addTest(entry, ++elementsAdded); |
54 | entry.getAndAddActivationAfter(2); | 61 | entry.getAndAddActivationAfter(2); |
55 | addTest(entry,++elementsAdded); | 62 | addTest(entry, ++elementsAdded); |
56 | entry.getAndAddActivationAfter(2); | 63 | entry.getAndAddActivationAfter(2); |
57 | addTest(entry,++elementsAdded); | 64 | addTest(entry, ++elementsAdded); |
58 | entry.getAndAddActivationAfter(2); | 65 | entry.getAndAddActivationAfter(2); |
59 | addTest(entry,++elementsAdded); | 66 | addTest(entry, ++elementsAdded); |
60 | } | 67 | } |
61 | 68 | ||
62 | @ParameterizedTest | 69 | @ParameterizedTest |
63 | @MethodSource("entries") | 70 | @MethodSource("entries") |
64 | void testFilling(ActivationStoreEntry entry) { | 71 | void testFilling(ActivationStoreEntry entry) { |
65 | int elementsAdded = 0; | 72 | int elementsAdded = 0; |
66 | while(elementsAdded < SMALL_SIZE) { | 73 | while (elementsAdded < SMALL_SIZE) { |
67 | entry.getAndAddActivationAfter(2); | 74 | entry.getAndAddActivationAfter(2); |
68 | elementsAdded++; | 75 | elementsAdded++; |
69 | } | 76 | } |
70 | Assertions.assertThrows(IllegalArgumentException.class,()-> entry.getAndAddActivationAfter(2)); | 77 | Assertions.assertThrows(IllegalArgumentException.class, () -> entry.getAndAddActivationAfter(2)); |
78 | } | ||
79 | |||
80 | void randomDifferentTestCase(ActivationStoreEntry entry, int seed) { | ||
81 | List<Integer> elements = new ArrayList<>(SMALL_SIZE); | ||
82 | for (int i = 0; i < SMALL_SIZE; i++) { | ||
83 | elements.add(i); | ||
84 | } | ||
85 | @SuppressWarnings("squid:S2245") | ||
86 | var random = new Random(seed); | ||
87 | Collections.shuffle(elements, random); | ||
88 | |||
89 | for (int element : elements) { | ||
90 | entry.getAndAddActivationAfter(element); | ||
91 | } | ||
92 | Assertions.assertThrows(IllegalArgumentException.class, () -> entry.getAndAddActivationAfter(2)); | ||
93 | } | ||
94 | |||
95 | private static final int fuzzNumber = 20; | ||
96 | |||
97 | @ParameterizedTest | ||
98 | @MethodSource("entryFactories") | ||
99 | void randomDifferentTest(Supplier<ActivationStoreEntry> entry) { | ||
100 | for (int i = 0; i < fuzzNumber; i++) { | ||
101 | randomDifferentTestCase(entry.get(), i); | ||
102 | } | ||
103 | } | ||
104 | |||
105 | void randomSameTestCase(ActivationStoreEntry entry, int seed) { | ||
106 | |||
107 | @SuppressWarnings("squid:S2245") | ||
108 | var random = new Random(seed); | ||
109 | |||
110 | for (int i = 0; i < SMALL_SIZE; i++) { | ||
111 | entry.getAndAddActivationAfter(random.nextInt(SMALL_SIZE)); | ||
112 | } | ||
113 | |||
114 | Assertions.assertThrows(IllegalArgumentException.class, () -> entry.getAndAddActivationAfter(2)); | ||
115 | } | ||
116 | |||
117 | @ParameterizedTest | ||
118 | @MethodSource("entryFactories") | ||
119 | void randomSameTest(Supplier<ActivationStoreEntry> entry) { | ||
120 | for (int i = 0; i < fuzzNumber; i++) { | ||
121 | randomSameTestCase(entry.get(), i); | ||
122 | } | ||
123 | } | ||
124 | |||
125 | private static Stream<Supplier<ActivationStoreEntry>> entryFactories() { | ||
126 | return Stream.of( | ||
127 | () -> new ActivationStoreBitVectorEntry(SMALL_SIZE), | ||
128 | () -> new ActivationStoreListEntry(SMALL_SIZE) | ||
129 | ); | ||
71 | } | 130 | } |
72 | } | 131 | } |