Maria relies on external programs translating LTL formulae into generalised Büchi automata or finite-word automata. It communicates with these programs by writing a formula to the standard input of the translator and by reading the translated automaton from the standard output of the translator. Each formula is translated in a separate run of the external program. The program is invoked without arguments.
The grammars are presented in Backus-Naur Form, one grammar rule per line. Comments delimited by the symbols /* and */ are not part of the formal grammar. Non-terminal symbols are enclosed within single quotes or presented as Flex-style regular-expressions.
Currently, Maria does not make use of the implication, equivalence or exclusive disjunction operators, but they might be generated in the future.
| <f> ::= | 't' |
/* true */ |
| <f> ::= | 'f' |
/* false */ |
| <f> ::= | 'p'[0-9]+ |
/* proposition */ |
| <f> ::= | '!'
<f> |
/* negation */ |
| <f> ::= | '|'
<f>
<f> |
/* disjunction */ |
| <f> ::= | '&'
<f>
<f> |
/* conjunction */ |
| <f> ::= | 'i'
<f>
<f> |
/* implication:
"i <f1> <f2>" is short-hand for
"| ! <f1> <f2>" */ |
| <f> ::= | 'e'
<f>
<f> |
/* equivalence */ |
| <f> ::= | '^'
<f>
<f> |
/* exclusive disjunction (xor) */ |
| <f> ::= | [ \t\n\r\v\f] <f> |
/* white space is ignored */ |
| <f> ::= | <f> [ \t\n\r\v\f] |
/* white space is ignored */ |
| <f> ::= | 'X'
<f> |
/* next */ |
| <f> ::= | 'F'
<f> |
/* finally, eventually */ |
| <f> ::= | 'G'
<f> |
/* globally, henceforth */ |
| <f> ::= | 'U'
<f>
<f> |
/* until */ |
| <f> ::= | 'V'
<f>
<f> |
/* release */ |
The same grammar is used for both finite automata (safety properties) and for generalised Büchi automata (liveness properties). A finite automaton has zero acceptance sets and exactly one final state that does not have any successor states. A generalised Büchi automaton has no final state. If the number of acceptance sets of a generalised Büchi automaton is zero, this means that the automaton has one acceptance set to which all states belong.
| <automaton> ::= | [0-9]+ <space>
[0-9]+
<states>
|
/* first the number of states, then the number of acceptance sets (if the latter is 0, it is a generalised Büchi automaton whose all states accept, or a finite automaton) */ |
| <space> ::= | [ \n]+ |
|
| <states> ::= | /* empty */ | |
| <states> ::= | <states> <space> <state> | |
| <state> ::= | [0-9]+ <space>
<finitial?> <space>
<acceptance sets> '-1'
<transitions> '-1' |
/* state identifiers can be arbitrary unsigned integers */ |
| <finitial?> ::= | '0' |
/* not an initial or a final state */ |
| <finitial?> ::= | '1' |
/* initial state (exactly one state must be initial) */ |
| <finitial?> ::= | '2' |
/* final state (exactly one state must be final for finite automata) */ |
| <acceptance sets> ::= | /* empty */ | |
| <acceptance sets> ::= | <acceptance sets>
[0-9]+ <space> |
/* acceptance set identifiers can be arbitrary unsigned integers */ |
| <transitions> ::= | /* empty */ | |
| <transitions> ::= | <transitions> <space> <transition> | |
| <transition> ::= | [0-9]+ <space>
't' |
/* constantly enabled transition to a state */ |
| <transition> ::= | [0-9]+ <space>
<gate> |
/* conditionally enabled transition to a state */ |
| <gate> ::= | 'p'[0-9]+ |
/* proposition */ |
| <gate> ::= | '!' <space>
<gate> |
/* negation */ |
| <gate> ::= | '|' <space>
<gate> <space>
<gate> |
/* disjunction */ |
| <gate> ::= | '&' <space>
<gate> <space>
<gate> |
/* conjunction */ |
Maria maps the state numbers in the property automata to a
contiguous sequence. If you want to see the automata after this
mapping, define the preprocessor symbol DEBUG_AUTOMATON
when compiling the file Property.C. In that way, Maria
will dump the mapped automaton to the standard output. The automaton
can be visualised with the lbt2dot tool of LBT.
To grab the formula sent by Maria to the external translator, write
a wrapper shell script for the translator that does something like
tee formula.txt | exec the-real-translator.