[PSym] Correct symbolic strategy name, bump version

p-org · Oct 14, 2023 · e43c2f1 · e43c2f1
1 parent ae305b0
commit e43c2f1
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 4 deletions.
diff --git a/Src/PCompiler/CompilerCore/Backend/Symbolic/Constants.cs b/Src/PCompiler/CompilerCore/Backend/Symbolic/Constants.cs
@@ -62,7 +62,7 @@ internal class Constants
         <dependency>
             <groupId>io.github.p-org</groupId>
             <artifactId>psym</artifactId>
-            <version>[1.1.3,)</version>
+            <version>[1.1.4,)</version>
         </dependency>
 
         <!-- https://mvnrepository.com/artifact/org.projectlombok/lombok -->

diff --git a/Src/PRuntimes/PSymRuntime/pom.xml b/Src/PRuntimes/PSymRuntime/pom.xml
@@ -327,7 +327,7 @@
         <maven.compiler.target>11</maven.compiler.target>
         <log4j2.configurationFile>${project.basedir}/src/main/resources/log4j2.xml</log4j2.configurationFile>
         <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
-        <revision>1.1.4</revision>
+        <revision>1.1.5</revision>
 
         <deps.path>${project.basedir}/../../../Bld</deps.path>
 

diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymConfiguration.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymConfiguration.java
@@ -33,7 +33,7 @@ public class PSymConfiguration implements Serializable {
   // level of verbosity for the logging
   @Getter @Setter int verbosity = 0;
   // strategy of exploration
-  @Getter @Setter String strategy = "symbolic";
+  @Setter String strategy = "symbolic";
   // max number of executions bound provided by the user
   @Getter @Setter int maxExecutions = 1;
   // max steps/depth bound provided by the user
@@ -84,6 +84,16 @@ public class PSymConfiguration implements Serializable {
   // whether or not to write the program state(s) to file
   @Getter @Setter boolean writeToFile = false;
 
+  public String getStrategy() {
+    String result = this.strategy;
+    if (isSymbolic()) {
+      if (getSchChoiceBound() > 1 || getDataChoiceBound() > 1) {
+        result = this.strategy + "-bounded";
+      }
+    }
+    return result;
+  }
+
   public boolean isSymbolic() {
     return (strategy.startsWith("symbolic"));
   }
@@ -117,7 +127,6 @@ public void setToSymbolicFixpoint() {
 
   public void setToSymbolicBounded() {
     setToSymbolic();
-    this.setStrategy("symbolic-bounded");
     this.setSchChoiceBound(2);
     this.setDataChoiceBound(2);
     this.setUseBacktrack(true);