From fd6511b977e1ecbaebd8e5e0a58259ae6637915a 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. --- .../java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java | 5 ++--- .../hu/bme/mit/theta/common/cfa/buchi/hoa/BuchiBuilder.kt | 2 +- .../hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt | 2 +- .../hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt | 2 +- .../hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt | 2 +- .../hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt | 2 +- 6 files changed, 7 insertions(+), 8 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/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(