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.

Communication Model(s):

async,,Floor,AccessBadge,RestrictedFloor

XPeer (LTS):

1,2,?,Floor 1,3,?,AccessBadge 3,4,?,Floor 3,4,?,RestrictedFloor init,1

XPeer (LTS):

1,2,!,Floor 1,3,!,AccessBadge 3,4,!,Floor 3,4,!,RestrictedFloor init,1

Add CCS peerAdd LTS peer

Properties:

• All peers terminate.
• The network ends up empty.
• No peer goes into a forbidden state.
• No (global) deadlocks

Test properties Infer all constraint sets (pessimistic) Infer one constraint set (pessimistic) Infer some constraint sets (optimistic) Infer one constraint set (optimistic) Infer all constraint sets (pessimistic, listened) Infer one constraint set (pessimistic, listened) Infer some constraint sets (optimistic, listened) Infer one constraint set (optimistic, listened)