Convert AcceptancePredicate to kotlin

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<S extends ExprState, A extends ExprAction> {
 
-	private final Predicate<? super S> statePredicate;
-	private final Predicate<? super A> actionPredicate;
+class AcceptancePredicate<S : State, A : Action>(
+    private val statePredicate: ((S?) -> Boolean)? = null,
+    private val actionPredicate: ((A?) -> Boolean)? = null,
+) : Predicate<Pair<S?, A?>> {
 
-	private AcceptancePredicate(Predicate<? super S> statePredicate, Predicate<? super A> actionPredicate) {
-		this.statePredicate = statePredicate;
-		this.actionPredicate = actionPredicate;
-	}
+    constructor(statePredicate: (S?) -> Boolean = { _ -> true }, a: Unit) : this(statePredicate) {
 
-	public static <S extends ExprState, A extends ExprAction> AcceptancePredicate<S, A> ofStatePredicate(Predicate<? super S> statePredicate) {
-		return new AcceptancePredicate<>(statePredicate, null);
-	}
+    }
 
-	public static <S extends ExprState, A extends ExprAction> AcceptancePredicate<S, A> ofActionPredicate(Predicate<? super A> actionPredicate) {
-		return new AcceptancePredicate<>(null, actionPredicate);
-	}
+    fun testState(state: S): Boolean {
+        return statePredicate?.invoke(state) ?: false
+    }
 
-	public static <S extends ExprState, A extends ExprAction> AcceptancePredicate<S, A> ofCombinedPredicate(Predicate<? super S> statePredicate, Predicate<? super A> actionPredicate) {
-		return new AcceptancePredicate<>(statePredicate, actionPredicate);
-	}
+    fun testAction(action: A) = actionPredicate?.invoke(action) ?: false
 
-	public static <S extends ExprState, A extends ExprAction> AcceptancePredicate<S, A> 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<S?, A?>): 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)))
+    }
 
 }

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<LDGEdge<S, A>> redSearch(LDGNode<S, A> seed, LDGEdge<S, A> edge, Li
 	private Collection<LDGTrace<S, A>> blueSearch(LDGEdge<S, A> edge, LinkedList<LDGEdge<S, A>> trace, Collection<LDGNode<S, A>> blueNodes, Set<LDGNode<S, A>> 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<LDGEdge<S, A>> redSearch = redSearch(accNode, edge, new LinkedList<>(trace), Containers.createSet());
 			if (!redSearch.isEmpty())

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<XstsState<ExplState>, XstsAction, ExplPrec> analysis = XstsAnalysis.create(ExplStmtAnalysis.create(abstractionSolver, xsts.getInitFormula(), 250));
 		final LTS<XstsState<ExplState>, XstsAction> lts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create()));
 		final Predicate<XstsState<ExplState>> statePredicate = new XstsStatePredicate<>(new ExplStatePredicate(xsts.getProp(), abstractionSolver));
-		final AcceptancePredicate<XstsState<ExplState>, XstsAction> target = AcceptancePredicate.ofStatePredicate(statePredicate);
+		final AcceptancePredicate<XstsState<ExplState>, 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<CfaState<ExplState>, CfaAction, CfaPrec<ExplPrec>> analysis = CfaAnalysis
-				.create(cfa.getInitLoc(), ExplStmtAnalysis.create(Z3SolverFactory.getInstance().createSolver(), True(), 250));
+				.create(cfa.getInitLoc(), ExplStmtAnalysis.create(Z3LegacySolverFactory.getInstance().createSolver(), True(), 250));
 		final CfaPrec<ExplPrec> precision = GlobalCfaPrec.create(ExplPrec.of(cfa.getVars()));
 		Predicate<CfaState<ExplState>> statePredicate = cfaState -> cfaState.getLoc().getName().equals(acceptingLocationName);
-		AcceptancePredicate<CfaState<ExplState>, CfaAction> target = AcceptancePredicate.ofStatePredicate(statePredicate);
+		AcceptancePredicate<CfaState<ExplState>, CfaAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE);
 		LDGAbstractor<CfaState<ExplState>, CfaAction, CfaPrec<ExplPrec>> 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());

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<XstsState<PredState>, XstsAction, PredPrec> analysis = XstsAnalysis.create(PredAnalysis.create(abstractionSolver, PredAbstractors.booleanSplitAbstractor(abstractionSolver), xsts.getInitFormula()));
 		final LTS<XstsState<PredState>, XstsAction> lts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create()));
 		final Predicate<XstsState<PredState>> statePredicate = new XstsStatePredicate<>(new ExprStatePredicate(xsts.getProp(), abstractionSolver));
-		final AcceptancePredicate<XstsState<PredState>, XstsAction> target = AcceptancePredicate.ofStatePredicate(statePredicate);
+		final AcceptancePredicate<XstsState<PredState>, 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<XstsState<PredState>, XstsAction, PredPrec, LDG<XstsState<PredState>, XstsAction>, LDGTrace<XstsState<PredState>, XstsAction>> refiner = BasicLDGTraceRefiner.create(itpSolver, new ItpRefToPredPrec(ExprSplitters.atoms()), RefinerStrategy.defaultValue(), logger);
@@ -135,7 +136,7 @@ private void testWithCfa() throws IOException {
 		final Analysis<CfaState<PredState>, CfaAction, CfaPrec<PredPrec>> analysis = CfaAnalysis
 				.create(cfa.getInitLoc(), PredAnalysis.create(abstractionSolver, PredAbstractors.booleanSplitAbstractor(abstractionSolver), True()));
 		final Predicate<CfaState<PredState>> statePredicate = cfaState -> cfaState.getLoc().getName().equals(acceptingLocationName);
-		final AcceptancePredicate<CfaState<PredState>, CfaAction> target = AcceptancePredicate.ofStatePredicate(statePredicate);
+		final AcceptancePredicate<CfaState<PredState>, CfaAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE);
 		final RefutationToPrec<PredPrec, ItpRefutation> refToPrec = new ItpRefToPredPrec(ExprSplitters.atoms());
 		final RefutationToGlobalCfaPrec<PredPrec, ItpRefutation> cfaRefToPrec = new RefutationToGlobalCfaPrec<>(refToPrec, cfa.getInitLoc());
         var abstractor = LDGAbstractor.create(analysis, lts, target, SearchStrategy.defaultValue(), logger);

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,18 +30,18 @@
 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;
 
 import java.io.FileInputStream;
 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<XstsState<PredState>, XstsAction, PredPrec> analysis = XstsAnalysis.create(PredAnalysis.create(abstractionSolver, PredAbstractors.booleanAbstractor(abstractionSolver), xsts.getInitFormula()));
 		final LTS<XstsState<PredState>, XstsAction> lts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create()));
 		final Predicate<XstsState<PredState>> statePredicate = new XstsStatePredicate<>(new ExprStatePredicate(xsts.getProp(), abstractionSolver));
-		final AcceptancePredicate<XstsState<PredState>, XstsAction> target = AcceptancePredicate.ofStatePredicate(statePredicate);
+		final AcceptancePredicate<XstsState<PredState>, XstsAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE);
 		final PredPrec precision = PredPrec.of();
 		final Logger logger = new ConsoleLogger(Logger.Level.DETAIL);
 		final LDGAbstractor<XstsState<PredState>, XstsAction, PredPrec> abstractor = LDGAbstractor.create(analysis, lts, target, SearchStrategy.defaultValue(), logger);

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<ExprState, ExprAction> from = LDGNode.of(fromState, true);
 		LDGNode<ExprState, ExprAction> to = LDGNode.of(toState, true);
-		LDGAbstractor<ExprState, ExprAction, ?> abstractor = LDGAbstractor.create((Analysis<ExprState, ExprAction, Prec>) mock(Analysis.class), (LTS<ExprState, ExprAction>) mock(LTS.class), AcceptancePredicate.alwaysTrue(), SearchStrategy.defaultValue(), NullLogger.getInstance());
+		LDGAbstractor<ExprState, ExprAction, ?> abstractor = LDGAbstractor.create((Analysis<ExprState, ExprAction, Prec>) mock(Analysis.class), (LTS<ExprState, ExprAction>) mock(LTS.class), new AcceptancePredicate<>(), SearchStrategy.defaultValue(), NullLogger.getInstance());
 
 		LDGEdge<ExprState, ExprAction> edge = abstractor.connectTwoNodes(from, to, actionFromTo);
 

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 <D : ExprState, S : ExprState, A : StmtAction> buchiPredicate(buchiAutomaton: CFA) : AcceptancePredicate<ExprMultiState<S, CfaState<UnitState>, D>, StmtMultiAction<A, CfaAction>> {
-        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) }) }
     }
 
 }