[ < ] [ > ]   [ << ] [ 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 by root on November 22, 2009 using texi2html 1.82.