Skip to content

Latest commit

 

History

History

MVDS

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
models
models
 
 
MVDS.tla
MVDS.tla
 
 
Makefile
Makefile
 
 
README.md
README.md
 
 

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.