Adjusted LazyXtaCheckerTest to the new checker interface

ftsrg · Feb 13, 2024 · 23d3926 · 23d3926
1 parent 95bc59c
commit 23d3926
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 8 deletions.
diff --git a/.../xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaCheckerFactory.java b/.../xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaCheckerFactory.java
@@ -29,10 +29,10 @@ public final class LazyXtaCheckerFactory {
 	private LazyXtaCheckerFactory() {
 	}
 
-	public static SafetyChecker<? extends ARG<?, ?>, ? extends Trace<?, ?>, UnitPrec> create(final XtaSystem system,
+	public static SafetyChecker<? extends ARG<? extends XtaState<?>, XtaAction>, ? extends Trace<? extends XtaState<?>, XtaAction>, UnitPrec> create(final XtaSystem system,
 																											 final DataStrategy dataStrategy, final ClockStrategy clockStrategy, final SearchStrategy searchStrategy) {
 		final CombinedStrategy<?, ?> algorithmStrategy = combineStrategies(system, dataStrategy, clockStrategy);
-		final SafetyChecker<? extends ARG<?,?>, ? extends Trace<?, ?>, UnitPrec> checker = LazyXtaChecker.create(system,
+		final SafetyChecker<? extends ARG<? extends XtaState<?>,XtaAction>, ? extends Trace<? extends XtaState<?>, XtaAction>, UnitPrec> checker = LazyXtaChecker.create(system,
 				algorithmStrategy, searchStrategy);
 		return checker;
 	}

diff --git a/...ects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java b/...ects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java
@@ -17,9 +17,11 @@
 
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
-import hu.bme.mit.theta.analysis.algorithm.ArgChecker;
-import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
+import hu.bme.mit.theta.analysis.Trace;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgChecker;
+import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
 import hu.bme.mit.theta.analysis.unit.UnitPrec;
 import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
 import hu.bme.mit.theta.xta.XtaSystem;
@@ -39,7 +41,7 @@
 import java.util.ArrayList;
 import java.util.Collection;
 
-import static hu.bme.mit.theta.analysis.algorithm.SearchStrategy.BFS;
+import static hu.bme.mit.theta.analysis.algorithm.arg.SearchStrategy.BFS;
 import static hu.bme.mit.theta.xta.analysis.lazy.ClockStrategy.LU;
 import static org.junit.Assert.assertTrue;
 
@@ -67,7 +69,7 @@ public final class LazyXtaCheckerTest {
 	@Parameter(2)
 	public ClockStrategy clockStrategy;
 
-	private SafetyChecker<? extends XtaState<?>, XtaAction, UnitPrec> checker;
+	private SafetyChecker<? extends ARG<? extends XtaState<?>, XtaAction>, ? extends Trace<? extends XtaState<?>, XtaAction>, UnitPrec> checker;
 
 	@Parameters(name = "model: {0}, discrete: {1}, clock: {2}")
 	public static Collection<Object[]> data() {
@@ -94,11 +96,11 @@ public void initialize() throws IOException {
 	@Test
 	public void test() {
 		// Act
-		final SafetyResult<? extends XtaState<?>, XtaAction> status = checker.check(UnitPrec.getInstance());
+		final SafetyResult<? extends ARG<? extends XtaState<?>, XtaAction>, ? extends Trace<? extends XtaState<?>, XtaAction>> status = checker.check(UnitPrec.getInstance());
 
 		// Assert
 		final ArgChecker argChecker = ArgChecker.create(Z3SolverFactory.getInstance().createSolver());
-		final boolean argCheckResult = argChecker.isWellLabeled(status.getArg());
+		final boolean argCheckResult = argChecker.isWellLabeled(status.getWitness());
 		assertTrue(argCheckResult);
 	}