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

A. The Grammar

This appendix presents the grammar of the Maria languages using a Bison-like Backus-Naur Form (see section `Languages and Context-Free Grammars' in The GNU Bison Manual) with the following extensions inspired by regular expressions (see 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'': 1.2.3.3 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*"': 1.2.3.4 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 January, 13 2005 using texi2html