Keep -> and <-> when converting a formula to Spin's syntax
Right now the same function removes xor
, ->
and <->
from LTL formulas. Because Spin does not support xor
, this function is called before we print a formula using the Spin syntax, but it incidentally removes the supported ->
and <->
as well.
For Spin we should probably just rewrite a xor b
as !(a <-> b)
.