6.8. The explorer🔗

The explorer is an executable built on the simulator: from the start state of an application model it follows user actions and the reactions the simulator finds, up to a bound, merges states whose renumberings by a colour-refinement heuristic are equal as data, and writes the graph for a web page that draws it. A user action (a click) is an edit of the state that places a request; it is not a reaction and no theorem covers it. Each reaction edge is a checked occurrence. The renumbering used for merging is not canonical and is not passed through the renumbering check. The explorer has no theorem of its own, and what it reports is TESTED.