Skip to content

Commit

Permalink
ltl
Browse files Browse the repository at this point in the history
  • Loading branch information
RipplB committed Aug 5, 2024
1 parent b1d8e5d commit f382dc1
Show file tree
Hide file tree
Showing 31 changed files with 1,477 additions and 27 deletions.
1 change: 1 addition & 0 deletions settings.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ include(
"common/common",
"common/core",
"common/grammar",
"common/ltl",
"common/multi-tests",

"frontends/c-frontend",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,17 @@
*/
package hu.bme.mit.theta.analysis.multi;

import com.google.common.base.Preconditions;

public enum MultiSide {
LEFT, RIGHT, BOTH
LEFT, RIGHT, BOTH;

public MultiSide otherSide() {
return complementer(this);
}

public static MultiSide complementer(MultiSide side) {
Preconditions.checkState(side != BOTH, "Only LEFT or RIGHT have complementer side");
return side == LEFT ? RIGHT : LEFT;
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,8 @@ class LDGAbstractor<S : ExprState, A : ExprAction, P : Prec>(
}
val expander: NodeExpander<S, A> = { node ->
lts.getEnabledActionsFor(node.state).flatMap { action ->
analysis.transFunc.getSuccStates(node.state, action, prec).map(ldg::getOrCreateNode)
analysis.transFunc.getSuccStates(node.state, action, prec).filterNot { it.isBottom }
.map(ldg::getOrCreateNode)
.map { ldg.drawEdge(node, it, action, acceptancePredicate.test(Pair(it.state, action))) }
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@ 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 java.util.*


object NdfsSearchStrategy : ILoopcheckerSearchStrategy {
Expand All @@ -42,52 +41,46 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy {
}

private fun <S : ExprState, A : ExprAction> redSearch(
seed: LDGNode<S, A>, edge: LDGEdge<S, A>, trace: MutableList<LDGEdge<S, A>>,
seed: LDGNode<S, A>, edge: LDGEdge<S, A>, trace: List<LDGEdge<S, A>>,
redNodes: MutableSet<LDGNode<S, A>>, target: AcceptancePredicate<S, A>, expand: NodeExpander<S, A>
): List<LDGEdge<S, A>> {
val targetNode = edge.target
trace.add(edge)
if (targetNode == seed) {
return trace
return trace + edge
}
if (redNodes.contains(targetNode)) {
trace.removeLast()
return emptyList()
}
redNodes.add(edge.target)
for (nextEdge in expand(targetNode)) {
val redSearch: List<LDGEdge<S, A>> = redSearch(seed, nextEdge, trace, redNodes, target, expand)
val redSearch: List<LDGEdge<S, A>> = redSearch(seed, nextEdge, trace + edge, redNodes, target, expand)
if (redSearch.isNotEmpty()) return redSearch
}
trace.removeLast()
return emptyList()
}

private fun <S : ExprState, A : ExprAction> blueSearch(
edge: LDGEdge<S, A>, trace: MutableList<LDGEdge<S, A>>, blueNodes: MutableCollection<LDGNode<S, A>>,
edge: LDGEdge<S, A>, trace: List<LDGEdge<S, A>>, blueNodes: MutableCollection<LDGNode<S, A>>,
redNodes: Set<LDGNode<S, A>>, target: AcceptancePredicate<S, A>, expand: NodeExpander<S, A>
): Collection<LDGTrace<S, A>> {
val targetNode = edge.target
trace.add(edge)
if (target.test(Pair(targetNode.state, edge.action))) {
// Edge source can only be null artificially, and is only used when calling other search strategies
val accNode =
if (targetNode.accepting) targetNode else edge.source!!
val redSearch: List<LDGEdge<S, A>> =
redSearch(accNode, edge, LinkedList<LDGEdge<S, A>>(trace), mutableSetOf(), target, expand)
redSearch(accNode, edge, trace, mutableSetOf(), target, expand)
if (redSearch.isNotEmpty()) return setOf(LDGTrace(redSearch, accNode))
}
if (blueNodes.contains(targetNode)) {
trace.removeLast()
return emptyList()
}
blueNodes.add(edge.target)
for (nextEdge in expand(targetNode)) {
val blueSearch: Collection<LDGTrace<S, A>> =
blueSearch(nextEdge, trace, blueNodes, redNodes, target, expand)
blueSearch(nextEdge, trace + edge, blueNodes, redNodes, target, expand)
if (!blueSearch.isEmpty()) return blueSearch
}
trace.removeLast()
return emptyList()
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,8 @@ enum class LDGTraceCheckerStrategy {
override fun <S : ExprState, A : ExprAction> check(
trace: LDGTrace<S, A>, solverFactory: SolverFactory, init: Expr<BoolType>, logger: Logger
) = MilanoLDGTraceCheckerStrategy(trace, solverFactory, init, logger).check()
}, BOUNDED_UNROLLING {
},
BOUNDED_UNROLLING {

override fun <S : ExprState, A : ExprAction> check(
trace: LDGTrace<S, A>, solverFactory: SolverFactory, init: Expr<BoolType>, logger: Logger
Expand All @@ -61,28 +62,42 @@ enum class LDGTraceCheckerStrategy {

val default = MILANO
}
abstract fun<S: ExprState, A : ExprAction> check(trace: LDGTrace<S, A>, solverFactory: SolverFactory, init : Expr<BoolType> = True(), logger: Logger = NullLogger.getInstance()): ExprTraceStatus<ItpRefutation>

abstract fun <S : ExprState, A : ExprAction> check(
trace: LDGTrace<S, A>, solverFactory: SolverFactory, init: Expr<BoolType> = True(),
logger: Logger = NullLogger.getInstance()
): ExprTraceStatus<ItpRefutation>
}

abstract class AbstractLDGTraceCheckerStrategy<S: ExprState, A : ExprAction>(private val trace: LDGTrace<S, A>, solverFactory: SolverFactory, private val init : Expr<BoolType>, private val logger: Logger) {
abstract class AbstractLDGTraceCheckerStrategy<S : ExprState, A : ExprAction>(
private val trace: LDGTrace<S, A>, solverFactory: SolverFactory, private val init: Expr<BoolType>,
private val logger: Logger
) {

protected val solver: ItpSolver = solverFactory.createItpSolver()
protected val stateCount = trace.length() + 1
protected val indexings = mutableListOf<VarIndexing>()
protected val satMarker: ItpMarker = solver.createMarker()
protected val unreachableMarker: ItpMarker = solver.createMarker()
protected val pattern: ItpPattern = solver.createBinPattern(satMarker, unreachableMarker)
protected val variables = trace.edges.flatMap { ExprUtils.getVars(it.source?.state?.toExpr() ?: True()) + ExprUtils.getVars(it.action?.toExpr() ?: True()) }
protected val variables = trace.edges.flatMap {
ExprUtils.getVars(it.source?.state?.toExpr() ?: True()) + ExprUtils.getVars(
it.action?.toExpr() ?: True()
)
}.distinct()

private fun findSatIndex(): Int {
for (i in 1 until stateCount) {
solver.push()
indexings.add(indexings[i - 1].add(trace.getAction(i - 1)!!.nextIndexing()))
solver.add(satMarker, PathUtils.unfold(trace.getState(i).toExpr(), indexings[i]))
val stateExpression = PathUtils.unfold(trace.getState(i).toExpr(), indexings[i])
solver.add(satMarker, stateExpression)
val actionExpression = PathUtils.unfold(
trace.getAction(i - 1)!!.toExpr(),
indexings[i - 1]
)
solver.add(
satMarker, PathUtils.unfold(
trace.getAction(i - 1)!!.toExpr(),
indexings[i - 1]
)
satMarker, actionExpression
)
if (solver.check().isUnsat) {
solver.pop()
Expand All @@ -92,7 +107,7 @@ abstract class AbstractLDGTraceCheckerStrategy<S: ExprState, A : ExprAction>(pri
return stateCount - 1
}

abstract fun evaluateLoop(valuation: Valuation) : ExprTraceStatus<ItpRefutation>
abstract fun evaluateLoop(valuation: Valuation): ExprTraceStatus<ItpRefutation>

fun check(): ExprTraceStatus<ItpRefutation> {
solver.push()
Expand Down Expand Up @@ -136,7 +151,10 @@ abstract class AbstractLDGTraceCheckerStrategy<S: ExprState, A : ExprAction>(pri
}
}

protected fun getItpRefutationFeasible(): Feasible<ItpRefutation> = ExprTraceStatus.feasible(Trace.of(indexings.map { PathUtils.extractValuation(solver.model, it) }, (trace.tail + trace.loop).map { it.action }))
protected fun getItpRefutationFeasible(): Feasible<ItpRefutation> = ExprTraceStatus.feasible(
Trace.of(
indexings.map { PathUtils.extractValuation(solver.model, it) }, (trace.tail + trace.loop).map { it.action })
)

protected fun logInterpolant(expr: Expr<BoolType>) {
logger.write(Logger.Level.INFO, "Interpolant : $expr%n")
Expand Down
32 changes: 32 additions & 0 deletions subprojects/common/ltl/build.gradle.kts
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
/*
* 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.
*/
plugins {
id("kotlin-common")
}

dependencies {
implementation(project(":theta-common"))
implementation(project(":theta-core"))
implementation(project(":theta-solver"))
implementation(project(":theta-analysis"))
implementation(project(":theta-cfa"))
implementation(project(":theta-cfa-analysis"))
testImplementation(project(":theta-solver-z3-legacy"))
testImplementation(project(":theta-solver-javasmt"))
testImplementation(project(":theta-solver-smtlib"))
testImplementation(project(":theta-xsts"))
testImplementation(project(":theta-xsts-analysis"))
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
/*
* 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.common.ltl

import hu.bme.mit.theta.analysis.InitFunc
import hu.bme.mit.theta.analysis.LTS
import hu.bme.mit.theta.analysis.Prec
import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate
import hu.bme.mit.theta.analysis.expr.ExprState
import hu.bme.mit.theta.analysis.expr.StmtAction
import hu.bme.mit.theta.analysis.multi.stmt.ExprMultiState
import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiAction
import hu.bme.mit.theta.analysis.unit.UnitState
import hu.bme.mit.theta.cfa.CFA
import hu.bme.mit.theta.cfa.analysis.CfaAction
import hu.bme.mit.theta.cfa.analysis.CfaState

class BuchiInitFunc<P : Prec>(private val initLoc: CFA.Loc) : InitFunc<CfaState<UnitState>, P> {

override fun getInitStates(prec: P) = mutableListOf(CfaState.of(initLoc, UnitState.getInstance()))
}

class BuchiLts<D : ExprState> : LTS<CfaState<D>, CfaAction> {

override fun getEnabledActionsFor(state: CfaState<D>) = state.loc.outEdges.map(CfaAction::create)
}

fun <S : ExprState, D : ExprState, A : StmtAction> buchiPredicate(
buchiAutomaton: CFA
): AcceptancePredicate<ExprMultiState<S, CfaState<UnitState>, D>, StmtMultiAction<A, CfaAction>> = AcceptancePredicate(
actionPredicate = { a ->
(a?.rightAction != null && a.rightAction.edges.any { e ->
buchiAutomaton.acceptingEdges.contains(
e
)
})
})

fun <D : ExprState> combineBlankBuchiStateWithData(buchiState: CfaState<UnitState>, dataState: D) =
CfaState.of(buchiState.loc, dataState)

fun <D : ExprState> stripDataFromBuchiState(buchiState: CfaState<D>) =
CfaState.of(buchiState.loc, UnitState.getInstance())
Original file line number Diff line number Diff line change
@@ -0,0 +1,119 @@
/*
* 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.common.ltl

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.SafetyChecker
import hu.bme.mit.theta.analysis.algorithm.SafetyResult
import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker
import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace
import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LDGAbstractor
import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy
import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG
import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy
import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.SingleLDGTraceRefiner
import hu.bme.mit.theta.analysis.expr.ExprState
import hu.bme.mit.theta.analysis.expr.StmtAction
import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation
import hu.bme.mit.theta.analysis.expr.refinement.JoiningPrecRefiner
import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec
import hu.bme.mit.theta.analysis.multi.MultiAnalysisSide
import hu.bme.mit.theta.analysis.multi.MultiPrec
import hu.bme.mit.theta.analysis.multi.NextSideFunctions
import hu.bme.mit.theta.analysis.multi.RefToMultiPrec
import hu.bme.mit.theta.analysis.multi.builder.stmt.StmtMultiBuilder
import hu.bme.mit.theta.analysis.multi.stmt.ExprMultiState
import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiAction
import hu.bme.mit.theta.analysis.unit.UnitPrec
import hu.bme.mit.theta.analysis.unit.UnitState
import hu.bme.mit.theta.analysis.utils.LdgVisualizer
import hu.bme.mit.theta.cfa.CFA
import hu.bme.mit.theta.cfa.analysis.CfaAction
import hu.bme.mit.theta.cfa.analysis.CfaAnalysis
import hu.bme.mit.theta.cfa.analysis.CfaPrec
import hu.bme.mit.theta.cfa.analysis.CfaState
import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec
import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec
import hu.bme.mit.theta.cfa.buchi.BuchiBuilder
import hu.bme.mit.theta.common.logging.Logger
import hu.bme.mit.theta.core.decl.VarDecl
import hu.bme.mit.theta.core.type.Expr
import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
import hu.bme.mit.theta.core.type.booltype.BoolType
import hu.bme.mit.theta.solver.SolverFactory

class LtlChecker<S : ExprState, ControlS : ExprState, A : StmtAction, P : Prec, ControlP : Prec, DataP : Prec, DataS : ExprState>(
multiSide: MultiAnalysisSide<S, DataS, ControlS, A, P, ControlP>,
lts: LTS<in S, A>,
refToPrec: RefutationToPrec<P, ItpRefutation>,
dataRefToPrec: RefutationToPrec<DataP, ItpRefutation>,
dataAnalysis: Analysis<DataS, in CfaAction, DataP>,
variables: Collection<VarDecl<*>>,
ltl: String,
solverFactory: SolverFactory,
logger: Logger,
searchStrategy: LoopcheckerSearchStrategy,
refinerStrategy: LDGTraceCheckerStrategy,
initExpr: Expr<BoolType> = True(),
nextSideFunction: NextSideFunctions.NextSideFunction<ControlS, CfaState<UnitState>, DataS, ExprMultiState<ControlS, CfaState<UnitState>, DataS>> = NextSideFunctions.Alternating()
) : SafetyChecker<LDG<ExprMultiState<ControlS, CfaState<UnitState>, DataS>, StmtMultiAction<A, CfaAction>>, LDGTrace<ExprMultiState<ControlS, CfaState<UnitState>, DataS>, StmtMultiAction<A, CfaAction>>, MultiPrec<P, CfaPrec<DataP>, DataP>> {

private val checker: CegarChecker<ExprMultiState<ControlS, CfaState<UnitState>, DataS>, StmtMultiAction<A, CfaAction>, MultiPrec<P, CfaPrec<DataP>, DataP>, LDG<ExprMultiState<ControlS, CfaState<UnitState>, DataS>, StmtMultiAction<A, CfaAction>>, LDGTrace<ExprMultiState<ControlS, CfaState<UnitState>, DataS>, StmtMultiAction<A, CfaAction>>>
private val buchiAutomaton: CFA

init {
buchiAutomaton = BuchiBuilder.of(ltl, variables, logger)
val cfaAnalysis: Analysis<CfaState<DataS>, CfaAction, CfaPrec<DataP>> =
CfaAnalysis.create(buchiAutomaton.initLoc, dataAnalysis)
val buchiSide = MultiAnalysisSide(
cfaAnalysis, BuchiInitFunc(buchiAutomaton.initLoc), ::combineBlankBuchiStateWithData,
::stripDataFromBuchiState, { it.state }, { _ -> GlobalCfaPrec.create(UnitPrec.getInstance()) })
val product = StmtMultiBuilder(multiSide, lts).addRightSide(
buchiSide, BuchiLts()
).build(nextSideFunction, dataAnalysis.initFunc)
val buchiRefToPrec =
RefutationToGlobalCfaPrec(dataRefToPrec, buchiAutomaton.initLoc)
val multiRefToPrec = RefToMultiPrec(refToPrec, buchiRefToPrec, dataRefToPrec)
val multiAnalysis = product.side.analysis
val abstractor =
LDGAbstractor(multiAnalysis, product.lts, buchiPredicate(buchiAutomaton), searchStrategy, logger)
val refiner: SingleLDGTraceRefiner<ExprMultiState<ControlS, CfaState<UnitState>, DataS>, StmtMultiAction<A, CfaAction>, MultiPrec<P, CfaPrec<DataP>, DataP>> =
SingleLDGTraceRefiner(
refinerStrategy, solverFactory, JoiningPrecRefiner.create(multiRefToPrec), logger, initExpr
)
val visualizer =
LdgVisualizer<ExprMultiState<ControlS, CfaState<UnitState>, DataS>, StmtMultiAction<A, CfaAction>>(
{ it.toString() },
{ it.toString() }
)
checker = CegarChecker.create(abstractor, refiner, logger, visualizer)
}

override fun check(
input: MultiPrec<P, CfaPrec<DataP>, DataP>
): SafetyResult<LDG<ExprMultiState<ControlS, CfaState<UnitState>, DataS>, StmtMultiAction<A, CfaAction>>, LDGTrace<ExprMultiState<ControlS, CfaState<UnitState>, DataS>, StmtMultiAction<A, CfaAction>>> {
return checker.check(input)
}

fun check(
prec: P, dataPrec: DataP
): SafetyResult<LDG<ExprMultiState<ControlS, CfaState<UnitState>, DataS>, StmtMultiAction<A, CfaAction>>, LDGTrace<ExprMultiState<ControlS, CfaState<UnitState>, DataS>, StmtMultiAction<A, CfaAction>>> {
return check(MultiPrec(prec, GlobalCfaPrec.create(dataPrec), dataPrec))
}
}
Loading

0 comments on commit f382dc1

Please sign in to comment.