dev to master

Dev

pom.xml

@@ -6,7 +6,7 @@
 
     <groupId>org.cinrc</groupId>
     <artifactId>IRDC</artifactId>
-    <version>4.2.4.1</version>
+    <version>4.3.7.1</version>
 
     <packaging>jar</packaging>
     <properties>

src/main/java/org/cinrc/parser/CCSParser.java

@@ -106,6 +106,7 @@ public static Process generateProcess(Process p, LinkedList<Label> prefixes, Lin
         }
       }else */{
         p.act(key.from);
+        p.setKey(key);
       }
     }
 

src/main/java/org/cinrc/parser/LTTNode.java

@@ -157,7 +157,6 @@ public void enumerate(boolean recurse) {
     for (Label l : pc.getActionableLabels()) {
       if (!(l instanceof LabelKey)) {
         Process tmp = pc.getProcess().clone();
-
         pc.act(l); //Act on that label and make a new node with that child process (clone)
         Process z = pc.getProcess().clone();
         addChild(l, z);

src/main/java/org/cinrc/parser/ProcessBuilder.java

@@ -87,19 +87,19 @@ private NestedIRDCToken handleParentheses(List<KnownIRDCToken> knownTokens){
   public Process export(){ // process;
     tokenize();
     handleParentheses();
-    return export(parent);
+    return export(parent, true);
   }
-  private Process export(NestedIRDCToken nest){
-    return export(nest, null);
+  private Process export(NestedIRDCToken nest, boolean parent){
+    return export(nest, null, parent);
   }
-  private Process export(NestedIRDCToken nest, LinkedList<LabelKey> key){
+  private Process export(NestedIRDCToken nest, LinkedList<LabelKey> key, boolean parent){
     LinkedList<LabelKey> keys = key == null ? new LinkedList<>() : key;
     LinkedList<Label> prefixes = null == null ? new LinkedList<>() : null;
 
     ProcessTemplate template = new ProcessTemplate();
     for (KnownIRDCToken token : nest.getTokens()){
       if (token instanceof NestedIRDCToken n){
-        template.add(CCSParser.generateProcess(export(n),prefixes,keys));
+        template.add(CCSParser.generateProcess(export(n, false),prefixes,keys));
         continue;
       }
       List<KnownIRDCToken> nestList = nest.getTokens();
@@ -155,7 +155,7 @@ private Process export(NestedIRDCToken nest, LinkedList<LabelKey> key){
       }
     }
     template.initComplex();
-    if (!taus.isEmpty()){
+    if (!taus.isEmpty() && parent){
       throw new CCSParserException("Unmatched tau keys! " + SetUtil.csvSet(taus));
     }
     return template.export();

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,7 +25,7 @@ public String prettyString() {
 
   public Collection<Label> getActionableLabels() {
     Collection<Label> labels = process.getActionableLabels();
-    labels.removeIf(Label::isRestricted);
+    labels = removeUnsyncableKeys(labels);
 
     return labels;
   }
@@ -31,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);
   }
@@ -43,6 +73,7 @@ public void reverseLastAction() {
     try {
       if (process.hasKey()) {
         process = process.act(process.getKey());
+
       } else {
         throw new CCSTransitionException(process, "Attempted to reverse, but found no key");
       }

src/main/java/org/cinrc/process/nodes/Label.java

@@ -48,7 +48,11 @@ public void setRestricted(boolean b) {
    * @return Returns true if the provided label is not in the sync-lock array
    */
   public boolean canSynchronize(Label l) {
-    return !synchronizeLock.contains(l);
+    return !(synchronizeLock.contains(l))
+        && !(l instanceof LabelKey)
+        && !(l instanceof TauLabelNode)
+        && getChannel().equals(l.getChannel())
+        && this != l;
   }
 
   /**

src/main/java/org/cinrc/process/nodes/LabelFactory.java

@@ -22,7 +22,8 @@ public static Label parseNode(String s) {
       if (!m.find()){
         throw new CCSParserException("Could not find key dupe in key " + s);
       }
-      return new LabelKey(l, Integer.parseInt(m.group()));
+      int dig = Integer.parseInt(m.group());
+      return new LabelKey(l, dig);
     }
 
     m = CCSGrammar.LABEL_TAU.match(s);
@@ -98,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);

src/main/java/org/cinrc/process/nodes/LabelKey.java

@@ -26,10 +26,9 @@ public LabelKey(Label node) {
   }
 
   public LabelKey(Label node, int dupe) {
-    super(node.dupe, node.getChannel());
+    super(dupe, node.getChannel());
     this.id = UUID.randomUUID();
     this.from = node;
-    this.dupe = dupe;
     time = System.nanoTime();
   }
 

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;

src/main/java/org/cinrc/process/process/ConcurrentProcess.java

@@ -1,12 +1,18 @@
 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;
 import org.cinrc.parser.CCSTransitionException;
 import org.cinrc.parser.CCSGrammar;
 import org.cinrc.process.nodes.Label;
 import org.cinrc.process.nodes.LabelKey;
+import org.cinrc.process.nodes.TauLabelNode;
 import org.cinrc.util.SetUtil;
 
 
@@ -109,15 +115,33 @@ public ConcurrentProcess clone() {
   public Collection<Label> getActionableLabels() {
     Collection<Label> l = super.getActionableLabels();
     if (!prefixes.isEmpty()) {
-      l.add(prefixes.peek());
-      return withdrawRestrictions(l);
+      return l;
     }
+
     l.addAll(getActionableLabelsStrict());
-    l.addAll(SetUtil.getTauMatches(l));
-    l = withdrawRestrictions(l);
+    l.addAll(collectSynchronizations(l));
+    l = removeRestrictions(l);
     return l;
   }
 
+
+  protected List<TauLabelNode> collectSynchronizations(Collection<Label> labels){
+    List<TauLabelNode> n = new ArrayList<>();
+    for (Label l : labels){
+      for(Label l2 : labels){
+        if (l.canSynchronize(l2) && l2.canSynchronize(l)){
+
+          TauLabelNode node = new TauLabelNode(l, l2);
+          if (!n.contains(node)){
+            n.add(node);
+          }
+        }
+      }
+    }
+    return n;
+  }
+
+
   public Process attemptRewind(LabelKey key) {
     if (getLeftRightLabels().stream().noneMatch(LabelKey.class::isInstance))//no keys left/right?
     {

src/main/java/org/cinrc/process/process/NullProcess.java

@@ -54,7 +54,7 @@ public String represent() {
 
   @Override
   public Collection<Label> getActionableLabels() {
-    return withdrawRestrictions(super.getActionableLabels());
+    return super.getActionableLabels();
   }
 
   @Override

src/main/java/org/cinrc/process/process/Process.java

@@ -65,19 +65,27 @@ public boolean isGhost(){
    * @param labels Base set of labels to apply restrictions to
    * @return Collection of labels with restrictions removed
    */
-  protected Collection<Label> withdrawRestrictions(Collection<Label> labels) {
+  protected Collection<Label> annotateRestrictions(Collection<Label> labels) {
     for (Label l : labels) {
       for (Label r : getRestriction()) {
         //if (r.isComplement() == l.isComplement())
         if (r.getChannel().equals(l.getChannel())
-            && SetUtil.isRestrictable(l)) {
+            /*&& SetUtil.isRestrictable(l)*/) {
           l.setRestricted(true);
         }
       }
     }
     return labels;
   }
 
+  protected Collection<Label> removeRestrictions(Collection<Label> labels){
+    labels.removeIf(z -> SetUtil.isRestrictable(z)
+        && restrictions.stream().anyMatch(z2 ->
+        z2.getChannel().equals(z.getChannel()))
+    );
+    return labels;
+  }
+
   public void addRestrictions(Collection<Label> labels) {
     restrictions.addAll(labels);
   }
@@ -183,6 +191,7 @@ public Process act(Label label) {
     return this.actOn(label);
   }
 
+
   public Process actInternal(Label l) {
     setPastLife(clone());
     getPrefixes().removeFirst();
@@ -239,13 +248,12 @@ public LabelKey getKey() {
    *
    * @param key key to set
    */
-  protected void setKey(LabelKey key) {
+  public void setKey(LabelKey key) {
     this.key = key;
   }
 
   public abstract Process attemptRewind(LabelKey l);
 
-
   /**
    * A formatted version of this process to be printed. This is the only method that
    * should be called to print to screen unless you will be comparing processes
@@ -326,7 +334,7 @@ public Collection<Label> getActionableLabels() {
     {
       l.add(getKey());
     }
-
+    l = (Set<Label>) removeRestrictions(l);
     return l;
   }
 

src/main/java/org/cinrc/process/process/ProcessImpl.java

@@ -60,7 +60,7 @@ public Collection<Process> getChildren() {
 
   @Override
   public Collection<Label> getActionableLabels() {
-    return withdrawRestrictions(super.getActionableLabels());
+    return annotateRestrictions(super.getActionableLabels());
   }
 
   @Override

src/main/java/org/cinrc/process/process/SummationProcess.java

@@ -146,7 +146,8 @@ public Collection<Label> getActionableLabels() {
       }
       //Otherwise nope
     }
-    return withdrawRestrictions(s);
+    s = removeRestrictions(s);
+    return s;
   }
 
   @Override
@@ -187,6 +188,7 @@ private Collection<Label> getActionableLabelsStrictInternal(boolean lock) {
     }
     s.addAll(l);
     s.addAll(r);
+    s = removeRestrictions(s);
     return s;
   }
 

src/main/java/org/cinrc/util/SetUtil.java

@@ -39,6 +39,8 @@ public static <T extends Label & IRDCObject> String csvSet(Collection<T> set) {
   public static Collection<TauLabelNode> getTauMatches(Collection<Label> nodes) {
     Set<TauLabelNode> tau = new HashSet<>();
     for (Label node : nodes) {
+      if (node.isRestricted())
+        continue;
       if (node instanceof ComplementLabelNode) {
         //Cool, there is a complement in the set. Let's see if any matches
         for (Label innerNode : nodes) {
@@ -63,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()) {

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);
+
+  }
+
 }