Hi all,
I did not find how to get the number of states (reachable or not) of an automaton using autfilt (in particular the `--stats` option). The option provided by `autfilt --stats` is for reachable states only. I did find a workaround with `--hoaf` which outputs the automaton in HOA format and then getting the number from the `States:` header. For the number of transitions (reachable or not) I don't have a workaround.
Since spot can compute these numbers easily, it seems handy (at least for me) to have a direct access to them thru the `--stats` interface.
Thank you, Pierre.
pierreganty@gmail.com writes:
I did not find how to get the number of states (reachable or not) of an automaton using autfilt (in particular the `--stats` option). The option provided by `autfilt --stats` is for reachable states only.
Hi Pierre
Thank you for the suggestion. Here is what you can now do with the latest development version [*].
Create a test automaton with an edge labeled by false in the middle:
$ ltl2tgba 'X[10]a' | sed '/State: 4/,/State: 5/s/[t]/[f]/' > test.hoa
Display count of [r]eachable, [u]unreachable, and [a]ll states:
$ autfilt --stats='%[r]s + %[u]s = %[a]s' test.hoa 7 + 5 = 12
The same syntax will work for %e and %t as well.
Best regards, Alexandre
[*] https://gitlab.lre.epita.fr/spot/spot/-/jobs/artifacts/next/browse?job=make-...
Thank you Alexandre!
I've played a bit with it and here is an observation.
If there is no `States: ` header in the file then all the numbers are computed based on the states listed in the body.
However if there is a `States: ` header then things are a bit different.
Warnings (many of them) will be displayed if, in the body, there are more states than the number declared in the header. In that case the total number `%[a]s` computed is the same as if the `States: ` header was absent.
If, in the body, there are less states than the number declared in the `States: ` header then the number of unreachable states will be "increased" so that the equality `%[r]s + %[u]s = %[a]s` holds. This behavior is consistent with the output of `--hoaf` which is "padding" the body part by declaring all these unreachable states explicitly.
On the other hand, `jhoafparser parse` returns a warning: `Warning: There are <number> states without definition` However `jhoafparser print` performs no padding unlike `autfilt --hoaf`.
I realize I might be the only one who got confused about this corner case. If there is somebody else then we now have a record in the mailing list. Perhaps the same warning should be output by `autfilt` so that the user knows something is going on when looking at `%[a]s`.
Pierre.
On Fri, 21 Oct 2022 at 17:37, Alexandre Duret-Lutz adl@lrde.epita.fr wrote:
pierreganty@gmail.com writes:
I did not find how to get the number of states (reachable or not) of an automaton using autfilt (in particular the `--stats` option). The option provided by `autfilt --stats` is for reachable states only.
Hi Pierre
Thank you for the suggestion. Here is what you can now do with the latest development version [*].
Create a test automaton with an edge labeled by false in the middle:
$ ltl2tgba 'X[10]a' | sed '/State: 4/,/State: 5/s/[t]/[f]/' > test.hoa
Display count of [r]eachable, [u]unreachable, and [a]ll states:
$ autfilt --stats='%[r]s + %[u]s = %[a]s' test.hoa 7 + 5 = 12
The same syntax will work for %e and %t as well.
Best regards, Alexandre
[*] https://gitlab.lre.epita.fr/spot/spot/-/jobs/artifacts/next/browse?job=make-...
Hi Pierre,
Pierre pierreganty@gmail.com writes:
On the other hand, `jhoafparser parse` returns a warning: `Warning: There are <number> states without definition` However `jhoafparser print` performs no padding unlike `autfilt --hoaf`.
Check out this discussion we had seven years ago while developing the format. It's about this exact point.
https://github.com/adl/hoaf/issues/39
[...] Perhaps the same warning should be output by `autfilt` so that the user knows something is going on when looking at `%[a]s`.
It seems like I wrote in the above issue that I considered the absence of warning as a bug. But somehow, when I implemented the diagnostic two days later, I only reported undeclared states if they were used somewhere.
https://gitlab.lre.epita.fr/spot/spot/-/commit/a83bde72b3b5e650dfae48cc12ac4...
I guess I should add a diagnostic for the unused ones as well. Thank for pointing this out.
Alexandre
-
Alexandre Duret-Lutz -
Pierre -
pierreganty＠gmail.com