diff --git a/build.gradle.kts b/build.gradle.kts index e5be05ea9b..3b60d44bbc 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -29,7 +29,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.7.0" + version = "6.8.0" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/settings.gradle.kts b/settings.gradle.kts index 5421f34ea0..c66e3b4fe6 100644 --- a/settings.gradle.kts +++ b/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", diff --git a/subprojects/common/ltl/build.gradle.kts b/subprojects/common/ltl/build.gradle.kts new file mode 100644 index 0000000000..7ba6367682 --- /dev/null +++ b/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"))) +} 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..f0619147e2 --- /dev/null +++ b/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

(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()) 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..2aa06c73ca --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt @@ -0,0 +1,162 @@ +/* + * 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.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.Ltl2BuchiTransformer +import hu.bme.mit.theta.common.logging.Logger +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, + lts: LTS, + refToPrec: RefutationToPrec, + dataRefToPrec: RefutationToPrec, + dataAnalysis: Analysis, + ltl: String, + solverFactory: SolverFactory, + logger: Logger, + searchStrategy: LoopcheckerSearchStrategy, + refinerStrategy: LDGTraceCheckerStrategy, + ltl2BuchiTransformer: Ltl2BuchiTransformer, + initExpr: Expr = True(), +) : + SafetyChecker< + LDG, DataS>, StmtMultiAction>, + LDGTrace, DataS>, StmtMultiAction>, + MultiPrec, DataP>, + > { + private val checker: + CegarChecker< + MultiPrec, DataP>, + LDG, DataS>, StmtMultiAction>, + LDGTrace, DataS>, StmtMultiAction>, + > + + init { + val buchiAutomaton = ltl2BuchiTransformer.transform(ltl) + 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(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, DataS>, + StmtMultiAction, + MultiPrec, DataP>, + > = + SingleLDGTraceRefiner( + refinerStrategy, + solverFactory, + JoiningPrecRefiner.create(multiRefToPrec), + logger, + initExpr, + ) + val visualizer = + LdgVisualizer< + ExprMultiState, DataS>, + StmtMultiAction, + >( + { it.toString() }, + { it.toString() }, + ) + checker = CegarChecker.create(abstractor, refiner, logger, visualizer) + } + + override fun check( + input: MultiPrec, DataP> + ): SafetyResult< + LDG, DataS>, StmtMultiAction>, + LDGTrace, DataS>, StmtMultiAction>, + > { + return checker.check(input) + } + + fun check( + prec: P, + dataPrec: DataP, + ): SafetyResult< + LDG, DataS>, StmtMultiAction>, + LDGTrace, DataS>, StmtMultiAction>, + > { + return check(MultiPrec(prec, GlobalCfaPrec.create(dataPrec), dataPrec)) + } +} 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..bbe63081d2 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfa.kt @@ -0,0 +1,107 @@ +/* + * 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.ItpRefToExplPrec +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.cfa.analysis.CfaPrec +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder +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.hoa.Ltl2BuchiThroughHoaf +import hu.bme.mit.theta.cfa.buchi.hoa.Ltl2HoafFromDir +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 configBuilder = + CfaConfigBuilder( + CfaConfigBuilder.Domain.EXPL, + CfaConfigBuilder.Refinement.SEQ_ITP, + itpSolverFactory, + ) + .encoding(CfaConfigBuilder.Encoding.SBE) + .ExplStrategy(cfa) + val dataAnalysis = ExplAnalysis.create(abstractionSolver, True()) + val refToPrec = RefutationToGlobalCfaPrec(ItpRefToExplPrec(), cfa.initLoc) + val variables = cfa.vars + val dataInitPrec = ExplPrec.of(variables) + val initPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) + + val checker = + LtlChecker( + configBuilder.multiSide, + configBuilder.lts, + refToPrec, + configBuilder.itpRefToPrec, + dataAnalysis, + ltlExpr, + itpSolverFactory, + logger, + LoopcheckerSearchStrategy.GDFS, + LDGTraceCheckerStrategy.MILANO, + Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), variables, logger), + ) + + Assert.assertEquals(result, checker.check(initPrec, dataInitPrec).isSafe) + } +} 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..a7c3e01875 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt @@ -0,0 +1,130 @@ +/* + * 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.expr.ExprAction +import hu.bme.mit.theta.analysis.pred.* +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder +import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec +import hu.bme.mit.theta.cfa.buchi.hoa.Ltl2BuchiThroughHoaf +import hu.bme.mit.theta.cfa.buchi.hoa.Ltl2HoafFromDir +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 LtlCheckTestWithCfaPred( + private val cfaName: String, + private val ltlExpr: String, + private val result: Boolean, + private val searchStrategy: LoopcheckerSearchStrategy, + private val refinerStrategy: LDGTraceCheckerStrategy, +) { + + private val itpSolverFactory = Z3LegacySolverFactory.getInstance() + private val abstractionSolver: Solver = Z3LegacySolverFactory.getInstance().createSolver() + private val logger: Logger = ConsoleLogger(Logger.Level.INFO) + + companion object { + 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), + ) + + @JvmStatic + @Parameterized.Parameters(name = "{3}-{4}: {0}") + fun params() = + listOf(LoopcheckerSearchStrategy.GDFS, LoopcheckerSearchStrategy.NDFS).flatMap { search -> + listOf(LDGTraceCheckerStrategy.MILANO, LDGTraceCheckerStrategy.BOUNDED_UNROLLING).flatMap { + ref -> + data().map { arrayOf(*it, search, ref) } + } + } + } + + @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 configBuilder = + CfaConfigBuilder( + CfaConfigBuilder.Domain.PRED_SPLIT, + CfaConfigBuilder.Refinement.SEQ_ITP, + itpSolverFactory, + ) + .encoding(CfaConfigBuilder.Encoding.SBE) + .PredStrategy(cfa) + val variables = cfa.vars + val dataAnalysis = + PredAnalysis.create( + abstractionSolver, + PredAbstractors.booleanSplitAbstractor(abstractionSolver), + True(), + ) + val refToPrec = RefutationToGlobalCfaPrec(ItpRefToPredPrec(ExprSplitters.atoms()), cfa.initLoc) + val dataInitPrec = PredPrec.of() + + val checker = + LtlChecker( + configBuilder.multiSide, + configBuilder.lts, + refToPrec, + configBuilder.itpRefToPrec, + dataAnalysis, + ltlExpr, + itpSolverFactory, + logger, + searchStrategy, + refinerStrategy, + Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), variables, logger), + ) + + Assert.assertEquals(result, checker.check(configBuilder.createInitPrec(), dataInitPrec).isSafe) + } +} 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..d75a5a957e --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXsts.kt @@ -0,0 +1,99 @@ +/* + * 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.cfa.buchi.hoa.Ltl2BuchiThroughHoaf +import hu.bme.mit.theta.cfa.buchi.hoa.Ltl2HoafFromDir +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder +import hu.bme.mit.theta.xsts.dsl.XstsDslManager +import hu.bme.mit.theta.xsts.normalize +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 LtlCheckTestWithXsts( + private val xstsName: String, + private val ltlExpr: String, + private val result: Boolean, +) { + + private val solverFactory = Z3LegacySolverFactory.getInstance() + private val logger: Logger = ConsoleLogger(Logger.Level.VERBOSE) + + companion object { + @JvmStatic + @Parameterized.Parameters + fun data() = + listOf( + arrayOf("counter3inf", "F G(x=3)", true), + arrayOf("counter3inf", "F(x=2)", true), + arrayOf("counter3inf", "G(x<4)", true), + arrayOf("counter3inf", "G(x=1)", false), + arrayOf("counter6to7", "G(x=1)", false), + arrayOf("counter6to7", "G(x=7)", false), + arrayOf("counter6to7", "G F(x=7)", true), + ) + } + + @Test + fun test() { + var xstsI: XSTS? + FileInputStream(String.format("src/test/resources/xsts/%s.xsts", xstsName)).use { inputStream -> + xstsI = XstsDslManager.createXsts(inputStream) + } + if (xstsI == null) fail("Couldn't read xsts $xstsName") + val xsts = normalize(xstsI) + 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, + ltlExpr, + solverFactory, + logger, + LoopcheckerSearchStrategy.GDFS, + LDGTraceCheckerStrategy.MILANO, + Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), xsts.vars, logger), + xsts.initFormula, + ) + val checkResult = checker.check(initPrec, initPrec) + + Assert.assertEquals(result, checkResult.isSafe) + } +} 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..7464f7d15f --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt @@ -0,0 +1,155 @@ +/* + * 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.pred.ExprSplitters +import hu.bme.mit.theta.analysis.pred.ItpRefToPredPrec +import hu.bme.mit.theta.cfa.buchi.hoa.Ltl2BuchiThroughHoaf +import hu.bme.mit.theta.cfa.buchi.hoa.Ltl2HoafFromDir +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.solver.Solver +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder +import hu.bme.mit.theta.xsts.dsl.XstsDslManager +import hu.bme.mit.theta.xsts.normalize +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 LtlCheckTestWithXstsPred( + private val xstsName: String, + private val ltlExpr: String, + private val result: Boolean, + private val searchStrategy: LoopcheckerSearchStrategy, + private val refinerStrategy: LDGTraceCheckerStrategy, +) { + + private val itpSolverFactory = Z3LegacySolverFactory.getInstance() + private val abstractionSolver: Solver = Z3LegacySolverFactory.getInstance().createSolver() + private val logger: Logger = ConsoleLogger(Logger.Level.INFO) + + companion object { + private fun data() = + listOf( + arrayOf("simple_types", "F G(color = Colors.Red)", false), + arrayOf("counter3inf", "F G(x=3)", true), + arrayOf("counter3inf", "F(x=2)", true), + arrayOf("counter3inf", "G(x<4)", true), + arrayOf("counter3inf", "G(x=1)", false), + arrayOf("counter6to7", "G(x=1)", false), + arrayOf("counter6to7", "G(x=7)", false), + arrayOf("counter6to7", "G F(x=7)", true), + // arrayOf("counter50", "G(x<49)", false), + arrayOf( + "trafficlight_v2", + "G(LightCommands_displayRed -> X(not LightCommands_displayGreen))", + true, + ), + arrayOf( + "trafficlight_v2", + "G((normal = Normal.Red and (not PoliceInterrupt_police) and Control_toggle) -> X(normal = Normal.Green))", + true, + ), + arrayOf( + "trafficlight_v2", + "G(PoliceInterrupt_police -> F(LightCommands_displayYellow))", + true, + ), + arrayOf("forever5", "G(x=5)", true), + arrayOf("forever5", "F(x=6)", false), + arrayOf("randomincreasingeven", "not F(x=1)", true), + arrayOf("randomincreasingeven", "F(x>10)", true), + arrayOf("randomincreasingeven", "G(x>=0)", true), + arrayOf("simple_color", "G(envColor = Colors.Green -> X(modelColor = Colors.Blue))", true), + arrayOf( + "simple_color", + "G(envColor = Colors.Green -> X(modelColor = Colors.Green))", + false, + ), + arrayOf("simple_color", "F G(envColor = modelColor)", false), + arrayOf("weather", "G F(isClever and isWet)", false), + arrayOf("weather", "F G(not isWet)", true), + arrayOf( + "weather", + "G(time = TimeOfDay.Noon -> X(time = TimeOfDay.Noon or time = TimeOfDay.Afternoon))", + true, + ), + // arrayOf("weather", "F G(weather = Weather.Foggy -> (clothing = + // Clothing.Nothing or clothing = Clothing.Warm))", true), + // arrayOf("weather_noinit", "G F(isClever and isWet)", false), + // arrayOf("weather_noinit", "F G(not isWet)", true), + // arrayOf("weather_noinit", "G(time = TimeOfDay.Noon -> X(time = TimeOfDay.Noon + // or time = TimeOfDay.Afternoon))", true), + // arrayOf("weather_noinit", "F G(weather = Weather.Foggy -> (clothing = + // Clothing.Nothing or clothing = Clothing.Warm))", true), + ) + + @JvmStatic + @Parameterized.Parameters(name = "{3}-{4}: {0}") + fun params() = + listOf(LoopcheckerSearchStrategy.GDFS, LoopcheckerSearchStrategy.NDFS).flatMap { search -> + LDGTraceCheckerStrategy.entries.flatMap { ref -> data().map { arrayOf(*it, search, ref) } } + } + } + + @Test + fun test() { + var xstsI: XSTS? + FileInputStream("src/test/resources/xsts/$xstsName.xsts").use { inputStream -> + xstsI = XstsDslManager.createXsts(inputStream) + } + if (xstsI == null) fail("Couldn't read xsts $xstsName") + val xsts = normalize(xstsI) + val configBuilder = + XstsConfigBuilder( + XstsConfigBuilder.Domain.PRED_SPLIT, + XstsConfigBuilder.Refinement.SEQ_ITP, + itpSolverFactory, + itpSolverFactory, + ) + .initPrec(XstsConfigBuilder.InitPrec.EMPTY) + .PredStrategy(xsts) + val variables = xsts.vars + val refToPrec = ItpRefToPredPrec(ExprSplitters.atoms()) + val initPrec = configBuilder.initPrec + + val checker = + LtlChecker( + configBuilder.multiSide, + configBuilder.lts, + refToPrec, + refToPrec, + configBuilder.dataAnalysis, + ltlExpr, + itpSolverFactory, + logger, + searchStrategy, + refinerStrategy, + Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), variables, logger), + xsts.initFormula, + ) + + Assert.assertEquals(result, checker.check(initPrec, initPrec).isSafe) + } +} 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/hoa/%21%28%21+F+ap0%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28%21+F+ap0%29.hoa new file mode 100644 index 0000000000..5feaea29ec --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28%21+F+ap0%29.hoa @@ -0,0 +1,18 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for F(ap0)" +owlArgs: "ltl2nba" "-f" "!(! F ap0)" "-o" "src/test/resources/hoa/%21%28%21+F+ap0%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +properties: deterministic unambiguous +properties: complete +AP: 1 "ap0" +--BODY-- +State: 0 +[!0] 0 +[0] 1 +State: 1 +[t] 1 {0} +--END-- diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28F+G+ap0%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28F+G+ap0%29.hoa new file mode 100644 index 0000000000..26792660e6 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28F+G+ap0%29.hoa @@ -0,0 +1,16 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for G(F(!ap0))" +owlArgs: "ltl2nba" "-f" "!(F G ap0)" "-o" "src/test/resources/hoa/%21%28F+G+ap0%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +properties: deterministic unambiguous +properties: complete +AP: 1 "ap0" +--BODY-- +State: 0 +[!0] 0 {0} +[0] 0 +--END-- diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28F+ap0%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28F+ap0%29.hoa new file mode 100644 index 0000000000..aa31b46518 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28F+ap0%29.hoa @@ -0,0 +1,14 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for G(!ap0)" +owlArgs: "ltl2nba" "-f" "!(F ap0)" "-o" "src/test/resources/hoa/%21%28F+ap0%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +properties: deterministic unambiguous +AP: 1 "ap0" +--BODY-- +State: 0 +[!0] 0 {0} +--END-- diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28ap0+-%3E+F+ap1%29%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28ap0+-%3E+F+ap1%29%29.hoa new file mode 100644 index 0000000000..5da3686644 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28ap0+-%3E+F+ap1%29%29.hoa @@ -0,0 +1,16 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for F(((ap0) & (G(!ap1))))" +owlArgs: "ltl2nba" "-f" "!(G (ap0 -> F ap1))" "-o" "src/test/resources/hoa/%21%28G+%28ap0+-%3E+F+ap1%29%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +AP: 2 "ap0" "ap1" +--BODY-- +State: 0 +[t] 0 +[0 & !1] 1 +State: 1 +[!1] 1 {0} +--END-- diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28ap0+-%3E+X+ap1%29%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28ap0+-%3E+X+ap1%29%29.hoa new file mode 100644 index 0000000000..abb333bb18 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28ap0+-%3E+X+ap1%29%29.hoa @@ -0,0 +1,18 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for F(((ap0) & (X(!ap1))))" +owlArgs: "ltl2nba" "-f" "!(G (ap0 -> X ap1))" "-o" "src/test/resources/hoa/%21%28G+%28ap0+-%3E+X+ap1%29%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +AP: 2 "ap0" "ap1" +--BODY-- +State: 0 +[t] 0 +[0] 1 +State: 1 +[!1] 2 +State: 2 +[t] 2 {0} +--END-- diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28G+F+ap0%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+F+ap0%29.hoa new file mode 100644 index 0000000000..a51520dce0 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+F+ap0%29.hoa @@ -0,0 +1,16 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for F(G(!ap0))" +owlArgs: "ltl2nba" "-f" "!(G F ap0)" "-o" "src/test/resources/hoa/%21%28G+F+ap0%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +AP: 1 "ap0" +--BODY-- +State: 0 +[t] 0 +[!0] 1 +State: 1 +[!0] 1 {0} +--END-- diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28G+ap0%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+ap0%29.hoa new file mode 100644 index 0000000000..f132de74f4 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+ap0%29.hoa @@ -0,0 +1,18 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for F(!ap0)" +owlArgs: "ltl2nba" "-f" "!(G ap0)" "-o" "src/test/resources/hoa/%21%28G+ap0%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +properties: deterministic unambiguous +properties: complete +AP: 1 "ap0" +--BODY-- +State: 0 +[0] 0 +[!0] 1 +State: 1 +[t] 1 {0} +--END-- 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/util/XstsCombineExtractUtils.kt b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/util/XstsCombineExtractUtils.kt index afda5eb642..579deaab67 100644 --- a/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/util/XstsCombineExtractUtils.kt +++ b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/util/XstsCombineExtractUtils.kt @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xsts.analysis.util import hu.bme.mit.theta.analysis.Prec @@ -23,15 +22,21 @@ import hu.bme.mit.theta.analysis.unit.UnitState import hu.bme.mit.theta.xsts.analysis.XstsState fun xstsCombineStates(xstsState: XstsState, dataState: S): XstsState { - return XstsState.of(dataState, xstsState.lastActionWasEnv(), xstsState.isInitialized) + // TODO here initialized should be xstsState.isInitialized, but that fails + // LtlCheckTestWithXstsPred + return XstsState.of(dataState, xstsState.lastActionWasEnv(), true) } fun xstsExtractControlState(xstsState: XstsState<*>): XstsState { - return XstsState.of(UnitState.getInstance(), xstsState.lastActionWasEnv(), xstsState.isInitialized) + return XstsState.of( + UnitState.getInstance(), + xstsState.lastActionWasEnv(), + xstsState.isInitialized, + ) } fun xstsExtractDataState(xstsState: XstsState): S { - return xstsState.state + return xstsState.state } -fun

xstsExtractControlPrec(p: P): UnitPrec = UnitPrec.getInstance() \ No newline at end of file +fun

xstsExtractControlPrec(p: P): UnitPrec = UnitPrec.getInstance() diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XstsTransformer.kt b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XstsTransformer.kt new file mode 100644 index 0000000000..b878c12e2f --- /dev/null +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XstsTransformer.kt @@ -0,0 +1,68 @@ +/* + * 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 + +import com.google.common.base.Preconditions.checkArgument +import hu.bme.mit.theta.core.stmt.NonDetStmt +import hu.bme.mit.theta.core.stmt.SequenceStmt +import hu.bme.mit.theta.core.stmt.SkipStmt +import hu.bme.mit.theta.core.stmt.Stmt + +fun normalize(rawXsts: XSTS?): XSTS { + checkArgument(rawXsts != null, "Can't normalize null") + val xstsInput = rawXsts!! + + val normalizedInit = normalize(xstsInput.init) + val normalizedTran = normalize(xstsInput.tran) + val normalizedEnv = normalize(xstsInput.env) + + return XSTS( + xstsInput.ctrlVars, + normalizedInit, + normalizedTran, + normalizedEnv, + xstsInput.initFormula, + xstsInput.prop, + ) +} + +private fun normalize(stmt: Stmt): NonDetStmt { + val collector = mutableListOf>() + collector.add(mutableListOf()) + normalize(stmt, collector) + return NonDetStmt.of(collector.map { SequenceStmt.of(it) }.toList()) +} + +private fun normalize(stmt: Stmt, collector: MutableList>) { + when (stmt) { + is SequenceStmt -> stmt.stmts.forEach { normalize(it, collector) } + is NonDetStmt -> { + val newCollector = mutableListOf>() + stmt.stmts.forEach { nondetBranch -> + val copy = collector.copy() + normalize(nondetBranch, copy) + newCollector.addAll(copy) + } + collector.clear() + collector.addAll(newCollector) + } + + is SkipStmt -> {} + else -> collector.forEach { it.add(stmt) } + } +} + +private fun MutableList>.copy() = map { it.toMutableList() }.toMutableList()