[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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):
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] | [ ? ] |
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.
decimal (‘[1-9][0-9]*’), octal (‘0[0-7]*’) or hexadecimal (‘0x[0-9a-fA-F]+’)
‘'c'’: Character Constants
number of a state in the reachability graph: ‘@[1-9][0-9]*’, ‘@0[0-7]*’ or ‘@0x[0-9a-fA-F]+’
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]+’
‘[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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
constraint: '(' range ( delim range )* ')' range: value | '..' value | value '..' value | value '..' value: expr |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
formula: TRUE | FALSE | NUMBER | CHARACTER | UNDEFINED | FATAL | '#' typereference | '<' typereference | '>' typereference | name |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
formula: name '()' | name '(' arg_list ')' arg_list: [ formula ( ',' formula )* ] |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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] | [ ? ] |
formula: IS typereference formula | name '=' formula | formula IS name |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
formula: typereference [ name ] '!' [ '(' expr ')' ] | typereference name [ '(' expr ')' ] ':' formula | typereference name [ '(' expr ')' ] '&&' formula | typereference name [ '(' expr ')' ] '||' formula | '.' name [ name ] | ':' name [ name ] |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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] | [ ? ] |
'<>' 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.