Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.
My Solution Satisfy S2 but not S1, Is my solution correct?
I am afraid that your solution is not correct. We can quickly rewrite your formulas to equivalent CTL formulas:
Then the model checker computes: