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.
hj.run(op,ph)performs a reduction step by applying operation
opto phaser state
ph. The function returns the new state or throws an exception if it cannot reduce.
hj.hb(ph1,ph2)returns true if, and only if, phaser
ph1happened before phaser
hj.par(ph1,ph2)returns true if, and only if, phaser
ph1may happen in parallel with
hj.wf(ph)returns true if, and only if, phaser
hj.wo(ph)returns true if, and only if, phaser
The trace in the text box is rendered as a graph. Editing the trace automatically updates the graph.
Rendering of the trace:
We provide the following functions to handle a trace:
trace()returns the trace from the input text box.
hj.run_trace(t)returns a phaser state from a given trace
tin the visualization widget.