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

Protocol specification liveness

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 -