8. Miolingo🔗

Miolingo is a language-pronunciation trainer: a learner practises a queue of phrases by recording them, has each recording checked against the target language's phonetic transcription, and collects words into a vocabulary. This chapter models it as a bigraphical reactive system (Milner, The Space and Motion of Communicating Agents, 2009; Jensen and Milner, TR-580, 2004) with a server region and one region for each browser session, and states the invariants proved of it, over reachability by checked reactions and user actions, and two shape invariants that are CONDITIONAL on a hypothesis about every rule of the family, which is not proved. A user action here is any well-formed request placed anywhere, which over-approximates the user and is not yet related to a transition of the library. Everything else is in Miolingo/: the first model and its rules (Model.lean), the families of the later models (D1.lean, Main.lean, App.lean), the generators and their completeness (Main.lean, AppInv.lean), the scenarios (ModelChecks.lean, MainChecks.lean), and the shape of a state by parents and the per-rule checks (Shape.lean; definitions and tests only).

1. 8.1. The signature and its rules
2. 8.2. The first models
3. 8.3. The main model
4. 8.4. The app model
5. 8.5. Two models: the present one and the normalised one
6. 8.6. Scenarios and the explorer