The property automaton translator interface

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.

Grammar Definitions

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.

Output format for LTL formulae

Currently, Maria does not make use of the implication, equivalence or exclusive disjunction operators, but they might be generated in the future.

Propositional operators

<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 */

Temporal operators

<f> ::= 'X' <f> /* next */
<f> ::= 'F' <f> /* finally, eventually */
<f> ::= 'G' <f> /* globally, henceforth */
<f> ::= 'U' <f> <f> /* until */
<f> ::= 'V' <f> <f> /* release */

Input format for automata

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 */

Hints for Debugging

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.