gmc-synthesis /

Filename Size Date modified Message
1.4 KB
1.4 KB
1.4 KB
1.5 KB
10.1 KB
1.8 KB
7.1 KB
4.8 KB
5.0 KB
11.6 KB
1.8 KB
2.1 KB
901 B
3.9 KB
7.9 KB
1.1 KB
2.8 KB
3.5 KB
17.1 KB
1.4 KB
1.4 KB
12.1 KB
4.2 KB
4.3 KB
2.9 KB
693 B
364 B
405 B
This tool implements the theory introduced in **From Communicating Machines to Graphical Choreographies** by Julien Lange,  Emilio Tuosto, and Nobuko Yoshida.

See for sample of graphical outputs; all the systems in this archive are GMC.


# Required Tools/ Libraries #
The following tools and libraries are required.

* graphviz (and python-numpy if you would like to run the benchmarks scripts)

You can install via the command "sudo apt-get install graphviz" on

- Haskell platform (cf.

- MissingH (a Haskell libraries)
  You can install it via the command:

cabal install MissingH split Graphalyze

- HKC (slight variation on git) --
  To compile: the modified version, use the following commands:
     - cd hknt-1.0/
     - make
     (you will need OCaml, ./hknt-1.0/README)

- Petrify --

NB: The tool has been tested on Ubuntu 13.04 and Mac OS X (v10.9)

# Compilation #
To compile the tool, run the following command:


 ghc -threaded --make GMC.hs && ghc --make BuildGlobal.hs

# Configuration #
To configure the tool to you environment, edit the file "" so
that the PETRY variable is set to the binary of petrify, e.g., PETRY =

# Syntax of the input files #
The syntax of the input files is similar to that of petrify, for

.state graph
q0 1 ! hello q1
q0 1 ! bye q1
.marking q0

.state graph
q0 0 ? hello q1
q0 0 ? bye q1
.marking q0
specifies a system of two machines, machine 0, may send either "hello"
or "bye" to machine 1, which is ready to receive either "hello" or
"bye" from machine 0.

# Running the tool #
You can run the tool via the command: ./rungmc <path/to/cfsms>

# Getting the results #
If the system in <cfsms> is GMC only of the tool ouputs the following
two lines:

<<----- Partial GMC Check: +++True+++ ----->> 
Is the system Language-equivalence Representable (part (i))? ^^^True^^^

If <cfsms> is GMC, then the "outputs" folder contains the following files:

* <cfsms>_a_machines.svg : a graphical representation of <cfsms>
* <cfsms>_c_global.svg : a graphical representation of the global graph synthesised from <cfsms>

and, if "debug = True" in, 

* <cfsms>_b_ts.svg : a graphical representation of TS(<cfsms>)
* <cfsms>_finalpn.svg : a reprensation of the Petri net to be transformed into the pre-global graph
* <cfsms>_preglobal.svg : the pre-global graph