Hi Pierre, Pierre Ganty <pierre.ganty@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)