Skip to content

Commit

Permalink
LTL checking capability
Browse files Browse the repository at this point in the history 
Add possibility of checking LTL properties with CEGAR.
CFA is now extended with optional accepting edges. Classes are available that convert LTL string to such CFA.
  • Loading branch information
@RipplB
RipplB committed Dec 4, 2024
1 parent 13d0f23 commit f35a7e1
Show file tree
Hide file tree
Showing 29 changed files with 475 additions and 368 deletions.
48 changes: 22 additions & 26 deletions ...analysis/algorithm/loopchecker/ldg/LDG.kt → ...e/mit/theta/analysis/algorithm/asg/ASG.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,21 +13,21 @@
* See the License for the specific language governing permissions and
* limitations under the License.
*/
package hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg
package hu.bme.mit.theta.analysis.algorithm.asg

import hu.bme.mit.theta.analysis.algorithm.Proof
import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate
import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace
import hu.bme.mit.theta.analysis.expr.ExprAction
import hu.bme.mit.theta.analysis.expr.ExprState

class LDG<S : ExprState, A : ExprAction>(
/** Abstract state graph */
class ASG<S : ExprState, A : ExprAction>(
private val acceptancePredicate: AcceptancePredicate<in S, in A>
) : Proof {

val nodes: MutableMap<S, LDGNode<S, A>> = mutableMapOf()
val initNodes: MutableList<LDGNode<S, A>> = mutableListOf()
var traces: List<LDGTrace<S, A>> = emptyList()
val nodes: MutableMap<S, ASGNode<S, A>> = mutableMapOf()
val initNodes: MutableList<ASGNode<S, A>> = mutableListOf()
var traces: List<ASGTrace<S, A>> = emptyList()

fun isUninitialised() = initNodes.isEmpty()

Expand All @@ -42,52 +42,48 @@ class LDG<S : ExprState, A : ExprAction>(
initNodes.addAll(initStates.map(this::getOrCreateNode))
}

fun getOrCreateNode(state: S): LDGNode<S, A> =
nodes.computeIfAbsent(state) { s -> LDGNode(s, acceptancePredicate.test(Pair(s, null))) }
fun getOrCreateNode(state: S): ASGNode<S, A> =
nodes.computeIfAbsent(state) { s -> ASGNode(s, acceptancePredicate.test(Pair(s, null))) }

fun containsNode(state: S) = nodes.containsKey(state)

fun drawEdge(
source: LDGNode<S, A>,
target: LDGNode<S, A>,
source: ASGNode<S, A>,
target: ASGNode<S, A>,
action: A?,
accepting: Boolean,
): LDGEdge<S, A> {
val edge = LDGEdge(source, target, action, accepting)
): ASGEdge<S, A> {
val edge = ASGEdge(source, target, action, accepting)
source.addOutEdge(edge)
target.addInEdge(edge)
return edge
}
}

data class LDGEdge<S : ExprState, A : ExprAction>(
val source: LDGNode<S, A>?,
val target: LDGNode<S, A>,
data class ASGEdge<S : ExprState, A : ExprAction>(
val source: ASGNode<S, A>?,
val target: ASGNode<S, A>,
val action: A?,
val accepting: Boolean,
)

class LDGNode<S : ExprState, A : ExprAction>(val state: S, val accepting: Boolean) {
class ASGNode<S : ExprState, A : ExprAction>(val state: S, val accepting: Boolean) {
companion object {

var idCounter: Long = 0
}

val inEdges: MutableList<LDGEdge<S, A>> = mutableListOf()
val outEdges: MutableList<LDGEdge<S, A>> = mutableListOf()
val inEdges: MutableList<ASGEdge<S, A>> = mutableListOf()
val outEdges: MutableList<ASGEdge<S, A>> = mutableListOf()
val id = idCounter++
var validLoopHondas: MutableSet<LDGNode<S, A>> = hashSetOf()
var validLoopHondas: MutableSet<ASGNode<S, A>> = hashSetOf()
var expanded: Boolean = false
set(value) {
if (!value) {
throw IllegalArgumentException("Can't set expanded to false")
}
require(value) { "Can't set expanded to false" }
field = true
}

fun addInEdge(edge: LDGEdge<S, A>) = inEdges.add(edge)
fun addInEdge(edge: ASGEdge<S, A>) = inEdges.add(edge)

fun addOutEdge(edge: LDGEdge<S, A>) = outEdges.add(edge)

fun smallerEdgeCollection() = if (inEdges.size > outEdges.size) inEdges else outEdges
fun addOutEdge(edge: ASGEdge<S, A>) = outEdges.add(edge)
}
18 changes: 8 additions & 10 deletions ...nalysis/algorithm/loopchecker/LDGTrace.kt → .../theta/analysis/algorithm/asg/ASGTrace.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,28 +13,26 @@
* See the License for the specific language governing permissions and
* limitations under the License.
*/
package hu.bme.mit.theta.analysis.algorithm.loopchecker
package hu.bme.mit.theta.analysis.algorithm.asg

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>>,
class ASGTrace<S : ExprState, A : ExprAction>(
val tail: List<ASGEdge<S, A>>,
val honda: ASGNode<S, A>,
val loop: List<ASGEdge<S, A>>,
) : Cex {

val edges by lazy { tail + loop }

constructor(
edges: List<LDGEdge<S, A>>,
honda: LDGNode<S, A>,
edges: List<ASGEdge<S, A>>,
honda: ASGNode<S, A>,
) : this(edges.takeWhile { it.source != honda }, honda, edges.dropWhile { it.source != honda })

init {
Expand All @@ -51,7 +49,7 @@ class LDGTrace<S : ExprState, A : ExprAction>(

override fun length() = edges.size

fun getEdge(index: Int): LDGEdge<S, A> {
fun getEdge(index: Int): ASGEdge<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]
Expand Down
8 changes: 3 additions & 5 deletions ...loopchecker/refinement/LDGTraceRefiner.kt → ...analysis/algorithm/asg/ASGTraceRefiner.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,14 +13,12 @@
* See the License for the specific language governing permissions and
* limitations under the License.
*/
package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement
package hu.bme.mit.theta.analysis.algorithm.asg

import hu.bme.mit.theta.analysis.Prec
import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner
import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace
import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG
import hu.bme.mit.theta.analysis.expr.ExprAction
import hu.bme.mit.theta.analysis.expr.ExprState

interface LDGTraceRefiner<S : ExprState, A : ExprAction, P : Prec> :
Refiner<P, LDG<S, A>, LDGTrace<S, A>> {}
interface ASGTraceRefiner<S : ExprState, A : ExprAction, P : Prec> :
Refiner<P, ASG<S, A>, ASGTrace<S, A>>
2 changes: 1 addition & 1 deletion ...common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ public final class CegarChecker<P extends Prec, Pr extends Proof, C extends Cex>
private final Refiner<P, Pr, C> refiner;
private final Logger logger;
private final Pr proof;
private final ProofVisualizer<? super Pr> proofVisualizer;
public final ProofVisualizer<? super Pr> proofVisualizer;

private CegarChecker(
final Abstractor<P, Pr> abstractor,
Expand Down
30 changes: 15 additions & 15 deletions .../loopchecker/abstraction/LDGAbstractor.kt → .../loopchecker/abstraction/ASGAbstractor.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,45 +18,45 @@ 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.asg.ASG
import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge
import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode
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>(
class ASGAbstractor<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>> {
) : Abstractor<P, ASG<S, A>> {

override fun createProof() = LDG(acceptancePredicate)
override fun createProof() = ASG(acceptancePredicate)

override fun check(ldg: LDG<S, A>, prec: P): AbstractorResult {
if (ldg.isUninitialised()) {
ldg.initialise(analysis.initFunc.getInitStates(prec))
ldg.traces = emptyList()
override fun check(ASG: ASG<S, A>, prec: P): AbstractorResult {
if (ASG.isUninitialised()) {
ASG.initialise(analysis.initFunc.getInitStates(prec))
ASG.traces = emptyList()
}
val expander: NodeExpander<S, A> =
fun(node: LDGNode<S, A>): Collection<LDGEdge<S, A>> {
fun(node: ASGNode<S, A>): Collection<ASGEdge<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)))
analysis.transFunc.getSuccStates(node.state, action, prec).map(ASG::getOrCreateNode).map {
ASG.drawEdge(node, it, action, acceptancePredicate.test(Pair(it.state, action)))
}
}
}
val searchResult = searchStrategy.search(ldg, acceptancePredicate, expander, logger)
ldg.traces = searchResult.toList()
val searchResult = searchStrategy.search(ASG, acceptancePredicate, expander, logger)
ASG.traces = searchResult.toList()
return AbstractorResult(searchResult.isEmpty())
}
}
38 changes: 19 additions & 19 deletions .../java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,30 +15,30 @@
*/
package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction

import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge
import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode
import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace
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>>?>
typealias BacktrackResult<S, A> = Pair<Set<ASGNode<S, A>>?, List<ASGTrace<S, A>>?>

fun <S : ExprState, A : ExprAction> combineLassos(results: Collection<BacktrackResult<S, A>>) =
Pair(setOf<LDGNode<S, A>>(), results.flatMap { it.second ?: emptyList() })
Pair(setOf<ASGNode<S, A>>(), results.flatMap { it.second ?: emptyList() })

abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy {

internal fun <S : ExprState, A : ExprAction> expandFromInitNodeUntilTarget(
initNode: LDGNode<S, A>,
initNode: ASGNode<S, A>,
stopAtLasso: Boolean,
expand: NodeExpander<S, A>,
logger: Logger,
): Collection<LDGTrace<S, A>> {
): Collection<ASGTrace<S, A>> {
return expandThroughNode(
emptyMap(),
LDGEdge(null, initNode, null, false),
ASGEdge(null, initNode, null, false),
emptyList(),
0,
stopAtLasso,
Expand All @@ -49,15 +49,15 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy {
}

private fun <S : ExprState, A : ExprAction> expandThroughNode(
pathSoFar: Map<LDGNode<S, A>, Int>,
incomingEdge: LDGEdge<S, A>,
edgesSoFar: List<LDGEdge<S, A>>,
pathSoFar: Map<ASGNode<S, A>, Int>,
incomingEdge: ASGEdge<S, A>,
edgesSoFar: List<ASGEdge<S, A>>,
targetsSoFar: Int,
stopAtLasso: Boolean,
expand: NodeExpander<S, A>,
logger: Logger,
): BacktrackResult<S, A> {
val expandingNode: LDGNode<S, A> = incomingEdge.target
val expandingNode: ASGNode<S, A> = incomingEdge.target
logger.write(
Logger.Level.VERBOSE,
"Expanding through %s edge to %s node with state %s%n",
Expand Down Expand Up @@ -86,7 +86,7 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy {
targetsThatFar,
)
}
val lasso: LDGTrace<S, A> = LDGTrace(edgesSoFar + incomingEdge, expandingNode)
val lasso: ASGTrace<S, A> = ASGTrace(edgesSoFar + incomingEdge, expandingNode)
logger.write(Logger.Level.DETAIL, "Built the following lasso:%n")
lasso.print(logger, Logger.Level.DETAIL)
return BacktrackResult(null, listOf(lasso))
Expand All @@ -102,7 +102,7 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy {
}
val expandStrategy: NodeExpander<S, A> =
if (needsTraversing) expand else { _ -> mutableSetOf() }
val outgoingEdges: Collection<LDGEdge<S, A>> = expandStrategy(expandingNode)
val outgoingEdges: Collection<ASGEdge<S, A>> = expandStrategy(expandingNode)
val results: MutableList<BacktrackResult<S, A>> = mutableListOf()
for (newEdge in outgoingEdges) {
val result: BacktrackResult<S, A> =
Expand All @@ -120,7 +120,7 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy {
}
val result: BacktrackResult<S, A> = combineLassos(results)
if (result.second != null) return result
val validLoopHondas: Collection<LDGNode<S, A>> = results.flatMap { it.first ?: emptyList() }
val validLoopHondas: Collection<ASGNode<S, A>> = results.flatMap { it.first ?: emptyList() }
expandingNode.validLoopHondas.addAll(validLoopHondas)
return BacktrackResult(validLoopHondas.toSet(), null)
}
Expand All @@ -129,13 +129,13 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy {
object GdfsSearchStrategy : AbstractSearchStrategy() {

override fun <S : ExprState, A : ExprAction> search(
initNodes: Collection<LDGNode<S, A>>,
initNodes: Collection<ASGNode<S, A>>,
target: AcceptancePredicate<S, A>,
expand: NodeExpander<S, A>,
logger: Logger,
): Collection<LDGTrace<S, A>> {
): Collection<ASGTrace<S, A>> {
for (initNode in initNodes) {
val possibleTraces: Collection<LDGTrace<S, A>> =
val possibleTraces: Collection<ASGTrace<S, A>> =
expandFromInitNodeUntilTarget(initNode, true, expand, logger)
if (!possibleTraces.isEmpty()) {
return possibleTraces
Expand All @@ -148,7 +148,7 @@ object GdfsSearchStrategy : AbstractSearchStrategy() {
object FullSearchStrategy : AbstractSearchStrategy() {

override fun <S : ExprState, A : ExprAction> search(
initNodes: Collection<LDGNode<S, A>>,
initNodes: Collection<ASGNode<S, A>>,
target: AcceptancePredicate<S, A>,
expand: NodeExpander<S, A>,
logger: Logger,
Expand Down
18 changes: 9 additions & 9 deletions .../hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,17 +15,17 @@
*/
package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction

import hu.bme.mit.theta.analysis.algorithm.asg.ASG
import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge
import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode
import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace
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.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
import hu.bme.mit.theta.common.logging.NullLogger

typealias NodeExpander<S, A> = (LDGNode<S, A>) -> Collection<LDGEdge<S, A>>
typealias NodeExpander<S, A> = (ASGNode<S, A>) -> Collection<ASGEdge<S, A>>

enum class LoopcheckerSearchStrategy(private val strategy: ILoopcheckerSearchStrategy) {
GDFS(GdfsSearchStrategy),
Expand All @@ -38,19 +38,19 @@ enum class LoopcheckerSearchStrategy(private val strategy: ILoopcheckerSearchStr
}

fun <S : ExprState, A : ExprAction> search(
ldg: LDG<S, A>,
ASG: ASG<S, A>,
target: AcceptancePredicate<S, A>,
expand: NodeExpander<S, A>,
logger: Logger = NullLogger.getInstance(),
): Collection<LDGTrace<S, A>> = strategy.search(ldg.initNodes, target, expand, logger)
): Collection<ASGTrace<S, A>> = strategy.search(ASG.initNodes, target, expand, logger)
}

interface ILoopcheckerSearchStrategy {

fun <S : ExprState, A : ExprAction> search(
initNodes: Collection<LDGNode<S, A>>,
initNodes: Collection<ASGNode<S, A>>,
target: AcceptancePredicate<S, A>,
expand: NodeExpander<S, A>,
logger: Logger,
): Collection<LDGTrace<S, A>>
): Collection<ASGTrace<S, A>>
}
Loading

0 comments on commit f35a7e1

Please sign in to comment.