SPECIFICATION SideBAuditSpecT11
INVARIANT SideBAuditInvariantT11
PROPERTY SideBAuditEventuallyHandoffT11