LTL Tool - clarification

Question

How do we check this diagram in the tool for F G[a SU b]?

I tried below 2 methods and I want to know which one is correct:

1) G F((!a &!b) & X(!a & b)) -> (F G[a SU b]) 

2) G((!a &!b) & X(!a & b)) -> (F G[a SU b]) 

I get confused on how to enter state transitions in tool when there is a Globally holding transiton of s0 -> s1, s1->s0.

Answer 1

Neither is correct. Better try

!a &!b & G (!a &!b & X(!a & b) | !a & b & X(!a & !b)) -> F G[a SU b] 

or

!a &!b & G ((!a &!b -> X(!a & b)) & (!a & b -> X(!a & !b))) -> F G[a SU b]