search

adl / hoaf

Hanoi Omega-Automata Format
13 stars 2 forks source link

HEADERNAME may not start with '-'. #37

Closed adl closed 9 years ago

adl commented 9 years ago

Identifier may not start with -, so that --ABORT-- may not be mistaken as an identifier. And although we state that HEADERNAME are like identifiers followed by :, the given regex allows them to start with -. This raises the question of whether --ABORT--: is a HEADERNAME, or if is --ABORT-- followed by :.

I suggest we simply fix the HEADERNAME definition to disallow a leading -. This is what is implemented in Spot 1.99a and jhoafparser 1.0.1 already. (But maybe there is a development version of jhoafparser that recognizes -: as a HEADERNAME by now, because this is one case in the test-suite developed by Joachim.)

kleinj commented 9 years ago

Yes, I think that allowing - at the start of the regex for HEADERNAME is just a typo. We should simply remove this. It's just a corner case that's tricky to implement in the parser and serves no purpose.