Source State Machine :: Requirement Under Verification (RUV) :: CTLSPEC EF( .state = _s2 ) <span class="derived">Variables</span> Source State Machine :: Requirement Under Verification (RUV) :: CTLSPEC EF( .state = _s2 ) <span class="derived">Variables</span>