diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/AcceptancePredicate.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/AcceptancePredicate.kt index 2cc1039031..3a85f7a45d 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/AcceptancePredicate.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/AcceptancePredicate.kt @@ -1,5 +1,5 @@ /* - * Copyright 2023 Budapest University of Technology and Economics + * 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. @@ -13,55 +13,36 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm.loopchecker; -import hu.bme.mit.theta.analysis.expr.ExprAction; -import hu.bme.mit.theta.analysis.expr.ExprState; +package hu.bme.mit.theta.analysis.algorithm.loopchecker -import java.util.function.Predicate; +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.State +import java.util.function.Predicate -public final class AcceptancePredicate { - private final Predicate statePredicate; - private final Predicate actionPredicate; +class AcceptancePredicate( + private val statePredicate: ((S?) -> Boolean)? = null, + private val actionPredicate: ((A?) -> Boolean)? = null, +) : Predicate> { - private AcceptancePredicate(Predicate statePredicate, Predicate actionPredicate) { - this.statePredicate = statePredicate; - this.actionPredicate = actionPredicate; - } + constructor(statePredicate: (S?) -> Boolean = { _ -> true }, a: Unit) : this(statePredicate) { - public static AcceptancePredicate ofStatePredicate(Predicate statePredicate) { - return new AcceptancePredicate<>(statePredicate, null); - } + } - public static AcceptancePredicate ofActionPredicate(Predicate actionPredicate) { - return new AcceptancePredicate<>(null, actionPredicate); - } + fun testState(state: S): Boolean { + return statePredicate?.invoke(state) ?: false + } - public static AcceptancePredicate ofCombinedPredicate(Predicate statePredicate, Predicate actionPredicate) { - return new AcceptancePredicate<>(statePredicate, actionPredicate); - } + fun testAction(action: A) = actionPredicate?.invoke(action) ?: false - public static AcceptancePredicate alwaysTrue() { - return new AcceptancePredicate<>(null, null); - } - - public boolean test(S state, A action) { - if (statePredicate == null && action == null) - return false; - return (statePredicate == null || statePredicate.test(state)) && (actionPredicate == null || (action !=null && actionPredicate.test(action))); - } - - public boolean testState(S state) { - if (statePredicate == null || state == null) - return false; - return statePredicate.test(state); - } - - public boolean testAction(A action) { - if (actionPredicate == null || action == null) - return false; - return actionPredicate.test(action); - } + override fun test(t: Pair): Boolean { + val state = t.first + val action = t.second + if (statePredicate == null && action == null) return false + return (statePredicate == null || statePredicate.invoke( + state + )) && (actionPredicate == null || (action != null && actionPredicate.invoke(action))) + } } \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractor.java index 9a3c79419a..6f8c4fc973 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractor.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractor.java @@ -1,5 +1,5 @@ /* - * Copyright 2023 Budapest University of Technology and Economics + * 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. @@ -29,6 +29,7 @@ import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.NullLogger; +import kotlin.Pair; import java.util.*; import java.util.function.Function; @@ -122,7 +123,7 @@ private List> redSearch(LDGNode seed, LDGEdge edge, Li private Collection> blueSearch(LDGEdge edge, LinkedList> trace, Collection> blueNodes, Set> redNodes) { var targetNode = edge.target(); trace.add(edge); - if (target.test(targetNode.getState(), edge.action())) { + if (target.test(new Pair<>(targetNode.getState(), edge.action()))) { var accNode = targetNode.isAccepting() ? targetNode : edge.source(); List> redSearch = redSearch(accNode, edge, new LinkedList<>(trace), Containers.createSet()); if (!redSearch.isEmpty()) diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java index cc01c058fc..0f491da456 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java @@ -1,5 +1,5 @@ /* - * Copyright 2023 Budapest University of Technology and Economics + * 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. @@ -36,11 +36,12 @@ 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.z3.Z3SolverFactory; +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.analysis.*; import hu.bme.mit.theta.xsts.analysis.initprec.XstsAllVarsInitPrec; import hu.bme.mit.theta.xsts.dsl.XstsDslManager; +import kotlin.Unit; import org.junit.Assert; import org.junit.Test; import org.junit.runner.RunWith; @@ -101,11 +102,11 @@ private void testWithXsts() throws IOException { try (InputStream inputStream = new SequenceInputStream(new FileInputStream(String.format("src/test/resources/xsts/%s", fileName)), new FileInputStream(String.format("src/test/resources/prop/%s", propFileName)))) { xsts = XstsDslManager.createXsts(inputStream); } - final Solver abstractionSolver = Z3SolverFactory.getInstance().createSolver(); + final Solver abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver(); final Analysis, XstsAction, ExplPrec> analysis = XstsAnalysis.create(ExplStmtAnalysis.create(abstractionSolver, xsts.getInitFormula(), 250)); final LTS, XstsAction> lts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); final Predicate> statePredicate = new XstsStatePredicate<>(new ExplStatePredicate(xsts.getProp(), abstractionSolver)); - final AcceptancePredicate, XstsAction> target = AcceptancePredicate.ofStatePredicate(statePredicate); + final AcceptancePredicate, XstsAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); final ExplPrec precision = new XstsAllVarsInitPrec().createExpl(xsts); var abstractor = LDGAbstractor.create(analysis, lts, target, SearchStrategy.defaultValue(), new ConsoleLogger(Logger.Level.DETAIL)); AbstractorResult result = abstractor.check(LDG.create(List.of(), target), precision); @@ -116,10 +117,10 @@ private void testWithCfa() throws IOException { final CFA cfa = CfaDslManager.createCfa(new FileInputStream(String.format("src/test/resources/cfa/%s", fileName))); final CfaLts lts = CfaConfigBuilder.Encoding.SBE.getLts(cfa.getInitLoc()); final Analysis, CfaAction, CfaPrec> analysis = CfaAnalysis - .create(cfa.getInitLoc(), ExplStmtAnalysis.create(Z3SolverFactory.getInstance().createSolver(), True(), 250)); + .create(cfa.getInitLoc(), ExplStmtAnalysis.create(Z3LegacySolverFactory.getInstance().createSolver(), True(), 250)); final CfaPrec precision = GlobalCfaPrec.create(ExplPrec.of(cfa.getVars())); Predicate> statePredicate = cfaState -> cfaState.getLoc().getName().equals(acceptingLocationName); - AcceptancePredicate, CfaAction> target = AcceptancePredicate.ofStatePredicate(statePredicate); + AcceptancePredicate, CfaAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); LDGAbstractor, CfaAction, CfaPrec> abstractor = LDGAbstractor.create(analysis, lts, target, SearchStrategy.defaultValue(), new ConsoleLogger(Logger.Level.DETAIL)); AbstractorResult result = abstractor.check(LDG.create(List.of(), target), precision); Assert.assertEquals(isLassoPresent, result.isUnsafe()); diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java index cc786341b3..e33e9d33db 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java @@ -1,5 +1,5 @@ /* - * Copyright 2023 Budapest University of Technology and Economics + * 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. @@ -40,10 +40,11 @@ import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.solver.ItpSolver; import hu.bme.mit.theta.solver.Solver; -import hu.bme.mit.theta.solver.z3.Z3SolverFactory; +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.analysis.*; import hu.bme.mit.theta.xsts.dsl.XstsDslManager; +import kotlin.Unit; import org.junit.Assert; import org.junit.BeforeClass; import org.junit.Test; @@ -69,8 +70,8 @@ public class LDGCegarVerifierTest { @BeforeClass public static void init() { - abstractionSolver = Z3SolverFactory.getInstance().createSolver(); - itpSolver = Z3SolverFactory.getInstance().createItpSolver(); + abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver(); + itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver(); logger = new ConsoleLogger(Logger.Level.INFO); } @@ -118,7 +119,7 @@ private void testWithXsts() throws IOException { final Analysis, XstsAction, PredPrec> analysis = XstsAnalysis.create(PredAnalysis.create(abstractionSolver, PredAbstractors.booleanSplitAbstractor(abstractionSolver), xsts.getInitFormula())); final LTS, XstsAction> lts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); final Predicate> statePredicate = new XstsStatePredicate<>(new ExprStatePredicate(xsts.getProp(), abstractionSolver)); - final AcceptancePredicate, XstsAction> target = AcceptancePredicate.ofStatePredicate(statePredicate); + final AcceptancePredicate, XstsAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); logger.write(Logger.Level.MAINSTEP, "Verifying %s%n", xsts.getProp()); var abstractor = LDGAbstractor.create(analysis, lts, target, SearchStrategy.defaultValue(), logger); final Refiner, XstsAction, PredPrec, LDG, XstsAction>, LDGTrace, XstsAction>> refiner = BasicLDGTraceRefiner.create(itpSolver, new ItpRefToPredPrec(ExprSplitters.atoms()), RefinerStrategy.defaultValue(), logger); @@ -135,7 +136,7 @@ private void testWithCfa() throws IOException { final Analysis, CfaAction, CfaPrec> analysis = CfaAnalysis .create(cfa.getInitLoc(), PredAnalysis.create(abstractionSolver, PredAbstractors.booleanSplitAbstractor(abstractionSolver), True())); final Predicate> statePredicate = cfaState -> cfaState.getLoc().getName().equals(acceptingLocationName); - final AcceptancePredicate, CfaAction> target = AcceptancePredicate.ofStatePredicate(statePredicate); + final AcceptancePredicate, CfaAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); final RefutationToPrec refToPrec = new ItpRefToPredPrec(ExprSplitters.atoms()); final RefutationToGlobalCfaPrec cfaRefToPrec = new RefutationToGlobalCfaPrec<>(refToPrec, cfa.getInitLoc()); var abstractor = LDGAbstractor.create(analysis, lts, target, SearchStrategy.defaultValue(), logger); diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java index f6463bf46f..6868890328 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java @@ -1,5 +1,5 @@ /* - * Copyright 2023 Budapest University of Technology and Economics + * 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. @@ -30,10 +30,11 @@ import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.solver.ItpSolver; import hu.bme.mit.theta.solver.Solver; -import hu.bme.mit.theta.solver.z3.Z3SolverFactory; +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.analysis.*; import hu.bme.mit.theta.xsts.dsl.XstsDslManager; +import kotlin.Unit; import org.junit.Assert; import org.junit.Test; @@ -41,7 +42,6 @@ import java.io.IOException; import java.io.InputStream; import java.io.SequenceInputStream; -import java.util.Collection; import java.util.List; import java.util.function.Predicate; @@ -52,12 +52,12 @@ public void testWithCounter3() throws IOException { try (InputStream inputStream = new SequenceInputStream(new FileInputStream("src/test/resources/xsts/counter3.xsts"), new FileInputStream("src/test/resources/prop/x_eq_3.prop"))) { xsts = XstsDslManager.createXsts(inputStream); } - final ItpSolver itpSolver = Z3SolverFactory.getInstance().createItpSolver(); - final Solver abstractionSolver = Z3SolverFactory.getInstance().createSolver(); + final ItpSolver itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver(); + final Solver abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver(); final Analysis, XstsAction, PredPrec> analysis = XstsAnalysis.create(PredAnalysis.create(abstractionSolver, PredAbstractors.booleanAbstractor(abstractionSolver), xsts.getInitFormula())); final LTS, XstsAction> lts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); final Predicate> statePredicate = new XstsStatePredicate<>(new ExprStatePredicate(xsts.getProp(), abstractionSolver)); - final AcceptancePredicate, XstsAction> target = AcceptancePredicate.ofStatePredicate(statePredicate); + final AcceptancePredicate, XstsAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); final PredPrec precision = PredPrec.of(); final Logger logger = new ConsoleLogger(Logger.Level.DETAIL); final LDGAbstractor, XstsAction, PredPrec> abstractor = LDGAbstractor.create(analysis, lts, target, SearchStrategy.defaultValue(), logger); diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGAbstractorTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGAbstractorTest.java index 20209a46a1..6cdd277ddc 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGAbstractorTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGAbstractorTest.java @@ -1,5 +1,5 @@ /* - * Copyright 2023 Budapest University of Technology and Economics + * 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. @@ -30,7 +30,7 @@ import org.mockito.Mock; import org.mockito.junit.MockitoJUnitRunner; -import static org.mockito.Mockito.*; +import static org.mockito.Mockito.mock; @RunWith(MockitoJUnitRunner.class) public class LDGAbstractorTest { @@ -47,7 +47,7 @@ public class LDGAbstractorTest { public void testConnectTwoNodes() { LDGNode from = LDGNode.of(fromState, true); LDGNode to = LDGNode.of(toState, true); - LDGAbstractor abstractor = LDGAbstractor.create((Analysis) mock(Analysis.class), (LTS) mock(LTS.class), AcceptancePredicate.alwaysTrue(), SearchStrategy.defaultValue(), NullLogger.getInstance()); + LDGAbstractor abstractor = LDGAbstractor.create((Analysis) mock(Analysis.class), (LTS) mock(LTS.class), new AcceptancePredicate<>(), SearchStrategy.defaultValue(), NullLogger.getInstance()); LDGEdge edge = abstractor.connectTwoNodes(from, to, actionFromTo); diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlCheck.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlCheck.kt index af3996687c..75971d1b9f 100644 --- a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlCheck.kt +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlCheck.kt @@ -16,15 +16,13 @@ package hu.bme.mit.theta.common.ltl -import hu.bme.mit.theta.analysis.* +import hu.bme.mit.theta.analysis.Analysis +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.SafetyResult import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker -import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGAbstractor -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTraceRefinerSupplier -import hu.bme.mit.theta.analysis.algorithm.loopchecker.RefinerStrategy -import hu.bme.mit.theta.analysis.algorithm.loopchecker.SearchStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.* import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.analysis.expr.StmtAction @@ -163,7 +161,7 @@ object LtlCheck { } private fun buchiPredicate(buchiAutomaton: CFA) : AcceptancePredicate, D>, StmtMultiAction> { - return AcceptancePredicate.ofActionPredicate { a -> (a.rightAction != null && a.rightAction.edges.any { e -> buchiAutomaton.acceptingEdges.contains(e) }) } + return AcceptancePredicate { a -> (a?.rightAction != null && a.rightAction.edges.any { e -> buchiAutomaton.acceptingEdges.contains(e) }) } } }