Habanero Phaser formalization

Phaser state operations

Welcome to our online interpreter of the Habanero formalization. Read on the developer notes for information about the implementation of this page.

The following two operations are translated automatically from our Coq formalization into Javascript.

Executable samples. The widget below is a Javascript REPL; input a Javascript expression to exercise our functions.

sandbox loading...

Happens-before visualization

The trace in the text box is rendered as a graph. Editing the trace automatically updates the graph.

Rendering of the trace:

Trace manipulation

We provide the following functions to handle a trace:

sandbox loading...


Our project is fully open source: Acknowledgments: