execute_alloy
Execute Alloy modeling language code to perform formal verification and software modeling, returning structured JSON results for analysis.
Instructions
Execute Alloy modeling language code and return structured JSON results
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| code | Yes | The Alloy modeling language code to execute |
Implementation Reference
- src/index.ts:21-60 (handler)Handler function that executes the provided Alloy code using alloy.eval(code), processes the result (success or error), and returns structured content with JSON for success cases and error messages.
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 }; } } ); - src/index.ts:18-20 (schema)Zod schema defining the input parameter 'code' for the execute_alloy tool.
{ code: z.string().describe("The Alloy modeling language code to execute"), }, - src/index.ts:16-60 (registration)Registration of the execute_alloy tool using server.tool(), including name, description, input schema, and inline handler function.
"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 }; } } ); - src/alloy-lang.d.ts:1-35 (helper)Type definitions for the 'alloy-lang' module, defining interfaces for Alloy results used in the handler for type guarding and processing.
declare module 'alloy-lang' { export interface AlloyInstance { messages: unknown[]; skolems: Record<string, unknown>; state: number; values: Record<string, unknown>; } export interface AlloySuccessResult { duration: number; incremental: boolean; instances: AlloyInstance[]; localtime: string; loopstate: number; sigs: Record<string, unknown>; timezone: string; utctime: number; } export interface AlloyErrorResult { error: string; } export type AlloyResult = AlloySuccessResult | AlloyErrorResult; export function evalRaw(alloyProgram: string): string; export function eval(alloyProgram: string): AlloyResult; const alloy: { evalRaw: typeof evalRaw; eval: typeof eval; }; export default alloy; }