Fix #76

CinRC · May 1, 2023 · 1345b89 · 1345b89
1 parent cfa51b6
commit 1345b89
Show file tree

Hide file tree

Showing 7 changed files with 67 additions and 3 deletions.
diff --git a/pom.xml b/pom.xml
@@ -6,7 +6,7 @@
 
     <groupId>org.cinrc</groupId>
     <artifactId>IRDC</artifactId>
-    <version>4.3.6.1</version>
+    <version>4.3.7.1</version>
 
     <packaging>jar</packaging>
     <properties>

diff --git a/src/main/java/org/cinrc/process/ProcessContainer.java b/src/main/java/org/cinrc/process/ProcessContainer.java
@@ -1,11 +1,15 @@
 package org.cinrc.process;
 
 import java.util.Collection;
+import java.util.Iterator;
 import org.cinrc.parser.CCSTransitionException;
 import org.cinrc.process.nodes.Label;
 import org.cinrc.process.nodes.LabelKey;
 import org.cinrc.process.nodes.NodeIDGenerator;
+import org.cinrc.process.nodes.TauLabelNode;
+import org.cinrc.process.process.ComplexProcess;
 import org.cinrc.process.process.Process;
+import org.cinrc.util.SetUtil;
 
 public class ProcessContainer {
 
@@ -21,6 +25,7 @@ public String prettyString() {
 
   public Collection<Label> getActionableLabels() {
     Collection<Label> labels = process.getActionableLabels();
+    labels = removeUnsyncableKeys(labels);
 
     return labels;
   }
@@ -30,6 +35,32 @@ public boolean canAct(Label node) {
     return l.contains(node);
   }
 
+  protected Collection<Label> removeUnsyncableKeys(Collection<Label> labels){
+    if (!(process instanceof ComplexProcess cp))
+      return labels;
+    Iterator<Label> iter = labels.iterator();
+    while (iter.hasNext()) {
+      Label l = iter.next();
+      if (!(l instanceof LabelKey key))//we only care about keys
+      {
+        continue;
+      }
+      if (!(key.from instanceof TauLabelNode)) {
+        continue; //don't care about regular keys
+      }
+      try {
+        if (!cp.recursiveIsSyncable(key))//both sides need to be able to do it
+        {
+          iter.remove();
+        }
+      } catch (Exception e) {
+        e.printStackTrace();
+      }
+    }
+    return labels;
+  }
+
+
   public void act(Label node) {
     process = process.act(node);
   }

diff --git a/src/main/java/org/cinrc/process/nodes/LabelFactory.java b/src/main/java/org/cinrc/process/nodes/LabelFactory.java
@@ -99,7 +99,7 @@ public static Label createLabel(String channel, int dupe) {
   }
 
 
-  public static String stripTau(String s){
+  private static String stripTau(String s){
     //Tau{a...}
     //Strips first 4 and last 1 characters
     Matcher m = CCSGrammar.LABEL_TAU.match(s);

diff --git a/src/main/java/org/cinrc/process/process/ComplexProcess.java b/src/main/java/org/cinrc/process/process/ComplexProcess.java
@@ -6,6 +6,7 @@
 import org.cinrc.IRDC;
 import org.cinrc.parser.CCSGrammar;
 import org.cinrc.process.nodes.Label;
+import org.cinrc.process.nodes.LabelKey;
 import org.cinrc.util.RCCSFlag;
 import org.cinrc.util.SetUtil;
 
@@ -164,6 +165,21 @@ public String origin() {
     return b.toString();
   }
 
+  public boolean recursiveIsSyncable(LabelKey key){
+    if (left.canAct(key) && right.canAct(key)){
+      return true;
+    }
+    if (left instanceof ComplexProcess cp)
+      if (cp.recursiveIsSyncable(key))
+        return true;
+    if (right instanceof ComplexProcess cp)
+      if (cp.recursiveIsSyncable(key))
+        return true;
+
+    return false;
+
+  }
+
   public boolean hasKey() {
     if (left == null || right == null) {
       return false;

diff --git a/src/main/java/org/cinrc/process/process/ConcurrentProcess.java b/src/main/java/org/cinrc/process/process/ConcurrentProcess.java
@@ -1,7 +1,10 @@
 package org.cinrc.process.process;
 
+import static org.cinrc.util.SetUtil.removeUnsyncableKeys;
+
 import java.util.ArrayList;
 import java.util.Collection;
+import java.util.Iterator;
 import java.util.LinkedList;
 import java.util.List;
 import org.cinrc.parser.CCSParserException;
@@ -114,6 +117,7 @@ public Collection<Label> getActionableLabels() {
     if (!prefixes.isEmpty()) {
       return l;
     }
+
     l.addAll(getActionableLabelsStrict());
     l.addAll(collectSynchronizations(l));
     l = removeRestrictions(l);
@@ -137,6 +141,7 @@ protected List<TauLabelNode> collectSynchronizations(Collection<Label> labels){
     return n;
   }
 
+
   public Process attemptRewind(LabelKey key) {
     if (getLeftRightLabels().stream().noneMatch(LabelKey.class::isInstance))//no keys left/right?
     {

diff --git a/src/main/java/org/cinrc/util/SetUtil.java b/src/main/java/org/cinrc/util/SetUtil.java
@@ -65,7 +65,6 @@ public static Collection<TauLabelNode> getTauMatches(Collection<Label> nodes) {
   }
 
   //Not sure why, but this no longer is feasible.
-  @Deprecated
   public static Collection<Label> removeUnsyncableKeys(ComplexProcess p, Collection<Label> labels) {
     Iterator<Label> iter = labels.iterator();
     while (iter.hasNext()) {

diff --git a/src/test/java/tests/ActionTest.java b/src/test/java/tests/ActionTest.java
@@ -78,4 +78,17 @@ public void testAdvancedActions() {
     assert !p.canAct(b) && !p.canAct(d);
   }
 
+  @Test
+  public void tauTest1(){
+    Process p = new CCSParser().parseLine("Tau{a}[k1] | Tau{a}[k1].Tau{b}[k2] | Tau{b}[k2]");
+    Label key2 = LabelFactory.createDebugLabel("Tau{b}[k2]");
+    Label key1 = LabelFactory.createDebugLabel("Tau{a}[k1]");
+    ProcessContainer pc = new ProcessContainer(p);
+    assert (pc.canAct(key2));
+    assert !(pc.canAct(key1));
+    pc.act(key2);
+    assert pc.canAct(key1);
+
+  }
+
 }