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
Using ltldo
the above command can be reduced to this:
ltldo 'ltl3ba -f %s>%O' -F sample.ltl --stats='%f,%s,%t'
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 -f a -f GFa 'spin -f %s>%O'
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 words, then the string on the right is appended. lbt <%L>%O ltl2ba -f %s>%O ltl2dstar --output-format=hoa %[MW]L %O ltl2tgba -H %f>%O ltl3ba -f %s>%O ltl3dra -f %s>%O ltl3hoa -f %f>%O modella %[MWei^]L %O spin -f %s>%O Any {name} and directory component is skipped for the purpose of matching those prefixes. So for instance '{DRA} ~/mytools/ltl2dstar-0.5.2' will changed into '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %[MR]L %O'
Therefore you can type just
ltldo ltl2ba -f a -d
to obtain a Dot output (as requested with -d
) for the neverclaim
produced by ltl2ba -f a
.
digraph G { rankdir=LR 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
.
The shorthand is only used if it is the first word of an command
string that does not use any %
character. 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--
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
.
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.