From b88079b3580ad8327ce84bdfba92bf711988d15b Mon Sep 17 00:00:00 2001 From: jn1z Date: Fri, 19 Jan 2024 13:01:47 -0500 Subject: [PATCH 1/7] Extract method to update Paige-Tarjan fields. --- .../PaigeTarjanInitializers.java | 30 ++++++++----------- 1 file changed, 12 insertions(+), 18 deletions(-) diff --git a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java index 274629d675..182a1c9123 100644 --- a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java +++ b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java @@ -162,12 +162,7 @@ private static void initCompleteDeterministicPrune(PaigeTarjan pt, } } - pt.setBlockData(data); - pt.setPosData(data, posDataLow); - pt.setPredOfsData(data, predOfsDataLow); - pt.setPredData(data); - pt.setBlockForState(blockForState); - pt.setSize(numStates, numInputs); + updatePTFields(pt, data, posDataLow, predOfsDataLow, blockForState, numStates, numInputs); } private static void initCompleteDeterministicNoPrune(PaigeTarjan pt, @@ -216,6 +211,7 @@ private static void initCompleteDeterministicNoPrune(PaigeTarjan pt, data[posDataLow + i] = pos; int predOfsBase = predOfsDataLow; + for (int j = 0; j < numInputs; j++) { int succ = absAutomaton.getSuccessor(i, j); assert succ >= 0; @@ -225,12 +221,7 @@ private static void initCompleteDeterministicNoPrune(PaigeTarjan pt, } } - pt.setBlockData(data); - pt.setPosData(data, posDataLow); - pt.setPredOfsData(data, predOfsDataLow); - pt.setPredData(data); - pt.setBlockForState(blockForState); - pt.setSize(numStates, numInputs); + updatePTFields(pt, data, posDataLow, predOfsDataLow, blockForState, numStates, numInputs); } public static void prefixSum(int[] array, int startInclusive, int endExclusive) { @@ -364,12 +355,7 @@ public static void initDeterministic(PaigeTarjan pt, } } - pt.setBlockData(data); - pt.setPosData(data, posDataLow); - pt.setPredOfsData(data, predOfsDataLow); - pt.setPredData(data); - pt.setSize(numStatesWithSink, numInputs); - pt.setBlockForState(blockForState); + updatePTFields(pt, data, posDataLow, predOfsDataLow, blockForState, numStatesWithSink, numInputs); pt.removeEmptyBlocks(); } @@ -386,4 +372,12 @@ private static Block getOrCreateSuccBlock( return block; } + private static void updatePTFields(PaigeTarjan pt, int[] data, int posDataLow, int predOfsDataLow, Block[] blockForState, int numStates, int numInputs) { + pt.setBlockData(data); + pt.setPosData(data, posDataLow); + pt.setPredOfsData(data, predOfsDataLow); + pt.setPredData(data); + pt.setBlockForState(blockForState); + pt.setSize(numStates, numInputs); + } } From 47cc150ae727e4df8bce5720af5aef300c68e8fd Mon Sep 17 00:00:00 2001 From: jn1z Date: Fri, 19 Jan 2024 13:10:43 -0500 Subject: [PATCH 2/7] Extract updateBlockAndPosData. --- .../PaigeTarjanInitializers.java | 22 +++++++++---------- 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java index 182a1c9123..9d52fa2ebe 100644 --- a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java +++ b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java @@ -146,10 +146,7 @@ private static void initCompleteDeterministicPrune(PaigeTarjan pt, for (int i = 0; i < reachableStates; i++) { int stateId = statesBuff[i]; - Block b = blockForState[stateId]; - int pos = --b.low; - data[pos] = stateId; - data[posDataLow + stateId] = pos; + updateBlockAndPosData(blockForState, stateId, data, posDataLow); int predOfsBase = predOfsDataLow; @@ -205,10 +202,7 @@ private static void initCompleteDeterministicNoPrune(PaigeTarjan pt, prefixSum(data, predOfsDataLow, predDataLow); for (int i = 0; i < numStates; i++) { - Block b = blockForState[i]; - int pos = --b.low; - data[pos] = i; - data[posDataLow + i] = pos; + updateBlockAndPosData(blockForState, i, data, posDataLow); int predOfsBase = predOfsDataLow; @@ -329,10 +323,7 @@ public static void initDeterministic(PaigeTarjan pt, for (int i = 0; i < reachableStates; i++) { int stateId = statesBuff[i]; - Block b = blockForState[stateId]; - int pos = --b.low; - data[pos] = stateId; - data[posDataLow + stateId] = pos; + updateBlockAndPosData(blockForState, stateId, data, posDataLow); int predOfsBase = predOfsDataLow; @@ -360,6 +351,13 @@ public static void initDeterministic(PaigeTarjan pt, pt.removeEmptyBlocks(); } + private static void updateBlockAndPosData(Block[] blockForState, int i, int[] data, int posDataLow) { + Block b = blockForState[i]; + int pos = --b.low; + data[pos] = i; + data[posDataLow + i] = pos; + } + private static Block getOrCreateSuccBlock( Map<@Nullable Object, Block> blockMap, Object classification, PaigeTarjan pt) { Block block = blockMap.get(classification); From 7155857cde0502b0f61588b7486644f41029da50 Mon Sep 17 00:00:00 2001 From: jn1z Date: Fri, 19 Jan 2024 13:43:03 -0500 Subject: [PATCH 3/7] Add more comments about behavior. --- .../PaigeTarjanInitializers.java | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java index 9d52fa2ebe..802dce377d 100644 --- a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java +++ b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java @@ -205,7 +205,6 @@ private static void initCompleteDeterministicNoPrune(PaigeTarjan pt, updateBlockAndPosData(blockForState, i, data, posDataLow); int predOfsBase = predOfsDataLow; - for (int j = 0; j < numInputs; j++) { int succ = absAutomaton.getSuccessor(i, j); assert succ >= 0; @@ -303,7 +302,7 @@ public static void initDeterministic(PaigeTarjan pt, blockForState[succId] = getOrCreateSuccBlock(blockMap, succClass, pt); statesBuff[reachableStates++] = succId; } - data[predCountBase + succId]++; + data[predCountBase + succId]++; // predOfsData predCountBase += numStatesWithSink; } } @@ -311,16 +310,22 @@ public static void initDeterministic(PaigeTarjan pt, if (partial) { int predCountIdx = predOfsDataLow + sinkId; for (int i = 0; i < numInputs; i++) { - data[predCountIdx]++; + data[predCountIdx]++; // predOfsData - sink state has all its symbols pointing to itself predCountIdx += numStatesWithSink; } } + // data[predOfsDataLow + j*numStatesWithSink+i] now contains the count of transitions to state i from input j + pt.canonizeBlocks(); + // Make predOfsData cumulative data[predOfsDataLow] += predDataLow; prefixSum(data, predOfsDataLow, predDataLow); + // data[predOfsDataLow + j*numStatesWithSink+i] now contains the final predOfsData value, + // plus the count of transitions to state i from input j + for (int i = 0; i < reachableStates; i++) { int stateId = statesBuff[i]; updateBlockAndPosData(blockForState, stateId, data, posDataLow); @@ -341,7 +346,7 @@ public static void initDeterministic(PaigeTarjan pt, } } - data[--data[predOfsBase + succId]] = stateId; + data[--data[predOfsBase + succId]] = stateId; // predOfsData and predData predOfsBase += numStatesWithSink; } } From ff3e730899e665216b21b47fefab7721bbdc5bdb Mon Sep 17 00:00:00 2001 From: jn1z Date: Fri, 19 Jan 2024 13:55:12 -0500 Subject: [PATCH 4/7] Use getOrCreateBlock for init classes. --- .../PaigeTarjanInitializers.java | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) diff --git a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java index 802dce377d..a37b83ca90 100644 --- a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java +++ b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java @@ -107,10 +107,7 @@ private static void initCompleteDeterministicPrune(PaigeTarjan pt, int init = absAutomaton.getIntInitialState(); Object initClass = initialClassification.apply(init); - Block initBlock = pt.createBlock(); - initBlock.high = 1; - blockForState[init] = initBlock; - blockMap.put(initClass, initBlock); + blockForState[init] = getOrCreateBlock(blockMap, initClass, pt); int[] statesBuff = new int[numStates]; statesBuff[0] = init; @@ -131,7 +128,7 @@ private static void initCompleteDeterministicPrune(PaigeTarjan pt, Block succBlock = blockForState[succ]; if (succBlock == null) { Object succClass = initialClassification.apply(succ); - blockForState[succ] = getOrCreateSuccBlock(blockMap, succClass, pt); + blockForState[succ] = getOrCreateBlock(blockMap, succClass, pt); statesBuff[reachableStates++] = succ; } data[predCountBase + succ]++; @@ -181,7 +178,7 @@ private static void initCompleteDeterministicNoPrune(PaigeTarjan pt, for (int i = 0; i < numStates; i++) { Object classification = initialClassification.apply(i); - blockForState[i] = getOrCreateSuccBlock(blockMap, classification, pt); + blockForState[i] = getOrCreateBlock(blockMap, classification, pt); int predCountBase = predOfsDataLow; @@ -261,10 +258,7 @@ public static void initDeterministic(PaigeTarjan pt, Object initClass = initialClassification.apply(initId); - Block initBlock = pt.createBlock(); - initBlock.high = 1; - blockForState[initId] = initBlock; - blockMap.put(initClass, initBlock); + blockForState[initId] = getOrCreateBlock(blockMap, initClass, pt); int[] statesBuff = new int[numStatesWithSink]; statesBuff[0] = initId; @@ -299,7 +293,7 @@ public static void initDeterministic(PaigeTarjan pt, } else { succClass = initialClassification.apply(succ); } - blockForState[succId] = getOrCreateSuccBlock(blockMap, succClass, pt); + blockForState[succId] = getOrCreateBlock(blockMap, succClass, pt); statesBuff[reachableStates++] = succId; } data[predCountBase + succId]++; // predOfsData @@ -363,7 +357,7 @@ private static void updateBlockAndPosData(Block[] blockForState, int i, int[] da data[posDataLow + i] = pos; } - private static Block getOrCreateSuccBlock( + private static Block getOrCreateBlock( Map<@Nullable Object, Block> blockMap, Object classification, PaigeTarjan pt) { Block block = blockMap.get(classification); if (block == null) { From 7abd7b233c54aca1cf89d91d051d55245bd28a0d Mon Sep 17 00:00:00 2001 From: jn1z Date: Mon, 22 Jan 2024 09:45:13 -0500 Subject: [PATCH 5/7] Add more comments. Note post-conditions for b.ptr. Remove unnecessary set of b.ptr. --- .../automatalib/util/partitionrefinement/Block.java | 1 + .../util/partitionrefinement/PaigeTarjan.java | 7 ++++++- .../partitionrefinement/PaigeTarjanInitializers.java | 10 ++++++---- 3 files changed, 13 insertions(+), 5 deletions(-) diff --git a/util/src/main/java/net/automatalib/util/partitionrefinement/Block.java b/util/src/main/java/net/automatalib/util/partitionrefinement/Block.java index 4a0f893127..3467c10dcf 100644 --- a/util/src/main/java/net/automatalib/util/partitionrefinement/Block.java +++ b/util/src/main/java/net/automatalib/util/partitionrefinement/Block.java @@ -104,6 +104,7 @@ public boolean isEmpty() { * reset to {@code -1}. *

* Preconditions: this.ptr != -1. + * Post-conditions: this.ptr = -1. * * @param newId * the ID of the newly created block, if applicable diff --git a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjan.java b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjan.java index fb01bff9d5..304c5cacb4 100644 --- a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjan.java +++ b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjan.java @@ -325,13 +325,18 @@ private void processTouched() { if (splt != null) { addToWorklist(splt); } - b.ptr = -1; b = next; } touchedHead = null; } + /** + * Invoke Block's split, and if it is successful, update PaigeTarjan fields to reflect the new block. + * @param b block to split + * @return smaller split block, or null if split is not successful + * Post-conditions: b.ptr = -1. + */ private @Nullable Block split(Block b) { Block splt = b.split(numBlocks); if (splt == null) { diff --git a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java index a37b83ca90..ee1fcb09d2 100644 --- a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java +++ b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjanInitializers.java @@ -317,8 +317,8 @@ public static void initDeterministic(PaigeTarjan pt, data[predOfsDataLow] += predDataLow; prefixSum(data, predOfsDataLow, predDataLow); - // data[predOfsDataLow + j*numStatesWithSink+i] now contains the final predOfsData value, - // plus the count of transitions to state i from input j + // data[predOfsDataLow + j*numStatesWithSink+i] now contains + // the final predOfsData value plus the count of transitions to state i from input j for (int i = 0; i < reachableStates; i++) { int stateId = statesBuff[i]; @@ -340,7 +340,7 @@ public static void initDeterministic(PaigeTarjan pt, } } - data[--data[predOfsBase + succId]] = stateId; // predOfsData and predData + data[--data[predOfsBase + succId]] = stateId; // decrement predOfsData, set predData predOfsBase += numStatesWithSink; } } @@ -369,7 +369,9 @@ private static Block getOrCreateBlock( return block; } - private static void updatePTFields(PaigeTarjan pt, int[] data, int posDataLow, int predOfsDataLow, Block[] blockForState, int numStates, int numInputs) { + private static void updatePTFields( + PaigeTarjan pt, int[] data, int posDataLow, int predOfsDataLow, + Block[] blockForState, int numStates, int numInputs) { pt.setBlockData(data); pt.setPosData(data, posDataLow); pt.setPredOfsData(data, predOfsDataLow); From 9c541945685d51952230e07323624dd559e366fd Mon Sep 17 00:00:00 2001 From: jn1z Date: Mon, 22 Jan 2024 10:05:17 -0500 Subject: [PATCH 6/7] Fix checkstyle. --- .../net/automatalib/util/partitionrefinement/PaigeTarjan.java | 1 + 1 file changed, 1 insertion(+) diff --git a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjan.java b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjan.java index 304c5cacb4..f791c38345 100644 --- a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjan.java +++ b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjan.java @@ -333,6 +333,7 @@ private void processTouched() { /** * Invoke Block's split, and if it is successful, update PaigeTarjan fields to reflect the new block. + * * @param b block to split * @return smaller split block, or null if split is not successful * Post-conditions: b.ptr = -1. From e2c77113df4c5979753bc40c9c5de19ed19e44f0 Mon Sep 17 00:00:00 2001 From: jn1z Date: Mon, 22 Jan 2024 10:13:42 -0500 Subject: [PATCH 7/7] Extend comment. Set b.ptr directly instead of also incrementing ptr. Since ptr is a local variable, this behavior is unnecessary. --- .../automatalib/util/partitionrefinement/PaigeTarjan.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjan.java b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjan.java index f791c38345..1be358fdef 100644 --- a/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjan.java +++ b/util/src/main/java/net/automatalib/util/partitionrefinement/PaigeTarjan.java @@ -283,7 +283,8 @@ public void computeCoarsestStablePartition() { } /** - * Move the state to the left of its Block ptr. This allows for the grouping of states with similar behavior. + * Move the state to the left of its Block ptr, and advance the ptr. + * This allows for the grouping of states with similar behavior. * * @param state * state to be moved left within its Block. @@ -312,7 +313,7 @@ private void moveLeft(int state) { posData[posIdx] = ptr; posData[posDataLow + other] = inBlockIdx; } - b.ptr = ++ptr; + b.ptr = ptr + 1; } }