Your last paragraph was an important remark which I was missing so thank you very much for pointing that out Prof. Schneider. Now if we ignore the trace part, after all, since according to model checker, the formula S1 is satisfied in state s1 and the formula S2 is not satisfied on any state, can we say the structure I drew is sufficient to show these 2 formulas are not equivalent or still not?