Skip to content

more PSL simplifications

I think the following simplifications are correct and simple to implement:

{e[*0..j]}<>->f  =  {e[*1..j]}<>->f
{e[*0..j]}[]->f  =  {e[*1..j]}[]->f

It matters for example in this random PSL formula:

./ltl2tgba -H '(({p1[*0..1]}[]-> 0) R XFp0)'
./ltl2tgba -H '(({p1[*1..1]}[]-> 0) R XFp0)'

The former produces a deterministic automaton, while the second produces a non-deterministic one.