benchmarks

ftsrg · May 16, 2024 · 4eb4a45 · 4eb4a45
1 parent fd1a5cd
commit 4eb4a45
Show file tree

Hide file tree

Showing 29 changed files with 3,488 additions and 16 deletions.
diff --git a/...mon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java b/...mon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java
@@ -86,7 +86,6 @@ public AbstractorResult check(final ARG<S, A> arg, final P prec) {
 
 		long startNodes = arg.getNodes().count();
 		long startIncompleteNodes = arg.getIncompleteNodes().count();
-
 		ArgCexCheckHandler.instance.setCurrentArg(new AbstractArg<S, A, P>(arg, prec));
 		logger.write(Level.INFO, "|  |  Starting ARG: %d nodes, %d incomplete, %d unsafe%n", arg.getNodes().count(),
 				arg.getIncompleteNodes().count(), arg.getUnsafeNodes().count());

diff --git a/subprojects/xta/xta-analysis/build.gradle.kts b/subprojects/xta/xta-analysis/build.gradle.kts
@@ -1,6 +1,5 @@
 plugins {
     id("java-common")
-    id("cli-tool")
 }
 
 dependencies {

diff --git a/...analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/SingleXtaTraceRefiner.java b/...analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/SingleXtaTraceRefiner.java
@@ -104,7 +104,6 @@ public RefinerResult<XtaState<Prod2State<S, ZoneState>>, XtaAction, XtaPrec<Prod
 
         assert cexZoneStatus.isFeasible() || cexZoneStatus.isInfeasible() : "Unknown CEX status";
         assert cexExprStatus.isFeasible() || cexExprStatus.isInfeasible() : "Unknown CEX status";
-
         if (cexZoneStatus.isFeasible() && cexExprStatus.isFeasible()) { // if any of traces are feasible than it is unsafe
             return RefinerResult.unsafe(traceToConcretize);
         } else {

diff --git a/...jects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/ConfigEnum.java b/...jects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/ConfigEnum.java
@@ -0,0 +1,29 @@
+package hu.bme.mit.theta.xta.analysis.config;
+
+import hu.bme.mit.theta.analysis.algorithm.ArgNodeComparators;
+
+public class ConfigEnum {
+    public enum Domain {
+        EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT
+    }
+
+    public enum Refinement {
+        FW_BIN_ITP, BW_BIN_ITP, SEQ_ITP, MULTI_SEQ, UNSAT_CORE, UCB,
+        NWT_WP, NWT_SP, NWT_WP_LV, NWT_SP_LV, NWT_IT_WP, NWT_IT_SP, NWT_IT_WP_LV, NWT_IT_SP_LV
+    }
+    public enum InitPrec {
+        EMPTY, ALLVARS, ALLASSUMES
+    }
+    public enum Search {
+        BFS(ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())),
+
+        DFS(ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.dfs()));
+
+        public final ArgNodeComparators.ArgNodeComparator comparator;
+
+        private Search(final ArgNodeComparators.ArgNodeComparator comparator) {
+            this.comparator = comparator;
+        }
+
+    }
+}
diff --git a/...alysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java b/...alysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java
@@ -146,15 +146,29 @@ public XtaConfigBuilder_ClockPred search(final Search search) {
         this.search = search;
         return this;
     }
+    public XtaConfigBuilder_ClockPred search(final String search) {
+        this.search = Search.valueOf(search);
+        return this;
+    }
     public XtaConfigBuilder_ClockPred predSplit(final PredSplit predSplit) {
         this.predSplit = predSplit;
         return this;
     }
+
+    public XtaConfigBuilder_ClockPred predSplit(final String predSplit) {
+        this.predSplit = PredSplit.valueOf(predSplit);
+        return this;
+    }
     public XtaConfigBuilder_ClockPred precGranularity(final PrecGranularity precGranularity) {
         this.precGranularity = precGranularity;
 
         return this;
     }
+    public XtaConfigBuilder_ClockPred precGranularity(final String precGranularity) {
+        this.precGranularity = PrecGranularity.valueOf(precGranularity);
+
+        return this;
+    }
     public XtaConfigBuilder_ClockPred maxEnum(final int maxEnum) {
         this.maxEnum = maxEnum;
         return this;
@@ -163,6 +177,10 @@ public XtaConfigBuilder_ClockPred initPrec(final InitPrec initPrec) {
         this.initPrec = initPrec;
         return this;
     }
+    public XtaConfigBuilder_ClockPred initPrec(final String initPrec) {
+        this.initPrec = InitPrec.valueOf(initPrec);
+        return this;
+    }
     public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrategy) {
         this.pruneStrategy = pruneStrategy;
         return this;

diff --git a/...ta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_Zone.java b/...ta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_Zone.java
@@ -140,15 +140,29 @@ public XtaConfigBuilder_Zone search(final Search search) {
         this.search = search;
         return this;
     }
+    public XtaConfigBuilder_Zone search(final String search) {
+        this.search = Search.valueOf(search);
+        return this;
+    }
     public XtaConfigBuilder_Zone predSplit(final PredSplit predSplit) {
         this.predSplit = predSplit;
         return this;
     }
+    public XtaConfigBuilder_Zone predSplit(final String predSplit) {
+        this.predSplit = PredSplit.valueOf(predSplit);
+        return this;
+    }
     public XtaConfigBuilder_Zone precGranularity(final PrecGranularity precGranularity) {
         this.precGranularity = precGranularity;
 
         return this;
     }
+
+    public XtaConfigBuilder_Zone precGranularity(final String precGranularity) {
+        this.precGranularity = PrecGranularity.valueOf(precGranularity);
+
+        return this;
+    }
     public XtaConfigBuilder_Zone maxEnum(final int maxEnum) {
         this.maxEnum = maxEnum;
         return this;
@@ -157,6 +171,10 @@ public XtaConfigBuilder_Zone initPrec(final InitPrec initPrec) {
         this.initPrec = initPrec;
         return this;
     }
+    public XtaConfigBuilder_Zone initPrec(final String initPrec) {
+        this.initPrec = InitPrec.valueOf(initPrec);
+        return this;
+    }
     public XtaConfigBuilder_Zone pruneStrategy(final PruneStrategy pruneStrategy) {
         this.pruneStrategy = pruneStrategy;
         return this;

diff --git a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/Test_ClockPred.java b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/Test_ClockPred.java
@@ -3,6 +3,7 @@
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
 import hu.bme.mit.theta.common.OsHelper;
 import hu.bme.mit.theta.common.logging.ConsoleLogger;
+import hu.bme.mit.theta.common.logging.FileLogger;
 import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.solver.SolverFactory;
 import hu.bme.mit.theta.solver.SolverManager;
@@ -42,7 +43,7 @@ public void check() throws Exception{
         refinement = XtaConfigBuilder_ClockPred.Refinement.SEQ_ITP;
         SolverManager.registerSolverManager(Z3SolverManager.create());
         if(OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX)) {
-            SolverManager.registerSolverManager(SmtLibSolverManager.create(SmtLibSolverManager.HOME, new ConsoleLogger(Logger.Level.DETAIL)));
+            SolverManager.registerSolverManager(SmtLibSolverManager.create(SmtLibSolverManager.HOME, new FileLogger(Logger.Level.DETAIL, "clockpred.log", false, false)));
         }
 
         final SolverFactory solverFactory;
@@ -51,15 +52,18 @@ public void check() throws Exception{
 
         XtaSystem system;
         try(InputStream inputStream =  new SequenceInputStream(new FileInputStream("src/test/resources/model/ClockPredTest.xta"), new FileInputStream("src/test/resources/property/ClockPredTest.prop"))){
-            system = XtaDslManager.createSystem(inputStream);
+            system = XtaDslManager.createSystem(new FileInputStream("src/test/resources/model/ClockPredTest.xta"));
         }
         XtaConfigBuilder_ClockPred builder =  new XtaConfigBuilder_ClockPred(domain, refinement, /*solverFactory*/ Z3SolverFactory.getInstance());
         builder.precGranularity(XtaConfigBuilder_ClockPred.PrecGranularity.GLOBAL);
         builder.initPrec(XtaConfigBuilder_ClockPred.InitPrec.EMPTY);
         builder.maxEnum(1);
-
+        builder.logger(new FileLogger(Logger.Level.DETAIL, "clockpred.txt", true, true));
         XtaConfig config = builder.build(system);
         SafetyResult result = config.check();
         System.out.println("Safe?: " + result.isSafe());
+        if(result.isUnsafe()){
+            System.out.println(result.asUnsafe().getTrace());
+        }
     }
 }
diff --git a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/clockpred.log b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/clockpred.log
diff --git a/subprojects/xta/xta-analysis/src/test/resources/model/ClockPredTest.xta b/subprojects/xta/xta-analysis/src/test/resources/model/ClockPredTest.xta
@@ -9,8 +9,6 @@ process P1(){
         A {y <= 1},
         B;
 
-    urgent
-        idle;
 
     init
         idle;
@@ -22,4 +20,7 @@ process P1(){
         A -> B {guard x >= 7   ;assign a = 3;};
 
 }
-system P1;
+system P1;
+prop{
+    E<> P1_B
+}