2 Aug
2021
2 Aug
'21
12:42 a.m.
Hi Pierre,
Pierre Ganty <pierre.ganty(a)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
batches:
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
#!/usr/bin/python3
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)