[PSym] Support liveness checking in symbolic bounded/iterative strategy

Support liveness checking with dynamic machine creation in symbolic bounded/iterative strategy Renames symbolic-iterative to symbolic-bounded
p-org · Oct 14, 2023 · 366a32a · 366a32a
1 parent be54c1f
commit 366a32a
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 24 deletions.
diff --git a/.github/workflows/psymit.yml → .github/workflows/psymb.yml b/.github/workflows/psymit.yml → .github/workflows/psymb.yml
@@ -1,7 +1,7 @@
 # This workflow will build and test PSym in symbolic iterative mode, and cache/restore any dependencies to improve the workflow execution time
 # For more information see: https://help.github.com/actions/language-and-framework-guides/building-and-testing-java-with-maven
 
-name: PSymIt on Ubuntu
+name: PSymB on Ubuntu
 
 on:
   push:
@@ -37,4 +37,4 @@ jobs:
       run: ./scripts/build.sh
     - name: Test PSym
       working-directory: Src/PRuntimes/PSymRuntime
-      run: mvn test -Dpsym.args="--strategy symbolic-iterative"
+      run: mvn test -Dpsym.args="--strategy symbolic-bounded"
diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymConfiguration.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymConfiguration.java
@@ -115,9 +115,9 @@ public void setToSymbolicFixpoint() {
     this.setStateCachingMode(StateCachingMode.Symbolic);
   }
 
-  public void setToSymbolicIterative() {
+  public void setToSymbolicBounded() {
     setToSymbolic();
-    this.setStrategy("symbolic-iterative");
+    this.setStrategy("symbolic-bounded");
     this.setSchChoiceBound(2);
     this.setDataChoiceBound(2);
     this.setUseBacktrack(true);

diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymOptions.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymOptions.java
@@ -105,7 +105,7 @@ public class PSymOptions {
     Option strategy =
         Option.builder("st")
             .longOpt("strategy")
-            .desc("Exploration strategy: symbolic, random, dfs, learn, stateless (default: symbolic)")
+            .desc("Exploration strategy: symbolic, random, dfs, learn (default: symbolic)")
             .numberOfArgs(1)
             .hasArg()
             .argName("Strategy (string)")
@@ -455,8 +455,8 @@ public static PSymConfiguration ParseCommandlineArgs(String[] args) {
             case "symbolic-fixpoint":
               config.setToSymbolicFixpoint();
               break;
-            case "symbolic-iterative":
-              config.setToSymbolicIterative();
+            case "symbolic-bounded":
+              config.setToSymbolicBounded();
               break;
             case "random":
               config.setToRandom();

diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Scheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Scheduler.java
@@ -106,19 +106,6 @@ public boolean isDone() {
     return done.isTrue() || depth == PSymGlobal.getConfiguration().getMaxStepBound();
   }
 
-  /**
-   * Find out whether current execution finished completely
-   *
-   * @return Whether or not current execution finished
-   */
-  public Guard isFinishedExecution() {
-    if (depth == PSymGlobal.getConfiguration().getMaxStepBound()) {
-      return Guard.constTrue();
-    } else {
-      return allMachinesHalted;
-    }
-  }
-
   /**
    * Get current depth
    *
@@ -310,7 +297,8 @@ public void initializeSearch() {
     start = target;
   }
 
-  protected void checkLiveness(Guard finished) {
+  protected void checkLiveness(Guard finished_orig) {
+    Guard finished = finished_orig.and(schedule.getFilter());
     if (!finished.isFalse()) {
       for (Monitor m : monitors) {
         PrimitiveVS<State> monitorState = m.getCurrentState().restrict(finished);

diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/SearchScheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/SearchScheduler.java
@@ -720,7 +720,7 @@ protected List<PrimitiveVS> getNextSchedulingChoices() {
     // prioritize the create actions
     for (Machine machine : machines) {
       if (!machine.getEventBuffer().isEmpty()) {
-        Guard initCond = machine.getEventBuffer().hasCreateMachineUnderGuard().getGuardFor(true);
+        Guard initCond = machine.getEventBuffer().hasCreateMachineUnderGuard().getGuardFor(true).and(schedule.getFilter());
         if (!initCond.isFalse()) {
           PrimitiveVS<Machine> ret = new PrimitiveVS<>(machine).restrict(initCond);
           return new ArrayList<>(Collections.singletonList(ret));
@@ -731,7 +731,7 @@ protected List<PrimitiveVS> getNextSchedulingChoices() {
     // prioritize the sync actions i.e. events that are marked as synchronous
     for (Machine machine : machines) {
       if (!machine.getEventBuffer().isEmpty()) {
-        Guard syncCond = machine.getEventBuffer().hasSyncEventUnderGuard().getGuardFor(true);
+        Guard syncCond = machine.getEventBuffer().hasSyncEventUnderGuard().getGuardFor(true).and(schedule.getFilter());
         if (!syncCond.isFalse()) {
           PrimitiveVS<Machine> ret = new PrimitiveVS<>(machine).restrict(syncCond);
           return new ArrayList<>(Collections.singletonList(ret));
@@ -746,7 +746,7 @@ protected List<PrimitiveVS> getNextSchedulingChoices() {
     for (Machine machine : machines) {
       if (!machine.getEventBuffer().isEmpty()) {
         Guard canRun =
-            machine.getEventBuffer().satisfiesPredUnderGuard(x -> x.canRun()).getGuardFor(true);
+            machine.getEventBuffer().satisfiesPredUnderGuard(x -> x.canRun()).getGuardFor(true).and(schedule.getFilter());
         if (!canRun.isFalse()) {
           guardedMachines.add(new GuardedValue(machine, canRun));
         }