/***************************************************************
------------------------- TOKENS ---------------------------
***************************************************************/ |
<DEFAULT,GENERIC_ID,MODULE_ID> SKIP : {
" "
| "\r"
| "\t"
| "\n"
| <"//" (~["\n","\r"])* ("\n" | "\r" | "\r\n")>
| <"/*" (~["*"])* "*" ("*" | ~["*","/"] (~["*"])* "*")* "/">
}
|
/* RESERVED WORDS */ |
<DEFAULT> TOKEN : {
<ASM: "asm"> : GENERIC_ID
| <MODULE: "module"> : GENERIC_ID
| <ASYNCR: "asyncr">
| <IMPORT: "import"> : MODULE_ID
| <EXPORT: "export">
| <SIGNATURE: "signature">
| <INIT: "init"> : GENERIC_ID
| <Default: "default">
| <AGENT: "agent">
| <INVARIANT: "invariant">
| <OVER: "over">
| <DEFINITIONS: "definitions">
| <FUNCTION: "function">
| <STATIC: "static">
| <DYNAMIC: "dynamic">
| <DERIVED: "derived">
| <MONITORED: "monitored">
| <CONTROLLED: "controlled">
| <SHARED: "shared">
| <OUT: "out">
| <DOMAIN: "domain">
| <ANYDOMAIN: "anydomain">
| <BASIC: "basic">
| <ABSTRACT: "abstract">
| <ENUM: "enum">
| <SUBSETOF: "subsetof">
| <PROD: "Prod">
| <SEQ: "Seq">
| <POWERSET: "Powerset">
| <BAG: "Bag">
| <MAP: "Map">
| <RULEDOM: "Rule">
| <TRUE: "true">
| <FALSE: "false">
| <UNDEF: "undef">
| <IM_PART: "i">
| <IF: "if">
| <THEN: "then">
| <ELSE: "else">
| <ENDIF: "endif">
| <SWITCH: "switch">
| <END_SWITCH: "endswitch">
| <CASE: "case">
| <OTHERWISE: "otherwise">
| <ENDCASE: "endcase">
| <LET: "let">
| <ENDLET: "endlet">
| <EXIST: "exist">
| <UNIQUE: "unique">
| <WITH: "with">
| <FORALL: "forall">
| <Skip: "skip">
| <RULE: "rule">
| <MACRO: "macro">
| <TURBO: "turbo">
| <MAIN: "main">
| <PAR: "par">
| <ENDPAR: "endpar">
| <CHOOSE: "choose">
| <DO: "do">
| <IFNONE: "ifnone">
| <EXTEND: "extend">
| <seq: "seq">
| <ENDSEQ: "endseq">
| <ITERATE: "iterate">
| <ENDITERATE: "enditerate">
| <LOCAL: "local">
| <TRY: "try">
| <CATCH: "catch">
| <WHILE: "while">
| <WHILEREC: "whilerec">
| <IN: "in">
| <EQ: "=">
| <LT: "<">
| <LE: "<=">
| <GT: ">">
| <GE: ">=">
| <NEQ: "!=">
| <PLUS: "+">
| <MINUS: "-">
| <MULT: "*">
| <DIV: "/">
| <PWR: "^">
}
|
/* IDENTIFIERS AND NUMBERS */ |
<DEFAULT> TOKEN : {
<NUMBER: (<DIGIT>)+>
| <NATNUMBER: (<DIGIT>)+ "n">
| <REAL_NUMBER: (<DIGIT>)+ "." (<DIGIT>)+>
| <COMPLEX_NUMBER: ((["+","-"])? (<DIGIT>)+ ("." (<DIGIT>)+)?)? (["+","-"])? "i" ((<DIGIT>)+ ("." (<DIGIT>)+)?)?>
| <ID_VARIABLE: "$" <LETTER> (<LETTER> | <DIGIT>)*>
| <ID_ENUM: ["A"-"Z"] ["A"-"Z"] ("_" | ["A"-"Z"] | <DIGIT>)*>
| <ID_DOMAIN: ["A"-"Z"] ("_" | ["a"-"z"] | ["A"-"Z"] | <DIGIT>)*>
| <ID_RULE: "r_" (<LETTER> | <DIGIT>)+>
| <ID_INVARIANT: "inv_" (<LETTER> | <DIGIT>)+>
| <ID_FUNCTION: ["a"-"z"] (<LETTER> | <DIGIT>)*>
| <#LETTER: ["_","a"-"z","A"-"Z"]>
| <#DIGIT: ["0"-"9"]>
| <CHAR_LITERAL: "\'" (~["\'","\\","\n","\r"] | "\\" (["n","t","b","r","f","\\","\'","\""] | ["0"-"7"] (["0"-"7"])? | ["0"-"3"] ["0"-"7"] ["0"-"7"]))* "\'">
| <STRING_LITERAL: "\"" (~["\"","\\","\n","\r"] | "\\" (["n","t","b","r","f","\\","\'","\""] | ["0"-"7"] (["0"-"7"])? | ["0"-"3"] ["0"-"7"] ["0"-"7"]))* "\"">
}
|
<GENERIC_ID> TOKEN : {
<ID: <LETTER> (<LETTER> | <DIGIT>)*> : DEFAULT
}
|
<MODULE_ID> TOKEN : {
<MOD_ID: (<LETTER> | "." | "/" | "\\") (<LETTER> | <DIGIT> | "." | "/" | "\\" | ":")*> : DEFAULT
}
|
Asm |
::= |
( <ASYNCR> )? ( <ASM>
| <MODULE> ) ID Header
Body ( <MAIN> MacroDeclaration
)? ( ( Initialization )* <Default> Initialization ( Initialization
)* )? <EOF>
|
Header |
::= |
( ImportClause
)* ( ExportClause )? Signature |
ImportClause |
::= |
<IMPORT> MOD_ID
( "(" ( ID_DOMAIN | ID_FUNCTION
| ID_RULE ) ( "," ( ID_DOMAIN
| ID_FUNCTION | ID_RULE
) )* ")" )?
|
ExportClause |
::= |
<EXPORT> ( ( ( ID_DOMAIN | ID_FUNCTION | ID_RULE ) ( "," ( ID_DOMAIN
| ID_FUNCTION | ID_RULE
) )* ) | "*" )
|
Signature |
::= |
<SIGNATURE> ":" ( Domain )* ( Function )*
|
Initialization |
::= |
<INIT> ID
":" ( DomainInitialization )* ( FunctionInitialization )* ( AgentInitialization
)*
|
DomainInitialization |
::= |
<DOMAIN> ID_DOMAIN
"=" Term |
FunctionInitialization |
::= |
<FUNCTION> ID_FUNCTION ( "(" VariableTerm
<IN> getDomainByID ( "," VariableTerm <IN> getDomainByID
)* ")" )? "=" Term |
AgentInitialization |
::= |
<AGENT> ID_DOMAIN
":" MacroCallRule |
Body |
::= |
<DEFINITIONS> ":" ( DomainDefinition )* ( FunctionDefinition
)* ( RuleDeclaration )* ( Invariant
)*
|
DomainDefinition |
::= |
<DOMAIN> ID_DOMAIN
"=" Term |
FunctionDefinition |
::= |
<FUNCTION> ID_FUNCTION ( "(" VariableTerm
<IN> getDomainByID ( "," VariableTerm <IN> getDomainByID
)* ")" )? "=" Term |
RuleDeclaration |
::= |
( MacroDeclaration
| TurboDeclaration )
|
MacroDeclaration |
::= |
( <MACRO> )? <RULE> ID_RULE ( "(" VariableTerm
<IN> getDomainByID ( "," VariableTerm <IN> getDomainByID
)* ")" )? "=" Rule |
TurboDeclaration |
::= |
<TURBO> <RULE> ID_RULE ( "(" VariableTerm
<IN> getDomainByID ( "," VariableTerm <IN> getDomainByID
)* ")" )? ( <IN> getDomainByID )? "=" Rule |
Invariant |
::= |
<INVARIANT> ( ID_INVARIANT )? <OVER> ( ID_DOMAIN
| ID_FUNCTION ( "(" ( getDomainByID
)? ")" )? | ID_RULE ) ( "," ( ID_DOMAIN | ID_FUNCTION (
"(" ( getDomainByID )? ")" )? | ID_RULE ) )* ":" Term |
Domain |
::= |
( ConcreteDomain
| TypeDomain )
|
ConcreteDomain |
::= |
( <DYNAMIC> )?
<DOMAIN> ID_DOMAIN <SUBSETOF> getDomainByID
|
TypeDomain |
::= |
( AnyDomain
| StructuredTD | EnumTD
| AbstractTD | BasicTD )
|
AnyDomain |
::= |
<ANYDOMAIN> ID_DOMAIN |
BasicTD |
::= |
<BASIC> <DOMAIN> ID_DOMAIN |
AbstractTD |
::= |
( <DYNAMIC> )?
<ABSTRACT> <DOMAIN> ID_DOMAIN
|
EnumTD |
::= |
<ENUM> <DOMAIN> ID_DOMAIN "=" "{" EnumElement
( "|" EnumElement )* "}"
|
EnumElement |
::= |
ID_ENUM |
StructuredTD |
::= |
( ProductDomain
| SequenceDomain | PowersetDomain
| BagDomain | MapDomain
)
|
ProductDomain |
::= |
<PROD> "(" getDomainByID ( "," getDomainByID
)+ ")"
|
SequenceDomain |
::= |
<SEQ> "(" getDomainByID
")"
|
PowersetDomain |
::= |
<POWERSET> "(" getDomainByID ")"
|
BagDomain |
::= |
<BAG> "(" getDomainByID
")"
|
MapDomain |
::= |
<MAP> "(" getDomainByID
"," getDomainByID ")"
|
getDomainByID |
::= |
( ID_DOMAIN
| StructuredTD )
|
Function |
::= |
( BasicFunction
| DerivedFunction )
|
BasicFunction |
::= |
( StaticFunction
| DynamicFunction )
|
DerivedFunction |
::= |
<DERIVED> ID_FUNCTION
":" ( getDomainByID "->" )? getDomainByID |
StaticFunction |
::= |
<STATIC> ID_FUNCTION
":" ( getDomainByID "->" )? getDomainByID |
DynamicFunction |
::= |
( OutFunction
| MonitoredFunction | SharedFunction
| ControlledFunction | LocalFunction
)
|
LocalFunction |
::= |
( <DYNAMIC> )?
<LOCAL> ID_FUNCTION ":" ( getDomainByID "->" )? getDomainByID
|
ControlledFunction |
::= |
( <DYNAMIC> )?
<CONTROLLED> ID_FUNCTION ":" ( getDomainByID "->" )? getDomainByID
|
SharedFunction |
::= |
( <DYNAMIC> )?
<SHARED> ID_FUNCTION ":" ( getDomainByID "->" )? getDomainByID
|
MonitoredFunction |
::= |
( <DYNAMIC> )?
<MONITORED> ID_FUNCTION ":" ( getDomainByID "->" )? getDomainByID
|
OutFunction |
::= |
( <DYNAMIC> )? <OUT>
ID_FUNCTION ":" ( getDomainByID
"->" )? getDomainByID
|
Term |
::= |
( Expression
| ExtendedTerm )
|
Expression |
::= |
or_xorLogicExpr
( ( <ID_FUNCTION> or_xorLogicExpr |
<ID_FUNCTION> or_xorLogicExpr ) )* |
or_xorLogicExpr |
::= |
andLogicExpr
( ( <ID_FUNCTION> | <ID_FUNCTION> ) andLogicExpr
)* |
andLogicExpr |
::= |
relationalExpr
( <ID_FUNCTION> relationalExpr )* |
relationalExpr |
::= |
notLogicExpr
( ( <EQ> notLogicExpr | <NEQ> notLogicExpr | <LT> notLogicExpr
| <LE> notLogicExpr | <GT> notLogicExpr | <GE> notLogicExpr
) )* |
notLogicExpr |
::= |
( <ID_FUNCTION> additiveExpr | additiveExpr
)
|
additiveExpr |
::= |
multiplicativeExpr
( ( <PLUS> multiplicativeExpr |
<MINUS> multiplicativeExpr ) )* |
multiplicativeExpr |
::= |
powerExpr (
( <MULT> powerExpr | <DIV> powerExpr | <ID_FUNCTION> powerExpr
) )* |
powerExpr |
::= |
unaryExpr (
<PWR> unaryExpr )* |
unaryExpr |
::= |
( ( <PLUS> unaryExpr | <MINUS> unaryExpr
) | basicExpr )
|
basicExpr |
::= |
( BasicTerm
| DomainTerm | FiniteQuantificationTerm
| "(" Expression ")" )
|
BasicTerm |
::= |
( ConstantTerm
| VariableTerm | FunctionTerm
)
|
FunctionTerm |
::= |
( ID_AGENT
"." )? ID_FUNCTION ( TupleTerm
)?
|
LocationTerm |
::= |
( ID_AGENT
"." )? ID_FUNCTION ( TupleTerm
)?
|
VariableTerm |
::= |
ID_VARIABLE |
ConstantTerm |
::= |
( ComplexTerm
| RealTerm | IntegerTerm
| NaturalTerm | CharTerm
| StringTerm | BooleanTerm
| UndefTerm | EnumTerm )
|
ComplexTerm |
::= |
<COMPLEX_NUMBER> |
RealTerm |
::= |
( <REAL_NUMBER> ) |
IntegerTerm |
::= |
<NUMBER> |
NaturalTerm |
::= |
<NATNUMBER> |
CharTerm |
::= |
<CHAR_LITERAL> |
StringTerm |
::= |
<STRING_LITERAL> |
BooleanTerm |
::= |
( <TRUE> | <FALSE> ) |
UndefTerm |
::= |
<UNDEF> |
EnumTerm |
::= |
ID_ENUM |
ExtendedTerm |
::= |
( ConditionalTerm
| CaseTerm | TupleTerm |
VariableBindingTerm | CollectionTerm
| RuleAsTerm | DomainTerm
)
|
ConditionalTerm |
::= |
<IF> Term
<THEN> Term ( <ELSE> Term )? <ENDIF>
|
CaseTerm |
::= |
<SWITCH> Term
( <CASE> Term ":" Term
)+ ( <OTHERWISE> Term )?
<END_SWITCH>
|
TupleTerm |
::= |
"(" Term (
"," Term )* ")"
|
CollectionTerm |
::= |
( SequenceTerm
| MapTerm | SetTerm | BagTerm )
|
SequenceTerm |
::= |
"[" ( Term
( ( "," Term )+ | ( ":" Term
( "," ( Term ) )? ) )? )? "]"
|
SetTerm |
::= |
"{" ( Term
( ( "," Term )+ | ( ":" Term
( "," ( Term ) )? ) )? )? "}"
|
MapTerm |
::= |
"{" ( "->" | ( Term "->" Term ( "," Term "->" Term )* ) )
"}"
|
BagTerm |
::= |
"<" ( Term
( ( "," Term )+ | ( ":" Term
( "," ( Term ) )? ) )? )? ">"
|
VariableBindingTerm |
::= |
( LetTerm |
FiniteQuantificationTerm | ComprehensionTerm
)
|
FiniteQuantificationTerm |
::= |
( ForallTerm
| ExistUniqueTerm | ExistTerm
)
|
ExistTerm |
::= |
"(" <EXIST> VariableTerm <IN> Term
( "," VariableTerm <IN> Term )* ( <WITH> Term
)? ")"
|
ExistUniqueTerm |
::= |
"(" <EXIST> <UNIQUE>
VariableTerm <IN> Term
( "," VariableTerm <IN> Term )* ( <WITH> Term
)? ")"
|
ForallTerm |
::= |
"(" <FORALL> VariableTerm <IN> Term
( "," VariableTerm <IN> Term )* ( <WITH> Term
)? ")"
|
LetTerm |
::= |
<LET> "(" VariableTerm
"=" Term ( "," VariableTerm
"=" Term )* ")" <IN> Term
<ENDLET>
|
ComprehensionTerm |
::= |
( SetCT | MapCT | SequenceCT | BagCT )
|
SetCT |
::= |
"{" VariableTerm
<IN> Term ( "," VariableTerm
<IN> Term )* ( "|" Term
)? ":" Term "}"
|
MapCT |
::= |
"{" VariableTerm
<IN> Term ( "," VariableTerm
<IN> Term )* ( "|" Term
)? ":" Term "->" Term
"|" "}"
|
SequenceCT |
::= |
"[" VariableTerm
<IN> Term ( "," VariableTerm
<IN> Term )* ( "|" Term
)? ":" Term "]"
|
BagCT |
::= |
"<" VariableTerm
<IN> Term ( "," VariableTerm
<IN> Term )* ( "|" Term
)? ":" Term ">"
|
DomainTerm |
::= |
getDomainByID |
RuleAsTerm |
::= |
"<<" ID_RULE
( "(" getDomainByID ( "," getDomainByID
)* ")" )? ">>"
|
Rule |
::= |
( BasicRule
| TurboRule | UpdateRule
| TurboReturnRule | TermAsRule
| DerivedRule )
|
TermAsRule |
::= |
( FunctionTerm
| VariableTerm )
|
BasicRule |
::= |
( SkipRule
| MacroCallRule | BlockRule
| ConditionalRule | ChooseRule
| ForallRule | LetRule
| ExtendRule )
|
SkipRule |
::= |
<Skip> |
UpdateRule |
::= |
( LocationTerm
| VariableTerm ) ":=" Term |
BlockRule |
::= |
<PAR> Rule
( Rule )+ <ENDPAR>
|
ConditionalRule |
::= |
<IF> Term
<THEN> Rule ( <ELSE> Rule )? <ENDIF>
|
ChooseRule |
::= |
<CHOOSE> VariableTerm
<IN> Term ( "," VariableTerm
<IN> Term )* <WITH> Term <DO> Rule (
<IFNONE> Rule )?
|
ForallRule |
::= |
<FORALL> VariableTerm
<IN> Term ( "," VariableTerm
<IN> Term )* ( <WITH> Term )? <DO> Rule |
LetRule |
::= |
<LET> "(" VariableTerm
"=" Term ( "," VariableTerm
"=" Term )* ")" <IN> Rule
<ENDLET>
|
MacroCallRule |
::= |
ID_RULE "["
( Term ( "," Term )* )?
"]" |
ExtendRule |
::= |
<EXTEND> ID_DOMAIN
<WITH> VariableTerm ( "," VariableTerm )* <DO> Rule |
TurboRule |
::= |
( SeqRule
| IterateRule | TurboCallRule
| TurboLocalStateRule )
|
SeqRule |
::= |
<seq> Rule
( Rule )+ <ENDSEQ>
|
IterateRule |
::= |
<ITERATE> Rule
<ENDITERATE>
|
TurboCallRule |
::= |
ID_RULE "("
( Term ( "," Term )* )?
")" |
TurboReturnRule |
::= |
( LocationTerm
| VariableTerm ) "<-" TurboCallRule |
TurboLocalStateRule |
::= |
LocalFunction
"[" Rule "]" ( LocalFunction
"[" Rule "]" )* Rule |
TryCatchRule |
::= |
<TRY> Rule
<CATCH> ( Term ) ( "," ( Term ) )* Rule |
DerivedRule |
::= |
( BasicDerivedRule
| TurboDerivedRule )
|
BasicDerivedRule |
::= |
CaseRule |
CaseRule |
::= |
<SWITCH> Term
( <CASE> Term ":" Rule
)+ ( <OTHERWISE> Rule )?
<END_SWITCH>
|
TurboDerivedRule |
::= |
( RecursiveWhileRule
| IterativeWhileRule )
|
RecursiveWhileRule |
::= |
<WHILEREC> Term <DO> Rule |
IterativeWhileRule |
::= |
<WHILE> Term
<DO> Rule |
ID_VARIABLE |
::= |
<ID_VARIABLE> |
ID_ENUM |
::= |
<ID_ENUM> |
ID_DOMAIN |
::= |
<ID_DOMAIN> |
ID_RULE |
::= |
<ID_RULE> |
ID_INVARIANT |
::= |
<ID_INVARIANT> |
ID_FUNCTION |
::= |
<ID_FUNCTION> |
ID_AGENT |
::= |
<ID_FUNCTION> |
ID |
::= |
( <ID> ) |
MOD_ID |
::= |
( <MOD_ID> ) |