Skip to content

Commit

Permalink
Merge pull request #80 from CinRC/master
Browse files Browse the repository at this point in the history 
Create new release
  • Loading branch information
@peterbro1
peterbro1 authored May 2, 2023
2 parents 6263ab9 + 3563319 commit b722cc9
Show file tree
Hide file tree
Showing 19 changed files with 210 additions and 101 deletions.
137 changes: 67 additions & 70 deletions docs/lts.md
View file
Original file line number Diff line number Diff line change
@@ -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' | |
| | |
| | |
| ``` | |
+-----------------------------------------------+---------------------------------------------------------------------+
2 changes: 1 addition & 1 deletion pom.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down
1 change: 1 addition & 0 deletions src/main/java/org/cinrc/parser/CCSParser.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,7 @@ public static Process generateProcess(Process p, LinkedList<Label> prefixes, Lin
}
}else */{
p.act(key.from);
p.setKey(key);
}
}

Expand Down
1 change: 0 additions & 1 deletion src/main/java/org/cinrc/parser/LTTNode.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
12 changes: 6 additions & 6 deletions src/main/java/org/cinrc/parser/ProcessBuilder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -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();
Expand Down
33 changes: 32 additions & 1 deletion src/main/java/org/cinrc/process/ProcessContainer.java
View file
Original file line number Diff line number Diff line change
@@ -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 {

Expand All @@ -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;
}
Expand All @@ -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);
}
Expand All @@ -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");
}
Expand Down
6 changes: 5 additions & 1 deletion src/main/java/org/cinrc/process/nodes/Label.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

/**
Expand Down
5 changes: 3 additions & 2 deletions src/main/java/org/cinrc/process/nodes/LabelFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand Down
3 changes: 1 addition & 2 deletions src/main/java/org/cinrc/process/nodes/LabelKey.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}

Expand Down
16 changes: 16 additions & 0 deletions src/main/java/org/cinrc/process/process/ComplexProcess.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down Expand Up @@ -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;
Expand Down
Loading

0 comments on commit b722cc9

Please sign in to comment.