Add loopchecker package

This new package makes it possible to find lasso-like traces in any type
of model.

subprojects/common/analysis/build.gradle.kts

@@ -31,4 +31,8 @@ dependencies {
     testImplementation(project(":theta-solver-z3-legacy"))
     testImplementation(project(":theta-solver-z3"))
     implementation("com.corundumstudio.socketio:netty-socketio:2.0.6")
+    testImplementation(project(mapOf("path" to ":theta-xsts-analysis")))
+    testImplementation(project(mapOf("path" to ":theta-xsts")))
+    testImplementation(project(mapOf("path" to ":theta-cfa-analysis")))
+    testImplementation(project(mapOf("path" to ":theta-cfa")))
 }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/AcceptancePredicate.kt

@@ -0,0 +1,42 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.algorithm.loopchecker
+
+import hu.bme.mit.theta.analysis.Action
+import hu.bme.mit.theta.analysis.State
+import java.util.function.Predicate
+
+class AcceptancePredicate<S : State, A : Action>(
+  private val statePredicate: ((S?) -> Boolean)? = null,
+  private val actionPredicate: ((A?) -> Boolean)? = null,
+) : Predicate<Pair<S?, A?>> {
+
+  constructor(statePredicate: (S?) -> Boolean = { _ -> true }, a: Unit) : this(statePredicate)
+
+  fun testState(state: S): Boolean {
+    return statePredicate?.invoke(state) ?: false
+  }
+
+  fun testAction(action: A) = actionPredicate?.invoke(action) ?: false
+
+  override fun test(t: Pair<S?, A?>): Boolean {
+    val state = t.first
+    val action = t.second
+    if (statePredicate == null && action == null) return false
+    return (statePredicate == null || statePredicate.invoke(state)) &&
+      (actionPredicate == null || (action != null && actionPredicate.invoke(action)))
+  }
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt

@@ -0,0 +1,81 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.algorithm.loopchecker
+
+import hu.bme.mit.theta.analysis.Cex
+import hu.bme.mit.theta.analysis.Trace
+import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge
+import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode
+import hu.bme.mit.theta.analysis.expr.ExprAction
+import hu.bme.mit.theta.analysis.expr.ExprState
+import hu.bme.mit.theta.common.logging.Logger
+import hu.bme.mit.theta.common.logging.Logger.Level
+
+class LDGTrace<S : ExprState, A : ExprAction>(
+  val tail: List<LDGEdge<S, A>>,
+  val honda: LDGNode<S, A>,
+  val loop: List<LDGEdge<S, A>>,
+) : Cex {
+
+  val edges by lazy { tail + loop }
+
+  constructor(
+    edges: List<LDGEdge<S, A>>,
+    honda: LDGNode<S, A>,
+  ) : this(edges.takeWhile { it.source != honda }, honda, edges.dropWhile { it.source != honda })
+
+  init {
+    check((1 until tail.size).none { tail[it - 1].target != tail[it].source }) {
+      "The edges of the tail have to connect into each other"
+    }
+    check(tail.isEmpty() || tail.last().target == honda) { "The tail has to finish in the honda" }
+    check(loop.first().source == honda) { "The loop has to start in the honda" }
+    check((1 until loop.size).none { loop[it - 1].target != loop[it].source }) {
+      "The edges of the loop have to connect into each other"
+    }
+    check(loop.last().target == honda) { "The loop has to finish in the honda" }
+  }
+
+  override fun length() = edges.size
+
+  fun getEdge(index: Int): LDGEdge<S, A> {
+    check(index >= 0) { "Can't get negative indexed edge (${index})" }
+    check(index < length()) { "Index out of range $index < ${length()}" }
+    return if (index < tail.size) tail[index] else loop[index - tail.size]
+  }
+
+  fun getAction(index: Int) = getEdge(index).action
+
+  fun getState(index: Int) = if (index < length()) getEdge(index).source!!.state else honda.state
+
+  fun toTrace(): Trace<S, A> =
+    Trace.of(edges.map { it.source!!.state } + honda.state, edges.map { it.action!! })
+
+  fun print(logger: Logger, level: Level) {
+    tail.forEach {
+      logger.write(
+        level,
+        "%s%n---through action:---%n%s%n--------->%n",
+        it.source?.state,
+        it.action,
+      )
+    }
+    logger.write(level, "---HONDA:---%n{ %s }---------%n", honda.state)
+    loop.forEach {
+      logger.write(level, "---through action:---%n%s%n--------->%n%s%n", it.action, it.target.state)
+    }
+  }
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt

@@ -0,0 +1,156 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction
+
+import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate
+import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace
+import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge
+import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode
+import hu.bme.mit.theta.analysis.expr.ExprAction
+import hu.bme.mit.theta.analysis.expr.ExprState
+import hu.bme.mit.theta.common.logging.Logger
+
+typealias BacktrackResult<S, A> = Pair<Set<LDGNode<S, A>>?, List<LDGTrace<S, A>>?>
+
+fun <S : ExprState, A : ExprAction> combineLassos(results: Collection<BacktrackResult<S, A>>) =
+  Pair(setOf<LDGNode<S, A>>(), results.flatMap { it.second ?: emptyList() })
+
+abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy {
+
+  internal fun <S : ExprState, A : ExprAction> expandFromInitNodeUntilTarget(
+    initNode: LDGNode<S, A>,
+    stopAtLasso: Boolean,
+    expand: NodeExpander<S, A>,
+    logger: Logger,
+  ): Collection<LDGTrace<S, A>> {
+    return expandThroughNode(
+        emptyMap(),
+        LDGEdge(null, initNode, null, false),
+        emptyList(),
+        0,
+        stopAtLasso,
+        expand,
+        logger,
+      )
+      .second!!
+  }
+
+  private fun <S : ExprState, A : ExprAction> expandThroughNode(
+    pathSoFar: Map<LDGNode<S, A>, Int>,
+    incomingEdge: LDGEdge<S, A>,
+    edgesSoFar: List<LDGEdge<S, A>>,
+    targetsSoFar: Int,
+    stopAtLasso: Boolean,
+    expand: NodeExpander<S, A>,
+    logger: Logger,
+  ): BacktrackResult<S, A> {
+    val expandingNode: LDGNode<S, A> = incomingEdge.target
+    logger.write(
+      Logger.Level.VERBOSE,
+      "Expanding through %s edge to %s node with state %s%n",
+      if (incomingEdge.accepting) "accepting" else "not accepting",
+      if (expandingNode.accepting) "accepting" else "not accepting",
+      expandingNode.state,
+    )
+    if (expandingNode.state.isBottom()) {
+      logger.write(Logger.Level.VERBOSE, "Node is a dead end since its bottom%n")
+      return BacktrackResult(null, null)
+    }
+    val totalTargets =
+      if (expandingNode.accepting || incomingEdge.accepting) targetsSoFar + 1 else targetsSoFar
+    if (pathSoFar.containsKey(expandingNode) && pathSoFar[expandingNode]!! < totalTargets) {
+      logger.write(
+        Logger.Level.SUBSTEP,
+        "Found trace with a length of %d, building lasso...%n",
+        pathSoFar.size,
+      )
+      logger.write(Logger.Level.DETAIL, "Honda should be: %s", expandingNode.state)
+      pathSoFar.forEach { (node, targetsThatFar) ->
+        logger.write(
+          Logger.Level.VERBOSE,
+          "Node state %s | targets that far: %d%n",
+          node.state,
+          targetsThatFar,
+        )
+      }
+      val lasso: LDGTrace<S, A> = LDGTrace(edgesSoFar + incomingEdge, expandingNode)
+      logger.write(Logger.Level.DETAIL, "Built the following lasso:%n")
+      lasso.print(logger, Logger.Level.DETAIL)
+      return BacktrackResult(null, listOf(lasso))
+    }
+    if (pathSoFar.containsKey(expandingNode)) {
+      logger.write(Logger.Level.VERBOSE, "Reached loop but no acceptance inside%n")
+      return BacktrackResult(setOf(expandingNode), null)
+    }
+    val needsTraversing =
+      !expandingNode.expanded ||
+        expandingNode.validLoopHondas.filter(pathSoFar::containsKey).any {
+          pathSoFar[it]!! < targetsSoFar
+        }
+    val expandStrategy: NodeExpander<S, A> =
+      if (needsTraversing) expand else { _ -> mutableSetOf() }
+    val outgoingEdges: Collection<LDGEdge<S, A>> = expandStrategy(expandingNode)
+    val results: MutableList<BacktrackResult<S, A>> = mutableListOf()
+    for (newEdge in outgoingEdges) {
+      val result: BacktrackResult<S, A> =
+        expandThroughNode(
+          pathSoFar + (expandingNode to totalTargets),
+          newEdge,
+          if (incomingEdge.source != null) edgesSoFar.plus(incomingEdge) else edgesSoFar,
+          totalTargets,
+          stopAtLasso,
+          expand,
+          logger,
+        )
+      results.add(result)
+      if (stopAtLasso && result.second?.isNotEmpty() == true) break
+    }
+    val result: BacktrackResult<S, A> = combineLassos(results)
+    if (result.second != null) return result
+    val validLoopHondas: Collection<LDGNode<S, A>> = results.flatMap { it.first ?: emptyList() }
+    expandingNode.validLoopHondas.addAll(validLoopHondas)
+    return BacktrackResult(validLoopHondas.toSet(), null)
+  }
+}
+
+object GdfsSearchStrategy : AbstractSearchStrategy() {
+
+  override fun <S : ExprState, A : ExprAction> search(
+    initNodes: Collection<LDGNode<S, A>>,
+    target: AcceptancePredicate<S, A>,
+    expand: NodeExpander<S, A>,
+    logger: Logger,
+  ): Collection<LDGTrace<S, A>> {
+    for (initNode in initNodes) {
+      val possibleTraces: Collection<LDGTrace<S, A>> =
+        expandFromInitNodeUntilTarget(initNode, true, expand, logger)
+      if (!possibleTraces.isEmpty()) {
+        return possibleTraces
+      }
+    }
+    return emptyList()
+  }
+}
+
+object FullSearchStrategy : AbstractSearchStrategy() {
+
+  override fun <S : ExprState, A : ExprAction> search(
+    initNodes: Collection<LDGNode<S, A>>,
+    target: AcceptancePredicate<S, A>,
+    expand: NodeExpander<S, A>,
+    logger: Logger,
+  ) = initNodes.flatMap { expandFromInitNodeUntilTarget(it, false, expand, logger) }
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt

@@ -0,0 +1,62 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction
+
+import hu.bme.mit.theta.analysis.Analysis
+import hu.bme.mit.theta.analysis.LTS
+import hu.bme.mit.theta.analysis.Prec
+import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor
+import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult
+import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate
+import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG
+import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge
+import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode
+import hu.bme.mit.theta.analysis.expr.ExprAction
+import hu.bme.mit.theta.analysis.expr.ExprState
+import hu.bme.mit.theta.common.logging.Logger
+
+class LDGAbstractor<S : ExprState, A : ExprAction, P : Prec>(
+  private val analysis: Analysis<S, in A, in P>,
+  private val lts: LTS<in S, A>,
+  private val acceptancePredicate: AcceptancePredicate<S, A>,
+  private val searchStrategy: LoopcheckerSearchStrategy,
+  private val logger: Logger,
+) : Abstractor<P, LDG<S, A>> {
+
+  override fun createProof() = LDG(acceptancePredicate)
+
+  override fun check(ldg: LDG<S, A>, prec: P): AbstractorResult {
+    if (ldg.isUninitialised()) {
+      ldg.initialise(analysis.initFunc.getInitStates(prec))
+      ldg.traces = emptyList()
+    }
+    val expander: NodeExpander<S, A> =
+      fun(node: LDGNode<S, A>): Collection<LDGEdge<S, A>> {
+        if (node.expanded) {
+          return node.outEdges
+        }
+        node.expanded = true
+        return lts.getEnabledActionsFor(node.state).flatMap { action ->
+          analysis.transFunc.getSuccStates(node.state, action, prec).map(ldg::getOrCreateNode).map {
+            ldg.drawEdge(node, it, action, acceptancePredicate.test(Pair(it.state, action)))
+          }
+        }
+      }
+    val searchResult = searchStrategy.search(ldg, acceptancePredicate, expander, logger)
+    ldg.traces = searchResult.toList()
+    return AbstractorResult(searchResult.isEmpty())
+  }
+}