I have one doubt here
Why A[a SB true] gives state set {s8} ?
![](https://q2a.cs.uni-kl.de/?qa=blob&qa_blobid=6290260271911489573)
In SB both RHS and LHS cannot coexist means they can't both be true, so here why s8 is included when a is true and other term is always true?
Is it because of Universal Path quantifier because it considers deadend state as well so thatswhy it is there ?
Tool Solution :
![](https://q2a.cs.uni-kl.de/?qa=blob&qa_blobid=3115175465113365956)