GitHub - gshanemiller/tla-examples: Model Checking for Industrial Programmers with TLA+ · GitHub
/" data-turbo-transient="true" />
Skip to content
Search or jump to...
Search code, repositories, users, issues, pull requests...
-->
Search
Clear
Search syntax tips
Provide feedback
--><br>We read every piece of feedback, and take your input very seriously.
Include my email address so I can be contacted
Cancel
Submit feedback
Saved searches
Use saved searches to filter your results more quickly
-->
Name
Query
To see all available qualifiers, see our documentation.
Cancel
Create saved search
Sign in
/;ref_cta:Sign up;ref_loc:header logged out"}"<br>Sign up
Appearance settings
Resetting focus
You signed in with another tab or window. Reload to refresh your session.<br>You signed out in another tab or window. Reload to refresh your session.<br>You switched accounts on another tab or window. Reload to refresh your session.
Dismiss alert
{{ message }}
gshanemiller
tla-examples
Public
Notifications<br>You must be signed in to change notification settings
Fork
Star<br>12
main
BranchesTags
Go to file
CodeOpen more actions menu
Folders and files<br>NameNameLast commit message<br>Last commit date<br>Latest commit
History<br>6 Commits<br>6 Commits
pluscal-assert
pluscal-assert
pluscal-assert1
pluscal-assert1
pluscal-diningphil
pluscal-diningphil
pluscal-increment
pluscal-increment
pluscal-light
pluscal-light
pluscal-nondeterminc
pluscal-nondeterminc
pluscal-pathfinder
pluscal-pathfinder
pluscal-peterson
pluscal-peterson
pluscal-rpc
pluscal-rpc
pluscal-stub
pluscal-stub
pluscal-wfair
pluscal-wfair
tla-elevator
tla-elevator
tla-increment
tla-increment
tla-queue
tla-queue
tla-stub
tla-stub
README.md
README.md
tla.pdf
tla.pdf
tla2tools.jar
tla2tools.jar
View all files
Repository files navigation
Summary
This repository contains TLA model examples for use with the accompanying document 'tla.pdf'. Links are provided therein to directories in this repository
Pre-requisites
See 'tla.pdf' section 4 for install instructions. If you have a recent JAVA runtime installed you're already done
Run Environment
Tested on Ubuntu 13.3.0 with the 25.0.1 JAVA compiler, and OpenJDK 25.0.1+8-Ubuntu-124.04 runtime
Running Models
Every example comes with a Makefile. Execute make to run verification
About
Model Checking for Industrial Programmers with TLA+
Topics
model-checking
tla
formal-models
tla-specification
Resources
Readme
Uh oh!
There was an error while loading. Please reload this page.
Activity
Stars
12<br>stars
Watchers
watching
Forks
forks
Report repository
Releases
No releases published
Packages
Uh oh!
There was an error while loading. Please reload this page.
Contributors
Uh oh!
There was an error while loading. Please reload this page.
Languages
TLA<br>88.4%
Makefile<br>11.6%
You can’t perform that action at this time.