From f382dc1d45b330173f834fc7402a497b258a8d65 Mon Sep 17 00:00:00 2001 From: RipplB Date: Sun, 21 Jul 2024 22:10:06 +0200 Subject: [PATCH] ltl --- settings.gradle.kts | 1 + .../mit/theta/analysis/multi/MultiSide.java | 13 +- .../loopchecker/abstraction/LDGAbstractor.kt | 3 +- .../abstraction/NdfsSearchStrategy.kt | 19 +- .../refinement/LDGTraceCheckerStrategy.kt | 40 +++-- subprojects/common/ltl/build.gradle.kts | 32 ++++ .../hu/bme/mit/theta/common/ltl/BuchiUtils.kt | 57 ++++++ .../hu/bme/mit/theta/common/ltl/LtlChecker.kt | 119 ++++++++++++ .../theta/common/ltl/LtlCheckTestWithCfa.kt | 123 +++++++++++++ .../common/ltl/LtlCheckTestWithCfaPred.kt | 135 ++++++++++++++ .../theta/common/ltl/LtlCheckTestWithXsts.kt | 101 +++++++++++ .../common/ltl/LtlCheckTestWithXstsPred.kt | 148 +++++++++++++++ .../src/test/resources/cfa/counter2inf.cfa | 12 ++ .../src/test/resources/cfa/counter5inf.cfa | 12 ++ .../ltl/src/test/resources/cfa/indicator.cfa | 14 ++ .../resources/cfa/indicator_multiassign.cfa | 12 ++ .../ltl/src/test/resources/cfa/wave_flag.cfa | 9 + .../ltl/src/test/resources/cfa/wave_flags.cfa | 18 ++ .../src/test/resources/xsts/counter3inf.xsts | 12 ++ .../src/test/resources/xsts/counter50.xsts | 16 ++ .../src/test/resources/xsts/counter6to7.xsts | 13 ++ .../ltl/src/test/resources/xsts/forever5.xsts | 9 + .../resources/xsts/randomincreasingeven.xsts | 14 ++ .../src/test/resources/xsts/simple_color.xsts | 24 +++ .../src/test/resources/xsts/simple_types.xsts | 16 ++ .../test/resources/xsts/trafficlight_v2.xsts | 169 ++++++++++++++++++ .../ltl/src/test/resources/xsts/weather.xsts | 104 +++++++++++ .../test/resources/xsts/weather_noinit.xsts | 106 +++++++++++ .../resources/xsts/weather_withprops.xsts | 105 +++++++++++ .../xsts/analysis/XstsNextSideFunctions.kt | 46 +++++ .../bme/mit/theta/xsts/analysis/XstsTest.java | 2 +- 31 files changed, 1477 insertions(+), 27 deletions(-) create mode 100644 subprojects/common/ltl/build.gradle.kts create mode 100644 subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/BuchiUtils.kt create mode 100644 subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt create mode 100644 subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfa.kt create mode 100644 subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt create mode 100644 subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXsts.kt create mode 100644 subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt create mode 100644 subprojects/common/ltl/src/test/resources/cfa/counter2inf.cfa create mode 100644 subprojects/common/ltl/src/test/resources/cfa/counter5inf.cfa create mode 100644 subprojects/common/ltl/src/test/resources/cfa/indicator.cfa create mode 100644 subprojects/common/ltl/src/test/resources/cfa/indicator_multiassign.cfa create mode 100644 subprojects/common/ltl/src/test/resources/cfa/wave_flag.cfa create mode 100644 subprojects/common/ltl/src/test/resources/cfa/wave_flags.cfa create mode 100644 subprojects/common/ltl/src/test/resources/xsts/counter3inf.xsts create mode 100644 subprojects/common/ltl/src/test/resources/xsts/counter50.xsts create mode 100644 subprojects/common/ltl/src/test/resources/xsts/counter6to7.xsts create mode 100644 subprojects/common/ltl/src/test/resources/xsts/forever5.xsts create mode 100644 subprojects/common/ltl/src/test/resources/xsts/randomincreasingeven.xsts create mode 100644 subprojects/common/ltl/src/test/resources/xsts/simple_color.xsts create mode 100644 subprojects/common/ltl/src/test/resources/xsts/simple_types.xsts create mode 100644 subprojects/common/ltl/src/test/resources/xsts/trafficlight_v2.xsts create mode 100644 subprojects/common/ltl/src/test/resources/xsts/weather.xsts create mode 100644 subprojects/common/ltl/src/test/resources/xsts/weather_noinit.xsts create mode 100644 subprojects/common/ltl/src/test/resources/xsts/weather_withprops.xsts create mode 100644 subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsNextSideFunctions.kt 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/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiSide.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiSide.java index f3c9010949..ee53e22849 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiSide.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiSide.java @@ -15,6 +15,17 @@ */ package hu.bme.mit.theta.analysis.multi; +import com.google.common.base.Preconditions; + public enum MultiSide { - LEFT, RIGHT, BOTH + LEFT, RIGHT, BOTH; + + public MultiSide otherSide() { + return complementer(this); + } + + public static MultiSide complementer(MultiSide side) { + Preconditions.checkState(side != BOTH, "Only LEFT or RIGHT have complementer side"); + return side == LEFT ? RIGHT : LEFT; + } } diff --git a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt index def7c964fb..e903160a83 100644 --- a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt +++ b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt @@ -42,7 +42,8 @@ class LDGAbstractor( } val expander: NodeExpander = { node -> lts.getEnabledActionsFor(node.state).flatMap { action -> - analysis.transFunc.getSuccStates(node.state, action, prec).map(ldg::getOrCreateNode) + analysis.transFunc.getSuccStates(node.state, action, prec).filterNot { it.isBottom } + .map(ldg::getOrCreateNode) .map { ldg.drawEdge(node, it, action, acceptancePredicate.test(Pair(it.state, action))) } } } diff --git a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt index 052771f017..5f9e6a3315 100644 --- a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt +++ b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt @@ -23,7 +23,6 @@ import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.logging.Logger -import java.util.* object NdfsSearchStrategy : ILoopcheckerSearchStrategy { @@ -42,52 +41,46 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy { } private fun redSearch( - seed: LDGNode, edge: LDGEdge, trace: MutableList>, + seed: LDGNode, edge: LDGEdge, trace: List>, redNodes: MutableSet>, target: AcceptancePredicate, expand: NodeExpander ): List> { val targetNode = edge.target - trace.add(edge) if (targetNode == seed) { - return trace + return trace + edge } if (redNodes.contains(targetNode)) { - trace.removeLast() return emptyList() } redNodes.add(edge.target) for (nextEdge in expand(targetNode)) { - val redSearch: List> = redSearch(seed, nextEdge, trace, redNodes, target, expand) + val redSearch: List> = redSearch(seed, nextEdge, trace + edge, redNodes, target, expand) if (redSearch.isNotEmpty()) return redSearch } - trace.removeLast() return emptyList() } private fun blueSearch( - edge: LDGEdge, trace: MutableList>, blueNodes: MutableCollection>, + edge: LDGEdge, trace: List>, blueNodes: MutableCollection>, redNodes: Set>, target: AcceptancePredicate, expand: NodeExpander ): Collection> { val targetNode = edge.target - trace.add(edge) if (target.test(Pair(targetNode.state, edge.action))) { // Edge source can only be null artificially, and is only used when calling other search strategies val accNode = if (targetNode.accepting) targetNode else edge.source!! val redSearch: List> = - redSearch(accNode, edge, LinkedList>(trace), mutableSetOf(), target, expand) + redSearch(accNode, edge, trace, mutableSetOf(), target, expand) if (redSearch.isNotEmpty()) return setOf(LDGTrace(redSearch, accNode)) } if (blueNodes.contains(targetNode)) { - trace.removeLast() return emptyList() } blueNodes.add(edge.target) for (nextEdge in expand(targetNode)) { val blueSearch: Collection> = - blueSearch(nextEdge, trace, blueNodes, redNodes, target, expand) + blueSearch(nextEdge, trace + edge, blueNodes, redNodes, target, expand) if (!blueSearch.isEmpty()) return blueSearch } - trace.removeLast() return emptyList() } diff --git a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt index 88392af426..625eb2abfa 100644 --- a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt +++ b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt @@ -42,7 +42,8 @@ enum class LDGTraceCheckerStrategy { override fun check( trace: LDGTrace, solverFactory: SolverFactory, init: Expr, logger: Logger ) = MilanoLDGTraceCheckerStrategy(trace, solverFactory, init, logger).check() - }, BOUNDED_UNROLLING { + }, + BOUNDED_UNROLLING { override fun check( trace: LDGTrace, solverFactory: SolverFactory, init: Expr, logger: Logger @@ -61,28 +62,42 @@ enum class LDGTraceCheckerStrategy { val default = MILANO } - abstract fun check(trace: LDGTrace, solverFactory: SolverFactory, init : Expr = True(), logger: Logger = NullLogger.getInstance()): ExprTraceStatus + + abstract fun check( + trace: LDGTrace, solverFactory: SolverFactory, init: Expr = True(), + logger: Logger = NullLogger.getInstance() + ): ExprTraceStatus } -abstract class AbstractLDGTraceCheckerStrategy(private val trace: LDGTrace, solverFactory: SolverFactory, private val init : Expr, private val logger: Logger) { +abstract class AbstractLDGTraceCheckerStrategy( + private val trace: LDGTrace, solverFactory: SolverFactory, private val init: Expr, + private val logger: Logger +) { + protected val solver: ItpSolver = solverFactory.createItpSolver() protected val stateCount = trace.length() + 1 protected val indexings = mutableListOf() protected val satMarker: ItpMarker = solver.createMarker() protected val unreachableMarker: ItpMarker = solver.createMarker() protected val pattern: ItpPattern = solver.createBinPattern(satMarker, unreachableMarker) - protected val variables = trace.edges.flatMap { ExprUtils.getVars(it.source?.state?.toExpr() ?: True()) + ExprUtils.getVars(it.action?.toExpr() ?: True()) } + protected val variables = trace.edges.flatMap { + ExprUtils.getVars(it.source?.state?.toExpr() ?: True()) + ExprUtils.getVars( + it.action?.toExpr() ?: True() + ) + }.distinct() private fun findSatIndex(): Int { for (i in 1 until stateCount) { solver.push() indexings.add(indexings[i - 1].add(trace.getAction(i - 1)!!.nextIndexing())) - solver.add(satMarker, PathUtils.unfold(trace.getState(i).toExpr(), indexings[i])) + val stateExpression = PathUtils.unfold(trace.getState(i).toExpr(), indexings[i]) + solver.add(satMarker, stateExpression) + val actionExpression = PathUtils.unfold( + trace.getAction(i - 1)!!.toExpr(), + indexings[i - 1] + ) solver.add( - satMarker, PathUtils.unfold( - trace.getAction(i - 1)!!.toExpr(), - indexings[i - 1] - ) + satMarker, actionExpression ) if (solver.check().isUnsat) { solver.pop() @@ -92,7 +107,7 @@ abstract class AbstractLDGTraceCheckerStrategy(pri return stateCount - 1 } - abstract fun evaluateLoop(valuation: Valuation) : ExprTraceStatus + abstract fun evaluateLoop(valuation: Valuation): ExprTraceStatus fun check(): ExprTraceStatus { solver.push() @@ -136,7 +151,10 @@ abstract class AbstractLDGTraceCheckerStrategy(pri } } - protected fun getItpRefutationFeasible(): Feasible = ExprTraceStatus.feasible(Trace.of(indexings.map { PathUtils.extractValuation(solver.model, it) }, (trace.tail + trace.loop).map { it.action })) + protected fun getItpRefutationFeasible(): Feasible = ExprTraceStatus.feasible( + Trace.of( + indexings.map { PathUtils.extractValuation(solver.model, it) }, (trace.tail + trace.loop).map { it.action }) + ) protected fun logInterpolant(expr: Expr) { logger.write(Logger.Level.INFO, "Interpolant : $expr%n") diff --git a/subprojects/common/ltl/build.gradle.kts b/subprojects/common/ltl/build.gradle.kts new file mode 100644 index 0000000000..41cb4c2c24 --- /dev/null +++ b/subprojects/common/ltl/build.gradle.kts @@ -0,0 +1,32 @@ +/* + * 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("kotlin-common") +} + +dependencies { + implementation(project(":theta-common")) + implementation(project(":theta-core")) + implementation(project(":theta-solver")) + implementation(project(":theta-analysis")) + implementation(project(":theta-cfa")) + implementation(project(":theta-cfa-analysis")) + testImplementation(project(":theta-solver-z3-legacy")) + testImplementation(project(":theta-solver-javasmt")) + testImplementation(project(":theta-solver-smtlib")) + testImplementation(project(":theta-xsts")) + testImplementation(project(":theta-xsts-analysis")) +} 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

(private val initLoc: CFA.Loc) : InitFunc, P> { + + override fun getInitStates(prec: P) = mutableListOf(CfaState.of(initLoc, UnitState.getInstance())) +} + +class BuchiLts : LTS, CfaAction> { + + override fun getEnabledActionsFor(state: CfaState) = state.loc.outEdges.map(CfaAction::create) +} + +fun buchiPredicate( + buchiAutomaton: CFA +): AcceptancePredicate, D>, StmtMultiAction> = AcceptancePredicate( + actionPredicate = { a -> + (a?.rightAction != null && a.rightAction.edges.any { e -> + buchiAutomaton.acceptingEdges.contains( + e + ) + }) + }) + +fun combineBlankBuchiStateWithData(buchiState: CfaState, dataState: D) = + CfaState.of(buchiState.loc, dataState) + +fun stripDataFromBuchiState(buchiState: CfaState) = + 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..7a6d41c643 --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt @@ -0,0 +1,119 @@ +/* + * 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.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.CFA +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.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( + multiSide: MultiAnalysisSide, + lts: LTS, + refToPrec: RefutationToPrec, + dataRefToPrec: RefutationToPrec, + dataAnalysis: Analysis, + variables: Collection>, + ltl: String, + solverFactory: SolverFactory, + logger: Logger, + searchStrategy: LoopcheckerSearchStrategy, + refinerStrategy: LDGTraceCheckerStrategy, + initExpr: Expr = True(), + nextSideFunction: NextSideFunctions.NextSideFunction, DataS, ExprMultiState, DataS>> = NextSideFunctions.Alternating() +) : SafetyChecker, DataS>, StmtMultiAction>, LDGTrace, DataS>, StmtMultiAction>, MultiPrec, DataP>> { + + private val checker: CegarChecker, DataS>, StmtMultiAction, MultiPrec, DataP>, LDG, DataS>, StmtMultiAction>, LDGTrace, DataS>, StmtMultiAction>> + private val buchiAutomaton: CFA + + init { + buchiAutomaton = BuchiBuilder.of(ltl, variables, logger) + val cfaAnalysis: Analysis, CfaAction, CfaPrec> = + 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(nextSideFunction, 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, DataS>, StmtMultiAction, MultiPrec, DataP>> = + SingleLDGTraceRefiner( + refinerStrategy, solverFactory, JoiningPrecRefiner.create(multiRefToPrec), logger, initExpr + ) + val visualizer = + LdgVisualizer, DataS>, StmtMultiAction>( + { it.toString() }, + { it.toString() } + ) + checker = CegarChecker.create(abstractor, refiner, logger, visualizer) + } + + override fun check( + input: MultiPrec, DataP> + ): SafetyResult, DataS>, StmtMultiAction>, LDGTrace, DataS>, StmtMultiAction>> { + return checker.check(input) + } + + fun check( + prec: P, dataPrec: DataP + ): SafetyResult, DataS>, StmtMultiAction>, LDGTrace, DataS>, StmtMultiAction>> { + 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..ae3cdbaacf --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfa.kt @@ -0,0 +1,123 @@ +/* + * 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.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 -> listOf>(CfaState.of(cfa.initLoc, UnitState.getInstance())) } +// val variables = cfa.vars +// val dataInitPrec = ExplPrec.of(variables) +// val initPrec:CfaPrec = GlobalCfaPrec.create(dataInitPrec) +// val combineStates = { c: CfaState, d: ExplState -> CfaState.of(c.loc, d) } +// val stripState = { c: CfaState -> CfaState.of(c.loc, UnitState.getInstance()) } +// val extractFromState = { c: CfaState -> c.state } +// val stripPrec = { p: CfaPrec -> 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..9127711ab1 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt @@ -0,0 +1,135 @@ +/* + * 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.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( +// 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 -> listOf>(CfaState.of(cfa.initLoc, UnitState.getInstance())) } +// val variables = cfa.vars +// val dataInitPrec = PredPrec.of() +// val initPrec:CfaPrec = GlobalCfaPrec.create(dataInitPrec) +// val combineStates = { c: CfaState, d: PredState -> CfaState.of(c.loc, d) } +// val stripState = { c: CfaState -> CfaState.of(c.loc, UnitState.getInstance()) } +// val extractFromState = { c: CfaState -> c.state } +// val stripPrec = { p: CfaPrec -> 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..ea474db860 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXsts.kt @@ -0,0 +1,101 @@ +/* + * 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.multi.MultiSide +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.SingleXstsNextSideFunction +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.MAINSTEP) + + 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), + arrayOf( + "trafficlight_v2", + "G((normal = Normal.Red and (not PoliceInterrupt_police) and Control_toggle) -> X(normal = Normal.Green or interrupted = Interrupted.BlinkingYellow))", + 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, + xsts.initFormula, + SingleXstsNextSideFunction({ it.leftState }, MultiSide.LEFT) + ) + 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..54e233db39 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt @@ -0,0 +1,148 @@ +/* + * 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.multi.MultiSide +import hu.bme.mit.theta.analysis.multi.NextSideFunctions +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.solver.SolverManager +import hu.bme.mit.theta.solver.javasmt.JavaSMTSolverManager +import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager +import hu.bme.mit.theta.solver.z3legacy.Z3SolverManager +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.SingleXstsNextSideFunction +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 combineSteps: 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), // OK + arrayOf("counter3inf", "F G(x=3)", true), // OK + arrayOf("counter3inf", "F(x=2)", true), // OK + arrayOf("counter3inf", "G(x<4)", true), // OK + arrayOf("counter3inf", "G(x=1)", false), // OK + arrayOf("counter6to7", "G(x=1)", false), // OK + arrayOf("counter6to7", "G(x=7)", false), // OK + arrayOf("counter6to7", "G F(x=7)", true), // OK + arrayOf("counter50", "G(x<49)", false), // OK + arrayOf( + "trafficlight_v2", "G(LightCommands_displayRed -> X(not LightCommands_displayGreen))", true + ), // OK + arrayOf( + "trafficlight_v2", + "G((normal = Normal.Red and (not PoliceInterrupt_police) and Control_toggle) -> X(normal = Normal.Green or interrupted = Interrupted.BlinkingYellow))", + true, true + ), // OK + arrayOf("trafficlight_v2", "G(PoliceInterrupt_police -> F(LightCommands_displayYellow))", true), // OK + arrayOf("forever5", "G(x=5)", true), // OK + arrayOf("forever5", "F(x=6)", false), // OK + arrayOf("randomincreasingeven", "not F(x=1)", true), // Stuck in iteration 12 in GDFS + arrayOf("randomincreasingeven", "F(x>10)", true), // OK + arrayOf("randomincreasingeven", "G(x>=0)", true), // OK + arrayOf("simple_color", "G(envColor = Colors.Green -> X(modelColor = Colors.Blue))", true), // OK + arrayOf("simple_color", "G(envColor = Colors.Green -> X(modelColor = Colors.Green))", false), // OK + arrayOf("simple_color", "F G(envColor = modelColor)", false), // OK + arrayOf("weather", "G F(isClever and isWet)", false), // timeout in GDFS +// arrayOf("weather", "F G(not isWet)", true), // theory not supported by interpolation or bad proof in GDFS + arrayOf( + "weather", "G(time = TimeOfDay.Noon -> X(time = TimeOfDay.Noon or time = TimeOfDay.Afternoon))", true + ), // OK +// 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 = "{0} ({1}): {4}-{5}") + fun params() = + data().map { if (it.size == 3) arrayOf(*it, false) else it }.flatMap { data -> + listOf(/*LoopcheckerSearchStrategy.GDFS,*/ LoopcheckerSearchStrategy.NDFS).flatMap { search -> + listOf(LDGTraceCheckerStrategy.MILANO, LDGTraceCheckerStrategy.BOUNDED_UNROLLING).map { ref -> + arrayOf(*data, 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!! + SolverManager.registerSolverManager(JavaSMTSolverManager.create()) + SolverManager.registerSolverManager(SmtLibSolverManager.create(SmtLibSolverManager.HOME, logger)) + SolverManager.registerSolverManager(Z3SolverManager.create()) + val solverFactory = SolverManager.resolveSolverFactory("Z3") + 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, + xsts.initFormula, + if (combineSteps) SingleXstsNextSideFunction( + { it.leftState }, MultiSide.LEFT + ) else NextSideFunctions.Alternating() + ) + 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 diff --git a/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsNextSideFunctions.kt b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsNextSideFunctions.kt new file mode 100644 index 0000000000..cb8e4dd3eb --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsNextSideFunctions.kt @@ -0,0 +1,46 @@ +/* + * 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.xsts.analysis + +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.multi.MultiSide +import hu.bme.mit.theta.analysis.multi.MultiState +import hu.bme.mit.theta.analysis.unit.UnitState +import hu.bme.mit.theta.analysis.multi.NextSideFunctions.NextSideFunction as NextsideFunction + +class SingleXstsNextSideFunction>( + private val getXstsState: (M) -> XstsState<*>, private val xstsSide: MultiSide +) : NextsideFunction { + + override fun defineNextSide(state: M): MultiSide { + if (state.sourceSide != xstsSide) return xstsSide + val xstsState = getXstsState(state) + return if (xstsState.lastActionWasEnv()) xstsSide else xstsSide.otherSide() + } + +} + +class BothXstsNextSideFunction, XstsState, D>> : + NextsideFunction, XstsState, D, M> { + + override fun defineNextSide(state: M): MultiSide { + val lastState: XstsState = + if (state.sourceSide == MultiSide.LEFT) state.leftState else state.rightState + return if (lastState.lastActionWasEnv()) state.sourceSide else state.sourceSide.otherSide() + } +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java index dad84105f5..d750d534be 100644 --- a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java @@ -45,7 +45,7 @@ @RunWith(value = Parameterized.class) public class XstsTest { - private static final String SOLVER_STRING = "Z3"; + private static final String SOLVER_STRING = "mathsat:latest"; private static final Path SMTLIB_HOME = SmtLibSolverManager.HOME; @Parameterized.Parameter(value = 0)