[Spot] Time to decide inclusion

Alexandre Duret-Lutz adl at lrde.epita.fr
Mon Aug 2 00:42:39 CEST 2021

Hi Pierre,

Pierre Ganty <pierre.ganty at imdea.org> writes:

> I want to measure how much time it takes Spot to decide whether the
> language of the automaton A is contained in that of B.
> I've been using the following command
> ```
> autfilt '--stats=%r, %R' A.hoa --included-in=B.hoa
> ```
> I think I am not interpreting the results correctly because `--stats`
> reports very small numbers
> while adding `time` in front of the command reports much much larger
> numbers (several orders of magnitude larger).

This is a case where autfilt is optimized to process automata in

autfilt A1.hoa A2.hoa A3.hoa ...  --included-in=B.hoa

would output the subset of input automata included in B.hoa.

Spot's inclusion check is currently done by checking if A{1,2,3,...}.hoa
intersect the complement of B.hoa; but to do that, B.hoa needs only be
complemented once.  So in practice, the complement of B.hoa is computed
very early, while option --included-in is processed, before even loading
the input files A{1,2,3,...}.hoa.

Now the --stats option for measuring time only accounts for what occurs
after an input file has been parsed, so it won't measure the time spent
(once) complementing the B.hoa automaton.

Also since --included-in is a filter, autfilt will not output any stats
if the input is not included in B.hoa.  Therefore the usefulness of
--stats=%r for filters is a bit unclear in my opinion.  (I'm not sure
how we could tweak the interface to allow gathering statistics for
filters regardless of their outputs; suggestions welcome.)

> What's the right way to measure the time it takes Spot to decide the
> inclusion?

If you are unhappy with 'time autfilt...', for instance because you want
to exclude as much time not being spent doing inclusion checks, another
option would be to write a small Python script similar to the following

import spot
from sys import argv
from time import perf_counter as pc
A = spot.automaton(argv[1])
B = spot.automaton(argv[2])
before = pc()
print(B.contains(A), end=',')
after = pc()
print(after - before)

More information about the Spot mailing list