ltldo

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'

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

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!

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

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--

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'

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.