First, you should produce the finite state machine according to the logical architecture of your system, which usually described by UML interaction and State diagrams.
Then try to define the state variables of each objects in the interaction course, which can be obtained by refinning the key attributes of the corresponding classes.
So far, you will get a vivid description in your mind about how the state machine of each object transited according to the interactions,
now you can easily depicts this event driven discret system by TLA+.
You can get some exmaple from Specifying System