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.
ftsrg · Nov 20, 2024 · fd6511b · fd6511b
1 parent dfd9455
commit fd6511b
Show file tree

Hide file tree

Showing 6 changed files with 7 additions and 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
@@ -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<UnitState, UnitPrec> {
 
     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
@@ -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/...rojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt b/...rojects/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/...rojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt b/...rojects/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/...ojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt b/...ojects/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/...ojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt b/...ojects/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(