This is an old revision of the document!
PHP's gd library is missing or unable to create PNG images
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