Syntax of SChorA script

SChorA syntax

SChorA uses a text file as input. The text file content must respect the syntax following. Literal characters are given in quotes. Vertical bars | separate alternatives. (X)+ represents repetition of X n>0 times, (X)? represents repetition of X zero or one time.

"DECLARATIONS"
   (component)+
"COMMANDS"
   (command)+

Component

A component is either a chor specification language or a STG

component : chorD | STG
 
chorD : "component" ID "chorD" chor "end component" 
 
chor : chor "+" chor 
     | chor "|" chor 
     | chor ";" chor 
     | chor "[>" chor 
     | "["guard"]" "|>" chor 
     | "["guard"]" "*" chor 
     | "(" chor ")" 
     | event 
     | "skip"
 
STG       : "component" ID "STG" (state)+ (transition)+ "end component" 
 
state     : INT ";"
          | INT "[ label=\"" ID "\"];"
 
transition: INT "->" INT " [label=\"" event "\"];"
          | INT "->" INT " [label=\"[" guard "]" event "\"];"
 
guard: "true" | "false" 
     | expr op expr 
 
expr : INT | ID 
 
op   : ">" | ">=" | "<" | "<=" | "=" | "!=" 
 
event: 
     | ID "[" ID "," ID "]" (dir)?
     | ID "[" ID "," ID "]" dir ID 
     | ID "[" ID "," ID "]" dir "<" ID ">"
 
dir  : "." | "?" | "!"
 
ID   : (["a"-"z", "A"-"Z", "_"])+ (["A"-"Z"] | ["a"-"z"] | ["0"-"9"] | "_")* 
 
INT  : ([ "0"-"9" ])+

Command

command    : "showTime"                    
           | "showStat" (ID)+ 
           | "showSTG" (ID)+          
           | "showReachableSTG" (ID)+
           | "showRealizableSTG" (ID)+ comm
           | "projection" (ID)+ model
           | "conformance" ID ID
 
comm       : "SYNC" | "ASYNC_SENDER" | "ASYNC_RECEIVER" | "ASYNC_DISJOINT"

Detail of each command is here

Example

Here is an example of an input:

/* This script show STG of online shopping choreography which involves 4 roles: b (buyer), v (vendor) 
   We declare 2 components using DOT and //chor// language. */
DECLARATIONS
    component shopping STG
	0; 1; 2; 3; //list of states
                    //list of transitions
	0 -> 1 [label="request[b,v].<x>"];
        1 -> 2 [label="[x<=0] error[v,b]."];
        2 -> 1 [label="request[b,v].<x>"];
        1 -> 3 [label="[x>0] response[v,b].<x1>"];
    end component
 
    component impl chorD
        request[b,v].<y> ; (response[v,b].<y1> + [y<=0] * (error[v,b]. ; request[b,v].<y>))
    end component
 
//List of commands
COMMANDS
    showTime	//display current system time 
    showSTG shopping impl
    projection shopping SYNC
    conformance impl shopping
    showTime       //

More examples, goto here