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 ubuntu/debian
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)
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