ltl2tgta

ltl2tgta was a tool introduced in Spot 1.0 to generates various forms of Testing Automata, i.e., automata that observe the changes of atomic propositions, not their values.

For more details, read Model checking using generalized testing automata, Ala Eddine Ben Salem, Alexandre Duret-Lutz, and Fabrice Kordon, in Transactions on Petri Nets and Other Models of Concurrency (ToPNoC VI), LNCS 7400, p. 94–112, 2012.

The code supporting this tool had some minimal update for Spot 2.0, but was still the least tested/covered code in the whole project, and required regular touch-ups to accommodate new compiler versions. Since it had no known uses (outside of a few publication about testing automata), we removed it from Spot to lower the maintenance burden. If you are interested in testing automata, and want to try this tool, please download a version prior to Spot 2.15. You are also welcome to get in touch and make a case for the reintegration of this tool.