Uppaal:


               Uppaal   ::= ( T_NEW | T_NEW_SYSTEM ) XTA
                          | ( T_NEW_DECLARATION | T_NEW_INST ) Declarations
                          | T_NEW_LOCAL_DECLProcLocalDeclList
                          | T_NEW_PARAMETERSParameterList
                          | ( T_NEW_INVARIANT | T_NEW_GUARD | 'probability' | T_EXPRESSION | T_CONDITION ) Expression
                          | T_NEW_SELECTSelectList
                          | T_NEW_SYNCSyncExpr
                          | ( T_NEW_ASSIGN | T_EXPRESSION_LIST | T_UPDATE ) ExprList
                          | T_PROPERTYQueryList
                          | T_XTA_PROCESSProcDecl
                          | T_EXPONENTIAL_RATEExpRate
                          | T_MESSAGEMessExpr
                          | T_INSTANCE_LINEInstanceLineExpression

no references

XTA:


               XTA      ::= DeclarationsSystemXTAQueryList

referenced by:

Uppaal

Instantiations:


               Instantiations
                        ::= Instantiation*

no references

Instantiation:


               Instantiation
                        ::= NonTypeIdOptionalInstanceParameterList '=' NonTypeId '(' ArgList ')' ';'

referenced by:

Declarations
Instantiations

InstanceLineExpression:


               InstanceLineExpression
                        ::= NonTypeId ( '(' ArgList ')' )?

referenced by:

Uppaal

OptionalInstanceParameterList:


               OptionalInstanceParameterList
                        ::= ( '(' ParameterList? ')' )?

referenced by:

Instantiation

System:


               System   ::= SysDeclProgressGanttDecl

referenced by:

PriorityDecl:


               PriorityDecl
                        ::= 'chan' 'priority' ChanElement ( ( ',' | '<' ) ChanElement )* ';'

referenced by:

Declarations

ChanElement:


               ChanElement
                        ::= NonTypeId ( '[' Expression ']' )*
                          | 'default'

referenced by:

PriorityDecl

SysDecl:


               SysDecl  ::= 'system' NonTypeId ( ( ',' | '<' ) NonTypeId )* ';'

referenced by:

System

Progress:


               Progress ::= ( 'progress' '{' ( Expression ( ':' Expression )? ';' )* '}' )?

referenced by:

System

GanttDecl:


               GanttDecl
                        ::= ( 'gantt' '{' ( NonTypeIdGanttArgs ':' GanttExpr ( ',' GanttExpr )* ';' )* '}' )?

referenced by:

System

GanttArgs:


               GanttArgs
                        ::= ( '(' Id ':' Type ( ',' Id ':' Type )* ')' )?

referenced by:

GanttDecl

GanttExpr:


               GanttExpr
                        ::= ( 'for' '(' Id ':' Type ( ',' Id ':' Type )* ')' )? Expression '->' Expression

referenced by:

GanttDecl

Declarations:


               Declarations
                        ::= ( FunctionDecl | ExternDecl | VariableDecl | TypeDecl | ProcDecl | BeforeUpdateDecl | AfterUpdateDecl | Instantiation | PriorityDecl | DynamicDeclaration )*

referenced by:

Uppaal
XTA

DynamicDeclaration:


               DynamicDeclaration
                        ::= 'dynamic' NonTypeIdOptionalParameterList ';'

referenced by:

Declarations

BeforeUpdateDecl:


               BeforeUpdateDecl
                        ::= 'before_update' '{' ExprList '}'

referenced by:

Declarations

AfterUpdateDecl:


               AfterUpdateDecl
                        ::= 'after_update' '{' ExprList '}'

referenced by:

Declarations

FunctionDecl:


               FunctionDecl
                        ::= TypeIdOptionalParameterList '{' BlockLocalDeclListStatementList '}'

referenced by:

Declarations
ProcLocalDeclList

ExternDecl:


               ExternDecl
                        ::= 'import' QuotedTextFwdDeclBlock

referenced by:

Declarations

FwdDeclBlock:


               FwdDeclBlock
                        ::= ( '{' ( FwdDecl ';' )+ '}' | FwdDecl ) ';'

referenced by:

ExternDecl

FwdDecl:


               FwdDecl  ::= ( Id '=' )? TypeIdOptionalParameterList

referenced by:

FwdDeclBlock

OptionalParameterList:


               OptionalParameterList
                        ::= '(' ParameterList? ')'

referenced by:

DynamicDeclaration
FunctionDecl
FwdDecl
ProcDecl

ParameterList:


               ParameterList
                        ::= Parameter ( ',' Parameter )*

referenced by:

OptionalInstanceParameterList
OptionalParameterList
Uppaal

Parameter:


               Parameter
                        ::= Type '&'? NonTypeIdArrayDecl

referenced by:

ParameterList

VariableDecl:


               VariableDecl
                        ::= TypeDeclId ( ',' DeclId )* ';'

referenced by:

BlockLocalDeclList
Declarations
ProcLocalDeclList

DeclId:


               DeclId   ::= IdArrayDeclVarInit

referenced by:

VariableDecl

VarInit:


               VarInit  ::= ( '=' Initializer )?

referenced by:

DeclId

Initializer:


               Initializer
                        ::= Expression
                          | '{' FieldInit ( ',' FieldInit )* '}'

referenced by:

FieldInit
VarInit

FieldInit:


               FieldInit
                        ::= ( Id ':' )? Initializer

referenced by:

Initializer

ArrayDecl:


               ArrayDecl
                        ::= ( '[' ( Expression | Type ) ']' )*

referenced by:

DeclId
FieldDeclId
Parameter
TypeId

TypeDecl:


               TypeDecl ::= 'typedef' TypeTypeId ( ',' TypeId )* ';'

referenced by:

BlockLocalDeclList
Declarations
ProcLocalDeclList

TypeId:


               TypeId   ::= IdArrayDecl

referenced by:

Id
Type
TypeDecl

Type:


               Type     ::= TypePrefix? ( TypeId | 'struct' '{' FieldDeclList '}' | 'bool' | 'double' | 'string' | 'int' ( '[' Expression ',' Expression ']' )? | 'chan' | 'scalar' '[' Expression ']' )
                          | 'hybrid'? 'clock'
                          | 'void'

referenced by:

ArrayDecl
Expression
FieldDecl
ForStatement
FunctionDecl
FwdDecl
GanttArgs
GanttExpr
Parameter
SelectList
TypeDecl
VariableDecl

Id:


               Id       ::= NonTypeId
                          | TypeId

referenced by:

DeclId
DynamicExpression
Expression
FieldDeclId
FieldInit
ForStatement
FunctionDecl
FwdDecl
GanttArgs
GanttExpr
Imitation
ProcDecl
Query
SelectList
SubjectionList
TypeId

NonTypeId:


               NonTypeId
                        ::= Identifier
                          | 'A'
                          | 'U'
                          | 'W'
                          | 'R'
                          | 'E'
                          | 'M'
                          | 'sup'
                          | 'inf'
                          | 'simulation'

referenced by:

BranchpointDecl
ChanElement
Commit
DynamicDeclaration
DynamicExpression
Expression
GanttDecl
Id
Init
InstanceLineExpression
Instantiation
Parameter
Query
StateDecl
SysDecl
Transition
TransitionOpt
Urgent

FieldDeclList:


               FieldDeclList
                        ::= FieldDecl+

referenced by:

Type

FieldDecl:


               FieldDecl
                        ::= TypeFieldDeclId ( ',' FieldDeclId )* ';'

referenced by:

FieldDeclList

FieldDeclId:


               FieldDeclId
                        ::= IdArrayDecl

referenced by:

FieldDecl

TypePrefix:


               TypePrefix
                        ::= 'urgent' 'broadcast'?
                          | 'broadcast'
                          | 'const'
                          | 'meta'

referenced by:

Type

ProcDecl:


               ProcDecl ::= 'process' IdOptionalParameterList '{' ProcBody '}'

referenced by:

Declarations
Uppaal

ProcBody:


               ProcBody ::= ( ProcLocalDeclListStatesBranchpoints? LocFlagsInitTransitions )?

referenced by:

ProcDecl

ProcLocalDeclList:


               ProcLocalDeclList
                        ::= ( FunctionDecl | VariableDecl | TypeDecl )*

referenced by:

ProcBody
Uppaal

States:


               States   ::= 'state' StateDecl ( ',' StateDecl )* ';'

referenced by:

ProcBody

StateDecl:


               StateDecl
                        ::= NonTypeId ( '{' ( ';' ExpRate | Expression ( ';' ExpRate )? ) '}' )?

referenced by:

States

Branchpoints:


               Branchpoints
                        ::= 'branchpoint' BranchpointDecl ( ',' BranchpointDecl )* ';'

referenced by:

ProcBody

BranchpointDecl:


               BranchpointDecl
                        ::= NonTypeId

referenced by:

Branchpoints

Init:


               Init     ::= 'init' NonTypeId ';'

referenced by:

ProcBody

Transitions:


               Transitions
                        ::= ( 'trans' Transition ( ',' TransitionOpt )* ';' )?

referenced by:

ProcBody

Transition:


               Transition
                        ::= NonTypeId ( '->' | '-u->' ) NonTypeId '{' SelectGuardSyncAssignProbability '}'

referenced by:

TransitionOpt
Transitions

TransitionOpt:


               TransitionOpt
                        ::= ( '->' | '-u->' ) NonTypeId '{' SelectGuardSyncAssign '}'
                          | Transition

referenced by:

Transitions

Select:


               Select   ::= ( 'select' SelectList ';' )?

referenced by:

Transition
TransitionOpt

SelectList:


               SelectList
                        ::= Id ':' Type ( ',' Id ':' Type )*

referenced by:

Select
Uppaal

Guard:


               Guard    ::= ( 'guard' Expression ';' )?

referenced by:

Transition
TransitionOpt

Sync:


               Sync     ::= ( 'sync' SyncExpr ';' )?

referenced by:

Transition
TransitionOpt

SyncExpr:


               SyncExpr ::= Expression ( '!' | '?' )

referenced by:

Sync
Uppaal

MessExpr:


               MessExpr ::= Expression

referenced by:

Uppaal

Assign:


               Assign   ::= ( 'assign' ExprList ';' )?

referenced by:

Transition
TransitionOpt

Probability:


               Probability
                        ::= ( 'probability' Expression ';' )?

referenced by:

Transition

LocFlags:


               LocFlags ::= ( Commit | Urgent )*

referenced by:

ProcBody

Commit:


               Commit   ::= 'commit' NonTypeId ( ',' NonTypeId )* ';'

referenced by:

LocFlags

Urgent:


               Urgent   ::= 'urgent' NonTypeId ( ',' NonTypeId )* ';'

referenced by:

LocFlags

ExpRate:


               ExpRate  ::= Expression ( ':' Expression )?

referenced by:

StateDecl
Uppaal

Block:


               Block    ::= '{' BlockLocalDeclListStatementList '}'

referenced by:

OtherStatement

BlockLocalDeclList:


               BlockLocalDeclList
                        ::= ( VariableDecl | TypeDecl )*

referenced by:

Block
FunctionDecl

StatementList:


               StatementList
                        ::= ( Statement ';' )*

referenced by:

Block
FunctionDecl
SwitchCase

Statement:


               Statement
                        ::= ( IfConditionThenMatched* IfCondition )* MatchedStatement

referenced by:

ForStatement
StatementList
WhileStatement

IfCondition:


               IfCondition
                        ::= 'if' '(' ExprList ')'

referenced by:

IfConditionThenMatched
Statement

IfConditionThenMatched:


               IfConditionThenMatched
                        ::= IfConditionMatchedStatement 'else'

referenced by:

MatchedStatement
Statement

MatchedStatement:


               MatchedStatement
                        ::= IfConditionThenMatched* OtherStatement

referenced by:

IfConditionThenMatched
Statement

OtherStatement:


               OtherStatement
                        ::= Block
                          | ( 'assert'? Expression | 'break' | 'continue' | 'return' Expression? )? ';'
                          | ForStatement
                          | WhileStatement
                          | 'switch' '(' ExprList ')' '{' SwitchCase+ '}'

referenced by:

MatchedStatement

ForStatement:


               ForStatement
                        ::= 'for' '(' ( ExprList ';' ExprList ';' ExprList | Id ':' Type ) ')' Statement

referenced by:

OtherStatement

WhileStatement:


               WhileStatement
                        ::= 'while' '(' ExprList ')' Statement
                          | 'do' Statement 'while' '(' ExprList ')' ';'

referenced by:

OtherStatement

SwitchCase:


               SwitchCase
                        ::= ( 'case' Expression | 'default' ) ':' StatementList

referenced by:

OtherStatement

ExprList:


               ExprList ::= Expression ( ',' Expression )*

referenced by:

AfterUpdateDecl
Assign
BeforeUpdateDecl
ForStatement
IfCondition
OtherStatement
Uppaal
WhileStatement

Expression:


               Expression
                        ::= 'false'
                          | 'true'
                          | PosInteger
                          | DecimalNumber
                          | QuotedText
                          | ( BuiltinFunction1? '(' | ( BuiltinFunction2 '(' | BuiltinFunction3 '(' Expression ',' ) Expression ',' ) Expression ')'
                          | NonTypeId
                          | Expression ( '(' ArgList ')' | '[' Expression ']' | '++' | '--' | ( '<' | '<=' | '==' | '!=' | '>' | '>=' | '+' | '-' | '*' | '/'
                  | '%' | '**' | '&' | '|' | '^' | '<<' | '>>' | '&&' | '||' | '?' Expression ':' | 'imply' | 'and' | 'or' | 'xor' | '<?' | '>?' ) Expression | '.' ( 'location' | NonTypeId ) | "\'" )
                          | ( '++' | '--' | '-' | '+' | '!' | 'not' | ( 'sum' | 'forall' | 'exists'
                  ) '(' Id ':' Type ')' ) Expression
                          | '-' '2147483648'
                          | 'deadlock'
                          | DynamicExpression
                          | MITLExpression
                          | Assignment

referenced by:

ArgList
ArrayDecl
Assignment
ChanElement
ControlQuery
DynamicExpression
ExpRate
ExprList
Expression
GanttExpr
Guard
InfPrefix
Initializer
LearnQuery
LoadQuery
MITLExpression
MessExpr
NonEmptyExpressionList
OtherStatement
Probability
Progress
Query
RunBound
SMCQuery
StateDecl
SupPrefix
SwitchCase
SymbolicQuery
SyncExpr
Type
Uppaal

DynamicExpression:


               DynamicExpression
                        ::= ( 'spawn' NonTypeId '(' ArgList | 'exit' '(' | 'numOf' '(' NonTypeId | ( 'forall' | 'exists' ) '(' Id ':' NonTypeId ')' '(' Expression ) ')'
                          | ( 'sum' | 'foreach' ) '(' Id ':' NonTypeId ')' Expression

referenced by:

Expression

Assignment:


               Assignment
                        ::= ExpressionAssignOpExpression

referenced by:

Expression

AssignOp:


               AssignOp ::= '='
                          | '+='
                          | '-='
                          | '/='
                          | '%='
                          | '*='
                          | '&='
                          | '|='
                          | '^='
                          | '<<='
                          | '>>='

referenced by:

Assignment

UnaryOp:


               UnaryOp  ::= '-'
                          | '+'
                          | '!'
                          | 'not'

no references

BuiltinFunction1:


               BuiltinFunction1
                        ::= 'abs'
                          | 'fabs'
                          | 'exp'
                          | 'exp2'
                          | 'expm1'
                          | 'ln'
                          | 'log'
                          | 'log10'
                          | 'log2'
                          | 'log1p'
                          | 'sqrt'
                          | 'cbrt'
                          | 'sin'
                          | 'cos'
                          | 'tan'
                          | 'asin'
                          | 'acos'
                          | 'atan'
                          | 'sinh'
                          | 'cosh'
                          | 'tanh'
                          | 'asinh'
                          | 'acosh'
                          | 'atanh'
                          | 'erf'
                          | 'erfc'
                          | 'tgamma'
                          | 'lgamma'
                          | 'ceil'
                          | 'floor'
                          | 'trunc'
                          | 'round'
                          | 'fint'
                          | 'ilogb'
                          | 'logb'
                          | 'fpclassify'
                          | 'isfinite'
                          | 'isinf'
                          | 'isnan'
                          | 'isnormal'
                          | 'signbit'
                          | 'isunordered'
                          | 'random'
                          | 'random_poisson'

referenced by:

Expression

BuiltinFunction2:


               BuiltinFunction2
                        ::= 'fmod'
                          | 'fmax'
                          | 'fmin'
                          | 'fdim'
                          | 'pow'
                          | 'hypot'
                          | 'atan2'
                          | 'ldexp'
                          | 'nextafter'
                          | 'copysign'
                          | 'random_arcsine'
                          | 'random_beta'
                          | 'random_gamma'
                          | 'random_normal'
                          | 'random_weibull'

referenced by:

Expression

BuiltinFunction3:


               BuiltinFunction3
                        ::= 'fma'
                          | 'random_tri'

referenced by:

Expression

ArgList:


               ArgList  ::= Expression? ( ',' Expression )*

referenced by:

DynamicExpression
Expression
InstanceLineExpression
Instantiation

ExpQuantifier:


               ExpQuantifier
                        ::= 'minE'
                          | 'maxE'

no references

SubjectionList:


               SubjectionList
                        ::= Id

referenced by:

SMCQuery
Subjection

Subjection:


               Subjection
                        ::= ( 'under' SubjectionList )?

referenced by:

ControlQuery
LearnQuery
Query

Imitation:


               Imitation
                        ::= ( 'imitate' Id )?

referenced by:

LearnQuery

QueryList:


               QueryList
                        ::= Query ( '\n' Query )*

referenced by:

Uppaal

XTAQueryList:


               XTAQueryList
                        ::= ( 'query' '{' Query '}' )*

referenced by:

SymbolicQuery:


               SymbolicQuery
                        ::= ( 'A<>' | 'E<>' | 'E[]' | Expression '-->' ) Expression
                          | 'A[]' ( Expression | '(' Expression ( 'and' | '&&' ) 'A<>' Expression ')' )
                          | 'A' '[' Expression ( 'U' | 'W' ) Expression ']'
                          | ( 'sup' | 'inf' ) ( '{' Expression '}' )? ':' NonEmptyExpressionList

referenced by:

ControlQuery
Query

Features:


               Features ::= ( BracketExprList '->' BracketExprList )?

referenced by:

LearnQuery
LoadQuery

AssignableQuery:


               AssignableQuery
                        ::= ControlQuery
                          | LearnQuery
                          | LoadQuery

referenced by:

Query

ControlQuery:


               ControlQuery
                        ::= ( 'E<>' | ObservablePredicates )? 'control' ':' SymbolicQuerySubjection
                          | 'control_t' '*' ( '(' Expression ( ',' Expression )? ')' )? ':' SymbolicQuery

referenced by:

AssignableQuery

ObservablePredicates:


               ObservablePredicates
                        ::= '{' ExpressionList '}'

referenced by:

ControlQuery

LearnQuery:


               LearnQuery
                        ::= ( 'minE' | 'maxE' ) ( '(' Expression ')' )? '[' RunBound ']' FeaturesSubjectionImitation

referenced by:

AssignableQuery

LoadQuery:


               LoadQuery
                        ::= 'loadStrategy' Features '(' Expression ')'

referenced by:

AssignableQuery

Query:


               Query    ::= ( SymbolicQuery | SMCQuery ) Subjection
                          | 'saveStrategy' '(' Expression ',' Id ')'
                          | ( 'strategy' Id '=' )? AssignableQuery
                          | 'Pmax' Expression
                          | 'sat' ':' NonTypeId

referenced by:

QueryList
XTAQueryList

SMCQuery:


               SMCQuery ::= 'simulate' SMCBounds '{' NonEmptyExpressionList '}' ( ':' ( NumberOfRuns ':' )? Expression )?
                          | 'Pr' ( SMCBounds '(' ( ( '<>' | '[]' ) Expression ')' ( ( '>=' | '<=' ) ProbNumber | ( 'under' SubjectionList )? '>=' 'Pr' SMCBounds '(' ( '<>' | '[]' ) Expression ')' )? | Expression 'U' Expression ')' ) | Expression )
                          | 'E' SMCBounds '(' ( 'max' | 'min' ) ':' Expression ')'

referenced by:

Query

MITLExpression:


               MITLExpression
                        ::= '(' ( ( Expression ( 'U' | 'R' ) | '<>' | '[]' ) '[' PosInteger ',' PosInteger ']' | 'X' ) Expression ')'

referenced by:

Expression

SMCBounds:


               SMCBounds
                        ::= '[' RunBound ( ';' PosInteger )? ']'

referenced by:

SMCQuery

RunBound:


               RunBound ::= ( '#' | Expression )? '<=' Expression

referenced by:

LearnQuery
SMCBounds

BracketExprList:


               BracketExprList
                        ::= '{' ExpressionList '}'

referenced by:

Features

ExpressionList:


               ExpressionList
                        ::= NonEmptyExpressionList?

referenced by:

BracketExprList
ObservablePredicates

NonEmptyExpressionList:


               NonEmptyExpressionList
                        ::= Expression ( ',' Expression )*

referenced by:

ExpressionList
SMCQuery
SymbolicQuery

SupPrefix:


               SupPrefix
                        ::= 'sup' ( '{' Expression '}' )? ':'

no references

InfPrefix:


               InfPrefix
                        ::= 'inf' ( '{' Expression '}' )? ':'

no references

... generated by RR - Railroad Diagram Generator