Skip to main content
Glama
CHASE MCP Server

CHASE MCP Server

by chase-cps

saturate

Read-onlyIdempotent

Transforms an assume-guarantee contract into its equivalent (A, A -> G) form for refinement, consistency, compatibility, and realizability checks.

Instructions

Saturation: the equivalent contract (A, A -> G). The other operations saturate their operands themselves.

Tool call template

Replace each placeholder with a value matching the input schema. Only required parameters are included; add optional parameters as needed.

{
  "id": 1,
  "jsonrpc": "2.0",
  "method": "tools/call",
  "params": {
    "arguments": {
      "contract": "<contract>"
    },
    "name": "saturate"
  }
}

Input Schema

NameRequiredDescriptionDefault
nameNo
contractYes

Schema Changelog

Changes observed during successful MCP inspections.

  1. Changed1 schema field changedv0.7.0
    • addedInput schema / $defs / ContractSpec / properties / constants
      Added value: +{
      +  "additionalProperties": {
      +    "anyOf": [
      +      {
      +        "type": "integer"
      +      },
      +      {
      +        "type": "number"
      +      }
      +    ]
      +  },
      +  "description": "Named constants: name -> value; the formulas use the names (repair changes them)",
      +  "title": "Constants",
      +  "type": "object"
      +}
  2. Changed4 schema fields changedv0.4.2
    • changedInput schema / $defs / ContractSpec / properties / inputs / additionalProperties / anyOf
      Previous value: -[
      -  {
      -    "enum": [
      -      "bool",
      -      "real"
      -    ],
      -    "type": "string"
      -  },
      -  {
      -    "maxItems": 2,
      -    "minItems": 2,
      -    "prefixItems": [
      -      {
      -        "type": "integer"
      -      },
      -      {
      -        "type": "integer"
      -      }
      -    ],
      -    "type": "array"
      -  }
      -]New value: +[
      +  {
      +    "enum": [
      +      "bool",
      +      "real"
      +    ],
      +    "type": "string"
      +  },
      +  {
      +    "maxItems": 2,
      +    "minItems": 2,
      +    "prefixItems": [
      +      {
      +        "type": "integer"
      +      },
      +      {
      +        "type": "integer"
      +      }
      +    ],
      +    "type": "array"
      +  },
      +  {
      +    "pattern": "^(signed |unsigned )?word\\[[1-9][0-9]*\\]$",
      +    "type": "string"
      +  }
      +]
    • changedInput schema / $defs / ContractSpec / properties / inputs / description
      Previous value: -"Input variables: \"bool\", [low, high], or \"real\""New value: +"Input variables: \"bool\", [low, high], \"real\", or \"word[n]\" (\"signed word[n]\")"
    • changedInput schema / $defs / ContractSpec / properties / outputs / additionalProperties / anyOf
      Previous value: -[
      -  {
      -    "enum": [
      -      "bool",
      -      "real"
      -    ],
      -    "type": "string"
      -  },
      -  {
      -    "maxItems": 2,
      -    "minItems": 2,
      -    "prefixItems": [
      -      {
      -        "type": "integer"
      -      },
      -      {
      -        "type": "integer"
      -      }
      -    ],
      -    "type": "array"
      -  }
      -]New value: +[
      +  {
      +    "enum": [
      +      "bool",
      +      "real"
      +    ],
      +    "type": "string"
      +  },
      +  {
      +    "maxItems": 2,
      +    "minItems": 2,
      +    "prefixItems": [
      +      {
      +        "type": "integer"
      +      },
      +      {
      +        "type": "integer"
      +      }
      +    ],
      +    "type": "array"
      +  },
      +  {
      +    "pattern": "^(signed |unsigned )?word\\[[1-9][0-9]*\\]$",
      +    "type": "string"
      +  }
      +]
    • changedInput schema / $defs / ContractSpec / properties / outputs / description
      Previous value: -"Output variables: \"bool\", [low, high], or \"real\""New value: +"Output variables: \"bool\", [low, high], \"real\", or \"word[n]\" (\"signed word[n]\")"
  3. First observedv0.3.1

TDQS

C2.9/5.0
Behavior3/5

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

Annotations already declare readOnlyHint=true, idempotentHint=true and openWorldHint=false, so the safety profile is covered and the description does not need to repeat it. The description adds that the output is an equivalent contract and that composition with other ops already performs saturation, which is useful behavioral context. It says nothing about failure modes (e.g. what happens if the contract is malformed) or what the returned object looks like.

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?

Two short sentences with no filler, and the identification of the operation is front-loaded. The terse symbolic notation (A, A -> G) is dense but earns its place for a specialist audience, though it could have been unpacked in one plain clause at little cost.

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

Completeness2/5

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

There is no output schema, so the description must explain what is returned; it only says "the equivalent contract", without stating the return shape or whether the input contract is echoed, modified, or replaced. Combined with fully undocumented top-level parameters and no error behavior, the definition is under-specified for a transformation tool, even accounting for annotations that cover safety.

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

Parameters2/5

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

Top-level schema description coverage is 0%: neither the `name` parameter nor the `contract` parameter is documented at the top level, and the description mentions neither. The nested ContractSpec does document its own fields, but the meaning of `name` (is it the name of the resulting saturated contract?) is left entirely ambiguous, and the description does not compensate for that gap.

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

Purpose3/5

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

The description names the operation (saturation) and characterizes the result as "the equivalent contract (A, A -> G)", which is meaningful to a domain expert but never states a verb or that a new contract is returned. An agent can tell it is distinct from siblings like repair or simplify, but only by decoding the notation rather than from a plain statement of what it does.

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?

"The other operations saturate their operands themselves" implicitly tells the agent that an explicit call is rarely needed except for standalone saturation, which is genuine usage guidance. However, it never says when you would want standalone saturation, nor names a specific sibling alternative or prerequisite, leaving the agent to infer the trigger condition.

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