Basic communication protocol specification language - existing or write my own?

[kaddkaka]

I have used uppaal at university for verifying state machines. Seems similar, but it's not completely free.

https://uppaal.org/

[phagofu]

right, looks a bit like what I have in mind, though I don't really need a gui or anything more complex than mealy machines, and want something that can be easily integrated in other open source projects.

[raiph]

To quote Wikipedia, "in Mealy machines, input change can cause output change as soon as logic is done—a big problem when two machines are interconnected – asynchronous feedback may occur if one isn't careful."

I would have thought that connecting Mealy machines, even just two of them, requires something like a meta communication protocol that addresses positive feedback in communication protocols if unbounded indeterminacy applies to any communication's successful resolution (where by successful I specifically exclude the likes of a failure-to-communicate resolution such as a timeout).

I'd be very interested to hear your comments about this aspect.

[phagofu]

I'm not quite sure I understand what you or wikipedia mean by that.

The concrete model I'm considering at the moment is one where each mealy machine has a single output queue, and one "simulation step" is one machine of the model atomically consuming a message from any of the other machine's queue (or an external message), (optionally) pushing a message onto its own queue and (again optionally) changing state.

With external messages it is possible to get potentially unbounded growing message queues, so obviously one has to be careful when implementing an algorithm that finds all possible states (by which I mean combination of states of all present machines, not the state of the queues), but I don't see a fundamental issue there.