ltl

settings.gradle.kts

@@ -20,6 +20,7 @@ include(
     "common/common",
     "common/core",
     "common/grammar",
+    "common/ltl",
     "common/multi-tests",
 
     "frontends/c-frontend",

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")))
+}

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())

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))
+    }
+}

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)
+//    }
+//
+//}