Automated Verification of Asynchronous Communicating Systems
(with TLA+)
Model Checker
Help
Examples
Download
About
Conflict
Two processes attempt to read the same message (as seen in red), depending on which one succeed, the system will be able to terminate or not.
Add the
analyzed_by_pf,,a,P1LocalLock,P1aLock,P2GoAhead,P4LocalLock
communication model, then attempt to infer the correct channel priorities.
Communication Model(s):
async,,a,P1LocalLock,P1aLock,P2GoAhead,P4LocalLock
X
Peer (LTS):
1,2,!,P1LocalLock 2,3,!,P1aLock 3,4,?,a 4,5,?,a 5,6,?,P1LocalLock 6,7,!,P1aLock 7,8,?,P1aLock init,1
X
Peer (LTS):
1,2,?,a 2,3,!,a 3,4,!,a 4,5,!,P2GoAhead init,1
X
Peer (LTS):
1,2,!,a init,1
X
Peer (LTS):
1,2,!,P4LocalLock 2,3,?,P2GoAhead 3,4,?,P4LocalLock 4,5,?,P1aLock 2,1,?,P4LocalLock init,1
Add CCS peer
Add 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)