FSM for a set of invariants of the form "A always precedes B". The FSM enters a permanent success state upon encountering an A, and enters a permanent failure state upon encountering a B. This reflects the fact that the first of the two events encountered is the only thing relevant to the failure st
source not stored for this graph (policy: none)
nothing calls this directly
no outgoing calls
no test coverage detected