Grammar
Below, the grammar of the CIF language is shown, in a form closely resembling Backus-Naur Form (BNF). The Specification non-terminal is the start symbol of the grammar. Text between quotes are terminals. Names using only upper case letters are defined in the lexical syntax. The remaining names are the non-terminals of the grammar.
Specification : OptDoubleAnnos GroupBody
;
GroupBody : OptGroupDecls
;
AutomatonBody : OptAutDecls Locations OptIoDecls
;
OptGroupDecls : /* empty */
| OptGroupDecls GroupDecl
;
GroupDecl : Decl
| "import" Imports ";"
| "namespace" IDENTIFIERTK ";"
| "namespace" RELATIVENAMETK ";"
| "func" Types Identifier FuncParams ":" FuncBody
| Annos "func" Types Identifier FuncParams ":" FuncBody
| Identifier ":" Name CompInstArgs ";"
| Annos Identifier ":" Name CompInstArgs ";"
| "group" "def" Identifier CompDefParms ":" GroupBody "end"
| Annos "group" "def" Identifier CompDefParms ":" GroupBody "end"
| OptSupKind "automaton" "def" Identifier CompDefParms ":" AutomatonBody "end"
| Annos OptSupKind "automaton" "def" Identifier CompDefParms ":" AutomatonBody "end"
| SupKind "def" Identifier CompDefParms ":" AutomatonBody "end"
| Annos SupKind "def" Identifier CompDefParms ":" AutomatonBody "end"
| "group" Identifier ":" GroupBody "end"
| Annos "group" Identifier ":" GroupBody "end"
| OptSupKind "automaton" Identifier ":" AutomatonBody "end"
| Annos OptSupKind "automaton" Identifier ":" AutomatonBody "end"
| SupKind Identifier ":" AutomatonBody "end"
| Annos SupKind Identifier ":" AutomatonBody "end"
;
OptAutDecls : /* empty */
| OptAutDecls AutDecl
;
AutDecl : Decl
| "alphabet" Events ";"
| "alphabet" ";"
| "monitor" Events ";"
| "monitor" ";"
| "disc" Type DiscDecls ";"
| Annos "disc" Type DiscDecls ";"
;
Decl : "type" TypeDefs ";"
| Annos "type" TypeDefs ";"
| "enum" Identifier "=" AnnotatedIdentifiers ";"
| Annos "enum" Identifier "=" AnnotatedIdentifiers ";"
| OptControllability "event" Identifiers ";"
| Annos OptControllability "event" Identifiers ";"
| OptControllability "event" EventType Identifiers ";"
| Annos OptControllability "event" EventType Identifiers ";"
| Controllability Identifiers ";"
| Annos Controllability Identifiers ";"
| Controllability EventType Identifiers ";"
| Annos Controllability EventType Identifiers ";"
| "const" Type ConstantDefs ";"
| Annos "const" Type ConstantDefs ";"
| "alg" Type AlgVarsDefs ";"
| Annos "alg" Type AlgVarsDefs ";"
| "input" Type Identifiers ";"
| Annos "input" Type Identifiers ";"
| "cont" ContDecls ";"
| Annos "cont" ContDecls ";"
| "equation" Equations ";"
| "initial" Expressions ";"
| InvariantDecls
| Annos InvariantDecls
| "marked" Expressions ";"
| IoDecl
;
Identifiers : Identifier
| Identifiers "," Identifier
;
Identifier : IDENTIFIERTK
;
AnnotatedIdentifiers : AnnotatedIdentifier
| AnnotatedIdentifiers "," AnnotatedIdentifier
;
AnnotatedIdentifier : OptAnnos IDENTIFIERTK
;
Imports : StringToken
| Imports "," StringToken
;
StringToken : STRINGTK
;
TypeDefs : Identifier "=" Type
| TypeDefs "," Identifier "=" Type
;
ConstantDefs : Identifier "=" Expression
| ConstantDefs "," Identifier "=" Expression
;
AlgVarsDefs : Identifier
| Identifier "=" Expression
| AlgVarsDefs "," Identifier
| AlgVarsDefs "," Identifier "=" Expression
;
FuncParams : "(" ")"
| "(" FuncParamDecls ")"
;
FuncParamDecls : FuncParamDecl
| FuncParamDecls ";" FuncParamDecl
;
FuncParamDecl : OptAnnos Type Identifiers
;
FuncBody : FuncVarDecls FuncStatements "end"
| StringToken ";"
;
FuncVarDecls : /* empty */
| FuncVarDecls Type FuncVarDecl ";"
| FuncVarDecls Annos Type FuncVarDecl ";"
;
FuncVarDecl : Identifier
| Identifier "=" Expression
| FuncVarDecl "," Identifier
| FuncVarDecl "," Identifier "=" Expression
;
FuncStatements : FuncStatement
| FuncStatements FuncStatement
;
FuncStatement : Addressables ":=" Expressions ";"
| "if" Expressions ":" FuncStatements
OptElifFuncStats OptElseFuncStat "end"
| "while" Expressions ":" FuncStatements "end"
| "break" ";"
| "continue" ";"
| "return" Expressions ";"
;
OptElifFuncStats : /* empty */
| OptElifFuncStats "elif" Expressions ":" FuncStatements
;
OptElseFuncStat : /* empty */
| "else" FuncStatements
;
Events : Name
| Events "," Name
;
CoreEdge : EdgeEvents OptEdgeGuard OptEdgeUrgent OptEdgeUpdate
| "when" Expressions OptEdgeUrgent OptEdgeUpdate
| "now" OptEdgeUpdate
| "do" Updates
;
OptEdgeGuard : /* empty */
| "when" Expressions
;
OptEdgeUrgent : /* empty */
| "now"
;
OptEdgeUpdate : /* empty */
| "do" Updates
;
EdgeEvents : EdgeEvent
| EdgeEvents "," EdgeEvent
;
EdgeEvent : "tau"
| Name
| Name "!"
| Name "!" Expression
| Name "?"
;
Locations : Location
| Locations Location
;
Location : "location" ";"
| Annos "location" ";"
| "location" Identifier ";"
| Annos "location" Identifier ";"
| "location" ":" LocationElements
| Annos "location" ":" LocationElements
| "location" Identifier ":" LocationElements
| Annos "location" Identifier ":" LocationElements
;
LocationElements : LocationElement
| LocationElements LocationElement
;
LocationElement : "initial" ";"
| "initial" Expressions ";"
| OptDoubleAnnos InvariantDecls
| "equation" Equations ";"
| "marked" ";"
| "marked" Expressions ";"
| "urgent" ";"
| OptDoubleAnnos "edge" CoreEdge ";"
| OptDoubleAnnos "edge" CoreEdge "goto" Identifier ";"
;
CompInstArgs : "(" ")"
| "(" Expressions ")"
;
CompDefParms : "(" ")"
| "(" CompDefDecls ")"
;
CompDefDecls : CompDefDeclaration
| CompDefDecls ";" CompDefDeclaration
;
CompDefDeclaration : OptControllability "event" EventParamIds
| OptControllability "event" EventType EventParamIds
| Controllability EventParamIds
| Controllability EventType EventParamIds
| Name Identifiers
| "location" Identifiers
| OptAnnos "alg" Type Identifiers
;
EventParamIds : EventParamId
| EventParamIds "," EventParamId
;
EventParamId : Identifier OptEventParamFlags
;
OptEventParamFlags : /* empty */
| OptEventParamFlags EventParamFlag
;
EventParamFlag : "!"
| "?"
| "~"
;
DiscDecls : DiscDecl
| DiscDecls "," DiscDecl
;
DiscDecl : Identifier
| Identifier "in" "any"
| Identifier "=" Expression
| Identifier "in" "{" Expressions "}"
;
ContDecls : ContDecl
| ContDecls "," ContDecl
;
ContDecl : Identifier OptDerivative
| Identifier "=" Expression OptDerivative
;
OptDerivative : /* empty */
| "der" Expression
;
Equations : Equation
| Equations "," Equation
;
Equation : Identifier "'" "=" Expression
| Identifier "=" Expression
;
InvariantDecls : OptSupKind "invariant" Invariants ";"
| SupKind Invariants ";"
;
Invariants : Invariant
| Invariants "," Invariant
;
Invariant : Expression
| Identifier ":" Expression
| Name "needs" Expression
| Identifier ":" Name "needs" Expression
| NonEmptySetExpression "needs" Expression
| Expression "disables" Name
| Identifier ":" Expression "disables" Name
| Expression "disables" NamesSet
;
NamesSet : "{" Names "}"
;
Names : Name
| Names "," Name
;
Updates : Update
| Updates "," Update
;
Update : Addressable ":=" Expression
| "if" Expressions ":" Updates
OptElifUpdates OptElseUpdate "end"
;
Addressables : Addressable
| Addressables "," Addressable
;
Addressable : Name
| Name Projections
| "(" Addressable "," Addressables ")"
;
Projections : Projection
| Projections Projection
;
Projection : "[" Expression "]"
;
OptElifUpdates : /* empty */
| OptElifUpdates "elif" Expressions ":" Updates
;
OptElseUpdate : /* empty */
| "else" Updates
;
OptSupKind : /* empty */
| SupKind
;
OptControllability : /* empty */
| Controllability
;
Controllability : "controllable"
| "uncontrollable"
;
///////////////////////////////////////////////////////////////////////////////
OptIoDecls : /* empty */
| OptIoDecls IoDecl
;
IoDecl : SvgFile
| SvgCopy
| SvgMove
| SvgOut
| SvgIn
| PrintFile
| Print
;
SvgFile : "svgfile" StringToken ";"
;
OptSvgFile : /* empty */
| "file" StringToken
;
SvgCopy : "svgcopy" "id" Expression OptSvgCopyPre OptSvgCopyPost OptSvgFile ";"
;
OptSvgCopyPre : /* empty */
| "pre" Expression
;
OptSvgCopyPost : /* empty */
| "post" Expression
;
SvgMove : "svgmove" "id" Expression "to" Expression "," Expression
OptSvgFile ";"
;
SvgOut : "svgout" "id" Expression SvgAttr "value" Expression OptSvgFile
";"
;
SvgAttr : "attr" StringToken
| "text"
;
SvgIn : "svgin" "id" Expression "event" SvgInEvent OptSvgFile ";"
| "svgin" "id" Expression "do" Updates OptSvgFile ";"
;
SvgInEvent : Name
| "if" Expression ":" Name OptSvgInEventElifs "else" Name "end"
| "if" Expression ":" Name SvgInEventElifs "end"
;
OptSvgInEventElifs : /* empty */
| SvgInEventElifs
;
SvgInEventElifs : "elif" Expression ":" Name
| SvgInEventElifs "elif" Expression ":" Name
;
PrintFile : "printfile" StringToken ";"
;
Print : "print" PrintTxt OptPrintFors OptPrintWhen OptPrintFile ";"
;
PrintTxt : Expression
| "pre" Expression
| "post" Expression
| "pre" Expression "post" Expression
;
OptPrintFors : /* empty */
| "for" PrintFors
;
PrintFors : PrintFor
| PrintFors "," PrintFor
;
PrintFor : "event"
| "time"
| Name
| "initial"
| "final"
;
OptPrintWhen : /* empty */
| "when" Expression
| "when" "pre" Expression
| "when" "post" Expression
| "when" "pre" Expression "post" Expression
;
OptPrintFile : /* empty */
| "file" StringToken
;
///////////////////////////////////////////////////////////////////////////////
Types : Type
| Types "," Type
;
EventType : "void"
| Type
;
Type : "bool"
| "int"
| "int" "[" Expression ".." Expression "]"
| "real"
| "string"
| "list" Type
| "list" "[" Expression "]" Type
| "list" "[" Expression ".." Expression "]" Type
| "set" Type
| "dict" "(" Type ":" Type ")"
| "tuple" "(" Fields ")"
| "func" Type "(" ")"
| "func" Type "(" Types ")"
| "dist" Type
| Name
;
Fields : Field
| Fields ";" Field
;
Field : Type Identifiers
;
///////////////////////////////////////////////////////////////////////////////
Expressions : Expression
| Expressions "," Expression
;
OptExpression : /* empty */
| Expression
;
Expression : OrExpression
| OrExpression "=>" OrExpression
| OrExpression "<=>" OrExpression
;
OrExpression : AndExpression
| OrExpression "or" AndExpression
;
AndExpression : CompareExpression
| AndExpression "and" CompareExpression
;
CompareExpression : AddExpression
| CompareExpression "<" AddExpression
| CompareExpression "<=" AddExpression
| CompareExpression "=" AddExpression
| CompareExpression "!=" AddExpression
| CompareExpression ">=" AddExpression
| CompareExpression ">" AddExpression
| CompareExpression "in" AddExpression
| CompareExpression "sub" AddExpression
;
AddExpression : MulExpression
| AddExpression "+" MulExpression
| AddExpression "-" MulExpression
;
MulExpression : UnaryExpression
| MulExpression "*" UnaryExpression
| MulExpression "/" UnaryExpression
| MulExpression "div" UnaryExpression
| MulExpression "mod" UnaryExpression
;
UnaryExpression : FuncExpression
| "-" UnaryExpression
| "+" UnaryExpression
| "not" UnaryExpression
| "sample" FuncExpression
;
FuncExpression : ExpressionFactor
| FuncExpression "[" Expression "]"
| FuncExpression
"[" OptExpression ":" OptExpression "]"
| FuncExpression "(" ")"
| FuncExpression "(" Expressions ")"
| StdLibFunction "(" ")"
| StdLibFunction "(" Expressions ")"
;
ExpressionFactor : "true"
| "false"
| NUMBERTK
| REALTK
| StringToken
| "time"
| "[" "]"
| "[" Expressions "]"
| "{" "}"
| NonEmptySetExpression
| "{" DictPairs "}"
| "(" Expression "," Expressions ")"
| "<" Type ">" ExpressionFactor
| "if" Expressions ":" Expression
OptElifExprs "else" Expression "end"
| "switch" Expression ":" SwitchBody "end"
| "(" Expression ")"
| Name
| Name "'"
| "?"
| "self"
;
NonEmptySetExpression : "{" Expressions "}"
;
DictPairs : Expression ":" Expression
| DictPairs "," Expression ":" Expression
;
OptElifExprs : /* empty */
| OptElifExprs "elif" Expressions ":" Expression
;
SwitchBody : SwitchCases
| SwitchCases "else" Expression
| "else" Expression
;
SwitchCases : "case" Expression ":" Expression
| SwitchCases "case" Expression ":" Expression
;
Name : Identifier
| RELATIVENAMETK
| ABSOLUTENAMETK
| ROOTNAMETK
;
///////////////////////////////////////////////////////////////////////////////
OptDoubleAnnos : /* empty */
| OptDoubleAnnos DoubleAnnotation
;
DoubleAnnotation : DOUBLE_ANNOTATION_NAMETK
| DOUBLE_ANNOTATION_NAMETK "(" ")"
| DOUBLE_ANNOTATION_NAMETK "(" AnnotationArgs OptComma ")"
;
OptAnnos : /* empty */
| OptAnnos Annotation
;
Annos : Annotation
| Annos Annotation
;
Annotation : REGULAR_ANNOTATION_NAMETK
| REGULAR_ANNOTATION_NAMETK "(" ")"
| REGULAR_ANNOTATION_NAMETK "(" AnnotationArgs OptComma ")"
;
AnnotationArgs : AnnotationArg
| AnnotationArgs "," AnnotationArg
;
AnnotationArg : IDENTIFIERTK ":" Expression
| RELATIVENAMETK ":" Expression
| Expression
;
OptComma : /* empty */
| ","
;
SupKind : "plant"
| "requirement"
| "supervisor"
;
StdLibFunction : "acosh"
| "acos"
| "asinh"
| "asin"
| "atanh"
| "atan"
| "cosh"
| "cos"
| "sinh"
| "sin"
| "tanh"
| "tan"
| "abs"
| "cbrt"
| "ceil"
| "del"
| "empty"
| "exp"
| "floor"
| "fmt"
| "ln"
| "log"
| "max"
| "min"
| "pop"
| "pow"
| "round"
| "scale"
| "sign"
| "size"
| "sqrt"
| "bernoulli"
| "beta"
| "binomial"
| "constant"
| "erlang"
| "exponential"
| "gamma"
| "geometric"
| "lognormal"
| "normal"
| "poisson"
| "random"
| "triangle"
| "uniform"
| "weibull"
;