SPECIFICATION SideAAuditSpecT11
INVARIANT SideAAuditInvariantT11
PROPERTY SideAAuditEventuallyHandoffT11