Wiki
Clone wikistable_chorgram / tutorial
Applying ChorGram
The main modes of usage of ChorGram are the top-down and bottom-up analysis communicating systems. Below we describe those modalities. More details are in the tutorials mentioned above.
Going top-down
ChorGram features a few operations for the top-down approach of choregraphic design. The workflow is
- to save in a .gc file a g-choreography specified with the syntax given above
- to refine the g-choreography until it is well-formed (using the operations ws, wb, and wf above)
- to generate the CFSMs with the operation project
As an illustration consider the PingPong protocol above, saved in the file experiments/pingpong.gc of this distribution.
To check for well-formedness we execute
wb experiments/pingpong.gc
wb: ok
wf experiments/pingpong.gc
wf: ok
ws experiments/pingpong.gc
ws: ok
which confirms that the protocol is well-branched. The CFSMs of Ping and Pong are abtained by executing
chorgram project experiments/pingpong.gc
which yields the fsa format of both machines. We execute
chorgram project -D no -fmt dot experiments/pingpong.gc -p Pong > pong.dot
to save in the file pong.dot the non minimised CFSM of the server only in the dot format.
NOTE if the directory where you installed ChorGram is not in the PATH list, all commands should start with ./
For instance you should type ./wb experiments/pingpong.gc and ./chorgram ./project experiments/pingpong.gc.
The same workflow can be executed using the GUI. After opening PingPong.gc (from the menu File > Open) the protocol is rendeder in the dot format as shown in the screenshot of Figure 1.
We can then check for well-formedness by choosing either of
Well-BranchednessWell-ForkednessWell-sequencedness
from the menu Analyses > Well-Formedness and then projecting the g-choreography using Generate > ProjectGC. The projection on Ping is then displayed after clicking on Ping in the left-most menu as shown in the screenshot in Figure 2.
Going bottom-up
Here is a quick description on how to use ChorGram to check for generalises multiparty compatibility and retrieve a g-choreography from a communicating system.
Executing cfsm2gg
The Python script cfsm2gg operation a command-line interface to gmc. For an overview of its usage, get the help message on the tool via the command:
python cfsm2gg --help
which prints on the screen the following message:
usage: cfsm2gg [-h] [-v] [-shh] [-df DF] [--dot DOT] [-l] [-sn] [-dw DW]
[-ts] [-tp TP] [-cp CP] [-p PATH] [-b BOUND] [-nc] [-pn PN]
[-hkc HKC] [-gmc GMC] [-bg BG] [-dir DIR] [-m MUL] [-D D]
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
-shh Switches off 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). Use 'none' if no manipulation of dot
files is required
-l Generates a legend from dot files
-sn Suppresses simple names for states
-dw DW Set fixedsize of dot nodes to the given value {default
= 0}
-ts Just computes the CFSMs and the transition system(s)
-nf, --bag Disable FIFO policy: buffers become bags
-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 = ""}
-p PATH, --path PATH Colours paths from the initial node to the ones
matching the configuration pattern PATH {default: ""}
-b BOUND, --bounded BOUND
Set the bound to BOUND; if BOUND < 1, the synchronous
TS is computed {default: 0}
-nc, --noclean Do not remove auxiliary files
-pn PN Specify the path to petrify {default:
./aux/petrify/bin/petrifyLinux}
-hkc HKC Specify the path to hkc {default:
./aux/hknt-1.0/hkcLinux}
-gmc GMC Specify the path to gmc {default: ./gmc}
-bg BG Specify the path to buildgc {default: ./buildgc}
-dir DIR Specify the directory for the output files {default:
outputs}
-m MUL Specify the multiplicity factor [DEPRECATED]
-D D Applies determinisation if D = det, minimisation if D
= min, or nothing otherwise
Getting the results
Upon execution with the -v option, cfsm2gg 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 basename of the input file. For example, if you run
python cfsm2gg -v -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 g-choreography in pdf format (1), the CFSM machines in dot (4) and pdf (5) format, the g-choreography in dot format (10), and the transition system in dot (19) and pdf format (20).
Figure 3 shows an example of the representation of the 1-bounded transition system of the pingpong protocol generated with the command
python cfsm2gg -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 with --dot. A better way to set dot preferences is to edit the file .dot.cfg described above.
Updated