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 f35a7e1 commit 84cfdcc
Show file tree
Hide file tree
Showing 6 changed files with 187 additions and 73 deletions.
12 changes: 7 additions & 5 deletions ...in/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy {
if (targetNode.state.isBottom) {
return emptyList()
}
if (targetNode == seed) {
if (targetNode == seed && trace.isNotEmpty()) {
return trace + edge
}
if (redNodes.contains(targetNode)) {
Expand Down Expand Up @@ -83,9 +83,11 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy {
// 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<ASGEdge<S, A>> =
redSearch(accNode, edge, trace, mutableSetOf(), target, expand)
if (redSearch.isNotEmpty()) return setOf(ASGTrace(redSearch, accNode))
for (outEdge in expand(edge.target)) {
val redSearch: List<ASGEdge<S, A>> =
redSearch(accNode, outEdge, trace + edge, mutableSetOf(), target, expand)
if (redSearch.isNotEmpty()) return setOf(ASGTrace(redSearch, accNode))
}
}
if (blueNodes.contains(targetNode)) {
return emptyList()
Expand All @@ -94,7 +96,7 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy {
for (nextEdge in expand(targetNode)) {
val blueSearch: Collection<ASGTrace<S, A>> =
blueSearch(nextEdge, trace + edge, blueNodes, redNodes, target, expand)
if (!blueSearch.isEmpty()) return blueSearch
if (blueSearch.isNotEmpty()) return blueSearch
}
return emptyList()
}
Expand Down
5 changes: 5 additions & 0 deletions ...main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,11 @@ import hu.bme.mit.theta.core.stmt.*
import hu.bme.mit.theta.core.type.Type
import hu.bme.mit.theta.core.utils.ExprUtils

/**
* Collects vars from a statement to a fixpoint. Collects recursively only variables that are
* dependant on the input set on themselves. To collect all variables from a statement, use
* [hu.bme.mit.theta.core.utils.StmtUtils.getVars] instead.
*/
class VarCollectorStmtVisitor : StmtVisitor<Set<VarDecl<*>>, Set<VarDecl<*>>> {

companion object {
Expand Down
156 changes: 93 additions & 63 deletions ...s/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGCegarVerifierTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -140,39 +140,56 @@ private void testWithXsts() throws IOException {
final AcceptancePredicate<XstsState<PredState>, XstsAction> target =
new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE);
logger.write(Logger.Level.MAINSTEP, "Verifying %s%n", xsts.getProp());
var abstractor =
new ASGAbstractor<>(
analysis,
lts,
target,
LoopcheckerSearchStrategy.Companion.getDefault(),
logger);
final Refiner<
PredPrec,
ASG<XstsState<PredState>, XstsAction>,
ASGTrace<XstsState<PredState>, XstsAction>>
refiner =
new SingleASGTraceRefiner<>(
ASGTraceCheckerStrategy.Companion.getDefault(),
solverFactory,
JoiningPrecRefiner.create(
new ItpRefToPredPrec(ExprSplitters.atoms())),
logger,
xsts.getInitFormula());
final CegarChecker<
PredPrec,
ASG<XstsState<PredState>, XstsAction>,
ASGTrace<XstsState<PredState>, XstsAction>>
verifier =
CegarChecker.create(
abstractor,
refiner,
logger,
new AsgVisualizer<>(Objects::toString, Objects::toString));
LoopcheckerSearchStrategy.getEntries()
.forEach(
lStrat -> {
ASGTraceCheckerStrategy.getEntries()
.forEach(
strat -> {
var abstractor =
new ASGAbstractor<>(
analysis, lts, target, lStrat,
logger);
final Refiner<
PredPrec,
ASG<
XstsState<PredState>,
XstsAction>,
ASGTrace<
XstsState<PredState>,
XstsAction>>
refiner =
new SingleASGTraceRefiner<>(
strat,
solverFactory,
JoiningPrecRefiner.create(
new ItpRefToPredPrec(
ExprSplitters
.atoms())),
logger,
xsts.getInitFormula());
final CegarChecker<
PredPrec,
ASG<
XstsState<PredState>,
XstsAction>,
ASGTrace<
XstsState<PredState>,
XstsAction>>
verifier =
CegarChecker.create(
abstractor,
refiner,
logger,
new AsgVisualizer<>(
Objects::toString,
Objects::toString));

final PredPrec precision = PredPrec.of();
var result = verifier.check(precision);
Assert.assertEquals(this.result, result.isUnsafe());
final PredPrec precision = PredPrec.of();
var result = verifier.check(precision);
Assert.assertEquals(this.result, result.isUnsafe());
});
});
}

private void testWithCfa() throws IOException {
Expand All @@ -195,37 +212,50 @@ private void testWithCfa() throws IOException {
new ItpRefToPredPrec(ExprSplitters.atoms());
final RefutationToGlobalCfaPrec<PredPrec, ItpRefutation> cfaRefToPrec =
new RefutationToGlobalCfaPrec<>(refToPrec, cfa.getInitLoc());
var abstractor =
new ASGAbstractor<>(
analysis,
lts,
target,
LoopcheckerSearchStrategy.Companion.getDefault(),
logger);
final Refiner<
CfaPrec<PredPrec>,
ASG<CfaState<PredState>, CfaAction>,
ASGTrace<CfaState<PredState>, CfaAction>>
refiner =
new SingleASGTraceRefiner<>(
ASGTraceCheckerStrategy.Companion.getDefault(),
solverFactory,
JoiningPrecRefiner.create(cfaRefToPrec),
logger,
True());
final CegarChecker<
CfaPrec<PredPrec>,
ASG<CfaState<PredState>, CfaAction>,
ASGTrace<CfaState<PredState>, CfaAction>>
verifier =
CegarChecker.create(
abstractor,
refiner,
logger,
new AsgVisualizer<>(Objects::toString, Objects::toString));
LoopcheckerSearchStrategy.getEntries()
.forEach(
lStrat -> {
ASGTraceCheckerStrategy.getEntries()
.forEach(
strat -> {
var abstractor =
new ASGAbstractor<>(
analysis, lts, target, lStrat,
logger);
final Refiner<
CfaPrec<PredPrec>,
ASG<CfaState<PredState>, CfaAction>,
ASGTrace<
CfaState<PredState>,
CfaAction>>
refiner =
new SingleASGTraceRefiner<>(
strat,
solverFactory,
JoiningPrecRefiner.create(
cfaRefToPrec),
logger,
True());
final CegarChecker<
CfaPrec<PredPrec>,
ASG<CfaState<PredState>, CfaAction>,
ASGTrace<
CfaState<PredState>,
CfaAction>>
verifier =
CegarChecker.create(
abstractor,
refiner,
logger,
new AsgVisualizer<>(
Objects::toString,
Objects::toString));

final GlobalCfaPrec<PredPrec> prec = GlobalCfaPrec.create(PredPrec.of());
var res = verifier.check(prec);
Assert.assertEquals(result, res.isUnsafe());
final GlobalCfaPrec<PredPrec> prec =
GlobalCfaPrec.create(PredPrec.of());
var res = verifier.check(prec);
Assert.assertEquals(result, res.isUnsafe());
});
});
}
}
12 changes: 8 additions & 4 deletions ...is/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGTraceCheckerTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,9 +84,13 @@ public void testWithCounter3() throws IOException {
abstractor.check(ASG, precision);
ASGTrace<XstsState<PredState>, XstsAction> trace = ASG.getTraces().iterator().next();

ExprTraceStatus<ItpRefutation> status =
ASGTraceCheckerStrategy.Companion.getDefault()
.check(trace, solverFactory, xsts.getInitFormula(), logger);
Assert.assertTrue(status.isInfeasible());
ASGTraceCheckerStrategy.getEntries()
.forEach(
strat -> {
ExprTraceStatus<ItpRefutation> status =
strat.check(
trace, solverFactory, xsts.getInitFormula(), logger);
Assert.assertTrue(status.isInfeasible());
});
}
}
74 changes: 74 additions & 0 deletions ...java/hu/bme/mit/theta/analysis/algorithm/loopchecker/utils/VarCollectorStmtVisitorTest.kt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,74 @@
/*
* 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.utils

import hu.bme.mit.theta.analysis.algorithm.loopchecker.util.VarCollectorStmtVisitor
import hu.bme.mit.theta.core.decl.Decls
import hu.bme.mit.theta.core.decl.VarDecl
import hu.bme.mit.theta.core.stmt.IfStmt
import hu.bme.mit.theta.core.stmt.Stmt
import hu.bme.mit.theta.core.stmt.Stmts
import hu.bme.mit.theta.core.type.booltype.BoolExprs
import hu.bme.mit.theta.core.type.booltype.BoolType
import hu.bme.mit.theta.core.type.inttype.IntExprs
import hu.bme.mit.theta.core.type.inttype.IntType
import java.util.*
import org.junit.Assert
import org.junit.Test
import org.junit.runner.RunWith
import org.junit.runners.Parameterized

@RunWith(Parameterized::class)
class VarCollectorStmtVisitorTest(
private val stmt: Stmt,
private val inputVars: Set<VarDecl<*>>,
private val expectedVars: Set<VarDecl<*>>,
) {

@Test
fun test() {
val vars = VarCollectorStmtVisitor.visitAll(listOf(stmt), inputVars)
Assert.assertEquals(expectedVars, vars)
}

companion object {

private val VA: VarDecl<BoolType?> = Decls.Var("a", BoolExprs.Bool())
private val VB: VarDecl<IntType?> = Decls.Var("b", IntExprs.Int())
private val VC: VarDecl<IntType?> = Decls.Var("d", IntExprs.Int())

@JvmStatic
@Parameterized.Parameters
fun data(): Collection<Array<Any>> {
return listOf(
arrayOf(Stmts.Skip(), emptySet<VarDecl<*>>(), emptySet<VarDecl<*>>()),
arrayOf(Stmts.Havoc(VA), emptySet<VarDecl<*>>(), setOf(VA)),
arrayOf(Stmts.Havoc(VB), emptySet<VarDecl<*>>(), setOf(VB)),
arrayOf(Stmts.Havoc(VA), setOf(VA), setOf(VA)),
arrayOf(Stmts.Havoc(VB), setOf(VA), setOf(VA, VB)),
arrayOf(Stmts.Assign(VB, IntExprs.Int(0)), setOf(VB), setOf(VB)),
arrayOf(Stmts.Assign(VB, IntExprs.Add(VB.ref, IntExprs.Int(1))), setOf(VB), setOf(VB)),
arrayOf(Stmts.Assign(VB, IntExprs.Add(VC.ref, VC.ref)), setOf(VC), setOf(VB, VC)),
arrayOf(
Stmts.Assume(BoolExprs.And(VA.ref, IntExprs.Eq(VB.ref, VC.ref))),
setOf(VC),
setOf(VC),
),
arrayOf(IfStmt.of(BoolExprs.False(), Stmts.Havoc(VB)), emptySet<VarDecl<*>>(), setOf(VB)),
)
}
}
}
1 change: 0 additions & 1 deletion ...ojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@ package hu.bme.mit.theta.common.ltl

import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy
import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy
import hu.bme.mit.theta.analysis.multi.MultiSide
import hu.bme.mit.theta.analysis.pred.ExprSplitters
import hu.bme.mit.theta.analysis.pred.ItpRefToPredPrec
import hu.bme.mit.theta.common.cfa.buchi.hoa.Ltl2BuchiThroughHoaf
Expand Down

0 comments on commit 84cfdcc

Please sign in to comment.