[ < ] [ > ]   [ << ] [ 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
A.1 Terminal Symbols   Terminal symbols used in the grammars
A.2 The Net Description Language   The net description language
A.3 The Query Language   The query language
A.4 Formulae and Expressions  
[ < ] [ > ]   [ << ] [ 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 '}'
A.2.1 Type   Data type definitions
A.2.1.1 Constraint   Constraints of data types
A.2.2 Function   Function definitions
A.2.3 Place   Place definitions
A.2.4 Transition   Transition definitions
A.2.5 State Properties   State properties
[ < ] [ > ]   [ << ] [ 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 ]
A.2.1.1 Constraint   ‘constraint’
A.2.1 Type   ‘typedefinition’
A.4 Formulae and Expressions   ‘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
A.2.1 Type   ‘typedefinition’
A.2.2 Function   ‘function’
A.4 Formulae and Expressions   ‘expr’, ‘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
A.4 Formulae and Expressions   ‘marking_list’, ‘formula’
[ < ] [ > ]   [ << ] [ 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 )*
A.4.1 Literals  
A.4.2 Functions   Function calls
A.4.3 Basic Formulae   Syntax for basic formulae
A.4.4 Typecasting and Union Values   Syntax related with unions and type casting
A.4.5 Non-Determinism and Quantification   Non-determinism and quantification
A.4.6 Multi-Set Operations   Multi-set operations
A.4.7 Temporal Logic   Temporal logic
[ < ] [ > ]   [ << ] [ 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 December 1, 2016 using texi2html 1.82.