Skip to content

Commit

Permalink
Adjusted classes to the new checker interface
Browse files Browse the repository at this point in the history
  • Loading branch information
@mondokm
mondokm committed Feb 13, 2024
1 parent 23d3926 commit 1b2d844
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 15 deletions.
17 changes: 9 additions & 8 deletions subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,11 +18,12 @@
import hu.bme.mit.theta.analysis.Analysis;
import hu.bme.mit.theta.analysis.LTS;
import hu.bme.mit.theta.analysis.State;
import hu.bme.mit.theta.analysis.algorithm.ARG;
import hu.bme.mit.theta.analysis.algorithm.ArgBuilder;
import hu.bme.mit.theta.analysis.algorithm.ArgNodeComparators;
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.ArgBuilder;
import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators;
import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor;
import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor;
import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker;
Expand Down Expand Up @@ -56,7 +57,7 @@
import java.util.Collections;
import java.util.function.Predicate;

import static hu.bme.mit.theta.analysis.algorithm.ArgUtils.isWellLabeled;
import static hu.bme.mit.theta.analysis.algorithm.arg.ArgUtils.isWellLabeled;
import static hu.bme.mit.theta.core.decl.Decls.Var;
import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime;
import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And;
Expand Down Expand Up @@ -115,11 +116,11 @@ public void test() {
final SingleExprTraceRefiner<ExplState, StsAction, ExplPrec, VarsRefutation> refiner = SingleExprTraceRefiner
.create(exprTraceChecker, JoiningPrecRefiner.create(new VarsRefToExplPrec()), PruneStrategy.LAZY, logger);

final SafetyChecker<ExplState, StsAction, ExplPrec> checker = CegarChecker.create(abstractor, refiner, logger);
final SafetyChecker<ARG<ExplState, StsAction>, Trace<ExplState, StsAction>, ExplPrec> checker = CegarChecker.create(abstractor, refiner, logger);

final SafetyResult<ExplState, StsAction> safetyStatus = checker.check(prec);
final SafetyResult<ARG<ExplState, StsAction>, Trace<ExplState, StsAction>> safetyStatus = checker.check(prec);

final ARG<ExplState, StsAction> arg = safetyStatus.getArg();
final ARG<ExplState, StsAction> arg = safetyStatus.getWitness();
assertTrue(isWellLabeled(arg, abstractionSolver));

// System.out.println(new
Expand Down
15 changes: 8 additions & 7 deletions subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@
*/
package hu.bme.mit.theta.sts.analysis;

import static hu.bme.mit.theta.analysis.algorithm.ArgUtils.isWellLabeled;
import static hu.bme.mit.theta.analysis.algorithm.arg.ArgUtils.isWellLabeled;
import static hu.bme.mit.theta.core.decl.Decls.Var;
import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime;
import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And;
Expand All @@ -30,6 +30,8 @@

import java.util.function.Predicate;

import hu.bme.mit.theta.analysis.Trace;
import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
import hu.bme.mit.theta.analysis.expr.refinement.*;
import hu.bme.mit.theta.solver.ItpSolver;
import hu.bme.mit.theta.solver.Solver;
Expand All @@ -39,10 +41,9 @@
import hu.bme.mit.theta.analysis.Analysis;
import hu.bme.mit.theta.analysis.LTS;
import hu.bme.mit.theta.analysis.State;
import hu.bme.mit.theta.analysis.algorithm.ARG;
import hu.bme.mit.theta.analysis.algorithm.ArgBuilder;
import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor;
import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor;
import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker;
Expand Down Expand Up @@ -109,12 +110,12 @@ public void testPredPrec() {
.create(exprTraceChecker, JoiningPrecRefiner.create(new ItpRefToPredPrec(ExprSplitters.atoms())),
PruneStrategy.LAZY, logger);

final SafetyChecker<PredState, StsAction, PredPrec> checker = CegarChecker.create(abstractor, refiner, logger);
final SafetyChecker<ARG<PredState, StsAction>, Trace<PredState, StsAction>, PredPrec> checker = CegarChecker.create(abstractor, refiner, logger);

final SafetyResult<PredState, StsAction> safetyStatus = checker.check(prec);
final SafetyResult<ARG<PredState, StsAction>, Trace<PredState, StsAction>> safetyStatus = checker.check(prec);
System.out.println(safetyStatus);

final ARG<PredState, StsAction> arg = safetyStatus.getArg();
final ARG<PredState, StsAction> arg = safetyStatus.getWitness();
assertTrue(isWellLabeled(arg, abstractionSolver));

// System.out.println(new
Expand Down

0 comments on commit 1b2d844

Please sign in to comment.