(Generally) How to specify asynchronous action with side effects using logic equations
One way to model your example is through program graphs. (See chapter 2 in Principles of Model Checking.) What you can do is model all() as one program, which synchronizes on action 'data' with another program that runs concurrently to all(), let's call it listen(). listen() will have an initial state where it waits until it can synchronize with the all() on action 'data'.

Once you have these two models (or more for bigger examples) you can interleave them, which is a construction that contains all the possible states. Program graph interleaving also preserves shared variables (so globalPacketCounter will be updated correctly) unlike interleaving on transition systems. Though I would be careful about them, since atomicity is not implicit in the models. You can read more about critical actions in section 2.2.2. of the book.

After interleaving of PGs you construct a transition system, which you can transform to a logical equation. And there you have it.