`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 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 contain 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 no 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 (`%s`

),
and in case of equality the smallest number of non-deterministic
states (`%n`

), 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 to a stream 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`

), runs that
formula through the three translators, picks the smallest automaton
(`--smallest`

), and for this automaton, it displays 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 actual 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 appends 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.