agent: Agent can reach EOS after having received something
The agent can reach EOS after performing one or more non-empty reads in its read loop, and then hitting EOS on the underlying stream. That means reached_eos is TRUE, but n_valid_messages is non-zero. Weaken the postcondition to reflect this.
Showing
Please register or sign in to comment