8.6. Scenarios and the explorer🔗

The scenario theorems of the first and the main model (capturing a word twice leaves one row seen twice, concurrent captures end in a single row, a check after switching the target language is recorded in the new language, and others) are PROVED, kernel-checked in Miolingo/ModelChecks.lean and Miolingo/MainChecks.lean, modules built on demand; a compiled regression of each is in the library (TESTED). The app model's scenarios are TESTED by compiled evaluation (#guard) against a stand-in outside world, and are not kernel-checked. The explorer, an executable that explores the app model breadth-first by user actions (edits that place a request) and checked occurrences, and writes the states to an interactive page, checks on every explored state the state invariants of Miolingo/Shape.lean (W1, W2, I3, L1 to L5), on every rule fired the per-rule checks (R1 to R10), and that every enabled flag of the screen agrees with the simulator, and stops at the first failure; its results are TESTED.