Automated Verification of Asynchronous Communicating Systems (with TLA+)

Elevator

The elevator may attempt obey the restricted floor access command before checking if an access badge was given.
Here are some ways to fix it:

Communication Model(s):

Peer (LTS):

Peer (LTS):

Properties: