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"
               ;