The emacs mode for HOA, supports multiple automata in the same buffer.
C-c C-c will display the automaton at point: this works by copying the surrounding HOA automaton, and piping it to
autfilt and then
dot. Of course when
autfilt reports a syntax error, it will use line and column numbers that are relative to its input (just one automaton) so this will not make a lot of sense in the context of a buffer with many automata.
I would like to have an environment variable called
SPOT_PARSE_LOCATION that could be used to "shift" the diagnostics of the HOA or LTL parsers in this kind of contexts. The variable would be read by the command-line tools in
bin/ (I don't think it's good to have such a variable checked by the library), but the two parsers still need to provide the machinery necessary to shift error messages (or maybe simply set the original location).
For instance I'd like to have:
% autfilt -q < foo.hoa 3.9: syntax error, unexpected identifier 11.3: syntax error, unexpected ']' 11.2-3: ignoring this invalid label % SPOT_PARSE_LOCATION=bar:11.1 autfilt -q < foo.hoa bar:13.9: syntax error, unexpected identifier bar:21.3: syntax error, unexpected ']' bar:21.2-3: ignoring this invalid label
bar:11.1 describes the actual location of line 1, column 1 of the input.)