LTL2BA parser has problem parsing skip

[mhtb32]

Hi!

The module ltl2ba.py cannot parse skip, which is equivalent to true. Did you not include the parsing rule for skip on purpose?
I can make a pull request if you mind.

[slivingston]

I do not understand. @mhtb32 can you give an example to illustrate?

Also, can you tell me which version of Tulip that you are using? You can find it via

python -c 'import tulip; print(tulip.__version__)'

[mhtb32]

I was using ltl2ba.py file separately like:

python ltl2ba.py

and I replaced the default formula

f = '[] !s && <> (a || c) && <> (b U c)'

with

f = 'p1 <> p2'

Then I received this error:

ERROR:__main__:Syntax error at skip

, Since ltl2ba command produces skip in the output.

I have a fork of your code using sly package(a successor to ply), in which I have a parsing rule for skip to create a self transition like this:

    @_('state ":" SKIP')
    def clause(self, p):
        u = p.state
        self.automaton.add_transition({(u, u, '1')})
        return u, p.SKIP

I wish this help.