Welcome

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).

Forewords

This branch has been started in order to

• improve the feedback to the user when generalised multiparty compatibility is violated,
• add new features to
• manipuate the TS (eg highlighting of configurations with some properties; click here for examples of graphical outputs.)
• improve usability
• use asserted CFSMs
• track paths from global graphs to the corresponding TS

(all this is still work in progress).

The main commands provided by the implementation are

• gmc: takes in input a CFSM system, checks it for generalised multiparty compatibility, and builds the corresponding global graph
• chosyn.py: a python script that executes gmc, transforms the .dot files it generates in graphical formats, and displays some performance information
• sgg: takes in input a description of a global graph in the syntax of the ICE 2016 paper and projects the graph in a set of (non-minimal) CFSM provided that the graph is well-branched and well-sequentiased.

Syntax of the input files

Strings are made of the following characters

0123456789<=>ABCDEFGHIJKLMNOPQRSTUVWXYZ()\^_`abcdefghijklmnopqrstuvwxyz\167/$#&~,

and must start with a letter when specifying the name of a machine (non-terminal Ptp).

GMC

The syntax of the input files of gmc can be either in the 'fsa' (after finite state automata) or 'sys' format, the latter being the simple process-algebraic syntax described in the following. Which format is used depends on the extesion to the file name ('.fsa' or '.sys' respectively).

The 'fsa' format is a text where each line describes (some element of) a CFSM: for instance,

#!ABNF

.outputs A
.state graph
q0 1 ! hello q1
q0 1 ! world q1
.marking q0
.end

.outputs
.state graph
q0 0 ? hello q1
q0 0 ? world q1
.marking q0
.end

specifies a system of two machines. - machine 0 is named A (line '.outputs A'), has q0 as initial state (line .marking q0) from which it may send either a message 'hello' or a message 'world' to machine 1 and move to state q1 (lines 'q0 1 ! hello q1' and 'q0 1 ! world q1', respectively). Messages can be any sort for string; the current implementation does not interpret them, but in the future we plan to fix a syntax and a semantics in order to deal with e.g., variables, binderds, values, etc. - machine 1 is ready to receive either message sent by machine 0.

Machine names are optional (e.g., machine 1 is anonymous in the example above); if present in the input file, they are used to denote the channels in the files generated by the tool (for instance, the first transition of A is displayed as "AB ! hello" rather than "01!hello". Lines '.outputs ...', '.state graph', '.marking ...', and '.end' are mandatory. Lines starting with '--' are ignored.

The 'sys' format is probably more appropriate for systems consisting of many machines. The idea is that each CFSM of a system is described by a simple process in the following syntax:

#!ABNF


    S     ::= 'system' str 'of' Ptp, ..., Ptp ':' Ptp '=' M || ... || Ptp '=' M
    M     ::= end
           | p ';' M
           | p 'do' Ptp
           | M '+' M
           | '*' M
    p     ::= Ptp '!' str | Ptp '?' str | 'tau' str | 'tau'

A system S is given a name, specifies the (space-separated list of the) names Ptps of its machines, and has a declaration Mdec for each machine. Each name in Ptps must have a unique defining equation Ptp = M where the syntax of M is straightforward. Transition are similar those of the 'fsa' format, but they use explicit names rather than positions to address machines. Moreover, it is possible to specify internal transitions 'tau' which also carry an uninterpred annotating string. Note that branches and forks have to be surrounded by round brackets (this constraint will be relaxed in the future).

The only syntactic check made (right now) during the parsing are (i) that sender and receiver of interactions have to be different, (ii) that defining equations are unique, (iii) that communication actions name existing machines, and (iv) a machine cannot be defined as its own dual. Error messages give some information, but should be improved. Text enclosed in '[' and ']' is ignored.

Syntax of Global Graphs

The syntax of syntactic global graph is defined by the grammar:

#!ABNF

    G ::= Ptp '->' Ptp ':' str | G'|'G | G'+'G | G';'G | '*' G '@' Ptp | '{' G '}'

and it is essentially the one in the ICE 2016 paper where the iteration construct * G @ Ptp has been added; intuitively, such constructs repeats G until participant Ptp decides to stop the iteration.

A global graph representing the ping-pong protocol in this syntax could be

#!python

Ping -> Pong : finished
+
*{
   Ping -> Pong : ping ; Pong -> Ping : pong
} @ Ping ; Ping -> Pong : finished

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

• 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).

Configuration

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

#!make

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

Compilation

Simply

#!bash

1. make config
2. make

Running

Executing chosyn.py

The Python script 'chosyn.py' offers a command-line interface to gmc. For an overview of its usage, get the help message on the tool via the command:

#!python

python chosyn.py --help 

#!bash

usage: chosyn.py [-h] [-v] [-df DF] [--dot DOT] [-l] [-dw DW] [-ts] [-tp TP]
                 [-cp CP] [-p PATH] [-b BOUND] [-nc] [-pn PN] [-hkc HKC]
                 [-gmc gmc_path] [-gg GG] [-dir DIR] [-m MUL]
                 filename

chosyn: From communicating machines to graphical choreographies

positional arguments:
  filename              Specify the path to file containing the CFSMs

optional arguments:
  -h, --help            show this help message and exit
  -v, --verbose         Run in verbose mode
  -df DF                Output format from dot files (svg, png, pdf, etc.) {default = svg}
  --dot DOT             Specify the options for dot starting without '-' (e.g., --dot Nnodesep=.5)
  -l                    Suppress legend from dot files
  -dw DW                Set fixedsize of dot nodes to the given value {default = 0}
  -ts                   Compute just the CFSMs and the transition system(s)
  -tp TP                Pattern for colouring transitions; the syntax is "s r d msg" where s and r are the indexes of sender and receiver,
                        d is the action, and msg is the message {default = "- - - -"}
  -cp CP                Pattern for colouring configurations; the syntax is a string with blank-separated local state ids or '*' (as
                        many as the number of machines) and then some blank separated string of the forom "s r" where s and r are the
                        indexes of sender and receiver {default = ""}
  --path PATH           Colour paths from the initial node to the ones matching the configuration pattern PATH {default: ""}
  -p PATH               Same as --path PATH
  --bounded BOUND       Set the bound to BOUND; if BOUND < 1, the synchronous TS is computed {default: 0}
  -b BOUND              Same as -- bound BOUND
  -nc, --noclean        Do not remove auxiliary files
  -pn PN                Specify the path to petrify {default: ../petrify/bin/petrifyDarwin}
  -hkc HKC              Specify the path to hkc {default: ./hknt-1.0/hkcDarwin}
  -gmc gmc_path         Specify the path to gmc {default: ./gmc}
  -gg GG                Specify the path to BuildGlobal {default: ./BuildGlobal}
  -dir DIR              Specify the directory for the output files {default: experiments/results/}

Configuring chosyn

Besides the command line options, there are two configurations files '.chosyn.cfg' and '.dot.cfg' that can be used to tune up details. The format of the file is very basic: each line is a blank-separated pair of key / value (the lines of '.dot.cfg' also have a comment (starting with ':' after each value). You will probably just need to change the 2nd column by setting your preferred value; for instance, to change to simbol separating local states in configurations to '++' you've to change the value of 'statesep': making the line look like

#!bash
'statesep       ++      :symbol to separate states in output files'

Unless you know what you're do doing, do not add lines to '.dot.cfg'. If you need to edit the file other than for altering the values as described, remember the following rules:

• do not insert text before the very first line.
• do not insert empty lines
• do not insert lines with the very same initial word

Getting the results

Upon execution, 'chosyn.py' displays some information about the files and the execution time and produces some files as results. Such files are collected in a directory that can either be a default one (currently the directory 'experiments/results/' followed by the basename of the input file) or the one you specify with the option 'dir' plus the base name of the input file. For example, if you run

#!bash
python chosyn.py -nc -dw 0 -df pdf -dir experiments/results/ experiments/pingpong.fsa 

chosyn: Execution Started on Sat, 15 Oct 2016 09:18:18 +0000
gmc:    Parsing CFSMs file...experiments/pingpong.sys
gmc:    dir "experiments/results/pingpong/"
gmc:    Synchronous TS: (nodes 3, transitions 3)
gmc:    1-bounded TS:   (nodes 6, transitions 6)
gmc:    Branching representability:     []
gmc:    Branching Property (part (ii)): []
chosyn: Language-equivalence (Representability part (i))? True
gg:     Global graph synthesis
chosyn: All done.
    Total execution time: 0.0250358581543
        GMC check:                         1.90734863281e-05
        HKC minimisation:                  0.00535798072815
        Petrify:                           0.00365400314331
        Global graph generation:           0.00565099716187

on the screen and the following files are generated in the directory 'experiments/results/pingpong'

#!bash
1. pingpong_global.pdf
2. pingpong_machine_0
3. pingpong_machine_1
4. pingpong_machines.dot
5. pingpong_machines.pdf
6. pingpong_petrinet
7. pingpong_petrinet_finalpn.dot
8. pingpong_petrinet_global.dot
9. pingpong_petrinet_onesourcepn.dot
10. pingpong_petrinet_preglobal.dot
11. pingpong_projected
12. pingpong_projection_0
13. pingpong_projection_0.dot
14. pingpong_projection_0.pdf
15. pingpong_projection_1
16. pingpong_projection_1.dot
17. pingpong_projection_1.pdf
18. pingpong_toPetrify
19. pingpong_ts0.dot
20. pingpong_ts0.pdf
21. tempefc

Here is an (ugly) example of the 1-bounded transition system of the pingpong protocol generated with the command

#!bash

python chosyn.py -df png -b 1 --dot "Nshape=parallelogram" --dot "Gnodesep=.5" -dir out \
-p "w *" -tp "Ping Pong * *" -cp "* * Ping Pong" experiments/pingpong.fsa 

this example is meant just to show how to specify conditions on nodes and transitions using the options -p, -ts, and -cp and how to use dot options --dot (the parallelogram shape is what makes the diagram look bad). A better way to set dot preferences is to edit the file .dot.cfg described above.

Executing sgg.py

The Python script 'sgg.py' offers a command-line interface to sgg. For an overview of its usage, get the help message via the command:

#!python

python sgg.py --help 

#!bash

usage: sgg.py [-h] [-v] [-df DF] [--dot DOT] [-l] [-dir DIR] filename

sgg: semantics of syntactic global graphs and their projections to
communicating machines

positional arguments:
  filename       Specify the path to file containing the CFSMs

optional arguments:
  -h, --help     show this help message and exit
  -v, --verbose  Run in verbose mode
  -df DF         Output format from dot files (svg, png, pdf, etc.) {default =
                 svg}
  --dot DOT      Options for dot starting without '-' (e.g., --dot
                 Nnodesep=.5)
  -l             Suppress legend from dot files
  -dir DIR       Specify the directory for the output files {default: outputs}

Getting the results

Upon execution, 'sgg.py' displays some information about the files and produces some files as results. Such files are collected in a directory that can either be a default one (currently the directory 'experiments/results/' followed by the basename of the input file) or the one you specify with the option 'dir' plus the base name of the input file. For example, if you run

#!bash
python sgg.py experiments/examples_sgg/pingpong.sgg

sgg: start
    experiments/results/pingpong/in.sgg: is the initial gg
    experiments/results/pingpong/graph_sgg.dot: is the input gg
    experiments/results/pingpong/norm_sgg.dot:  is the normalised initial gg
    experiments/results/pingpong/fact_sgg.dot:  is the factorised initial gg
    experiments/results/pingpong/sem_sgg.dot: is the semantics of the initial gg
    experiments/results/pingpong/cfsmPing.dot is the machine for participant Ping
    experiments/results/pingpong/cfsmPong.dot is the machine for participant Pong
sgg: end