model-checking - SMV の CTL 仕様を確認する

Question

SMV で「EG (!s11included & !s10included)」をチェックしようとすると、false と報告され、次のように反例が示されます。これは、逆にこの CTL 仕様をサポートしていると思います。CTL 仕様に何か問題がありますか?

-- specification EG (!s11included & !s10included)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 9.1 <-
    s00included = TRUE
    s01included = TRUE
    s10included = FALSE
    s11included = FALSE