Skip to content

Algorithm examples in PlusCal, the algorithm language of Lamport's TLA+

Notifications You must be signed in to change notification settings

raghavendrahg/PlusCal-Examples

This branch is up to date with quux00/PlusCal-Examples:master.

Folders and files

NameName
Last commit message
Last commit date

Latest commit

1369a5c · Apr 14, 2015

History

10 Commits
Apr 10, 2015
Apr 6, 2015
Apr 6, 2015
Apr 5, 2015
Apr 7, 2015
Apr 5, 2015
Apr 6, 2015
Apr 13, 2015
Apr 13, 2015
Apr 13, 2015
Apr 13, 2015
Apr 14, 2015
Apr 14, 2015
Apr 5, 2015
Apr 13, 2015
Apr 13, 2015
Apr 6, 2015

Repository files navigation

Overview

These are examples of algorithms written in PlusCal, the algorithm language for Leslie Lamport's TLA+ algorithm specification system.

These have been created in the TLA+ Toolbox, so most of the files are supporting files for running in the Toolbox and using the TLC algorithm verification checker.

The important (non-auto-generated) files for review are those that end in .tla, such as Euclid/Euclid.tla and HourClock/HourClock.tla.

I've written the part above the line \* BEGIN TRANSLATION and the PlusCal code falls between the (* and *) comment markers, starting with the --algorithm XXX indicator.

About

Algorithm examples in PlusCal, the algorithm language of Lamport's TLA+

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published