Hello TLA+ experts,
I recently wrote a peer-to-peer protocol specification for an industrial protocol. In order to simplify the number of states, I purposely left out from the specification message exchanges between the client and server when the communication line is in idle state. However, the specification goes into deadlock. When I include the idle state message exchange, I have a state space explosion until the JVM heap ran out of memory.
In your opinion, without specifying the idle message exchange, can I still argue that the specification meets its liveness property even though it goes into deadlock.
Thank you
- Wan -