https://github.com/afonsonf/tlaplus-graph-explorer

Skip to content
 
Sign up Sign up

  * Why GitHub?
    Features -
      + Mobile -
      + Actions -
      + Codespaces -
      + Packages -
      + Security -
      + Code review -
      + Project management -
      + Integrations -
      + GitHub Sponsors -
      + Customer stories-
  * Team
  * Enterprise
  * Explore
      + Explore GitHub -

    Learn and contribute

      + Topics -
      + Collections -
      + Trending -
      + Learning Lab -
      + Open source guides -

    Connect with others

      + The ReadME Project -
      + Events -
      + Community forum -
      + GitHub Education -
      + GitHub Stars program -
  * Marketplace
  * Pricing
    Plans -
      + Compare plans -
      + Contact Sales -
      + Education -

[                    ] [search-key]

  *  
    #
    In this repository All GitHub |
    Jump to |

  * No suggested jump to results

  *  
    #
    In this repository All GitHub |
    Jump to |
  *  
    #
    In this user All GitHub |
    Jump to |
  *  
    #
    In this repository All GitHub |
    Jump to |

Sign in Sign up Sign up
{{ message }}

afonsonf / tlaplus-graph-explorer

  * Notifications
  * Star 50
  * Fork 0

A static web application to explore and animate TLA+ states.

MIT License
50 stars 0 forks
Star
Notifications

  * Code
  * Issues 0
  * Pull requests 0
  * Actions
  * Projects 0
  * Security
  * Insights

More

  * Code
  * Issues
  * Pull requests
  * Actions
  * Projects
  * Security
  * Insights

main
Switch branches/tags
[                    ]
Branches Tags
Nothing to show
{{ refName }} default View all branches
Nothing to show
{{ refName }} default
View all tags
1 branch 0 tags
Go to file Code
 
Clone
HTTPS GitHub CLI
[https://github.com/a]

Use Git or checkout with SVN using the web URL.

[gh repo clone afonso]

Work fast with our official CLI. Learn more.

  * Open with GitHub Desktop
  * Download ZIP

Launching GitHub Desktop

If nothing happens, download GitHub Desktop and try again.

Go back

Launching GitHub Desktop

If nothing happens, download GitHub Desktop and try again.

Go back

Launching Xcode

If nothing happens, download Xcode and try again.

Go back

Launching Visual Studio

If nothing happens, download the GitHub extension for Visual Studio
and try again.

Go back

Latest commit

@afonsonf
afonsonf first version
...
d1dfc24 Apr 7, 2021
first version
d1dfc24

Git stats

  * 2 commits

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
example-gifs
first version
Apr 7, 2021
examples/ceph-consensus-3mon
first version
Apr 7, 2021
expr-parser
first version
Apr 7, 2021
src
first version
Apr 7, 2021
LICENSE
Initial commit
Apr 5, 2021
README.md
first version
Apr 7, 2021
View code
TLA+ Graph Explorer Examples Example 1 - Missionaries and Cannibals
Example 2 - Ceph consensus algorithm How to use Related tools

README.md

 TLA+ Graph Explorer

This is a static web application to explore and animate a TLA+ state
graph.

The application works by parsing a dot file generated by a TLA+
specification and then having visual representations to more easily
understand and go through the reachable states.

The application is written to support big dot files and not load the
whole file into memory. This is achieved by reading the file in
chunks and storing only the location of the node in the file. The
structure to save the nodes location, in my experiments, takes around
1/10th of the dot file size.

 Examples

 Example 1 - Missionaries and Cannibals

Spec: https://github.com/tlaplus/Examples/tree/master/specifications/
MissionariesAndCannibals.

[example1]

 Example 2 - Ceph consensus algorithm

Spec: https://github.com/afonsonf/ceph-consensus-spec.

[example2]

 How to use

The application is in the folder src.

The default way to represent a state is showing the pretty printed
version, as shown previously in example 1.

The representation of a state can be personalized by changing the
function drawState in the file tla-state.js. An example of a
personalized state representation is shown in the example 2 and the
source code is in examples/ceph-consensus-3mon.

To help create a personalized representation of a state, the
application comes with a parser that parses a tla+ state into
JavaScript structures. The parser definition is in folder expr-parser
and example usage of the parser (function parseVars) can be found at
examples/ceph-consensus-3mon.

 Related tools

The ideas behind this tool were inspired by TLA+ Animation Module and
Runway.

About

A static web application to explore and animate TLA+ states.

Resources

Readme

License

MIT License

Releases

No releases published

Packages 0

No packages published

Languages

  * JavaScript 58.5%
  * CSS 14.7%
  * HTML 14.2%
  * Yacc 12.6%

  * (c) 2021 GitHub, Inc.
  * Terms
  * Privacy
  * Security
  * Status
  * Docs

 

  * Contact GitHub
  * Pricing
  * API
  * Training
  * Blog
  * About

You can't perform that action at this time.
You signed in with another tab or window. Reload to refresh your
session. You signed out in another tab or window. Reload to refresh
your session.