Related Work

Runway's specification language is heavily influenced by TLA+ and Murphi. Like Runway, TLA+ integrates several tools. It includes a specification language, a model checker, and a proof system (that can mechanically verify proofs). TLA+ specifications are written in untyped logic and mathematics, whereas Runway specifications closely resemble computer programs, more familiar to industry engineers. Murphi is a model checker which could be very accessible to industry engineers. Unfortunately, its code does not seem to be actively maintained (the best version seems to be CMurphi). Like Runway, Murphi's language is strongly typed and rule-oriented. Murphi rules have explicit preconditions written in Boolean logic, whereas Runway rules are simply considered inactive when they do not change any state. We think this makes Runway more flexible for complex preconditions, despite being more difficult to implement efficiently.

Runway's emphasis on visualization/animation is heavily influenced by The Secret Lives of Data and RaftScope. The Secret Lives of Data is a step-by-step guided tour of Raft (more visualizations may be added later), created by Ben Johnson. RaftScope is an interactive visualization of Raft that I (Diego Ongaro) created for my PhD defense. Both run in the browser and are built using JavaScript and SVG. These projects helped me see the value of visualization for distributed systems. The Secret Lives of Data's step-by-step approach is well-suited to self-guided learning; we plan to support similar usage in Runway. Runway is a generalization of the RaftScope idea, making it easier to visualize other systems and algorithms. The Runway visualization of Raft is roughly equivalent to RaftScope. Of course, Runway goes beyond that, as a specification, model checking, and simulation tool.

Unprocessed

This is a dumping ground for potentially related projects. They're sorted alphabetically by project name. The idea is we should introduce what they are, where to find more info, and how they're related to Runway, then move them into nice categories to be created above.