From 436d2dd7ccb7e6bfe370ca8d356de91bfc146900 Mon Sep 17 00:00:00 2001
From: peterbro1 <pbrowning7@gmail.com>
Date: Sun, 30 Apr 2023 17:40:41 -0400
Subject: [PATCH 1/6] Rewrite restriction engine

---
 pom.xml                                       |  2 +-
 src/main/java/org/cinrc/parser/LTTNode.java   |  1 -
 .../org/cinrc/process/ProcessContainer.java   |  2 +-
 .../java/org/cinrc/process/nodes/Label.java   |  6 ++++-
 .../process/process/ConcurrentProcess.java    | 27 ++++++++++++++++---
 .../cinrc/process/process/NullProcess.java    |  2 +-
 .../org/cinrc/process/process/Process.java    | 15 ++++++++---
 .../cinrc/process/process/ProcessImpl.java    |  2 +-
 .../process/process/SummationProcess.java     |  4 ++-
 src/main/java/org/cinrc/util/SetUtil.java     |  2 ++
 src/test/java/tests/RestrictionTest.java      |  8 +++---
 11 files changed, 53 insertions(+), 18 deletions(-)

diff --git a/pom.xml b/pom.xml
index c87974d..4d5acaf 100644
--- a/pom.xml
+++ b/pom.xml
@@ -6,7 +6,7 @@
 
     <groupId>org.cinrc</groupId>
     <artifactId>IRDC</artifactId>
-    <version>4.2.4.1</version>
+    <version>4.3.4.1</version>
 
     <packaging>jar</packaging>
     <properties>
diff --git a/src/main/java/org/cinrc/parser/LTTNode.java b/src/main/java/org/cinrc/parser/LTTNode.java
index 41e3c73..cf5d966 100644
--- a/src/main/java/org/cinrc/parser/LTTNode.java
+++ b/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);
diff --git a/src/main/java/org/cinrc/process/ProcessContainer.java b/src/main/java/org/cinrc/process/ProcessContainer.java
index 7f19c66..dec91f6 100644
--- a/src/main/java/org/cinrc/process/ProcessContainer.java
+++ b/src/main/java/org/cinrc/process/ProcessContainer.java
@@ -21,7 +21,6 @@ public String prettyString() {
 
   public Collection<Label> getActionableLabels() {
     Collection<Label> labels = process.getActionableLabels();
-    labels.removeIf(Label::isRestricted);
 
     return labels;
   }
@@ -43,6 +42,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");
       }
diff --git a/src/main/java/org/cinrc/process/nodes/Label.java b/src/main/java/org/cinrc/process/nodes/Label.java
index 33991df..55556e6 100644
--- a/src/main/java/org/cinrc/process/nodes/Label.java
+++ b/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;
   }
 
   /**
diff --git a/src/main/java/org/cinrc/process/process/ConcurrentProcess.java b/src/main/java/org/cinrc/process/process/ConcurrentProcess.java
index 8649777..1249348 100644
--- a/src/main/java/org/cinrc/process/process/ConcurrentProcess.java
+++ b/src/main/java/org/cinrc/process/process/ConcurrentProcess.java
@@ -1,12 +1,15 @@
 package org.cinrc.process.process;
 
+import java.util.ArrayList;
 import java.util.Collection;
 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 +112,31 @@ 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?
     {
diff --git a/src/main/java/org/cinrc/process/process/NullProcess.java b/src/main/java/org/cinrc/process/process/NullProcess.java
index 2126b35..cc95c0b 100644
--- a/src/main/java/org/cinrc/process/process/NullProcess.java
+++ b/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
diff --git a/src/main/java/org/cinrc/process/process/Process.java b/src/main/java/org/cinrc/process/process/Process.java
index 92f80cc..069306b 100644
--- a/src/main/java/org/cinrc/process/process/Process.java
+++ b/src/main/java/org/cinrc/process/process/Process.java
@@ -65,12 +65,12 @@ 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);
         }
       }
@@ -78,6 +78,14 @@ protected Collection<Label> withdrawRestrictions(Collection<Label> labels) {
     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);
   }
@@ -246,6 +254,7 @@ protected void setKey(LabelKey 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 +335,7 @@ public Collection<Label> getActionableLabels() {
     {
       l.add(getKey());
     }
-
+    l = (Set<Label>) removeRestrictions(l);
     return l;
   }
 
diff --git a/src/main/java/org/cinrc/process/process/ProcessImpl.java b/src/main/java/org/cinrc/process/process/ProcessImpl.java
index 9f8b0db..1cc4704 100644
--- a/src/main/java/org/cinrc/process/process/ProcessImpl.java
+++ b/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
diff --git a/src/main/java/org/cinrc/process/process/SummationProcess.java b/src/main/java/org/cinrc/process/process/SummationProcess.java
index 11f6dd1..5f0cb22 100644
--- a/src/main/java/org/cinrc/process/process/SummationProcess.java
+++ b/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;
   }
 
diff --git a/src/main/java/org/cinrc/util/SetUtil.java b/src/main/java/org/cinrc/util/SetUtil.java
index 8ef7238..6fa8aaf 100644
--- a/src/main/java/org/cinrc/util/SetUtil.java
+++ b/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) {
diff --git a/src/test/java/tests/RestrictionTest.java b/src/test/java/tests/RestrictionTest.java
index 5681434..eb36fa4 100644
--- a/src/test/java/tests/RestrictionTest.java
+++ b/src/test/java/tests/RestrictionTest.java
@@ -67,13 +67,13 @@ public void testRestrictionSync() {
 
     ProcessContainer pc = new ProcessContainer(p);
 
-    //System.out.printf("Asserting that %s cannot act on %s...\n", pc.prettyString(), a);
+    System.out.printf("Asserting that %s cannot act on %s...\n", pc.prettyString(), a);
     assert (!pc.canAct(a)); // (a|'a)\{a} cannot do a
-    //System.out.printf("Asserting that %s cannot act on %s...\n", pc.prettyString(), oa);
+    System.out.printf("Asserting that %s cannot act on %s...\n", pc.prettyString(), oa);
     assert (!pc.canAct(oa)); // (a|'a)\{a} cannot do 'a
-    //System.out.printf("Asserting that %s can act on %s...\n", pc.prettyString(), ta);
+    System.out.printf("Asserting that %s can act on %s...\n", pc.prettyString(), ta);
     assert (pc.canAct(ta)); // (a|'a)\{a} can do Tau(a, 'a)
-    //System.out.printf("Asserting that %s can act on %s...\n", pc.prettyString(), taswitch);
+    System.out.printf("Asserting that %s can act on %s...\n", pc.prettyString(), taswitch);
     assert (pc.canAct(taswitch)); // (a|'a)\{a} can do Tau('a, a)
   }
 

From 49754104d3ef48fc2f3c439b79993d2cf1bce81d Mon Sep 17 00:00:00 2001
From: peterbro1 <pbrowning7@gmail.com>
Date: Sun, 30 Apr 2023 17:41:59 -0400
Subject: [PATCH 2/6] Rewrite restriction engine

---
 src/test/java/tests/SimulationTest.java | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/test/java/tests/SimulationTest.java b/src/test/java/tests/SimulationTest.java
index 90a913e..ab24bcf 100644
--- a/src/test/java/tests/SimulationTest.java
+++ b/src/test/java/tests/SimulationTest.java
@@ -179,6 +179,19 @@ public void testSimulation() {
 
     assert (node_q.canSimulate(node_p));
     assert (node_p.canSimulate(node_q));
+
+    p = new CCSParser().parseLine("(a.c | 'a)\\{a}");
+    q = new CCSParser().parseLine("(b|'b.c)\\{b}");
+
+    node_p = new LTTNode(p);
+    node_p.enumerate(true);
+    System.out.println(node_p);
+    node_q = new LTTNode(q);
+    node_q.enumerate(true);
+    System.out.println(node_q);
+
+    assert (node_q.canSimulate(node_p));
+    assert (node_p.canSimulate(node_q));
   }
 
 

From f4f92d55a58ca43c2d63b9da25445ad5cd84a1be Mon Sep 17 00:00:00 2001
From: peterbro1 <pbrowning7@gmail.com>
Date: Sun, 30 Apr 2023 17:55:05 -0400
Subject: [PATCH 3/6] Fix processes like ((Tau{a}[k1].b|'b)|Tau{a}[k1].c.0) not
 parsing.

Processes would try and finalize all export taus even when exporting nested processes
---
 pom.xml                                            |  2 +-
 src/main/java/org/cinrc/parser/ProcessBuilder.java | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/pom.xml b/pom.xml
index 4d5acaf..b97f31e 100644
--- a/pom.xml
+++ b/pom.xml
@@ -6,7 +6,7 @@
 
     <groupId>org.cinrc</groupId>
     <artifactId>IRDC</artifactId>
-    <version>4.3.4.1</version>
+    <version>4.3.5.1</version>
 
     <packaging>jar</packaging>
     <properties>
diff --git a/src/main/java/org/cinrc/parser/ProcessBuilder.java b/src/main/java/org/cinrc/parser/ProcessBuilder.java
index 0d77970..1b48ec1 100644
--- a/src/main/java/org/cinrc/parser/ProcessBuilder.java
+++ b/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();

From cfa51b60a8ee63fd19ccc3df14b1c55602ce0a70 Mon Sep 17 00:00:00 2001
From: peterbro1 <pbrowning7@gmail.com>
Date: Mon, 1 May 2023 12:37:06 -0400
Subject: [PATCH 4/6] Keys are no longer renamed when parsed.

---
 pom.xml                                                 | 2 +-
 src/main/java/org/cinrc/parser/CCSParser.java           | 1 +
 src/main/java/org/cinrc/process/nodes/LabelFactory.java | 3 ++-
 src/main/java/org/cinrc/process/nodes/LabelKey.java     | 3 +--
 src/main/java/org/cinrc/process/process/Process.java    | 5 ++---
 5 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/pom.xml b/pom.xml
index b97f31e..be638e1 100644
--- a/pom.xml
+++ b/pom.xml
@@ -6,7 +6,7 @@
 
     <groupId>org.cinrc</groupId>
     <artifactId>IRDC</artifactId>
-    <version>4.3.5.1</version>
+    <version>4.3.6.1</version>
 
     <packaging>jar</packaging>
     <properties>
diff --git a/src/main/java/org/cinrc/parser/CCSParser.java b/src/main/java/org/cinrc/parser/CCSParser.java
index e476d5d..cfa07c2 100644
--- a/src/main/java/org/cinrc/parser/CCSParser.java
+++ b/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);
       }
     }
 
diff --git a/src/main/java/org/cinrc/process/nodes/LabelFactory.java b/src/main/java/org/cinrc/process/nodes/LabelFactory.java
index 03f6f47..7e46f6e 100644
--- a/src/main/java/org/cinrc/process/nodes/LabelFactory.java
+++ b/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);
diff --git a/src/main/java/org/cinrc/process/nodes/LabelKey.java b/src/main/java/org/cinrc/process/nodes/LabelKey.java
index 129fc98..b6cc877 100644
--- a/src/main/java/org/cinrc/process/nodes/LabelKey.java
+++ b/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();
   }
 
diff --git a/src/main/java/org/cinrc/process/process/Process.java b/src/main/java/org/cinrc/process/process/Process.java
index 069306b..2578161 100644
--- a/src/main/java/org/cinrc/process/process/Process.java
+++ b/src/main/java/org/cinrc/process/process/Process.java
@@ -191,6 +191,7 @@ public Process act(Label label) {
     return this.actOn(label);
   }
 
+
   public Process actInternal(Label l) {
     setPastLife(clone());
     getPrefixes().removeFirst();
@@ -247,14 +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

From 1345b89332798db391b2181a0924243b39c8b541 Mon Sep 17 00:00:00 2001
From: peterbro1 <pbrowning7@gmail.com>
Date: Mon, 1 May 2023 13:25:30 -0400
Subject: [PATCH 5/6] Fix https://github.com/CinRC/IRDC-CCSK/issues/76

---
 pom.xml                                       |  2 +-
 .../org/cinrc/process/ProcessContainer.java   | 31 +++++++++++++++++++
 .../org/cinrc/process/nodes/LabelFactory.java |  2 +-
 .../cinrc/process/process/ComplexProcess.java | 16 ++++++++++
 .../process/process/ConcurrentProcess.java    |  5 +++
 src/main/java/org/cinrc/util/SetUtil.java     |  1 -
 src/test/java/tests/ActionTest.java           | 13 ++++++++
 7 files changed, 67 insertions(+), 3 deletions(-)

diff --git a/pom.xml b/pom.xml
index be638e1..d91adf7 100644
--- 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
index dec91f6..3c34eb2 100644
--- 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
index 7e46f6e..ea97172 100644
--- 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
index f121722..93eb522 100644
--- 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
index 1249348..951bd2a 100644
--- 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
index 6fa8aaf..32b14f6 100644
--- 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
index 922b4b4..8a9f21a 100644
--- 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);
+
+  }
+
 }

From 41292ace9c6420c66842a71101b2ef11563d0fda Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment=20Aubert?= <caubert@augusta.edu>
Date: Mon, 1 May 2023 17:35:12 -0400
Subject: [PATCH 6/6] Restored style in lts

---
 docs/lts.md | 137 +++++++++++++++++++++++++---------------------------
 1 file changed, 67 insertions(+), 70 deletions(-)

diff --git a/docs/lts.md b/docs/lts.md
index ffe8821..7fba68d 100644
--- a/docs/lts.md
+++ b/docs/lts.md
@@ -1,93 +1,90 @@
-
 _This document is best viewed in ["raw format" on github](https://raw.githubusercontent.com/CinRC/IRDC-CCSK/master/docs/lts.md)._
 
-The LTS (labelled transition system, or SOS, for structural operational semantics) of CSSK is the set of "reduction
-rules" describing how the system reacts / evolves.
-It is given, for instance, in _Forward-Reverse Observational Equivalences in CCSK_ (page 4, for the forward-only system)
-, or [in this exercise sheet](https://github.com/CinRC/Exercises-on-CCS-CCSK-and-RCCS/blob/master/exercises_2/main.pdf).
+The LTS (labelled transition system, or SOS, for structural operational semantics) of CSSK is the set of "reduction rules" describing how the system reacts / evolves.
+It is given, for instance, in _Forward-Reverse Observational Equivalences in CCSK_ (page 4, for the forward-only system), or [in this exercise sheet](https://github.com/CinRC/Exercises-on-CCS-CCSK-and-RCCS/blob/master/exercises_2/main.pdf).
 
 For simplification, we have written these rules down in 'ascii' format.
 They are as follows:
 
 +-----------------------------------------------+---------------------------------------------------------------------+
-| Rule | Example(s)                                                          |
+| Rule                                          | Example(s)                                                          |
 +:=============================================:+:===================================================================:+
-|```                                            | - `a.P -a[k0]-> a[k0].P`                                            |
-| | - `a.b.P -a[k0]-> a[k0].b.P`                                        |
-| | |
-| std(X)------------------ (top)                | |
-| a.X -a[m]-> a[m].X | |
-| | |
-| | |
-|```                                            | |
+|```                                            | - `a.P -a[k0]-> a[k0].P`                                            | 
+|                                               | - `a.b.P -a[k0]-> a[k0].b.P`                                        |
+|                                               |                                                                     |
+| std(X)------------------ (top)                |                                                                     |
+|         a.X -a[m]-> a[m].X                    |                                                                     |
+|                                               |                                                                     |
+|                                               |                                                                     |
+|```                                            |                                                                     |
 +-----------------------------------------------+---------------------------------------------------------------------+
 |```                                            | - `a[k0].b.P -b[k1]-> a[k0].b[k1].P`                                |
-| | - `a[k0].(b.X|Y) -b[k1]-> a[k0].(b[k1].X|Y)`                        |
-| | |
-| X -b[n]-> X' | |
-| m neq n------------------------ (pre.)        | |
-| a[m].X -b[n]-> a[m].X' | |
-| | |
-| | |
-|```                                            | |
+|                                               | - `a[k0].(b.X|Y) -b[k1]-> a[k0].(b[k1].X|Y)`                        |
+|                                               |                                                                     |
+|               X -b[n]-> X'                    |                                                                     |
+| m neq n------------------------ (pre.)        |                                                                     |
+|          a[m].X -b[n]-> a[m].X'               |                                                                     |
+|                                               |                                                                     |
+|                                               |                                                                     |
+|```                                            |                                                                     |
 +-----------------------------------------------+---------------------------------------------------------------------+
 | ```                                           | - `a.P\{b} -a[k0]-> a[k0].P\{b}`                                    |
-| | |
-| | |
-| X -z[m]-> X' | |
-| z notin {a, 'a} --------------------- (res.)  | |
-| X\{a} -z[m]-> X'\{a} | |
-| | |
-| | |
-| ```                                           | |
+|                                               |                                                                     |
+|                                               |                                                                     |
+|                      X -z[m]-> X'             |                                                                     |
+| z notin {a, 'a} --------------------- (res.)  |                                                                     |
+|                  X\{a} -z[m]-> X'\{a}         |                                                                     |
+|                                               |                                                                     |
+|                                               |                                                                     |
+| ```                                           |                                                                     |
 +-----------------------------------------------+---------------------------------------------------------------------+
 | ```                                           | - `a.P|b.Q -a[k0]-> a[k0].P|b.Q`                                    |
-| | |
-| | |
-| X -a[m]-> X' | |
-| m notin keys(Y)-------------------- (|L)      | |
-| X|Y -a[m]-> X'|Y | |
-| | |
-| | |
-| ```                                           | |
+|                                               |                                                                     |
+|                                               |                                                                     |
+|                    X -a[m]-> X'               |                                                                     |
+| m notin keys(Y)-------------------- (|L)      |                                                                     |
+|                  X|Y -a[m]-> X'|Y             |                                                                     |
+|                                               |                                                                     |
+|                                               |                                                                     |
+| ```                                           |                                                                     |
 +-----------------------------------------------+---------------------------------------------------------------------+
 | ```                                           | - `a.P|b.Q -b[k0]-> a.P|b[k0].Q`                                    |
-| | |
-| | |
-| Y -a[m]-> Y' | |
-| m notin keys(X)-------------------- (|R)      | |
-| X|Y -a[m]-> X|Y' | |
-| | |
-| | |
-| ```                                           | |
+|                                               |                                                                     |
+|                                               |                                                                     |
+|                    Y -a[m]-> Y'               |                                                                     |
+| m notin keys(X)-------------------- (|R)      |                                                                     |
+|                  X|Y -a[m]-> X|Y'             |                                                                     |
+|                                               |                                                                     |
+|                                               |                                                                     |
+| ```                                           |                                                                     |
 +-----------------------------------------------+---------------------------------------------------------------------+
 | ```                                           | - `a.P + b.Q -a[k0]-> a[k0].P + b.Q`                                |
-| | |
-| | |
-| X -a[m]-> X' | |
-| std(Y)------------------------ (+L)           | |
-| X+Y -a[m]-> X'+Y | |
-| | |
-| | |
-| ```                                           | |
+|                                               |                                                                     |
+|                                               |                                                                     |
+|             X -a[m]-> X'                      |                                                                     |
+| std(Y)------------------------ (+L)           |                                                                     |
+|           X+Y -a[m]-> X'+Y                    |                                                                     |
+|                                               |                                                                     |
+|                                               |                                                                     |
+| ```                                           |                                                                     |
 +-----------------------------------------------+---------------------------------------------------------------------+
 | ```                                           | - `a.P + b.Q -b[k0]-> a.P + b[k0].Q`                                |
-| | |
-| | |
-| Y -a[m]-> Y' | |
-| std(X)------------------------ (+R)           | |
-| X+Y -a[m]-> X+Y' | |
-| | |
-| | |
-| ```                                           | |
+|                                               |                                                                     |
+|                                               |                                                                     |
+|             Y -a[m]-> Y'                      |                                                                     |
+| std(X)------------------------ (+R)           |                                                                     |
+|           X+Y -a[m]-> X+Y'                    |                                                                     |
+|                                               |                                                                     |
+|                                               |                                                                     |
+| ```                                           |                                                                     |
 +-----------------------------------------------+---------------------------------------------------------------------+
 | ```                                           | - `a.P|'a.Q -Tau{a,'a}[k0]-> Tau{a,'a}[k0].P|Tau{a,'a}[k0].Q`       |
-| | |
-| | |
-| X -a[m]-> X' Y -'a[m]-> Y' | |
-| -------------------------------- (syn.)       | |
-| X|Y -Tau{a,'a}[m]-> X'|Y'                 | |
-| | |
-| | |
-| ```                                           | |
+|                                               |                                                                     |
+|                                               |                                                                     |
+|  X -a[m]-> X'      Y -'a[m]-> Y'              |                                                                     |
+| -------------------------------- (syn.)       |                                                                     |
+|     X|Y -Tau{a,'a}[m]-> X'|Y'                 |                                                                     |
+|                                               |                                                                     |
+|                                               |                                                                     |
+| ```                                           |                                                                     |
 +-----------------------------------------------+---------------------------------------------------------------------+