6.3 Output file format for automata

lbtt expects the Büchi automata generated by each LTL-to-Büchi translator implementation to be in the format specified below. The format encodes a generalized Büchi automaton (a Büchi automaton with zero or more acceptance conditions) with a single initial state and labels (guards) on transitions. For the full formal definition and examples on how to reduce other definitions into the one used by lbtt, see Definitions.

The output file generated by the translator should contain an automaton described using the following grammar (as before, quoted characters denote the characters themselves, sp denotes any nonempty string of white space, lines containing a // are comments that are not part of the grammar, and `\n' corresponds to the newline character).

     automaton  ::=  num-states sp cond-specifier state-list
     
     num-states  ::=  [0---9]+
     
     cond-specifier  ::=  [0---9]+[st]*
     
     state-list  ::=  state-list sp state
                   |  // empty

The automaton description begins with a nonnegative number that gives the number of states in the automaton. If the number of states is 0, the automaton will not accept any input. If the number is positive, it should be followed by a cond-specifier that determines the number and placement of acceptance conditions in the automaton. If the number of acceptance conditions is 0, the automaton accepts an input word if and only if it has a run on that word according to the definition given in the Appendix (see Definitions).

The placement of acceptance conditions is specified by concatenating a string formed from the symbols `s' and `t' to the number of acceptance conditions (with no white space in between). The interpretation of this string is as follows:

• If the string is empty or does not include the symbol `t', the acceptance conditions of the automaton are placed exclusively on its states. (This alternative corresponds to the definition supported by lbtt 1.0.x.)
• If the string is nonempty but does not include the symbol `s', the automaton has acceptance conditions exclusively on its transitions.
• Otherwise, the automaton has acceptance conditions on both states and transitions.

The cond-specifier is followed by a list of the descriptions of states in the automaton. The format of this list is affected by the choice of the placement of the acceptance conditions. More precisely, the choice affects the interpretation of the cond-list nonterminal symbol in the following fragment of the grammar: we indicate this by prefixing the nonterminal with either “<s>” or “<t>” to denote that the list (together with its terminating `-1') should be omitted in automata that do not associate acceptance conditions with states or transitions, respectively.

     state  ::=  state-id sp initial? <s>cond-list transition-list
     
     state-id  ::=  [0---9]+
     
     initial?  ::=  `0'  |  `1'
     
     cond-list  ::=  sp acceptance-condition-id cond-list
                  |  sp `-1'
     
     acceptance-condition-id  ::=  [0---9]+
     
     transition-list  ::=  sp transition transition-list
                        |  sp `-1'
     
     transition  ::=  state-id <t>cond-list sp guard-formula `\n'
     
     guard-formula  ::=  `t'
                                                  // ``true''
                      |  `f'
                                                  // ``false''
                      |  `p'[0---9]+
                                                  // atomic proposition
                      |  `!' sp guard-formula
                                                  // negation
                      |  `&' sp guard-formula sp guard-formula
                                                  // conjunction
                      |  `|' sp guard-formula sp guard-formula
                                                  // disjunction
                      |  `i' sp guard-formula sp guard-formula
                                                  // implication
                      |  `e' sp guard-formula sp guard-formula
                                                  // equivalence
                      |  `^' sp guard-formula sp guard-formula
                                                  // exclusive or

The description of each state begins with a numeric state identifier, which can be any nonnegative integer. The state identifier should be followed by a number telling whether the state is initial (`1' if yes). The automaton should have exactly one initial state. If the automaton has acceptance conditions associated with its states, this number should then be followed by a list of acceptance condition identifiers separated by white space. This list should be terminated with `-1'.

The state description should be followed by the list of transitions starting from the state (terminated again by `-1'). Each transition consists of a state identifier (the target state of the transition), a list of acceptance condition identifiers (if the automaton has acceptance conditions on transitions), and a propositional formula ¹ that encodes the symbols of the alphabet 2^AP (where AP is a finite set of atomic propositions) on which the automaton is allowed to take the transition. The propositional formula should be terminated with a newline.

The state and acceptance condition identifiers need not be successive, and the states or acceptance conditions can be listed in any order. The only restrictions are that the identifiers of different states and acceptance conditions should be unique and that the total number of different identifiers should equal num-states or num-conds, respectively. (The same identifiers can be shared between states and acceptance conditions, however.)

Note that the output file should always contain a valid automaton description if the LTL-to-Büchi translation was successful, even in the case that the resulting automaton is empty (lbtt interprets a missing automaton description file as an error).

The following examples illustrate the file format. The first example gives the description of an automaton with acceptance conditions on states. Note that in this case the `s' is optional for describing the placement of acceptance conditions; therefore, the automaton files used with lbtt 1.0.x are upwards compatible with newer versions of the tool (provided that each guard of a transition is terminated by a newline).

     6 2s         // an automaton with six states and two acc. conditions on states
     0 1 -1       // state 0: initial state, no acceptance conditions
     2 p1         //     transition to state 2, guard `p1'
     5 p2         //     transition to state 5, guard `p2'
     15 p3        //     transition to state 15, guard `p3'
     -1           // end of state 0
     2 0 1 -1     // state 2: non-initial state, acceptance condition 1
     2 p1         //     transition to state 2, guard `p1'
     5 p2         //     transition to state 5, guard `p2'
     15 p3        //     transition to state 15, guard `p3'
     -1           // end of state 2
     5 0 0 -1     // state 5: non-initial state, acceptance condition 0
     5 p2         //     transition to state 5, guard `p2'
     8 & p1 p2    //     transition to state 8, guard `p1 /\ p2'
     12 & p1 p3   //     transition to state 12, guard `p1 /\ p3'
     15 p3        //     transition to state 15, guard `p3'
     -1           // end of state 5
     8 0 0 -1     // state 8: non-initial state, acceptance condition 0
     5 p2         //     transition to state 5, guard `p2'
     8 & p1 p2    //     transition to state 8, guard `p1 /\ p2'
     12 & p1 p3   //     transition to state 12, guard `p1 /\ p3'
     15 p3        //     transition to state 15, guard `p3'
     -1           // end of state 8
     15 0 1 0 -1  // state 15: non-initial state, acceptance conditions 1 and 0
     2 p1         //     transition to state 2, guard `p1'
     5 p2         //     transition to state 5, guard `p2'
     15 p3        //     transition to state 15, guard `p3'
     -1           // end of state 15
     12 0 1 0 -1  // state 12: non-initial state, acceptance conditions 1 and 0
     2 p1         //     transition to state 2, guard `p1'
     5 p2         //     transition to state 5, guard `p2'
     15 p3        //     transition to state 15, guard `p3'
     -1           // end of state 12

The following example illustrates an automaton in which acceptance conditions are placed on transitions.

     4 3t         // four states, three acceptance conditions on transitions
     5 0          // state 5: non-initial state
     84 0 -1 p1   //     transition to state 84, condition 0, guard `p1'
     27 0 -1 & p1 ! p2 // tr. to state 27, condition 0, guard `p1 /\ ! p2'
     5 -1 t       //     transition to state 5, no conditions, guard `true'
     -1           // end of state 5
     84 1         // state 84: initial state
     5 1 -1 t     //     transition to state 5, condition 1, guard `true'
     27 0 -1 p1   //     transition to state 27, condition 0, guard `p1'
     -1           // end of state 84
     49 0         // state 49: non-initial state
     5 -1 t       //     transition to state 5, no conditions, guard `true'
     49 1 4 -1 & p1 ! p2 // tr. to state 49, conds. 1 and 4, guard `p1 /\ ! p2'
     84 -1 p1     //     transition to state 84, no conditions, guard `p1'
     -1           // end of state 49
     27 0         // state 27: non-initial state
     49 -1 & p1 p3 //    transition to state 49, no conds., guard `p1 /\ p3'
     -1           // end of state 27

Automata with acceptance conditions on both states and transitions can be specified using a combination of the above two formats, that is, by using `st' as the acceptance condition placement specifier and including a list of acceptance conditions both after the value determining the initialness of a state, and after the identifier of the target state of each transition.