machine

MACHINEGRAPHidentifier{ action code }LBRACEglobalVariableDecl{ action code }state{ action code }trans{ action code }invariantExpression{ action code }goal{ action code }RBRACEEOF

state

stateModifier{ action code }{ action code }STATENODEidentifier{ action code }LBRACElocalVariableDecl{ action code }expressionSEMI{ action code }RBRACE

trans

TRANS1TRANS2EDGEidentifier{ action code }LBRACEidentifier{ action code }ARROWidentifier{ action code }STAR{ action code }PLUS{ action code }ONLABELlabel{ action code }WHEREexpression{ action code }SEMIRBRACE

invariantExpression

INVARIANTidentifier{ action code }LBRACEexpressionSEMI{ action code }RBRACEINLPARENidentifier{ action code }COMMAidentifier{ action code }RPAREN

goal

GOAL{ action code }LBRACEletExpr{ action code }IDENTpathCondAssignExprSEMI{ action code }assertExpr{ action code }CHECKENUMERATE{ action code }forExpr{ action code }viaExpr{ action code }stopExpr{ action code }RBRACE

forExpr

FOR{ action code }EACH{ action code }INTLITERAL{ action code }COMMAINTLITERAL{ action code }

stopExpr

REACHSTOPLPARENidentifier{ action code }COMMAidentifier{ action code }RPAREN

viaExpr

VIAWITHCONDITION{ action code }LPARENpathExpr{ action code }COMMApathExpr{ action code }RPAREN

letExpr

LETIDENT{ action code }pathCondAssignExpr{ action code }SEMI{ action code }

pathCondAssignExpr

EQUALpathCondition{ action code }

pathExpr

pathCondition{ action code }

pathCondition

orPathCondition{ action code }

orPathCondition

andPathCondition{ action code }'||'andPathCondition{ action code }

andPathCondition

xorPathCondition{ action code }'&&'xorPathCondition{ action code }

xorPathCondition

unaryPathCondition{ action code }'^'unaryPathCondition{ action code }

unaryPathCondition

'!'unaryPathCondition{ action code }primaryCondition{ action code }parPathCondition{ action code }

primaryCondition

stateIncExpr{ action code }pathPrimaryExpr{ action code }BOOLLITERAL{ action code }

parPathCondition

'('pathCondition{ action code }')'

stateCondExpr

stateOrExpr{ action code }

stateOrExpr

stateAndExpr{ action code }'||'stateAndExpr{ action code }

stateAndExpr

stateAtomicExpr{ action code }'&&'stateAtomicExpr{ action code }

stateUnaryExpr

'!'stateUnaryExpr{ action code }stateAtomicExpr{ action code }

stateAtomicExpr

parStateIncExpr{ action code }stateIncExpr{ action code }

parStateIncExpr

'('stateIncExpr{ action code }')'

stateIncExpr

'<<'{ action code }INTLITERAL{ action code }'>>'{ action code }INTLITERAL{ action code }identifier{ action code }HATLBRACEINTLITERAL{ action code }COLONINTLITERAL{ action code }RBRACE'<<'{ action code }INTLITERAL{ action code }'>>'{ action code }INTLITERAL{ action code }'('identifier{ action code }HATLBRACEINTLITERAL{ action code }COLONINTLITERAL{ action code }RBRACE')'

transIncExpr

pathOrExpr{ action code }

pathOrExpr

pathAndExpr{ action code }'||'pathAndExpr{ action code }

pathAndExpr

pathXorExpr{ action code }'&&'pathXorExpr{ action code }

pathXorExpr

pathUnaryExpr{ action code }'^'pathUnaryExpr{ action code }

pathUnaryExpr

'!'pathUnaryExpr{ action code }pathAtomicExpr{ action code }

pathAtomicExpr

parTransIncExpr{ action code }pathPrimaryExpr{ action code }

pathPrimaryExpr

identifier{ action code }pathOP{ action code }ARROWidentifier{ action code }pathOP{ action code }'<<'INTLITERAL{ action code }{ action code }'>>'INTLITERAL{ action code }{ action code }'('identifier{ action code }pathOP{ action code }ARROWidentifier{ action code }pathOP{ action code }')'HATLBRACEINTLITERAL{ action code }COLONINTLITERAL{ action code }RBRACE

parTransIncExpr

'('transIncExpr{ action code }')'

pathOP

P_OP_ONE{ action code }

label

STRINGLITERAL{ action code }

identifier

IDENT{ action code }

stateModifier

START{ action code }FINAL{ action code }ABSTRACT{ action code }NORMAL{ action code }

literal

INTLITERAL{ action code }REALLITERAL{ action code }BOOLLITERAL{ action code }STRINGLITERAL{ action code }CHARLITERAL{ action code }

globalVariableDecl

typevariableDeclarator{ action code }SEMI

localVariableDecl

typevariableDeclarator{ action code }SEMI

modifier

'global''native'

type

primitiveType{ action code }enumType{ action code }

primitiveType

INT{ action code }BOOL{ action code }REAL{ action code }STRING{ action code }

enumType

ENUM{ action code }LBRACEidentifier{ action code }COMMAidentifier{ action code }RBRACE

variableDeclarator

{ action code }identifier{ action code }'='variableInitializer{ action code }WHEREexpression{ action code }

variableInitializer

expression{ action code }

assertExpr

ASSERTexpression{ action code }INLPARENidentifier{ action code }COMMAidentifier{ action code }RPARENSEMI

expression

conditionalImpliesExpression{ action code }assignmentOperatorexpression{ action code }

assignmentOperator

'='{ action code }'+='{ action code }'-='{ action code }'*='{ action code }'/='{ action code }

conditionalImpliesExpression

conditionalOrExpression{ action code }IMPLIESconditionalOrExpression{ action code }

conditionalOrExpression

conditionalAndExpression{ action code }'||'conditionalAndExpression{ action code }

conditionalAndExpression

conditionalXorExpression{ action code }'&&'conditionalXorExpression{ action code }

conditionalXorExpression

equalityExpression{ action code }XORequalityExpression{ action code }

equalityExpression

relationalExpression{ action code }'==''!='relationalExpression{ action code }

relationalExpression

additiveExpression{ action code }relationalOpadditiveExpression{ action code }

relationalOp

'<='{ action code }'>='{ action code }'<'{ action code }'>'{ action code }

additiveExpression

multiplicativeExpression{ action code }'+''-'multiplicativeExpression{ action code }

multiplicativeExpression

unaryExpression{ action code }'*''/''%'unaryExpression{ action code }

unaryExpression

'+'unaryExpression{ action code }'-'unaryExpression{ action code }unaryExpressionNotPlusMinus{ action code }

unaryExpressionNotPlusMinus

'!'unaryExpression{ action code }primary{ action code }'--''++'{ action code }

primary

parExpression{ action code }identifierDOTidentifier{ action code }literal{ action code }PREVLPARENidentifierRPAREN{ action code }INITIALLPARENidentifierRPAREN{ action code }FRESHLPARENidentifierRPAREN{ action code }

parExpression

'('expression{ action code }')'