Skip to content

Commit

Permalink
tacas AET
Browse files Browse the repository at this point in the history
  • Loading branch information
breandan committed Oct 25, 2024
1 parent 18dc689 commit 054918c
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 6 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ open class FSA(open val Q: TSA, open val init: Set<Σᐩ>, open val final: Set<
val states by lazy { Q.states }
val stateLst by lazy { states.toList() }
val stateMap by lazy { states.withIndex().associate { it.value to it.index } }
// Index of every state pair of states the FSA to the shortest path distance between them
val APSP: Map<Pair<Int, Int>, Int> by lazy {
graph.APSP.map { (k, v) ->
// println("Hashing: ${k.first.label} -> ${k.second.label} == $v")
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -50,10 +50,11 @@ fun CFG.parikhBounds(nt: Σᐩ, size: Int): ParikhBounds {
return bounds
}

// For a description of this datastructure: https://github.com/breandan/galoisenne/blob/master/latex/popl2025/rebuttal.md
class ParikhMap(val cfg: CFG, val size: Int, reconstruct: Boolean = true) {
private val lengthBounds: MutableMap<Int, Set<Σᐩ>> = mutableMapOf()
private val parikhMap: MutableMap<Int, ParikhBoundsMap> = mutableMapOf()
val parikhRangeMap: MutableMap<IntRange, ParikhBoundsMap> = mutableMapOf()
val parikhRangeMap: MutableMap<IntRange, ParikhBoundsMap> = mutableMapOf() // Parameterized Parikh map
val ntIdx = cfg.nonterminals.toList()

companion object {
Expand Down Expand Up @@ -106,7 +107,7 @@ class ParikhMap(val cfg: CFG, val size: Int, reconstruct: Boolean = true) {
}

fun populatePRMFromPM() {
genRanges().forEach { range ->
genRanges(n = size).forEach { range ->
range.map { parikhMap[it] ?: emptyMap() }
.fold(emptyMap<Σᐩ, ParikhBounds>()) { acc, map -> pbmplus(acc, map) }
.also {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -159,10 +159,11 @@ val MAX_PRODS = 150_000_000

// We pass pm and lbc because cache often flushed forcing them to be reloaded
// and we know they will usually be the same for all calls to this function.
fun CFG.jvmIntersectLevFSAP(fsa: FSA,
parikhMap: ParikhMap = this.parikhMap,
lbc: List<IntRange> = this.lengthBoundsCache
): CFG {
fun CFG.jvmIntersectLevFSAP(
fsa: FSA,
parikhMap: ParikhMap = this.parikhMap,
lbc: List<IntRange> = this.lengthBoundsCache
): CFG {
// if (fsa.Q.size < 650) throw Exception("FSA size was out of bounds")
if (parikhMap.size < fsa.width + fsa.height) throw Exception("WARNING: Parikh map size exceeded")
var clock = TimeSource.Monotonic.markNow()
Expand Down

0 comments on commit 054918c

Please sign in to comment.