CHASE MCP Server

Overview Schema Source Related Servers Discussions Admin

parse_smv

Read-onlyIdempotent

Parse an SMV model's specifications into a contract: inputs (IVAR), outputs (VAR), and guarantees for is_implementation checks.

Instructions

Read an SMV model with its specifications (LTLSPEC, INVARSPEC; text or a file path) as a contract: the IVAR are its inputs, the VAR its outputs (a VAR with no ASSIGN is still an output: write an input as IVAR), the specifications its guarantees. is_implementation with smv set to the model (its specifications are left out) checks it. An enumerated type is read as the integers 0, 1, ... in the order written (in the traces too), a DEFINE in a specification as its definition. Not read: CTL, past operators, and a DEFINE written with case ... esac; the error says which.

Tool call template

This tool declares no required parameters. Add optional parameters from the input schema as needed.

{
  "id": 1,
  "jsonrpc": "2.0",
  "method": "tools/call",
  "params": {
    "arguments": {},
    "name": "parse_smv"
  }
}

Input Schema

Name	Required	Description	Default
`path`	No
`text`	No

Schema Changelog

Changes observed during successful MCP inspections.

Addedv0.7.0Nov 2, 2026

TDQS

A3.9/5.0

Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Well beyond the readOnly/idempotent annotations, the description discloses the semantic contract (IVAR = inputs, VAR = outputs, a VAR without ASSIGN is still an output, specifications = guarantees), the reading conventions (enumerated types become 0,1,... in written order, a DEFINE in a specification is inlined), and the hard limits (CTL, past operators, and DEFINE with case...esac are not read, and the error names which). That is exactly the behavioral context annotations cannot carry.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Dense and front-loaded: the core definition, then the contract interpretation, then the downstream check, then the limitations. The nested parentheses make it run-on in places, but every clause carries real information and nothing is filler.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

For a parser with no output schema and no annotations beyond safety hints, the description covers what the model means, what is rejected, and how the result is consumed downstream. The remaining gap is the shape of the returned spec object and the text-vs-path precedence rule.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 0% and neither parameter has a description, so the description must compensate. It partially does by indicating the model may come as text or a file path, but it never states whether both may be supplied, which wins if both are given, or what happens when both are null (required count is 0).

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose4/5

Does the description clearly state what the tool does and how it differs from similar tools?

States a specific verb and resource (read/parse an SMV model with its LTLSPEC/INVARSPEC specifications) and immediately frames the result as a contract with inputs, outputs and guarantees. The SMV format name implicitly separates it from parse_sva, parse_c and parse_spec, but no sibling is named to make the distinction explicit.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Usage is implied by the follow-up sentence: pass the parsed model to is_implementation via `smv`, with the model's own specifications left out. Beyond that there is no guidance on when to choose this over parse_spec or the other parsers, and no statement about when it should not be used.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.