diff --git a/settings.gradle.kts b/settings.gradle.kts
index 5421f34ea0..aea8ecaaba 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -20,6 +20,7 @@ include(
     "common/common",
     "common/core",
     "common/grammar",
+    "common/ltl",
     "common/multi-tests",
 
     "frontends/c-frontend",
diff --git a/subprojects/common/ltl/build.gradle.kts b/subprojects/common/ltl/build.gradle.kts
new file mode 100644
index 0000000000..a034fc64a2
--- /dev/null
+++ b/subprojects/common/ltl/build.gradle.kts
@@ -0,0 +1,31 @@
+/*
+ *  Copyright 2023 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("java-common")
+    id("kotlin-common")
+}
+
+dependencies {
+    implementation(project(":theta-common"))
+    implementation(project(":theta-core"))
+    implementation(project(":theta-solver"))
+    implementation(project(":theta-analysis"))
+    implementation(project(mapOf("path" to ":theta-cfa")))
+    implementation(project(mapOf("path" to ":theta-cfa-analysis")))
+    testImplementation(project(":theta-solver-z3-legacy"))
+    testImplementation(project(mapOf("path" to ":theta-xsts-analysis")))
+    testImplementation(project(mapOf("path" to ":theta-xsts")))
+}
diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/BuchiUtils.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/BuchiUtils.kt
new file mode 100644
index 0000000000..0b725c3d02
--- /dev/null
+++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/BuchiUtils.kt
@@ -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())
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt
new file mode 100644
index 0000000000..da7112c8d8
--- /dev/null
+++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt
@@ -0,0 +1,104 @@
+/*
+ *  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.*
+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.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.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
+) : SafetyChecker<LDG<ExprMultiState<ControlS, CfaState<UnitState>, DataS>, StmtMultiAction<A, CfaAction>>, LDGTrace<ExprMultiState<ControlS, CfaState<UnitState>, DataS>, StmtMultiAction<A, CfaAction>>, MultiPrec<P, CfaPrec<DataP>, DataP>> {
+    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>>>
+
+    init {
+        val 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(NextSideFunctions.Alternating(), 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)
+        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))
+    }
+}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfa.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfa.kt
new file mode 100644
index 0000000000..1fca597b8d
--- /dev/null
+++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfa.kt
@@ -0,0 +1,107 @@
+package hu.bme.mit.theta.common.ltl
+//
+//import hu.bme.mit.theta.analysis.algorithm.loopchecker.RefinerStrategy
+//import hu.bme.mit.theta.analysis.algorithm.loopchecker.SearchStrategy
+//import hu.bme.mit.theta.analysis.expl.ExplAnalysis
+//import hu.bme.mit.theta.analysis.expl.ExplPrec
+//import hu.bme.mit.theta.analysis.expl.ExplState
+//import hu.bme.mit.theta.analysis.expl.ItpRefToExplPrec
+//import hu.bme.mit.theta.analysis.unit.UnitState
+//import hu.bme.mit.theta.cfa.CFA
+//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.lts.CfaLts
+//import hu.bme.mit.theta.cfa.analysis.lts.CfaSbeLts
+//import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec
+//import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec
+//import hu.bme.mit.theta.cfa.dsl.CfaDslManager
+//import hu.bme.mit.theta.common.logging.ConsoleLogger
+//import hu.bme.mit.theta.common.logging.Logger
+//import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
+//import hu.bme.mit.theta.solver.ItpSolver
+//import hu.bme.mit.theta.solver.Solver
+//import hu.bme.mit.theta.solver.z3.Z3SolverFactory
+//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 LtlCheckTestWithCfa(
+//    private val cfaName: String,
+//    private val ltlExpr: String,
+//    private val result: Boolean
+//) {
+//
+//    private val itpSolver: ItpSolver = Z3SolverFactory.getInstance().createItpSolver()
+//    private val abstractionSolver: Solver = Z3SolverFactory.getInstance().createSolver()
+//    private val logger: Logger = ConsoleLogger(Logger.Level.VERBOSE)
+//
+//    companion object {
+//        @JvmStatic
+//        @Parameterized.Parameters
+//        fun data() = listOf(
+//            arrayOf("counter2inf", "G(x=1)", false),
+//            arrayOf("counter2inf", "G(x=2)", false),
+//            arrayOf("counter2inf", "F G(x=2)", true),
+//            arrayOf("counter2inf", "F(x=1)", true),
+//            arrayOf("counter2inf", "F(x=3)", false),
+//        )
+//    }
+//
+//    @Test
+//    fun test() {
+//        itpSolver.reset()
+//        abstractionSolver.reset()
+//        var cfaI: CFA?
+//        FileInputStream(String.format("src/test/resources/cfa/%s.cfa", cfaName)).use { inputStream ->
+//            cfaI = CfaDslManager.createCfa(inputStream)
+//        }
+//        if (cfaI == null)
+//            fail("Couldn't read cfa $cfaName")
+//        val cfa = cfaI!!
+//        val dataAnalysis = ExplAnalysis.create(
+//            abstractionSolver,
+//            True()
+//        )
+//        val analysis = CfaAnalysis.create(cfa.initLoc, dataAnalysis)
+//        val lts: CfaLts = CfaSbeLts.getInstance()
+//        val refToPrec = RefutationToGlobalCfaPrec(ItpRefToExplPrec(), cfa.initLoc)
+//        val initFunc = { _: CfaPrec<ExplPrec> -> listOf<CfaState<UnitState>>(CfaState.of(cfa.initLoc, UnitState.getInstance())) }
+//        val variables = cfa.vars
+//        val dataInitPrec = ExplPrec.of(variables)
+//        val initPrec:CfaPrec<ExplPrec> = GlobalCfaPrec.create(dataInitPrec)
+//        val combineStates = { c: CfaState<UnitState>, d: ExplState -> CfaState.of(c.loc, d) }
+//        val stripState = { c: CfaState<ExplState> -> CfaState.of(c.loc, UnitState.getInstance()) }
+//        val extractFromState = { c: CfaState<ExplState> -> c.state }
+//        val stripPrec = { p: CfaPrec<ExplPrec> -> p }
+//
+//        val checkResult = LtlCheck.check(
+//            analysis,
+//            lts,
+//            refToPrec,
+//            dataAnalysis,
+//            ItpRefToExplPrec(),
+//            initFunc,
+//            initPrec,
+//            True(),
+//            dataInitPrec,
+//            variables,
+//            combineStates,
+//            stripState,
+//            extractFromState,
+//            stripPrec,
+//            ltlExpr,
+//            itpSolver,
+//            logger,
+//            SearchStrategy.DFS,
+//            RefinerStrategy.MILANO
+//        )
+//
+//        Assert.assertEquals(result, checkResult.isSafe)
+//    }
+//
+//}
\ No newline at end of file
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
new file mode 100644
index 0000000000..4541ccc79b
--- /dev/null
+++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt
@@ -0,0 +1,119 @@
+package hu.bme.mit.theta.common.ltl
+//
+//import hu.bme.mit.theta.analysis.algorithm.loopchecker.RefinerStrategy
+//import hu.bme.mit.theta.analysis.algorithm.loopchecker.SearchStrategy
+//import hu.bme.mit.theta.analysis.expr.ExprAction
+//import hu.bme.mit.theta.analysis.pred.*
+//import hu.bme.mit.theta.analysis.unit.UnitState
+//import hu.bme.mit.theta.cfa.CFA
+//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.lts.CfaLts
+//import hu.bme.mit.theta.cfa.analysis.lts.CfaSbeLts
+//import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec
+//import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec
+//import hu.bme.mit.theta.cfa.dsl.CfaDslManager
+//import hu.bme.mit.theta.common.logging.ConsoleLogger
+//import hu.bme.mit.theta.common.logging.Logger
+//import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
+//import hu.bme.mit.theta.solver.ItpSolver
+//import hu.bme.mit.theta.solver.Solver
+//import hu.bme.mit.theta.solver.z3.Z3SolverFactory
+//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(
+//    private val cfaName: String,
+//    private val ltlExpr: String,
+//    private val result: Boolean
+//) {
+//
+//    private val itpSolver: ItpSolver = Z3SolverFactory.getInstance().createItpSolver()
+//    private val abstractionSolver: Solver = Z3SolverFactory.getInstance().createSolver()
+//    private val logger: Logger = ConsoleLogger(Logger.Level.INFO)
+//
+//    companion object {
+//        @JvmStatic
+//        @Parameterized.Parameters
+//        fun data() = listOf(
+//                arrayOf("wave_flags", "F G(x)", false),
+//                arrayOf("wave_flags", "F G(x and y)", false),
+//                arrayOf("wave_flag", "G F(x)", true),
+//                arrayOf("wave_flag", "G(x)", false),
+//                arrayOf("wave_flag", "F G(x)", false),
+//                arrayOf("counter5inf", "G(not(x=6))", true),
+//                arrayOf("counter5inf", "G(x=1)", false),
+//                arrayOf("counter5inf", "G(x=5)", false),
+//                arrayOf("counter5inf", "F G(x=5)", true),
+//                arrayOf("counter5inf", "F(x=1)", true),
+//                arrayOf("counter5inf", "F(x=5)", true),
+//                arrayOf("wave_flags", "G F(y)", true),
+//                arrayOf("wave_flags", "F G(x)", false),
+//                arrayOf("indicator", "G (x -> y)", true),
+////                arrayOf("indicator_multiassign", "G (x -> y)", true),
+//                arrayOf("indicator", "G (x -> X (not x))", true),
+//                arrayOf("indicator", "G (y -> X (not y))", false),
+//        )
+//    }
+//
+//    @Test
+//    fun test() {
+//        itpSolver.reset()
+//        abstractionSolver.reset()
+//        var cfaI: CFA?
+//        FileInputStream(String.format("src/test/resources/cfa/%s.cfa", cfaName)).use { inputStream ->
+//            cfaI = CfaDslManager.createCfa(inputStream)
+//        }
+//        if (cfaI == null)
+//            fail("Couldn't read cfa $cfaName")
+//        val cfa = cfaI!!
+//        val dataAnalysis = PredAnalysis.create<ExprAction>(
+//            abstractionSolver,
+//            PredAbstractors.booleanSplitAbstractor(abstractionSolver),
+//            True()
+//        )
+//        val analysis = CfaAnalysis.create(cfa.initLoc, dataAnalysis)
+//        val lts: CfaLts = CfaSbeLts.getInstance()
+////        val lts: CfaLts = CfaLbeLts.of(cfa.initLoc)
+//        val refToPrec = RefutationToGlobalCfaPrec(ItpRefToPredPrec(ExprSplitters.atoms()), cfa.initLoc)
+//        val initFunc = { _: CfaPrec<PredPrec> -> listOf<CfaState<UnitState>>(CfaState.of(cfa.initLoc, UnitState.getInstance())) }
+//        val variables = cfa.vars
+//        val dataInitPrec = PredPrec.of()
+//        val initPrec:CfaPrec<PredPrec> = GlobalCfaPrec.create(dataInitPrec)
+//        val combineStates = { c: CfaState<UnitState>, d: PredState -> CfaState.of(c.loc, d) }
+//        val stripState = { c: CfaState<PredState> -> CfaState.of(c.loc, UnitState.getInstance()) }
+//        val extractFromState = { c: CfaState<PredState> -> c.state }
+//        val stripPrec = { p: CfaPrec<PredPrec> -> p }
+//
+//        val checkResult = LtlCheck.check(
+//            analysis,
+//            lts,
+//            refToPrec,
+//            dataAnalysis,
+//            ItpRefToPredPrec(ExprSplitters.atoms()),
+//            initFunc,
+//            initPrec,
+//            True(),
+//            dataInitPrec,
+//            variables,
+//            combineStates,
+//            stripState,
+//            extractFromState,
+//            stripPrec,
+//            ltlExpr,
+//            itpSolver,
+//            logger,
+//            SearchStrategy.DFS,
+//            RefinerStrategy.MILANO
+//        )
+//
+//        Assert.assertEquals(result, checkResult.isSafe)
+//    }
+//
+//}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXsts.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXsts.kt
new file mode 100644
index 0000000000..ba79e4ef07
--- /dev/null
+++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXsts.kt
@@ -0,0 +1,85 @@
+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.LDGTraceCheckerStrategy
+import hu.bme.mit.theta.analysis.expl.ExplAnalysis
+import hu.bme.mit.theta.analysis.expl.ExplPrec
+import hu.bme.mit.theta.analysis.expl.ExplState
+import hu.bme.mit.theta.analysis.expl.ItpRefToExplPrec
+import hu.bme.mit.theta.analysis.multi.MultiAnalysisSide
+import hu.bme.mit.theta.analysis.multi.MultiPrec
+import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer
+import hu.bme.mit.theta.analysis.unit.UnitState
+import hu.bme.mit.theta.cfa.analysis.CfaPrec
+import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec
+import hu.bme.mit.theta.common.logging.ConsoleLogger
+import hu.bme.mit.theta.common.logging.Logger
+import hu.bme.mit.theta.solver.Solver
+import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory
+import hu.bme.mit.theta.xsts.XSTS
+import hu.bme.mit.theta.xsts.analysis.*
+import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder
+import hu.bme.mit.theta.xsts.dsl.XstsDslManager
+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 LtlCheckTestWithXsts(
+    private val xstsName: String,
+    private val ltlExpr: String,
+    private val result: Boolean
+) {
+
+    private val logger: Logger = ConsoleLogger(Logger.Level.VERBOSE)
+
+    companion object {
+        @JvmStatic
+        @Parameterized.Parameters
+        fun data() = listOf(
+            arrayOf("counter3inf", "F G(x=3)", true),
+            arrayOf("counter3inf", "F(x=2)", true),
+            arrayOf("counter3inf", "G(x<4)", true),
+            arrayOf("counter3inf", "G(x=1)", false),
+            arrayOf("counter6to7", "G(x=1)", false),
+            arrayOf("counter6to7", "G(x=7)", false),
+            arrayOf("counter6to7", "G F(x=7)", true),
+        )
+    }
+
+    @Test
+    fun test() {
+        var xstsI: XSTS?
+        FileInputStream("src/test/resources/xsts/$xstsName.xsts")
+            .use { inputStream ->
+            xstsI = XstsDslManager.createXsts(inputStream)
+        }
+        if (xstsI == null)
+            fail("Couldn't read xsts $xstsName")
+        val xsts = xstsI!!
+        val solverFactory = Z3LegacySolverFactory.getInstance()
+        val configBuilder = XstsConfigBuilder(XstsConfigBuilder.Domain.EXPL, XstsConfigBuilder.Refinement.SEQ_ITP, solverFactory, solverFactory).initPrec(XstsConfigBuilder.InitPrec.EMPTY).ExplStrategy(xsts)
+        val initPrec = configBuilder.initPrec
+
+        val checker = LtlChecker(
+            configBuilder.multiSide,
+            configBuilder.lts,
+            configBuilder.itpRefToPrec,
+            configBuilder.itpRefToPrec,
+            configBuilder.dataAnalysis,
+            xsts.vars,
+            ltlExpr,
+            solverFactory,
+            logger,
+            LoopcheckerSearchStrategy.GDFS,
+            LDGTraceCheckerStrategy.MILANO
+        )
+        val checkResult = checker.check(initPrec, initPrec)
+
+        Assert.assertEquals(result, checkResult.isSafe)
+    }
+
+}
\ No newline at end of file
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
new file mode 100644
index 0000000000..91077760f8
--- /dev/null
+++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt
@@ -0,0 +1,106 @@
+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.LDGTraceCheckerStrategy
+import hu.bme.mit.theta.common.logging.ConsoleLogger
+import hu.bme.mit.theta.common.logging.Logger
+import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory
+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 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(
+    private val xstsName: String,
+    private val ltlExpr: String,
+    private val result: Boolean,
+    private val searchStrategy: LoopcheckerSearchStrategy,
+    private val refinerStrategy: LDGTraceCheckerStrategy,
+) {
+
+    private val logger: Logger = ConsoleLogger(Logger.Level.INFO)
+
+    companion object {
+        private fun data() = listOf(
+            arrayOf("simple_types", "F G(color = Colors.Red)", false),
+            arrayOf("counter3inf", "F G(x=3)", true),
+            arrayOf("counter3inf", "F(x=2)", true),
+            arrayOf("counter3inf", "G(x<4)", true),
+            arrayOf("counter3inf", "G(x=1)", false),
+            arrayOf("counter6to7", "G(x=1)", false),
+            arrayOf("counter6to7", "G(x=7)", false),
+            arrayOf("counter6to7", "G F(x=7)", true),
+//            arrayOf("counter50", "G(x<49)", false),
+            arrayOf("trafficlight_v2", "G(LightCommands_displayRed -> X(not LightCommands_displayGreen))", true),
+            arrayOf("trafficlight_v2", "G((normal = Normal.Red and (not PoliceInterrupt_police) and Control_toggle) -> X(normal = Normal.Green))", true),
+            arrayOf("trafficlight_v2", "G(PoliceInterrupt_police -> F(LightCommands_displayYellow))", true),
+            arrayOf("forever5", "G(x=5)", true),
+            arrayOf("forever5", "F(x=6)", false),
+            arrayOf("randomincreasingeven", "not F(x=1)", true),
+            arrayOf("randomincreasingeven", "F(x>10)", true),
+            arrayOf("randomincreasingeven", "G(x>=0)", true),
+            arrayOf("simple_color", "G(envColor = Colors.Green -> X(modelColor = Colors.Blue))", true),
+            arrayOf("simple_color", "G(envColor = Colors.Green -> X(modelColor = Colors.Green))", false),
+            arrayOf("simple_color", "F G(envColor = modelColor)", false),
+            arrayOf("weather", "G F(isClever and isWet)", false),
+            arrayOf("weather", "F G(not isWet)", true),
+            arrayOf("weather", "G(time = TimeOfDay.Noon -> X(time = TimeOfDay.Noon or time = TimeOfDay.Afternoon))", true),
+//            arrayOf("weather", "F G(weather = Weather.Foggy -> (clothing = Clothing.Nothing or clothing = Clothing.Warm))", true),
+//            arrayOf("weather_noinit", "G F(isClever and isWet)", false),
+//            arrayOf("weather_noinit", "F G(not isWet)", true),
+//            arrayOf("weather_noinit", "G(time = TimeOfDay.Noon -> X(time = TimeOfDay.Noon or time = TimeOfDay.Afternoon))", true),
+//            arrayOf("weather_noinit", "F G(weather = Weather.Foggy -> (clothing = Clothing.Nothing or clothing = Clothing.Warm))", true),
+        )
+
+        @JvmStatic
+        @Parameterized.Parameters(name = "{3}-{4}: {0}")
+        fun params() =
+        listOf(LoopcheckerSearchStrategy.GDFS, /*LoopcheckerSearchStrategy.NDFS*/).flatMap { search ->
+            LDGTraceCheckerStrategy.entries.flatMap { ref ->
+                data().map {
+                    arrayOf(*it, search, ref)
+                }
+            }
+        }
+    }
+
+    @Test
+    fun test() {
+        var xstsI: XSTS?
+        FileInputStream("src/test/resources/xsts/$xstsName.xsts")
+            .use { inputStream ->
+                xstsI = XstsDslManager.createXsts(inputStream)
+            }
+        if (xstsI == null)
+            fail("Couldn't read xsts $xstsName")
+        val xsts = xstsI!!
+        val solverFactory = Z3LegacySolverFactory.getInstance()
+        val configBuilder = XstsConfigBuilder(XstsConfigBuilder.Domain.PRED_SPLIT, XstsConfigBuilder.Refinement.SEQ_ITP, solverFactory, solverFactory).initPrec(
+            XstsConfigBuilder.InitPrec.EMPTY).predSplit(XstsConfigBuilder.PredSplit.ATOMS).PredStrategy(xsts)
+        val initPrec = configBuilder.initPrec
+
+        val checker = LtlChecker(
+            configBuilder.multiSide,
+            configBuilder.lts,
+            configBuilder.itpRefToPrec,
+            configBuilder.itpRefToPrec,
+            configBuilder.dataAnalysis,
+            xsts.vars,
+            ltlExpr,
+            solverFactory,
+            logger,
+            searchStrategy,
+            refinerStrategy,
+        )
+        val checkResult = checker.check(initPrec, initPrec)
+
+        Assert.assertEquals(result, checkResult.isSafe)
+    }
+
+}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/cfa/counter2inf.cfa b/subprojects/common/ltl/src/test/resources/cfa/counter2inf.cfa
new file mode 100644
index 0000000000..81e578cc5d
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/cfa/counter2inf.cfa
@@ -0,0 +1,12 @@
+main process cfa {
+	var x : int
+
+	init loc I
+	loc L0
+	loc L1
+
+    I -> L0 { x := 0 }
+	L0 -> L1 { assume x < 2 }
+    L1 -> L0 { x := x + 1 }
+    L0 -> L0 { assume x = 2 }
+}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/cfa/counter5inf.cfa b/subprojects/common/ltl/src/test/resources/cfa/counter5inf.cfa
new file mode 100644
index 0000000000..6fb102aaf8
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/cfa/counter5inf.cfa
@@ -0,0 +1,12 @@
+main process cfa {
+	var x : int
+
+	init loc I
+	loc L0
+	loc L1
+
+    I -> L0 { x := 0 }
+	L0 -> L1 { assume x < 5 }
+    L1 -> L0 { x := x + 1 }
+    L0 -> L0 { assume x = 5 }
+}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/cfa/indicator.cfa b/subprojects/common/ltl/src/test/resources/cfa/indicator.cfa
new file mode 100644
index 0000000000..c8a7062768
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/cfa/indicator.cfa
@@ -0,0 +1,14 @@
+main process cfa {
+	var x : bool
+	var y : bool
+
+	loc L0
+	loc L1
+	init loc L2
+	loc L3
+
+    L0 -> L1 { y := true }
+    L1 -> L2 { x := true }
+    L2 -> L3 { x := false }
+    L3 -> L0 { y := false }
+}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/cfa/indicator_multiassign.cfa b/subprojects/common/ltl/src/test/resources/cfa/indicator_multiassign.cfa
new file mode 100644
index 0000000000..8330500158
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/cfa/indicator_multiassign.cfa
@@ -0,0 +1,12 @@
+main process cfa {
+	var x : bool
+	var y : bool
+
+	loc L0
+	loc L1
+	init loc L2
+
+    L0 -> L1 { y := true }
+    L1 -> L2 { x := true }
+    L2 -> L0 { y := false x := false }
+}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/cfa/wave_flag.cfa b/subprojects/common/ltl/src/test/resources/cfa/wave_flag.cfa
new file mode 100644
index 0000000000..77322ac49d
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/cfa/wave_flag.cfa
@@ -0,0 +1,9 @@
+main process cfa {
+	var x : bool
+
+	init loc L0
+	loc L1
+
+    L0 -> L1 { x := true }
+    L1 -> L0 { x := false }
+}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/cfa/wave_flags.cfa b/subprojects/common/ltl/src/test/resources/cfa/wave_flags.cfa
new file mode 100644
index 0000000000..dc192bb7e5
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/cfa/wave_flags.cfa
@@ -0,0 +1,18 @@
+main process cfa {
+	var x : bool
+	var y : bool
+
+	init loc I0
+	loc I1
+	loc L0
+	loc L1
+	loc L2
+	loc L3
+
+    I0 -> I1 { x := false }
+    I1 -> L0 { y := false }
+    L0 -> L1 { y := true }
+    L1 -> L2 { y := false x := true }
+    L2 -> L3 { y := true }
+    L3 -> L0 { y := false x := false }
+}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/xsts/counter3inf.xsts b/subprojects/common/ltl/src/test/resources/xsts/counter3inf.xsts
new file mode 100644
index 0000000000..af2080f290
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/xsts/counter3inf.xsts
@@ -0,0 +1,12 @@
+var x: integer = 0
+
+trans {
+    assume x<3;
+    x:=x+1;
+} or {
+    assume x>=3;
+}
+
+init {}
+env {}
+prop{true}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/xsts/counter50.xsts b/subprojects/common/ltl/src/test/resources/xsts/counter50.xsts
new file mode 100644
index 0000000000..ffed019bc4
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/xsts/counter50.xsts
@@ -0,0 +1,16 @@
+ctrl var x: integer = 0
+
+trans {
+    choice {
+        assume x<50;
+        x:=x+1;
+    } or {
+        assume x == 50;
+    }
+}
+
+init {}
+
+env {}
+
+prop{true}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/xsts/counter6to7.xsts b/subprojects/common/ltl/src/test/resources/xsts/counter6to7.xsts
new file mode 100644
index 0000000000..f331be2ee6
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/xsts/counter6to7.xsts
@@ -0,0 +1,13 @@
+var x: integer = 0
+
+trans {
+    assume x<=6;
+    x:=x+1;
+} or {
+    assume x==7;
+    x:=x-1;
+}
+
+init {}
+env {}
+prop{true}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/xsts/forever5.xsts b/subprojects/common/ltl/src/test/resources/xsts/forever5.xsts
new file mode 100644
index 0000000000..975cfc8f93
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/xsts/forever5.xsts
@@ -0,0 +1,9 @@
+var x: integer = 5
+
+trans {
+    x:=x;
+}
+
+init {}
+env {}
+prop{true}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/xsts/randomincreasingeven.xsts b/subprojects/common/ltl/src/test/resources/xsts/randomincreasingeven.xsts
new file mode 100644
index 0000000000..d6f9c53796
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/xsts/randomincreasingeven.xsts
@@ -0,0 +1,14 @@
+var x: integer = 0
+var y: integer = 0
+
+trans {
+    if (y < 0) y := -y;
+    if (y == 0) y := 1;
+    if (y % 2 == 1) y := y + 1;
+    x:= x + y;
+}
+init {}
+env {
+    havoc y;
+}
+prop{true}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/xsts/simple_color.xsts b/subprojects/common/ltl/src/test/resources/xsts/simple_color.xsts
new file mode 100644
index 0000000000..6443992dff
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/xsts/simple_color.xsts
@@ -0,0 +1,24 @@
+type Colors : { Red, Green, Blue}
+var envColor : Colors = Red
+var modelColor : Colors = Red
+
+trans {
+    choice {
+        assume envColor == Red;
+        modelColor := Green;
+    } or {
+        assume envColor == Green;
+        modelColor := Blue;
+    } or {
+        assume envColor == Blue;
+        modelColor := Red;
+    }
+}
+
+init{}
+
+env {
+    havoc envColor;
+}
+
+prop{true}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/xsts/simple_types.xsts b/subprojects/common/ltl/src/test/resources/xsts/simple_types.xsts
new file mode 100644
index 0000000000..3f1dda287f
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/xsts/simple_types.xsts
@@ -0,0 +1,16 @@
+type Abc : { A, B, C, D}
+type Colors : { Red, Green, Blue}
+var letter : Abc = A
+var color : Colors = Red
+
+trans {
+    havoc letter;
+}
+
+init{}
+
+env {
+    havoc color;
+}
+
+prop{true}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/xsts/trafficlight_v2.xsts b/subprojects/common/ltl/src/test/resources/xsts/trafficlight_v2.xsts
new file mode 100644
index 0000000000..e2f50cef51
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/xsts/trafficlight_v2.xsts
@@ -0,0 +1,169 @@
+type Main_region : { __Inactive__, Interrupted, Normal}
+type Normal : { __Inactive__, Green, Red, Yellow}
+type Interrupted : { __Inactive__, Black, BlinkingYellow}
+var PoliceInterrupt_police : boolean = false
+var LightCommands_displayRed : boolean = false
+var Control_toggle : boolean = false
+var LightCommands_displayYellow : boolean = false
+var LightCommands_displayNone : boolean = false
+var LightCommands_displayGreen : boolean = false
+ctrl var main_region : Main_region = __Inactive__
+ctrl var normal : Normal = __Inactive__
+ctrl var interrupted : Interrupted = __Inactive__
+ctrl var BlackTimeout3 : integer = 500
+ctrl var BlinkingYellowTimeout4 : integer = 500
+var c : boolean = true
+var b : integer = 0
+var asd : integer = 0
+var a : boolean = false
+
+trans {
+	choice {
+		assume ((!(((main_region == Interrupted) && (PoliceInterrupt_police == true)))) && (((main_region == Interrupted) && (interrupted == BlinkingYellow)) && (500 <= BlinkingYellowTimeout4)));
+		assume (interrupted == BlinkingYellow);
+		interrupted := Black;
+		assume (interrupted == Black);
+		BlackTimeout3 := 0;
+		LightCommands_displayNone := true;
+	} or {
+		assume ((!(((main_region == Interrupted) && (PoliceInterrupt_police == true)))) && (((main_region == Interrupted) && (interrupted == Black)) && (500 <= BlackTimeout3)));
+		assume (interrupted == Black);
+		interrupted := BlinkingYellow;
+		assume (interrupted == BlinkingYellow);
+		BlinkingYellowTimeout4 := 0;
+		LightCommands_displayYellow := true;
+	} or {
+		assume ((!(((main_region == Normal) && (PoliceInterrupt_police == true)))) && (((main_region == Normal) && (normal == Green)) && (Control_toggle == true)));
+		assume (normal == Green);
+		b := 4;
+		normal := Yellow;
+		assume (normal == Yellow);
+		LightCommands_displayYellow := true;
+	} or {
+		assume ((!(((main_region == Normal) && (PoliceInterrupt_police == true)))) && (((main_region == Normal) && (normal == Red)) && (Control_toggle == true)));
+		assume (normal == Red);
+		a := true;
+		normal := Green;
+		assume (normal == Green);
+		LightCommands_displayGreen := true;
+	} or {
+		assume ((!(((main_region == Normal) && (PoliceInterrupt_police == true)))) && (((main_region == Normal) && (normal == Yellow)) && (Control_toggle == true)));
+		assume (normal == Yellow);
+		normal := Red;
+		assume (normal == Red);
+		LightCommands_displayRed := true;
+	} or {
+		assume (((main_region == Interrupted) && (PoliceInterrupt_police == true)));
+		assume (main_region == Interrupted);
+		interrupted := __Inactive__;
+		main_region := Normal;
+		choice {
+			assume (normal == __Inactive__);
+			normal := Red;
+		} or {
+			assume !((normal == __Inactive__));
+		}
+		assume (main_region == Normal);
+		choice {
+			assume (normal == Green);
+			LightCommands_displayGreen := true;
+		} or {
+			assume (normal == Red);
+			LightCommands_displayRed := true;
+		} or {
+			assume (normal == Yellow);
+			LightCommands_displayYellow := true;
+		}
+	} or {
+		assume (((main_region == Normal) && (PoliceInterrupt_police == true)));
+		assume (main_region == Normal);
+		choice {
+			assume (normal == Green);
+		} or {
+			assume (normal == Red);
+			a := true;
+		} or {
+			assume (normal == Yellow);
+		}
+		asd := 321;
+		main_region := Interrupted;
+		interrupted := BlinkingYellow;
+		assume (main_region == Interrupted);
+		choice {
+			assume (interrupted == Black);
+			BlackTimeout3 := 0;
+			LightCommands_displayNone := true;
+		} or {
+			assume (interrupted == BlinkingYellow);
+			BlinkingYellowTimeout4 := 0;
+			LightCommands_displayYellow := true;
+		}
+	}
+}
+
+init {
+	c := true;
+	b := 0;
+	a := false;
+	asd := 0;
+	BlackTimeout3 := 500;
+	BlinkingYellowTimeout4 := 500;
+	normal := __Inactive__;
+	interrupted := __Inactive__;
+	PoliceInterrupt_police := false;
+	Control_toggle := false;
+	LightCommands_displayRed := false;
+	LightCommands_displayYellow := false;
+	LightCommands_displayNone := false;
+	LightCommands_displayGreen := false;
+	main_region := Normal;
+	choice {
+		assume (normal == __Inactive__);
+		normal := Red;
+	} or {
+		assume !((normal == __Inactive__));
+	}
+	choice {
+		assume (main_region == Interrupted);
+		choice {
+			assume (interrupted == Black);
+			BlackTimeout3 := 0;
+			LightCommands_displayNone := true;
+		} or {
+			assume (interrupted == BlinkingYellow);
+			BlinkingYellowTimeout4 := 0;
+			LightCommands_displayYellow := true;
+		}
+	} or {
+		assume (main_region == Normal);
+		choice {
+			assume (normal == Green);
+			LightCommands_displayGreen := true;
+		} or {
+			assume (normal == Red);
+			LightCommands_displayRed := true;
+		} or {
+			assume (normal == Yellow);
+			LightCommands_displayYellow := true;
+		}
+	}
+}
+
+env {
+	choice {
+		PoliceInterrupt_police := true;
+	} or {
+		PoliceInterrupt_police := false;
+	}
+	choice {
+		Control_toggle := true;
+	} or {
+		Control_toggle := false;
+	}
+	LightCommands_displayYellow := false;
+	LightCommands_displayRed := false;
+	LightCommands_displayNone := false;
+	LightCommands_displayGreen := false;
+}
+
+prop{true}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/xsts/weather.xsts b/subprojects/common/ltl/src/test/resources/xsts/weather.xsts
new file mode 100644
index 0000000000..b5d9da75dc
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/xsts/weather.xsts
@@ -0,0 +1,104 @@
+type Weather : { Sunny , Cloudy , Rainy, Foggy }
+type TimeOfDay : { Morning , Noon, Afternoon, Night }
+type Clothing : { Nothing, Shorts, Warm, Waterproof }
+var isWet : boolean = false
+var looksOut : boolean = false
+var isClever : boolean = false
+var weather : Weather = Sunny
+var time : TimeOfDay
+var clothing  : Clothing = Nothing
+
+trans {
+    choice {
+        assume time == Morning;
+        choice {
+            assume (looksOut == false && isClever == false);
+            havoc clothing;
+        } or {
+            assume (looksOut == true && isClever == false);
+            choice {
+                assume weather == Sunny;
+                clothing := Shorts;
+            } or {
+                assume (weather == Cloudy || weather == Foggy);
+                clothing := Warm;
+            } or {
+                assume weather == Rainy;
+                clothing := Waterproof;
+            }
+        } or {
+            assume (isClever == true);
+            choice {
+                assume weather == Sunny;
+                clothing := Shorts;
+            } or {
+                assume (weather == Cloudy || weather == Rainy);
+                clothing := Waterproof;
+            } or {
+                assume weather == Foggy;
+                clothing := Warm;
+            }
+        }
+    } or {
+        assume time == Noon;
+        if (isWet == true) looksOut := true;
+    } or {
+        assume time == Afternoon;
+    } or {
+        assume time == Night;
+        if (isWet == true) isClever := true;
+        clothing := Nothing;
+    }
+}
+
+init {
+    havoc weather;
+    time := Morning;
+}
+
+env {
+        if (clothing != Waterproof && weather == Rainy) isWet := true;
+        if (time == Noon || time == Night) isWet := false;
+        choice {
+            assume time == Morning;
+            time := Noon;
+        } or {
+            assume time == Noon;
+            time := Afternoon;
+        } or {
+            assume time == Afternoon;
+            time := Night;
+        } or {
+            assume time == Night;
+            time := Morning;
+        }
+
+        choice {
+            assume time != Noon;
+            choice {
+                assume (weather == Sunny || weather == Cloudy || weather == Foggy);
+                choice {
+                    weather := Cloudy;
+                } or {
+                    weather := Sunny;
+                } or {
+                    assume weather == Cloudy;
+                    weather := Rainy;
+                }
+            } or {
+                assume (weather == Rainy);
+                choice {
+                    weather := Rainy;
+                } or {
+                    weather := Sunny;
+                }
+            } or {
+                assume time == Morning;
+                weather := Foggy;
+            }
+        } or {
+            assume time == Noon;
+        }
+
+}
+prop {true}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/xsts/weather_noinit.xsts b/subprojects/common/ltl/src/test/resources/xsts/weather_noinit.xsts
new file mode 100644
index 0000000000..78f5efe332
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/xsts/weather_noinit.xsts
@@ -0,0 +1,106 @@
+type Weather : { Sunny , Cloudy , Rainy, Foggy }
+type TimeOfDay : { __init__, Morning , Noon, Afternoon, Night }
+type Clothing : { Nothing, Shorts, Warm, Waterproof }
+var isWet : boolean = false
+var looksOut : boolean = false
+var isClever : boolean = false
+var weather : Weather = Sunny
+var time : TimeOfDay = __init__
+var clothing  : Clothing = Nothing
+
+trans {
+    choice {
+        assume time == Morning;
+        choice {
+            assume (looksOut == false && isClever == false);
+            havoc clothing;
+        } or {
+            assume (looksOut == true && isClever == false);
+            choice {
+                assume weather == Sunny;
+                clothing := Shorts;
+            } or {
+                assume (weather == Cloudy || weather == Foggy);
+                clothing := Warm;
+            } or {
+                assume weather == Rainy;
+                clothing := Waterproof;
+            }
+        } or {
+            assume (isClever == true);
+            choice {
+                assume weather == Sunny;
+                clothing := Shorts;
+            } or {
+                assume (weather == Cloudy || weather == Rainy);
+                clothing := Waterproof;
+            } or {
+                assume weather == Foggy;
+                clothing := Warm;
+            }
+        }
+    } or {
+        assume time == Noon;
+        if (isWet == true) looksOut := true;
+    } or {
+        assume time == Afternoon;
+    } or {
+        assume time == Night;
+        if (isWet == true) isClever := true;
+        clothing := Nothing;
+    }
+}
+
+init { }
+
+env {
+    choice {
+        assume time == __init__;
+        time := Morning;
+    } or {
+        assume time != __init__;
+        if (clothing != Waterproof && weather == Rainy) isWet := true;
+        if (time == Noon || time == Night) isWet := false;
+        choice {
+            assume time == Morning;
+            time := Noon;
+        } or {
+            assume time == Noon;
+            time := Afternoon;
+        } or {
+            assume time == Afternoon;
+            time := Night;
+        } or {
+            assume time == Night;
+            time := Morning;
+        }
+
+        choice {
+            assume time != Noon;
+            choice {
+                assume (weather == Sunny || weather == Cloudy || weather == Foggy);
+                choice {
+                    weather := Cloudy;
+                } or {
+                    weather := Sunny;
+                } or {
+                    assume weather == Cloudy;
+                    weather := Rainy;
+                }
+            } or {
+                assume (weather == Rainy);
+                choice {
+                    weather := Rainy;
+                } or {
+                    weather := Sunny;
+                }
+            } or {
+                assume time == Morning;
+                weather := Foggy;
+            }
+        } or {
+            assume time == Noon;
+        }
+    }
+}
+prop{true}
\ No newline at end of file
diff --git a/subprojects/common/ltl/src/test/resources/xsts/weather_withprops.xsts b/subprojects/common/ltl/src/test/resources/xsts/weather_withprops.xsts
new file mode 100644
index 0000000000..4cdde5291a
--- /dev/null
+++ b/subprojects/common/ltl/src/test/resources/xsts/weather_withprops.xsts
@@ -0,0 +1,105 @@
+type Weather : { Sunny , Cloudy , Rainy, Foggy }
+type TimeOfDay : { Morning , Noon, Afternoon, Night }
+type Clothing : { Nothing, Shorts, Warm, Waterproof }
+var isWet : boolean = false
+var looksOut : boolean = false
+var isClever : boolean = false
+var weather : Weather = Sunny
+var time : TimeOfDay
+var clothing  : Clothing = Nothing
+
+trans {
+    choice {
+        assume time == Morning;
+        choice {
+            assume (looksOut == false && isClever == false);
+            havoc clothing;
+        } or {
+            assume (looksOut == true && isClever == false);
+            choice {
+                assume weather == Sunny;
+                clothing := Shorts;
+            } or {
+                assume (weather == Cloudy || weather == Foggy);
+                clothing := Warm;
+            } or {
+                assume weather == Rainy;
+                clothing := Waterproof;
+            }
+        } or {
+            assume (isClever == true);
+            choice {
+                assume weather == Sunny;
+                clothing := Shorts;
+            } or {
+                assume (weather == Cloudy || weather == Rainy);
+                clothing := Waterproof;
+            } or {
+                assume weather == Foggy;
+                clothing := Warm;
+            }
+        }
+    } or {
+        assume time == Noon;
+        if (isWet == true) looksOut := true;
+    } or {
+        assume time == Afternoon;
+    } or {
+        assume time == Night;
+        if (isWet == true) isClever := true;
+        clothing := Nothing;
+    }
+}
+
+init {
+    havoc weather;
+    time := Morning;
+}
+
+env {
+        if (clothing != Waterproof && weather == Rainy) isWet := true;
+        if (time == Noon || time == Night) isWet := false;
+        choice {
+            assume time == Morning;
+            time := Noon;
+        } or {
+            assume time == Noon;
+            time := Afternoon;
+        } or {
+            assume time == Afternoon;
+            time := Night;
+        } or {
+            assume time == Night;
+            time := Morning;
+        }
+
+        choice {
+            assume time != Noon;
+            choice {
+                assume (weather == Sunny || weather == Cloudy || weather == Foggy);
+                choice {
+                    weather := Cloudy;
+                } or {
+                    weather := Sunny;
+                } or {
+                    assume weather == Cloudy;
+                    weather := Rainy;
+                }
+            } or {
+                assume (weather == Rainy);
+                choice {
+                    weather := Rainy;
+                } or {
+                    weather := Sunny;
+                }
+            } or {
+                assume time == Morning;
+                weather := Foggy;
+            }
+        } or {
+            assume time == Noon;
+        }
+
+}
+prop{true}
+ltl{G(time = TimeOfDay.Noon -> X(time = TimeOfDay.Noon or time = TimeOfDay.Afternoon))}
\ No newline at end of file