source: vis_dev/vis-2.1/examples/dcnew/dcnew.ltl @ 14

!G!((int.state=go3)+(int.state=go4));
G F(!(int.state=go3)*!(int.state=go4));
G((interpretation = go) -> (train = absent));
G((interpretation = go) -> !(train = present2));