LIP6 UPMC CNRS Move-team LIP6 UPMC CNRS Move-team Macao FrameKit CPN-AMI
LIP6 > Software > MoVe Sofware > SDD/DDD >

Guarded Action Language Meta-model and grammar documentation

GAL Metamodels

GAL is a DSL meant to express model semantics. As such it is meant to be the target of a model transformation process.

This page gives the technical details : it explains the concrete syntax (using an Xtext grammar) and the abstract syntax (using a meta-model).

Contents

1. Install

For a developer, it is recommended to set up your eclipse as indicated in the developer corner of the download page.

The fr.lip6.move.gal package hosts the full Xtext grammar (or you can >browse it here

After executing the MWE2 workflow, the ecore metamodel is found in model/generated folder. The model folder contains a .aird file that hosts the diagrams presented in this page. You can open them natively using the EcoreTools plugin from standard eclipse download site.

2. GAL overview

This page presents the concrete and abstract syntax of GAL, please read this document for a more formal overview of GAL semantics and some of their applications.

2.0 Lexer Terminals

These are the terminal lexer tokens of GAL. ID is an Xtext predefined terminal that matches C identifiers. Many of our names support '.' in their definition, to help trace flattening of composite types to plain GAL. Parameters (which are runtime constants) are identified by a dollar sign. The its-tools command line parser cannot parse all of this grammar, many concepts (such as parameters) are simplified out before invoking the its-tools.


// This means a quoted "arbitrary #d%$ string"
Label :
    name=STRING
;

// Our qualified name may have integer at any position except first one
FullyQualifiedName:
    ID ( '.' (ID|INT))*
;

// semantic comments that can be added to model elements
// can span multiple lines
terminal COMMENT :
    '/**' -> '*/' 
;

// Note that SL_COMMENT, i.e. "// to \n"
// comments to end of line

// Start with $ and build an ID
terminal PARAMNAME:
    '$'  ('^')?('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'0'..'9')*;

// although we shoudl support parse of negative int, they will produce errors if output.
// please wrap any negative Constant value int in UnaryMinus.
Integer returns ecore::EInt:
    ('-')? INT;

2.1 Specification

download

Specification :
    (interfaces+=Interface
    | types+=GALOrCompositeTypeDeclaration
    | typedefs+=TypedefDeclaration
    | params += ConstParameter ';'
    )*
    (
        'main' main=[TypeDeclaration|FullyQualifiedName] ';'
    )?
    (properties+=Property) *
;

Interface :
    'interface' name=ID '{'
        ( labels+=Label ';' )*    
    '}'
;

//these are the real types
GALOrCompositeTypeDeclaration returns TypeDeclaration :
    GALTypeDeclaration
    | CompositeTypeDeclaration    
;

//this enforces that a TemplateTypeDeclaration is a legal target for InstanceDecl
TypeDeclaration :
    GALTypeDeclaration
    | CompositeTypeDeclaration
    | TemplateTypeDeclaration
;

// A typedef found in many places (spec, gal, composite)
TypedefDeclaration: (comment=COMMENT)? 'typedef' name=ID '=' min=BitOr '..' max=BitOr ';';

// A constant defined as type parameter or global specification level
ConstParameter : 
    name=PARAMNAME '=' value=Integer
;

A Specification is the root of a gal model. It holds types, of which one is the main, and properties. It can also define constant parameters (symbolic constants) and ranges, in any order. Interfaces are used in the template parameter type system.

2.2 GAL type declaration

download GALTypeDeclaration:
    ('gal'|'GAL') name=FullyQualifiedName 
    ('('
    params += ConstParameter
    ( ',' params+= ConstParameter)* 
    ')')?
    '{'
    (
    (typedefs+=TypedefDeclaration)
    |(variables+=VariableDeclaration) 
    |(arrays+=ArrayDeclaration) 
    )*
    (transitions+=Transition 
    | predicates+=Predicate    
    )*
    ('TRANSIENT' '=' transient=Or ';')?
    '}';


// A constant defined as type parameter or global specification level
ConstParameter : 
    name=PARAMNAME '=' value=Integer
;


// A typedef found in many places (spec, gal, composite)
TypedefDeclaration: (comment=COMMENT)? 'typedef' name=ID '=' min=BitOr '..' max=BitOr ';';



//Ex: int abc = 10 ; 
VariableDeclaration returns Variable:
    (comment=COMMENT)?
    (hotbit?='hotbit' '(' hottype=[TypedefDeclaration] ')')? 'int' name=FullyQualifiedName '=' value=BitOr ';';


    //Ex: array[1] tab = (2) ;
ArrayDeclaration returns ArrayPrefix:
    (comment=COMMENT)?
    (hotbit?='hotbit' '(' hottype=[TypedefDeclaration] ')')? 
    'array' '[' size=INT ']' name=FullyQualifiedName '=' '(' ( (values+=BitOr) (',' values+=BitOr)* )? ')' ';';

Transition:
    (comment=COMMENT)? 
    'transition' name=FullyQualifiedName 
    ('(' params+=Parameter     ( ',' params+=Parameter)* ')')? 
    '[' guard=Or ']' 
    ('label' label=Label)? 
    '{'
    (actions+=GalStatement)*
    '}';

Predicate:
    (comment=COMMENT)? 
    'predicate' name=FullyQualifiedName '=' value=Or  ';' 
;

A GALTypeDeclaration mainly holds variables and arrays, and transitions. It can also define type parameters (that can be fixed at instantiation) as well as local range types. Predicates can be referred to by logic properties.

2.3 Integer Expressions

download /* =====   Arithmetic expressions ===== */

/* ====== Bitwise operators ======= */
// by order of increasing precedence
BitOr returns IntExpression:
    BitXor ({BinaryIntExpression.left=current} op='|' right=BitXor)*;

BitXor returns IntExpression:
    BitAnd ({BinaryIntExpression.left=current} op='^' right=BitAnd)*;

BitAnd returns IntExpression:
    BitShift ({BinaryIntExpression.left=current} op='&' right=BitShift)*;

BitShift returns IntExpression:
    Addition ({BinaryIntExpression.left=current} op=('<<' | '>>') right=Addition)*;

Addition returns IntExpression:
    Multiplication ({BinaryIntExpression.left=current} op=('+' | '-') right=Multiplication)*;

Multiplication returns IntExpression:
    UnaryExpr ({BinaryIntExpression.left=current} op=('/' | '*' | '%') right=UnaryExpr)*;

UnaryExpr returns IntExpression :
    BitComplement | UnaryMinus | Power
;

UnaryMinus returns IntExpression:
    {UnaryMinus} '-' value=UnaryExpr;
    
BitComplement returns IntExpression:
    {BitComplement} '~' value=UnaryExpr ;

Power returns IntExpression:
    Primary ({BinaryIntExpression.left=current} op=('**') right=Primary)*;

Primary returns IntExpression:
    Reference |
    ConstRef |
    (=> ('(' BitOr ')') | ('(' WrapBoolExpr ')'));

ConstRef returns IntExpression:
    Constant |
    ParamRef ;
    

WrapBoolExpr:
    value=Or;

Constant:
    value=INT;

2.4 Boolean Expressions

download /* =====   Boolean expressions ===== */
enum ComparisonOperators:
    GT='>' | // Greater Thean
    LT='<' | // Lower Than
    GE='>=' | // Greater or Equal
    LE='<=' | // Lower or Equal
    EQ='==' | // Equal
    NE='!='; // Not Equal
    
Or returns BooleanExpression:
    (And ({Or.left=current} ->'||' right=And)*);

And returns BooleanExpression:
    Not ({And.left=current} ->'&&' right=Not)*;

Not returns BooleanExpression:
    (->'!' {Not} value=PrimaryBool) | PrimaryBool;

PrimaryBool returns BooleanExpression:
    True | False | => Comparison | ('(' Or ')');

Comparison:
    (left=BitOr
    ->operator=ComparisonOperators
    right=BitOr);

True:
    {True}
    'true';

False:
    {False}
    'false';

2.5 Composite type declaration

download CompositeTypeDeclaration :
    'composite' name=ID 
    ( '<' templateParams+=TemplateTypeDeclaration   ( ',' templateParams +=TemplateTypeDeclaration )*   '>' )?
    ('('
    params += ConstParameter
    ( ',' params+= ConstParameter)* 
    ')')?
    '{'
        (typedefs+=TypedefDeclaration |
        instances+=InstanceDecl)*
        (synchronizations+=Synchronization)*
    '}'
;

ConstParameter : 
    name=PARAMNAME '=' value=Integer
;

TemplateTypeDeclaration  :
    name=ID 'extends' interfaces+=[Interface] ( ',' interfaces+=[Interface] )* 
;

// A typedef found in many places (spec, gal, composite)
TypedefDeclaration: (comment=COMMENT)? 'typedef' name=ID '=' min=BitOr '..' max=BitOr ';';

InstanceDecl :
    InstanceDeclaration | ArrayInstanceDeclaration
;

ParamDef :
    param=[ConstParameter|PARAMNAME] '=' value=Integer 
;


InstanceDeclaration :
    type = [TypeDeclaration] name = FullyQualifiedName 
    ( '(' paramDefs+=ParamDef  (',' paramDefs+=ParamDef )* ')' )? ';'
;

ArrayInstanceDeclaration :
    type = [TypeDeclaration] '[' size=INT ']'  name = FullyQualifiedName 
    ( '(' paramDefs+=ParamDef  (',' paramDefs+=ParamDef )* ')' )? ';'
;


Synchronization:
    'synchronization' name = ID 
    ('(' params+=Parameter     ( ',' params+=Parameter)* ')')?     
    'label' label = Label '{'
        (actions+=CompStatement)*
    '}'
;


// A constant defined as type parameter or global specification level
ConstParameter : 
    name=PARAMNAME '=' value=Integer
;


// A typedef found in many places (spec, gal, composite)
TypedefDeclaration: (comment=COMMENT)? 'typedef' name=ID '=' min=BitOr '..' max=BitOr ';';


2.6 Named declaration

download NamedDeclaration : VarDecl | InstanceDecl ;


// GAL referables
VarDecl :
    VariableDeclaration | ArrayDeclaration
;

//Ex: int abc = 10 ; 
VariableDeclaration returns Variable:
    (comment=COMMENT)?
    (hotbit?='hotbit' '(' hottype=[TypedefDeclaration] ')')? 'int' name=FullyQualifiedName '=' value=BitOr ';';


    //Ex: array[1] tab = (2) ;
ArrayDeclaration returns ArrayPrefix:
    (comment=COMMENT)?
    (hotbit?='hotbit' '(' hottype=[TypedefDeclaration] ')')? 
    'array' '[' size=INT ']' name=FullyQualifiedName '=' '(' ( (values+=BitOr) (',' values+=BitOr)* )? ')' ';';


// composite referables
InstanceDecl :
    InstanceDeclaration | ArrayInstanceDeclaration
;

InstanceDeclaration :
    type = [TypeDeclaration] name = FullyQualifiedName 
    ( '(' paramDefs+=ParamDef  (',' paramDefs+=ParamDef )* ')' )? ';'
;

ArrayInstanceDeclaration :
    type = [TypeDeclaration] '[' size=INT ']'  name = FullyQualifiedName 
    ( '(' paramDefs+=ParamDef  (',' paramDefs+=ParamDef )* ')' )? ';'
;


// a reference
VariableReference :
    ref=[NamedDeclaration|FullyQualifiedName] 
        (-> '[' index=BitOr ']' )?
;

2.7 References

download Reference :
VariableReference 
        (
            (-> ':' {QualifiedReference.qualifier=current} next=Reference )
            
        )?     
;


VariableReference :
    ref=[NamedDeclaration|FullyQualifiedName] 
        (-> '[' index=BitOr ']' )?
;

2.8 Statements

download
// transitions bear statements parsed with GalStatement rule
Transition:
    (comment=COMMENT)? 
    'transition' name=FullyQualifiedName 
    ('(' params+=Parameter     ( ',' params+=Parameter)* ')')? 
    '[' guard=Or ']' 
    ('label' label=Label)? 
    '{'
    (actions+=GalStatement)*
    '}';

GalStatement returns Statement :
    GalIte | Abort | Fixpoint | GalFor | SelfCall | Assignment 
;

// synchronizations use CompStatement rule
Synchronization:
    'synchronization' name = ID 
    ('(' params+=Parameter     ( ',' params+=Parameter)* ')')?     
    'label' label = Label '{'
        (actions+=CompStatement)*
    '}'
;

CompStatement returns Statement :
    CompIte | Abort | CompFor | SelfCall  | InstanceCall
;

// The statements, grammar rules are duplicated in places
// so that recursive parse into control structure (for, if)
//enforces type of statements encountered 
Assignment:
    (comment=COMMENT)?     
   left=VariableReference '=' right=BitOr ';';

InstanceCall:
        (comment=COMMENT)?         
    instance=VariableReference '.' label=[Label|STRING] ';'
;

GalIte returns Ite:(comment=COMMENT)?     
    'if' '(' cond=Or ')' '{' (ifTrue+=GalStatement)* '}'
    ('else'  '{' (ifFalse+=GalStatement)*  '}')?    
;

CompIte returns Ite:(comment=COMMENT)?     
    'if' '(' cond=Or ')' '{' (ifTrue+=CompStatement)* '}'
    ('else'  '{' (ifFalse+=CompStatement)*  '}')?    
;

Fixpoint:
    {Fixpoint}
    (comment=COMMENT)?     
    'fixpoint' '{' (actions+=GalStatement)* '}'
;


SelfCall:
    (comment=COMMENT)?     
    'self' '.' label=[Label|STRING] ';';

Abort:
    {Abort} 
    (comment=COMMENT)?     
    'abort' ';'
;

GalFor returns For: 
    (comment=COMMENT)?         
    'for' '(' param=ForParameter ')' 
    '{'
        (actions+=GalStatement)*
    '}' 
;


CompFor returns For: 
    (comment=COMMENT)?         
    'for' '(' param=ForParameter ')' 
    '{'
        (actions+=CompStatement)*
    '}' 
;

ForParameter returns Parameter: 
    name=PARAMNAME ':' type=[TypedefDeclaration] 
;

2.9 Parameters

download
AbstractParameter :
    Parameter | ConstParameter 
;

Parameter :
    type=[TypedefDeclaration] name=PARAMNAME
;

// for control structure
For : 
    (comment=COMMENT)?         
    'for' '(' param=ForParameter ')' 
    '{'
        (actions+=Statement)*
    '}' 
;

ForParameter returns Parameter: 
    name=PARAMNAME ':' type=[TypedefDeclaration] 
;




// a primary int expression
ParamRef:
    refParam=[AbstractParameter|PARAMNAME]
;

// A constant defined as type parameter or global specification level
ConstParameter : 
    name=PARAMNAME '=' value=Integer
;

ParamDef :
    param=[ConstParameter|PARAMNAME] '=' value=Integer 
;

// instances can override const parameter values using ParamDef
InstanceDeclaration :
    type = [TypeDeclaration] name = FullyQualifiedName 
    ( '(' paramDefs+=ParamDef  (',' paramDefs+=ParamDef )* ')' )? ';'
;

ArrayInstanceDeclaration :
    type = [TypeDeclaration] '[' size=INT ']'  name = FullyQualifiedName 
    ( '(' paramDefs+=ParamDef  (',' paramDefs+=ParamDef )* ')' )? ';'
;

// Start with $ and build an ID
terminal PARAMNAME:
    '$'  ('^')?('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'0'..'9')*;

Acknowledgements

The GAL metamodel, xtext grammar, and this page are the work of Yann Thierry-Mieg. The initial metamodel/grammar of GAL was built during the internship (Master 1 2011) of KOUADIO Stephane, SELLOU Hakim and ABKA Faycal. Initial version of composite metamodel/grammar was built during internship (Master 1 2012) of CANTAIS Alexis and TRAN Marie-Diana.

Bas