Connection check
verified live · 27h ago
endiagram-mcp
EN Diagram — structural verification for concurrent systems. Pure math, no AI.
Tools
7
GitHub stars
—
Installs / wk
—
Licence
—
Transport
streamable-http, stdio
Last checked
27h ago
Tools & capabilities
7 toolsRead from the running server on 27h ago.
compose
linkssourcesource_asource_bsubsystem
How do parts combine, or how does a part stand alone? Merge mode (source_a + source_b + links): declare which entities in A are the same as entities in B; the combined graph is wir… How do parts combine, or how does a part stand alone? Merge mode (source_a + source_b + links): declare which entities in A are the same as entities in B; the combined graph is wired via string-equality of shared names. Extract mode (source + subsystem): pull a named subsystem out as standalone EN with boundary inputs/outputs, actors, and locations. Valid subsystem names come from structure's `subsystems` field — call structure on the source first to discover them. See the server instructions for EN language syntax.
equivalent
patchsourcesource_asource_b
Are two systems the same, or what changes if I change this one? Compare mode (source_a + source_b): structural differences, edit distance, spectral equivalence. isCospectral=true m… Are two systems the same, or what changes if I change this one? Compare mode (source_a + source_b): structural differences, edit distance, spectral equivalence. isCospectral=true means identical graph structure up to relabeling — topologically the same despite different names, actors, or locations. Evolve mode (source + patch): dry-run a change, shows diff plus new/lost bridge nodes. Patch has three directive types — plain EN statement adds an action; a line starting with `-` (and not containing `do:`) removes the named action; a statement whose action name matches an existing one replaces the original. See the server instructions for EN language syntax.
invariant
rulessource*
What's always true — automatic findings and on-demand checks. Automatic outputs: conservationLaws (weighted entity sums constant across executions), sustainableCycles (T-invariants… What's always true — automatic findings and on-demand checks. Automatic outputs: conservationLaws (weighted entity sums constant across executions), sustainableCycles (T-invariants — action sequences returning to start state), depletableSets (entity groups whose simultaneous depletion is irreversible), behavioral.deficiency (0 means structure fully determines dynamics), behavioral.isReversible, behavioral.hasUniqueEquilibrium. On-demand via `rules`: encode domain-specific claims and verify them against the graph — this is how to check things the topology alone can't see (precedence, coverage, centrality bounds, resilience). See the rules parameter for supported sentence shapes.
live
source*
Can it deadlock? Can entities overflow? isStructurallyLive means every siphon contains a trap — no structural deadlock possible. uncoveredSiphons are entity groups that can drain p… Can it deadlock? Can entities overflow? isStructurallyLive means every siphon contains a trap — no structural deadlock possible. uncoveredSiphons are entity groups that can drain permanently, with the actors and locations affected. isStructurallyBounded means no entity can accumulate without limit. unboundedCycles are action sequences that could cause overflow. See the server instructions for EN language syntax.
reachable
to*from*source*defense_nodes
Can X reach Y? Follows directed data flow first; falls back to undirected. `from` and `to` accept entity names or action names (resolved against the program). Path shows each step… Can X reach Y? Follows directed data flow first; falls back to undirected. `from` and `to` accept entity names or action names (resolved against the program). Path shows each step with actor and location. locationCrossings counts boundary transitions. defense_nodes checks if guards cover all paths; coverage.fullCoverage=false means unguarded routes exist. See the server instructions for EN language syntax.
render
typeviewcolorthemeisDarkoutput
+4
SVG or PNG diagram. Only call when user explicitly asks to visualize. The rendered image is delivered to the user, not injected into the model's context. See the server instruction… SVG or PNG diagram. Only call when user explicitly asks to visualize. The rendered image is delivered to the user, not injected into the model's context. See the server instructions for EN language syntax.
structure
nodesource*detect_findings