/*
         * Formula As Typed: <>message_delivered
         * The Never Claim Below Corresponds
         * To The Negated Formula !(<>message_delivered)
         * (formalizing violations of the original)
         */

never {    /* !(<>message_delivered) */
accept_init:
T0_init:
        if
        :: (! ((message_delivered))) -> goto T0_init
        fi;
}