|
/*
|
|
ANTLR Grammar for OO-Action Systems
|
|
(C) Willibald Krenn, 2009 - 2010
|
|
|
|
|
|
Notes
|
|
~~~~~
|
|
(*) No recursion
|
|
(*) float acutally is fixed-point!
|
|
(*) Named actions can only be "called" within the do-od block
|
|
(*) Methods can be called from within an action and a method.
|
|
Attention: Mutual Recursion not supported!
|
|
|
|
FixMe
|
|
~~~~~
|
|
(*) List-Enum: Length Restriction! (Defaults to 500 for now)
|
|
(*) subseteq missing
|
|
|
|
|
|
|
|
History
|
|
~~~~~~~
|
|
Changes 1.03 to 1.04
|
|
~ Fix bug with set constuctor: set with only one element produced wrong AST (inner element wasn't added correctly).
|
|
|
|
Changes 1.02 to 1.03
|
|
+ option to name objects when they are constructed: new (<class>,"<name>")
|
|
|
|
Changes 1.00 to 1.02
|
|
+ cast operator for objects ( ... as <typename> )
|
|
|
|
Changes 1.00 to 1.01
|
|
+ enum-type with fixed integer values
|
|
|
|
Changes 0.99b to 1.00
|
|
+ constant section added (consts a=4; b=4)
|
|
+ limits of simple types and lists can be const
|
|
+ local vars allowed in methods (... = var... begin...end)
|
|
+ prioritized composition on statement level
|
|
+ skip in do-od block
|
|
+ filter expression in do-od block sequential var statement
|
|
+ fold operator
|
|
|
|
Changes 0.99 to 0.99b
|
|
- disabled sequential composition of action systems (remains in grammar, though out-commented)
|
|
|
|
Changes 0.98 to 0.99
|
|
~ changed QR syntax.
|
|
|
|
Changes 0.97 to 0.98
|
|
~ changed syntax for list and set comprehension
|
|
list comprehension:
|
|
'[' expression '|' 'var' id ':' type (';' id ':' type)* ('&' expression)? ']'
|
|
set comprehension
|
|
'{' expression '|' 'var' id ':' type (';' id ':' type)* ('&' expression)? '}'
|
|
|
|
Usage: defined variables will sweep over value-range. If the latter expression
|
|
(after '&') evaluates to true (hence this expression must return a bool) with
|
|
the current valuation of the defined vars, the values are used to evaluate the
|
|
first expression, which has to return a value of the correct type.
|
|
|
|
Example:
|
|
type
|
|
myint = int [0..300000];
|
|
mytuple = (myint, myint)
|
|
var
|
|
l_tuple : list of mytuple = [nil];
|
|
l_int : list of myint = [nil];
|
|
...
|
|
l_int := [l_tuple[x][0] | var x: myint & x < len l_tuple ]
|
|
|
|
|
|
+ list element access by '[int]' allowed!
|
|
|
|
|
|
Changes 0.96 to 0.97
|
|
+ tuple-type initialization now properly supported
|
|
+ binary operator precedence handling
|
|
+ local variables in named actions
|
|
+ support for (<expression>).<reference> and
|
|
(<expression>).<accessExpression>
|
|
~ conditional expression: End required.
|
|
- remove support for power-operator
|
|
(may be we need to do calculation backwards)
|
|
|
|
Changes 0.95 to 0.96
|
|
~ string literals now ".."
|
|
~ priming of identifier access only supported at the end of the
|
|
expression
|
|
|
|
Changes 0.9 to 0.95
|
|
+ composition of action systems in 'system' block
|
|
~ Produce C# code
|
|
~ Operator Precedence
|
|
~ vars in action composition
|
|
~ forall/extists now with colon instead of in
|
|
|
|
|
|
Earlier changes removed.
|
|
|
|
*/
|
|
|
|
|
|
grammar ooa;
|
|
|
|
options {
|
|
language = CSharp2;
|
|
k = 2;
|
|
// output = AST;
|
|
}
|
|
|
|
|
|
@lexer::namespace { TUG.Mogentes }
|
|
|
|
@lexer::header
|
|
{
|
|
/*
|
|
Ulysses OO-Action System Parser
|
|
|
|
Copyright Willibald Krenn 2009
|
|
|
|
*/
|
|
}
|
|
|
|
@parser::namespace { TUG.Mogentes }
|
|
|
|
@parser::header
|
|
{
|
|
/*
|
|
Ulysses OO-Action System Parser
|
|
|
|
Copyright Willibald Krenn 2009
|
|
|
|
*/
|
|
}
|
|
|
|
ooActionSystems
|
|
: {initializeTopLevelParserState();}
|
|
|
|
(T_CONSTS namedConstList)?
|
|
|
|
T_TYPES
|
|
namedTypeList
|
|
T_SYSTEM
|
|
comp=asTypeComposition[null]
|
|
{fixUpRun(comp);}
|
|
;
|
|
|
|
|
|
|
|
//
|
|
// ------------ named consts ------------
|
|
//
|
|
|
|
namedConstList
|
|
: namedConst (T_SEMICOLON namedConst)*
|
|
;
|
|
|
|
namedConst
|
|
: aName=T_IDENTIFIER
|
|
T_EQUAL
|
|
anExpr=expression
|
|
{addNamedConst(aName,anExpr);}
|
|
;
|
|
|
|
|
|
//
|
|
// ------------ named types ------------
|
|
//
|
|
namedTypeList
|
|
: namedType (T_SEMICOLON namedType)*
|
|
;
|
|
|
|
namedType
|
|
: aName=T_IDENTIFIER
|
|
T_EQUAL
|
|
(
|
|
aType=complexType {createNamedType(aName,aType);}
|
|
| anOoaType=ooActionSystem {createNamedType(aName,anOoaType);}
|
|
)
|
|
|
|
;
|
|
|
|
|
|
asTypeComposition [IdentifierList top]
|
|
returns [IdentifierList prioList]
|
|
: {prioList = new PrioIdentifierList(top);}
|
|
asTypeCompositionParallel[prioList] (T_PRIO asTypeCompositionParallel[prioList] )*
|
|
;
|
|
|
|
asTypeCompositionParallel [IdentifierList top]
|
|
: {IdentifierList parList = new NondetIdentifierList(top);}
|
|
asTypeCompositionSequential[parList] (T_NONDET asTypeCompositionSequential[parList])*
|
|
;
|
|
|
|
asTypeCompositionSequential [IdentifierList top]
|
|
: {IdentifierList seqList = new SeqIdentifierList(top);}
|
|
asTypeCompositionBlockParen[seqList] //(T_SEMICOLON asTypeCompositionBlockParen[seqList])*
|
|
;
|
|
|
|
asTypeCompositionBlockParen [IdentifierList top]
|
|
: T_LPAREN asTypeComposition[top] T_RPAREN
|
|
| aName=T_IDENTIFIER {addToIdentifierList(top,aName);}
|
|
;
|
|
|
|
|
|
//
|
|
// ------------ basic types ------------
|
|
//
|
|
|
|
complexType
|
|
returns [UlyssesType aTypeSymbol]
|
|
@init{
|
|
aTypeSymbol = null;
|
|
alandmark = null;
|
|
}
|
|
: T_LIST T_LSQPAREN numOfElements=(T_INTNUMBER|T_IDENTIFIER) T_RSQPAREN T_OF innertype=complexType
|
|
{aTypeSymbol = createListType(numOfElements,innertype);}
|
|
|
|
// list type with predefined elements (dupes of each element as many as needed) FIXME: Length Restriction!
|
|
| T_LSQPAREN alistelem=T_IDENTIFIER {aTypeSymbol = createListEnumType(alistelem);}
|
|
(T_COMMA otherlistelem=T_IDENTIFIER {addToListEnumType(aTypeSymbol,otherlistelem);})* T_RSQPAREN // set of identifiers..
|
|
|
|
// maps do not really need a length restriction, as simpleType already is restricted..
|
|
| T_MAP (T_LSQPAREN numOfElements=(T_INTNUMBER|T_IDENTIFIER) T_RSQPAREN)? mapfromtype=simpleType T_TO maptotype=complexType
|
|
{aTypeSymbol = createMapType(numOfElements,mapfromtype,maptotype);}
|
|
// quantity space
|
|
| T_QUANTITY T_OF T_LSQPAREN (alandmark=T_IDENTIFIER| alandmark=T_MINUS T_INFTY) {aTypeSymbol = createQrType(alandmark);}
|
|
(T_COMMA (otherlandmark=T_IDENTIFIER|otherlandmark=T_INFTY) {addToQrType(aTypeSymbol,otherlandmark);})* T_RSQPAREN
|
|
// tuple
|
|
| T_LPAREN aType=complexType {aTypeSymbol = createTupleType(aType);}
|
|
(T_COMMA anotherType=complexType {addToTupleType(aTypeSymbol,anotherType);})* T_RPAREN
|
|
|
|
// some simple type (note that this includes identifiers, which may be complex object types..)
|
|
| r=simpleType {aTypeSymbol = r;}
|
|
;
|
|
finally
|
|
{fixupComplexType(aTypeSymbol);}
|
|
|
|
|
|
simpleType
|
|
returns [UlyssesType aTypeSymbol]
|
|
@init{
|
|
aTypeSymbol = null;
|
|
}
|
|
: T_BOOL {aTypeSymbol = createBoolType();}
|
|
|
|
// ints plus subtypes
|
|
| T_INT T_LSQPAREN rangeLow=(T_INTNUMBER|T_INFTY|T_IDENTIFIER) T_RANGETO rangeHigh=(T_INTNUMBER|T_INFTY|T_IDENTIFIER) T_RSQPAREN
|
|
{aTypeSymbol = createIntType(rangeLow,rangeHigh);}
|
|
|
|
// floats plus subtypes
|
|
| T_FLOAT T_LSQPAREN rangeLow=(T_FLOATNUMBER|T_INFTY|T_IDENTIFIER) T_RANGETO rangeHigh=(T_FLOATNUMBER|T_INFTY|T_IDENTIFIER) T_RSQPAREN
|
|
{aTypeSymbol = createFloatType(rangeLow,rangeHigh);}
|
|
|
|
// char
|
|
| T_CHAR {aTypeSymbol = createCharType();}
|
|
|
|
// simple type, domain restricted to the values within the given set. (operators supported: equal, not equal) - may be casted to integer if
|
|
// explicit int values are given
|
|
| T_CBRL aRangeValue=T_IDENTIFIER (T_EQUAL optVal=T_INTNUMBER)? {aTypeSymbol = createEnumType(aRangeValue, optVal);}
|
|
(T_COMMA otherRangeValue=T_IDENTIFIER (T_EQUAL otherOptVal=T_INTNUMBER)? {addToEnumType(aTypeSymbol,otherRangeValue,otherOptVal); otherOptVal=null;})* T_CBRR
|
|
|
|
| aType=T_IDENTIFIER {aTypeSymbol = getNamedType(aType);} // alias could be simple type - otherwise, it's a complex type!!
|
|
;
|
|
finally
|
|
{fixupSimpleType(aTypeSymbol);}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
ooActionSystem
|
|
returns [OoActionSystemType aTypeSymbol]
|
|
@init{
|
|
bool autoCons = false;
|
|
aTypeSymbol = null;
|
|
refinesSystemName = null;
|
|
}
|
|
: (T_AUTOCONS {autoCons = true;})?
|
|
T_SYSTEM (T_LPAREN refinesSystemName=T_IDENTIFIER T_RPAREN)?
|
|
{aTypeSymbol = createOoaType(refinesSystemName,autoCons);}
|
|
'|['
|
|
(T_VAR attrList)?
|
|
(T_METHODS methodList)?
|
|
(T_ACTIONS namedActionList)?
|
|
(T_DO (bl=actionBlock[null] {addActionBlock(aTypeSymbol,bl);})? T_OD)?
|
|
']|'
|
|
;
|
|
finally
|
|
{fixupOoaType(aTypeSymbol);}
|
|
|
|
|
|
|
|
|
|
//
|
|
// ------------ variables (objects and simple types) ------------
|
|
//
|
|
attrList
|
|
: {BeginParsingAttributes();}
|
|
attr (T_SEMICOLON attr)*
|
|
;
|
|
finally {
|
|
EndParsingAttributes();
|
|
}
|
|
|
|
attr
|
|
@init{
|
|
bool isStatic = false;
|
|
bool isCtr = false;
|
|
bool isObs = false;
|
|
|
|
}
|
|
: (T_STATIC {isStatic = true;})? (T_OBS {isObs = true;} | T_CTRL {isCtr = true;})?
|
|
varname=T_IDENTIFIER T_COLON aType=complexType (T_EQUAL anExpr=expression)?
|
|
{createAttribute(varname, isStatic, isObs, isCtr, aType, anExpr);}
|
|
;
|
|
|
|
//
|
|
// ------------ methods ------------
|
|
//
|
|
methodList
|
|
: method (T_SEMICOLON method)*
|
|
;
|
|
|
|
method
|
|
@init {
|
|
FunctionIdentifier newMethod = null;
|
|
}
|
|
: mname=T_IDENTIFIER {newMethod = createMethodSymbol(mname);}
|
|
(T_LPAREN methodParameterList[newMethod] T_RPAREN)?
|
|
(T_COLON rt=complexType {setMethodReturnType(newMethod,rt);})? // actions can not have a return type!!
|
|
T_EQUAL
|
|
(T_VAR localActionVars[newMethod] 'begin')?
|
|
statements=actionBody[null] {addMethodBody(newMethod,statements);}
|
|
T_END
|
|
;
|
|
finally
|
|
{popResolveStack(newMethod);}
|
|
|
|
methodParameterList[FunctionIdentifier newMethod]
|
|
: paramName=T_IDENTIFIER T_COLON atype=complexType {addMethodParameter(newMethod,paramName,atype);}
|
|
(T_COMMA otherparam=T_IDENTIFIER T_COLON othertype=complexType
|
|
{addMethodParameter(newMethod,otherparam,othertype);} )*
|
|
;
|
|
|
|
|
|
//
|
|
// ------------ named, anonymous actions ------------
|
|
//
|
|
|
|
namedActionList
|
|
: namedAction (T_SEMICOLON namedAction)*
|
|
;
|
|
|
|
namedAction
|
|
@init {
|
|
FunctionTypeEnum actionType;
|
|
FunctionIdentifier newAction = null;
|
|
}
|
|
: T_CONT cactionname=T_IDENTIFIER {newAction = createNamedContinuousAction(cactionname, FunctionTypeEnum.Continuous);}
|
|
(T_LPAREN methodParameterList[newAction] T_RPAREN)?
|
|
T_EQUAL constraints=continuousActionBody {addContinuousActionBody(newAction,constraints);}
|
|
|
|
| {actionType = FunctionTypeEnum.Internal;}
|
|
(T_CTRL {actionType = FunctionTypeEnum.Controllable;}| T_OBS {actionType = FunctionTypeEnum.Observable;}| )
|
|
actionname=T_IDENTIFIER {newAction = createNamedAction(actionname,actionType);}
|
|
(T_LPAREN methodParameterList[newAction] T_RPAREN)?
|
|
T_EQUAL
|
|
(T_VAR localActionVars[newAction] )?
|
|
body=discreteActionBody
|
|
{addActionBody(newAction,body);}
|
|
;
|
|
finally
|
|
{popResolveStack(newAction);}
|
|
|
|
|
|
localActionVars[FunctionIdentifier newMethod]
|
|
: // a named, discrete action may have local variables.
|
|
id1=T_IDENTIFIER T_COLON t1=complexType {addLocalVariableToNamedAction(newMethod,id1,t1);}
|
|
(T_SEMICOLON id2=T_IDENTIFIER T_COLON t2=complexType
|
|
{addLocalVariableToNamedAction(newMethod,id2,t2);} )*
|
|
;
|
|
|
|
|
|
|
|
anonymousAction
|
|
returns [GuardedCommand result]
|
|
: a=continuousActionBody {result = a;}
|
|
| b=discreteActionBody {result = b;}
|
|
;
|
|
|
|
continuousActionBody
|
|
returns [GuardedCommand result]
|
|
@init {
|
|
result = null;
|
|
}
|
|
: T_CONT T_REQUIRES expr=expression T_COLON
|
|
bdy=qualConstraintList
|
|
T_END
|
|
{result = createGuardedCommandStatement(expr,bdy,true);}
|
|
;
|
|
|
|
qualConstraintList
|
|
returns [Block result]
|
|
@init{
|
|
result = createSeqBlock(null);
|
|
pushBlockToResolveStack(result);
|
|
}
|
|
: stmt=qualConstraint {addToBlockList(result,stmt);}
|
|
(T_COMMA ostmt=qualConstraint {addToBlockList(result,ostmt);})*
|
|
;
|
|
finally
|
|
{popBlockFromResolveStack(result);}
|
|
|
|
|
|
|
|
qualConstraint
|
|
returns [QualitativeConstraintStatement result]
|
|
: id1=T_IDENTIFIER T_EQUAL
|
|
( T_DERIV derivid=T_IDENTIFIER
|
|
{result = createQualDerivConstraintStatement(id1,derivid);}
|
|
|
|
|
|
|
id2=T_IDENTIFIER
|
|
(
|
|
( op=T_SUM
|
|
| op=T_DIFF
|
|
| op=T_PROD
|
|
)
|
|
id3=T_IDENTIFIER
|
|
{result = createQualArithConstraintStatement(id1,id2,id3,op);}
|
|
|
|
|
{result = createQualEqualConstraintStatement(id1,id2);}
|
|
)
|
|
)
|
|
;
|
|
|
|
|
|
|
|
|
|
discreteActionBody
|
|
returns [GuardedCommand result]
|
|
@init{
|
|
result = null;
|
|
}
|
|
:
|
|
T_REQUIRES expr=expression T_COLON
|
|
bdy=actionBody[null]
|
|
T_END
|
|
{result = createGuardedCommandStatement(expr,bdy);}
|
|
;
|
|
|
|
|
|
//
|
|
// ------------ do-od block ------------
|
|
//
|
|
|
|
actionBlock [Block top]
|
|
returns [Block prioList]
|
|
: {prioList = createPrioBlock(top);}
|
|
actionBlockParallel[prioList] (T_PRIO actionBlockParallel[prioList])*
|
|
;
|
|
|
|
actionBlockParallel [Block top]
|
|
: {Block parList = createNondetBlock(top);}
|
|
actionBlockSequential[parList] (T_NONDET actionBlockSequential[parList])*
|
|
;
|
|
|
|
// atomic sequential composition of actions
|
|
actionBlockSequential [Block top]
|
|
@init {
|
|
Block seqList = createSeqBlock(top);
|
|
pushBlockToResolveStack(seqList);
|
|
}
|
|
: (T_VAR syms=blockvarlist[seqList] ('&' sexpr=expression {addSeqBlockExpression(seqList,sexpr);} )? T_COLON )?
|
|
actionBlockParen[seqList] (T_SEMICOLON actionBlockParen[seqList])*
|
|
;
|
|
finally
|
|
{popBlockFromResolveStack(seqList);}
|
|
|
|
actionBlockParen [Block top]
|
|
: T_LPAREN actionBlock[top] T_RPAREN
|
|
| anonymousOrNamedAction[top]
|
|
;
|
|
|
|
anonymousOrNamedAction [Block top]
|
|
: gcmd=anonymousAction {addToBlockList(top,gcmd);}
|
|
| aname=T_IDENTIFIER
|
|
(T_LPAREN m_params=methodCallParams T_RPAREN)?
|
|
(amap=(T_FOLDLR|T_FOLDRL) '(' amapexpr=expression ')')?
|
|
{addNamedActionCallToBlockList(top,aname,m_params,amap,amapexpr);}
|
|
| T_SKIP {addSkipStatementToBlockList(top);}
|
|
;
|
|
|
|
|
|
blockvarlist [Block seqList]
|
|
: blockvar[seqList] (T_SEMICOLON blockvar[seqList] )*
|
|
;
|
|
|
|
blockvar [Block seqList]
|
|
: varname=T_IDENTIFIER T_COLON aType=complexType
|
|
{addBlockVariable(seqList,varname,aType);}
|
|
;
|
|
|
|
|
|
|
|
//
|
|
// ------------ action body of non-continuous actions ------------
|
|
//
|
|
|
|
actionBody[Block top]
|
|
returns [Block result]
|
|
: {result = createPrioBlock(top);}
|
|
actionBodyParallel[result] (T_PRIO actionBodyParallel[result])?
|
|
;
|
|
|
|
actionBodyParallel[Block top]
|
|
returns [Block result]
|
|
: {result = createNondetBlock(top);}
|
|
actionBodySequential[result]
|
|
(T_NONDET olst=actionBodySequential[result])*
|
|
;
|
|
|
|
// seq binds stronger than nondet, i.e. a;b;cd;e is read as (a;b;c)[](d;e)
|
|
actionBodySequential[Block top]
|
|
returns [Block result]
|
|
: {result = createSeqBlock(top);}
|
|
actionBodyParen[result] (T_SEMICOLON actionBodyParen[result])*
|
|
;
|
|
|
|
actionBodyParen [Block top]
|
|
: T_LPAREN actionBody[top] T_RPAREN
|
|
| stmt=statement
|
|
{addToStatementList(top,stmt);}
|
|
;
|
|
|
|
|
|
statement
|
|
returns [Statement result]
|
|
@init {
|
|
bool popFromResolveStack = false;
|
|
result = null;
|
|
}
|
|
: T_ABORT {result = createAbortStatement();}
|
|
| T_SKIP {result = createSkipStatement();}
|
|
| T_KILL T_LPAREN aname=(T_IDENTIFIER | T_SELF) T_RPAREN {result = createKillStatement(aname);}
|
|
| gc=discreteActionBody {result = gc;}
|
|
| aqname=reference
|
|
( // single assignment
|
|
T_ASSIGNMENT aexp=expression {result = createSingleAssignmentStatement(aqname,aexp);}
|
|
(T_WITH ndexp=expression {addConstraintToAssignment(result,ndexp);})? // nondet assignment
|
|
|
|
// multi assignment
|
|
| {result = createMultipleAssignmentStatementLHS(aqname);}
|
|
(T_COMMA malhs=reference {addMultipleAssignmentStatementLHS(result,malhs);})+
|
|
T_ASSIGNMENT
|
|
{pushAssignmentOnResolveStack(result); popFromResolveStack = true;}
|
|
mexp=expression
|
|
{addMutlipleAssignmentStatementRHS(result,mexp);}
|
|
(T_COMMA mexp2=expression {addMutlipleAssignmentStatementRHS(result,mexp2);})+
|
|
(T_WITH ndex2=expression {addConstraintToAssignment(result,ndex2);})? // nondet assignment
|
|
|
|
// just a call of a method.
|
|
| {result = createCallStatement(aqname);}
|
|
)
|
|
;
|
|
finally {
|
|
if (popFromResolveStack == true)
|
|
popAssignmentOffResolveStack(result);
|
|
}
|
|
|
|
//
|
|
// ------------ expression ------------
|
|
//
|
|
expression
|
|
returns [Expression expr]
|
|
@init{
|
|
System.Collections.Generic.List<BinaryOperator> operators = new System.Collections.Generic.List<BinaryOperator>();
|
|
System.Collections.Generic.List<Expression> expressions = new System.Collections.Generic.List<Expression>();
|
|
}
|
|
: left=atomExpression
|
|
{expressions.Add(left);}
|
|
( op=binoperator
|
|
right=atomExpression
|
|
{
|
|
operators.Add(op);
|
|
expressions.Add(right);
|
|
}
|
|
)*
|
|
{expr = createPrecedenceTree(expressions,operators);}
|
|
;
|
|
|
|
|
|
binoperator
|
|
returns [BinaryOperator binop]
|
|
: T_BIIMPLIES
|
|
{binop = createBinaryOperator(ExpressionKind.biimplies);}
|
|
| T_GREATER
|
|
{binop = createBinaryOperator(ExpressionKind.greater);}
|
|
| T_GREATEREQUAL
|
|
{binop = createBinaryOperator(ExpressionKind.greaterequal);}
|
|
| T_LESS
|
|
{binop = createBinaryOperator(ExpressionKind.less);}
|
|
| T_LESSEQUAL
|
|
{binop = createBinaryOperator(ExpressionKind.lessequal);}
|
|
| T_EQUAL // bool, numeric, char, lists, maps
|
|
{binop = createBinaryOperator(ExpressionKind.equal);}
|
|
| T_NOTEQUAL // bool, numeric, char, lists, maps
|
|
{binop = createBinaryOperator(ExpressionKind.notequal);}
|
|
| T_IMPLIES
|
|
{binop = createBinaryOperator(ExpressionKind.implies);}
|
|
| T_MINUS
|
|
{binop = createBinaryOperator(ExpressionKind.minus);}
|
|
| T_SUM
|
|
{binop = createBinaryOperator(ExpressionKind.sum);}
|
|
| T_IN T_SET? // A * list of A -> bool
|
|
{binop = createBinaryOperator(ExpressionKind.elemin);}
|
|
| T_NOT T_IN T_SET? // A * list of A -> bool
|
|
{binop = createBinaryOperator(ExpressionKind.notelemin);}
|
|
| T_SUBSET // list of A * list of A -> bool (does not respect dupes)
|
|
{binop = createBinaryOperator(ExpressionKind.subset);}
|
|
| T_OR
|
|
{binop = createBinaryOperator(ExpressionKind.or);}
|
|
| T_DIV
|
|
{binop = createBinaryOperator(ExpressionKind.div);}
|
|
| T_PROD
|
|
{binop = createBinaryOperator(ExpressionKind.prod);}
|
|
| T_IDIV
|
|
{binop = createBinaryOperator(ExpressionKind.idiv);}
|
|
| T_MOD
|
|
{binop = createBinaryOperator(ExpressionKind.mod);}
|
|
| T_UNION // list of A * list of A -> list of A (does not respect dupes)
|
|
{binop = createBinaryOperator(ExpressionKind.union);}
|
|
| T_DIFF // list of A * list of A -> list of A (does not respect dupes)
|
|
{binop = createBinaryOperator(ExpressionKind.diff);}
|
|
| T_INTER // list of A * list of A -> list of A (does not respect dupes)
|
|
{binop = createBinaryOperator(ExpressionKind.inter);}
|
|
| T_AND
|
|
{binop = createBinaryOperator(ExpressionKind.and);}
|
|
| T_POW
|
|
{binop = createBinaryOperator(ExpressionKind.pow);}
|
|
| T_CONC // list of A * list of A -> list of A
|
|
{binop = createBinaryOperator(ExpressionKind.conc);}
|
|
| T_DOMRESBY // list of A * map A to B -> map A to B
|
|
{binop = createBinaryOperator(ExpressionKind.domresby);}
|
|
| T_DOMRESTO // list of A * map A to B -> map A to B
|
|
{binop = createBinaryOperator(ExpressionKind.domresto);}
|
|
| T_RNGRESBY // map A to B * list of B -> map A to B
|
|
{binop = createBinaryOperator(ExpressionKind.rngresby);}
|
|
| T_RNGRESTO // map A to B * list of B -> map A to B
|
|
{binop = createBinaryOperator(ExpressionKind.rngresto);}
|
|
| T_MUNION // map A to B * map A to B -> map A to B
|
|
{binop = createBinaryOperator(ExpressionKind.munion);}
|
|
| T_SEQMOD_MAPOVERRIDE // list of A * map int to A -> list of A or
|
|
// map A to B * map A to B -> map A to B
|
|
{binop = createBinaryOperator(ExpressionKind.seqmod_mapoverride);}
|
|
;
|
|
|
|
|
|
atomExpression
|
|
returns [Expression expr]
|
|
@init {
|
|
expr = null;
|
|
}
|
|
: (unexpr=op_un? (
|
|
e=identifierExpression
|
|
| e=qvalExpression
|
|
| e=constant
|
|
| e=initializedComplexType
|
|
| e=quantifierExpression
|
|
| T_LPAREN e=expression T_RPAREN
|
|
(
|
|
(T_POINT
|
|
idn=T_IDENTIFIER
|
|
{e = addIdentifierAccessExpression(e,idn);})+
|
|
(res=accessExpression[e] {e=res;})?
|
|
|
|
|
e=accessExpression[e]
|
|
)?
|
|
) ('as' cid=T_IDENTIFIER {e=addCastExpression(e,cid);})?
|
|
{expr = addUnaryExpression(unexpr,e);}
|
|
)
|
|
| ie=T_IF ce=expression T_THEN te=expression T_ELSE ee=expression T_END
|
|
{expr = createConditionalExpression(ce,te,ee,ie);}
|
|
;
|
|
|
|
|
|
quantifierExpression
|
|
returns [Quantifier result]
|
|
@init {
|
|
result = null;
|
|
}
|
|
: t=(T_FORALL | T_EXISTS)
|
|
{result = createQuantifierExpression(t);}
|
|
(id=T_IDENTIFIER (T_COLON id_type=simpleType {addBoundVarToQuantifierExpression(result,id,id_type);})
|
|
(T_COMMA id2=T_IDENTIFIER (T_COLON id_type2=simpleType){addBoundVarToQuantifierExpression(result,id2,id_type2);})*)
|
|
T_COLON T_LPAREN e=expression T_RPAREN
|
|
{addExpressionToQuantifier(result,e);}
|
|
;
|
|
finally
|
|
{removeBoundVarsFromResolveStack(result);}
|
|
|
|
constant
|
|
returns [LeafExpression result]
|
|
@init {
|
|
result = null;
|
|
}
|
|
: T_TRUE {result = createBoolConstant(true);}
|
|
| T_FALSE {result = createBoolConstant(false);}
|
|
| T_NIL {result = createNullPointerConstant();}
|
|
| T_SELF {result = createSelfPointer();}
|
|
| t_fl=T_FLOATNUMBER {result = createFloatConstant(t_fl);}
|
|
| t_in=T_INTNUMBER {result = createIntConstant(t_in);}
|
|
| t_l=T_STRINGLITERAL {result = createStringConstant(t_l);}
|
|
;
|
|
|
|
initializedComplexType
|
|
returns [Expression result]
|
|
@init {
|
|
result = null;
|
|
}
|
|
: res=initializedListType {result = res;}
|
|
| res=initializedSetType {result = res;}
|
|
| T_NEW T_LPAREN anid=T_IDENTIFIER
|
|
(
|
|
T_COMMA aname=T_STRINGLITERAL T_RPAREN {result = createNamedObject(anid, aname);}
|
|
| T_RPAREN {result = createObject(anid);} // constructor call..
|
|
)
|
|
;
|
|
|
|
initializedListType
|
|
returns [ListConstructor result]
|
|
@init {
|
|
result = createInitializedList();
|
|
pushListVarsOnResolveStack(result); // need this here for list comprehension
|
|
}
|
|
: T_LSQPAREN e=expression {addListElement(result,e);} (
|
|
(T_COMMA e2=expression {addListElement(result,e2);})+
|
|
| listComprehension[result]
|
|
)? T_RSQPAREN
|
|
;
|
|
finally
|
|
{popListVarsFromResolveStack(result);}
|
|
|
|
listComprehension [ListConstructor result]
|
|
@init{
|
|
result.SetHasComprehension(true);
|
|
}
|
|
:
|
|
T_BAR T_VAR
|
|
id=T_IDENTIFIER T_COLON t1=complexType {addListComprVar(result,id,t1);}
|
|
(T_SEMICOLON id2=T_IDENTIFIER t2=complexType {addListComprVar(result,id2,t2);})*
|
|
('&'
|
|
e=expression {addListComprExpr(result,e);})?
|
|
;
|
|
|
|
initializedSetType
|
|
returns[Expression result]
|
|
@init {
|
|
result = null;
|
|
}
|
|
: T_CBRL T_MAPS T_CBRR {result = createEmptyMap();} // empty map
|
|
| res=initializedSet {result = res;}
|
|
;
|
|
|
|
initializedSet
|
|
returns [Expression result]
|
|
@init {
|
|
SetConstructor theset = createSet();
|
|
pushSetVarsOnResolveStack(theset); // need this here for set comprehension
|
|
result = theset;
|
|
}
|
|
: T_CBRL e1=expression
|
|
( // set constructor; empty set: {nil}
|
|
{addToSet(result,e1);}
|
|
(T_COMMA e2=expression {addToSet(result,e2);})* // set constructor for sets > 1 elem
|
|
| m=map[result, e1] {result = m;} // we have a set in the resolution stack, but this should be fine (no syms)
|
|
| {addToSet(result,e1);} setComprehension[(SetConstructor)result] // set comprehension
|
|
) T_CBRR
|
|
;
|
|
finally
|
|
{popSetVarsFromResolveStack(theset);}
|
|
|
|
|
|
map[Expression _map, Expression e1]
|
|
returns [Expression result]
|
|
@init {
|
|
result = null;
|
|
}
|
|
: am=T_MAPS e2=expression {result = createMap(e1,e2,am);} (T_COMMA e3=expression T_MAPS e4=expression {addToMap(result,e3,e4);})*
|
|
;
|
|
|
|
setComprehension[SetConstructor _set]
|
|
@init {
|
|
_set.SetHasComprehension(true);
|
|
}
|
|
: T_BAR T_VAR (id1=T_IDENTIFIER T_COLON t1=complexType
|
|
{ addSetComprVar(_set, id1, t1); }
|
|
T_SEMICOLON id2=T_IDENTIFIER T_COLON t2=complexType
|
|
{ addSetComprVar(_set, id2, t2); })*
|
|
('&'
|
|
epx=expression
|
|
{ addSetComprExpr(_set,epx); })?
|
|
;
|
|
|
|
|
|
qvalExpression
|
|
returns [QValConstructor result]
|
|
@init {
|
|
bool minus = false;
|
|
result = null;
|
|
}
|
|
: // constructor for qualitative values
|
|
aval='qval' T_LPAREN
|
|
{result = createQualitativeValue(aval);}
|
|
(
|
|
T_NIL
|
|
{setQualitativeValueDontCare(result);}
|
|
|
|
|
( expr=qualifiedIdentifier
|
|
{setQualitativeValueLandmark(result,expr);}
|
|
|
|
|
('-' {minus = true;})? T_INFTY
|
|
{setQualitativeValueInfinity(result,minus);}
|
|
)
|
|
(T_RANGETO
|
|
( expr2=qualifiedIdentifier
|
|
{setQualitativeValueRange(result,expr2);}
|
|
|
|
|
T_INFTY
|
|
{setQualitativeValueRangeInfinity(result,false);}
|
|
) )?
|
|
)
|
|
T_COMMA
|
|
(
|
|
T_NIL
|
|
{setQualitativeDerivDontCare(result);}
|
|
|
|
|
( 'steady'
|
|
{setQualitativeDerivSteady(result);}
|
|
| 'inc'
|
|
{setQualitativeDerivInc(result);}
|
|
| 'dec'
|
|
{setQualitativeDerivDec(result);}
|
|
)
|
|
)
|
|
T_RPAREN
|
|
;
|
|
|
|
|
|
identifierExpression
|
|
returns [Expression result]
|
|
: // if next token is a tuple-type then create an initialized tuple!
|
|
{isTuple(input.LT(1).Text)}?
|
|
aName=T_IDENTIFIER T_LPAREN m_params=methodCallParams T_RPAREN
|
|
{result = createInitializedTuple(aName,m_params);}
|
|
| // is some sort of reference
|
|
res=reference
|
|
{result = res;}
|
|
;
|
|
|
|
|
|
reference
|
|
returns [Expression result]
|
|
@init {
|
|
result = null;
|
|
init = null;
|
|
}
|
|
: {!isTuple(input.LT(1).Text)}? // check that the next token is not a reference to a tuple-type
|
|
aName=qualifiedIdentifier {result = aName;}
|
|
( output=accessExpression[result] {result = output;}
|
|
// call expression
|
|
| // variable access or method call that takes no params? (do we allow for that? - answer: no!)
|
|
)
|
|
( pr=T_PRIMED {setIdentifierExpressionPrimed(ref result,pr);}
|
|
|
|
|
('::' T_LPAREN init=expression T_RPAREN)? afold=(T_FOLDLR|T_FOLDRL) T_LPAREN anexpr=expression T_RPAREN
|
|
{result = createFoldExpression(result,afold,init,anexpr);}
|
|
)?
|
|
;
|
|
|
|
accessExpression[Expression subexpr]
|
|
returns [Expression result]
|
|
@init{
|
|
UnaryOperator newExpr = null;
|
|
result = subexpr;
|
|
}
|
|
:
|
|
( tcall=T_LSQPAREN ac=expression T_RSQPAREN // access tuples, maps
|
|
{ result = createTupleMapAccessExpression(result,ac,tcall); }
|
|
| bcall=T_LPAREN m_params=methodCallParams T_RPAREN // access method
|
|
{ result = createMethodAccessExpression(result,m_params,bcall); }
|
|
)+
|
|
( // a[1].c.e()...
|
|
(T_POINT
|
|
idn=T_IDENTIFIER
|
|
{result = addIdentifierAccessExpression(result,idn);})+
|
|
(res=accessExpression[result] {result=res;})?
|
|
)?
|
|
;
|
|
|
|
qualifiedIdentifier
|
|
returns [Expression top]
|
|
@init {
|
|
IdentifierExpression selfexpr = null;
|
|
top = null;
|
|
}
|
|
:
|
|
(self=T_SELF T_POINT {selfexpr = createSelfIdentifierExpression(self);})?
|
|
idb=T_IDENTIFIER {top = createIdentifierAccessExpression(selfexpr,idb);}
|
|
(T_POINT idd=T_IDENTIFIER {top = addIdentifierAccessExpression(top,idd);})*
|
|
;
|
|
|
|
|
|
methodCallParams
|
|
returns [System.Collections.Generic.List<Expression> result]
|
|
@init {
|
|
result = new System.Collections.Generic.List<Expression>();
|
|
}
|
|
: (expa=expression {result.Add(expa);} (T_COMMA expb=expression {result.Add(expb);})*)?
|
|
;
|
|
|
|
|
|
|
|
//
|
|
// ------------ unary Operators ------------
|
|
//
|
|
|
|
|
|
op_un
|
|
returns [UnaryOperator expr]
|
|
@init {
|
|
expr = null;
|
|
}
|
|
: r=op_un_set_list {expr = r;}
|
|
| r2=op_un_map {expr = r2;}
|
|
| T_MINUS {expr = createUnaryOperator(ExpressionKind.unminus);}
|
|
| T_NOT {expr = createUnaryOperator(ExpressionKind.not);}
|
|
| T_ABS {expr = createUnaryOperator(ExpressionKind.abs);}
|
|
;
|
|
|
|
|
|
op_un_set_list
|
|
returns [UnaryOperator expr]
|
|
@init {
|
|
expr = null;
|
|
}
|
|
: T_CARD // list of A -> int (does not respect dupes, i.e. dupes do not count)
|
|
{expr = createUnaryOperator(ExpressionKind.card);}
|
|
| T_DCONC // list of list of A -> list of A
|
|
{expr = createUnaryOperator(ExpressionKind.dconc);}
|
|
| T_DINTER // list of list of A -> list of A (intersection, does not respect dupes)
|
|
{expr = createUnaryOperator(ExpressionKind.dinter);}
|
|
| T_DUNION // list of list of A -> list of A (union, does not respect dupes)
|
|
{expr = createUnaryOperator(ExpressionKind.dunion);}
|
|
| T_ELEMS // list of A -> list of A (does not respect dupes)
|
|
{expr = createUnaryOperator(ExpressionKind.elems);}
|
|
| T_HEAD // list of A -> A
|
|
{expr = createUnaryOperator(ExpressionKind.head);}
|
|
| T_INDS // list of A -> list of int
|
|
{expr = createUnaryOperator(ExpressionKind.inds);}
|
|
| T_LEN // list of A -> int (dupes count)
|
|
{expr = createUnaryOperator(ExpressionKind.len);}
|
|
| T_TAIL // list of A -> list of A
|
|
{expr = createUnaryOperator(ExpressionKind.tail);}
|
|
;
|
|
|
|
|
|
op_un_map
|
|
returns [UnaryOperator expr]
|
|
@init {
|
|
expr = null;
|
|
}
|
|
: T_DOM // map A to B -> list of A
|
|
{expr = createUnaryOperator(ExpressionKind.dom);}
|
|
| T_RNG // map A to B -> list of B
|
|
{expr = createUnaryOperator(ExpressionKind.range);}
|
|
| T_MERGE // list of map A to B -> map A to B
|
|
{expr = createUnaryOperator(ExpressionKind.merge);}
|
|
;
|
|
|
|
|
|
|
|
|
|
|
|
|
|
//
|
|
// ============== LEXER =================
|
|
//
|
|
T_WS : (' '|'\r'|'\t'|'\u000C'|'\n') {$channel=HIDDEN;}
|
|
;
|
|
|
|
T_COMMENT
|
|
: '/*' .* '*/' {$channel=HIDDEN;}
|
|
;
|
|
|
|
LINE_COMMENT
|
|
: '#' ~('\n'|'\r')* '\r'? '\n' {$channel=HIDDEN;}
|
|
;
|
|
|
|
T_PRIMED
|
|
: '\'';
|
|
|
|
T_STRINGLITERAL
|
|
: '"'
|
|
(
|
|
( '"' '"' )=> '"'
|
|
| ~'"'
|
|
)*
|
|
'"'
|
|
;
|
|
|
|
|
|
T_ABORT : 'abort';
|
|
T_ACTIONS
|
|
: 'actions';
|
|
T_ASSIGNMENT
|
|
: ':=';
|
|
T_AUTOCONS: 'autocons';
|
|
T_BAR : '|';
|
|
T_BOOL : 'bool';
|
|
T_CBRL : '{';
|
|
T_CBRR : '}';
|
|
T_COLON : ':';
|
|
T_COMMA : ',';
|
|
T_CONT : 'qual';
|
|
T_CHAR : 'char';
|
|
T_CTRL : 'ctr';
|
|
T_SYSTEM
|
|
: 'system';
|
|
T_DO : 'do';
|
|
T_ELSE : 'else';
|
|
T_END : 'end';
|
|
T_EQUAL : '=';
|
|
T_EXISTS: 'exists';
|
|
T_FLOAT : 'float';
|
|
T_FORALL: 'forall';
|
|
T_FALSE : 'false';
|
|
T_IF : 'if';
|
|
T_IN : 'in';
|
|
T_INT : 'int';
|
|
T_KILL : 'kill';
|
|
T_LIST : 'list';
|
|
T_LPAREN: '(';
|
|
T_LSQPAREN: '[';
|
|
T_MAP : 'map';
|
|
T_MAPS : '->';
|
|
T_METHODS
|
|
: 'methods';
|
|
T_NEW : 'new';
|
|
T_NIL : 'nil';
|
|
T_NONDET: '[]';
|
|
T_OBS : 'obs';
|
|
T_OD : 'od';
|
|
T_OF : 'of';
|
|
T_PRIO : '//';
|
|
T_REQUIRES
|
|
: 'requires';
|
|
T_RPAREN: ')';
|
|
T_RSQPAREN: ']';
|
|
T_QUANTITY
|
|
: 'qspace';
|
|
T_SELF : 'self';
|
|
T_SET : 'set';
|
|
T_SEMICOLON
|
|
: ';';
|
|
T_STATIC: 'static';
|
|
T_SKIP : 'skip';
|
|
T_THEN : 'then';
|
|
T_TRUE : 'true';
|
|
T_TO : 'to';
|
|
T_TYPES : 'types';
|
|
T_VAR : 'var';
|
|
T_WITH : 'with'; // for nondet assignment
|
|
|
|
|
|
//T_ACTION: 'action';
|
|
|
|
//BOOL
|
|
T_AND : 'and';
|
|
T_BIIMPLIES
|
|
: '<=>';
|
|
T_IMPLIES
|
|
: '=>'; //VDM-Style
|
|
T_NOT : 'not'; //VDM-Style
|
|
T_NOTEQUAL: '<>'; //VDM-Style
|
|
T_OR : 'or';
|
|
|
|
//Numeric (equal, not equal same as in BOOL)
|
|
T_ABS : 'abs';
|
|
T_DIV : '/';
|
|
T_GREATER
|
|
: '>';
|
|
T_GREATEREQUAL
|
|
: '>=';
|
|
T_IDIV : 'div';
|
|
T_LESS : '<';
|
|
T_LESSEQUAL
|
|
: '<='; //VDM-Style
|
|
T_MOD : 'mod'; //VDM-Style
|
|
T_POW : '**';
|
|
T_PROD : '*';
|
|
T_DERIV : 'dt';
|
|
|
|
// set/list
|
|
T_CARD : 'card';
|
|
T_CONC : '^';
|
|
T_DCONC : 'conc';
|
|
T_DIFF : '\\';
|
|
T_DINTER: 'dinter';
|
|
T_DUNION: 'dunion';
|
|
T_ELEMS : 'elems';
|
|
T_HEAD : 'hd';
|
|
T_INDS : 'inds';
|
|
T_INTER : 'inter';
|
|
T_LEN : 'len'; // differs from T_CARD, as card does not count dupes..
|
|
T_SEQMOD_MAPOVERRIDE
|
|
: '++';
|
|
T_SUBSET: 'subset';
|
|
T_TAIL : 'tl';
|
|
T_UNION : 'union';
|
|
T_FOLDLR
|
|
: ':>:';
|
|
T_FOLDRL
|
|
: ':<:';
|
|
|
|
|
|
// maps
|
|
T_DOM : 'dom';
|
|
T_DOMRESBY
|
|
: '<-:';
|
|
T_DOMRESTO
|
|
: '<:';
|
|
T_RNG : 'rng';
|
|
T_RNGRESBY
|
|
: ':->';
|
|
T_RNGRESTO
|
|
: ':>';
|
|
T_MERGE : 'merge';
|
|
T_MUNION: 'munion';
|
|
|
|
T_CONSTS: 'consts';
|
|
|
|
// numbers
|
|
|
|
T_INFTY : (T_MINUS|T_SUM)? 'inf'
|
|
;
|
|
|
|
|
|
// INTNUMBER, FLOATNUMBER, RANGETO, T_MINUS, T_PLUS are set within
|
|
// FLOAT_OR_INT_OR_RANGE
|
|
fragment T_INTNUMBER
|
|
: ;
|
|
fragment T_FLOATNUMBER
|
|
: ;
|
|
fragment T_RANGETO
|
|
: ;
|
|
|
|
FLOAT_OR_INT_OR_RANGE
|
|
: (T_MINUS|T_SUM)? T_DIGIT+
|
|
( // at this stage, we could face an int, int..int (=range), int.exp (=float), int.exp..int.exp (=float range) etc..
|
|
(T_POINT T_POINT) => {$type=T_INTNUMBER;}
|
|
| (T_POINT T_DIGIT) => T_POINT T_DIGIT+ (('e'|'E') (T_MINUS|T_SUM)? T_DIGIT+)? {$type=T_FLOATNUMBER;}
|
|
| {$type=T_INTNUMBER;}
|
|
)
|
|
| T_POINT
|
|
( // could be point or range..
|
|
T_POINT {$type=T_RANGETO;}
|
|
| {$type=T_POINT;}
|
|
)
|
|
| T_MINUS {$type=T_MINUS;}
|
|
| T_SUM {$type=T_SUM;}
|
|
;
|
|
|
|
|
|
|
|
fragment T_MINUS: '-';
|
|
fragment T_SUM : '+';
|
|
fragment T_POINT: '.';
|
|
|
|
|
|
|
|
// identifiers
|
|
T_IDENTIFIER
|
|
: T_LETTER (T_LETTER|T_DIGIT)*
|
|
;
|
|
|
|
//T_PRIMEDIDENTIFIER
|
|
// : T_IDENTIFIER '\'';
|
|
|
|
fragment
|
|
T_LETTER
|
|
: '$'
|
|
| 'A'..'Z'
|
|
| 'a'..'z'
|
|
| '_'
|
|
;
|
|
|
|
fragment
|
|
T_DIGIT: '0'..'9';
|
|
|