Syntax of the input files

Strings are made of the any character which is not a separator; the current list of separators is

'\n\t @.,;:()[]{}|+-*/^!?%&#'

Names of participants, machines, or systems must start with a capital letter.

Specifying CFSMs

There are two formats to specify CFSMs: the fsa format (after finite state automata) and the cms format (after _c_ommunicating _m_achines _s_ystem). Which format is used depends on the extesion to the file name (.fsa or .cms respectively).

The fsa format is a textual format suitable for specifying communicating systems consisting of a small number of CFSMS. 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. Each line describes (some element of) a CFSM:

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).
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 considered comments and therefore ignored. Messages are strings; 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.

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:

   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' | 'accept'

Text surrounded by double-square brackets or between .. and a newline is treated as comment. For instance

'[[ this is a
    two-lines comment ]]'

and

'.. this is a one-line comment'

are ignored during the parsing.

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. Transitions are similar to those in 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 syntactic checks currently supported by the parser are

(i) that sender and receiver of interactions are different, (ii) that defining equations are unique, (iii) that communication actions name existing machines, (iv) that a machine cannot be defined as its own dual, (v) that strings obey the constraints above, (vi) that the participant controlling a loop is active in the loop.

More checks are planned.

Syntax of Global Choreographies

The syntax of g-choreographies (aka global graphs) is obtained by blending together and sugaring the syntaxes presented in various papers (barred the construct 'break' and the syntax in the section Extended syntax below, which do not occur in any of our papers). The grammar of g-choreographies is:

   G ::= (o)                                  * empty graph
      |  Ptp -> Ptp : str                     * interaction
      |  Ptp => Ptps : str                    * multiple interactions (syntactic sugar: A -> B1, ..., Bn : m = A -> B1: M |  ... | A -> Bn : m)
      |  break                                * exit a loop
      |  accept P1 ... Pn                     * marks accepting points of participants; if n = 0 then all participants are marked for acceptance
      |  G '|' G                              * fork
      |  G ';' G                              * sequential
      |  'sel' '{' Brc '}'                    * choice without explicit selector
      |  'sel' Ptp '{' Brc '}'                * choice with explicit selector 
      |  'repeat' '{' G '}'                   * loop without explicit selector
      |  'repeat' P '{' G 'unless' guard '}'  * loop with explicit selector
      |  '{' G '}'
      |  '(' G ')'                            * DEPRECATED
      |  '*' G '@' P                          * DEPRECATED: irreversible loop

   Brc ::= G | Brc + Brc

   Ptps ::= P Ptps  |  P

where (o) is the empty graph. A break statement exits a loop; it can occur only in branch of a choice wrapped in a loop and it is controlled by an explicitely specified participant (e.g., repeat X { ... break ....} is valid, while repeat { ... break ....} is not). Notice that the sel and the branch constructs have the same semantics and require to specify the selector of the branch.

The following equivalences hold when reversibility is not assumed

   sel P { G1 + ... + Gn } = G1 + ... + Gn      if P is the selector in each branch G1, ..., Gn 
   repeat P { G }          = * G @ P

The binary operators \_|\_, \_+\_, and \_;\_ are given in ascending order of precedence.

A g-choreography representing the ping-pong protocol in this syntax could be

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

(Note that we specify the selector for the choice but not for the loop and recall that \_;\_ takes precedence over \_+\_ and that * {...} @ ... is deprecated).

Extended syntax

The grammar above basically reflects the bare syntax introduced in our papers. To allow for more flexibility and improve the usability of the language, eM is currently extending this basic syntax. The following are the extensions currently available.

G-choreographies constants

A rudimentary mechanism of definition of g-choreography constants is provided by the following syntactic construnct

   let X_1 = Ctx_1 & ... & X_n = Ctx_n in G

where X_1, ..., X_n are pairwise different and Ctx_1, ..., Ctx_n are contexts (g-choreographies with a hole '[]') generated by the following grammar:

    Ctx ::= []
            |  (o)
            |  P -> P : M
            |  P => P ... P : M
            |  break                                * exit a loop
            |  accept P1 ... Pn                     * marks accepting points of participants; if n = 0 then all participants are marked for acceptance
            |  do str
            |  choiceop { GCCtx }
            |  choiceop P { GCCtx }
            |  GCCtx ; GCCtx
            |  repeat { Ctx }
            |  repeat P { Ctx }
            |  * { GCCtx } @ ptp
            |  { GCCtx }

The set of mappings should not yield recursive definitions and let cannot be nested.

To use constants and contexts the productions of G are extended as follows:

   G ::= ...
      |  do X
      |  do X[G]

where do X = do X[(o)]. The parser flags uses of undefined constants; likewise, the parser checks that Ctx_i uses only constants X_j with j < i.

For instance, for the ping-pong example above, we can write:

   let
     end =  Ping -> Pong : finished
   in
     sel {
       do end
       +
       repeat Ping {
         Ping -> Pong : ping ;
         Pong -> Ping : pong
       };
       Ping -> Pong : finished
     }

where we used g-choreography constansts (and avoided deprecated constructs). And, with the use of contexts:

   let
     pingpong = sel {
       []
       +
       repeat Ping {
         Ping -> Pong : ping ;
         Pong -> Ping : pong
       };
        []
      }
     &
     end = Ping -> Pong : finished
   in
     do pingpong[do end]

Parameters

The syntax for constants is actually slightly richer and allows to use parameters. Let's see how to use parameters with on the ping-pong example. Consider

   let
     comm @ X Y x = X -> Y: x
     &
     pingpong @ X Y = sel {
       []
       +
       repeat X {
         do comm with X Y ping ;
         do comm with Y X pong
       };
       []
     }
   in
     do pingpong[Ping -> Pong : finished] with Ping Pong

The definition of comm (given just for illustrative purposes) provides a simple where all elements are parameters. Notice the capitalisation: X and Y are meant to be replaced by participant names (namely strings with the initial capitalised) while x is a parameter for messages. The g-choreography is the resultant of invoking the constant pingpong with actual parameters Ping and Pong.

Emacs users

Being a big fan of emacs, eM wrote a major mode for editing g-choreographies. To use it copy aux/sgc-mode.el in one of the folders from where emacs loads stuff and add (require 'sgc-mode) in your init emacs file.

Wiki

stable_chorgram / syntax