This is Emilio's branch of Julien's gmc-synthesis, a tool implementing the theory introduced in From Communicating Machines to Graphical Choreographies (J. Lange, E. Tuosto, and N. Yoshida, POPL 2015). This branch is also based on An abstract semantics of the global view of choreographies (R. Guanciale and E. Tuosto, ICE 2016).

See the wiki for more details.

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

  • 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, 14.04, 16.04 and Mac OS X (v10.9).


To configure chosyn, edit the assignments to 'HKCDIR' and 'PETRYDIR' in the file 'Makefile' so
that the HKC and PETRY are set to the binary of hkc and petrify respectively. An example is

HKCDIR = ./hknt-1.0                     # change to the actual directory of hkc
PETRYDIR = ../petrify/bin               # change to the actual directory of petrify



1. make config
2. make