`ltl2tgta`

This tool generates various form of Testing Automata, i.e., automata
that observe the *changes* of atomic propositions, not their values.

Three types of automata can be output. The only output format
supported currently is GraphViz's format, with option `-8`

to enable
UTF-8 characters as in other tools.

The `--ta`

option will translate a formula into Testing Automaton, as
described by Geldenhuys and Hansen (Spin'06).

Here is the output on `a U Gb`

(we omit the call to `dot`

, as shown while
discussing `ltl2tgba`

).

```
ltl2tgta --ta --multiple-init 'a U Gb'
```

As always, the labels of the states have no influence on the language
recognized by the automaton. This automaton has three possible
initial states. The initial state should be chosen depending on the
initial valuation of `a`

and `b`

in the system to be synchronized with
this testing automaton. For instance if `a`

is true and `b`

false in
the initial state, the testing automaton should start in the state
pointed to by the initial arrow labeled `a & !b`

. In the rest of the
testing automaton, the transitions are labeled by the sets of atomic
propositions that should change in the system for the testing
automaton to progress. States with a double enclosure are Büchi
accepting, meaning that any execution that visits one of these states
is accepting. All states have an implicit self-loop labeled by `{}`

:
if the system progress without changing the value of `a`

and `b`

, the
testing automaton remains in the same state. Rectangle states are
livelock-accepting: any execution of the system that get stuck into
one of these state is accepting.

Without the `--multiple-init`

option, a fake initial state is added.
This is the default since it often makes the result more readable.

```
ltl2tgta --ta 'a U Gb'
```

digraph G { 0 [label="", style=invis, height=0] 0 -> 1 1 [label=init] 1 -> 2 [label="!a & b\n"] 1 -> 3 [label="a & b\n"] 1 -> 4 [label="a & !b\n"] 2 [label="2",shape=box] 2 -> 5 [label="{a}\n"] 3 [label="3",shape=box] 3 -> 5 [label="{a}\n"] 3 -> 2 [label="{a}\n"] 3 -> 4 [label="{b}\n"] 4 [label="1"] 4 -> 3 [label="{b}\n"] 4 -> 2 [label="{a, b}\n"] 5 [label="4",peripheries=2,shape=box] 5 -> 5 [label="{a}\n{0}"] }

The `--gba`

option can be used to request a Generalized Testing
Automaton, i.e., a Testing Automaton with Generalized Büchi
acceptance. In that case double-enclosures are not used anymore, and
Büchi accepting transitions are marked with the same `{0,1}`

notation used in TGBA.

```
ltl2tgta --gta 'GFa & GFb'
```

digraph G { 0 [label="", style=invis, height=0] 0 -> 1 1 [label=init] 1 -> 2 [label="a & b\n"] 1 -> 3 [label="!a & b\n"] 1 -> 4 [label="a & !b\n"] 1 -> 5 [label="!a & !b\n"] 2 [label="1",shape=box] 2 -> 3 [label="{a}\n{0,1}"] 2 -> 4 [label="{b}\n{0,1}"] 2 -> 5 [label="{a, b}\n{0,1}"] 3 [label="3"] 3 -> 2 [label="{a}\n{1}"] 3 -> 4 [label="{a, b}\n{1}"] 3 -> 5 [label="{b}\n{1}"] 4 [label="2"] 4 -> 2 [label="{b}\n{0}"] 4 -> 3 [label="{a, b}\n{0}"] 4 -> 5 [label="{a}\n{0}"] 5 [label="4"] 5 -> 2 [label="{a, b}\n"] 5 -> 3 [label="{b}\n"] 5 -> 4 [label="{a}\n"] }

The interpretation is similar to that of the TA. Execution that
stutter in a livelock-accepting (square) state are accepting as well
as execution that visit the `0`

and `1`

acceptance sets
infinitely often. Those acceptance sets are carried by transitions,
as in TGBAs.

Finally, the default is to output a Transition-based Generalized
Testing Automaton ^{1}. In TGTAs, the stuttering states are
made explicit with `{}`

self-loops. Since these self-loop can be in
acceptance sets, livelock acceptance states are no longer needed.

```
ltl2tgta 'GFa & GFb'
```

digraph G { 0 [label="", style=invis, height=0] 0 -> 1 1 [label=init] 1 -> 2 [label="a & b\n"] 1 -> 3 [label="!a & b\n"] 1 -> 4 [label="a & !b\n"] 1 -> 5 [label="!a & !b\n"] 2 [label="3"] 2 -> 3 [label="{a}\n{0,1}"] 2 -> 4 [label="{b}\n{0,1}"] 2 -> 5 [label="{a, b}\n{0,1}"] 2 -> 2 [label="{}\n{0,1}"] 3 [label="2"] 3 -> 2 [label="{a}\n{1}"] 3 -> 4 [label="{a, b}\n{1}"] 3 -> 5 [label="{b}\n{1}"] 3 -> 3 [label="{}\n"] 4 [label="4"] 4 -> 2 [label="{b}\n{0}"] 4 -> 3 [label="{a, b}\n{0}"] 4 -> 5 [label="{a}\n{0}"] 4 -> 4 [label="{}\n"] 5 [label="1"] 5 -> 2 [label="{a, b}\n"] 5 -> 3 [label="{b}\n"] 5 -> 4 [label="{a}\n"] 5 -> 5 [label="{}\n"] }

## Footnotes:

^{1}

: This new class of automaton, as well as the implementation of the previous testing automata classes, is part of Ala Eddine BEN SALEM's PhD work, and should appear in a future edition of ToPNoC (LNCS 7400).