Doubt in temporal operator in CTL

Question

I have one doubt here 

Why A[a SB true] gives state set {s8} ?

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 :

Answer 1

That S8 is in the state set has nothing to do with SB but with A. Since S8 has no infinite paths, it satisfies a condition requiring all paths to satisfy the unsatisfiable condition.

You are right about the following assumptions:

1. [ whatever SB true ] is satisfied by no path
2. Precisely the deadend states satisfy A false

Comments

Thanks for this explanation.

Answer 2

This is because s8 is a deadend state. Note that deadend states satisfy all formulas A psi no matter what psi is (even A false is satisfied this way).

Comments

Thanks for this explanation.