diff options
author | OszkarSemerath <semerath@mit.bme.hu> | 2023-09-05 20:04:37 +0200 |
---|---|---|
committer | OszkarSemerath <semerath@mit.bme.hu> | 2023-09-05 20:04:37 +0200 |
commit | b65094147cfa2fc46f37916c2f5b52e723a6db34 (patch) | |
tree | e8bd9ac96e9f94c0a9ead4ca654e1f256b06c4e3 /subprojects/store-dse/src/main/java/tools | |
parent | restructured DSE framework, failing build (diff) | |
download | refinery-b65094147cfa2fc46f37916c2f5b52e723a6db34.tar.gz refinery-b65094147cfa2fc46f37916c2f5b52e723a6db34.tar.zst refinery-b65094147cfa2fc46f37916c2f5b52e723a6db34.zip |
fixed numerous issues with activation coder
Diffstat (limited to 'subprojects/store-dse/src/main/java/tools')
3 files changed, 30 insertions, 20 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!"); |