From 05c2d2d9ef089ec74e99f73ca075f7d7d694971d Mon Sep 17 00:00:00 2001 From: RipplB Date: Wed, 20 Nov 2024 10:08:33 +0100 Subject: [PATCH] LTL checking capability 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. --- .../mit/theta/analysis/unit/UnitInitFunc.java | 5 ++--- .../loopchecker/LDGAbstractorCheckingTest.java | 16 ++++++++-------- .../theta/common/cfa/buchi/hoa/BuchiBuilder.kt | 2 +- .../theta/common/ltl/LtlCheckTestWithCfaExpl.kt | 2 +- .../theta/common/ltl/LtlCheckTestWithCfaPred.kt | 2 +- .../theta/common/ltl/LtlCheckTestWithXstsExpl.kt | 2 +- .../theta/common/ltl/LtlCheckTestWithXstsPred.kt | 2 +- 7 files changed, 15 insertions(+), 16 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java index 87326268f1..78289cc1e0 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java @@ -15,13 +15,12 @@ */ package hu.bme.mit.theta.analysis.unit; +import static com.google.common.base.Preconditions.checkNotNull; + import com.google.common.collect.ImmutableList; import hu.bme.mit.theta.analysis.InitFunc; - import java.util.Collection; -import static com.google.common.base.Preconditions.checkNotNull; - public final class UnitInitFunc implements InitFunc { private static final UnitInitFunc INSTANCE = new UnitInitFunc(); diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java index 4c6acec5e1..8581ee7a2c 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java @@ -15,8 +15,6 @@ */ package hu.bme.mit.theta.analysis.algorithm.loopchecker; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; - import hu.bme.mit.theta.analysis.Analysis; import hu.bme.mit.theta.analysis.LTS; import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult; @@ -45,6 +43,12 @@ import hu.bme.mit.theta.xsts.analysis.*; import hu.bme.mit.theta.xsts.analysis.initprec.XstsAllVarsInitPrec; import hu.bme.mit.theta.xsts.dsl.XstsDslManager; +import kotlin.Unit; +import org.junit.Assert; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + import java.io.FileInputStream; import java.io.IOException; import java.io.InputStream; @@ -52,11 +56,8 @@ import java.util.Arrays; import java.util.Collection; import java.util.function.Predicate; -import kotlin.Unit; -import org.junit.Assert; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; @RunWith(Parameterized.class) public class LDGAbstractorCheckingTest { @@ -80,7 +81,6 @@ public static Collection data() { {"counter6to7.xsts", "x_eq_7.prop", "", true}, {"counter6to7.xsts", "x_eq_6.prop", "", true}, {"infinitehavoc.xsts", "x_eq_7.prop", "", true}, - {"colors.xsts", "currentColor_eq_Green.prop", "", true}, {"counter5.xsts", "x_eq_5.prop", "", true}, {"forever5.xsts", "x_eq_5.prop", "", true}, {"counter6to7.xsts", "x_eq_5.prop", "", false}, diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/BuchiBuilder.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/BuchiBuilder.kt index d4e5df5b8a..3820cc1876 100644 --- a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/BuchiBuilder.kt +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/BuchiBuilder.kt @@ -21,12 +21,12 @@ import hu.bme.mit.theta.core.stmt.Stmts import hu.bme.mit.theta.core.type.Expr import hu.bme.mit.theta.core.type.booltype.BoolExprs import hu.bme.mit.theta.core.type.booltype.BoolType +import java.util.function.Consumer import jhoafparser.ast.AtomAcceptance import jhoafparser.ast.AtomLabel import jhoafparser.ast.BooleanExpression import jhoafparser.consumer.HOAConsumer import jhoafparser.consumer.HOAConsumerException -import java.util.function.Consumer class BuchiBuilder internal constructor( diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt index d00d91bf49..2e409bce24 100644 --- a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt @@ -33,12 +33,12 @@ import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.core.type.booltype.BoolExprs.True import hu.bme.mit.theta.solver.Solver import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import java.io.FileInputStream import junit.framework.TestCase.fail import org.junit.Assert import org.junit.Test import org.junit.runner.RunWith import org.junit.runners.Parameterized -import java.io.FileInputStream @RunWith(Parameterized::class) class LtlCheckTestWithCfaExpl( diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt index 8c95a84921..8244c83e4f 100644 --- a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt @@ -30,12 +30,12 @@ import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.core.type.booltype.BoolExprs.True import hu.bme.mit.theta.solver.Solver import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import java.io.FileInputStream import junit.framework.TestCase.fail import org.junit.Assert import org.junit.Test import org.junit.runner.RunWith import org.junit.runners.Parameterized -import java.io.FileInputStream @RunWith(Parameterized::class) class LtlCheckTestWithCfaPred( diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt index f55c04544b..f651e9ac88 100644 --- a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt @@ -32,12 +32,12 @@ import hu.bme.mit.theta.xsts.analysis.XstsState import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder import hu.bme.mit.theta.xsts.dsl.XstsDslManager import hu.bme.mit.theta.xsts.passes.XstsNormalizerPass +import java.io.FileInputStream import junit.framework.TestCase.fail import org.junit.Assert import org.junit.Test import org.junit.runner.RunWith import org.junit.runners.Parameterized -import java.io.FileInputStream @RunWith(Parameterized::class) class LtlCheckTestWithXstsExpl( diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt index 7ce8759ee6..ba843ce3da 100644 --- a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt @@ -29,12 +29,12 @@ import hu.bme.mit.theta.xsts.XSTS import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder import hu.bme.mit.theta.xsts.dsl.XstsDslManager import hu.bme.mit.theta.xsts.passes.XstsNormalizerPass +import java.io.FileInputStream import junit.framework.TestCase.fail import org.junit.Assert import org.junit.Test import org.junit.runner.RunWith import org.junit.runners.Parameterized -import java.io.FileInputStream @RunWith(Parameterized::class) class LtlCheckTestWithXstsPred(