vacp2p/formalities
1
0
Fork 0
mirror of https://github.com/vacp2p/formalities.git synced 2026-01-10 06:17:55 -05:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
formalities/MVDS
History
Dean Eigenmann 0a4927f3be Update README.md
2019-11-06 14:49:05 +01:00
..
models
travis (#3)
2019-11-06 14:48:38 +01:00
Makefile
travis (#3)
2019-11-06 14:48:38 +01:00
MVDS.tla
travis (#3)
2019-11-06 14:48:38 +01:00
README.md
Update README.md
2019-11-06 14:49:05 +01:00

README.md

MVDS

TLA+ specification of the MVDS spec.

Model Checking

  • SpecOK: This Model runs with 2 Nodes and uses the AllMessagesDelivered state constraint. It proves that messages are eventually received by peers if requested.
Reference in New Issue View Git Blame Copy Permalink