Hello
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?
https://github.com/mssabr01/ICSVerifiedSoftwareProject/blob/master/Modbus/Modbus.tla
Thanks,
Mehdi