Permalink
Find file Copy path
3681ed0 May 1, 2017
2 contributors

Users who have contributed to this file

@yanntm @dvojtise
729 lines (525 sloc) 17 KB
grammar fr.lip6.move.Gal with org.eclipse.xtext.common.Terminals
generate gal "http://www.lip6.fr/move/Gal"
import "http://www.eclipse.org/emf/2002/Ecore" as ecore
Specification :
imports+=Import*
(interfaces+=Interface
| types+=GALOrCompositeTypeDeclaration
| typedefs+=TypedefDeclaration
| params += ConstParameter ';'
)*
(
'main' main=[TypeDeclaration|FullyQualifiedName] ';'
)?
(properties+=Property) *
;
Import:
'import' importURI=STRING ';'
;
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
;
/**
* System
*/
GALTypeDeclaration:
('gal'|'GAL') name=FullyQualifiedName
('('
params += ConstParameter
( ',' params+= ConstParameter)*
')')?
'{'
(
(typedefs+=TypedefDeclaration)
|(variables+=VariableDeclaration)
|(arrays+=ArrayDeclaration)
// |(lists+=ListDeclaration)
)*
(transitions+=Transition
| predicates+=Predicate
)*
('TRANSIENT' '=' transient=Or ';')?
'}';
CompositeTypeDeclaration :
'composite' name=ID
( '<' templateParams+=TemplateTypeDeclaration ( ',' templateParams +=TemplateTypeDeclaration )* '>' )?
('('
params += ConstParameter
( ',' params+= ConstParameter)*
')')?
'{'
(typedefs+=TypedefDeclaration |
instances+=InstanceDecl)*
(synchronizations+=Synchronization)*
'}'
;
// A typedef found in many places (spec, gal, composite)
TypedefDeclaration: (comment=COMMENT)? 'typedef' name=ID '=' min=KBitOr '..' max=KBitOr ';';
TemplateTypeDeclaration :
name=ID 'extends' interfaces+=[Interface] ( ',' interfaces+=[Interface] )*
;
/* ============ GAL System Content ================== */
NamedDeclaration : VarDecl | InstanceDecl ;
VarDecl :
VariableDeclaration | ArrayDeclaration
;
InstanceDecl :
InstanceDeclaration | ArrayInstanceDeclaration
;
//Ex: int abc = 10 ;
VariableDeclaration returns Variable:
(comment=COMMENT)?
(hotbit?='hotbit' '(' hottype=[TypedefDeclaration] ')')?
'int' name=FullyQualifiedName
('=' value=KBitOr)? /* initial value is now optional, default is 0 */
';'
;
//Ex: array[1] tab = (2) ;
ArrayDeclaration returns ArrayPrefix:
(comment=COMMENT)?
(hotbit?='hotbit' '(' hottype=[TypedefDeclaration] ')')?
'array' '[' size=KBitOr ']' name=FullyQualifiedName
('=' '(' ( (values+=KBitOr) (',' values+=KBitOr)* )? ')')? /* we assume 0 as initial values for all cells */
';'
;
//ListDeclaration returns List:
// 'list' name=FullyQualifiedName ('=' '(' ( (values+=BitOr) (',' values+=BitOr)* )? ')')? ';';
Event : Transition | Synchronization;
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 ';'
;
AbstractParameter :
Parameter | ConstParameter
;
Parameter :
type=[TypedefDeclaration] name=PARAMNAME
;
// A constant defined as type parameter or global specification level
ConstParameter :
name=PARAMNAME '=' value=Integer
;
GalStatement returns Statement :
GalIte | Abort | Fixpoint | GalFor | SelfCall | Assignment
;
CompStatement returns Statement :
CompIte | Abort | CompFor | LabelCall
;
LabelCall :
SelfCall | InstanceCall
;
// The statements, grammar rules are duplicated in places
// so that recursive parse into control structure (for, if)
//enforces type of statements encountered
/* ========= Transition Content ============ */
//Statement: Ite | Abort | Fixpoint | For | SelfCall | Assignment | InstanceCall
// | Push | Pop
// ;
//Push:
// 'push' '(' list=[List|FullyQualifiedName] ',' value=BitOr ')' ';';
//
//Pop:
// 'pop' '(' list=[List|FullyQualifiedName] ')' ';';
Assignment:
(comment=COMMENT)?
left=VariableReference type=AssignType right=BitOr ';';
enum AssignType :
ASSIGN='='
| INCR='+='
| DECR='-='
;
InstanceCall:
(comment=COMMENT)?
instance=VariableReference '.' label=[Label|STRING] ('(' params+=KBitOr (',' params+=KBitOr)* ')')? ';'
;
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] ('(' params+=KBitOr (',' params+=KBitOr)* ')')? ';';
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]
;
Reference :
VariableReference
(
(-> ':' {QualifiedReference.qualifier=current} next=Reference )
)?
;
VariableReference :
ref=[NamedDeclaration|FullyQualifiedName]
(-> '[' index=BitOr ']' )?
;
ParamRef:
refParam=[AbstractParameter|PARAMNAME]
;
/* ==== Properties ========== */
Property : 'property' (name=ID | name=STRING) body=LogicProp ';' ;
LogicProp : SafetyProp | BoundsProp | CTLProp | LTLProp ;
SafetyProp : ReachableProp | InvariantProp | NeverProp
;
BoundsProp : '[' 'bounds' ']' ':' target=BoundsPredicate ;
ReachableProp : '[' 'reachable' ']' ':' predicate=POr;
InvariantProp : '[' 'invariant' ']' ':' predicate=POr;
NeverProp : '[' 'never' ']' ':' predicate=POr;
CTLProp : '[' 'ctl' ']' ':' predicate=CTLUntil;
LTLProp : '[' 'ltl' ']' ':' predicate=LTLUntil;
/* ===== 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:
VariableReference |
ConstRef |
(=> ('(' BitOr ')') | ('(' WrapBoolExpr ')'));
ConstRef returns IntExpression:
Constant |
ParamRef ;
WrapBoolExpr:
value=Or;
Constant:
value=INT;
// constant expressions K_ don't have variables inside
KBitOr returns IntExpression:
KBitXor ({BinaryIntExpression.left=current} op='|' right=KBitXor)*;
KBitXor returns IntExpression:
KBitAnd ({BinaryIntExpression.left=current} op='^' right=KBitAnd)*;
KBitAnd returns IntExpression:
KBitShift ({BinaryIntExpression.left=current} op='&' right=KBitShift)*;
KBitShift returns IntExpression:
KAddition ({BinaryIntExpression.left=current} op=('<<' | '>>') right=KAddition)*;
KAddition returns IntExpression:
KMultiplication ({BinaryIntExpression.left=current} op=('+' | '-') right=KMultiplication)*;
KMultiplication returns IntExpression:
KUnaryExpr ({BinaryIntExpression.left=current} op=('/' | '*' | '%') right=KUnaryExpr)*;
KUnaryExpr returns IntExpression :
KBitComplement | KUnaryMinus | KPower
;
KUnaryMinus returns IntExpression:
{UnaryMinus} '-' value=KUnaryExpr;
KBitComplement returns IntExpression:
{BitComplement} '~' value=KUnaryExpr ;
KPower returns IntExpression:
KPrimary ({BinaryIntExpression.left=current} op=('**') right=KPrimary)*;
KPrimary returns IntExpression:
ConstRef |
(=> ('(' KBitOr ')') | ('(' KWrapBoolExpr ')'));
KWrapBoolExpr returns WrapBoolExpr :
value=KOr;
KOr returns BooleanExpression:
(KAnd ({Or.left=current} ->'||' right=KAnd)*);
KAnd returns BooleanExpression:
KNot ({And.left=current} ->'&&' right=KNot)*;
KNot returns BooleanExpression:
(->'!' {Not} value=KPrimaryBool) | KPrimaryBool;
KPrimaryBool returns BooleanExpression:
True | False | => KComparison | ('(' KOr ')');
KComparison returns Comparison:
(left=KBitOr
->operator=ComparisonOperators
right=KBitOr);
// P_ versions are for predicates in property queries
PBitOr returns IntExpression:
PBitXor ({BinaryIntExpression.left=current} op='|' right=PBitXor)*;
PBitXor returns IntExpression:
PBitAnd ({BinaryIntExpression.left=current} op='^' right=PBitAnd)*;
PBitAnd returns IntExpression:
PBitShift ({BinaryIntExpression.left=current} op='&' right=PBitShift)*;
PBitShift returns IntExpression:
PAddition ({BinaryIntExpression.left=current} op=('<<' | '>>') right=PAddition)*;
PAddition returns IntExpression:
PMultiplication ({BinaryIntExpression.left=current} op=('+' | '-') right=PMultiplication)*;
PMultiplication returns IntExpression:
PUnaryExpr ({BinaryIntExpression.left=current} op=('/' | '*' | '%') right=PUnaryExpr)*;
PUnaryExpr returns IntExpression :
PBitComplement | PUnaryMinus | PPrimary
;
PUnaryMinus returns IntExpression:
{UnaryMinus} '-' value=PUnaryExpr;
PBitComplement returns IntExpression:
{BitComplement} '~' value=PUnaryExpr ;
PPrimary returns IntExpression:
Reference |
ConstRef |
(=> ('(' PBitOr ')') | ('(' PWrapBoolExpr ')'));
PWrapBoolExpr returns WrapBoolExpr:
value=POr;
POr returns BooleanExpression:
(PAnd ({Or.left=current} ->'||' right=PAnd)*);
PAnd returns BooleanExpression:
PNot ({And.left=current} ->'&&' right=PNot)*;
PNot returns BooleanExpression:
(->'!' {Not} value=PPrimaryBool) | PPrimaryBool;
PPrimaryBool returns BooleanExpression:
True | False | => PComparison | ('(' POr ')');
PComparison returns Comparison:
(left=PBitOr
->operator=ComparisonOperators
right=PBitOr);
// CTL_ versions are for predicates in CTL property queries
CTLBitOr returns IntExpression:
CTLBitXor ({BinaryIntExpression.left=current} op='|' right=CTLBitXor)*;
CTLBitXor returns IntExpression:
CTLBitAnd ({BinaryIntExpression.left=current} op='^' right=CTLBitAnd)*;
CTLBitAnd returns IntExpression:
CTLBitShift ({BinaryIntExpression.left=current} op='&' right=CTLBitShift)*;
CTLBitShift returns IntExpression:
CTLAddition ({BinaryIntExpression.left=current} op=('<<' | '>>') right=CTLAddition)*;
CTLAddition returns IntExpression:
CTLMultiplication ({BinaryIntExpression.left=current} op=('+' | '-') right=CTLMultiplication)*;
CTLMultiplication returns IntExpression:
CTLUnaryExpr ({BinaryIntExpression.left=current} op=('/' | '*' | '%') right=CTLUnaryExpr)*;
CTLUnaryExpr returns IntExpression :
CTLBitComplement | CTLUnaryMinus | CTLPrimary
;
CTLUnaryMinus returns IntExpression:
{UnaryMinus} '-' value=CTLUnaryExpr;
CTLBitComplement returns IntExpression:
{BitComplement} '~' value=CTLUnaryExpr ;
CTLPrimary returns IntExpression:
Reference |
ConstRef |
(=> ('(' CTLBitOr ')') | ('(' CTLWrapBoolExpr ')'));
CTLWrapBoolExpr returns WrapBoolExpr:
value=CTLOr;
CTLUntil returns BooleanExpression:
('A' {AU} left=CTLImply 'U' right=CTLImply)
|('E' {EU} left=CTLImply 'U' right=CTLImply)
| CTLImply
;
CTLImply returns BooleanExpression:
(CTLEquiv ({Imply.left=current} ->'->' right=CTLEquiv)*);
CTLEquiv returns BooleanExpression:
(CTLOr ({Equiv.left=current} ->'<->' right=CTLOr)*);
CTLOr returns BooleanExpression:
(CTLAnd ({Or.left=current} ->'||' right=CTLAnd)*);
CTLAnd returns BooleanExpression:
CTLTemporal ({And.left=current} ->'&&' right=CTLTemporal)*;
CTLTemporal returns BooleanExpression :
('AG' {AG} prop=CTLNot )
|('AF' {AF} prop=CTLNot )
|('AX' {AX} prop=CTLNot )
|('EG' {EG} prop=CTLNot )
|('EF' {EF} prop=CTLNot )
|('EX' {EX} prop=CTLNot )
| CTLNot
;
CTLNot returns BooleanExpression:
(->'!' {Not} value=CTLPrimaryBool) | CTLPrimaryBool;
CTLPrimaryBool returns BooleanExpression:
True | False | => CTLComparison | ('(' CTLUntil ')');
CTLComparison returns Comparison:
(left=CTLBitOr
->operator=ComparisonOperators
right=CTLBitOr);
// LTL_ versions are for predicates in LTL property queries
LTLBitOr returns IntExpression:
LTLBitXor ({BinaryIntExpression.left=current} op='|' right=LTLBitXor)*;
LTLBitXor returns IntExpression:
LTLBitAnd ({BinaryIntExpression.left=current} op='^' right=LTLBitAnd)*;
LTLBitAnd returns IntExpression:
LTLBitShift ({BinaryIntExpression.left=current} op='&' right=LTLBitShift)*;
LTLBitShift returns IntExpression:
LTLAddition ({BinaryIntExpression.left=current} op=('<<' | '>>') right=LTLAddition)*;
LTLAddition returns IntExpression:
LTLMultiplication ({BinaryIntExpression.left=current} op=('+' | '-') right=LTLMultiplication)*;
LTLMultiplication returns IntExpression:
LTLUnaryExpr ({BinaryIntExpression.left=current} op=('/' | '*' | '%') right=LTLUnaryExpr)*;
LTLUnaryExpr returns IntExpression :
LTLBitComplement | LTLUnaryMinus | LTLPrimary
;
LTLUnaryMinus returns IntExpression:
{UnaryMinus} '-' value=LTLUnaryExpr;
LTLBitComplement returns IntExpression:
{BitComplement} '~' value=LTLUnaryExpr ;
LTLPrimary returns IntExpression:
Reference
| ConstRef
| ( '(' LTLBitOr ')' )
;
LTLImply returns BooleanExpression:
LTLEquiv ({Imply.left=current} ->'->' right=LTLEquiv)?;
LTLEquiv returns BooleanExpression:
LTLOr ({Equiv.left=current} ->'<->' right=LTLOr)?;
LTLOr returns BooleanExpression:
LTLAnd ({Or.left=current} ->'||' right=LTLAnd)*;
LTLAnd returns BooleanExpression:
LTLUntil ({And.left=current} ->'&&' right=LTLUntil)*;
LTLUntil returns BooleanExpression:
LTLFutGen
(
( 'U' {LTLUntil.left = current} right=LTLFutGen)
|( 'W' {LTLWeakUntil.left = current} right=LTLFutGen)
|( 'M' {LTLStrongRelease.left = current} right=LTLFutGen)
|('R' {LTLRelease.left = current} right=LTLFutGen)
)?
;
LTLFutGen returns BooleanExpression :
('F' {LTLFuture} prop=LTLFutGen)
|('G' {LTLGlobally} prop=LTLFutGen)
| LTLNext
;
LTLNext returns BooleanExpression :
('X' {LTLNext} prop=LTLNext)
| LTLNot
;
LTLNot returns BooleanExpression:
(->'!' {Not} value=LTLPrimaryBool) | LTLPrimaryBool;
LTLPrimaryBool returns BooleanExpression:
True | False | => LTLComparison | ('(' LTLImply ')');
LTLComparison returns Comparison:
(left=LTLBitOr
->operator=ComparisonOperators
right=LTLBitOr);
// Bounds versions are severely limited to sums
BoundsPredicate returns IntExpression :
BPPrimary ({BinaryIntExpression.left=current} op='+' right=BPPrimary)*;
BPPrimary returns IntExpression:
Reference |
ConstRef ;
// | Peek is a Primary
//Peek:
// 'peek' '(' list=[List|FullyQualifiedName] ')';
/* ===== 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';
ParamDef :
param=[ConstParameter|PARAMNAME] '=' value=Integer
;
InstanceDeclaration :
type = [TypeDeclaration] name = FullyQualifiedName
( '(' paramDefs+=ParamDef (',' paramDefs+=ParamDef )* ')' )? ';'
;
ArrayInstanceDeclaration :
type = [TypeDeclaration] '[' size=KBitOr ']' name = FullyQualifiedName
( '(' paramDefs+=ParamDef (',' paramDefs+=ParamDef )* ')' )? ';'
;
Synchronization:
'synchronization' name = ID
('(' params+=Parameter ( ',' params+=Parameter)* ')')?
('label' label = Label)? '{'
(actions+=CompStatement)*
'}'
;
/* ===== Basic types ===== */
// This means a quoted "arbitrary #d%$ string"
Label :
name=STRING ('(' params+=BitOr (',' params+=BitOr)* ')')?
;
// 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
terminal COMMENT :
'/**' -> '*/'
;
// override default behavior
terminal ML_COMMENT :
'xxxXXXxxx'
;
// Note that SL_COMMENT, i.e. "// to \n"
// comments to end of line
// it goes to hidden channel
// 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;