Transient states with meaningful properties (e.g., a state reachable by a FAIL transition from which an ONLINE transition can immediately be taken) currently cause either an error or are ignored when translating to a CTMC. The translators need to correctly mark the state following the ONLINE transition as having experience a transient failure. The model-checker queries should take this new marking into account.
Transient states with meaningful properties (e.g., a state reachable by a FAIL transition from which an ONLINE transition can immediately be taken) currently cause either an error or are ignored when translating to a CTMC. The translators need to correctly mark the state following the ONLINE transition as having experience a transient failure. The model-checker queries should take this new marking into account.