[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Defining a message in a communication protocol


I'm still early in my TLA+ career so I was hoping I could get some feedback on this definition of a Modbus packet. The idea is that given a string this operator checks that the length of the message is valid and that each character of the string correctly corresponds to a field of a Modbus packet. Modbus is pretty simple as far as protocols go, but is this a good way to do something like this?