First, break a tiny scene on purpose. Only after the instrument catches the planted fault may it touch a real text.
Enter Alice. Alice speaks. Exit Alice. Then plant one impossible speech.
No result yet. The Shakespeare trace stays untrusted.
An unchanged Spin safety assertion refuses a second entrance for an actor already onstage. The rival set scanner does the same. That is a valid counterexample to Folger's encoded event stream, then a printing witness changes its meaning.
Run the calibration to establish the instrument, then inspect the two typed events.
The strict adapter reads the attribute, not the verb in the displayed words. Mining the prose after seeing the result would make the test self-confirming.
Select a trace step.
Both actors move onstage. No property has failed.
Every counterexample must pass through the edition, the printing witness, and the adapter. These are different kinds of result. An empty class stays empty.
The machine record asserts more than its displayed words and independent witness support. In this case, an action carries an entrance type.
A different early witness supplies a different entrance, exit, or boundary. The resulting state trace belongs to the selected witness.
More than one textually allowed trace survives the source audit, and at least one allowed path violates the property.
The model checker is unchanged. The interpretation is not neutral. Almost every consequential choice lives in the adapter.
QUESTION MALFORMED pending live recomputation.
Before stage directions, the same pinned Spin binary checks its native kind of object. The canonical two-process Peterson model is safe. A mutant that bypasses the wait reaches both processes in the critical section. Full models and trails are shipped with the verifier.
loading recorded Spin summary
| Input | Treatment | Consequence |
|---|---|---|
| stage type, who, xml:id, n | used | typed transition, referents, evidence link |
| speech who | used | speech event |
| displayed words | evidence only | never repairs a strict transition |
| business, delivery, modifier, sound | dropped from strict transitions | retained for audit |
| blocking, props, costume, meter | outside model | no claim |
Hand-supplied conventions include clearing the stage at Folger scene boundaries, deduplicating repeated IDs, refusing to flatten groups, allowing explicit offstage locations, distinguishing bodies from actors and manifestations from embodied identities, keeping ranged deaths nondeterministic, and leaving unresolved mixed directions unknown.
For a fixed trace, a set and a loop are equivalent to the safety assertions. That simpler scanner was chosen before the result and agrees on the first failing event. The positive mutation appends Alice speaking after her exit. The negative mutation changes only dialogue text, which the strict structural trace must ignore.
for event in trace: ENTER(c) requires c not present EXIT(c) requires c present SPEAK(c) requires c present or explicitly audible offstage
Folger Shakespeare XML
Folger Digital Texts, edited by Barbara A. Mowat and Paul Werstine, encoded by Michael Poston and Rebecca Niles. CC BY-NC 3.0. Changes: stage events extracted and normalized for this visualization.
Bodleian First Folio, Cymbeline
Digital facsimile of the Bodleian First Folio of Shakespeare's plays, Arch. G c.7, Bodleian Libraries, University of Oxford. CC BY 3.0.
Internet Shakespeare Editions, Hamlet Q2
Copyright text used under the site's educational, non-profit permission. It is not presented as openly licensed.
Spin model checker
Unmodified Linux binary, version ?, pinned by SHA-256 in the research manifest. BSD 3-Clause.
Eric Johnson's ACTORS report already processed electronic plays to track entrances, exits, and who was simultaneously onstage. This page's narrower contribution is provenance-aware triage: carry a formal counterexample back through the adapter and printing witness before deciding what kind of result it is.
A clean fixed trace does not prove a production physically possible. A flag does not prove Shakespeare made a continuity error. Offstage voices, corpses, ghosts, disguise, doubling, group identities, ranged deaths, scene divisions, and unsegmented mixed directions need explicit states or must remain unresolved. This page verifies one focal encoding artifact and one witness-sensitive boundary. It does not claim whole-corpus verification.