Automated Verification of Asynchronous Communicating Systems
(with TLA+)
Model Checker
Help
Examples
Download
About
Communication Model(s):
async,,a,b,c,d,e,f,LLOCK1,LLOCK2,P2TP1L,P3TP1L
X
Peer (LTS):
1,2,!,d 2,3,!,e 3,4,!,f 4,5,?,P3TP1L init,1
X
Peer (LTS):
1,2,!,a 2,3,!,b 3,4,!,c 4,5,?,P2TP1L init,1
X
Peer (LTS):
1,2,!,LLOCK1 2,3,!,P2TP1L 3,4,?,a 4,5,?,b 5,6,?,c 6,7,?,LLOCK1 7,8,!,P2TP1L 8,9,?,P2TP1L 9,10,!,LLOCK2 10,11,!,P3TP1L 11,12,?,d 12,13,?,e 13,14,?,f 14,15,?,LLOCK2 15,16,!,P3TP1L 16,17,?,P3TP1L 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)