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 : GroupBody
;
GroupBody : OptGroupDecls
;
AutomatonBody : OptAutDecls Locations OptIoDecls
;
OptGroupDecls : /* empty */
| OptGroupDecls GroupDecl
;
GroupDecl : Decl
| "import" Imports ";"
| "namespace" IDENTIFIERTK ";"
| "namespace" RELATIVENAMETK ";"
| "func" Types Identifier FuncParams ":" FuncBody
| Identifier ":" Name CompInstArgs ";"
| "group" "def" Identifier CompDefParms ":" GroupBody "end"
| OptSupKind "automaton" "def" Identifier CompDefParms ":" AutomatonBody "end"
| SupKind "def" Identifier CompDefParms ":" AutomatonBody "end"
| "group" Identifier ":" GroupBody "end"
| OptSupKind "automaton" Identifier ":" AutomatonBody "end"
| SupKind Identifier ":" AutomatonBody "end"
;
OptAutDecls : /* empty */
| OptAutDecls AutDecl
;
AutDecl : Decl
| "alphabet" Events ";"
| "alphabet" ";"
| "monitor" Events ";"
| "monitor" ";"
| "disc" Type DiscDecls ";"
;
Decl : "type" TypeDefs ";"
| "enum" Identifier "=" Identifiers ";"
| OptControllability "event" Identifiers ";"
| OptControllability "event" EventType Identifiers ";"
| Controllability Identifiers ";"
| Controllability EventType Identifiers ";"
| "const" Type ConstantDefs ";"
| "alg" Type AlgVarsDefs ";"
| OptAnnos "input" Type Identifiers ";"
| "cont" ContDecls ";"
| "equation" Equations ";"
| "initial" Expressions ";"
| InvariantDecls
| "marked" Expressions ";"
| IoDecl
;
Identifier : 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 : Type Identifiers
| FuncParamDecls ";" Type Identifiers
;
FuncBody : FuncVarDecls FuncStatements "end"
| StringToken ";"
;
FuncVarDecls : /* empty */
| FuncVarDecls 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 : OptAnnos "location" ";"
| OptAnnos "location" Identifier ";"
| OptAnnos "location" ":" LocationElements
| OptAnnos "location" Identifier ":" LocationElements
;
LocationElements : LocationElement
| LocationElements LocationElement
;
LocationElement : "initial" ";"
| "initial" Expressions ";"
| InvariantDecls
| "equation" Equations ";"
| "marked" ";"
| "marked" Expressions ";"
| "urgent" ";"
| "edge" CoreEdge ";"
| "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
| "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 : Identifier
| Identifier Projections
| "(" Addressable "," Addressables ")"
;
Projections : Projection
| Projections Projection
;
Projection : "[" Expression "]"
;
OptElifUpdates : /* empty */
| OptElifUpdates "elif" Expressions ":" Updates
;
OptElseUpdate : /* empty */
| "else" Updates
;
Identifiers : Identifier
| Identifiers "," Identifier
;
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 ";"
;
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
;
///////////////////////////////////////////////////////////////////////////////
OptAnnos : /* empty */
| OptAnnos Annotation
;
Annotation : ANNOTATIONNAMETK
| ANNOTATIONNAMETK "(" ")"
| ANNOTATIONNAMETK "(" AnnotationArgs OptComma ")"
;
AnnotationArgs : AnnotationArg
| AnnotationArgs "," AnnotationArg
;
AnnotationArg : IDENTIFIERTK "=" Expression
| RELATIVENAMETK "=" 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"
;