CHARON Department of Computer and Information Science
University of Pennsylvania
   
  | | | | | |
 Modular Specification of Hybrid Systems
 CHARON Grammar
 

BNF for charon.jj

NON-TERMINALS

ProgramInput ::= ( AgentDef ProgramInput | ModeDef ProgramInput | ExternDecl ProgramInput )? <EOF>
AgentDef ::= <AGENT> AgentName <LPAREN> ParamList <RPAREN> <LBRACE> Declarations AgentInit AgentStmts <RBRACE>
AgentName ::= <ID>
AgentInit ::= ( <INIT> <LBRACE> ( AssignStmt ( <SEMICOLON> )? )* <RBRACE> )?
AgentStmts ::= ( ( ModeReference ) | ( ( AgentReference )+ ) )
AgentReference ::= <AGENT> AgentName <ASSIGN> AgentName ( <LPAREN> ParamEval <RPAREN> ( <LBRACKET> IORenaming <RBRACKET> )? ) ( <SEMICOLON> )?
ParamList ::= ( ParamDecl ( <COMMA> ParamDecl )* | )
ParamDecl ::= ParamType ( <ID> )
ParamType ::= VarType ( <LBRACKET> <RBRACKET> )?
VarType ::= ( StandardType | UserDefinedType )
StandardType ::= ( <REAL> | <INT> | <BOOL> )
UserDefinedType ::= <ID> ( <DOT> <ID> )*
Declarations ::= ( RwDecl Declarations | )
ExternDecl ::= <EXTERN> ExternType ExternName ( <LPAREN> ParamTypeList <RPAREN> )? ( <SEMICOLON> )?
ExternType ::= ParamType
ExternName ::= <ID> ( <DOT> <ID> )*
ParamTypeList ::= ( ParamType ( <COMMA> ParamType )* )?
ParamEval ::= ( EvaluationList )?
EvaluationList ::= ArithExpr ( <COMMA> ArithExpr )*
IORenaming ::= VarList <APPLY> RenamingVarList
RenamingVarList ::= VarList
ModeDef ::= <MODE> ModeName <LPAREN> ParamList <RPAREN> <LBRACE> CtrlPoints Declarations ModeStmts <RBRACE>
ModeName ::= <ID>
CtrlPoints ::= ( CtrlPointType CtrlPointList ( <SEMICOLON> )? )*
CtrlPointName ::= <ID>
CtrlPointType ::= ( <ENTRY> | <EXIT> )
CtrlPointList ::= CtrlPointName ( <COMMA> CtrlPointName )*
ModeStmts ::= ( ModeInvariant ModeStmts | DiffEqns ModeStmts | AlgeEqns ModeStmts | ModeReference ModeStmts | Transition ModeStmts | )
ModeReference ::= <MODE> ModeName <ASSIGN> ModeName <LPAREN> ParamEval <RPAREN> ( <SEMICOLON> )?
RwDecl ::= RwInterface VarOrChannel
RwInterface ::= ( <READWRITE> | <READ> | <WRITE> | <PRIVATE> )
VarOrChannel ::= ( VarDecl | ChannelDecl )
VarDecl ::= UpdateSpecifier VarType VarList ( <SEMICOLON> )?
UpdateSpecifier ::= ( <ANALOG> | <DISCRETE> | )
VarList ::= VarName ( <COMMA> VarName )*
VarName ::= ( <ID> ) ( <LBRACKET> IndexDecl <RBRACKET> )?
IndexDecl ::= ( <ID> | <INT_NUM> ) <DOUBLEDOTS> ( <ID> | <INT_NUM> )
ChannelDecl ::= <CHANNEL> BufSize <OF> MessageType BufFullPolicy ChannelList ( <SEMICOLON> )?
BufSize ::= ( <LBRACKET> ( <INT_NUM> ) <RBRACKET> | )
MessageType ::= ParamType
BufFullPolicy ::= ( <COLD> | <HOT> | )
ChannelList ::= ChannelName ( <COMMA> ChannelName )*
ChannelName ::= <ID>
ModeInvariant ::= <INV> InvName <LBRACE> BoolExpr <RBRACE>
InvName ::= ( ( <ID> ) | )
BoolExpr ::= SimpleExpr ( <OR> SimpleExpr )*
SimpleExpr ::= RelExpr ( <AND> RelExpr )*
RelExpr ::= ArithExpr ( RelOp ArithExpr )?
RelOp ::= ( <LT> | <GT> | <LE> | <GE> | <EQ> | <NE> )
DiffEqns ::= <DIFF> DiffEqnName <LBRACE> ( DiffEqn )* <RBRACE>
DiffEqnName ::= ( ( <ID> ) | )
DiffEqn ::= <D> DiffVarName <RPAREN> RelOp ArithExpr ( <SEMICOLON> )?
DiffVarName ::= ObjectRef
AlgeEqns ::= <ALGE> AlgeEqnName <LBRACE> ( AlgeEqn )* <RBRACE>
AlgeEqnName ::= ( ( <ID> ) | )
AlgeEqn ::= ObjectRef RelOp ArithExpr ( <SEMICOLON> )?
Transition ::= <TRANS> TransitionName <FROM> LocName ( <WHEN> Guard )? ToConstruct
TransitionName ::= ( ( <ID> ) | )
LocName ::= NameDefault ( <DOT> NameDefault )?
NameDefault ::= ( ( <ID> ) | <_DEFAULT> )
ToConstruct ::= ( <TO> LocName GuardedAction )+
GuardedAction ::= <WHEN> Guard Actions
Guard ::= BoolExpr
Actions ::= ( <DO> ActionStmts )?
ActionStmts ::= <LBRACE> ( TermActionStmt )* <RBRACE>
TermActionStmt ::= ( AssignStmt | SendReceive ) ( <SEMICOLON> )?
SendReceive ::= ( SendAction | ReceiveAction )
SendAction ::= <SEND> <LPAREN> ChannelName <COMMA> ArithExpr <RPAREN>
ReceiveAction ::= <RECEIVE> <LPAREN> ChannelName <COMMA> ObjectRef <RPAREN>
AssignStmt ::= ObjectRef <ASSIGN> ArithExpr
ArithExpr ::= Term ( AddOp Term )*
Term ::= Factor ( MulOp Factor )*
Factor ::= ( ObjectRef | <INT_NUM> | <REAL_NUM> | <LPAREN> BoolExpr <RPAREN> | <TRUE> | <FALSE> | <ISEMPTY> <LPAREN> ChannelName <RPAREN> | <NOT> Factor | <PLUS> Factor | <MINUS> Factor )
ObjectRef ::= FieldRef ( <DOT> ( MethodCall | FieldRef ) )*
MethodCall ::= ( <ID> ) <LPAREN> ParamEval <RPAREN>
FieldRef ::= ( <ID> ) ( <LBRACKET> ArithExpr <RBRACKET> )?
AddOp ::= ( <PLUS> | <MINUS> )
MulOp ::= ( <MULT> | <DIV> | "%" )

Maintained by Oleg Sokolsky, Valentina Sokolskaya