LTL checking

Add LTL checking possibility

build.gradle.kts

@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.6.4"
+    version = "6.7.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

settings.gradle.kts

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

subprojects/common/ltl/build.gradle.kts

@@ -0,0 +1,31 @@
+/*
+ *  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.
+ */
+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,55 @@
+/*
+ *  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,164 @@
+/*
+ *  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 cfa.buchi.ExternalLtl2Hoaf
+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.MultiAnalysisSide
+import hu.bme.mit.theta.analysis.multi.MultiPrec
+import hu.bme.mit.theta.analysis.multi.NextSideFunctions
+import hu.bme.mit.theta.analysis.multi.RefToMultiPrec
+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.Ltl2BuchiThroughHoaf
+import hu.bme.mit.theta.common.logging.Logger
+import hu.bme.mit.theta.core.decl.VarDecl
+import hu.bme.mit.theta.core.type.Expr
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
+import hu.bme.mit.theta.core.type.booltype.BoolType
+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,
+  initExpr: Expr<BoolType> = True(),
+) :
+  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<
+      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 = Ltl2BuchiThroughHoaf(ExternalLtl2Hoaf("wsl /mnt/c/Users/brippl/Downloads/owl-linux-amd64-21.0/owl-linux-musl-amd64-21.0/bin/owl ltl2nba -f"), variables, logger).transform(ltl)
+    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,
+        initExpr,
+      )
+    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,114 @@
+/*
+ *  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.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.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.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
+
+@RunWith(Parameterized::class)
+class LtlCheckTestWithCfa(
+  private val cfaName: String,
+  private val ltlExpr: String,
+  private val result: Boolean,
+) {
+
+  private val itpSolverFactory = Z3LegacySolverFactory.getInstance()
+  private val abstractionSolver: Solver = Z3LegacySolverFactory.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() {
+    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 multiSide =
+      MultiAnalysisSide(analysis, initFunc, combineStates, stripState, extractFromState, stripPrec)
+
+    val checker =
+      LtlChecker(
+        multiSide,
+        lts,
+        refToPrec,
+        ItpRefToExplPrec(),
+        dataAnalysis,
+        variables,
+        ltlExpr,
+        itpSolverFactory,
+        logger,
+        LoopcheckerSearchStrategy.GDFS,
+        LDGTraceCheckerStrategy.MILANO,
+      )
+
+    Assert.assertEquals(result, checker.check(initPrec, dataInitPrec).isSafe)
+  }
+}