MCP Server for Alloy Modeling Language

#!/usr/bin/env node import { McpServer } from "@modelcontextprotocol/sdk/server/mcp.js"; import { StdioServerTransport } from "@modelcontextprotocol/sdk/server/stdio.js"; import { z } from "zod"; import alloy from "alloy-lang"; // Create MCP server const server = new McpServer({ name: "mcp-server-alloy", version: "1.0.0" }); // Tool: Execute Alloy code server.tool( "execute_alloy", "Execute Alloy modeling language code and return structured JSON results", { code: z.string().describe("The Alloy modeling language code to execute"), }, async ({ code }) => { try { const result = alloy.eval(code); // Type guard: check if result is an error if ('error' in result) { return { content: [ { type: "text", text: `Error executing Alloy code: ${result.error}` } ], isError: true }; } // TypeScript now knows result is AlloySuccessResult return { content: [ { type: "text", text: JSON.stringify(result, null, 2) } ] }; } catch (error) { const errorMessage = error instanceof Error ? error.message : String(error); return { content: [ { type: "text", text: `Error executing Alloy code: ${errorMessage}` } ], isError: true }; } } ); // Prompt: Help create Alloy models server.prompt( "create_alloy_model", "Generate an Alloy model based on a system description", { description: z.string().describe("Description of the system to model"), }, ({ description }) => ({ messages: [ { role: "user", content: { type: "text", text: `Create an Alloy model for the following system:\n\n${description}\n\nPlease include:\n1. Signature definitions\n2. Facts or predicates as needed\n3. A run or check command to verify the model` } } ] }) ); // Resource: Alloy documentation server.resource( "alloy-docs", "alloy://docs", async (uri) => ({ contents: [{ uri: uri.href, text: `# Alloy Language Documentation Alloy is a declarative modeling language for software design. ## Basic Syntax ### Signatures (sig) Define types/sets: \`\`\` sig Person { friends: set Person } \`\`\` ### Facts State constraints that must always hold: \`\`\` fact { all p: Person | p not in p.friends // no self-friendship } \`\`\` ### Predicates Define reusable constraints: \`\`\` pred connected(p1, p2: Person) { p2 in p1.friends or p1 in p2.friends } \`\`\` ### Run and Check - \`run {}\` finds instances satisfying constraints - \`check {}\` verifies assertions ## Example \`\`\` sig Node { edges: set Node } run { some n: Node | #n.edges > 1 } for 5 \`\`\` ## Resources - [Alloy Tools](https://alloytools.org/) - [Version 6 Overview](https://alloytools.org/alloy6.html) - [Documentation](https://alloytools.org/documentation.html) ` }] }) ); // Resource: Example Alloy models server.resource( "alloy-examples", "alloy://examples", async (uri) => ({ contents: [{ uri: uri.href, text: `# Alloy Example Models ## Simple Graph \`\`\`alloy sig Node { edges: set Node } // No self-loops fact { all n: Node | n not in n.edges } // Find a graph with a cycle run { some n: Node | n in n.^edges } for 5 \`\`\` ## File System \`\`\`alloy abstract sig Object {} sig File extends Object {} sig Dir extends Object { contents: set Object } // No cycles in directory structure fact { all d: Dir | d not in d.^contents } // Find a directory with files run { some d: Dir | some d.contents & File } for 5 \`\`\` ## State Machine \`\`\`alloy sig State { transitions: set State } pred reachable(s1, s2: State) { s2 in s1.*transitions } // Find a state machine with unreachable states run { some disj s1, s2: State | not reachable[s1, s2] } for 5 \`\`\` ` }] }) ); // Start the server const transport = new StdioServerTransport(); await server.connect(transport);