Clone wiki

chorgram / Home

Welcome

Chorgram is 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
  • chorgram.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.

Chorgram is a polished and extended version of gmc-synthesis and of gmc-synthesis-v0.2; those old versions are deprecated.

Syntax of the input files

Strings are made of the following characters

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

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

GMC

The syntax of the input files of gmc can be either in the 'fsa' (after finite state automata) or 'cms' 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 '.cms' respectively).

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

.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 'cms' 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:

Comments can any text surrounded by square brackets or following '..' up to the new line.

    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 (comma-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:

    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

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

(recall that ';' has priority over '+').

How to install chorgram

At the moment choregram is available for linux-like architectures only. So far, chorgram has been tested on Ubuntu 13.04, 14.04, 16.04 and Mac OS X (v10.9).

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

Besides the command line options, there is a configuration file 'aux/dot.cfg' that can be used to tune up dot files. The format of the file is very basic: each line is a blank-separated pair of key / value and an optional 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

'statesep       ++      :symbol to separate states in output files'

Unless you know what you're do doing, do not add lines to 'aux/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

Configuration

Move the directories of HKC and Petrify in under the directory chorgram. Any subdirectory would do, but we advise to put them under 'aux'. if you want, you can compile HKC yourself by going into the directory of HKC and typing make (you will need OCaml, ./hknt-1.0/README).

Compilation

Once both the directories of HKC and Petrify have been moved in the directory chorgram, you simply

1. from a shell cd in the directory chorgram
2. make setup

Running

Executing cfsm2gg.py

The Python script 'cfsm2gg.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 cfsm2gg.py --help 

which prints on the screen the following message:

usage: cfsm2gg.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] [-D TRF]
                 filename

chorgram: 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 --dot Granksep=1). Use 'none' if you don't want to transform dot files in other graphical formats
  -l                    Generates 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 form "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/}
  -D TRF                Apply minimisation if TRF = 'min', determinisation if TRF = 'det', nothing if TRF = 'no'

Getting the results

Upon execution, 'cfsm2gg.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

python cfsm2gg.py -nc -dw 0 -df pdf -dir experiments/results/ experiments/pingpong.fsa 

you get a message like

chorgram: Execution Started on Sat, 15 Oct 2016 09:18:18 +0000
gmc:    Parsing CFSMs file...experiments/pingpong.fsa
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)): []
chorgram: Language-equivalence (Representability part (i))? True
gg:     Global graph synthesis
chorgram: 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'

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

The important files are 1, 4, 5, 10, 19, and 20 which respectively are the global graph in pdf format (1), the CFSM machines in dot (4) and pdf (5) format, the global graph in dot format (10), and the transition system in dot (19) and pdf format (20).

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

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

pingpong_ts1.png

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 sgg.py --help 

which prints on the screen the following message:

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

python sgg.py experiments/examples_sgg/pingpong.sgg

you get the message

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

and, for each line between 'sgg: start' and 'sgg: end' the corresponding file is genereated (in the default directory) together with the 'svg' format of each '.dot' file. For instance, the svg format of the graphical representation of the global graph of the ping-pong example is

pingpong_gg.svg

Updated