This text format is used to read and write TGBA. It can be loaded as a tgba_explicit automaton using the spot::tgba_parse() function.
Here is a sample automaton using this format:
acc = p2 "p3"; s1, s2, "!a & b", p2; s2, "s3", "a & !b", p3 p2; s3, s1, "true",;
This describes an automaton with two acceptance sets p2 and p3. There are three states (s1, s2, s3) and three transitions. The first transition is going between s1 and s2 is guarded by !a & b and belongs to the acceptance set p2. The second goes between s2 and s3 with a & !b as guard and belongs to p3 and p2. The last one links s3 back to s1, accepts any input, and is not in any acceptance set.
2. More formally...
This text format has two parts. It begins with an optional declaration of acceptance sets, and is followed by a list of transition specifications.
Inside double-quoted string, a double quote can be represented with \", and a backslash can be represented with \\.
An identifier is either a word matching [a-zA-Z][a-zA-Z0-9_]*, or a double-quoted string.
The optional acceptance set declaration should begin with acc =, followed by a possibly empty space-delimited list of identifiers, and terminated by a semicolon. This declaration can be omitted if the list is empty.
Each transition specification is made of four coma-separated items and is terminated by a semicolon. The first two items are identifiers labeling respectively the input and the output states of the transition. The third is a double-quoted string (it is necessarily doubly quoted) that contains a propositional formula (using the LtlSyntax, but without temporal operators). The last item is a space-separated list of identifiers designating acceptance sets the transition belongs to.
Acceptance sets must be declared before they are used in transition specifications. This is not the case for states, which are created as needed by the transition specifications.