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):
- Square brackets (`[]') indicate optional symbols
- Asterisk (`*') denotes any amount repetition (0 or more instances)
- Parentheses (`()') are used for grouping grammar symbols
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:
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
| 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
|
A.2.1.1 Constraint
| constraint:
'(' range ( delim range )* ')'
range:
value
|
'..' value
|
value '..' value
|
value '..'
value:
expr
|
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
|
A.2.3 Place
| place:
PLACE name constraint* typedefinition
[ CONST ] [ ':' marking_list ]
|
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.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.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
|
A.4 Formulae and Expressions
| expr:
formula
marking:
formula
marking_list:
marking ( ',' marking )*
|
A.4.1 Literals
| formula:
TRUE | FALSE
|
NUMBER
|
CHARACTER
|
UNDEFINED | FATAL
|
'#' typereference
|
'<' typereference | '>' typereference
|
name
|
A.4.2 Functions
| formula:
name '()'
|
name '(' arg_list ')'
arg_list:
[ formula ( ',' formula )* ]
|
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
|
A.4.4 Typecasting and Union Values
| formula:
IS typereference formula
|
name '=' formula
|
formula IS name
|
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 ]
|
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
|
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
|
This document was generated
by root on August, 5 2003
using texi2html