This is an old revision of the document!
Welcome to the TLA+ Wiki
This wiki is community driven, and aims to become a useful resource for TLA+ users.
TLA+
'
---------------------- MODULE HourClock ----------------------
EXTENDS Naturals
VARIABLE hr
HCini == hr \in (1 .. 12)
HCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 1
HC == HCini /\ [][HCnxt]_hr
--------------------------------------------------------------
THEOREM HC => []HCini
==============================================================
'
Contributing
Contributions to the wiki are very welcome!
To contribute you will need to register an account on this website (it only requires a username, email and password). Should you need it, TLA+ was created by Leslie Lamport.
You can learn the syntax from here. Markdown is not supported.
Browse Topics:
fponzi