The Reversible Calculus of Communicating Systems (RCCS) and the Calculus of Communicating Systems with Keys (CCSK) are two formal languages that describes the interaction of concurrent systems in a reversible paradigm. They are both described in Static versus dynamic reversibility in CCS (doi:10.1007/s00236-019-00346-6), and shown to be equivalent (in terms of labelled transition system isomorphism) in the same paper.
This project is the first to publicly available implementation a functional formal language (in this case, inspired by CCSK) that models concurrent reversible systems. At its core, this is a parser and evaluation tool. The program takes user input in the form of CCS processes (using the syntax specified below) and parses, tokenizes, and traverses it at the user's will (using CSSK's labelled transition system, described and exemplified in this documentation).
Everything in this program is original, including string traversal libraries and GUI. It is currently developed in the School of Computer and Cyber Sciences, primarily by Peter Browning and Dr.Clément Aubert. Please, refer to our list of contributors for an up-to-date list of contributors.
You will need the Java Runtime Environment (JRE) (≥8) to execute this program. Download the .jar file in our latest release, potentially using this simple one-liner[^1]: [^1]: Inspired by https://gist.github.com/steinwaywhw/a4cd19cda655b8249d908261a62687f8.
curl -s https://api.github.com/repos/CinRC/IRDC-CCSK/releases/latest \
| grep browser_download_url \
| cut -d : -f 2,3 \
| tr -d \" \
| wget -qi -
Then execute e.g., the process $((a+b) | \overline{b}) | \overline{a}) \backslash a$ using
java -jar IRDC-*.jar "(((a+b) |'b)|'a)\{a}"
To run with a GUI, use the --gui
flag. Else, a command-line-interface will open instead, you can use it with:
java -jar IRDC-*.jar <FLAGS> "[Process]"
Some examples of processes are indicated in docs/example_processes.md
if you need inspiration.
The flags are documented below.
You will need Maven (≥3.0) and the Java Development Kit (≥17) to compile this program. Some of the possible phases are:
mvn package
to build from source (the executable will be in the target/
folder),mvn validate
to test for checkstyle violations (we use google_checks.xml),mvn test
to run our pre-written unit tests (gathered in the src/test/java
folder) that are
designed to represent difficult a diverse range of different scenarios.To run e.g., all the test methods whose name starts with simulationIsStructural
in the tests.SimulationTest
class,
use
mvn -Dtest="tests.SimulationTest#simulationIsStructural*" test
We are thrilled that you consider contributing to our project. Please refer to our contributing guidelines.
Some parts of this program are named different from the convention. Some of the notable ones are are listed below:
|
) are referred to as 'Concurrent Processes'+
) are referred to as 'Summation Processes'a[k0].P
) are referred to as 'Label Keys'This program follows a slightly modified semantic structure based off of CCSK. Some notes are included below.
By default, all labels are given implicit null processes (a
is implied to represent a.0
). This is toggleable using the --require-explicit-null
flag.
Channel labels are limited to lowercase english letters [a-z]
.
Complement channels are represented by an apostrophe before the label, 'a
, 'b
, etc.
Process names are limited to uppercase english letters [A-Z]
.
We assume that all channels sharing the same label are complements. This means that 'a
is the complement to a
, 'b
to b
, and so forth.
Restrictions are applied under the following format: a.P\{a,b,c}
.
We assume that the operators have decreasing binding power, in the following order: \a
, a.
, |
, +
.
a|b\{a}
will be interpreted as (a)|(b\{a})
.a.a + b | c \{a}
is to be read as (a.a) + (b | (c\a))
(infix notation)
or + . a a | b \a c
(postfix notation).(((a)|(b)))
will be accepted but interpreted as (a|b)
.This program can be configured by using command-line arguments, or flags. The flags are as follows:
Flag | Description |
---|---|
--debug | Enables debug mode. Will print info to stdout |
--help | Prints help message documenting flags |
--dL | Labels are visibly differentiated by integers |
--hide-keys | CCSK keys are hidden |
--sA | Alternative display mode for summation processes. Reversible summations are not annotated |
--process-names-equivalent | Processes names will be treated as being equivalent (P == Q) |
--sC | Alternative display mode for summation processes. Reversible summations are hidden after execution |
--require-explicit-null | Labels explicitly require a trailing process. Labels will no longer have an implicit null process attached |
--hP | Parenthesis surrounding complex processes will be omitted |
--dN | Null processes will be displayed explicitly |
--iU | Parser will ignore unrecognized characters in the process formula |
--kL | (Deprecated) Keys will be visibly similar to the label they represent |
--gui | Program will start with a GUI instead of CLI |
--forward-only | Program will run in a non-reversible paradigm |
--interactive | Run the program in interactive mode. In interactive mode, the given process will be displayed and the user will be prompted to give a label or key to act on. |
--enumerate | Run the program in enumeration mode (Default). In enumeration mode, the given process will be enumerated to completion, and the transition tree will be printed to stdout |
--validate | Run the program in validation mode. In validation mode, a user inputted file will be scanned for processes to parse. Processes in the file must be separated by newlines, with one process per line. Each process will be validated for syntax and formatting. |
--equivalence | Run the program in equivalence mode. In equivalence mode, your input will be in the form of a list of processes separated by commas (,). All equivalence relationships between the given processes will be printed. |
--regenerate | Run the program in regeneration mode. In regeneration mode, you may input a process that has already begun execution. It will then regenerate to its ancestor process and enumerate. |
If you'd like to contribute to this project, please refer to the CONTRIBUTING.md file
When contributing, the project version must be appropriately incremented inside the pom.xml
file. We use a semantic
Maj.Min.Patch.Rev system, where:
When making changes, increment the version number according to changes made.
This project, in particular, is a working implementation of the Calculus of Communicating Systems with Keys (CCSk). Some of the other implementations of process algebras that are publicly available are:
The implementation of CCSk described in this master thesis is to our knowledge not publicly available.