arche/arche-lang-model

arche-lang, described in arche-lang

This example is the toolchain in this repository written as a model: its parts, the data passing between them, how a build runs, what each generator makes, the editor, where each part runs, the design decisions, and the tests that verify what the language promises. Each part has a source naming the real files, written from the arche-lang folder, so the model is also a map of the code.

archec build examples/arche-lang/main.arche -o out    # then: arche --project out
archec doc   examples/arche-lang/main.arche --html -o arche-lang.html
archec gen   examples/arche-lang/main.arche --target nusmv -o smv   # the two machines, for NuSMV

In VS Code, open main.arche. The diagram shows the Toolchain system, and you open a block to see the parts inside it.

Read it in this order

| File | What it says | |---|---| | main.arche | The Toolchain system: the command line, the editor, the compiler, the generators, the exporters, the analyses, the rewriters, the libraries, the importers, the Arche app and the outside tools, and what flows between them. | | data.arche | What the stages hand each other: source text, tokens, the file AST, the Program, diagnostics, the Arche project, generated files, LSP messages, source edits. Each message names the TypeScript type that carries it. | | pipeline.arche | The compiler, stage by stage: host → lexer → parser → loader → checker → emitter → validator → writer. Its state machine is one archec build, and shows where a build stops and why. | | generators.arche | archec gen: the dispatcher, the readers the generators share, and each generator with the --target values it answers. | | exchange.arche | Importers (an Arche project, SysML v2, ReqIF, FMU), exporters (ReqIF, SysML, FMI, LaTeX, HTML), analyses (timing, model checking, studies, certification, TARA), rewriters (fmt, simplify, extract, merge) and the libraries with the board store. | | editor.arche | The VS Code extension and its language server. The server's state machine is what happens after a keystroke: a quick check, then a full build once typing pauses. | | cli.arche | Every archec command, and the function in src/cli/*.ts that runs it. | | outside.arche | The Arche app and the other tools arche-lang reads from or writes for. | | scenarios.arche | Five walk-throughs as sequence diagrams: archec build, archec gen --target embassy, typing in VS Code, dragging a block, archec board add. | | decisions.arche | Why it is built this way: one table for the language, contextual keywords, recovery at the next line, pure generators, a formatter that never moves a token, Arche's own code for Arche's verdicts, builds judged by meaning, the compiler run in the editor's process. | | requirements.arche, verification.arche | What the toolchain promises, and the test file of npm test that verifies each promise. | | qualification.arche | archec in a safety project: the use cases a team may rely on (archec qualify --use gen-c), the requirements on archec that refine each, and, in verification.arche, the tests that show them — what archec qualify writes the ISO 26262-8 and DO-330 kit from ([qualification](../../docs/qualification.md)). | | deployment.arche | The three node programs (dist/cli.js, the extension, the language server) on the developer's machine. | | canvas.arche | Where the blocks sit in the diagrams. |

It stays true

test/selfmodel.test.js fails when the model and the code part ways:

• the model builds with no error and no warning;
• every source exists, and every .ts module in src/, vscode/src/ and bridge/ is named by one;
• the generators' prop target values are exactly archec gen's targets;
• Cli has one operation per command in src/cli.ts, named after the function that runs it;
• the built project, imported back with archec import, builds into the same project.

So when you add a module, a generator or a command, give it a place here.

Limits

• The model works at the level of modules, not functions. A part names files, not lines.
• The state machines are untimed. NuSMV checks that every state is reachable,

but cannot prove that a build always ends: the generated model lets a state wait for ever, and a leads to property would need fairness.

• The test plan's cases name the npm test files. Arche's simulator does not run them.
• The Arche app is shown as one block. Its own repository is not described here.