[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

# A. The Grammar

This appendix presents the grammar of the Maria languages using a Bison-like Backus-Naur Form (see (bison)Language and Grammar section ‘Languages and Context-Free Grammars’ in The GNU Bison Manual) with the following extensions inspired by regular expressions (see (flex)Patterns section ‘Patterns’ in The Flex Manual):

1. Square brackets (‘`[]`’) indicate optional symbols
2. Asterisk (‘`*`’) denotes any amount repetition (0 or more instances)
3. Parentheses (‘`()`’) are used for grouping grammar symbols

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## A.1 Terminal Symbols

By convention, terminal symbols are written in all-uppercase letters or as character strings enclosed in single quotation marks, and non-terminal symbols are written in all-lowercase letters. The non-trivial terminal symbols used in the grammar are as follows.

‘`NUMBER`’

  decimal (‘`[1-9][0-9]*`’), octal (‘`0[0-7]*`’) or hexadecimal (‘`0x[0-9a-fA-F]+`’)

‘`CHARACTER`’

  ‘`'c'`’: Character Constants

‘`STATE`’

  number of a state in the reachability graph: ‘`@[1-9][0-9]*`’, ‘`@0[0-7]*`’ or ‘`@0x[0-9a-fA-F]+`’

‘`COMP`’

  number of a strongly connected component of (part of) the reachability graph ‘`@@[1-9][0-9]*`’, ‘`@@0[0-7]*`’ or ‘`@@0x[0-9a-fA-F]+`’

‘`name`’

  ‘`[a-zA-Z_][0-9a-zA-Z_]*|"c*"`’: Identifiers

Reserved words are not listed in the above table. For instance, the symbol ‘`PLACE`’ stands for the keyword ‘`place`’.

In addition, there are a few low-level grammar rules that are almost like terminal symbols in their nature:

    delim:
            ','
            |
            ';'

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## A.2 The Net Description Language

    net:
            ( netcomponent ';' )*

    netcomponent:
            type
            |
            function
            |
            place
            |
            transition
            |
            verify
            |
            fairness
            |
            proposition
            |
            subnet

    subnet:
            SUBNET [ name ] '{' net '}'

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

### A.2.1 Type

    type:
            TYPEDEF typedefinition name

    typedefinition:
            ENUM '{' enum_item ( delim enum_item )* '}'
            |
            STRUCT '{' [ comp_list ] '}'
            |
            UNION '{' comp_list '}'
            |
            ID '[' number ']'
            |
            typereference
            |
            typedefinition constraint
            |
            typedefinition '[' typedefinition ']'
            |
            typedefinition '[' QUEUE number ']'
            |
            typedefinition '[' STACK number ']'

    typereference:
            name

    enum_item:
            name [ [ '=' ] number ]

    comp_list:
            comp ( delim comp )* [ delim ]
    comp:
            typedefinition name

    number:
            expr

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

#### A.2.1.1 Constraint

    constraint:
            '(' range ( delim range )* ')'

    range:
            value
            |
            '..' value
            |
            value '..' value
            |
            value '..'

    value:
            expr

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

### A.2.2 Function

    function:
            typereference name eq formula
            |
            typereference name '(' param_list ')' formula

    eq:     '=' | '()'

    param_list:
            [ param_list_item ( delim param_list_item )* ]
    param_list_item:
            typereference name

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

### A.2.3 Place

    place:
            PLACE name constraint* typedefinition
            [ CONST ] [ ':' marking_list ]

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

### A.2.4 Transition

    transition:
            TRANS [ ':' ] name [ '!' ] trans*

    trans:
            '{' [ var_expr ( delim var_expr )* [ delim ] ] '}'
            |
            IN trans_places
            |
            OUT trans_places
            |
            GATE expr ( ',' expr )*

            |
            HIDE expr

            |
            STRONGLY_FAIR expr
            |
            WEAKLY_FAIR expr
            |
            ENABLED expr

            |
            ':' [ TRANS ] name
            |
            NUMBER

    var_expr:
            [ HIDE ] typereference name
            |
            [ HIDE ] typereference name '!' [ '(' expr ')' ]
            |
            function

    trans_places:
            '{' place_marking ( ';' place_marking )* '}'
    place_marking:
            [ PLACE ] name ':' marking_list

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

### A.2.5 State Properties

    verify:
            REJECT expr
            |
            DEADLOCK expr

    fairness:
            STRONGLY_FAIR qual_expr ( ',' qual_expr )*
            |
            WEAKLY_FAIR qual_expr ( ',' qual_expr )*
            |
            ENABLED qual_expr ( ',' qual_expr )*

    proposition:
            PROP name ':' expr

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## A.3 The Query Language

Keywords of the query language are reserved words only in the beginning of a statement. For instance, ‘`eval eval`’ will try to evaluate the symbol ‘`eval`’ in the current state.

    script:
            [ statement ( ';' statement )* [ ';' ] ]

    statement:
            MODEL name
            |
            GRAPH name
            |
            [ VISUAL ] DUMP
            |
            UNFOLD name
            |
            LSTS [ name ]
            |
            [ VISUAL ] DUMPGRAPH
            |
            ( BREADTH | DEPTH ) [ STATE ]
            |
            [ VISUAL ] ( BREADTH | DEPTH ) formula
            |

            [ VISUAL ] [ EVAL ] [ STATE ] formula
            |
            [ VISUAL ] SHOW [ STATE ]
            |
            [ VISUAL ] SHOW STATE STATE ( STATE )*
            |
            HIDE [ '!' ] [ [ PLACE ] name ( ',' [ PLACE ] name )* ]
            |
            [ VISUAL ] ( SUCC | PRED ) [ '!' ] [ STATE ]
            |
            [ GO ] STATE
            |
            [ VISUAL ] [ STATE ] TRANS atrans*

    atrans:
            '{' [ avar_expr ( delim avar_expr )* [ delim ] ] '}'
            |
            IN trans_places
            |
            OUT trans_places
            |
            GATE expr ( ',' expr )*

    avar_expr:
            typereference name
            |
            typereference name '!' [ '(' expr ')' ]

    statement:
            STRONG [ STATE ] [expr]
            |
            TERMINAL
            |
            [ VISUAL ] COMPONENTS
            |
            [ VISUAL ] ( SUCC | PRED ) COMP
            |
            [ VISUAL ] [ SHOW ] COMP [ expr ]
            |

            [ VISUAL ] PATH ( STATE | COMP | expr ) [ STATE ] [ ',' expr ]
            |
            [ VISUAL ] PATH STATE ( COMP | expr ) [ ',' expr ]
            |
            [ VISUAL ] PATH STATE STATE STATE ( STATE )* [ ',' expr ]

            FUNCTION function
            |

            STATS
            |

            TIME
            |

            CD [ name ]
            |
            TRANSLATOR [ name ]
            |
            COMPILEDIR [ name ]
            |
            LOG [ name ]
            |

            PROMPT [ 'c' ]
            |

            HELP
            |
            EXIT

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## A.4 Formulae and Expressions

    expr:
            formula

    marking:
            formula
    marking_list:
            marking ( ',' marking )*

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

### A.4.1 Literals

    formula:
            TRUE | FALSE
            |
            NUMBER
            |
            CHARACTER
            |
            UNDEFINED | FATAL
            |
            '#' typereference
            |
            '<' typereference | '>' typereference
            |
            name

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

### A.4.2 Functions

    formula:
            name '()'
            |
            name '(' arg_list ')'
    arg_list:
            [ formula ( ',' formula )* ]

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

### A.4.3 Basic Formulae

    formula:
            '(' formula ')'
            |
            ATOM formula
            |

            formula '<' formula
            |
            formula '==' formula
            |
            formula '>' formula
            |
            formula '>=' formula
            |
            formula '!=' formula
            |
            formula '<=' formula
            |

            '-' formula
            |
            formula '+' formula
            |
            formula '-' formula
            |
            formula '/' formula
            |
            formula '*' formula
            |
            formula '%' formula
            |

            '|' formula | '+' formula
            |
            '*' formula
            |
            '/' formula | '%' formula
            |
            '~' formula
            |

            formula '<<' formula
            |
            formula '>>' formula
            |
            formula '&' formula
            |
            formula '^' formula
            |
            formula '|' formula
            |

            formula '?' formula ( ':' formula )*
            |

            '{' [ name ':' ] [ expr ] ( ',' [ name ':' ] [ expr ] )* '}'
            |
            formula '.' name
            |
            formula '.' '{' name expr '}'
            |
            formula '[' formula ']'
            |
            formula '.' '{' '[' expr ']' expr '}'
            |

            '!' formula
            |
            formula '&&' formula
            |
            formula '^^' formula
            |
            formula '||' formula
            |
            formula '<=>' formula
            |
            formula '=>' formula

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

### A.4.4 Typecasting and Union Values

    formula:
            IS typereference formula
            |
            name '=' formula
            |
            formula IS name

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

### A.4.5 Non-Determinism and Quantification

    formula:
            typereference [ name ] '!' [ '(' expr ')' ]
            |
            typereference name [ '(' expr ')' ] ':' formula
            |
            typereference name [ '(' expr ')' ] '&&' formula
            |
            typereference name [ '(' expr ')' ] '||' formula
            |
            '.' name [ name ]
            |
            ':' name [ name ]

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

### A.4.6 Multi-Set Operations

    formula:
            EMPTY
            |
            '(' marking_list ')'
            |
            formula '#' marking
            |
            PLACE name
            |

            marking SUBSET marking
            |
            marking INTERSECT marking
            |
            marking MINUS marking
            |
            marking UNION marking
            |
            marking EQUALS marking
            |

            CARDINALITY marking
            |
            MAX marking
            |
            MIN marking
            |

            SUBSET name '{' marking_list '}' expr
            |
            MAP name '{' marking_list '}' expr
            |
            MAP name '#' name '{' marking_list '}' marking

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

### A.4.7 Temporal Logic

            '<>' formula
            |
            '[]' formula
            |
            '()' formula
            |
            formula UNTIL formula
            |
            formula RELEASE formula

    qual_expr:
            TRANS name [ ':' expr ]
            |
            '(' qual_expr ')'
            |

            '!' qual_expr
            |

            qual_expr '&&' qual_expr
            |

            qual_expr '^^' qual_expr
            |

            qual_expr '||' qual_expr
            |

            qual_expr '<=>' qual_expr
            |
            qual_expr '=>' qual_expr

[ << ] | [ >> ] |  |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

This document was generated on January 22, 2026 using texi2html 1.82.