Markdown with embedded TLA+

[frankshearar]

VS Code's Alloy extension gives me the ability to embed Alloy code inside a Markdown file. This allows me to produce a model and nicely laid out documentation in the same file. (At the moment I write a prose description of what the model simulates, but I have no ability to add structure to this, like emphasis or sections or whatever.

I'm imagining a UX like where model appears inside tlaplus fenceposts. I could still run "Check with TLC" and all the other TLA+ commands in VS Code, just within a .md file instead of a .tla file. Either the configuration could stay in a .cfg file or appear within the file in a tlaplus fence.