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:
Replace async by fifo11.
Add the fifo11,,AccessBadge,RestrictedFloor communication model.
Add the
channel_priorities,"BLOCKS <- {<<{""AccessBadge""},""RestrictedFloor"">>}",AccessBadge,RestrictedFloor
communication model. It does not ends up with an empty network, though.
Add the analyzed_by_pf,,AccessBadge,Floor,RestrictedFloor communication model, then
attempt to infer the correct channel priorities.