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 ActualParms ";"
          | "group"                "def" Identifier FormalParms ":" GroupBody     "end"
          | OptSupKind "automaton" "def" Identifier FormalParms ":" AutomatonBody "end"
          |    SupKind             "def" Identifier FormalParms ":" 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 "}" ";"
     | "enum" Identifier "=" Identifiers ";"
     | OptControllability "event"           Identifiers ";"
     | OptControllability "event" EventType Identifiers ";"
     |    Controllability                   Identifiers ";"
     |    Controllability         EventType Identifiers ";"
     | "const" Type ConstantDefs ";"
     | "alg" Type AlgVarsDefs ";"
     | "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 : "location" ";"
         | "location" Identifier ";"
         | "location" ":" LocationElements
         | "location" Identifier ":" LocationElements
         ;

LocationElements : LocationElement
                 | LocationElements LocationElement
                 ;

LocationElement : "initial" ";"
                | "initial" Expressions ";"
                | InvariantDecls
                | "equation" Equations ";"
                | "marked" ";"
                | "marked" Expressions ";"
                | "urgent" ";"
                | "edge" CoreEdge ";"
                | "edge" CoreEdge "goto" Identifier ";"
                ;

ActualParms : "(" ")"
            | "(" Expressions ")"
            ;

FormalParms : "(" ")"
            | "(" FormalDecls ")"
            ;

FormalDecls : FormalDeclaration
            | FormalDecls ";" FormalDeclaration
            ;

FormalDeclaration : 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
          | Name                  "needs"    Expression
          | NonEmptySetExpression "needs"    Expression
          | 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
     ;

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