MOML Grammar
============

This is the full abstract grammar of MOML:


.. code-block:: bnf

    <model> ::=
        | [<model-type>] <specification>*


    <model-type> ::=
        | ‘model_type’ MODEL-TYPE


    <specification> ::=
        | <metadata-definition>
        | <variable-declaration>
        | <constant-declaration>
        | <action-declaration>
        | <automaton-definition>
        | <network-definition>
        | <property-definition>

    <metadata-definition> ::=
        | ‘metadata’ ‘:’ INDENT <metadata-field>* DEDENT

    <variable-declaration> ::=
        | [‘transient’] ‘variable’ IDENTIFIER ‘:’ <type> [‘:=’ <expression>] [<comment>]

    <constant-declaration> ::=
        | ‘constant’ IDENTIFIER ‘:’ <type> [‘:=’ <expression>] [<comment>]

    <action-declaration> ::=
        | ‘action’ IDENTIFIER [‘(’ [<action-parameter> [(‘,’ <action-parameter>)+]] ‘)’] [<comment>]

    <automaton-definition> ::=
        | ‘automaton’ IDENTIFIER ‘:’ INDENT <automaton-specification>* DEDENT

    <network-definition> ::=
        | ‘network’ [IDENTIFIER] ‘:’ INDENT <network-specification>* DEDENT

    <property-definition> ::=
        | ‘property’ IDENTIFIER ‘:=’ <property> [<comment>]


    <metadata-field> ::=
        | <string> ‘:’ <string>


    <action-parameter> ::=
        | <type> [<comment>]


    <automaton-specification> ::=
        | <variable-declaration>
        | <location-definition>
        | <edge-definition>

    <network-specification> ::=
        | <instance-definition>
        | <restrict-initial>
        | <composition>


    <location-definition> ::=
        | [‘initial’] ‘location’ IDENTIFIER [‘:’ INDENT <location-specification>* DEDENT]

    <location-specification> ::=
        | ‘invariant’ <expression>
        | <assignment>


    <edge-definition> ::=
        | ‘edge’ ‘from’ IDENTIFIER ‘:’ INDENT <edge-specification>* DEDENT

    <edge-specification> ::=
        | ‘action’ IDENTIFIER
        | ‘guard’ <expression> [<comment>]
        | ‘rate’ <expression> [<comment>]
        | ‘to’ IDENTIFIER [‘:’ INDENT <destination-specification>* DEDENT]

    <destination-specification> ::=
        | ‘probability’ <expression> [<comment>]
        | <assignment>

    <assignment> ::=
        | ‘assign’ [/\d+/] IDENTIFIER ‘:=’ <expression>


    <instance-definition> ::=
        | ‘instance’ IDENTIFIER IDENTIFIER [‘:’ INDENT <instance-specification>* DEDENT]

    <instance-specification> ::=
        | ‘input’ ‘enable’ IDENTIFIER [‘,’ IDENTIFIER]


    <restrict-initial> ::=
        | ‘restrict’ ‘initial’ <expression>


    <composition> ::=
        | ‘composition’ IDENTIFIER [‘|’ IDENTIFIER] [‘:’ INDENT <composition-specification>* DEDENT]

    <composition-specification> ::=
        | ‘synchronize’ <action-pattern> [(‘|’ <action-pattern>)+] (‘->’ | ‘→’) <action-pattern>

    <action-pattern> ::=
        | IDENTIFIER [‘(’ [IDENTIFIER [(‘,’ IDENTIFIER)+]] ‘)’]
        | ‘-’ | ‘τ’


    <expression> ::=
        | <constant>
        | IDENTIFIER ‘(’ [<expression> [‘,’ <expression>]] ‘)’
        | IDENTIFIER
        | <unary-operator> <expression>
        | <expression> <binary-operator> <expression>
        | <expression> ‘?’ <expression> ‘:’ <expression>

    <constant> ::=
        | ‘true’ | ‘false’
        | /[0-9]+/ ‘.’ /[0-9]+/ | ‘real[’ <NAMED-REAL> ‘]’
        | /[0-9]+/

    <unary-operator> ::=
        | ‘¬’ | ‘not’

    <binary-operator> ::=
        | ‘∨’ | ‘or’
        | ‘∧’ | ‘and’
        | ‘⊕’ | ‘xor’
        | ‘⇒’ | ‘==>’
        | ‘⇔’ | ‘<=>’
        | ‘=’ | ‘!=’ | ‘≠’
        | ‘<’ | ‘≤’ | ‘≥’ | ‘>’
        | ‘+’ | ‘-’ | ‘*’ | ‘%’
        | ‘/’ | ‘//’


    <property> ::=
        | <expression>
        | … TODO …


    <comment> ::=
        | ‘"’ /([^"]|\")/ ‘"’


    <string> ::=
        | ‘"’ /([^"]|\")/ ‘"’


    <type> ::=
        | <primitive-type>
        | <bounded-type>
        | <array-type>

    <primitive-type> ::=
        | ‘bool’
        | <numeric-type>

    <numeric-type> ::=
        | ‘int’
        | ‘real’
        | ‘clock’
        | ‘continuous’

    <bounded-type> ::=
        | <numeric-type> ‘[’ <expression> ‘,’ <expression> ‘]’

    <array-type> ::=
        | <type> ‘[]’


If the model type is omitted the file must not contain anything else than property definitions.
This allows to separate property and model definitions.