`ltldo`

## Table of Contents

This tool is a wrapper for tools that read LTL/PSL formulas and (optionally) output automata.

It reads formulas specified using the common options for specifying
input and passes each formula to a tool (or a list of tools) specified
using options similar to those of `ltlcross`

. In case that tool
returns an automaton, the resulting automaton is read back by `ltldo`

and is finally output as specified using the common options for
outputing automata.

In effect, `ltldo`

wraps the I/O interface of the Spot tools on top of
any other tool.

## Example: computing statistics for `ltl3ba`

As a motivating example, consider a scenario where we want to run
`ltl3ba`

on a set of 10 formulas stored in a file. For each formula
we would like to compute compute the number of states and edges in the
Büchi automaton produced by `ltl3ba`

.

Here is the input file:

cat >sample.ltl <<EOF 1 1 U a !(!((a U Gb) U b) U GFa) (b <-> Xc) xor Fb FXb R (a R (1 U b)) Ga G(!(c | (a & (a W Gb))) M Xa) GF((b R !a) U (Xc M 1)) G(Xb | Gc) XG!F(a xor Gb) EOF

We will first implement this scenario without `ltldo`

.

A first problem that the input is not in the correct syntax: although
`ltl3ba`

understands `G`

and `F`

, it does not support `xor`

or `M`

,
and requires the Boolean operators `||`

and `&&`

. This syntax
issue can be fixed by processing the input with `ltlfilt -s`

.

A second problem is that `ltl3ba`

(at least version 1.1.1) can only
process one formula at a time. So we'll need to call `ltl3ba`

in a
loop.

Finally, one way to compute the size of the resulting Büchi automaton
is to pipe the output of `ltl3ba`

through `autfilt`

.

Here is how the shell command could look like:

ltlfilt -F sample.ltl -s | while read f; do ltl3ba -f "$f" | autfilt --stats="$f,%s,%t" done

true,1,1 true U a,2,4 !(!((a U []b) U b) U []<>a),2,4 !((b <-> Xc) <-> <>b),7,21 <>Xb V (a V (true U b)),6,28 []a,1,1 [](Xa U (Xa && !(c || (a && [](a || []b))))),1,0 []<>((b V !a) U <>Xc),2,4 [](Xb || []c),3,11 X[]!<>!(a <-> []b),4,10

Using `ltldo`

the above command can be reduced to this:

ltldo 'ltl3ba -f %s>%O' -F sample.ltl --stats='%f,%s,%t'

1,1,1 1 U a,2,4 !(!((a U Gb) U b) U GFa),2,4 (b <-> Xc) xor Fb,7,21 FXb R (a R (1 U b)),6,28 Ga,1,1 G(!(c | (a & (a W Gb))) M Xa),1,0 GF((b R !a) U (Xc M 1)),2,4 G(Xb | Gc),3,11 XG!F(a xor Gb),4,10

Note that the formulas look different in both cases, because in the
`while`

loop the formula printed has already been processed with
`ltlfilt`

, while `ltldo`

emits the input string untouched.

In fact, as we will discuss below, `ltl3ba`

is a tool that `ltldo`

already knows about, so there is a shorter way to run the above
command:

```
ltldo ltl3ba -F sample.ltl --stats='%f,%s,%t'
```

## Example: running `spin`

and producing HOA

Here is another example, where we use Spin to produce two automata in
the HOA format. Spin has no support for HOA, but `ltldo`

simply
converts the never claim produced by `spin`

into this format.

```
ltldo 'spin -f %s>%O' -f a -f GFa
```

HOA: v1 States: 2 Start: 0 AP: 1 "a" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc colored properties: deterministic --BODY-- State: 0 {0} [0] 1 State: 1 {0} [t] 1 --END-- HOA: v1 States: 2 Start: 0 AP: 1 "a" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete --BODY-- State: 0 [0] 1 [t] 0 State: 1 {0} [t] 0 --END--

Again, using the shorthands defined below, the previous command can be simplified to just this:

ltldo spin -f a -f GFa

## Syntax for specifying tools to call

The syntax for specifying how a tool should be called is the same as
in `ltlcross`

. Namely, the following sequences are available.

%% a single % %f,%s,%l,%w the formula as a (quoted) string in Spot, Spin, LBT, or Wring's syntax %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or Wring's syntax %O the automaton output in HOA, never claim, LBTT, or ltl2dstar's format

Contrarily to `ltlcross`

, it this not mandatory to specify an output
filename using one of the sequence for that last line. For instance
we could simply run a formula though `echo`

to compare different
output syntaxes:

ltldo -f 'p0 U p1' -f 'GFp0' 'echo %f, %s, %l, %w'

(p0) U (p1), (p0) U (p1), U p0 p1, (p0=1) U (p1=1) G(F(p0)), [](<>(p0)), G F p0, G(F(p0=1))

In this case (i.e., when the command does not specify any output
filename), `ltldo`

will not output anything.

As will `ltlcross`

, multiple commands can be given, and they will be
executed on each formula in the same order.

A typical use-case is to compare statistics of different tools:

ltldo -F sample.ltl 'spin -f %s>%O' 'ltl3ba -f %s>%O' --stats=%T,%f,%s,%e

Here we used `%T`

to output the name of the tool used to translate the
formula `%f`

as an automaton with `%s`

states and `%e`

edges.
If you feel that `%T`

has too much clutter, you can give each tool
a shorter name by prefixing its command with `{name}`

.

In the following example, we moved the formula used on its own line
using the trick that the command `echo %f`

will not be subject to
`--stats`

(since it does not declare any output automaton).

ltldo -F sample.ltl --stats=%T,%s,%e \ 'echo "#" %f' '{spin}spin -f %s>%O' '{ltl3ba}ltl3ba -f %s>%O'

Much more readable!

## Shorthands for existing tools

There is a list of existing tools for which `ltldo`

(and `ltlcross`

)
have built-in specifications. This list can be printed using the
`--list-shorthands`

option:

ltldo --list-shorthands

If a COMMANDFMT does not use any %-sequence, and starts with one of the following regexes, then the string on the right is appended. delag %f>%O lbt <%L>%O ltl2ba -f %s>%O ltl2(da|dgra|dpa|dra|ldba|na|nba|ngba) %f>%O ltl2dstar --output-format=hoa %[MW]L %O ltl2tgba -H %f>%O ltl3(ba|dra|hoa|tela) -f %s>%O modella %[MWei^]L %O spin -f %s>%O owl.* ltl2[bdeglnpr]+a\b -f %f>%O owl.* ltl2delta2\b -f %f owl.* ltl-utilities\b -f %f Any {name} and directory component is skipped for the purpose of matching those prefixes. So for instance '{DRA} ~/mytools/ltl2dstar-0.5.2' will be changed into '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %[MW]L %O'

Therefore you can type the following to obtain a Dot output (as
requested with `-d`

) for the neverclaim produced by `ltl2ba -f a`

.

ltldo ltl2ba -f a -d

digraph "" { rankdir=LR label="[Büchi]" labelloc="t" node [shape="circle"] I [label="", style=invis, width=0] I -> 0 0 [label="0", peripheries=2] 0 -> 1 [label="a"] 1 [label="1", peripheries=2] 1 -> 1 [label="1"] }

The `ltl2ba`

argument passed to `ltldo`

was interpreted as if you had
typed `{ltl2ba}ltl2ba -f %s>%O`

.

Those shorthand patterns are only tested if the command string does
not contains any `%`

character. They should always patch a prefix of
the command, ignoring any leading directory. This makes it possible
to add options:

ltldo ltl3ba 'ltl3ba -H2' -f GFa --stats='%T, %s states, %e edges'

ltl3ba, 2 states, 4 edges ltl3ba -H2, 1 states, 2 edges

## Transparent renaming

If you have ever tried to use `spin`

, `ltl2ba`

, or `ltl3ba`

, to translate
a formula such as `[]!Error`

, you have noticed that it does not work:

```
spin -f '[]!Error'
```

tl_spin: expected predicate, saw 'E' tl_spin: []!Error -------------^

All these tools are based on the same LTL parser, that allows only atomic propositions starting with a lowercase letter.

Running the same command through `ltldo`

will work:

```
ltldo spin -f '[]!Error' -s
```

never { accept_init: if :: (!(Error)) -> goto accept_init fi; }

(We need the `-s`

option to obtain a never claim, instead of the
default HOA output.)

What happened is that `ltldo`

renamed the atomic propositions in the
formula before calling `spin`

. So `spin`

actually received the
formula `[]!p0`

and produced a never claim using `p0`

. That never
claim was then relabeled by `ltldo`

to use `Error`

instead of `p0`

.

This renaming occurs any time some command uses `%s`

or `%S`

and the
formula has atomic propositions incompatible with Spin's conventions;
or when some command uses `%l`

or `%L`

, and the formula has
atomic propositions incompatible with LBT's conventions.

For `%f`

, `%w`

, `%F`

, and `%W`

, no relabeling is automatically
performed, but you can pass option `--relabel`

if you need to force it
for some reason (e.g., if you have a tool that uses almost Spot's
syntax, but cannot cope with double-quoted atomic propositions).

There are some cases where the renaming is not completely transparent.
For instance if a translator tool outputs some HOA file named after
the formula translated, the name will be output unmodified (since this
can be any text string, there is not way for `ltldo`

to assume it is
an LTL formula). In the following example, you can see that the
automaton uses the atomic proposition `Error`

, but its name contains a
reference to `p0`

.

ltldo 'ltl3ba -H' -f '[]!Error'

HOA: v1 name: "BA for [](!(p0))" States: 1 Start: 0 AP: 1 "Error" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc colored properties: deterministic --BODY-- State: 0 "accept_init" {0} [!0] 0 --END--

If this is a problem, you can always force a new name with the
`--name`

option:

ltldo 'ltl3ba -H' -f '[]!Error' --name='BA for %f'

HOA: v1 name: "BA for []!Error" States: 1 Start: 0 AP: 1 "Error" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc colored properties: deterministic --BODY-- State: 0 "accept_init" {0} [!0] 0 --END--

## Acting as a portfolio of translators

Here is a formula on which different translators produce Büchi automata of different sizes (states and edges):

ltldo ltl2ba ltl3ba 'ltl2tgba -s' -f 'F(a & Xa | FGa)' \ --stats='%T: %s st. (%n non-det.), %e ed.'

ltl2ba: 5 st. (2 non-det.), 9 ed. ltl3ba: 3 st. (1 non-det.), 4 ed. ltl2tgba -s: 3 st. (0 non-det.), 5 ed.

Instead of outputting the result of the translation of each formula by each
translator, `ltldo`

can also be configured to output the smallest
automaton obtained for each formula:

ltldo ltl2ba ltl3ba 'ltl2tgba -s' -f 'F(a & Xa | FGa)' --smallest

HOA: v1 States: 3 Start: 0 AP: 1 "a" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc --BODY-- State: 0 [t] 0 [0] 1 State: 1 [0] 2 State: 2 {0} [t] 2 --END--

Therefore, in practice, `ltldo --smallest trans1 trans2 trans3...`

acts like a portfolio of translators, always returning the smallest
produced automaton.

The sorting criterion can be specified using `--smallest`

or
`--greatest`

, optionally followed by a format string with
`%`

-sequences. The default criterion is `%s,%e`

, so the number of
states will be compared first, and in case of equality the number of
edges. If we desire the automaton that has the fewest states, and in
case of equality the smallest number of non-deterministic states, we
can use the following command instead.

ltldo ltl2ba ltl3ba 'ltl2tgba -s' -f 'F(a & Xa | FGa)' --smallest=%s,%n

HOA: v1 name: "F(a & Xa)" States: 3 Start: 1 AP: 1 "a" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete properties: deterministic terminal --BODY-- State: 0 {0} [t] 0 State: 1 [!0] 1 [0] 2 State: 2 [0] 0 [!0] 1 --END--

We can of course apply this on a large number of formulas. For
instance here is a more complex pipeline, where we take 11 patterns
from Dwyer et al. (FMSP'98), and print which translator among
`ltl2ba`

, `ltl3ba`

, and `ltl2tgba -s`

would produce the smallest
automaton.

genltl --dac=10..20 --format=%F:%L,%f | ltldo -F-/2 ltl2ba ltl3ba 'ltl2tgba -s' --smallest --stats='%<,%T'

dac-patterns:10,ltl2ba dac-patterns:11,ltl2ba dac-patterns:12,ltl2tgba -s dac-patterns:13,ltl2tgba -s dac-patterns:14,ltl2tgba -s dac-patterns:15,ltl2tgba -s dac-patterns:16,ltl2ba dac-patterns:17,ltl2tgba -s dac-patterns:18,ltl2ba dac-patterns:19,ltl3ba dac-patterns:20,ltl2ba

Note that in case of equality, only the first translator is returned.
So when `ltl2ba`

is output above, it could be (and it probably is, see
below) the case that `ltl3ba`

or `ltl2tgba -s`

are also producing
automata of equal size.

To understand the above pipeline, remove the `ltldo`

invocation. The
`genltl`

command outputs this:

genltl --dac=10..20 --format=%F:%L,%f

dac-patterns:10,G((p0 & !p1) -> (!p1 U (!p1 & p2))) dac-patterns:11,!p0 W (p0 W (!p0 W (p0 W G!p0))) dac-patterns:12,Fp0 -> ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | (!p1 U p0))))))))) dac-patterns:13,Fp0 -> (!p0 U (p0 & (!p1 W (p1 W (!p1 W (p1 W G!p1)))))) dac-patterns:14,G((p0 & Fp1) -> ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | (!p2 U p1)))))))))) dac-patterns:15,G(p0 -> ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | (!p1 W p2) | Gp1))))))))) dac-patterns:16,Gp0 dac-patterns:17,Fp0 -> (p1 U p0) dac-patterns:18,G(p0 -> Gp1) dac-patterns:19,G((p0 & !p1 & Fp1) -> (p2 U p1)) dac-patterns:20,G((p0 & !p1) -> (p2 W p1))

This is a two-column CSV file where each line is a description of the
origin of the formula (`%F:%L`

), followed by the formula itself
(`%f`

). The `ltldo`

from the previous pipeline simply takes its input
from the second column of its standard input (`-F-/2`

), run that
formula through the three translator, pick the smallest automaton
(`--smallest`

), and for this automaton, it display the translator that
was used (`%T`

) along with the portion of the CSV file that was before
the input column (`%<`

).

If you are curious about the actually size of the automata produced by
`ltl2ba`

, `ltl3ba`

, and `ltl2tgba -s`

in the above example, you can
quickly build a CSV file using the following pipeline where each
command append a new column. We wrap `ltl2ba`

and `ltl3ba`

with
`ltldo`

so that they can process one column of the CSV that is input,
and output statistics in CSV as output. `ltl2tgba`

does not need
that, as it already supports those features. In the resulting CSV
file, displayed as a table below, entries like `2s 4e 0d`

represent an
automaton with 2 states, 4 edges, and that is not deterministic. .
(We have a separate page with more examples of reading and writing CSV
files.)

echo input,ltl2ba,ltl3ba,ltl2tgba -s genltl --dac=10..20 --format=%F:%L,%f | ltldo -F-/2 ltl2ba --stats '%<,%f,%ss %ee %dd' | ltldo -F-/2 ltl3ba --stats '%<,%f,%>,%ss %ee %dd' | ltl2tgba -s -F-/2 --stats '%<,%>,%ss %ee %dd'

input |
ltl2ba |
ltl3ba |
ltl2tgba -s |
---|---|---|---|

dac-patterns:10 | 2s 4e 0d | 2s 4e 1d | 2s 4e 1d |

dac-patterns:11 | 5s 9e 1d | 5s 9e 1d | 5s 9e 1d |

dac-patterns:12 | 8s 29e 0d | 8s 20e 0d | 7s 17e 1d |

dac-patterns:13 | 8s 17e 0d | 8s 17e 0d | 6s 12e 1d |

dac-patterns:14 | 16s 62e 0d | 11s 33e 0d | 7s 19e 1d |

dac-patterns:15 | 10s 47e 0d | 10s 41e 0d | 6s 17e 1d |

dac-patterns:16 | 1s 1e 1d | 1s 1e 1d | 1s 1e 1d |

dac-patterns:17 | 4s 7e 0d | 4s 7e 0d | 3s 5e 1d |

dac-patterns:18 | 2s 3e 0d | 2s 3e 1d | 2s 3e 1d |

dac-patterns:19 | 4s 8e 0d | 3s 6e 0d | 3s 7e 1d |

dac-patterns:20 | 2s 4e 0d | 2s 4e 1d | 2s 4e 1d |

## Controlling and measuring time

The run time of each command can be restricted with the `-T NUM`

option. The argument is the maximum number of seconds that each
command is allowed to run.

When a timeout occurs a warning is printed on stderr, and no automaton
(or statistic) is output by `ltdo`

for this specific pair of
command/formula. The processing then continue with other formulas and
tools. Timeouts are not considered as errors, so they have no effect
on the exit status of `ltldo`

. This behavior can be changed with
option `--fail-on-timeout`

, in which case timeouts are considered
as errors.

For each command (that does not terminate with a timeout) the runtime
can be printed using the `%r`

escape sequence. This makes `ltldo`

an
alternative to `ltlcross`

for running benchmarks without any
verification.