This webpage is an implementation of the Labelled Transition System of the SynpaTick process algebra, designed by Luigi Liquori, Michael Mendler, and Claude Stolze, as submitted to FSCD 2026. You can find a draft of the article here. The source code of the interpreter has been written in OCaml, and can be found here.
Enter a process, or select one from the example, then click on the Parse button. If there was no syntax error, a graph should appear. Click on a colored node to compute a transition.
Syntax:
ID ::=
[A-Za-z][A-Za-z0-9'_-]*
ACT ::=
!ID
positive action
?ID
negative action
#ID
clock action
tau
silent action
P, Q ::=
0_[ID, ...,ID]
the zero process
ACT: [ACT, ...,ACT].P
prefix
ACT.P
Equivalent to ACT: [ ].P
P+Q
sum
P|Q
parallel
P\ [ID, ...,ID]
restriction
P/ [ID, ...,ID]
hiding
ID[ID, ...,ID]
process name
DECL ::=
ID:=P;
declaring a process
PROC ::=
DECL ... DECLP
full process
Notes on the syntax:
when you use a process name, you have to declare all its clocks between brackets, which should be the same list everytime you use the same name. When you declare a process, do not declare its clocks on the left-hand side of :=, for instance one := #clock. one[clock];
lists can be empty. In processes, lists are comma-separated and bracketed